Add wasip2 envelope wall vocabulary

aver-cert/assets/wall/current/Wasip2Envelope.lean

@@ -0,0 +1,80 @@
+/-
+  Wasip2Envelope — target-specific vocabulary for the future WASI 0.2
+  Component Model certificate envelope.
+
+  This module intentionally does NOT parse, scan, or navigate component-model
+  syntax. It only defines the declared-length split the producer will state:
+
+      prefix ++ embedded_core_module ++ suffix
+
+  A future schema can feed the delivered component bytes into these definitions,
+  prove the declared split by equality, and then reuse the existing core-module
+  checks on the declared embedded module bytes. Schema 5 does not import this
+  vocabulary into acceptance, and the Rust verifier still rejects target
+  `wasip2` fail-closed before byte validation.
+-/
+import CertDecode
+
+namespace AverCert.Wasip2Envelope
+
+abbrev ByteSeq := List Nat
+
+def expectedKind : String := "prefix-core-suffix/v1"
+
+/-- Length-only declaration of a `prefix ++ embedded_core_module ++ suffix`
+    component split. Positions are derived only from these lengths. -/
+structure ComponentEnvelope where
+  prefixLen : Nat
+  embeddedCoreModuleLen : Nat
+  suffixLen : Nat
+deriving Repr, DecidableEq
+
+namespace ComponentEnvelope
+
+/-- The manifest kind string this declaration belongs to. -/
+def kind (_env : ComponentEnvelope) : String := expectedKind
+
+/-- Total component length described by the declaration. -/
+def componentLen (env : ComponentEnvelope) : Nat :=
+  env.prefixLen + env.embeddedCoreModuleLen + env.suffixLen
+
+/-- Start offset of the embedded Aver user-core module. -/
+def coreStart (env : ComponentEnvelope) : Nat := env.prefixLen
+
+/-- End offset of the embedded Aver user-core module. -/
+def coreEnd (env : ComponentEnvelope) : Nat :=
+  env.prefixLen + env.embeddedCoreModuleLen
+
+/-- Byte-list view of a little-endian encoded byte blob. -/
+def bytes (blob blobLen : Nat) : ByteSeq :=
+  CertDecode.takeBytes blobLen blob
+
+/-- Declared split of the delivered component, driven by lengths only.
+    The body extracts byte slices but never interprets component syntax. -/
+def split (env : ComponentEnvelope) (componentBytes componentLen : Nat) :
+    Option (ByteSeq × ByteSeq × ByteSeq) :=
+  if env.embeddedCoreModuleLen == 0 then none
+  else if componentLen == env.componentLen then
+    let allBytes := bytes componentBytes componentLen
+    some (
+      allBytes.take env.prefixLen,
+      (allBytes.drop env.coreStart).take env.embeddedCoreModuleLen,
+      (allBytes.drop env.coreEnd).take env.suffixLen
+    )
+  else none
+
+/-- Trust-bearing shape future wasip2 acceptance will consume: a component's
+    byte sequence splits into exactly the declared prefix, core module, and
+    suffix sequences. -/
+def splitsTo (env : ComponentEnvelope) (componentBytes componentLen : Nat)
+    (pre core post : ByteSeq) : Prop :=
+  env.split componentBytes componentLen = some (pre, core, post)
+
+/-- Convenience predicate when only the embedded core-module bytes are relevant. -/
+def declaresCore (env : ComponentEnvelope) (componentBytes componentLen : Nat)
+    (core : ByteSeq) : Prop :=
+  ∃ pre post, env.splitsTo componentBytes componentLen pre core post
+
+end ComponentEnvelope
+
+end AverCert.Wasip2Envelope

aver-cert/src/format.rs

@@ -139,7 +139,7 @@ pub const ARTIFACT_CERTIFICATE_ROOT: &str = "AverCert.Artifact.certificate";
 
 /// Identity of the exact checker-owned Lean wall shipped by this release.
 pub const CURRENT_WALL_ID: &str =
-    "sha256:b06a0b43554911693b6f8b4b539dff7bb82b2dc8b1081b956c3a5db5238df8a0";
+    "sha256:ea9bf24a9293ad5b107024e75eba4f8ed55575d02505084a19ea6d1f82d45f70";
 
 /// Complete host-import surface admitted by the wasm-gc certificate format.
 ///

aver-cert/src/wall.rs

@@ -19,6 +19,7 @@ pub const CERT_PLAN_CHECK: &str = include_str!("../assets/wall/current/PlanCheck
 pub const CERT_PLAN_LOWER: &str = include_str!("../assets/wall/current/PlanLower.lean");
 pub const CERT_PLAN_BYTES: &str = include_str!("../assets/wall/current/PlanBytes.lean");
 pub const CERT_WASM_SLICE: &str = include_str!("../assets/wall/current/WasmSlice.lean");
+pub const CERT_WASIP2_ENVELOPE: &str = include_str!("../assets/wall/current/Wasip2Envelope.lean");
 pub const CERT_EXPR_FRAGMENT_ACCEPTED: &str =
     include_str!("../assets/wall/current/ExprFragmentAccepted.lean");
 pub const CERT_ACCEPTED_ARTIFACT: &str =
@@ -83,7 +84,7 @@ pub struct Source {
 
 /// Exact checker-owned source set. Ordering is not part of the identity:
 /// [`compute_id`] sorts by filename before hashing.
-pub const SOURCES: [Source; 38] = [
+pub const SOURCES: [Source; 39] = [
     Source {
         name: "AcceptedArtifact.lean",
         contents: CERT_ACCEPTED_ARTIFACT,
@@ -232,6 +233,10 @@ pub const SOURCES: [Source; 38] = [
         name: "WasmSlice.lean",
         contents: CERT_WASM_SLICE,
     },
+    Source {
+        name: "Wasip2Envelope.lean",
+        contents: CERT_WASIP2_ENVELOPE,
+    },
     Source {
         name: "WidenedEnvelope.lean",
         contents: CERT_WIDENED_ENVELOPE,
@@ -240,11 +245,12 @@ pub const SOURCES: [Source; 38] = [
 
 /// Roots whose complete import graph is artifact-independent and can therefore
 /// be cached before a certificate is seen.
-pub const PRISTINE_ROOTS: [&str; 36] = [
+pub const PRISTINE_ROOTS: [&str; 37] = [
     "CertPrelude",
     "CertDecode",
     "ArithTemplateDerisk",
     "WasmSlice",
+    "Wasip2Envelope",
     "SchemaCore",
     "PlanCheck",
     "PlanLower",

docs/certificate-format.md

@@ -26,7 +26,7 @@ Schema version 4 differs from version 3 in exactly one point, of the same kind:
 
 Schema version 5 differs from version 4 in two related points: the manifest gained the required top-level `target` field, and `Schema.Holds` now checks the target/profile/ABI identifiers against fixed checker-owned constants. The only target admitted by version 5 is `"wasm-gc"`; a version-5 verifier MUST NOT accept a `schema_version: 4` package.
 
-The wall identity is computed, not assigned. It is the SHA-256 of a domain-separated, sorted, length-framed encoding of every wall source file plus the Lean toolchain pin, formatted as `sha256:` followed by 64 lowercase hex digits. The exact encoding: the ASCII bytes `aver-certificate-wall\0v1\0`, then the file count as a big-endian `u64`, then for each file in ascending filename order: the filename length as big-endian `u64`, the filename bytes, the contents length as big-endian `u64`, the contents bytes. The file set is the 38 embedded `.lean` wall sources plus one synthetic file named `lean-toolchain` whose contents are the embedded toolchain file hashed verbatim — currently the ASCII bytes `leanprover/lean4:v4.32.2` followed by one trailing newline (the file is embedded with `include_str!`, so the newline byte is part of the hashed contents; a reimplementation that hashes the trimmed pin computes a different identity). The current embedded wall identity is `sha256:b06a0b43554911693b6f8b4b539dff7bb82b2dc8b1081b956c3a5db5238df8a0` (`CURRENT_WALL_ID` in `format.rs`). The reference verifier recomputes this digest over its own embedded sources on first use and aborts if it disagrees with the compiled-in constant, so a verifier binary cannot silently ship a wall that does not match its advertised identity. A reimplementation MUST resolve `format.wall_id` only against wall source sets whose recomputed identity is byte-exact; it MUST NOT resolve a wall by name, path, or prefix.
+The wall identity is computed, not assigned. It is the SHA-256 of a domain-separated, sorted, length-framed encoding of every wall source file plus the Lean toolchain pin, formatted as `sha256:` followed by 64 lowercase hex digits. The exact encoding: the ASCII bytes `aver-certificate-wall\0v1\0`, then the file count as a big-endian `u64`, then for each file in ascending filename order: the filename length as big-endian `u64`, the filename bytes, the contents length as big-endian `u64`, the contents bytes. The file set is the 39 embedded `.lean` wall sources plus one synthetic file named `lean-toolchain` whose contents are the embedded toolchain file hashed verbatim — currently the ASCII bytes `leanprover/lean4:v4.32.2` followed by one trailing newline (the file is embedded with `include_str!`, so the newline byte is part of the hashed contents; a reimplementation that hashes the trimmed pin computes a different identity). The current embedded wall identity is `sha256:ea9bf24a9293ad5b107024e75eba4f8ed55575d02505084a19ea6d1f82d45f70` (`CURRENT_WALL_ID` in `format.rs`). The reference verifier recomputes this digest over its own embedded sources on first use and aborts if it disagrees with the compiled-in constant, so a verifier binary cannot silently ship a wall that does not match its advertised identity. A reimplementation MUST resolve `format.wall_id` only against wall source sets whose recomputed identity is byte-exact; it MUST NOT resolve a wall by name, path, or prefix.
 
 > **TODO-decision: freeze criteria.** Neither `format.version = 1` nor `schema_version = 5` is declared frozen yet. The criteria for freezing (what constitutes a compatible extension versus a version bump, and whether a frozen schema admits additive optional fields) are an open decision; section 11 states what bumps each identity today, the certificate-lifetime consequences, and the freeze proposal on the table. Until freeze, every schema change bumps `schema_version` and verifiers reject non-matching versions exactly.
 
@@ -344,7 +344,7 @@ What changes bump which identity:
 | 1 Versioning, wall identity | `aver-cert/src/format.rs` (`FORMAT_VERSION`, `CERT_SCHEMA_VERSION`, `TARGET_WASM_GC`, `PROFILE_ID`, `RUNTIME_ABI_WASM_GC`, `CURRENT_WALL_ID` — the inline identity value, `ARTIFACT_CERTIFICATE_ROOT`), `aver-cert/src/wall.rs` (`compute_id`, `current_id`, `resolve`, `SOURCES`, `LEAN_TOOLCHAIN` — the `include_str!` embedding that preserves the trailing newline), `aver-cert/assets/wall/current/lean-toolchain` (ends in a newline byte) |
 | 2.1 Producer layout convention | `aver-cert/src/engine/render_project.rs` (`write_project`, `sanitize_model_for_cert`, `render_artifact_certificate` — the emitted `#print axioms`, `render_artifact_soundness`), `aver-cert/src/engine/render_manifest.rs` (`render_final`), `src/main/commands.rs` (certify entry, model emission reuse), `tests/cert_certify_spec.rs` |
 | 2.2 Acceptance file-set contract | `aver-cert/src/verifier.rs` (`assemble_build` — staging loop, `is_checker_owned`, `lean_module_root`, `checker_witness` — the witness import list), `aver-cert/assets/wall/current/Schema.lean` (`Holds` — the only wall reference to `CertModule`), `aver-cert/assets/wall/current/AcceptedArtifactCore.lean` (family predicates binding `obligation.code`, not named definitions) |
-| 3, 4 Manifest schema, pinned vs declared | `aver-cert/src/verifier.rs` (`trusted_check`, `read_manifest_identity`, `require_supported_identity`, `read_candidates` — the exhaustive list of fields read on the acceptance path, `parse_termination`, `exact_object_fields`, `gate_candidate`, `checker_witness` — the `target`/`profile`/`abi` `rfl` pins, `report_face`, `manifest_face`, `explain` — the second manifest read and zero-export early return), `aver-cert/src/engine/mod.rs` (`ARTIFACT_TARGET`, `PROFILE_ID`, `RUNTIME_ABI`, `CERT_LEVEL`, contract strings), `aver-cert/src/engine/render_manifest.rs` (`render_manifest`, `render_manifest_lean`), `aver-cert/assets/wall/current/ClaimAxes.lean` (`ContractUse.contracts` — the canonical contract order, `contractsMatch` — exact list equality), `aver-cert/assets/wall/current/AcceptedArtifactCore.lean` (`exportsAccounted`, `declaredUncertifiedNames` — names-only byte accounting, `decodedStringHostRoles`), `tests/snapshots/cert_certify_spec__add_one_certificate_package.snap` (worked example) |
+| 3, 4 Manifest schema, pinned vs declared | `aver-cert/src/verifier.rs` (`trusted_check`, `read_manifest_identity`, `require_supported_identity`, `read_candidates` — the exhaustive list of fields read on the acceptance path, `parse_termination`, `exact_object_fields`, `gate_candidate`, `checker_witness` — the `target`/`profile`/`abi` `rfl` pins, `report_face`, `manifest_face`, `explain` — the second manifest read and zero-export early return), `aver-cert/src/engine/mod.rs` (`ARTIFACT_TARGET`, `PROFILE_ID`, `RUNTIME_ABI`, `CERT_LEVEL`, contract strings), `aver-cert/src/engine/render_manifest.rs` (`render_manifest`, `render_manifest_lean`), `aver-cert/assets/wall/current/ClaimAxes.lean` (`ContractUse.contracts` — the canonical contract order, `contractsMatch` — exact list equality), `aver-cert/assets/wall/current/AcceptedArtifactCore.lean` (`exportsAccounted`, `declaredUncertifiedNames` — names-only byte accounting, `decodedStringHostRoles`), `aver-cert/assets/wall/current/Wasip2Envelope.lean` (reserved declared-length component split vocabulary, not imported into schema 5 acceptance), `tests/snapshots/cert_certify_spec__add_one_certificate_package.snap` (worked example) |
 | 4.3 Three-state host-role decode | `aver-cert/assets/wall/current/CertDecode.lean` (`decodeRawExports`, `functionExports`, `decodeExports` — function-export projection, `AddSub.boxIdx`, `AddSub.toIndexIdx`, `AddSub.cmpIdx`, `AddSub.eqIdx`, `AddSub.Roles`, `AddSub.carrierHelperAbsent` — the exact pinned fact, `carrierState` — the carrier struct a declared table must name, `StringHost.classify`/`StringHost.roleTable` — defined-function order with duplicates retained), `aver-cert/assets/wall/current/ArithTemplateDerisk.lean` (`ArithRole`, `ArithHostParams`, `checkArithHostParams` — the LEB regime, `s33`, `boxTemplateBody`/`toIndexTemplateBody`/`addTemplateBody`/`subTemplateBody`/`mulTemplateBody`/`cmpTemplateBody`/`eqTemplateBody`, `arithHelperBody` — the role-to-bytes dispatch), `aver-cert/assets/wall/current/AcceptedArtifactCore.lean` (`bodyBytesAtFuncIndex`, `arithRoleCheck`, `arithTableCheck`, `decodedHostRoleTable`, `decodedStringHostRoles`), `aver-cert/assets/wall/current/SchemaCore.lean` (`Subject`, `Subject.hostRoles`) |
 | 5 Obligations, policies, acceptance | `aver-cert/assets/wall/current/SchemaCore.lean` (`Obligation`, `holds`, `holdsTotal`, `HoldsCore`, `Policy`, `TotalityRole`, `TerminationWitness`, `checkTerm`, `checkTermMutual`, `CAPABILITY_REGISTRY`), `aver-cert/assets/wall/current/Schema.lean` (`Holds`), `aver-cert/assets/wall/current/AcceptedArtifact.lean` (`accepted`), `aver-cert/assets/wall/current/AcceptedArtifactCore.lean` (`ArtifactData`, `claimsMatchManifest` — plan-pair vs export-name-list equalities per family, `claimObligationExports`, `exportsAccounted`, coverage/accounting/closure defs), `aver-cert/assets/wall/current/StandardFace.lean` (`checkedFaces`, `reportEntries`, `hostTableBound`), `aver-cert/assets/wall/current/ClaimAxes.lean` (`checked`, `canonicalTermination`) |
 | 6 Plan grammar, byte-lowering contract | `aver-cert/assets/wall/current/SchemaCore.lean` (all raw-plan types and node grammars), `aver-cert/assets/wall/current/PlanCheck.lean` (checkers, `encodeSymRawPlanToExprFragmentRawPlan` and `encodeSymBlockFuel` — the generic bridge and its fail-closed node cases, `hostRoleIdx?`/`structTyIdx?` — byte-derived index provenance, `stringEqPlanMatchesSymRawPlan`, `stringConcatPlanMatchesSymRawPlan`, `constructPlanMatchesSymRawPlan` — the non-encoded family bridges, `classifyRecursionPlanShape` — self-call pinned to the current function, `checkMutualPlanShape`/`recStepMutual` — tail-call target pinned to the SCC member set, profile strings), `aver-cert/assets/wall/current/PlanLower.lean`, `aver-cert/assets/wall/current/PlanBytes.lean` (ULEB/SLEB, `lower*CodeEntry`, `singleCarrierLocalBodyBytes`/`noLocalBodyBytes`/`carrierLocalsBodyBytes` — the carrier-state-selected locals prelude), `aver-cert/assets/wall/current/CertDecode.lean` (`carrierState` — the strict three-state carrier decode), `aver-cert/assets/wall/current/WasmSlice.lean` (`FuncBinding`, `exactFuncBindingForExport`, type matchers, `checkHostRoleFuncType`/`hostRoleFuncTypeMatches`/`hostTableFuncTypesMatch` — the host-table declared-function-type pin, `checkExprProjectionTypes`/`checkTagDispatchTypes` — the face-layout arity pins, closure scanner), `aver-cert/assets/wall/current/AcceptedArtifactCore.lean` (family `*PlanAccepted` predicates — separate `exportName`/`exportNameBytes` fields, `stringConcatNLocals`, `decodedCarrierIndex`/`decodedCarrierFreeClaims` — the String.concat-only three-state binding, `decodedStrictCarrierIndex`/`decodedObligationFacts` — the strict binding every other non-expression-fragment family keeps; the expression-fragment family is bound by neither and carries `symFragmentCarrierBound`/`symFragmentCarrierBindingRequired`/`fragPlanMentionsIntCarrier` instead, see `ExprFragmentAccepted.lean`), `aver-cert/src/engine/render_project.rs` (`render_expr_fragment_plans` — the emitted `rfl` surface) |

docs/certification-architecture.md

@@ -143,7 +143,8 @@ split while constructing the component, surfaced under the reserved
 rediscover the user core by walking component bytes. It should consume the
 declaration, split only by declared lengths, confirm byte equality against the
 caller-supplied component, and then run the core-module checks on the declared
-embedded module.
+embedded module. The reserved wall vocabulary for that future proof lives in
+`Wasip2Envelope.lean`; schema 5 does not import it into acceptance.
 
 ## Lean acceptance wall
 

src/codegen/wasip2/wrap.rs

@@ -95,13 +95,12 @@ impl Wasip2ComponentEnvelope {
 
         let mut ranges = Vec::new();
         for payload in Parser::new(0).parse_all(component) {
-            match payload.map_err(|error| {
+            if let Payload::ModuleSection {
+                unchecked_range, ..
+            } = payload.map_err(|error| {
                 Wasip2Error::Envelope(format!("cannot parse produced component: {error}"))
             })? {
-                Payload::ModuleSection {
-                    unchecked_range, ..
-                } => ranges.push(unchecked_range),
-                _ => {}
+                ranges.push(unchecked_range);
             }
         }
         let range = match ranges.as_slice() {

tests/snapshots/cert_certify_spec__add_one_certificate_package.snap

@@ -5,7 +5,7 @@ expression: golden
 == cert-manifest.json ==
 {
   "schema_version": 5,
-  "format": {"version": 1, "wall_id": "sha256:b06a0b43554911693b6f8b4b539dff7bb82b2dc8b1081b956c3a5db5238df8a0"},
+  "format": {"version": 1, "wall_id": "sha256:ea9bf24a9293ad5b107024e75eba4f8ed55575d02505084a19ea6d1f82d45f70"},
   "wasm": "add_one.wasm",
   "wasm_sha256": "5f41ddfa9a5a395546d0c21e00c232be77e330ea587b2666456f0488ff0450c9",
   "target": "wasm-gc",