[jkkms]

Change and scope

Adds mkfifo (issue #14): one FIFO per operand in command-line order, with -m/--mode (octal and symbolic MODE), --help, --version and GNU parsing diagnostics. A failed operand does not stop later operands.

MODE is specified as abstract syntax with Render and Meaning; the specification contains no parsing algorithm. The Core parser is proved to invert Render, which makes the invalid mode decision exact and shows that a valid MODE has one meaning. With -m, each successful creation is followed by one non-following SetFileMode call, which is GNU's lchmod after mkfifo. (mkdir leaves out -m because chmod after creation adds a failure point that GNU does not have. For mkfifo that second call is GNU's own behavior.)

Example (umask 022): mkfifo -m =rw,+x pipe creates pipe with mode 0755; mkfifo -m +644,u+x pipe gives 0766; mkfifo -m u+s pipe reports mkfifo: mode must specify only file permission bits and creates nothing.

• Task ID(s) and kind: mkfifo, coreutils.
• Tested commit and any uncommitted changes: 62c4c9ffef2464255c6234e76005615745ebbdde (branch head). All results below come from one run on base a832a0c with the changes of the last two commits applied but not yet committed; git diff a832a0c 62c4c9f is byte-identical to the tested diff (sha256 6c66e4e339de2074444f56a2bda299690743364821f6588317bb2c35aacd01bd).
• Working directory, OS/container image and tool versions: /workspace/dafnyutils in the contributor container (Ubuntu 24.04, Linux x86-64); Dafny 4.11.1+10dca3ba4a2909c11299176440401fc31413b53d, .NET SDK 8.0.132, Python 3.12.3, pytest 9.1.1, Ruff 0.15.12, Rust/Cargo 1.94.0, Z3 4.16.0.
• Changed boundaries:
  • specification, implementation, proof, tests: new files in bench/utils/mkfifo/
  • evaluator: new generator tools/coreutils_fuzzer/src/fuzz/input/generators/mkfifo.rs, registered in generators/mod.rs and utils/capabilities.rs
  • shared fuzzer change: fuzz/comparison/fs_snapshot.rs now records a FIFO node from its metadata (kind fifo, no contents) instead of failing with "unsupported filesystem node". It never opens the FIFO. Character devices are still rejected. A regression test is added in src/tests/fuzzer.rs. Please review this part separately.
• GNU source revision, URL/license and upstream test scenarios: coreutils src/mkfifo.c at 2cf491412c199e2211880ec3f4ba387026638a33, gnulib lib/modechange.c at 83730551b451b43577531986a5c4300e0166c42f, https://www.gnu.org/software/coreutils/, GPL-3.0-or-later; ported tests/misc/mknod.sh (mkfifo -m 734, mkfifo --mode='ug+rw,o+r' under umask 777).
• Specified scope and trusted model/API revision: see bench/utils/mkfifo/mkfifo.md; base revision 3c704ee78884a4e764354431bb72b27771c02980. Trusted calls: CreateSpecialNode, SetFileMode, GetUmask, quoting, errno text and stream writes.

Changes after review

Review comment of 2026-10-27: a long MODE could overflow the stack in the parser, and 0…0600 and u…u+r should become test cases.

• Before: the parser and Meaning recursed once per character. A 50,000-character MODE crashed with Stack overflow, and 20,000 characters took 12 s because every step copied the rest of the string.
• Fix: the recursive functions stay as the definitions the proofs use. At run time, ParseMode (its by method body) and ComputeMeaning walk string indices, and each loop is proved to return the value of the function it replaces, so the specification and the existing proofs are unchanged. Octal digits stop at the first value above 07777, as mode_compile does. The compiled C# calls none of the recursive functions.
• Tests: 8 GNU parity cases with MODE strings of about 100,000 characters: the two cases from the review, long runs of permission letters, actions and clauses, a digit run after an operator, and two digit runs above 07777 that must be rejected.
• Additional checks (beyond the template): a MODE of 131,071 characters, Linux's limit for one argument, matches GNU in 0.3 s; 50,000 random MODE strings (grammar-based, mutated and noise, up to 130,014 characters, random umask, -m and --mode=) match GNU in output, exit status and resulting mode; the fuzzer with five more seeds (2, 3, 5, 11, 13; 1,000 iterations each) found no mismatch; and the changed modules (MkfifoModeCore.dfy, MkfifoCore.dfy) verify with five other Z3 seeds (1, 7, 100, 2026, 12345) under both the repository's isolated-assertion settings and the per-method settings of make check, with no failure or timeout.
• Rebase: onto main at 3c704ee (tsort). The only conflict was the utility list in utils/capabilities.rs, which now contains both.

Soundness and completeness

Following the review guidance on #38 (soundness: the specification accepts a correct execution trace; completeness: it rejects an incorrect one):

• Soundness. The verified Core implementation matches the pinned GNU build on 153 runtime cases and on 3,000 generated fuzzing cases (sections 1 and 2), so GNU's observed traces satisfy the specification on all of them.

• Completeness. For each operand the specification fixes the exact native requests: one CreateSpecialNode with 0666 (no -m) or the MODE bits (-m), and, only after a successful creation with -m, one non-following SetFileMode. It also fixes operand order, every diagnostic byte and its order, the exit status, and the MODE decision before any operand. It states what does not change: the filesystem after a rejected MODE, the filesystem between operands, and standard output. Help, version, parse errors and a missing operand are early exits of the shared runner, which never call RunCore.

• Mutation check. Each incorrect implementation below changes one place in the reference Core (the specification is unchanged); unchanged controls verify. Every mutant fails verification at a specification obligation. This shows that the reference proof cannot be completed for these behaviors; it is not a separate proof that no other proof exists.

  Incorrect behavior	Rejected by
  permission change without -m	OperandStep (no -m: one creation only)
  create with 0666, then chmod to MODE	OperandStep (creation mode is the MODE bits)
  permission change follows a symlink	OperandStep (SetFileMode(path, false, …))
  permission change after a failed creation	OperandStep (failure ends the operand)
  retry a failed creation	OperandStep (one creation request)
  wrong or missing diagnostic	OutcomeDiagnostic
  skip the remaining operands after a failure	OperandResults
  process operands in reverse order	OperandResults
  exit 0 after a failure	PlanRun exit status
  reversed diagnostic order	OrderedDiagnostics
  evaluate MODE without the umask	ModePlanOf (Meaning)
  accept set-ID or sticky bits	ModePlanOf (OnlyPermissionBits)
  create FIFOs after an invalid MODE	PlanRun (filesystem unchanged)
  write to standard output	Spec (io.stdout() == old(io.stdout()))
  parser accepts u+r,	ModeInvalid (parser round trip)
  run-time parser loop accepts u+r,	ParseMode by method (equals the parser function)
  run-time octal check accepts 010000	OctalUpTo (equals OctalValue(ds) <= 07777)
  run-time MODE evaluation skips the last clause	ComputeMeaning (equals Meaning)

• Left open on purpose. Only the native observations: the resulting FIFO's mode, ownership and timestamps come from the trusted CreateSpecialNode and SetFileMode results, as for mkdir. A failed permission change after a successful creation is specified and proved but cannot be produced by the fixtures.

Issues raised on #39 and #40 are covered: --= lists GNU's possibilities, -é reports only its first byte, both diagnostics use GNU's quoteaf, the scope document starts with the manual's description, and the branch has no merge commit.

AI usage

I investigated how GNU mkfifo works and when it fails (permission bits, umask, symbolic MODE), decided the scope (-m included, -Z/--context left out) and how MODE is specified, then directed the implementation. Claude assisted with writing and reviewing the specification, code, proofs, tests and fuzzer generator based on my instructions. I reviewed the specification, the scope document and the shared fuzzer change against GNU src/mkfifo.c.

Setup note for maintainers

On a host whose user ID is not 1000, .devcontainer/post-create.sh fails with mkdir: cannot create directory '/workspace/tmp/update-z3-rebuild': Permission denied: the image creates /workspace/tmp for UID 1000, and updateRemoteUserUID then changes vscode to the host UID. Running chown vscode:vscode /workspace/tmp as root inside the container and rerunning the script worked. This PR does not change the setup files.

Options left out due to IO.dfy

Utility	Option left out	Missing API support
mkfifo	-Z, --context[=CTX]	No operation for SELinux/SMACK enablement, file labels or the default creation context (selabel_open/defaultcon, setfscreatecon, smack_set_label_for_self). Same decision as mkdir.

1. Test results

• Exact command(s): make -C bench/utils/mkfifo test
• Exit code(s): 0
• Passed / failed / skipped: 153 / 0 / 0 (the 6 dafny_verify cases are deselected here and run by make check, below).

make: Entering directory '/workspace/dafnyutils/bench/utils/mkfifo'
python3 -m benchmarks.make_tasks test --root "/workspace/dafnyutils" --task "mkfifo"
........................................................................ [ 47%]
........................................................................ [ 94%]
.........                                                                [100%]
153 passed, 6 deselected in 45.48s
make: Leaving directory '/workspace/dafnyutils/bench/utils/mkfifo'

2. Fuzzing results

• Utility and exact command: python3 tools/coreutils_fuzzer/run.py fuzz mkfifo --seeds 1,7,19 --iterations 1000
• Required seeds: 1,7,19; requested iterations per seed: 1000.
• GNU reference and DUT: _build/coreutils/src/mkfifo (native, sha256 2eda4b35ab2839d68f98803caf2263376929c0e3cb828fe6c8bc821693c94be1), _build/bench/mkfifo_bench.dll (dotnet DLL, sha256 958d7e867d9b95c9638d9c232654e644bd692bf8c2d1afb044cd17c53010b751).
• Fuzzer revision and container image identity: this branch at 62c4c9f; dafnyutils-coreutils-fuzzer:latest sha256:c312109aeaec50957a8240aa7c52d6bf8b564f18d926afdcf6a672f552f2c6d5.
• Exit code(s): 0; standard error was empty.
• Missing semantic buckets: fs:file-added counts only regular files (node_is_file in fuzz/semantic.rs), so a run that creates a FIFO falls in no filesystem bucket. The other missing buckets are changes mkfifo never makes: it does not modify, remove or retime existing entries (an existing path fails with File exists), and it never reads standard input. The filesystem comparison itself does include the new FIFO nodes and their modes. This PR leaves semantic.rs unchanged.

Full standard output:

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

=== Coreutils fuzz campaign ===
Configuration
  Utility    : mkfifo
  Seed       : 1
  Budget     : 1000 iterations
  Reference  : "/workspace/dafnyutils/_build/coreutils/src/mkfifo" (Native)
  DUT        : "/workspace/dafnyutils/_build/bench/mkfifo_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:c312109aeaec50957a8240aa7c52d6bf8b564f18d926afdcf6a672f552f2c6d5
  Option pool: 4 (discovered)
  Outside scope: --context, -Z
Coverage
  Option coverage: singles 4/4 (100.0%), pairs 6/6 (100.0%)
  Semantic coverage: buckets 20/27 (74.1%), extra=0, missing: fs:file-added, 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    : 381.91s
  Status     : PASS - all requested iterations matched; no mismatch found
=== End campaign ===
    seed: 7

=== Coreutils fuzz campaign ===
Configuration
  Utility    : mkfifo
  Seed       : 7
  Budget     : 1000 iterations
  Reference  : "/workspace/dafnyutils/_build/coreutils/src/mkfifo" (Native)
  DUT        : "/workspace/dafnyutils/_build/bench/mkfifo_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:c312109aeaec50957a8240aa7c52d6bf8b564f18d926afdcf6a672f552f2c6d5
  Option pool: 4 (discovered)
  Outside scope: --context, -Z
Coverage
  Option coverage: singles 4/4 (100.0%), pairs 6/6 (100.0%)
  Semantic coverage: buckets 20/27 (74.1%), extra=0, missing: fs:file-added, 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    : 382.40s
  Status     : PASS - all requested iterations matched; no mismatch found
=== End campaign ===
    seed: 19

=== Coreutils fuzz campaign ===
Configuration
  Utility    : mkfifo
  Seed       : 19
  Budget     : 1000 iterations
  Reference  : "/workspace/dafnyutils/_build/coreutils/src/mkfifo" (Native)
  DUT        : "/workspace/dafnyutils/_build/bench/mkfifo_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:c312109aeaec50957a8240aa7c52d6bf8b564f18d926afdcf6a672f552f2c6d5
  Option pool: 4 (discovered)
  Outside scope: --context, -Z
Coverage
  Option coverage: singles 4/4 (100.0%), pairs 6/6 (100.0%)
  Semantic coverage: buckets 20/27 (74.1%), extra=0, missing: fs:file-added, 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    : 373.26s
  Status     : PASS - all requested iterations matched; no mismatch found
=== End campaign ===

3. Verification results

• Exact verification command and exit code: make -C bench/utils/mkfifo verify, 0
• Verified files: Mkfifo.dfy, MkfifoCore.dfy, MkfifoProof.dfy and the files they include (MkfifoSpec.dfy, MkfifoSchema.dfy, MkfifoModeCore.dfy, MkfifoModeProof.dfy, CliSupport.dfy); repository limits: isolated assertions, 30-second condition limit, 100-second declaration limit. Termination of MODE parsing and the operand loop is proved; CLI termination keeps the shared runner's boundary.
• Verified / errors / timeouts: 112 declarations, 1,542 conditions, 0 failed, 0 timeouts.
• Definition/layout validation and final gate: python3 -m benchmarks validate mkfifo → mkfifo: valid (exit 0); make check TASK=mkfifo → mkfifo: checks passed (exit 0; it rebuilds, reruns the 153 runtime cases and the verification, and runs the 6 dafny_verify cases).
• Conditions still to prove: none.

make -C bench/utils/mkfifo verify (first and last lines; one block per declaration in between):

make: Entering directory '/workspace/dafnyutils/bench/utils/mkfifo'
python3 -m benchmarks.verify --project "/workspace/dafnyutils/bench/utils/mkfifo" --library "/workspace/dafnyutils/bench/utils/mkfifo/../../core"
Verification targets (112 declarations):
…
Results File: /tmp/tmpglgq64gy/111.trx
[112/112] Completed MkfifoProof.dfy: total=5 failed=0
DAFNY_VERIFICATION_OUTCOME=verified phase=verify
DAFNY_VERIFICATION_RESULT total=1542 failed=0
make: Leaving directory '/workspace/dafnyutils/bench/utils/mkfifo'

python3 -m benchmarks validate mkfifo:

mkfifo: valid

make check TASK=mkfifo (last lines):

DAFNY_VERIFICATION_RESULT total=1542 failed=0
make[1]: Leaving directory '/workspace/dafnyutils/bench/utils/mkfifo'
......                                                                   [100%]
6 passed, 153 deselected in 132.83s (0:02:12)
mkfifo: checks passed

🤖 Generated with Claude Code

[jkkms]

prosyslab-classroom/cs424-program-reasoning#608

[duncan020313]

현재 Mode 파싱 부분이 매우 긴 문자열이 들어왔을 때 stack overflow가 발생할 수 있는 구현 구조입니다.
tail-recursive하게 구현하거나, 반복문을 사용하여 stack overflow가 발생하지 않도록 해주세요.

stack overflow를 발생시키는 mode 예시: 0000000 ... 0000600, uuuuuuuu ... uuuu+r

위 케이스를 테스트 케이스에도 추가해주세요

[jkkms]

리뷰 감사합니다. 반영했습니다.

• MODE를 읽는 부분(ParseMode)과 계산하는 부분(Meaning)을 실행할 때는 문자열 위치를 따라가는 반복문으로 바꿨습니다. 증명에 쓰는 재귀 함수 정의는 그대로 두고, 반복문이 그 함수와 같은 값을 낸다는 것을 증명했습니다(ParseMode의 by method, ComputeMeaning). 8진수는 07777을 넘는 순간 읽기를 멈춥니다(GNU mode_compile과 같음).
• 고치기 전에는 길이 50,000에서 stack overflow가 났고, 20,000에서도 12초가 걸렸습니다. 지금은 한 인자의 최대 길이인 131,071자도 0.3초 안에 끝납니다.
• 말씀하신 두 경우(0…0600, u…u+r)와 함께, 권한 글자·연산·절이 길게 이어지는 경우, 연산자 뒤의 긴 8진수, 07777을 넘는 긴 숫자(거부되어야 함)를 길이 100,000으로 Tests.py에 추가했습니다. 모두 GNU 결과와 비교합니다.
• 추가로 무작위 MODE 50,000개(최대 130,014자, umask와 -m/--mode= 형태도 무작위)를 GNU와 비교했고, 퍼저는 필수 시드 외에 5개(2, 3, 5, 11, 13)를 더 돌렸습니다. 바뀐 모듈은 Z3 시드 5개에서도 검증되는 것을 확인했습니다. 불일치나 실패는 없었습니다.
• upstream의 tsort 추가와 충돌이 있어 최신 main(3c704ee) 위로 rebase했습니다.

검증·테스트·퍼징 결과는 PR 본문에 갱신했습니다.