Skip to content

[Candidate][Consensus runtime] Implement executable bounded output-plan correspondence #8

Closed

Description

@a19q3

Summary

Implement the positive runtime semantics for BoundedList<P, N>::create_each.

The compiler already retains the plan predicate and create template, but production builds correctly reject the operation because there is no canonical witness codec or on-chain proof that every plan corresponds to exactly one output Cell in the required order, with the required identity, Script, data, lock, and capacity.

This issue depends on the selection and decoding foundations in #7, but it remains separate because output authorization and one-to-one correspondence have a larger attack surface than bounded input consumption.

Portfolio status

This is a candidate consensus-runtime workstream, not an authorized 0.26 or P0 implementation commitment. Until the post-0.25 evidence review accepts concrete use cases, an accountable owner, an independent reviewer, capacity, and stop conditions, only Phase 0 specification and use-case discovery are authorized. The issue priority describes semantic risk, not a promised release slot.

Security statement

A transaction builder may construct a plausible transaction, but builder behavior is not a consensus boundary. The emitted CKB Script must independently prove:

plan count == selected output count <= N
and
for every i: plan[i] authorizes exactly selected_output[i]

Missing, extra, duplicated, or reordered outputs must fail on chain.

flowchart LR
    W["WitnessArgs.input_type"] --> CODEC["Decode versioned PlanList<P>"]
    CODEC --> PC["plan_count"]
    GO["Canonical group-relative outputs"] --> OC["output_count"]
    PC --> EQ{"plan_count == output_count <= N?"}
    OC --> EQ
    EQ -- "no" --> REJECT["Stable correspondence error"]
    EQ -- "yes" --> ZIP["Zip plan[i] with output[i]"]
    ZIP --> SCRIPT["Verify Type/Lock Script policy"]
    SCRIPT --> DATA["Verify canonical output data"]
    DATA --> CAP["Verify occupied capacity floor"]
    CAP --> ID["Verify fresh/preserved identity policy"]
    ID --> ACCEPT["Every pair covered exactly once"]
Loading

Required semantic contract

The first supported shape should require:

  • a versioned canonical Molecule list in WitnessArgs.input_type;
  • a compile-time maximum N and runtime count enforcement;
  • canonical Type Script group-relative output ordering;
  • exact one-to-one plan/output correspondence;
  • one evaluation of each plan predicate and one materialization of each output template;
  • explicit Type Script, Lock Script, data schema, and capacity policies;
  • an explicit identity rule for every created resource;
  • stable failures for omission, duplication, reordering, malformed plans, and under-capacity outputs;
  • builder evidence that mirrors—but never replaces—the checks performed by the Script.

The accepted RFC must decide whether the initial version permits zero plans. It must not infer freshness or authority from action/function names.

Correspondence model

sequenceDiagram
    participant B as Transaction builder
    participant W as Witness PlanList
    participant T as Candidate outputs
    participant V as CellScript verifier
    B->>W: encode versioned plans
    B->>T: construct candidate outputs
    V->>W: decode and bound count
    V->>T: select canonical group outputs
    loop each index i
        V->>V: validate plan[i] against output[i]
    end
    V-->>B: accept only if all pairs and counts match
Loading

The builder and verifier must use the same ordering specification. A global-index witness is acceptable only if the Script proves uniqueness, monotonicity, group membership, and complete coverage.

Required failure taxonomy

Failure Required behavior
missing or empty required witness field stable witness/codec error
unknown plan codec version reject
malformed offset table or truncated item stable Molecule error
plan count greater than N stable count error
fewer outputs than plans stable missing-output error
more outputs than plans stable extra-output error
reordered outputs stable correspondence error
duplicate plan or output index stable duplication error
wrong Type Script or Lock Script stable Script-policy error
wrong data/schema stable output-data error
insufficient capacity stable capacity error
reused identity where freshness is required stable identity error
machine block removed standalone checker rejects the mutation

Implementation phases

Phase 0 — specification

Extend or add an accepted RFC that fixes:

  1. witness field and Molecule schema;
  2. codec versioning and canonical encoding;
  3. output selection source and ordering;
  4. count and zero-element behavior;
  5. one-to-one correspondence;
  6. Script/data/lock verification;
  7. occupied-capacity policy;
  8. fresh and preserved identity policies;
  9. ProofPlan and typed-semantics records;
  10. error codes and resource budgets.

Phase 1 — codec and typed boundary

  • generate and verify the canonical plan-list codec;
  • bind codec identity into entry ABI and metadata;
  • retain the full create template and predicate in typed semantics;
  • add separate ProofPlan obligations for decode, count, selection, ordering, pair correspondence, identity, and capacity;
  • make the builder manifest generate a fillable but non-authoritative plan skeleton.

Phase 2 — CKB runtime lowering

  • decode once with strict bounds;
  • select group-relative outputs canonically;
  • compare counts before materialization;
  • lower a deterministic bounded pair loop;
  • verify all output fields the compiler claims are constructed;
  • retain fail-closed behavior for every unsupported shape.

Phase 3 — independent verification and builder parity

  • teach the standalone checker to link every pair-validation block to typed semantics and source ranges;
  • add mutations deleting or bypassing count, ordering, identity, capacity, and data checks;
  • ensure generated builders and cellc tx validate use the same ordering and codec;
  • run every positive and adversarial fixture in simulator, CKB-VM, and the stateful harness.

Acceptance matrix

Case Expected
zero plans/outputs when allowed pass
one plan/output pass
exactly N pairs pass
N + 1 plans stable count error
missing output stable missing-output error
extra output stable extra-output error
reordered outputs stable correspondence error
duplicated plan or selected output stable duplication error
wrong Type Script stable Script-policy error
wrong Lock Script stable Script-policy error
wrong data payload stable schema/data error
under-capacity output stable capacity error
reused Type ID or logical identity stable identity error
valid builder output with one adversarial post-build mutation CKB-VM rejects
removed correspondence block in ELF standalone checker rejects

Completion criteria

  • An accepted RFC fixes the codec, ordering, identity, and capacity contracts.
  • Supported shapes no longer emit runtime error 24 or E2105.
  • Unsupported output collections remain fail-closed.
  • The builder and Script share one versioned plan/order specification.
  • Every plan/output pair is verified on chain exactly once.
  • Standalone checker mutations cover count, ordering, pair, identity, data, lock, type, and capacity checks.
  • Simulator, CKB-VM, stateful acceptance, and tx validate agree.
  • Worst-case cycles, stack, code size, transaction size, and occupied capacity are recorded.
  • dev, ci, and backend gates pass.
  • Independent security review is complete.

Non-goals

  • arbitrary allocator-backed output vectors;
  • transaction-wide fuzzy matching;
  • builder-only authorization;
  • implicit output ordering;
  • identity inferred from source names;
  • Cell-backed collection return values;
  • ranged foreign-Script composition, which belongs to a protocol-composition design.

Dependencies

References

Activity

  1. a19q3 commented on Aug 27, 2026

    @a19q3
    CollaboratorAuthor

    Research update: output ranges need a stricter consensus codec than the builder path

    Comment audit

    There were no prior comments on this issue at the time of review.

    Argent PR #44 has active review comments, and the dynamic array ABI finding is directly relevant to create_each:

    Argent's route/output coverage work in PR #1 and bounded emits work in PR #44 are useful design signals, but neither changes the CKB requirement that the Type Script independently prove output correspondence.

    Sharpened CKB model

    For the first supported Type Script shape, the selected output set should be the complete GroupOutput view for the current exact Type Script. That gives a consensus-defined ordering and automatically makes an extra output with the same Type Script visible to the count check.

    The core invariant should be evaluated from independently obtained values:

    • plan_count comes only from a fully validated witness PlanList;
    • output_count comes only from enumerating GroupOutput;
    • both are bounded before pair iteration;
    • plan_count equals output_count;
    • each plan[i] authorizes exactly GroupOutput[i].

    A builder-supplied list of global output indexes is a more complex later shape. If allowed, the Script would also need to prove strict monotonicity, uniqueness, group membership, in-range indexes, and complete group coverage. The group-relative form is safer for v1.

    Decoder requirements

    The PR #44 ABI review demonstrates why a canonical encoder is insufficient. Before reading plan[i], the CKB runtime must validate:

    • witness field presence and exact field selection;
    • supported codec version;
    • total byte length and maximum plan count;
    • Molecule offset-table width and bounds;
    • monotonic offsets;
    • item start/end within the loaded region;
    • schema leaf cardinality;
    • bounded dynamic field lengths;
    • checked arithmetic for every offset and allocation/scratch calculation.

    A plan count that is less than or equal to N is not enough if the corresponding offsets can address outside the validated byte region.

    The builder, simulator, CKB-VM runtime, and independent checker should share golden vectors, but the on-chain decoder must not assume those producers were used.

    Pair validation should be explicit

    For each pair, the runtime should keep separate ProofPlan/checker obligations for:

    1. plan predicate;
    2. output selection/index;
    3. exact Type Script;
    4. Lock Script policy;
    5. canonical data codec and value;
    6. occupied-capacity floor computed from the actual serialized output;
    7. resource identity/freshness or preservation rule;
    8. exactly-once pair coverage.

    This prevents a future optimization from replacing “verify constructed output” with “trust generated template.”

    Occupied capacity deserves special care: it must be calculated from the actual output capacity, lock script, optional type script, and data length, not from a builder estimate or a type-only constant.

    Relationship to #7

    The issues should share:

    • bounded loop lowering;
    • strict count/offset primitives;
    • stable runtime error allocation;
    • ProofPlan and checker mutation patterns;
    • cycle/stack/code-size measurement.

    They should not share the source semantics:

    Keeping them separate avoids treating a witness plan as a Cell or a GroupOutput as authored plan state.

    Acceptance additions

    Please include adversarial cases for:

    • valid plan_count with a truncated offset table;
    • overlapping or non-monotonic plan item offsets;
    • offset arithmetic overflow;
    • correct number of outputs but one output outside the current Type Script group;
    • one extra GroupOutput with otherwise valid first N pairs;
    • valid data with the wrong Lock Script;
    • capacity equal to a stale builder estimate but below the actual occupied-capacity floor;
    • Type ID reuse/freshness violations;
    • duplicate logical identity across two otherwise distinct outputs;
    • a valid builder transaction mutated after construction by inserting, deleting, reordering, or changing exactly one output;
    • deletion of only the output_count equality block in the ELF;
    • deletion of only the last pair validation block, to catch off-by-one coverage.

    Scope recommendation

    The first version should remain:

    • Type Script only;
    • GroupOutput ordered;
    • one versioned WitnessArgs field;
    • fixed or tightly bounded plan schemas;
    • no allocator-backed vectors;
    • no foreign Script output roles;
    • no implicit global index list;
    • no builder-only freshness or authorization.

    Cross-Script output coordination belongs in #9/#10 after this local one-to-one verifier is complete.

    Conclusion

    The issue remains valid and appropriately separate from #7. The most important research result is that the canonical PlanList contract must specify both the normal encoding and every rejection condition. Argent's current range review shows that “the builder emits valid arrays” is not enough; CellScript's completion criterion must be adversarial decoder safety plus complete GroupOutput correspondence.

    Current honest boundary:

    • | `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 |
      | `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
      The current backend supports bounded local `Vec<T>` operations only when `T`
    • entry!(
      "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"]
      ),
      ];
  2. changed the title [-][0.26][P0] Implement executable bounded output-plan correspondence[/-] [+][Candidate][Consensus runtime] Implement executable bounded output-plan correspondence[/+] on Aug 27, 2026
  3. a19q3 commented on Sep 12, 2026

    @a19q3
    CollaboratorAuthor

    0.30 closure update: the admitted fixed-width bounded output-plan contract is complete. CSBPLv1 composes inside the canonical CSARGv1 WitnessArgs.input_type envelope; the verifier independently enforces bounded plan count, complete canonical GroupOutput order, exact one-to-one count/correspondence, data, Lock, Type, capacity, and identity policy. Generated builders, ProtocolBundle/adapter validation, independent machine checks, adversarial mutations, CKB-VM, stateful, and production evidence cover the same contract.

    The clean release replay at 3cf60a1 passed, including the final product and local-node gates. Independent review was explicitly waived by the maintainer for this bounded 0.30 scope; it was not performed or claimed as passed. Computed/dynamic templates, foreign Script output roles, and unbounded plans remain fail-closed and out of scope. Closing the accepted issue.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions