[Benchmark] add link

[elecball]

This PR implements GNU link and adds specifications, proofs, tests, and a fuzzer generator. (#11)

Change and scope

• Task ID and kind: link, coreutils.
• Tested state: ac71c9b336a5897caf5964b0267cafa1c101be3b.
• Working directory and environment: /workspace/dafnyutils, Ubuntu 24.04 development container.
• Tool versions: Dafny 4.11.1+1eb9fc5fa2661483de151ff85b21eed0b695878a, Python 3.12.3.
• Changed boundaries: utility specification, implementation, tests, documentation, and fuzzer input generation. Shared IO contracts and comparison rules are unchanged.
• GNU source: coreutils/src/link.c at 2cf491412c199e2211880ec3f4ba387026638a33.
• Source URL/license: https://www.gnu.org/software/coreutils/, GPL-3.0-or-later.
• Scope and model/API revision: see bench/utils/link/link.md.

Question	Answer
What is the source?	Pinned GNU coreutils/src/link.c
What is accepted?	Two pathnames; --help, --version, long-option abbreviations, and --
What is observed?	stdout, stderr, exit status, and filesystem effects
Which environment?	Linux, C locale, current user permissions
Which errors matter?	Missing/extra operands, invalid options, missing/empty paths, existing targets, missing target parents, directories, and permission denial
What is trusted?	Existing shared parser, filesystem, errno-text, argument/path quoting, and stream contracts
What is proved?	Core behavior satisfies LinkSpec.Spec under the shared contracts

Options left out due to IO.dfy

None.

1. Test results

• make -C bench/utils/link test: 28 passed, 3 proof tests deselected; exit 0.
• Cases cover successful hard-link creation, inode identity, operand errors, missing sources, existing targets, missing target parents, option handling, and diagnostic quoting for special characters.
• ruff check bench/utils/link/Tests.py, ruff format --check bench/utils/link/Tests.py, and Rust formatting passed.

2. Fuzzing results

• Generator: 21 fixed scenarios plus generated inputs.
• Required command: python3 tools/coreutils_fuzzer/run.py fuzz 'link' --seeds 1,7,19 --iterations 1000.
• Seeds 1, 7, and 19: 1,000 matches each, with zero mismatches, timeouts, incomplete coverage, or other errors; exit 0.

3. Verification results

• make -C bench/utils/link verify: 253 verified, 0 errors; exit 0.
• python3 -m benchmarks validate 'link': valid; exit 0.
• 3 proof tests passed.
• make check TASK=link: link: checks passed; exit 0.

Progress notes

• Completed: implementation, specification, proof connection, tests, documentation, fuzzer registration, and GNU diagnostic quoting.
• Limitations: the shared CreateHardLinkSpec does not guarantee filesystem preservation on failure. Behavior for symbolic-link sources is unspecified by GNU. Non-UTF-8 pathname bytes and closed-stream or /dev/full parity are not established.
• Remaining review: whether to strengthen the shared failure contract.
• Artifact: bench/utils/link/link.md.

AI usage

This contribution was based primarily on my existing GNU unlink benchmark implementation. Codex reviewed and revised the adaptation for link.

[duncan020313]

안녕하세요. 기여에 참여해 주셔서 감사합니다.

다음 수정 사항들을 반영해 주세요

1. merge commit을 만들지 마세요.

rebase를 사용하여 merge commit이 생성되지 않도록 해 주시기 바랍니다.

2. 다음 불일치들을 수정해 주세요

구현과 명세를 수정하고, fuzzing 시나리오에도 추가하여 동일한 시드로 1000회 fuzzing 결과를 첨부해 주시기 바랍니다.

a. 모호한 상황에서의 에러 메시지 출력

link --=

GNU:

link: option '--=' is ambiguous; possibilities: '--help' '--version'
Try 'link --help' for more information.

Dafny:

link: option '--=' is ambiguous
Try 'link --help' for more information.

b. 입력 인자에서 유니코드 처리 오류

link '-é' 2>&1 | od -An -tx1 -v

-GNU:   27 c3 27
+Dafny: 27 c3 a9 27

GNU는 잘못된 옵션의 첫 번째 바이트만 출력하지만, 구현해 주신 Dafny link는 é의 전체 UTF-8 인코딩을 출력합니다.

[duncan020313]

fuzzing 결과도 다시 첨부해 주시기 바랍니다.
출력을 그대로 복사해서 올려주세요

---

Please attach the fuzzing results again.
Copy the output exactly as it is and upload it.

[elecball]

$ python3 tools/coreutils_fuzzer/run.py fuzz 'link' --seeds 1,7,19 --iterations 1000 
selected utilities: link
==> utility: link
    seed: 1

=== Coreutils fuzz campaign ===
Configuration
  Utility    : link
  Seed       : 1
  Budget     : 1000 iterations
  Reference  : "/workspace/dafnyutils/_build/coreutils/src/link" (Native)
  DUT        : "/workspace/dafnyutils/_build/bench/link_bench.dll" (DotnetDll)
  Case source: generated (scenarios, random inputs and corpus mutation)
  Limits     : max_args=10 max_fs_entries=12 timeout=10s shrink_attempts=250
  Comparison : stderr=included workdir=per-iteration
  Image      : dafnyutils-coreutils-fuzzer:latest
  Identity   : uid=1000 gid=1000
  Metrics    : disabled
  Image ID   : sha256:982cb85174e4d05682d034aa026ae71fa235341fb7167d8aff55003352b20fac
  Option pool: 2 (discovered)
Coverage
  Option coverage: singles 2/2 (100.0%), pairs 1/1 (100.0%)
  Semantic coverage: buckets 21/27 (77.8%), extra=0, missing: fs:file-content-changed, fs:file-removed, fs:mode-changed, fs:target-changed, fs:time-changed, stdin:consumed
Results
  Iterations : requested=1000 submitted=1000 completed=1000 not_started=0 unfinished=0
  Outcomes   : match=1000 mismatch=0 timeout=0 other_errors=0
  Elapsed    : 197.46s
  Status     : PASS - all requested iterations matched; no mismatch found
=== End campaign ===
    seed: 7

=== Coreutils fuzz campaign ===
Configuration
  Utility    : link
  Seed       : 7
  Budget     : 1000 iterations
  Reference  : "/workspace/dafnyutils/_build/coreutils/src/link" (Native)
  DUT        : "/workspace/dafnyutils/_build/bench/link_bench.dll" (DotnetDll)
  Case source: generated (scenarios, random inputs and corpus mutation)
  Limits     : max_args=10 max_fs_entries=12 timeout=10s shrink_attempts=250
  Comparison : stderr=included workdir=per-iteration
  Image      : dafnyutils-coreutils-fuzzer:latest
  Identity   : uid=1000 gid=1000
  Metrics    : disabled
  Image ID   : sha256:982cb85174e4d05682d034aa026ae71fa235341fb7167d8aff55003352b20fac
  Option pool: 2 (discovered)
Coverage
  Option coverage: singles 2/2 (100.0%), pairs 1/1 (100.0%)
  Semantic coverage: buckets 21/27 (77.8%), extra=0, missing: fs:file-content-changed, fs:file-removed, fs:mode-changed, fs:target-changed, fs:time-changed, stdin:consumed
Results
  Iterations : requested=1000 submitted=1000 completed=1000 not_started=0 unfinished=0
  Outcomes   : match=1000 mismatch=0 timeout=0 other_errors=0
  Elapsed    : 200.78s
  Status     : PASS - all requested iterations matched; no mismatch found
=== End campaign ===
    seed: 19

=== Coreutils fuzz campaign ===
Configuration
  Utility    : link
  Seed       : 19
  Budget     : 1000 iterations
  Reference  : "/workspace/dafnyutils/_build/coreutils/src/link" (Native)
  DUT        : "/workspace/dafnyutils/_build/bench/link_bench.dll" (DotnetDll)
  Case source: generated (scenarios, random inputs and corpus mutation)
  Limits     : max_args=10 max_fs_entries=12 timeout=10s shrink_attempts=250
  Comparison : stderr=included workdir=per-iteration
  Image      : dafnyutils-coreutils-fuzzer:latest
  Identity   : uid=1000 gid=1000
  Metrics    : disabled
  Image ID   : sha256:982cb85174e4d05682d034aa026ae71fa235341fb7167d8aff55003352b20fac
  Option pool: 2 (discovered)
Coverage
  Option coverage: singles 2/2 (100.0%), pairs 1/1 (100.0%)
  Semantic coverage: buckets 21/27 (77.8%), extra=0, missing: fs:file-content-changed, fs:file-removed, fs:mode-changed, fs:target-changed, fs:time-changed, stdin:consumed
Results
  Iterations : requested=1000 submitted=1000 completed=1000 not_started=0 unfinished=0
  Outcomes   : match=1000 mismatch=0 timeout=0 other_errors=0
  Elapsed    : 196.34s
  Status     : PASS - all requested iterations matched; no mismatch found
=== End campaign ===

세 시드에 대해 전부 통과하였습니다.