Coq: re-verify 0 real gaps + fix build/verify from clean; add just run launcher#164
Merged
Merged
Conversation
Verified the Coq proof tree with coqc + Print Assumptions under Coq 8.18.0: the full _CoqProject (11 files) compiles with zero admit/Admitted/Axiom markers. obliterate_overwrites_all_blocks and overwrite_pass_equalizes_storage are 'Closed under the global context'; single_op_reversible, operation_sequence_reversible, copy_file_reversible, mkdir_two_dirs_reversible and obliterate_not_injective depend only on standard functional_extensionality. The historically-tracked '1 real gap' and the three 2026-06-02 admits (#56/#57/#58) are all closed. Remaining assumptions are standard/justified: functional_extensionality (stdlib) + is_empty_dir_dec (justified classical), Agda funext (structural). Build/tooling fixes (both failed from a clean checkout): - just build-coq and scripts/verify-proofs.sh compiled an incomplete file subset (missing filesystem_composition.v etc.), so posix_errors.v failed with 'Cannot find a physical path bound to logical path filesystem_composition'. Both now compile the full _CoqProject chain in dependency order and mkdir -p extracted before extraction.v, matching the validation.yml CI oracle. - verify-proofs.sh: fixed two latent set -e bugs that aborted before any test ran — ((VAR++)) counters (first bump from 0 returns exit 1) replaced with assignment form; per-test cd side effects isolated via subshell. - gitignore proofs/coq/.lia.cache (Coq Lia build artifact). Docs reconciled to 0 real gaps (live docs only; dated audit snapshots left as records): PROOF_HOLES_AUDIT.md, README.adoc, FAQ.adoc, CLAUDE.md, docs/wiki/{Verification-Status,For-Developers}.md, ROADMAP.adoc, docs/ROADMAP_TO_V1.md, STATE.a2ml, methodology.a2ml, CHANGELOG.adoc. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU
🔍 Hypatia Security ScanFindings: 41 issues detected
View findings[
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/valence-shell/valence-shell/proofs/agda/FilesystemModel.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "believe_me undermines formal verification (2 occurrences, CWE-704)",
"type": "believe_me",
"file": "/home/runner/work/valence-shell/valence-shell/proofs/idris2/src/Filesystem/Axioms.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Obj.magic bypassing type safety (2 occurrences, CWE-704)",
"type": "obj_magic",
"file": "/home/runner/work/valence-shell/valence-shell/impl/mcp/src/bindings/Mcp.res",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "JSON decode without validation (1 occurrences, CWE-20)",
"type": "json_decode_no_validation",
"file": "/home/runner/work/valence-shell/valence-shell/impl/mcp/src/Server.res",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "expect() in hot path (1 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/external.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (6 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/external.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "from_raw constructs types from raw pointers without safety checks (4 occurrences, CWE-676)",
"type": "from_raw",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/external.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "expect() in hot path (1 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/glob.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "expect() in hot path (1 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/arith.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/process_sub.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
The user-facing launcher was missing: the Justfile had no run/setup/install recipe, and QUICKSTART-USER.adoc was an unfilled RSR template promising 'just run', 'just setup', 'just uninstall', 'just stapeln-run' — none of which existed. - Add 'just run *ARGS' (alias 'just launch'): builds and starts the interactive vsh shell, passing extra args through to the binary. Verified end-to-end: 'just run --version' -> vsh 0.9.0 (exit 0); the REPL banner starts; and 'just run <script>' executes and exits 0. - Rewrite QUICKSTART-USER.adoc to the real, working flow. Every 'just' command it cites is a real recipe (verified via 'just --show'): run/launch, build-cli, install-cli, test-cli, container-build/run/shell, doctor, heal, tour, help-me, clean. Uninstall documents the honest 'cargo uninstall vsh' path. Removes the template placeholder/instruction cruft. - Point the wiki For-Users page at 'just run' as the primary launch path. Note: full alignment to the external launcher standard (hyperpolymath/standards) is not attempted here — that repo is outside this session's scope. This adds a real, verified launch entry point consistent with what the quickstart promised. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU
hyperpolymath
changed the title
just run launcher
🔍 Hypatia Security ScanFindings: 41 issues detected
View findings[
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/valence-shell/valence-shell/proofs/agda/FilesystemModel.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "believe_me undermines formal verification (2 occurrences, CWE-704)",
"type": "believe_me",
"file": "/home/runner/work/valence-shell/valence-shell/proofs/idris2/src/Filesystem/Axioms.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Obj.magic bypassing type safety (2 occurrences, CWE-704)",
"type": "obj_magic",
"file": "/home/runner/work/valence-shell/valence-shell/impl/mcp/src/bindings/Mcp.res",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "JSON decode without validation (1 occurrences, CWE-20)",
"type": "json_decode_no_validation",
"file": "/home/runner/work/valence-shell/valence-shell/impl/mcp/src/Server.res",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "expect() in hot path (1 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/external.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (6 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/external.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "from_raw constructs types from raw pointers without safety checks (4 occurrences, CWE-676)",
"type": "from_raw",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/external.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "expect() in hot path (1 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/glob.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "expect() in hot path (1 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/arith.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/valence-shell/valence-shell/impl/rust-cli/src/process_sub.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
hyperpolymath
marked this pull request as ready for review
July 17, 2026 04:19
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Two outstanding items, both verified with the actual toolchain.
1. Coq proof stack — re-verified 0 admits / 0 real gaps (Coq 8.18.0)
The full
_CoqProject(11 files) compiles with zeroadmit/Admitted/Axiommarkers.Print Assumptionson the load-bearing theorems:obliterate_overwrites_all_blocksoverwrite_pass_equalizes_storage(#57)single_op_reversible/operation_sequence_reversible/copy_file_reversible/mkdir_two_dirs_reversible(#56) /obliterate_not_injective(#58)functional_extensionality_deponlyThe historically-tracked "1 real gap" and the three 2026-06-02 admits (#56/#57/#58) are all closed. Remaining assumptions are standard/justified: Coq
functional_extensionality(stdlib) +is_empty_dir_dec(justified classical), Agdafunext(structural). Net: 2 documented axioms, 0 real gaps.Docs reconciled (live docs only; dated audit snapshots left as records):
PROOF_HOLES_AUDIT.md,README.adoc,FAQ.adoc,CLAUDE.md,docs/wiki/,ROADMAP*.{adoc,md},STATE.a2ml,methodology.a2ml,CHANGELOG.adoc.2. Coq build/verify entry points — fixed to work from a clean checkout
just build-coqandscripts/verify-proofs.shcompiled an incomplete file subset (missingfilesystem_composition.vetc.), soposix_errors.vfailed with "Cannot find a physical path bound to logical path filesystem_composition." Both now compile the full_CoqProjectchain in order andmkdir -p extractedbeforeextraction.v, matching thevalidation.ymlCI oracle.scripts/verify-proofs.sh: fixed two latentset -ebugs that aborted before any test ran —((VAR++))counters (first bump from 0 returns exit 1) → assignment form; per-testcdleaks → each command runs in a subshell. Script now runs end-to-end (exit 0).proofs/coq/.lia.cache.3. Launcher — add
just run/just launchThe user-facing launcher was missing (no
run/setup/installrecipe), andQUICKSTART-USER.adocwas an unfilled template promising recipes that didn't exist.just run *ARGS(aliasjust launch): builds and starts the interactivevshshell, passing args through. Verified end-to-end:just run --version→vsh 0.9.0(exit 0); REPL banner starts;just run <script>executes and exits 0.QUICKSTART-USER.adocto the real flow — everyjustcommand it cites is a real recipe (verified viajust --show).Scope note: full alignment to the external launcher standard (
hyperpolymath/standards) is not attempted — that repo is outside this session's GitHub scope. This adds a real, verified launch entry point consistent with what the quickstart already promised; standard-conformance can follow when the standard is readable.Validation
coqc -R . ValenceShellon all 11 files: clean;Print Assumptionsas tabulated.just build-coqandscripts/verify-proofs.shfrom a cleaned tree: exit 0.just run --version,just run <script>: exit 0 with correct output.🤖 Generated with Claude Code
https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU