[Benchmark] add sort

[suhdonghwi]

Draft for scope review before implementation (refs #28).

This PR adds the sort scaffold and its scope in bench/utils/sort/sort.md. This PR uses the sort row of TODOLIST.csv without changes: Whole-line C byte order; -r, -u, -s, -c, -C, -z; file/stdin operands, stdout output (check mode uses regular files)..

Change and scope

• Task ID(s) and kind: sort, coreutils.
• Tested commit and any uncommitted changes: 8bd205f, no uncommitted changes.
• Working directory, OS/container image and tool versions: /workspace/dafnyutils in the contributor dev container (Ubuntu 24.04), dafny-benchmark 4.11.1+1eb9fc5fa, Python 3.12.3, ruff 0.15.12.
• Changed specification / implementation / proof / evaluator / dataset boundaries: scope document and metadata only. The Dafny modules and tests are scaffold stubs.
• GNU source revision, URL/license and upstream test scenarios: coreutils 2cf491412 (v9.10-13-g2cf491412), src/sort.c, https://www.gnu.org/software/coreutils/, GPL-3.0-or-later. Upstream test scenarios will be selected during implementation.
• Accepted input/environment/observation scope and trusted model/API revision: see sort.md. Linux, C locale, TZ=UTC0; stdout, stderr, exit status and standard input consumption; bench/core at a98d11a.

Question	Answer
What is the source?	Pinned coreutils/src/sort.c at 2cf491412
What is accepted?	-r -u -s -c -C -z and their long spellings, grouped short options, --, --help and --version; zero or more file operands or -; arbitrary bytes in newline or NUL records. Check mode takes one regular file.
What is observed?	Exact stdout and stderr bytes, exit status (0 / 1 disorder / 2 failure) and standard input consumption
Which environment?	Linux, C locale, TZ=UTC0, fixed non-root user, stable files in the test tree, stdout captured by the evaluator
Which errors matter?	Missing, unreadable and directory operands; invalid and incompatible options; extra operands in check mode
What is trusted?	bench/core/IO.dfy read, write, errno-text and quoting contracts at a98d11a
What remains to prove?	Output records are a sorted permutation of the input records (a sorted set with -u); first disorder in check mode; diagnostics and exit policy

Options left out due to IO.dfy

Utility	Option left out	Missing API support
sort	-c / -C reading standard input (no operand, or -)	GNU stops reading at the first disorder. IO.dfy provides only whole-input standard input reads (ReadStdinAll, ReadStdinWithOutcome), so the consumed prefix cannot be matched.

1. Test results

• Reason not run: scope-review stage; nothing is implemented yet.

2. Fuzzing results

• Reason not run: scope-review stage; the generator will be added with the implementation.

3. Verification results

• Reason not run: scope-review stage; the Dafny modules are scaffold stubs.
• Definition validation: python3 -m benchmarks validate sort, exit 0.

sort: valid

Progress notes

• Completed work: scaffold; scope document with observations from the pinned GNU binary; source metadata.
• Remaining work: specification, core, proof, tests and fuzzer generator; evidence runs.
• Blockers: maintainer scope review.
• Commands and results: ruff format --check ., ruff check . and python3 -m benchmarks validate sort pass.
• Artifact links: bench/utils/sort/sort.md.
• Next action: implement SortSpec.dfy after the scope review.

AI usage

I wrote this PR with the help of Claude Opus 5.5. It helped me probe the pinned GNU sort source code and assisted with writing the body of this draft. I reviewed the content.

[suhdonghwi]

@duncan020313

Could you review the scope in bench/utils/sort/sort.md before I start the implementation? Thank you.

[duncan020313]

안녕하세요. Dafnyutils 프로젝트에 참여해 주셔서 감사드립니다.

현재 구현 절차가 변경되어 draft PR 없이 현재 IO modeling이 허용하는 범위 내에서 최대한 상세한명세를 작성하고 구현과 증명을 작성하시면 됩니다.

여기서 상세한 명세란,

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

감사합니다. 추가로 질문이 있으시면 편하게 댓글을 남겨 주세요.

---

Hello. Thank you for participating in the Dafnyutils project.

The implementation procedure has recently changed. You no longer need to create a draft PR. Instead, please write the most precise specification possible within the scope currently supported by IO modeling, and then implement the code and provide the corresponding proofs.

By a detailed specification, we mean aiming for a specification that is sound 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?
  Your goal should be to write a specification that satisfies soundness while achieving the highest possible degree of completeness.

You can think of the provided fuzzer as a tool for checking soundness.

Thank you. If you have any additional questions, please feel free to leave a comment.