Add the `sync` benchmark, including its specification, implementation, proof, and GNU comparison tests, within the scope below. | Question | Answer | | --- | --- | | Where is the GNU code? | sync.c: main / sync_arg | | What must I implement? | Global no-operand sync; --help/--version and invalid option combinations including -d without operands. | | What must the spec guarantee? | Typed FilesystemSync(AllSyncTargets, SyncAllFilesystems) result; exact CLI diagnostics and exit. Persistence internals stay trusted. | | Which APIs can I use? | Typed filesystem request/result calls selected by this entry; path/kind queries where needed, output outcomes and diagnostics. | | What is outside this task? | All path-targeted modes: adapter lacks GNU write-only-open retry and open/sync/close failure-phase observations. | Source paths in the table are relative to `coreutils/src/`. See [implementation notes](https://github.com/prosyslab/dafnyutils/blob/7b481114ea5fd4a787f4dc1e587d17e8ee10b6a8/docs/implementation-notes.md#sync), [common implementation rules](https://github.com/prosyslab/dafnyutils/blob/7b481114ea5fd4a787f4dc1e587d17e8ee10b6a8/docs/implementation-notes.md#common-implementation-rules), and the [contribution workflow](https://github.com/prosyslab/dafnyutils/blob/7b481114ea5fd4a787f4dc1e587d17e8ee10b6a8/CONTRIBUTING.md#extending-benchmark).
Activity