[elecball]

This PR implements GNU pathchk, which checks file name portability, with specifications, proofs, tests, and a fuzzer generator. (#17)

Change and scope

• Task ID and kind: pathchk, coreutils.
• Tested state: fcac7aa399a1074dc00538889848ef58accd3a51.
• Environment: /workspace/dafnyutils, Ubuntu 24.04 development container, Linux x86-64.
• Tools: Dafny 4.11.1+9f281d50a7befa662350be47dd73ff0b2e0bb8d9, Python 3.12.3, .NET 8.0.133, Cargo 1.94.0.
• Changed boundaries: utility specification, implementation, proofs, tests, documentation, and fuzzer generation/registration. Shared IO and comparison rules are unchanged.
• GNU source: coreutils/src/pathchk.c at 2cf491412c199e2211880ec3f4ba387026638a33.
• Source URL/license: https://www.gnu.org/software/coreutils/, GPL-3.0-or-later.
• Scope/model/API revision: bench/utils/pathchk/pathchk.md.

Question	Answer
What is the source?	Pinned GNU pathchk.c
What is accepted?	-p or --portability with names; -P combined with -p, help/version, long-option abbreviations, --
What is observed?	Exact stdout/stderr, exit status, stdin and filesystem preservation
Which environment?	Linux, C locale, UTF-8 arguments, sufficient memory
Which errors matter?	Options/operands, empty names, non-portable bytes, path/component limits, leading hyphens, and modeled stream errors
What is trusted?	Existing parser, UTF-8/quoting definitions, and stream/errno contracts
What is proved?	RunCore ensures PathchkSpec.Spec; portable-byte, length, and ordered-diagnostic relations determine GNU's result

Options left out due to IO.dfy

Utility	Option left out	Missing API support
pathchk	Default mode and -P alone	Host pathconf limits are not exposed by IO.dfy; both modes are outside issue #17.

1. Test results

• Runtime tests within make -C bench/utils/pathchk final-check: 59 passed, 5 deselected in 8.61s; the 5 proof tests run in the separate proof stage.
• Covers coreutils/tests/misc/pathchk.sh, byte boundaries, error precedence, continued operand checking, --=x, Unicode option bytes, quoting, /dev/full, and long names/options.
• ruff check bench/utils/pathchk/Tests.py: exit 0.
• ruff format --check bench/utils/pathchk/Tests.py: exit 0.
• cargo fmt --manifest-path tools/coreutils_fuzzer/Cargo.toml --all -- --check: exit 0.

Runtime stdout from make -C bench/utils/pathchk final-check:

59 passed, 5 deselected in 8.61s

• Fixed a 10-second timeout in long option-error formatting; regression tests include a 131,071-byte short-option bundle ending in an invalid character.

2. Fuzzing results

• 29 fixed scenarios plus random inputs and corpus mutation.
• Required command: python3 tools/coreutils_fuzzer/run.py fuzz pathchk --seeds 1,7,19 --iterations 1000.
• Seeds 1, 7, and 19: 1,000 matches each, with zero mismatches, timeouts, unfinished iterations, or other errors; exit 0.
• GNU reference: _build/coreutils/src/pathchk (native); SHA-256: 80f745590495c992148ea3d3f043298aa398962a9136b91e25a2d56912ae1808.
• DUT: _build/bench/pathchk_bench.dll (dotnet DLL); SHA-256: e9faa43c36887d6752afbac8ab44f0c373d7f6fd5e0b30549cfd70c9205a85d0.
• Fuzzer revision: the tested state above; container image identity is included in stdout.
• All 10 option pairs occurred across the campaigns. Missing fixture and filesystem buckets reflect argv-only portability checks.

Full fuzzing stdout

selected utilities: pathchk
==> utility: pathchk
    seed: 1

=== Coreutils fuzz campaign ===
Configuration
  Utility    : pathchk
  Seed       : 1
  Budget     : 1000 iterations
  Reference  : "/workspace/dafnyutils/_build/coreutils/src/pathchk" (Native)
  DUT        : "/workspace/dafnyutils/_build/bench/pathchk_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: 5 (discovered)
Coverage
  Option coverage: singles 5/5 (100.0%), pairs 10/10 (100.0%)
  Semantic coverage: buckets 15/27 (55.6%), extra=0, missing: fixture:has-dir, fixture:has-file, fixture:has-symlink, fs:file-added, fs:file-content-changed, fs:file-removed, fs:mode-changed, fs:target-changed, fs:time-changed, operand:existing-file
Results
  Iterations : requested=1000 submitted=1000 completed=1000 not_started=0 unfinished=0
  Outcomes   : match=1000 mismatch=0 timeout=0 other_errors=0
  Elapsed    : 152.62s
  Status     : PASS - all requested iterations matched; no mismatch found
=== End campaign ===
    seed: 7

=== Coreutils fuzz campaign ===
Configuration
  Utility    : pathchk
  Seed       : 7
  Budget     : 1000 iterations
  Reference  : "/workspace/dafnyutils/_build/coreutils/src/pathchk" (Native)
  DUT        : "/workspace/dafnyutils/_build/bench/pathchk_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: 5 (discovered)
Coverage
  Option coverage: singles 5/5 (100.0%), pairs 9/10 (90.0%)
  Semantic coverage: buckets 15/27 (55.6%), extra=0, missing: fixture:has-dir, fixture:has-file, fixture:has-symlink, fs:file-added, fs:file-content-changed, fs:file-removed, fs:mode-changed, fs:target-changed, fs:time-changed, operand:existing-file
Results
  Iterations : requested=1000 submitted=1000 completed=1000 not_started=0 unfinished=0
  Outcomes   : match=1000 mismatch=0 timeout=0 other_errors=0
  Elapsed    : 154.09s
  Status     : PASS - all requested iterations matched; no mismatch found
=== End campaign ===
    seed: 19

=== Coreutils fuzz campaign ===
Configuration
  Utility    : pathchk
  Seed       : 19
  Budget     : 1000 iterations
  Reference  : "/workspace/dafnyutils/_build/coreutils/src/pathchk" (Native)
  DUT        : "/workspace/dafnyutils/_build/bench/pathchk_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: 5 (discovered)
Coverage
  Option coverage: singles 5/5 (100.0%), pairs 10/10 (100.0%)
  Semantic coverage: buckets 15/27 (55.6%), extra=0, missing: fixture:has-dir, fixture:has-file, fixture:has-symlink, fs:file-added, fs:file-content-changed, fs:file-removed, fs:mode-changed, fs:target-changed, fs:time-changed, operand:existing-file
Results
  Iterations : requested=1000 submitted=1000 completed=1000 not_started=0 unfinished=0
  Outcomes   : match=1000 mismatch=0 timeout=0 other_errors=0
  Elapsed    : 153.45s
  Status     : PASS - all requested iterations matched; no mismatch found
=== End campaign ===

3. Verification results

• make -C bench/utils/pathchk final-check: exit 0; includes make -C bench/utils/pathchk verify, layout checks, runtime tests, fuzzing and 5 proof tests.
• make -C bench/utils/pathchk verify: 2438 verified, 0 errors; exit 0.
• Scope: all seven task Dafny files below. Shared IO is trusted; Core loop termination is proved, whole-process termination is not.
• Limits: 30 s/assertion batch; seed 42. Shared sources are supplied through --library, which produces library-verification warnings.
• A separate 5-second whole-method probe timed out in CheckName; repository-standard verification passed without changing its limits.

Proof targets and analysis-only files

• Direct proof targets (bench/utils/pathchk/): Spec/PathchkSchema.dfy, Spec/PathchkSpec.dfy, Impl/Pathchk.dfy, Impl/PathchkCore.dfy, Impl/PathchkCli.dfy, Impl/CliSupport.dfy, Proof/PathchkProof.dfy.
• Analysis only (bench/utils/pathchk/): None; all seven local Dafny files are verification targets.
• Analysis-only shared includes (bench/core/): CliTypes.dfy, Errno.dfy, IO.dfy, IOContract.dfy, Result.dfy, SecurityModel.dfy, StringEscaping.dfy, Utf8.dfy, World.dfy.

Verification and proof-test summaries from make -C bench/utils/pathchk final-check:

Dafny program verifier finished with 2438 verified, 0 errors
5 passed, 59 deselected in 49.17s
pathchk: checks passed

make -C bench/utils/pathchk lint: exit 0.

pathchk: valid

Progress notes

• Completed: implementation, declarative specification, proofs, tests, docs, and fuzzer. The main difficulty was reproducing GNU's byte-level diagnostics and error precedence without timing out on long arguments.
• Limitations: native IO and CLI parsing are trusted; whole-process termination is not proved. Runtime tests and random input sizes are bounded.
• Remaining review: specification precision under the shared contracts.
• Artifact: bench/utils/pathchk/pathchk.md.

AI usage

I investigated how GNU pathchk works and when it fails, then directed the implementation. Codex assisted with writing and reviewing code based on my instructions.