pub const CERT_DECODE: &str = "/-\n CertDecode \u{2014} checker-owned, in-kernel decoder for the AverUserProfile/v1\n certificate profile. Given a wasm-gc module as a little-endian big-`Nat`\n plus a byte length, it decodes the profile-relevant sections into PURE DATA\n (`rfl`-comparable): a typed type-section IR, raw import/export indices, the\n Int carrier type index, exact data/code locations, and per-function `WCode`\n (arity from the type section, nlocals from the locals declaration, body as\n `List CertPrelude.WInstr` \u{2014} the full 39-opcode fragment, if/else/end folded\n into `WInstr.ifElse`).\n\n Differential fixtures pin this decoder against the producer decoder and the\n standalone certkit reference implementation.\n\n Construction constraints (from the C2 kill-fast probes):\n * All recursion is STRUCTURAL or on an explicit fuel `Nat`. There is no\n well-founded recursion and no `partial def`, so every `decode\u{2026}` reduces in\n the kernel and a certificate witness closes by `rfl` (axioms `[propext]`).\n * The byte representation is one little-endian big-`Nat` + a length. Reading a\n byte is `n &&& 0xff`, advancing is `n >>> 8`, and skipping a section body of\n `size` bytes is a single GMP-accelerated shift `n >>> (8 * size)`.\n\n Scope is PROFILE-ONLY and REJECT-BY-DEFAULT. The type-section subset decoded\n is exactly what the Aver wasm-gc compiler emits and the fixtures exercise:\n rec groups, optional `sub`/`sub final` prefixes, `func`/`struct`/`array`\n composite types, numeric valtypes (0x7b\u{2013}0x7f), reference valtypes\n (0x63/0x64 + heaptype), and the abstract-heap valtype shorthands (0x6a\u{2013}0x73,\n e.g. `eqref`). Anything outside this subset (a valtype/opcode the emitter does\n not produce, an overlong LEB, a truncated section) decodes to `none` \u{2014} never a\n garbage success. `moduleFramingValid` separately guards the entire module;\n prefix-preserving section projections remain useful for isolated negative\n tests, while whole-artifact admission requires strict global framing.\n-/\nimport CertPrelude\nopen CertPrelude\n\nnamespace CertDecode\n\n/-- ASCII/latin1 name bytes \u{2192} `String` (defeq to the string literal under `rfl`,\n so the certified export names are anchored, not weakened to byte lists). -/\ndef mkName (ns : List Nat) : String := String.ofList (ns.map (fun n => Char.ofNat n))\n\n/-- Peel `count` bytes off the little-endian big-`Nat` into a `List Nat`. -/\ndef takeBytes : Nat \u{2192} Nat \u{2192} List Nat\n | 0, _ => []\n | k+1, n => (n &&& 0xff) :: takeBytes k (n >>> 8)\n\n/- ===================================================================== -/\n/- LEB128 -/\n/- ===================================================================== -/\n\n/-- Canonical unsigned LEB128 over `(n, len)`; overlong trailing-zero \u{2192} none. -/\ndef uleb : Nat \u{2192} Nat \u{2192} Nat \u{2192} Nat \u{2192} Nat \u{2192} Option (Nat \u{d7} Nat \u{d7} Nat)\n | 0, _, _, _, _ => none\n | fuel+1, acc, shift, n, len =>\n if len == 0 then none else\n let b := n &&& 0xff\n let n\' := n >>> 8\n let acc\' := acc + ((b &&& 0x7f) <<< shift)\n if b < 128 then\n if (shift != 0) && (b == 0) then none else some (acc\', n\', len-1)\n else uleb fuel acc\' (shift+7) n\' (len-1)\n\n@[inline] def readU (n len : Nat) : Option (Nat \u{d7} Nat \u{d7} Nat) := uleb 5 0 0 n len\n\n/-- Signed LEB128 (i64/i32 const immediates, s33 heaptypes / typeidx). -/\ndef sleb : Nat \u{2192} Int \u{2192} Nat \u{2192} Nat \u{2192} Nat \u{2192} Option (Int \u{d7} Nat \u{d7} Nat)\n | 0, _, _, _, _ => none\n | fuel+1, acc, shift, n, len =>\n if len == 0 then none else\n let b := n &&& 0xff\n let n\' := n >>> 8\n let acc\' := acc + (Int.ofNat (b &&& 0x7f)) * ((2 : Int) ^ shift)\n if b < 128 then\n let signed := if (b &&& 0x40) != 0 then acc\' - ((2 : Int) ^ (shift+7)) else acc\'\n some (signed, n\', len-1)\n else sleb fuel acc\' (shift+7) n\' (len-1)\n\n@[inline] def readS (n len : Nat) : Option (Int \u{d7} Nat \u{d7} Nat) := sleb 10 0 0 n len\n\n/-- Spec-bounded signed heap type: at most five bytes and in s33 range. -/\ndef readS33 (n len : Nat) : Option (Int \u{d7} Nat \u{d7} Nat) :=\n match sleb 5 0 0 n len with\n | some (v, n1, len1) =>\n if -(Int.ofNat (2 ^ 32)) \u{2264} v \u{2227} v < Int.ofNat (2 ^ 32) then\n some (v, n1, len1)\n else none\n | none => none\n\n/- ===================================================================== -/\n/- Section walk -/\n/- ===================================================================== -/\n\n/-- Isolate exactly `len` low bytes. Besides enforcing the declared section\n boundary, this keeps every subsequent byte shift proportional to the\n payload being decoded instead of to the remaining module suffix. -/\ndef isolateBytes (n len : Nat) : Nat :=\n n &&& ((1 <<< (8 * len)) - 1)\n\n/-- A bounded section table. Payloads are stored as exact low-byte slices, so\n no consumer retains or shifts the enclosing module suffix. -/\nstructure ModuleView where\n sections : List (Nat \u{d7} Nat \u{d7} Nat)\n\ndef sectionTable : Nat \u{2192} Nat \u{2192} Nat \u{2192} Option (List (Nat \u{d7} Nat \u{d7} Nat))\n | 0, _, _ => none\n | fuel+1, n, len =>\n if len == 0 then some [] else\n let id := n &&& 0xff\n let n1 := n >>> 8\n match readU n1 (len - 1) with\n | none => some []\n | some (size, n2, len2) =>\n if size \u{2264} len2 then\n match sectionTable fuel (n2 >>> (8 * size)) (len2 - size) with\n | none => none\n | some rest => some ((id, isolateBytes n2 size, size) :: rest)\n else some []\n\ndef ModuleView.payload (view : ModuleView) (target : Nat) : Option (Nat \u{d7} Nat) :=\n (view.sections.find? (fun entry => entry.1 == target)).map\n (fun entry => (entry.2.1, entry.2.2))\n\n/-- Validate the header and materialize the bounded section-table prefix in one\n pass. A malformed frame terminates the table: already-complete earlier\n sections remain independently decodable, while that section and every\n later section are absent. The separate whole-module framing guard still\n rejects malformed modules globally. -/\ndef moduleView (modBytes modLen : Nat) : Option ModuleView :=\n if 8 \u{2264} modLen \u{2227} (modBytes &&& 0xffffffffffffffff) = 0x000000016d736100 then\n (sectionTable 64 (modBytes >>> 64) (modLen - 8)).map (fun sections => \u{27e8}sections\u{27e9})\n else none\n\n/-- Strict whole-file framing, intentionally separate from prefix-decoding\n `moduleView`: every canonical section-size LEB must be in bounds and the\n declared module length must be exhausted within 64 section frames. -/\ndef sectionFramingValid : Nat \u{2192} Nat \u{2192} Nat \u{2192} Bool\n | 0, _, len => len == 0\n | fuel+1, n, len =>\n if len == 0 then true else\n match readU (n >>> 8) (len - 1) with\n | none => false\n | some (size, payload, payloadAndRestLen) =>\n size \u{2264} payloadAndRestLen &&\n sectionFramingValid fuel (payload >>> (8 * size))\n (payloadAndRestLen - size)\n\ndef moduleFramingValid (modBytes modLen : Nat) : Bool :=\n 8 \u{2264} modLen &&\n (modBytes &&& 0xffffffffffffffff) == 0x000000016d736100 &&\n sectionFramingValid 64 (modBytes >>> 64) (modLen - 8)\n\n/-- Header-validated exact payload of the first section with id `target`. All\n section decoders share this one framing implementation. -/\ndef modulePayload (target modBytes modLen : Nat) : Option (Nat \u{d7} Nat) :=\n (moduleView modBytes modLen).bind (fun view => view.payload target)\n\n/- ===================================================================== -/\n/- Type section: one exact typed IR shared by every checker projection -/\n/- ===================================================================== -/\n\n/-- Exact wasm value-type form admitted by this certificate profile. Tags are\n retained because nullability (`0x63`/`0x64`) and abstract shorthands are\n byte-significant even when a downstream projection ignores the detail. -/\ninductive ValType\n | numeric (tag : Nat)\n | abstract (tag : Nat)\n | ref (tag : Nat) (heap : Int)\nderiving Repr, DecidableEq\n\ninductive StorageType\n | packed (tag : Nat)\n | val (type : ValType)\nderiving Repr, DecidableEq\n\nstructure FieldType where\n storage : StorageType\n mutability : Nat\nderiving Repr, DecidableEq\n\ninductive CompositeType\n | funcType (params results : List ValType)\n | structType (fields : List FieldType)\n | arrayType (field : FieldType)\nderiving Repr, DecidableEq\n\ninductive SubtypeForm\n | plain\n | sub (supertypes : List Nat)\n | subFinal (supertypes : List Nat)\nderiving Repr, DecidableEq\n\n/-- One flattened subtype in absolute type-index order. -/\nstructure TypeEntry where\n form : SubtypeForm\n composite : CompositeType\nderiving Repr, DecidableEq\n\n/-- One strict type-section pass plus compatibility summaries used by WCode. -/\nstructure TypeInfo where\n nfields : List Nat\n arityIndex : Array Nat\n nfieldIndex : Array Nat\n carrier : Option Nat\n entries : List TypeEntry\n entryIndex : Array TypeEntry\n\ndef readValType (n len : Nat) : Option (ValType \u{d7} Nat \u{d7} Nat) :=\n if len == 0 then none else\n let tag := n &&& 0xff\n let n1 := n >>> 8\n let len1 := len - 1\n if tag == 0x7f || tag == 0x7e || tag == 0x7d || tag == 0x7c || tag == 0x7b then\n some (.numeric tag, n1, len1)\n else if tag == 0x63 || tag == 0x64 then\n match readS33 n1 len1 with\n | some (heap, n2, len2) => some (.ref tag heap, n2, len2)\n | none => none\n else if decide (0x6a \u{2264} tag \u{2227} tag \u{2264} 0x73) then\n some (.abstract tag, n1, len1)\n else none\n\ndef readValTypes : Nat \u{2192} Nat \u{2192} Nat \u{2192} Option (List ValType \u{d7} Nat \u{d7} Nat)\n | 0, n, len => some ([], n, len)\n | k+1, n, len =>\n match readValType n len with\n | none => none\n | some (type, n1, len1) =>\n match readValTypes k n1 len1 with\n | none => none\n | some (rest, n2, len2) => some (type :: rest, n2, len2)\n\ndef readStorageType (n len : Nat) : Option (StorageType \u{d7} Nat \u{d7} Nat) :=\n if len == 0 then none else\n let tag := n &&& 0xff\n if tag == 0x78 || tag == 0x77 then some (.packed tag, n >>> 8, len - 1)\n else (readValType n len).map (fun p => (.val p.1, p.2.1, p.2.2))\n\ndef readField (n len : Nat) : Option (FieldType \u{d7} Nat \u{d7} Nat) :=\n match readStorageType n len with\n | none => none\n | some (storage, n1, len1) =>\n if len1 == 0 then none else\n let mutability := n1 &&& 0xff\n if mutability == 0 || mutability == 1 then\n some (\u{27e8}storage, mutability\u{27e9}, n1 >>> 8, len1 - 1)\n else none\n\ndef readFields : Nat \u{2192} Nat \u{2192} Nat \u{2192} Option (List FieldType \u{d7} Nat \u{d7} Nat)\n | 0, n, len => some ([], n, len)\n | k+1, n, len =>\n match readField n len with\n | none => none\n | some (field, n1, len1) =>\n match readFields k n1 len1 with\n | none => none\n | some (rest, n2, len2) => some (field :: rest, n2, len2)\n\ndef readUlebs : Nat \u{2192} Nat \u{2192} Nat \u{2192} Option (List Nat \u{d7} Nat \u{d7} Nat)\n | 0, n, len => some ([], n, len)\n | k+1, n, len =>\n match readU n len with\n | none => none\n | some (value, n1, len1) =>\n match readUlebs k n1 len1 with\n | none => none\n | some (rest, n2, len2) => some (value :: rest, n2, len2)\n\n/-- Cursor-only compatibility projection used by instruction scanners. -/\ndef skipUlebs (k n len : Nat) : Option (Nat \u{d7} Nat) :=\n (readUlebs k n len).map (fun p => (p.2.1, p.2.2))\n\ndef readCompositeType (n len : Nat) : Option (CompositeType \u{d7} Nat \u{d7} Nat) :=\n if len == 0 then none else\n let tag := n &&& 0xff\n let n1 := n >>> 8\n let len1 := len - 1\n if tag == 0x60 then\n match readU n1 len1 with\n | none => none\n | some (np, n2, len2) =>\n match readValTypes np n2 len2 with\n | none => none\n | some (params, n3, len3) =>\n match readU n3 len3 with\n | none => none\n | some (nr, n4, len4) =>\n match readValTypes nr n4 len4 with\n | some (results, n5, len5) => some (.funcType params results, n5, len5)\n | none => none\n else if tag == 0x5f then\n match readU n1 len1 with\n | none => none\n | some (nf, n2, len2) =>\n match readFields nf n2 len2 with\n | some (fields, n3, len3) => some (.structType fields, n3, len3)\n | none => none\n else if tag == 0x5e then\n match readField n1 len1 with\n | some (field, n2, len2) => some (.arrayType field, n2, len2)\n | none => none\n else none\n\ndef readSubtypeForm (n len : Nat) : Option (SubtypeForm \u{d7} Nat \u{d7} Nat) :=\n if len == 0 then none else\n let tag := n &&& 0xff\n if tag == 0x50 || tag == 0x4f then\n match readU (n >>> 8) (len - 1) with\n | none => none\n | some (count, n1, len1) =>\n match readUlebs count n1 len1 with\n | none => none\n | some (supertypes, n2, len2) =>\n if tag == 0x50 then some (.sub supertypes, n2, len2)\n else some (.subFinal supertypes, n2, len2)\n else some (.plain, n, len)\n\ndef readTypeEntry (n len : Nat) : Option (TypeEntry \u{d7} Nat \u{d7} Nat) :=\n match readSubtypeForm n len with\n | none => none\n | some (form, n1, len1) =>\n match readCompositeType n1 len1 with\n | none => none\n | some (composite, n2, len2) =>\n some (\u{27e8}form, composite\u{27e9}, n2, len2)\n\ndef readTypeEntries : Nat \u{2192} Nat \u{2192} Nat \u{2192} Option (List TypeEntry \u{d7} Nat \u{d7} Nat)\n | 0, n, len => some ([], n, len)\n | k+1, n, len =>\n match readTypeEntry n len with\n | none => none\n | some (entry, n1, len1) =>\n match readTypeEntries k n1 len1 with\n | none => none\n | some (rest, n2, len2) => some (entry :: rest, n2, len2)\n\n/-- Decode the declared rectype vector, flattening explicit rec groups into one\n absolute type-index order. This is the only type grammar parser. -/\ndef decRecVec : Nat \u{2192} Nat \u{2192} Nat \u{2192} Option (List TypeEntry \u{d7} Nat \u{d7} Nat)\n | 0, n, len => some ([], n, len)\n | k+1, n, len =>\n if len == 0 then none else\n if (n &&& 0xff) == 0x4e then\n match readU (n >>> 8) (len - 1) with\n | none => none\n | some (count, n1, len1) =>\n match readTypeEntries count n1 len1 with\n | none => none\n | some (group, n2, len2) =>\n match decRecVec k n2 len2 with\n | none => none\n | some (rest, n3, len3) => some (group ++ rest, n3, len3)\n else\n match readTypeEntry n len with\n | none => none\n | some (entry, n1, len1) =>\n match decRecVec k n1 len1 with\n | none => none\n | some (rest, n2, len2) => some (entry :: rest, n2, len2)\n\ndef StorageType.tag : StorageType \u{2192} Nat\n | .packed tag => tag\n | .val (.numeric tag) => tag\n | .val (.abstract tag) => tag\n | .val (.ref tag _) => tag\n\ndef TypeEntry.arity (entry : TypeEntry) : Nat :=\n match entry.composite with\n | .funcType params _ => params.length\n | _ => 0\n\ndef TypeEntry.fieldCount (entry : TypeEntry) : Nat :=\n match entry.composite with\n | .structType fields => fields.length\n | _ => 0\n\ndef TypeEntry.isCarrier (entry : TypeEntry) : Bool :=\n match entry.composite with\n | .structType fields =>\n fields.length == 3 && (fields[0]?).map (fun f => f.storage.tag) == some 0x7e &&\n (fields[2]?).map (fun f => f.storage.tag) == some 0x7f\n | _ => false\n\ndef firstCarrier : Nat \u{2192} List TypeEntry \u{2192} Option Nat\n | _, [] => none\n | idx, entry :: rest =>\n if entry.isCarrier then some idx else firstCarrier (idx + 1) rest\n\ndef decodeTypes (n len : Nat) : Option TypeInfo :=\n match modulePayload 1 n len with\n | none => none\n | some (tN, tLen) =>\n match readU tN tLen with\n | none => none\n | some (count, n1, len1) =>\n match decRecVec count n1 len1 with\n | some (entries, _, 0) =>\n let arities := entries.map TypeEntry.arity\n let nfields := entries.map TypeEntry.fieldCount\n some { nfields := nfields\n , arityIndex := arities.toArray\n , nfieldIndex := nfields.toArray\n , carrier := firstCarrier 0 entries\n , entries := entries\n , entryIndex := entries.toArray }\n | _ => none\n\n/-- The Int carrier struct type index. -/\ndef decodeCarrier (n len : Nat) : Option Nat :=\n match decodeTypes n len with\n | some ti => ti.carrier\n | none => none\n\n/-- The decoded struct-field count at one type index. Non-struct type entries\n have count zero; an out-of-range index or malformed type section is\n rejected. -/\ndef decodeStructFieldCount (n len typeidx : Nat) : Option Nat :=\n match decodeTypes n len with\n | some ti => ti.nfieldIndex[typeidx]?\n | none => none\n\n/- ===================================================================== -/\n/- Function / import / export / data sections -/\n/- ===================================================================== -/\n\n/-- Read `k` type indices (function section entries). -/\ndef decFuncVec : Nat \u{2192} Nat \u{2192} Nat \u{2192} Option (List Nat \u{d7} Nat \u{d7} Nat)\n | 0, n, len => some ([], n, len)\n | k+1, n, len =>\n match readU n len with\n | none => none\n | some (t, n1, len1) =>\n match decFuncVec k n1 len1 with\n | none => none\n | some (rest, n2, len2) => some (t :: rest, n2, len2)\n\n/-- Per-defined-function type index (function section). -/\ndef decodeFuncTypes (n len : Nat) : Option (List Nat) :=\n match modulePayload 3 n len with\n | none => some []\n | some (fN, fLen) =>\n match readU fN fLen with\n | none => none\n | some (cnt, n1, len1) =>\n match decFuncVec cnt n1 len1 with\n | none => none\n | some (ts, _, 0) => some ts\n | some _ => none\n\n/-! The raw module-indexing records below retain descriptor kinds and byte-exact\n names. Profile-specific APIs are projections of this one strict parse. -/\n\nstructure ImportEntry where\n moduleName : List Nat\n fieldName : List Nat\n kind : Nat\n funcTypeIdx : Option Nat\nderiving Repr, DecidableEq\n\nstructure ExportEntry where\n name : List Nat\n kind : Nat\n idx : Nat\nderiving Repr, DecidableEq\n\n/-- A bounded raw wasm name. -/\ndef readName (n len : Nat) : Option (List Nat \u{d7} Nat \u{d7} Nat) :=\n match readU n len with\n | none => none\n | some (nameLen, bytes, bytesLen) =>\n if nameLen \u{2264} bytesLen then\n some (takeBytes nameLen bytes, bytes >>> (8 * nameLen), bytesLen - nameLen)\n else none\n\n/-- Skip exactly one import-descriptor value type. Import descriptors admit\n the `0x69` abstract shorthand in addition to the profile type-section IR. -/\ndef skipImportValType (n len : Nat) : Option (Nat \u{d7} Nat) :=\n if len != 0 && (n &&& 0xff) == 0x69 then some (n >>> 8, len - 1)\n else (readValType n len).map (fun p => (p.2.1, p.2.2))\n\n/-- Skip one table/memory limits descriptor. This is the exact descriptor\n subset admitted by the certificate wasm slicer. -/\ndef skipLimits (n len : Nat) : Option (Nat \u{d7} Nat) :=\n match readU n len with\n | none => none\n | some (flags, n1, len1) =>\n if flags < 16 then\n match readU n1 len1 with\n | none => none\n | some (_, n2, len2) =>\n let afterMax :=\n if (flags &&& 0x01) != 0 then readU n2 len2 else some (0, n2, len2)\n match afterMax with\n | none => none\n | some (_, n3, len3) =>\n if (flags &&& 0x08) != 0 then\n match readU n3 len3 with\n | some (_, n4, len4) => some (n4, len4)\n | none => none\n else some (n3, len3)\n else none\n\n/-- Parse one import descriptor. Function imports retain their type index;\n table, memory, global, and tag imports are validated but store `none`. -/\ndef readImportDesc (n len : Nat) : Option (Nat \u{d7} Option Nat \u{d7} Nat \u{d7} Nat) :=\n if len == 0 then none else\n let kind := n &&& 0xff\n let rest := n >>> 8\n let restLen := len - 1\n if kind == 0x00 then\n match readU rest restLen with\n | some (typeIdx, tail, tailLen) => some (kind, some typeIdx, tail, tailLen)\n | none => none\n else if kind == 0x01 then\n match skipImportValType rest restLen with\n | some (limits, limitsLen) =>\n (skipLimits limits limitsLen).map (fun p => (kind, none, p.1, p.2))\n | none => none\n else if kind == 0x02 then\n (skipLimits rest restLen).map (fun p => (kind, none, p.1, p.2))\n else if kind == 0x03 then\n match skipImportValType rest restLen with\n | some (mutability, mutabilityLen) =>\n if mutabilityLen == 0 then none else\n let m := mutability &&& 0xff\n if m == 0 || m == 1 then\n some (kind, none, mutability >>> 8, mutabilityLen - 1)\n else none\n | none => none\n else if kind == 0x04 then\n if restLen == 0 || (rest &&& 0xff) != 0 then none else\n match readU (rest >>> 8) (restLen - 1) with\n | some (_, tail, tailLen) => some (kind, none, tail, tailLen)\n | none => none\n else none\n\ndef readImportEntry (n len : Nat) : Option (ImportEntry \u{d7} Nat \u{d7} Nat) :=\n match readName n len with\n | none => none\n | some (moduleName, n1, len1) =>\n match readName n1 len1 with\n | none => none\n | some (fieldName, n2, len2) =>\n match readImportDesc n2 len2 with\n | none => none\n | some (kind, typeIdx, n3, len3) =>\n some (\u{27e8}moduleName, fieldName, kind, typeIdx\u{27e9}, n3, len3)\n\ndef decRawImportVec : Nat \u{2192} Nat \u{2192} Nat \u{2192} Option (List ImportEntry \u{d7} Nat \u{d7} Nat)\n | 0, n, len => some ([], n, len)\n | k+1, n, len =>\n match readImportEntry n len with\n | none => none\n | some (entry, n1, len1) =>\n match decRawImportVec k n1 len1 with\n | none => none\n | some (rest, n2, len2) => some (entry :: rest, n2, len2)\n\n/-- Byte-exact import table. The declared vector must exhaust section 2. -/\ndef decodeRawImports (n len : Nat) : Option (List ImportEntry) :=\n match modulePayload 2 n len with\n | none => some []\n | some (iN, iLen) =>\n match readU iN iLen with\n | none => none\n | some (cnt, n1, len1) =>\n match decRawImportVec cnt n1 len1 with\n | some (entries, _, 0) => some entries\n | _ => none\n\ndef functionImports : List ImportEntry \u{2192} Option (List (String \u{d7} String))\n | [] => some []\n | entry :: rest =>\n if entry.kind == 0 && entry.funcTypeIdx.isSome then\n (functionImports rest).map\n (fun tail => (mkName entry.moduleName, mkName entry.fieldName) :: tail)\n else none\n\n/-- Imported function names. Any valid non-function import still declines this\n profile projection, preserving the original fail-closed contract. -/\ndef decodeImports (n len : Nat) : Option (List (String \u{d7} String)) :=\n (decodeRawImports n len).bind functionImports\n\n/-- Number of imported functions = the base offset for defined function indices. -/\ndef funcImportBase (n len : Nat) : Option Nat :=\n (decodeImports n len).map List.length\n\ndef readExportEntry (n len : Nat) : Option (ExportEntry \u{d7} Nat \u{d7} Nat) :=\n match readName n len with\n | none => none\n | some (name, n1, len1) =>\n if len1 == 0 then none else\n let kind := n1 &&& 0xff\n if kind > 4 then none else\n match readU (n1 >>> 8) (len1 - 1) with\n | none => none\n | some (idx, n2, len2) => some (\u{27e8}name, kind, idx\u{27e9}, n2, len2)\n\ndef decRawExportVec : Nat \u{2192} Nat \u{2192} Nat \u{2192} Option (List ExportEntry \u{d7} Nat \u{d7} Nat)\n | 0, n, len => some ([], n, len)\n | k+1, n, len =>\n match readExportEntry n len with\n | none => none\n | some (entry, n1, len1) =>\n match decRawExportVec k n1 len1 with\n | none => none\n | some (rest, n2, len2) => some (entry :: rest, n2, len2)\n\n/-- Byte-exact export table. The declared vector must exhaust section 7. -/\ndef decodeRawExports (n len : Nat) : Option (List ExportEntry) :=\n match modulePayload 7 n len with\n | none => none\n | some (eN, eLen) =>\n match readU eN eLen with\n | none => none\n | some (cnt, n1, len1) =>\n match decRawExportVec cnt n1 len1 with\n | some (entries, _, 0) => some entries\n | _ => none\n\ndef functionExports : List ExportEntry \u{2192} List (String \u{d7} Nat)\n | [] => []\n | entry :: rest =>\n if entry.kind == 0 then (mkName entry.name, entry.idx) :: functionExports rest\n else functionExports rest\n\n/-- Function-export compatibility projection of `decodeRawExports`. -/\ndef decodeExports (n len : Nat) : Option (List (String \u{d7} Nat)) :=\n (decodeRawExports n len).map functionExports\n\n/-- `some none` means section 8 is absent; a present section must contain one\n canonical u32 and no trailing bytes. -/\ndef decodeStart (n len : Nat) : Option (Option Nat) :=\n match modulePayload 8 n len with\n | none => some none\n | some (sN, sLen) =>\n match readU sN sLen with\n | some (idx, _, 0) => some (some idx)\n | _ => none\n\n/-- Read `k` (passive) data segments as byte lists. Non-passive flags are\n outside the profile \u{2192} reject (fail-closed). -/\ndef decDataVec : Nat \u{2192} Nat \u{2192} Nat \u{2192} Option (List (List Nat) \u{d7} Nat \u{d7} Nat)\n | 0, n, len => some ([], n, len)\n | k+1, n, len =>\n if len == 0 then none else\n let flag := n &&& 0xff\n let n1 := n >>> 8\n let len1 := len - 1\n if flag == 0x01 then\n match readU n1 len1 with -- byte count\n | none => none\n | some (bc, n2, len2) =>\n if bc \u{2264} len2 then\n let bytes := takeBytes bc n2\n let n3 := n2 >>> (8*bc)\n let len3 := len2 - bc\n match decDataVec k n3 len3 with\n | none => none\n | some (rest, n4, len4) => some (bytes :: rest, n4, len4)\n else none\n else none\n\n/-- Data segment payloads by segment index. Absent data section \u{2192} no segments. -/\ndef decodeData (n len : Nat) : Option (List (List Nat)) :=\n match modulePayload 11 n len with\n | none => some []\n | some (dN, dLen) =>\n match readU dN dLen with\n | none => none\n | some (cnt, n1, len1) =>\n match decDataVec cnt n1 len1 with\n | none => none\n | some (segs, _, 0) => some segs\n | some _ => none\n\n/- ===================================================================== -/\n/- Code section: locals, instructions, nested if/else -/\n/- ===================================================================== -/\n\n/-- Skip `g` local-declaration groups; return the total declared local count\n (handles wasm-gc ref valtypes 0x63/0x64 followed by a heaptype). -/\ndef decLocals : Nat \u{2192} Nat \u{2192} Nat \u{2192} Option (Nat \u{d7} Nat \u{d7} Nat)\n | 0, n, len => some (0, n, len)\n | g+1, n, len =>\n match readU n len with -- group count\n | none => none\n | some (c, n1, len1) =>\n if len1 == 0 then none else\n let t := n1 &&& 0xff\n let n2 := n1 >>> 8\n if t == 0x63 || t == 0x64 then\n match readS n2 (len1-1) with -- heaptype\n | none => none\n | some (_, n3, len3) =>\n match decLocals g n3 len3 with\n | none => none\n | some (m, n4, len4) => some (c + m, n4, len4)\n else\n match decLocals g n2 (len1-1) with\n | none => none\n | some (m, n4, len4) => some (c + m, n4, len4)\n\n/-- Consume an `if` blocktype (empty / numeric / ref+heaptype / typeidx s33). -/\ndef skipBlockType (n len : Nat) : Option (Nat \u{d7} Nat) :=\n if len == 0 then none else\n let b0 := n &&& 0xff\n if b0 == 0x40 then some (n >>> 8, len - 1)\n else if b0 == 0x7f || b0 == 0x7e || b0 == 0x7d || b0 == 0x7c || b0 == 0x7b then\n some (n >>> 8, len - 1)\n else if b0 == 0x63 || b0 == 0x64 then\n match readS (n >>> 8) (len - 1) with\n | none => none\n | some (_, n1, len1) => some (n1, len1)\n else\n match readS n len with -- typeidx s33 blocktype\n | none => none\n | some (_, n1, len1) => some (n1, len1)\n\n/-- Decode one non-structured instruction. `pending` holds i32 const values\n most-recent-first, so `array.new_data` resolves its (offset, length). -/\ndef decInstr (nfields : List Nat) (segs : List (List Nat)) (pending : List Int)\n (op n len : Nat) : Option (WInstr \u{d7} List Int \u{d7} Nat \u{d7} Nat) :=\n if op == 0x20 then (readU n len).map (fun p => (WInstr.localGet p.1, pending, p.2.1, p.2.2))\n else if op == 0x21 then (readU n len).map (fun p => (WInstr.localSet p.1, pending, p.2.1, p.2.2))\n else if op == 0x42 then (readS n len).map (fun p => (WInstr.i64Const p.1, pending, p.2.1, p.2.2))\n else if op == 0x41 then (readS n len).map (fun p => (WInstr.i32Const p.1, p.1 :: pending, p.2.1, p.2.2))\n else if op == 0x44 then\n if len < 8 then none\n else some (WInstr.f64Const (UInt64.ofNat (n &&& 0xffffffffffffffff)), pending, n >>> 64, len - 8)\n else if op == 0xd0 then (readS n len).map (fun p => (WInstr.refNull, pending, p.2.1, p.2.2))\n else if op == 0xd1 then some (WInstr.refIsNull, pending, n, len)\n else if op == 0x10 then (readU n len).map (fun p => (WInstr.call p.1, pending, p.2.1, p.2.2))\n else if op == 0x12 then (readU n len).map (fun p => (WInstr.returnCall p.1, pending, p.2.1, p.2.2))\n else if op == 0x0f then some (WInstr.ret, pending, n, len)\n -- integer / float scalar ops (single byte, no immediate)\n else if op == 0x50 then some (WInstr.i64Eqz, pending, n, len)\n else if op == 0x51 then some (WInstr.i64Eq, pending, n, len)\n else if op == 0x57 then some (WInstr.i64LeS, pending, n, len)\n else if op == 0x53 then some (WInstr.i64LtS, pending, n, len)\n else if op == 0x59 then some (WInstr.i64GeS, pending, n, len)\n else if op == 0x55 then some (WInstr.i64GtS, pending, n, len)\n else if op == 0x46 then some (WInstr.i32Eq, pending, n, len)\n else if op == 0x71 then some (WInstr.i32And, pending, n, len)\n else if op == 0x48 then some (WInstr.i32LtS, pending, n, len)\n else if op == 0x4c then some (WInstr.i32LeS, pending, n, len)\n else if op == 0x4a then some (WInstr.i32GtS, pending, n, len)\n else if op == 0xa0 then some (WInstr.f64Add, pending, n, len)\n else if op == 0xa1 then some (WInstr.f64Sub, pending, n, len)\n else if op == 0xa2 then some (WInstr.f64Mul, pending, n, len)\n else if op == 0xa3 then some (WInstr.f64Div, pending, n, len)\n else if op == 0x61 then some (WInstr.f64Eq, pending, n, len)\n else if op == 0x63 then some (WInstr.f64Lt, pending, n, len)\n else if op == 0x65 then some (WInstr.f64Le, pending, n, len)\n else if op == 0x66 then some (WInstr.f64Ge, pending, n, len)\n else if op == 0x64 then some (WInstr.f64Gt, pending, n, len)\n -- wasm-gc prefixed opcodes (0xfb sub)\n else if op == 0xfb then\n match readU n len with\n | none => none\n | some (sub, n1, len1) =>\n if sub == 0x00 then -- struct.new\n (readU n1 len1).map (fun q =>\n (WInstr.structNew q.1 ((nfields[q.1]?).getD 0), pending, q.2.1, q.2.2))\n else if sub == 0x02 then -- struct.get\n match readU n1 len1 with\n | none => none\n | some (ty, n2, len2) =>\n (readU n2 len2).map (fun f => (WInstr.structGet ty f.1, pending, f.2.1, f.2.2))\n else if sub == 0x08 then -- array.new_fixed\n match readU n1 len1 with\n | none => none\n | some (ty, n2, len2) =>\n (readU n2 len2).map (fun m => (WInstr.arrayNewFixed ty m.1, pending, m.2.1, m.2.2))\n else if sub == 0x09 then -- array.new_data\n match readU n1 len1 with\n | none => none\n | some (ty, n2, len2) =>\n match readU n2 len2 with\n | none => none\n | some (seg, n3, len3) =>\n let length := (pending.headD 0).toNat\n let offset := ((pending.drop 1).headD 0).toNat\n let payload := (segs[seg]?).getD []\n let chunk := (payload.drop offset).take length\n some (WInstr.arrayNewData ty chunk, pending, n3, len3)\n else if sub == 0x14 || sub == 0x15 then -- ref.test\n (readS n1 len1).map (fun h => (WInstr.refTest h.1.toNat, pending, h.2.1, h.2.2))\n else if sub == 0x16 || sub == 0x17 then -- ref.cast\n (readS n1 len1).map (fun h => (WInstr.refCast h.1.toNat, pending, h.2.1, h.2.2))\n else none\n else none\n\n/-- Decode a block of instructions. Returns the folded instructions, the\n threaded `pending` list, the new `(n, len)`, and a terminator tag\n (0 = `end` 0x0b, 1 = `else` 0x05), both consumed. Fuel bounds the number of\n instructions (body byte size is a safe bound). -/\ndef decBlock (nfields : List Nat) (segs : List (List Nat)) :\n Nat \u{2192} List Int \u{2192} Nat \u{2192} Nat \u{2192} Option (List WInstr \u{d7} List Int \u{d7} Nat \u{d7} Nat \u{d7} Nat)\n | 0, _, _, _ => none\n | fuel+1, pending, n, len =>\n if len == 0 then none else\n let op := n &&& 0xff\n let n1 := n >>> 8\n let len1 := len - 1\n if op == 0x0b then some ([], pending, n1, len1, 0)\n else if op == 0x05 then some ([], pending, n1, len1, 1)\n else if op == 0x04 then\n match skipBlockType n1 len1 with\n | none => none\n | some (n2, len2) =>\n match decBlock nfields segs fuel pending n2 len2 with\n | none => none\n | some (thenB, pend1, n3, len3, t1) =>\n if t1 == 1 then\n match decBlock nfields segs fuel pend1 n3 len3 with\n | none => none\n | some (elseB, pend2, n4, len4, t2) =>\n if t2 == 0 then\n match decBlock nfields segs fuel pend2 n4 len4 with\n | none => none\n | some (rest, pend3, n5, len5, t3) =>\n some (WInstr.ifElse thenB elseB :: rest, pend3, n5, len5, t3)\n else none\n else if t1 == 0 then\n match decBlock nfields segs fuel pend1 n3 len3 with\n | none => none\n | some (rest, pend3, n5, len5, t3) =>\n some (WInstr.ifElse thenB [] :: rest, pend3, n5, len5, t3)\n else none\n else\n match decInstr nfields segs pending op n1 len1 with\n | none => none\n | some (ins, pending\', n2, len2) =>\n match decBlock nfields segs fuel pending\' n2 len2 with\n | none => none\n | some (rest, pend3, n3, len3, t3) => some (ins :: rest, pend3, n3, len3, t3)\n\n/- ===================================================================== -/\n/- Per-function obligation decode -/\n/- ===================================================================== -/\n\nstructure CodeLoc where\n nlocals : Nat\n bodyN : Nat\n bodyLen : Nat\n /-- Exact raw code entry, including its size-LEB prefix. -/\n entryN : Nat\n entryLen : Nat\n\n/-- One bounded code-section pass. Every body is isolated from both the next\n code entry and the enclosing section, and its final list position is its\n defined-function index. -/\ndef decCodeLocs : Nat \u{2192} Nat \u{2192} Nat \u{2192} Option (List CodeLoc)\n | 0, _, len => if len == 0 then some [] else none\n | k+1, n, len =>\n match readU n len with\n | none => none\n | some (esz, bN, bLen) =>\n if esz \u{2264} bLen then\n let entryBodyN := isolateBytes bN esz\n let sizePrefixLen := len - bLen\n let wholeEntryLen := sizePrefixLen + esz\n let wholeEntryN := isolateBytes n wholeEntryLen\n match readU entryBodyN esz with\n | none => none\n | some (ng, gN, gLen) =>\n match decLocals ng gN gLen with\n | none => none\n | some (nloc, bodyN, bodyLen) =>\n match decCodeLocs k (bN >>> (8 * esz)) (bLen - esz) with\n | none => none\n | some rest =>\n some (\u{27e8}nloc, isolateBytes bodyN bodyLen, bodyLen,\n wholeEntryN, wholeEntryLen\u{27e9} :: rest)\n else none\n\ndef codeLocs (n len : Nat) : Option (Array CodeLoc) :=\n match modulePayload 10 n len with\n | none => none\n | some (codeN, codeLen) =>\n match readU codeN codeLen with\n | none => none\n | some (nf, r0, l0) => (decCodeLocs nf r0 l0).map List.toArray\n\n/-- Full `WCode` (arity from the type section, nlocals from the locals decl,\n body from the code section) for the module function `funcidx`. -/\ndef decodeCode (n len funcidx : Nat) : Option WCode :=\n match decodeTypes n len with\n | none => none\n | some ti =>\n match decodeData n len with\n | none => none\n | some segs =>\n match funcImportBase n len with\n | none => none\n | some nimp =>\n match decodeFuncTypes n len with\n | none => none\n | some ftys =>\n match ftys[funcidx - nimp]? with\n | none => none\n | some tyidx =>\n match ti.arityIndex[tyidx]? with\n | none => none\n | some ar =>\n match codeLocs n len with\n | none => none\n | some locs =>\n match locs[funcidx - nimp]? with\n | none => none\n | some loc =>\n match decBlock ti.nfields segs loc.bodyLen [] loc.bodyN loc.bodyLen with\n | none => none\n | some (instrs, _, _, restLen, term) =>\n if term == 0 && restLen == 0 then\n some \u{27e8}ar, loc.nlocals, instrs\u{27e9}\n else none\n\n/- ===================================================================== -/\n/- Plan-first add/mul/sub/box host-role table -/\n/- ===================================================================== -/\n\nnamespace AddSub\n\n/-- Per parameter/result: `some idx` for a concrete `(ref [null] idx)`, and\n `none` for scalar or abstract-heap value types. -/\nabbrev Sig := List (Option Nat) \u{d7} List (Option Nat)\n\n/-- Both concrete-reference tags retain their nonnegative heap type index;\n scalars, abstract shorthands, and negative abstract heaps project to none. -/\ndef valTarget : ValType \u{2192} Option Nat\n | .ref _ heap => if heap \u{2265} 0 then some heap.toNat else none\n | _ => none\n\ndef decodeTypeSig (entry : TypeEntry) : Option Sig :=\n match entry.composite with\n | .funcType params results => some (params.map valTarget, results.map valTarget)\n | _ => none\n\n/-- Function-signature and carrier projections of the canonical type parse. -/\ndef decodeTypeSigsC (n len : Nat) : Option (Array (Option Sig) \u{d7} Option Nat) :=\n (decodeTypes n len).map (fun info =>\n ((info.entries.map decodeTypeSig).toArray, info.carrier))\n\ndef isCarrierBinop (carrier : Nat) : Option Sig \u{2192} Bool\n | some (ptgts, rtgts) =>\n (ptgts == [some carrier, some carrier]) && (rtgts == [some carrier])\n | none => false\n\ninductive Arith | add | sub | mul\n deriving DecidableEq, Repr, BEq\n\n/-- Walk instruction boundaries linearly, skipping structured-control and\n other immediates without interpreting control flow. The first `i64.add`,\n `i64.sub`, or `i64.mul` determines the arithmetic marker. Unknown encodings\n fail closed. Numeric/comparison/conversion opcodes `0x45..0xc4` are all\n single-byte instructions. -/\ndef firstArithScan : Nat \u{2192} Nat \u{2192} Nat \u{2192} Option (Option Arith)\n | 0, _, _ => none\n | fuel+1, n, len =>\n if len == 0 then some none else\n let op := n &&& 0xff\n let n1 := n >>> 8\n let len1 := len - 1\n if op == 0x7c then some (some Arith.add)\n else if op == 0x7d then some (some Arith.sub)\n else if op == 0x7e then some (some Arith.mul)\n else if decide (0x45 \u{2264} op \u{2227} op \u{2264} 0xc4) then firstArithScan fuel n1 len1\n else if op == 0x0b || op == 0x05 || op == 0x0f || op == 0x00 || op == 0x01\n || op == 0x1a || op == 0x1b || op == 0xd1 then firstArithScan fuel n1 len1\n else if op == 0x20 || op == 0x21 || op == 0x22 || op == 0x23 || op == 0x24\n || op == 0x0c || op == 0x0d || op == 0x10 || op == 0x12 then\n match readU n1 len1 with\n | none => none\n | some (_, n2, len2) => firstArithScan fuel n2 len2\n else if op == 0x0e then\n match readU n1 len1 with\n | none => none\n | some (cnt, n2, len2) =>\n match skipUlebs (cnt+1) n2 len2 with\n | none => none\n | some (n3, len3) => firstArithScan fuel n3 len3\n else if op == 0x11 then\n match readU n1 len1 with\n | none => none\n | some (_, n2, len2) =>\n match readU n2 len2 with\n | none => none\n | some (_, n3, len3) => firstArithScan fuel n3 len3\n else if op == 0x02 || op == 0x03 || op == 0x04 then\n match skipBlockType n1 len1 with\n | none => none\n | some (n2, len2) => firstArithScan fuel n2 len2\n else if op == 0x41 || op == 0x42 then\n match readS n1 len1 with\n | none => none\n | some (_, n2, len2) => firstArithScan fuel n2 len2\n else if op == 0x43 then\n if len1 < 4 then none else firstArithScan fuel (n1 >>> 32) (len1 - 4)\n else if op == 0x44 then\n if len1 < 8 then none else firstArithScan fuel (n1 >>> 64) (len1 - 8)\n else if op == 0xd0 then\n match readS n1 len1 with\n | none => none\n | some (_, n2, len2) => firstArithScan fuel n2 len2\n else if op == 0xd2 then\n match readU n1 len1 with\n | none => none\n | some (_, n2, len2) => firstArithScan fuel n2 len2\n else if op == 0xfb then\n match readU n1 len1 with\n | none => none\n | some (sub, n2, len2) =>\n if sub == 0x00 || sub == 0x01 || sub == 0x06 || sub == 0x07\n || sub == 0x0b || sub == 0x0c || sub == 0x0d || sub == 0x0e then\n match readU n2 len2 with\n | none => none\n | some (_, n3, len3) => firstArithScan fuel n3 len3\n else if sub == 0x02 || sub == 0x05 || sub == 0x08 || sub == 0x09 then\n match readU n2 len2 with\n | none => none\n | some (_, n3, len3) =>\n match readU n3 len3 with\n | none => none\n | some (_, n4, len4) => firstArithScan fuel n4 len4\n else if sub == 0x0f then firstArithScan fuel n2 len2\n else if sub == 0x14 || sub == 0x15 || sub == 0x16 || sub == 0x17 then\n match readS n2 len2 with\n | none => none\n | some (_, n3, len3) => firstArithScan fuel n3 len3\n else none\n else none\n\ndef bodyLocs (n len : Nat) : Option (List (Nat \u{d7} Nat)) :=\n (CertDecode.codeLocs n len).map (fun locs =>\n locs.toList.map (fun loc => (loc.bodyN, loc.bodyLen)))\n\n/-- Scan defined functions in index order, retaining the first arithmetic\n marker only for functions with the exact carrier-binop signature. -/\ndef scanFns (carrier : Nat) (tsigs : Array (Option Sig)) (nimp : Nat) :\n Nat \u{2192} List Nat \u{2192} List (Nat \u{d7} Nat) \u{2192} Option (List (Nat \u{d7} Option Arith))\n | _, [], [] => some []\n | def_idx, ty :: rest, (bodyN, bodyByteLen) :: locs =>\n let sig := (tsigs[ty]?).getD none\n if isCarrierBinop carrier sig then\n match firstArithScan (bodyByteLen + 1) bodyN bodyByteLen with\n | none => none\n | some fa =>\n match scanFns carrier tsigs nimp (def_idx+1) rest locs with\n | none => none\n | some tl => some ((nimp + def_idx, fa) :: tl)\n else scanFns carrier tsigs nimp (def_idx+1) rest locs\n | _, _, _ => none\n\ndef candFor (a : Arith) (l : List (Nat \u{d7} Option Arith)) : List Nat :=\n (l.filter (fun p => p.2 == some a)).map Prod.fst\n\ndef uniqueC : List Nat \u{2192} Option Nat\n | [x] => some x\n | _ => none\n\ndef boxIdx (n len : Nat) : Option Nat :=\n match decodeExports n len with\n | none => none\n | some es => (es.find? (fun e => e.1 == \"__rt_aint_from_i64\")).map Prod.snd\n\nstructure Roles where\n box : Option Nat\n add : Option Nat\n mul : Option Nat\n sub : Option Nat\n deriving DecidableEq, Repr\n\n/-- Carrier-binop candidates from one type pass, one function-section pass,\n and one code-section pass. -/\ndef carrierBinopFns (n len : Nat) : Option (List (Nat \u{d7} Option Arith)) :=\n match decodeTypeSigsC n len, decodeFuncTypes n len,\n funcImportBase n len, bodyLocs n len with\n | some (tsigs, some carrier), some ftys, some nimp, some locs =>\n scanFns carrier tsigs nimp 0 ftys locs\n | _, _, _, _ => none\n\n/-- The module-wide plan-first host-role table. `add`, `mul`, and `sub` are admitted\n only for unique carrier-binop candidates; ambiguity or absence declines the\n individual role to `none`. `box` is the named runtime export. -/\ndef roleTable (n len : Nat) : Option Roles :=\n match carrierBinopFns n len with\n | none => none\n | some fns =>\n some { box := boxIdx n len\n , add := uniqueC (candFor Arith.add fns)\n , mul := uniqueC (candFor Arith.mul fns)\n , sub := uniqueC (candFor Arith.sub fns) }\n\nend AddSub\n\n/- ===================================================================== -/\n/- Byte-exact String.eq/String.concat host-role table -/\n/- ===================================================================== -/\n\nnamespace StringHost\n\n/-- F5-relevant value-type detail: i32, a concrete reference target, or a\n lumped kind that cannot satisfy either string-helper signature. -/\ninductive Ty\n | i32\n | scalar\n | ref (idx : Nat)\n | abstractHeap\n deriving DecidableEq, Repr, BEq\n\nabbrev Sig := List Ty \u{d7} List Ty\n\ndef projectVal : ValType \u{2192} Ty\n | .numeric tag => if tag == 0x7f then .i32 else .scalar\n | .ref _ heap => if heap \u{2265} 0 then .ref heap.toNat else .abstractHeap\n | .abstract _ => .abstractHeap\n\ndef decodeTypeSig (entry : TypeEntry) : Option Sig :=\n match entry.composite with\n | .funcType params results => some (params.map projectVal, results.map projectVal)\n | _ => none\n\n/-- Exactly the packed-i8 array shape used as String byte storage. As before,\n either validated field mutability projects to the same array index. -/\ndef stringBytesIndex (tidx : Nat) (entry : TypeEntry) : Option Nat :=\n match entry.composite with\n | .arrayType \u{27e8}.packed tag, _\u{27e9} => if tag == 0x78 then some tidx else none\n | _ => none\n\n@[inline] def consOpt (o : Option Nat) (l : List Nat) : List Nat :=\n match o with | some x => x :: l | none => l\n\ndef decodeTypeEntries : Nat \u{2192} List TypeEntry \u{2192} List (Option Sig) \u{d7} List Nat\n | _, [] => ([], [])\n | tidx, entry :: rest =>\n let decoded := decodeTypeEntries (tidx + 1) rest\n (decodeTypeSig entry :: decoded.1,\n consOpt (stringBytesIndex tidx entry) decoded.2)\n\n/-- Function signatures and string-byte-array indices from one type pass. -/\ndef decodeTypeSigs (n len : Nat) :\n Option (Array (Option Sig) \u{d7} List Nat) :=\n (CertDecode.decodeTypes n len).map (fun info =>\n let decoded := decodeTypeEntries 0 info.entries\n (decoded.1.toArray, decoded.2))\n\n/-- Exact admitted host-operation vocabulary. Non-mapped but boundary-known\n opcodes are `other`, making exact template comparison decline. -/\ninductive Op\n | localGet (i : Nat)\n | localSet (i : Nat)\n | i32Const (v : Int)\n | arrayLen\n | arrayGetU (t : Nat)\n | arrayGet (t : Nat)\n | arrayNewDefault (t : Nat)\n | arrayCopy (dst src : Nat)\n | i32Ne\n | i32GeU\n | i32Add\n | hIf\n | hBlock\n | hLoop\n | br (d : Nat)\n | brIf (d : Nat)\n | hReturn\n | hEnd\n | other\n deriving DecidableEq, Repr, BEq\n\n/-- Decode one instruction and skip every immediate exactly. Unknown encodings\n fail closed; known non-template instructions become `other`. -/\ndef decodeOne (n len : Nat) : Option (Op \u{d7} Nat \u{d7} Nat) :=\n let op := n &&& 0xff\n let n1 := n >>> 8\n let len1 := len - 1\n if op == 0x20 then\n (CertDecode.readU n1 len1).map (fun p => (Op.localGet p.1, p.2.1, p.2.2))\n else if op == 0x21 then\n (CertDecode.readU n1 len1).map (fun p => (Op.localSet p.1, p.2.1, p.2.2))\n else if op == 0x41 then\n (CertDecode.readS n1 len1).map (fun p => (Op.i32Const p.1, p.2.1, p.2.2))\n else if op == 0x47 then some (Op.i32Ne, n1, len1)\n else if op == 0x4f then some (Op.i32GeU, n1, len1)\n else if op == 0x6a then some (Op.i32Add, n1, len1)\n else if op == 0x02 then\n (CertDecode.skipBlockType n1 len1).map (fun p => (Op.hBlock, p.1, p.2))\n else if op == 0x03 then\n (CertDecode.skipBlockType n1 len1).map (fun p => (Op.hLoop, p.1, p.2))\n else if op == 0x04 then\n (CertDecode.skipBlockType n1 len1).map (fun p => (Op.hIf, p.1, p.2))\n else if op == 0x0c then\n (CertDecode.readU n1 len1).map (fun p => (Op.br p.1, p.2.1, p.2.2))\n else if op == 0x0d then\n (CertDecode.readU n1 len1).map (fun p => (Op.brIf p.1, p.2.1, p.2.2))\n else if op == 0x0f then some (Op.hReturn, n1, len1)\n else if op == 0x0b then some (Op.hEnd, n1, len1)\n else if op == 0x00 || op == 0x01 || op == 0x05 || op == 0x1a ||\n op == 0x1b || op == 0xd1 then some (Op.other, n1, len1)\n else if decide (0x45 \u{2264} op \u{2227} op \u{2264} 0xc4) then some (Op.other, n1, len1)\n else if op == 0x22 || op == 0x23 || op == 0x24 || op == 0x10 || op == 0x12 then\n (CertDecode.readU n1 len1).map (fun p => (Op.other, p.2.1, p.2.2))\n else if op == 0x0e then\n match CertDecode.readU n1 len1 with\n | none => none\n | some (cnt, n2, len2) =>\n (CertDecode.skipUlebs (cnt+1) n2 len2).map (fun p => (Op.other, p.1, p.2))\n else if op == 0x11 then\n match CertDecode.readU n1 len1 with\n | none => none\n | some (_, n2, len2) =>\n (CertDecode.readU n2 len2).map (fun p => (Op.other, p.2.1, p.2.2))\n else if op == 0x42 then\n (CertDecode.readS n1 len1).map (fun p => (Op.other, p.2.1, p.2.2))\n else if op == 0x43 then\n if len1 < 4 then none else some (Op.other, n1 >>> 32, len1 - 4)\n else if op == 0x44 then\n if len1 < 8 then none else some (Op.other, n1 >>> 64, len1 - 8)\n else if op == 0xd0 then\n (CertDecode.readS n1 len1).map (fun p => (Op.other, p.2.1, p.2.2))\n else if op == 0xd2 then\n (CertDecode.readU n1 len1).map (fun p => (Op.other, p.2.1, p.2.2))\n else if op == 0xfb then\n match CertDecode.readU n1 len1 with\n | none => none\n | some (sub, n2, len2) =>\n if sub == 0x0f then some (Op.arrayLen, n2, len2)\n else if sub == 0x0b then\n (CertDecode.readU n2 len2).map (fun p => (Op.arrayGet p.1, p.2.1, p.2.2))\n else if sub == 0x0d then\n (CertDecode.readU n2 len2).map (fun p => (Op.arrayGetU p.1, p.2.1, p.2.2))\n else if sub == 0x07 then\n (CertDecode.readU n2 len2).map\n (fun p => (Op.arrayNewDefault p.1, p.2.1, p.2.2))\n else if sub == 0x11 then\n match CertDecode.readU n2 len2 with\n | none => none\n | some (dst, n3, len3) =>\n (CertDecode.readU n3 len3).map\n (fun p => (Op.arrayCopy dst p.1, p.2.1, p.2.2))\n else if sub == 0x00 || sub == 0x01 || sub == 0x06 ||\n sub == 0x0c || sub == 0x0e then\n (CertDecode.readU n2 len2).map (fun p => (Op.other, p.2.1, p.2.2))\n else if sub == 0x02 || sub == 0x05 || sub == 0x08 || sub == 0x09 then\n match CertDecode.readU n2 len2 with\n | none => none\n | some (_, n3, len3) =>\n (CertDecode.readU n3 len3).map (fun p => (Op.other, p.2.1, p.2.2))\n else if sub == 0x14 || sub == 0x15 || sub == 0x16 || sub == 0x17 then\n (CertDecode.readS n2 len2).map (fun p => (Op.other, p.2.1, p.2.2))\n else none\n else none\n\ndef scan : Nat \u{2192} Nat \u{2192} Nat \u{2192} Option (List Op)\n | 0, _, _ => none\n | fuel+1, n, len =>\n if len == 0 then some [] else\n match decodeOne n len with\n | none => none\n | some (op, n1, len1) =>\n match scan fuel n1 len1 with\n | none => none\n | some rest => some (op :: rest)\n\ndef eqTemplate (t : Nat) : List Op :=\n [.localGet 0, .arrayLen, .localGet 1, .arrayLen, .i32Ne, .hIf,\n .i32Const 0, .hReturn, .hEnd, .localGet 0, .arrayLen, .localSet 2,\n .i32Const 0, .localSet 3, .hBlock, .hLoop, .localGet 3, .localGet 2,\n .i32GeU, .brIf 1, .localGet 0, .localGet 3, .arrayGetU t, .localGet 1,\n .localGet 3, .arrayGetU t, .i32Ne, .hIf, .i32Const 0, .hReturn, .hEnd,\n .localGet 3, .i32Const 1, .i32Add, .localSet 3, .br 0, .hEnd, .hEnd,\n .i32Const 1, .hEnd]\n\ndef concatTemplate (c b : Nat) : List Op :=\n [.localGet 0, .arrayLen, .localSet 3, .i32Const 0, .localSet 1,\n .i32Const 0, .localSet 2, .hBlock, .hLoop, .localGet 2, .localGet 3,\n .i32GeU, .brIf 1, .localGet 1, .localGet 0, .localGet 2, .arrayGet c,\n .arrayLen, .i32Add, .localSet 1, .localGet 2, .i32Const 1, .i32Add,\n .localSet 2, .br 0, .hEnd, .hEnd, .localGet 1, .arrayNewDefault b,\n .localSet 6, .i32Const 0, .localSet 7, .i32Const 0, .localSet 2,\n .hBlock, .hLoop, .localGet 2, .localGet 3, .i32GeU, .brIf 1,\n .localGet 0, .localGet 2, .arrayGet c, .localSet 4, .localGet 4,\n .arrayLen, .localSet 5, .localGet 6, .localGet 7, .localGet 4,\n .i32Const 0, .localGet 5, .arrayCopy b b, .localGet 7, .localGet 5,\n .i32Add, .localSet 7, .localGet 2, .i32Const 1, .i32Add, .localSet 2,\n .br 0, .hEnd, .hEnd, .localGet 6, .hEnd]\n\ninductive Role | eq | concat\n deriving DecidableEq, Repr, BEq\n\ndef eqCandidate : Option Sig \u{2192} Nat \u{2192} Option Nat\n | some (params, results), nloc =>\n match params, results with\n | [Ty.ref lhs, Ty.ref rhs], (Ty.i32 :: _) =>\n if lhs == rhs && nloc == 2 then some lhs else none\n | _, _ => none\n | none, _ => none\n\ndef concatCandidate : Option Sig \u{2192} Nat \u{2192} Option (Nat \u{d7} Nat)\n | some (params, results), nloc =>\n match params, results with\n | [Ty.ref c], (Ty.ref b :: _) =>\n if nloc == 7 then some (c, b) else none\n | _, _ => none\n | none, _ => none\n\ndef classifyOne (sbat : List Nat) (sig : Option Sig)\n (nloc bodyN bodyLen : Nat) : Option Role :=\n match eqCandidate sig nloc with\n | some lhs =>\n if sbat.contains lhs then\n match scan (bodyLen+1) bodyN bodyLen with\n | some ops => if ops == eqTemplate lhs then some Role.eq else none\n | none => none\n else none\n | none =>\n match concatCandidate sig nloc with\n | some (c, b) =>\n if sbat.contains b then\n match scan (bodyLen+1) bodyN bodyLen with\n | some ops => if ops == concatTemplate c b then some Role.concat else none\n | none => none\n else none\n | none => none\n\ndef bodyLocs (n len : Nat) : Option (List (Nat \u{d7} Nat \u{d7} Nat)) :=\n (CertDecode.codeLocs n len).map (fun locs =>\n locs.toList.map (fun loc => (loc.nlocals, loc.bodyN, loc.bodyLen)))\n\n/-- Classify each function independently. This intentionally has no uniqueness\n or cross-function decline: two exact eq helpers produce two entries. -/\ndef classify (nimp : Nat) (sbat : List Nat) (tsigs : Array (Option Sig)) :\n Nat \u{2192} List Nat \u{2192} List (Nat \u{d7} Nat \u{d7} Nat) \u{2192} List (Nat \u{d7} Role)\n | _, [], _ => []\n | _, _ :: _, [] => []\n | def_idx, ty :: tys, (nloc, bodyN, bodyLen) :: locs =>\n let sig := (tsigs[ty]?).getD none\n match classifyOne sbat sig nloc bodyN bodyLen with\n | some role =>\n (nimp + def_idx, role) :: classify nimp sbat tsigs (def_idx+1) tys locs\n | none => classify nimp sbat tsigs (def_idx+1) tys locs\n\n/-- Decode-once F5 result: every String.eq/String.concat `(funcIdx, role)` in\n defined-function order. -/\ndef roleTable (n len : Nat) : Option (List (Nat \u{d7} Role)) :=\n match decodeTypeSigs n len, CertDecode.decodeFuncTypes n len,\n CertDecode.funcImportBase n len, bodyLocs n len with\n | some (tsigs, sbat), some ftys, some nimp, some locs =>\n some (classify nimp sbat tsigs 0 ftys locs)\n | _, _, _, _ => none\n\nend StringHost\n\nend CertDecode\n";