docs+test: ROADMAP truthfulness audit + drift-detection aspect (closes Phase 0 housekeeping)#60
Merged
Merged
Conversation
Phase 0 housekeeping. The 6-phase production path doc instructed a
ROADMAP truthfulness audit: every "DONE" claim verified against a
green CI run + every path reference verified against the filesystem.
Audit findings (fixed in this commit):
1. spec/10-levels-for-wasm.adoc → spec/type-safety-levels-for-wasm.adoc
The file was renamed at some point but 5 callers still pointed at
the old path: ROADMAP.adoc, README.adoc, EXPLAINME.adoc (twice),
.claude/CLAUDE.md. All updated.
2. EXPLAINME.adoc described a pre-restructure Idris2 ABI architecture:
listed Types.idr / Layout.idr / Access.idr / Effects.idr /
Linearity.idr / Foreign.idr as the load-bearing proof modules.
Actual structure is src/abi/TypedWasm/ABI/{Region, TypedAccess,
Pointer, Levels, Effects, Lifetime, Linear, MultiModule, Layout,
Proofs, SessionProtocol, ResourceCapabilities, Choreography,
Tropical, Epistemic, Echo, ModuleIsolation}.idr. EXPLAINME's
evidence sentence and full file table rewritten to match the real
structure, with each entry naming the actual load-bearing types
from each file.
3. EXPLAINME.adoc still referenced src/abi/Foreign.idr (a file that
doesn't exist in the current tree). Removed.
To prevent this drift class going forward, claim-envelope.mjs gets a
new section 8 ("Path references in docs resolve to real files") that
scans README/ROADMAP/EXPLAINME/CLAUDE for repo-relative path tokens
(adoc/md/mjs/res/idr/zig/rs/ebnf/toml/ipkg extensions) and verifies
each resolves on disk. Filters: only paths with a `/` (bare filenames
are conventional prose references); cross-repo paths
(typedqliser/affinescript/ephapax/standards/hypatia/typell/vql-ut/
echidna) are allowlisted; templated paths ({{...}}) and well-known
non-repo paths (github.com, /home/runner/) are allowlisted.
Section 8 prints every stale reference inline (not just first-5)
because rename drift is the kind of thing reviewers must see in full.
Net: 53 claim-envelope assertions all pass; no regressions in other
test surfaces (property 29/0, security 10/0, proof 25/0/1skip, smoke
40/0, structural E2E 53/0/1skip).
🔍 Hypatia Security ScanFindings: 96 issues detected
View findings[
{
"reason": "Issue in quality.yml",
"type": "missing_workflow",
"file": "quality.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in security-policy.yml",
"type": "missing_workflow",
"file": "security-policy.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Action actions/upload-artifact@v4 needs attention",
"type": "unpinned_action",
"file": "release.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action actions/download-artifact@v4 needs attention",
"type": "unpinned_action",
"file": "release.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
"type": "believe_me",
"file": "/home/runner/work/typed-wasm/typed-wasm/src/abi/TypedWasm/ABI/SessionProtocol.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "assert_total bypasses totality checker (1 occurrences, CWE-704)",
"type": "assert_total",
"file": "/home/runner/work/typed-wasm/typed-wasm/src/abi/TypedWasm/ABI/SessionProtocol.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
"type": "believe_me",
"file": "/home/runner/work/typed-wasm/typed-wasm/src/abi/TypedWasm/ABI/Echo.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "assert_total bypasses totality checker (1 occurrences, CWE-704)",
"type": "assert_total",
"file": "/home/runner/work/typed-wasm/typed-wasm/src/abi/TypedWasm/ABI/Echo.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
"type": "believe_me",
"file": "/home/runner/work/typed-wasm/typed-wasm/src/abi/TypedWasm/ABI/ResourceCapabilities.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
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.
Summary
Phase 0 housekeeping — the ROADMAP truthfulness audit that
docs/PRODUCTION-PATH.adoc§Phase 0 requires before advancing to Phase 1. Three real drifts found and fixed, plus a new aspect-test section that catches this drift class going forward.Drifts found and fixed
1.
spec/10-levels-for-wasm.adoc→spec/type-safety-levels-for-wasm.adocThe file was renamed but 5 callers still pointed at the old path:
ROADMAP.adocREADME.adocEXPLAINME.adoc(twice).claude/CLAUDE.mdAll updated.
2.
EXPLAINME.adocIdris2 ABI table out of dateEXPLAINME described a pre-restructure architecture (Types.idr / Layout.idr / Access.idr / Effects.idr / Linearity.idr / Foreign.idr). The actual structure is
src/abi/TypedWasm/ABI/{Region, TypedAccess, Pointer, Levels, Effects, Lifetime, Linear, MultiModule, Layout, Proofs, SessionProtocol, ResourceCapabilities, Choreography, Tropical, Epistemic, Echo, ModuleIsolation}.idr.Rewrote claim 3's evidence sentence and the full file table to match reality, with each entry naming the actual load-bearing types from each file (
Region.idr→ Schema, sizeOf, alignOf;TypedAccess.idr→ HostType, RegionPredicate;Levels.idr→ Level1_InstructionValidity through Level10_Linear data types; etc.).3.
src/abi/Foreign.idrdoesn't existEXPLAINME's file table claimed
Foreign.idrprovided "FFI declarations: C header generation from Idris2 ABI". The file doesn't exist (the FFI surface isffi/zig/src/main.zig, hand-maintained per the comment in that file's header). Removed the stale row.Drift-detection: claim-envelope §8
To prevent this class of drift recurring,
tests/aspect/claim-envelope.mjsgets a new section 8 — "Path references in docs resolve to real files":typedqliser/,affinescript/,ephapax/,standards/,hypatia/,typell/,vql-ut/,echidna/), templated paths ({{...}}), well-known non-repo paths (github.com,/home/runner/)/(those are prose conventions like "see PROOF-NEEDS.md")Section 8 now finds 31 path references across the 4 docs, all resolving. Before this PR's fixes: 7 stale (the EXPLAINME refs to old
src/abi/paths).Verification
All test surfaces green after the changes:
Files changed
.claude/CLAUDE.md— spec path fixEXPLAINME.adoc— spec path fix + claim 3 evidence rewrite + file table restructureREADME.adoc— spec path fix in Quick TourROADMAP.adoc— spec path fix in Current Statetests/aspect/claim-envelope.mjs— new section 8 (path-reference drift detection)Closes Phase 0
This PR completes the ROADMAP truthfulness audit checklist item in #48. After it lands, Phase 0's housekeeping subsection is fully closed. Remaining Phase 0 items are Track A's multi-PR codegen pipeline work and Track B's cross-repo AffineScript migration — both outside what one session can ship.
Generated by Claude Code