[Benchmark] add unlink

[elecball]

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

Change and scope

• Task ID and kind: unlink, coreutils.
• Tested state: 82f02b29e3cfcc0e9a247bee64e8e25e7b63dc20 plus the quoting implementation, specification, and test changes now committed in 01aa8fa3fa9cc3d5bb98d2a1d3dfa34e657bbe0b.
• 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/unlink.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/unlink/unlink.md.

Question	Answer
What is the source?	Pinned GNU coreutils/src/unlink.c
What is accepted?	One pathname; --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, 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 UnlinkSpec.Spec under the shared contracts

Options left out due to IO.dfy

None.

1. Test results

• make -C bench/utils/unlink test: 28 passed, 3 proof tests deselected; exit 0.
• Cases cover regular files, symlinks, dangling links, hard links, operand errors, directory rejection, permission denial, option handling, and diagnostic quoting for special characters.
• ruff check ., ruff format --check ., and Rust formatting passed.

2. Fuzzing results

• Generator: 24 fixed scenarios plus generated inputs.
• Required command: python3 tools/coreutils_fuzzer/run.py fuzz 'unlink' --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/unlink verify: 216 verified, 0 errors; exit 0.
• python3 -m benchmarks validate 'unlink': valid; exit 0.
• 3 proof tests passed.
• make check TASK=unlink: unlink: checks passed; exit 0.

Progress notes

• Completed: implementation, specification, proof connection, tests, documentation, fuzzer registration, and GNU diagnostic quoting.
• Limitations: the shared UnlinkPathSpec does not guarantee filesystem preservation on failure. 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/unlink/unlink.md.

AI usage

Codex helped with source analysis, implementation guidance, code and proof review, and writing Dafny tests, the fuzzer, and documentation. I reviewed and revised the changes.

[duncan020313]

여기에는 unlink의 man page (--help)를 작성해 주셔야 합니다.
다른 유틸리티를 참고해 주세요.

---

Here, you need to write the man page (--help) for unlink.
Please refer to the other utilities for guidance.

[duncan020313]

상태가 있는 프로그램의 명세를 작성할 때는 변하는 상태를 작성하는 것도 중요하지만, 변하지 않는 것을 명시적으로 작성하는 것도 중요합니다. 예를 들어, --help 옵션을 주었을 때 파일 시스템에 어떠한 영향도 없어야 한다는 것이 명세에 작성되어 있어야 합니다. 그렇지 않으면 --help옵션을 주었을 때 파일을 삭제해 버리는 잘못된 unlink구현도 올바른 것으로 증명 가능한 상태가 되어 우리가 원하는 만큼의 완전성(completeness)이 보장되지 않는 명세가 됩니다.

다음 두 자료를 참고해 주세요:

• Frame Problem
• Separation Logic

참고로, 우리의 목표는 IO modeling이 허용하는 범위 내에서 최대한 상세한명세를 작성하고 구현과 증명을 작성하는 것입니다.

여기서 상세한 명세란,

• 안전성(soundness): 올바른 실행 trace를 명세에 대입했을 때 수락하는가?
• 완전성(completeness): 잘못된 실행 trace를 명세에 대입했을 때 거부하는가?
  에서 안전성을 만족하면서도 동시에 최대한 완전한 명세를 작성하는 것을 목표로 하시면 됩니다.
  제공해 드린 fuzzer는 안전성을 확인하는 도구라고 생각해 주시면 됩니다.

---

When writing specifications for stateful programs, it is important not only to specify what changes, but also to explicitly specify what must remain unchanged. For example, the specification should state that providing the --help option must have no effect on the file system. Otherwise, an incorrect implementation of unlink that deletes a file when given the --help option could still be proven correct, resulting in a specification that does not provide the level of completeness we want.

Refer to the following materials:

• Frame Problem
• Separation Logic

Our goal is to write the most detailed specification possible within the scope supported by the current IO modeling, and then provide the corresponding implementation and proof.
By a detailed specification, we mean aiming for a specification that satisfies soundness while being as complete as possible:

• Soundness: Does the specification accept a correct execution trace when the trace is checked against it?
• Completeness: Does the specification reject an incorrect execution trace when the trace is checked against it?

The provided fuzzer can be considered a tool for checking soundness.

[elecball]

피드백에 따라 unlink 명세에 파일시스템 불변 조건을 추가했습니다. --help나 인자 오류처럼 삭제를 시도하지 않는 경우는 증명됩니다. 하지만 UnlinkPath가 실패했을 때 beforeFs == afterFs라는 조건을 추가하면 증명할 수 없습니다.
현재 IOContract.UnlinkPathSpec에는 실패 시 파일시스템 보존이 명시되어 있지 않습니다. 반면 ln에서 사용하는 CreateSymlinkContractFields에는 !ok ==> fs2 == fs가 명시되어 있습니다.
실패 시 불변 조건을 공유 IO 계약에 추가하는 것이 적절한지, 아니면 현 모델의 범위에 맞춰 unlink 명세에서 제외하는 것이 적절한지 질문드립니다

[elecball]

추가적으로, ln 퍼저에서도 특수문자가 포함된 경로의 오류 출력이 GNU와 달랐습니다. unlink에서는 따옴표가 들어간 인자에서 같은 종류의 차이가 났습니다. 이런 오류 문구의 인용 처리도 이번 PR에서 처리해야 하는지 질문드립니다.

[duncan020313]

안녕하세요. UnlinkPath 의 실패 케이스에 대해서는 현재 모델에서 모델링하지 않으므로 따로 다뤄 주지 않으셔도 됩니다.

따옴표 사례의 경우 unlink에 대해서만 문제를 해결해 주시면 됩니다.

---

Hello. Since the UnlinkPath failure is not currently modeled in the model, you do not need to handle it separately.

In the case of the quotation marks, you only need to resolve the issue with unlink.