Fix audited 0.25 correctness and security gaps with CKB-VM evidence

Close the swarm-audit findings on the Move-informed 0.25 surface:
stop dynamic Molecule-table field validation from clobbering live u128
limbs by routing wide binary operands through shared stack-spilled
loading, keep constant folding from wrapping arithmetic the runtime
traps on, decide match exhaustiveness with a bounded constructor
matrix that merges nested and or-pattern payload coverage, derive
Cell-backed value abilities structurally through struct/enum fields,
and register E2501 with the shared error registry.

Also enforce real package boundaries for public(package) visibility,
specialize generic templates in their owning module, bind typed
semantics v2 and lowering v3 to machine records checked by the
standalone checker, and tighten Registry SemVer admission.

Add the missing exact CKB-VM execution vectors for u128 bitwise,
addition, and shift over dynamic-schema fields (verified to fail on
the pre-fix code generator), plus the audit_poc reproduction corpus.

💘 Generated with Crush

Assisted-by: Crush:glm-5.2

Author: a19q3

BRANCHES.md

@@ -1,5 +1,15 @@
 # Branch Context
 
+## nightly-0.25
+
+`nightly-0.25` is the active language-completeness development line. It adds
+bounded value generics, explicit visibility and package interfaces, exhaustive
+IR-surface classification, and the typed-semantics v2 / lowering-record v3
+boundary. Treat it as merge-ready only when compiler, independent checker,
+Registry, editor/Playground, docs, and the `dev`, `ci`, and `backend` gates all
+agree. It is not a stable release or production CKB evidence claim; the crate
+version remains pinned until the coordinated release gate changes it.
+
 ## 0.12-era proposal baseline
 
 The 0.12-era work is the formal proposal baseline for grant-style acceptance

CHANGELOG.md

@@ -18,11 +18,21 @@
   reborrowing while preserving non-escape and lifecycle-crossing rejection.
   Add explicit public/package/private visibility, canonical package interfaces,
   six-dimensional interface compatibility with stable E2501 rejection,
-  Registry interface/hash admission, metadata schema 60 typed-semantics records,
-  lowering-record v2 and independent V2419/V2420 typed-to-machine checks. Add
+  Registry interface/hash admission, metadata schema 61 typed-semantics-v2 records,
+  lowering-record v3 and independent V2419/V2420 typed-to-machine checks. Generic
+  templates now specialize across package boundaries in their owning module;
+  implementation monomorphizations no longer pollute package interfaces. Add
   labeled break/continue CFG lowering and CKB-VM evidence. Upgrade the VS Code
   grammar and Playground highlighting, and show interface and typed-semantics
-  identities in the Playground Inspector.
+  identities in the Playground Inspector. Route all wide u128 binary operands
+  through shared stack-spilled loading so dynamic Molecule-table field
+  validation can no longer clobber live limbs, keep constant folding from
+  wrapping arithmetic the runtime would trap on, decide match exhaustiveness
+  with a bounded constructor-matrix computation that merges nested and
+  or-pattern payload coverage, derive Cell-backed value abilities structurally
+  through struct and enum fields, and register E2501 with the shared error
+  registry. Dynamic-schema u128 bitwise, addition, and shift paths now carry
+  exact CKB-VM execution vectors.
 
 - Ship the 0.24 package and Registry trust closure, informed by Sui Move's
   package-alt separation of resolution from compilation. Replace permissive

Cargo.toml

@@ -39,6 +39,7 @@ exclude = [
     ".idea/",
     ".playwright-mcp/",
     ".rustfmt.toml",
+    "audit_poc/",
     "rust-toolchain.toml",
     ".github/",
     "AGENTS.md",

audit_poc/Cell.toml

@@ -0,0 +1,4 @@
+[package]
+edition = "2026"
+name = "auditpoc"
+version = "0.1.0"

audit_poc/hidden_cell.cell

@@ -0,0 +1,22 @@
+// audit: hidden-cell laundering attempt via plain struct wrapper
+module audit::hidden_cell
+
+resource Token has store, create, consume, replace, burn {
+    amount: u128,
+}
+
+struct Wrapper has fixed, serializable {
+    token: Token,
+}
+
+struct Box<T: fixed + serializable + non_linear>
+    has fixed, serializable, non_linear
+{
+    value: T,
+}
+
+action verify() -> u64 {
+    verification
+        let boxed: Box<Wrapper> = Box<Wrapper> { value: Wrapper { token: ... } }
+        0
+}

audit_poc/nested_exhaustive.cell

@@ -0,0 +1,15 @@
+// audit: exhaustive nested-variant match should be accepted
+module audit::nested_patterns
+
+enum Inner { None, Some((u64, u64)) }
+enum Outer { Empty, Wrapped(Inner) }
+
+action verify() -> u64 {
+    verification
+        let outer: Outer = Outer::Wrapped(Inner::Some((20, 22)))
+        match outer {
+            Outer::Empty => { 0 }
+            Outer::Wrapped(Inner::None) => { 1 }
+            Outer::Wrapped(Inner::Some((left, right))) => { left + right }
+        }
+}

audit_poc/or_pattern_payload.cell

@@ -0,0 +1,14 @@
+// audit: payload or-pattern covering all variants should be accepted
+module audit::or_pattern
+
+enum Inner { None, Some((u64, u64)) }
+enum Outer { Empty, Wrapped(Inner) }
+
+action verify() -> u64 {
+    verification
+        let outer: Outer = Outer::Wrapped(Inner::None)
+        match outer {
+            Outer::Empty => { 0 }
+            Outer::Wrapped(Inner::None | Inner::Some(_)) => { 1 }
+        }
+}

audit_poc/src/main.cell

@@ -0,0 +1,14 @@
+// dynamic-layout struct forces Molecule-table field decoding for u128 limbs
+module audit::dyn_struct_u128
+
+struct Entry {
+    amount: u128,
+    note: Vec<u8>,
+}
+
+action verify(e1: Entry, e2: Entry) -> u64 {
+    verification
+        let masked: u128 = e1.amount & e2.amount
+        let shifted: u128 = e1.amount << 3
+        0
+}

crates/cellscript-artifact-checker/src/checker.rs

@@ -1,11 +1,12 @@
 use serde::{Deserialize, Serialize};
 
-pub const LOWERING_RECORD_SCHEMA: &str = "cellscript-verified-lowering-record-v2";
-pub const TYPED_SEMANTICS_SCHEMA: &str = "cellscript-typed-semantics-v1";
+pub const LOWERING_RECORD_SCHEMA: &str = "cellscript-verified-lowering-record-v3";
+pub const TYPED_SEMANTICS_SCHEMA: &str = "cellscript-typed-semantics-v2";
 pub const SOURCE_MAP_SCHEMA: &str = "cellscript-source-artifact-map-v1";
 pub const CHECKER_POLICY_SCHEMA: &str = "cellscript-artifact-checker-policy-v1";
 pub const CHECKER_REPORT_SCHEMA: &str = "cellscript-artifact-checker-report-v1";
-pub const LOWERING_RECORD_VERSION: u32 = 2;
+pub const LOWERING_RECORD_VERSION: u32 = 3;
+pub const TYPED_SEMANTICS_VERSION: u32 = 2;
 pub const SOURCE_MAP_VERSION: u32 = 1;
 pub const CHECKER_VERSION: &str = env!("CARGO_PKG_VERSION");
 
@@ -68,6 +69,11 @@ impl VerifiedLoweringRecord {
             entry.proof_ids.dedup();
             entry.capabilities.sort();
             entry.capabilities.dedup();
+            entry.typed_blocks.sort_by_key(|block| block.id);
+            for block in &mut entry.typed_blocks {
+                block.machine_block_ids.sort();
+                block.machine_block_ids.dedup();
+            }
         }
         self.blocks.sort_by(|a, b| a.id.cmp(&b.id));
         for block in &mut self.blocks {
@@ -104,6 +110,10 @@ impl TypedSemanticRecord {
         self.types.sort_by(|left, right| left.name.cmp(&right.name));
         for ty in &mut self.types {
             ty.fields.sort_by(|left, right| left.offset.cmp(&right.offset).then(left.name.cmp(&right.name)));
+            ty.variants.sort_by(|left, right| left.tag.cmp(&right.tag).then(left.name.cmp(&right.name)));
+            for variant in &mut ty.variants {
+                variant.fields.sort_by_key(|field| field.index);
+            }
             ty.capabilities.sort();
             ty.capabilities.dedup();
         }
@@ -133,7 +143,10 @@ pub struct TypedSemanticType {
     pub kind: String,
     pub encoded_size: Option<u32>,
     pub fields: Vec<TypedSemanticField>,
+    pub tag_width_bytes: Option<u32>,
+    pub variants: Vec<TypedSemanticVariant>,
     pub capabilities: Vec<String>,
+    pub identity_policy: String,
     pub layout_hash: String,
 }
 
@@ -146,6 +159,25 @@ pub struct TypedSemanticField {
     pub width_bytes: Option<u32>,
 }
 
+#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(deny_unknown_fields)]
+pub struct TypedSemanticVariant {
+    pub name: String,
+    pub tag: u32,
+    pub payload_width_bytes: u32,
+    pub fields: Vec<TypedSemanticVariantField>,
+}
+
+#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(deny_unknown_fields)]
+pub struct TypedSemanticVariantField {
+    pub index: u32,
+    pub ty: String,
+    pub offset: u32,
+    pub width_bytes: u32,
+    pub linear: bool,
+}
+
 #[derive(Debug, Clone, Default, PartialEq, Eq, Serialize, Deserialize)]
 #[serde(deny_unknown_fields)]
 pub struct TypedSemanticEntry {
@@ -155,6 +187,7 @@ pub struct TypedSemanticEntry {
     pub params: Vec<TypedSemanticParam>,
     pub return_type: String,
     pub effect: String,
+    pub entry_block: u32,
     pub locals: Vec<TypedSemanticLocal>,
     pub blocks: Vec<TypedSemanticBlock>,
     pub borrows: Vec<TypedSemanticBorrow>,
@@ -178,6 +211,7 @@ pub struct TypedSemanticParam {
 #[serde(deny_unknown_fields)]
 pub struct TypedSemanticLocal {
     pub id: u32,
+    pub source_id: u64,
     pub name: String,
     pub ty: String,
 }
@@ -189,14 +223,24 @@ pub struct TypedSemanticBlock {
     pub operations: Vec<TypedSemanticOperation>,
     pub successors: Vec<u32>,
     pub terminator: String,
+    pub runtime_error: Option<TypedSemanticRuntimeError>,
+}
+
+#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(deny_unknown_fields)]
+pub struct TypedSemanticRuntimeError {
+    pub code: u64,
+    pub name: String,
 }
 
 #[derive(Debug, Clone, Default, PartialEq, Eq, Serialize, Deserialize)]
 #[serde(deny_unknown_fields)]
 pub struct TypedSemanticOperation {
+    pub index: u32,
     pub opcode: String,
     pub destinations: Vec<u32>,
     pub operands: Vec<TypedSemanticOperand>,
+    pub detail: TypedSemanticOperationDetail,
     pub call: Option<TypedSemanticCall>,
 }
 
@@ -205,6 +249,90 @@ pub struct TypedSemanticOperation {
 pub struct TypedSemanticOperand {
     pub local: Option<u32>,
     pub ty: String,
+    pub constant: Option<TypedSemanticConstant>,
+}
+
+#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(tag = "kind", rename_all = "kebab-case", deny_unknown_fields)]
+pub enum TypedSemanticOperationDetail {
+    #[default]
+    None,
+    Constant {
+        value: TypedSemanticConstant,
+    },
+    Binding {
+        name: String,
+    },
+    BinaryOperator {
+        operator: String,
+    },
+    UnaryOperator {
+        operator: String,
+    },
+    Field {
+        name: String,
+    },
+    Collection {
+        declared_type: String,
+    },
+    Reference {
+        declared_type: String,
+    },
+    EnumConstruct {
+        enum_name: String,
+        variant: String,
+    },
+    EnumTag {
+        enum_name: String,
+    },
+    EnumPayload {
+        enum_name: String,
+        variant: String,
+        field_index: u32,
+    },
+    Create {
+        pattern: TypedSemanticCreatePattern,
+    },
+    Destroy {
+        policy: String,
+    },
+    CreateUnique {
+        pattern: TypedSemanticCreatePattern,
+        identity: String,
+    },
+    ReplaceUnique {
+        pattern: TypedSemanticCreatePattern,
+        identity: String,
+    },
+    CellMetadata {
+        field: String,
+    },
+}
+
+#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(deny_unknown_fields)]
+pub struct TypedSemanticCreatePattern {
+    pub operation: String,
+    pub ty: String,
+    pub binding: String,
+    pub field_names: Vec<String>,
+    pub has_lock: bool,
+    pub identity: String,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(tag = "kind", content = "value", rename_all = "kebab-case", deny_unknown_fields)]
+pub enum TypedSemanticConstant {
+    Unit,
+    U8(String),
+    U16(String),
+    U32(String),
+    U64(String),
+    U128(String),
+    Bool(bool),
+    Address(String),
+    Hash(String),
+    Array(Vec<TypedSemanticConstant>),
 }
 
 #[derive(Debug, Clone, Default, PartialEq, Eq, Serialize, Deserialize)]
@@ -225,6 +353,10 @@ pub struct TypedSemanticBorrow {
     pub binding: String,
     pub root_type: String,
     pub view_type: String,
+    pub start_block: u32,
+    pub start_operation: u32,
+    pub end_block: Option<u32>,
+    pub end_operation: Option<u32>,
     pub escapes: bool,
 }
 
@@ -242,10 +374,16 @@ pub struct TypedSemanticOwnership {
 #[serde(deny_unknown_fields)]
 pub struct TypedSemanticInstantiation {
     pub kind: String,
+    pub module: String,
     pub template: String,
+    pub concrete_name: String,
     pub identity: String,
     pub type_arguments: Vec<String>,
+    pub value_ability_registry_version: u32,
     pub constraints_verified: bool,
+    pub fixed_layout_required: bool,
+    pub cell_backed_layout_rejected: bool,
+    pub identity_includes_phantom_arguments: bool,
 }
 
 #[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
@@ -262,6 +400,15 @@ pub struct LoweringEntry {
     pub proof_ids: Vec<String>,
     pub frame_size_bytes: u32,
     pub outgoing_argument_bytes: u32,
+    pub typed_blocks: Vec<TypedBlockBinding>,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(deny_unknown_fields)]
+pub struct TypedBlockBinding {
+    pub id: u32,
+    pub hash: String,
+    pub machine_block_ids: Vec<String>,
 }
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
@@ -302,6 +449,7 @@ pub struct LoweringBlock {
     pub owner_entry: String,
     pub reachable: bool,
     pub lowering_block_id: Option<u32>,
+    pub typed_block_hash: Option<String>,
     pub machine_label: Option<String>,
     pub terminator: MachineTerminator,
     pub range: MachineRange,