Feat/wasm verifier e2e

CHANGELOG.md

@@ -9,6 +9,18 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Breaking
 
+- Rocq output: the per-spec `_specs` lists are now **assertion-valued** —
+  `Definition <mod>__<SpecName>_specs : list assertion := (@nil assertion).` —
+  matching the downstream wasm-verifier contract
+  (`ValidSpec`/`ValidExistsSpec`/`ValidUniqueSpec : module -> list assertion -> Prop`;
+  wasm-verifier PR #2 for `ValidSpec`, issue #6 for the existential pair). The
+  former `list N` index lists are gone; each group's WASM function indices are
+  preserved in a preceding `(* function indices: … *)` comment, and the
+  generated file now imports `From WasmVerifier Require Import Assertions.`
+  whenever at least one spec is present (zero-spec output is unchanged).
+  Assertion payloads are not synthesized yet — every list is emitted empty;
+  downstream provers carry the semantic content in standalone lemmas (see
+  `core/wasm-to-v/ROCQ_CONTRACT.md` → Migration).
 - `inference_wasm_codegen::CodegenOutput::spec_func_indices: Vec<u32>` →
   `spec_func_indices_by_spec: FxHashMap<String, Vec<u32>>`. The accessor renames
   to `spec_func_indices_by_spec()`. Library embedders of `core/inference` must

core/inference/src/lib.rs

@@ -761,8 +761,9 @@ fn module_is_import_free(wasm: &[u8]) -> bool {
 /// - `spec_funcs_by_spec`: WASM function indices that originated from `spec`
 ///   blocks, grouped by spec name (typically obtained from
 ///   [`CodegenOutput::spec_func_indices_by_spec`]). Emitted as per-spec
-///   `Definition <mod_name>__<SpecName>_specs : list N` definitions consumed
-///   by the corresponding `ValidModule` theorems. Pass an empty `FxHashMap`
+///   `Definition <mod_name>__<SpecName>_specs : list assertion` definitions
+///   (currently empty, indices carried in a comment) consumed by the
+///   corresponding `Valid*Spec` theorems. Pass an empty `FxHashMap`
 ///   when no spec marker is needed.
 ///
 /// # Errors

core/wasm-codegen/src/lib.rs

@@ -48,7 +48,7 @@
 
 use inference_ast::arena::AstArena;
 use inference_ast::ids::DefId;
-use inference_ast::nodes::Def;
+use inference_ast::nodes::{BlockKind, Def};
 use inference_type_checker::typed_context::TypedContext;
 use rustc_hash::FxHashMap;
 
@@ -71,11 +71,21 @@ pub use target::{CompilationMode, OptLevel, Target};
 /// place.
 pub use crate::spec_section::SECTION_NAME as SPEC_FUNCS_SECTION_NAME;
 
-/// Wire-format version of the `inference.spec_funcs` custom section payload.
-/// Decoders must reject payloads whose leading varuint32 does not equal this
-/// constant; bumping the value is a breaking change to the section format.
+/// Legacy wire-format version of the `inference.spec_funcs` payload (function
+/// indices only). Decoders accept this alongside
+/// [`SPEC_FUNCS_SECTION_VERSION_WITH_KINDS`]; the encoder emits it whenever
+/// every obligation is the default [`SpecObligationKind::Spec`].
 pub use crate::spec_section::SECTION_VERSION as SPEC_FUNCS_SECTION_VERSION;
 
+/// Wire-format version that additionally carries one [`SpecObligationKind`]
+/// byte per index. Emitted only when an `exists`/`unique` obligation is present.
+pub use crate::spec_section::SECTION_VERSION_WITH_KINDS as SPEC_FUNCS_SECTION_VERSION_WITH_KINDS;
+
+/// The downstream proof obligation a spec function carries (`Spec` / `Exists` /
+/// `Unique`), threaded through the `inference.spec_funcs` section so the Rocq
+/// translator can pick `ValidSpec` / `ValidExistsSpec` / `ValidUniqueSpec`.
+pub use crate::spec_section::SpecObligationKind;
+
 /// Generates WebAssembly binary from a typed AST for the specified target and compilation mode.
 ///
 /// `module_name` is written into the WASM module-name subsection and flows
@@ -533,6 +543,7 @@ fn register_function_indices(
         compiler.record_spec_index(
             &qualified_spec_name(&entry.module_path, &entry.spec_name),
             *assigned_idx,
+            spec_obligation_kind(arena, entry.def_id),
         );
     }
 
@@ -556,6 +567,7 @@ fn register_function_indices(
         compiler.record_spec_index(
             &qualified_spec_name(&entry.module_path, &entry.spec_name),
             *assigned_idx,
+            spec_obligation_kind(arena, entry.def_id),
         );
     }
 
@@ -578,6 +590,33 @@ fn register_function_indices(
     Ok(())
 }
 
+/// Recovers the downstream proof obligation a spec function carries from the
+/// quantifier on its body.
+///
+/// Inference's function-level quantifier convention (`fn f() forall { … }`,
+/// `fn f() exists { … }`, `fn f() unique { … }`) lowers the quantifier block
+/// *as* the function body, so the obligation kind is exactly the body block's
+/// [`BlockKind`]: `Exists` → [`SpecObligationKind::Exists`], `Unique` →
+/// [`SpecObligationKind::Unique`]. A `forall`, regular, or `assume` body — and
+/// any non-function def — is a universal safety obligation
+/// ([`SpecObligationKind::Spec`], the default), which the downstream contract
+/// discharges as `ValidSpec`. A quantifier written as a *nested* statement
+/// inside a regular body (`fn f() { exists { … } }`) leaves the body `Regular`
+/// and is treated as `Spec`; the established spec convention uses the
+/// function-level form.
+fn spec_obligation_kind(arena: &AstArena, def_id: DefId) -> SpecObligationKind {
+    match &arena[def_id].kind {
+        Def::Function { body, .. } => match arena[*body].block_kind {
+            BlockKind::Exists => SpecObligationKind::Exists,
+            BlockKind::Unique => SpecObligationKind::Unique,
+            BlockKind::Forall | BlockKind::Assume | BlockKind::Regular => {
+                SpecObligationKind::Spec
+            }
+        },
+        _ => SpecObligationKind::Spec,
+    }
+}
+
 /// A top-level free function to emit, tagged with its defining file's module
 /// path (empty for the entry file). The module path file-qualifies the
 /// function's flat WASM name so two files can each define a same-named function.

core/wasm-codegen/src/output.rs

@@ -83,8 +83,9 @@ pub struct CodegenOutput {
     ///
     /// Empty in `compile` mode. In `proof` mode, contains per-spec function
     /// indices in registration order. The Rocq translator uses this to emit
-    /// per-spec `Definition <mod>__<SpecName>_specs : list N` lists consumed
-    /// by the corresponding `ValidModule` theorems.
+    /// per-spec `Definition <mod>__<SpecName>_specs : list assertion` lists
+    /// (currently empty, indices carried in a comment) consumed by the
+    /// corresponding `Valid*Spec` theorems.
     spec_func_indices_by_spec: FxHashMap<String, Vec<u32>>,
 
     /// Per-function shadow-stack frame sizes in bytes, keyed by the structured