Harden bounded lifecycle collection lowering

Author: a19q3

CHANGELOG.md

@@ -2,6 +2,20 @@
 
 ## Unreleased
 
+- Harden bounded lifecycle collections at the production boundary. The typed
+  IR now retains `consume_each` predicates and the `create_each` output
+  template and lowers both constructs to an explicit registered fail-closed
+  call instead of silently replacing the body with `Unit`. Non-production
+  CKB artifacts reject the entry with stable runtime error 24
+  (`collection-runtime-unsupported`); `--production` and
+  `--deny-fail-closed` stop before ASM/ELF generation with E2105 and report the
+  operation, source origin, missing ProofPlan enforcement, and remediation.
+  Entry ABI metadata no longer presents either bounded collection as a
+  supported schema pointer, and ProofPlan no longer fabricates a
+  runtime-observed cardinality. Runtime Cell selection/decoding and witness
+  plan/output correspondence remain deliberately unsupported until their
+  consensus semantics are specified.
+
 - Bound local compiler and gate storage without weakening the verified-artifact
   contract. Incremental build caches now retain at most 32 recent identities
   per cache root, syntax-combination success runs discard reproducible

docs/CELLSCRIPT_COLLECTIONS_SUPPORT_MATRIX.md

@@ -20,7 +20,9 @@ not be collapsed into one generic "collections are supported" claim.
 | `HashMap<u64, u64>` | Limited | Limited | No production helper surface | Unsupported/fail-closed for production contracts |
 | `HashMap<Hash, Token>` | No | No | No | Unsupported; must fail closed |
 | `HashSet<T>` | Limited | Limited | No production helper surface | Unsupported/fail-closed for production contracts |
-| Cell-backed resource collections | No executable ownership model | No | No | Unsupported until a linear collection ownership primitive exists |
+| `BoundedCellSet<Resource, N>` + `consume_each` | Frontend and metadata only | Explicit fail-closed IR; checked predicates retained | No source scan/decoder | Production-rejected with E2105; non-production artifacts return error 24 |
+| `BoundedList<Plan, N>` + `create_each` | Frontend and metadata only | Explicit fail-closed IR; predicates and create template retained | No witness codec/output verifier | Production-rejected with E2105; non-production artifacts return error 24 |
+| Generic Cell-backed resource collections | No executable ownership model | No | No | Unsupported |
 
 ## Stack-Backed Local Vec Rule
 
@@ -67,15 +69,36 @@ shape. They must produce one of:
 - structured blocker in metadata/constraints
 - explicit fail-closed runtime path with a registered runtime error
 
+Every selected consensus-relevant ProofPlan status beginning with `gap:` is a
+production blocker, including `gap:runtime-helper-required`,
+`gap:builder-evidence-required`, and `gap:metadata-only`. A transaction builder
+can supply evidence for construction, but that evidence cannot authorize a
+consensus operation the emitted Script does not check.
+
+## Bounded Lifecycle Boundary
+
+The bound `N` is currently a static type and complexity declaration. It is not
+evidence that a runtime scan observed at most `N` items. Metadata therefore
+records the maximum but leaves actual cardinality unobserved.
+
+Positive `consume_each` execution needs a specified transaction versus
+script-group source, a resource Type Script identity, canonical cell-data
+decoding, actual-count enforcement, and per-element predicate plus consumption
+semantics. Positive `create_each` execution additionally needs a canonical
+witness list codec, output ordering and one-to-one plan/output correspondence,
+fresh Cell identity, and occupied-capacity rules. Until those contracts exist,
+use explicit fixed-arity input/output bindings and ordinary lowered
+`require`/`consume`/`create` operations.
+
 ## Authoring Guidance
 
 Use dynamic vectors for data that is still a single cell field, such as signer
 lists, proposal payload bytes, NFT attributes, or launch distributions.
 
-Do not model ownership of multiple independent linear cells as a generic vector
-or map. Use explicit action parameters, named output bindings, and explicit
-`consume`/`destroy` operations or compiler-recognized stdlib lifecycle patterns
-until the language gains a verifier-backed collection ownership primitive.
+Do not deploy ownership of multiple independent linear cells through a generic
+vector, map, `BoundedCellSet`, or `BoundedList`. Use explicit fixed-arity action
+parameters, named output bindings, and lowered `consume`/`destroy`/`create`
+operations until the bounded runtime contract is implemented.
 
 The missing verifier pieces are explicit cell consumption, typed collection
 destructuring, and membership proofs tied to Molecule schema manifests. Until

docs/CELLSCRIPT_GATE_POLICY.md

@@ -340,17 +340,29 @@ quantifiers. It has a compile-time `1..=64` bound, emits a real resolved
 positive/missing-dependency CKB-VM cases. Out point, dep type, and original
 DepGroup identity remain manifest/builder evidence.
 
-Bounded Cell collections use the same finite-evidence rule. An action may take
-`input cells: BoundedCellSet<T, N>` and discharge its linear ownership exactly
-once with `consume_each`. A fixed-width witness plan may use
-`witness plans: BoundedList<P, N>` and exactly one `create` template per plan
-element through `create_each`. `runtime.collection_instantiations` records the
-explicit source, maximum cardinality, runtime-cardinality placeholder, vacuous
-zero policy, and ownership. Consume iteration remains
-`runtime-helper-required`; create iteration additionally emits
-`builder-evidence-required` output-count and capacity obligations. The quick
-syntax gate covers missing bounds, duplicate consumption, and
-`Vec<Resource>` rejection.
+Bounded Cell collections use the same finite-evidence rule, but are not yet an
+executable production surface. The ownership checker accepts
+`input cells: BoundedCellSet<T, N>` only when its binding is statically
+discharged once by `consume_each`. A fixed-width witness plan may describe
+`witness plans: BoundedList<P, N>` with exactly one `create` template per plan
+element. `runtime.collection_instantiations` records the declared source,
+maximum cardinality, vacuous-zero possibility, and ownership; it does not
+claim an actual runtime count. ProofPlan records
+`actual_scanned_cardinality:not-observed-no-runtime-lowering`.
+
+The IR retains the checked predicates and create template, then emits a
+registered fail-closed operation. Non-production CKB artifacts return runtime
+error 24 (`collection-runtime-unsupported`). `--production` and
+`--deny-fail-closed` reject both operations before ASM/ELF generation with
+E2105. The diagnostic names the operation, source origin, missing enforcement,
+and remediation. The quick syntax gate continues to cover missing bounds,
+duplicate static consumption, and `Vec<Resource>` rejection; CKB-VM coverage
+pins the exact-negative runtime boundary.
+
+More generally, production treats every selected consensus-relevant ProofPlan
+`gap:*` status as a hard blocker. This includes runtime-helper, builder-evidence,
+and metadata-only gaps. Builder output/capacity evidence is construction data,
+not a substitute for a verifier check.
 
 Type validity uses one evidence contract across parser, type checking, IR,
 metadata, ProofPlan, codegen, formatter, and LSP. A pure field predicate is

docs/CELLSCRIPT_LINEAR_OWNERSHIP.md

@@ -51,9 +51,11 @@ would require a verifier-backed membership and consumption model. Until that
 model exists, such cases must remain compile-time rejected or represented as
 structured runtime blockers.
 
-Missing verifier pieces:
+Missing executable verifier pieces:
 
-- `consume_each`
+- runtime source selection, decoding, and per-element enforcement for
+  `consume_each`
+- canonical witness/output correspondence for `create_each`
 - typed collection destructuring
 - verifier-backed membership proofs
 - schema-level ownership witnesses

docs/examples/collections_matrix.md

@@ -14,8 +14,10 @@ Recommended authoring rule:
 - treat nested dynamic containers as schema/ABI boundary shapes unless
   metadata, constraints, and verifier evidence prove a concrete production
   helper
-- model Cell-backed collections with a source-aware `BoundedCellSet<T, N>`;
-  `Vec<Cell>` is rejected because it hides transaction source and ownership
+- use explicit fixed-arity Cell parameters and lifecycle operations for
+  deployable ownership; a source-aware `BoundedCellSet<T, N>` is currently an
+  audit-only contract and production-rejected, while `Vec<Cell>` is rejected
+  because it hides transaction source and ownership
 
 Current stack-backed local `Vec<T>` support is deliberately bounded compiler
 lowering for verifier-local fixed-width values. It is not a production

docs/generated/CELLSCRIPT_EXECUTABLE_SURFACE_MATRIX.md

@@ -76,3 +76,5 @@ Production compilation means `--production` or `--deny-fail-closed`; both stop b
 | `ir:cell-metadata-equality` | instruction | complete | accepted | Lock-hash or capacity equality over validated Cell views. | `none` |
 | `artifact:create-output-verification` | artifact-policy | shape-gated | accepted only when the shape classifier reports no fail-closed feature | All constructed output fields and output lock must be materializable by the verifier. | `output-verification-incomplete, output-lock-verification-incomplete` |
 | `artifact:cell-backed-collection-return` | artifact-policy | reserved | rejected by production policy | Returning a hidden Cell-backed collection has no linear ownership ABI. | `cell-backed-collection-return` |
+| `artifact:bounded-consume-each-runtime` | artifact-policy | reserved | rejected by production policy | BoundedCellSet source selection, element decoding, and per-element predicate execution are not yet an executable contract. | `bounded-consume-each-runtime` |
+| `artifact:bounded-create-each-runtime` | artifact-policy | reserved | rejected by production policy | BoundedList witness codec, output correspondence, ordering, identity, and capacity enforcement are not yet an executable contract. | `bounded-create-each-runtime` |

docs/generated/cellscript-executable-surface.json

@@ -611,6 +611,26 @@
       "layer": "artifact-policy",
       "production_policy": "rejected by production policy",
       "status": "reserved"
+    },
+    {
+      "conditions": "BoundedCellSet source selection, element decoding, and per-element predicate execution are not yet an executable contract.",
+      "fail_closed_features": [
+        "bounded-consume-each-runtime"
+      ],
+      "id": "artifact:bounded-consume-each-runtime",
+      "layer": "artifact-policy",
+      "production_policy": "rejected by production policy",
+      "status": "reserved"
+    },
+    {
+      "conditions": "BoundedList witness codec, output correspondence, ordering, identity, and capacity enforcement are not yet an executable contract.",
+      "fail_closed_features": [
+        "bounded-create-each-runtime"
+      ],
+      "id": "artifact:bounded-create-each-runtime",
+      "layer": "artifact-policy",
+      "production_policy": "rejected by production policy",
+      "status": "reserved"
     }
   ],
   "schema": "cellscript-executable-surface-v1"

docs/releases/CELLSCRIPT_0_25_RELEASE_NOTES.md

@@ -74,6 +74,31 @@ remain defense in depth rather than a public feature boundary. An unregistered
 IR variant fails compilation, and an unregistered runtime feature fails closed
 under every policy.
 
+## Bounded Lifecycle Collections Fail Closed
+
+An audit of `consume_each` and `create_each` found a serious lowering gap: the
+frontend and ownership checker accepted the bounded body, but IR replaced it
+with `Unit`. A body containing `require false` could therefore compile to an
+action that returned success without scanning, consuming, checking, or
+creating anything.
+
+0.25 removes that path. The typed IR retains the predicates and create
+template and contains an explicit fail-closed call. Metadata reports
+`actual_scanned_cardinality:not-observed-no-runtime-lowering`; it does not
+claim that a helper ran. The entry ABI marks `BoundedCellSet<T, N>` and
+`BoundedList<P, N>` unsupported. A non-production artifact returns stable
+runtime error 24 (`collection-runtime-unsupported`) in CKB-VM, while
+`--production` and `--deny-fail-closed` return E2105 before writing ASM or ELF.
+The diagnostic includes the operation, source origin, missing ProofPlan tier,
+and a concrete remediation.
+
+This is a safety boundary, not positive runtime support. The language still
+needs a canonical transaction/group selection rule and Type Script identity
+for `BoundedCellSet`, plus a witness element codec, output order and
+one-to-one correspondence, fresh identity, and capacity rules for
+`BoundedList`/`create_each`. Builder evidence is not accepted as a replacement
+for those on-chain checks.
+
 ## Validation Before Release
 
 The implementation is not release-complete until the generated surface and

docs/wiki/Tutorial-03-Resources-and-Cell-Effects.md

@@ -66,10 +66,11 @@ validated as a named successor output, or handled by an explicit stdlib
 lifecycle pattern. Silent loss is rejected because silent loss would make Cell
 movement unclear.
 
-## Finite Batch Movement In 0.22
+## Finite Batch Contracts (Metadata-Only Boundary)
 
-Use source-aware bounded collections when one action must account for a finite
-set of Cells or witness plans:
+Source-aware bounded collections can describe how one action intends to account
+for a finite set of Cells or witness plans. In the current CKB executable
+profile, the following is auditable metadata, not deployable code:
 
 ```cellscript
 action batch(
@@ -90,16 +91,20 @@ action batch(
 }
 ```
 
-`BoundedCellSet<T, N>` is input-qualified and linearly owned: every selected
-Cell must be discharged by `consume_each`. `BoundedList<T, N>` is fixed-width
-and may come from witness/static input; `create_each` records a maximum output
-cardinality and capacity-builder obligation. The bound makes review and
-ProofPlan complexity finite. It does not prove that a builder supplied the
-outputs or enough capacity.
+`BoundedCellSet<T, N>` is input-qualified and statically linearly owned: the
+binding must be discharged by one `consume_each`. `BoundedList<T, N>` is
+fixed-width; `create_each` records a maximum output cardinality and
+capacity-builder obligation. The bound makes review and ProofPlan complexity
+finite. It does not prove a runtime count, a Cell selection, or that a builder
+supplied matching outputs and enough capacity.
 
 Generic `Vec<Resource>` and unbounded iteration remain rejected. Inspect
-`runtime.collection_instantiations` and the matching ProofPlan records before
-treating a batch path as executable.
+`runtime.collection_instantiations` and the matching ProofPlan records for
+audit, but do not treat the batch path as executable. Production returns E2105
+before codegen; non-production CKB artifacts return runtime error 24. Use
+explicit fixed-arity Cell inputs/outputs and ordinary lifecycle operations for
+deployable code until source selection, codecs, correspondence, identity, and
+capacity rules are implemented.
 
 ## Borrowed Read Views
 

docs/wiki/Tutorial-06-Metadata-Verification-and-Production-Gates.md

@@ -218,11 +218,21 @@ contract, not proof that the selected artifact emitted or executed that helper.
 `runtime.collection_instantiations` also distinguishes local stack collections
 from source-aware bounded Cell collections. For `BoundedCellSet<T, N>`, verify
 `source = input`, `ownership = linear-cell-set`, the finite `max_elements`, and
-the `consume_each` runtime-helper tier. For `BoundedList<P, N>` driving
+the `consume_each` runtime-helper gap. For `BoundedList<P, N>` driving
 `create_each`, verify `source = witness`, `output_cardinality_max = N`, and
 `capacity_builder_evidence_required = true`. Its ProofPlan evidence is
 `builder-evidence-required`; it is not proof that a transaction builder supplied
-the matching outputs or sufficient capacity.
+the matching outputs or sufficient capacity. Actual cardinality must read
+`not-observed-no-runtime-lowering`, not `runtime-recorded`.
+
+Neither form is deployable in the current CKB profile. The IR retains the
+checked body for audit and emits a fail-closed operation; CKB-VM returns runtime
+error 24. Production compilation stops at E2105 before codegen. Treat any
+selected consensus ProofPlan whose `codegen_coverage_status` begins with
+`gap:` as a blocker, including runtime-helper, builder-evidence, and
+metadata-only records. Until the source/codec/correspondence contract is
+implemented, write explicit fixed-arity inputs, outputs, predicates, and
+lifecycle operations instead.
 
 The validity record first appeared in schema 55 during the 0.22 line and is
 retained by current metadata schema 61 as `types[].validity_predicates`. Review each predicate's