Follow-up to PR #62 (crash-consistency keystone). See docs/THEORY-CRASH-CONSISTENCY.adoc § Frontier C and docs/SEAM_ANALYSIS_AND_IDRIS2_PLAN.md.
Statement
valence-shell's Idris 2 proof tree is intended to extract to typed-WASM. The crash story at the WASM boundary is different from the crash story at the syscall boundary:
- The WASM host can terminate the module mid-instruction; the host observes the linear memory at the termination point.
- The WASM module has no syscall-level atomicity guarantee on its own; whatever atomicity exists comes from host import-function contracts.
Proposed approach
Define a WasmCrashPoint inductive parallel to CrashPoint but indexed by WASM instruction boundaries. Prove that for each FilesystemOp as compiled to typed-WASM, the only host-observable crash points coincide with import-function boundaries — and that import-function contracts then provide the atomicity story. Two-level proof: source-level keystone (this repo) + compilation-preserves-keystone (typed-wasm sibling).
Gates
Gates on typed-wasm proposal 0003 (cross-module L13).
Tier: S (Foundational gap, gated).
Follow-up to PR #62 (crash-consistency keystone). See
docs/THEORY-CRASH-CONSISTENCY.adoc§ Frontier C anddocs/SEAM_ANALYSIS_AND_IDRIS2_PLAN.md.Statement
valence-shell's Idris 2 proof tree is intended to extract to typed-WASM. The crash story at the WASM boundary is different from the crash story at the syscall boundary:
Proposed approach
Define a
WasmCrashPointinductive parallel toCrashPointbut indexed by WASM instruction boundaries. Prove that for eachFilesystemOpas compiled to typed-WASM, the only host-observable crash points coincide with import-function boundaries — and that import-function contracts then provide the atomicity story. Two-level proof: source-level keystone (this repo) + compilation-preserves-keystone (typed-wasm sibling).Gates
Gates on
typed-wasmproposal 0003 (cross-module L13).Tier: S (Foundational gap, gated).