Umbrella: proof-mode e2e readiness — any valid program + any spec => dischargeable .v

[0xGeorgii]

Tracking umbrella for everything needed on the inference side so that any valid Inference program (or linked wasm 1.0 module set) with any properly-defined spec block lowers through infc --mode proof into a .v that type-checks against wasm-verifier with all obligations stated correctly and dischargeable. Companion verifier-side umbrella: Inference-Global-Software/wasm-verifier (see the cross-linked issue there).

What already works (verified 2026-08-08, main@4f2ddf1)

The post-#299 hassert pipeline is live end to end for the forall/scalar fragment: spec fns are omitted from the module record, obligations travel as real hassert payloads (inference.hspecs) and are printed as list hassert _specs targeting the hassert-valued ValidSpec; two generated modules (with_spec.v, rocq_prime_example.v — incl. a genuine br_if loop) are fully Qed downstream.

Soundness / meaningfulness (obligations must say what the spec says)

• hassert: guard T_app-bearing Univ-mode comparisons and call atoms with HA_defined/HA_app_ok (vacuous-obligation soundness hole) #353 — unguarded Univ-mode ==/</<=/>/>=/call atoms over T_app: false specs provable (verified)
• Spec bodies that compute degrade to HA_true silently (vacuous obligation, no diagnostic) #356 — computational spec bodies silently become HA_true
• Narrow-scalar @ and spec params emit unconstrained obligations (missing range antecedents) #357 — narrow-scalar @/params over-quantify (missing range antecedents)

Spec coverage ("any spec block")

• Proof mode: support exists/assume/unique-quantified spec functions (lift P001; quantifier-kind channel; kind-selected theorems) #354 — exists/assume/unique spec functions rejected (P001); kind channel + kind-selected theorems (refs Full support for the unique non-deterministic block (currently proof-inert) #318)
• hassert expressiveness: arrays, struct fields, memory, iteration, aggregate @ (lift P002/P004/P008) #355 — hassert expressiveness: arrays/structs/memory/iteration/aggregate-@ (P002/P004/P008)

Program coverage ("any valid program")

• Codegen panics (todo!) on accepted programs: strings, unit literals, Stmt::TypeDef, Expr::Type, complex assignment targets #360 — codegen todo!() panics on accepted programs (strings, type stmt, …; refs codegen: reject generic functions at the codegen boundary with a targeted diagnostic #320)
• Existing: Proof-mode: discharge no-overflow obligations for add/sub/mul (currently silent wraparound) #316 (overflow obligations), Proof-mode: discharge dynamic array bounds as Rocq proof obligations #214/Static rule: require a dominating in-bounds guard before dynamic array indexing #212/Optimization: eliminate runtime bounds guard for provably in-bounds dynamic indices #215 (dynamic-bounds obligations — note proof-mode artifact is currently unguarded where compile mode traps), Configurable, statically-known linear-memory size for generated WASM (CLI flag + [wasm] Inference.toml) #221/Compilation parameter: number of linear-memory pages to allocate (Inference.toml + CLI) #210/Static check + diagnostics: program memory footprint must fit the requested pages (no OOM) #211 (memory sizing), Memory grow #170 (memory.grow)

Linked wasm 1.0 modules

• infs project-mode build drops [wasm-dependencies] and -L: linked (proof) builds cannot resolve externals #361 — infs project mode drops [wasm-dependencies]/-L (linked proof builds broken)
• Cross-module specs: allow obligations to reference linked external functions (post-link T_app) + write-set contracts #362 — specs over linked externals (post-link T_app) + write-set contracts (refs linker/type-checker: mut on external fn parameters as a linker-verified write-set declaration #333)
• Linker envelope: accept real-toolchain externals (own globals/data/tables; integer width conversions) for proof mode #363 — envelope: real-toolchain externals (own globals/data/tables; width conversions)

Artifact & process

• wasm-to-v: emit compilable proof skeletons (Admitted.) instead of Qed. on open proofs #358 — emit compilable skeletons (Admitted.), not Qed. on open proofs
• CI: type-check generated .v against the real wasm-verifier + stub-drift gate #359 — CI against the real wasm-verifier + stub-drift gate (refs wasm-to-v: element/data segment emission does not type-check against the proof contract; br_table drops its default label #346, wasm-to-v: ROCQ_CONTRACT.md describes the post-#21 ValidModule/ValidSpec split but the emitter still writes the pre-#21 2-ary form #277)
• Disposition of feat/wasm-verifier-e2e (draft PR #235): superseded by the hassert pipeline #364 — disposition of feat/wasm-verifier-e2e / draft PR Feat/wasm verifier e2e #235 (superseded)
• wasm-to-v: GC composite types silently emit garbage; unwrap aborts on malformed foreign wasm #365 — foreign-wasm robustness: GC-type silent garbage, unwrap aborts (refs wasm-to-v: element/data segment emission does not type-check against the proof contract; br_table drops its default label #346)
• Existing: wasm-to-v: element/data segment emission does not type-check against the proof contract; br_table drops its default label #346 (data/element/br_table emission defects), wasm-to-v: ROCQ_CONTRACT.md describes the post-#21 ValidModule/ValidSpec split but the emitter still writes the pre-#21 2-ary form #277 (contract doc — substance now fixed by Spec obligations as hassert values: the full wasm-verifier contract — A042, hassert IR/codec, AST-to-hassert translation, section embedding, and the .v emission flip #299; likely closable)

Provenance: full cross-repo audit + live pipeline probe + adversarial verification, 2026-08-08.