Skip to content

Commit 95eb2c9

Browse files
a19q3a19q3
committed
Harden 0.16 assurance and add iCKB benchmark
1 parent 9ad1af1 commit 95eb2c9

66 files changed

Lines changed: 3934 additions & 267 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎docs/0.17/CELLSCRIPT_0_17_ROADMAP.md‎

Lines changed: 489 additions & 0 deletions
Large diffs are not rendered by default.

‎docs/0.17/ickb_cellscript_gap_matrix.md‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
# iCKB CellScript Expressibility Matrix
2+
3+
Support levels:
4+
5+
- `NATIVE`: direct, clear CellScript surface.
6+
- `EXPRESSIBLE_WITH_PATTERN`: possible with recurring idiom or model helper.
7+
- `EXPRESSIBLE_WITH_ESCAPE_HATCH`: needs raw CKB/Rust/codegen-level logic.
8+
- `NOT_EXPRESSIBLE`: not currently representable.
9+
- `OUT_OF_SCOPE`: off-chain or external protocol behaviour.
10+
11+
| iCKB semantic item | Support | Desired CellScript surface | Current workaround | Compiler/codegen need | Test strategy | Severity |
12+
|---|---|---|---|---|---|---|
13+
| Linear receipt consumption | NATIVE | `receipt R`, `consume receipt` | Used in `ickb_logic.cell` | None | Compile plus model duplicate receipt fixture | LOW |
14+
| DAO deposit/receipt output grouping | EXPRESSIBLE_WITH_PATTERN | `assert_grouped_outputs(DaoDeposit.amount == Receipt.amount * qty)` | Rust model fixture; CellScript resource/receipt fields | Executable aggregate invariant lowering over output groups | Positive deposit phase 1, forged receipt negative | HIGH |
15+
| Deposit min/max unoccupied capacity | NATIVE | `assert_invariant(amount >= min && amount <= max)` | Used in CellScript and fixture model | Better occupied/unoccupied capacity primitive | Capacity violation negative | MEDIUM |
16+
| Header dep accumulated-rate load | NOT_EXPRESSIBLE | `let ar = header_dep(input).dao.accumulated_rate` | Explicit `deposit_accumulated_rate` field plus model flag | HeaderDep source API with fail-closed missing-header behaviour | Missing/wrong header negatives are model-level | BLOCKER |
17+
| Exact iCKB accounting across tokens, receipts, deposits | EXPRESSIBLE_WITH_ESCAPE_HATCH | `assert_sum(inputs<IckbToken>.amount + receipt_value(...)) == ...` | Fixture model checks exact equation | Runtime aggregate lowering, computed aggregate expressions, group scans | Inflation/deflation negatives | BLOCKER |
18+
| Proposal `>=` vs Rust exact equality distinction | EXPRESSIBLE_WITH_PATTERN | Relation operator in aggregate invariant | Model uses Rust exact equality | Diagnostic/reporting support for source/proposal discrepancies | Deflation negative | HIGH |
19+
| xUDT args `[logic_hash, flags]` binding | EXPRESSIBLE_WITH_ESCAPE_HATCH | `type xudt<owner_mode=input_type>(logic_hash)` | `xudt_args_hash: Hash` placeholder | First-class Script and xUDT stdlib ABI constructors | Wrong xUDT binding negative | HIGH |
20+
| Script used as both lock and type in coordinated cells | NOT_EXPRESSIBLE | `current_script_role()`, `cell.lock == self`, `cell.type == self` | Comments and model fixture | Script-role introspection and Source group APIs | Script role confusion negative | BLOCKER |
21+
| Empty args for all current/output script uses | EXPRESSIBLE_WITH_ESCAPE_HATCH | `require_empty_args(self, outputs = true)` | Not represented in CellScript; model fixture | Script args source and output lock/type scan | Witness/script misuse fixture | HIGH |
22+
| CKB occupied/unoccupied capacity | EXPRESSIBLE_WITH_PATTERN | `cell.capacity.unoccupied()` | Explicit field on model resources | Native occupied capacity syscall wrapper and capacity evidence | Capacity fixture | HIGH |
23+
| NervosDAO deposit/withdrawal data classification | EXPRESSIBLE_WITH_ESCAPE_HATCH | `is_dao_deposit(cell)`, `is_dao_withdrawal(cell)` | Model fields and docs | DAO stdlib primitives over type hash and data bytes | Deposit/withdrawal fixtures | HIGH |
24+
| DAO maturity/second withdrawal | EXPRESSIBLE_WITH_ESCAPE_HATCH | `require_dao_maturity(request)` | Explicit epoch fields in model | Since/DAO maturity helper that binds deposit/request headers | Immature redeem negative | HIGH |
25+
| CKB CellDep/deployment dep-group binding | EXPRESSIBLE_WITH_PATTERN | `requires_cell_dep("ickb_dep_group")` | Metadata assumptions and fixture model | Stronger deploy manifest/runtime dep validation | Cell dep substitution negative | HIGH |
26+
| Limit Order C256 checked arithmetic | EXPRESSIBLE_WITH_ESCAPE_HATCH | `checked_u256` or `ckb::u256` | u128 CellScript model | Checked 256-bit arithmetic library/codegen | Underpayment positive/negative | HIGH |
27+
| Limit Order MetaPoint/OutPoint binding | NOT_EXPRESSIBLE | `input.out_point`, `output.index`, signed relative distance | Unsigned model fields | OutPoint/index Source APIs and signed ints | Limit order and Owned-Owner fixtures | BLOCKER |
28+
| Limit Order ratio validation | EXPRESSIBLE_WITH_PATTERN | `Ratio?`, `Option<Ratio>` | Zero-pair sentinel fields | Option/union ergonomic support and Molecule union encoding | Malformed ratio model support | MEDIUM |
29+
| Limit Order partial fill min | NATIVE for arithmetic | `assert_invariant(delta >= min)` | Implemented in `limit_order.cell` | u256 support for production parity | Limit positive/underpayment negative | MEDIUM |
30+
| Owned-Owner signed i32 distance | NOT_EXPRESSIBLE | `i32`, `owner.index + distance == owned.index` | Unsigned indexes | Signed integer types and source index APIs | Owned-Owner positive/wrong-owner negative | HIGH |
31+
| Witness parsing and malformation rejection | EXPRESSIBLE_WITH_PATTERN | `witness T`, explicit ABI | Existing witness params for simple typed data | Full Molecule witness parser and signature primitive | Witness malformation negative is model-level | HIGH |
32+
| CoBuild/OTX UI heuristics | OUT_OF_SCOPE | N/A | Document only | Off-chain tooling | Not tested | LOW |
33+
| Non-upgradable deployment proof | OUT_OF_SCOPE for compiler semantics | Deployment manifest proof | Docs only | Deployment verification tooling | Not tested | MEDIUM |
34+
35+
## Compiler Features Missing For iCKB-Grade Claims
36+
37+
1. Header dep access that binds an input/receipt/deposit to its block header and
38+
fails closed when absent.
39+
2. First-class Script values, current script hash, current role, lock/type group
40+
views, and script args inspection.
41+
3. Executable transaction aggregate invariants with computed expressions, not
42+
only metadata-only proof-plan records.
43+
4. CKB source views for outpoints, output indexes, occupied capacity, and
44+
outputs/outputs-data alignment as ordinary typed expressions.
45+
5. DAO and xUDT stdlib primitives that match deployed script ABIs.
46+
6. Signed integer types and checked 256-bit arithmetic.
47+
7. Stable diagnostics/error codes for each lowered invariant family.

‎docs/0.17/ickb_diff_results.md‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
# iCKB Differential Results
2+
3+
The differential harness is partial and model-level only.
4+
5+
`tests/benchmarks/ickb_diff/matrix.json` records the selected comparison
6+
matrix. The test `ickb_diff_matrix_is_partial_and_consistent_with_model_fixtures`
7+
checks that every row is labelled as a model result rather than CKB VM
8+
equivalence.
9+
10+
| Scenario | Original iCKB expected | CellScript expected | Result |
11+
|---|---:|---:|---|
12+
| valid deposit phase 1 | pass | pass | model-pass |
13+
| valid mint from receipt | pass | pass | model-pass |
14+
| duplicate receipt | fail | fail | model-pass |
15+
| amount inflation | fail | fail | model-pass |
16+
| wrong owner | fail | fail | model-pass |
17+
| wrong xUDT args | fail | fail | model-pass |
18+
| immature redeem | fail | fail | model-pass |
19+
| valid limit order | pass | pass | model-pass |
20+
| limit order underpayment | fail | fail | model-pass |
21+
22+
## Why This Is Not Behavioural Equivalence
23+
24+
- The original iCKB Rust scripts were not executed side-by-side with generated
25+
CellScript artifacts.
26+
- iCKB `cargo test --locked` did not run to completion because prebuilt Capsule
27+
contract binaries were missing under `scripts/build/debug`.
28+
- CellScript currently lacks first-class HeaderDep, Script role, CKB OutPoint,
29+
occupied capacity, xUDT args, and DAO maturity primitives required for a true
30+
CKB VM differential test.
31+
32+
## Next Differential Step
33+
34+
Build the iCKB scripts with Capsule, then adapt a small CKB testtool fixture set
35+
so each transaction skeleton can run:
36+
37+
1. original iCKB binary,
38+
2. generated CellScript binary,
39+
3. identical cell deps, header deps, witnesses, inputs, outputs, and output
40+
data where semantics overlap.
41+
42+
Until that exists, equivalence must not be claimed.

‎docs/0.17/ickb_discovery.md‎

Lines changed: 169 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,169 @@
1+
# iCKB CellScript Completeness Benchmark: Discovery
2+
3+
Date: 2026-04-28
4+
5+
## Repositories
6+
7+
- CellScript: current repository, `/Users/arthur/RustroverProjects/CellScript`.
8+
- iCKB proposal: cloned to `/tmp/cellscript-ickb-audit/proposal`.
9+
- Commit inspected: `055f0cb2c44b2988531c241a6f7167397bbe42c7`.
10+
- iCKB v1-core: cloned to `/tmp/cellscript-ickb-audit/v1-core`.
11+
- Commit inspected: `f7bbf7fe691d449a68a4b973d3102b7af28b2c9b`.
12+
13+
No iCKB repository was vendored into CellScript source control.
14+
15+
## CellScript Architecture Map
16+
17+
- Parser and AST:
18+
- `src/parser/mod.rs`
19+
- `src/ast/mod.rs`
20+
- Semantic analysis and name/type handling:
21+
- `src/types/mod.rs`
22+
- `src/resolve/mod.rs`
23+
- `src/lifecycle/mod.rs`
24+
- IR and compile pipeline:
25+
- `src/lib.rs`
26+
- `src/ir/mod.rs`
27+
- `src/optimize/mod.rs`
28+
- CKB backend/codegen/runtime metadata:
29+
- `src/codegen/mod.rs`
30+
- `src/stdlib/mod.rs`
31+
- `src/stdlib/ckb_protocols/*`
32+
- `src/assumptions.rs`
33+
- `src/runtime_errors.rs`
34+
- CLI and user-facing commands:
35+
- `src/main.rs`
36+
- `src/cli/commands.rs`
37+
- LSP/editor:
38+
- `src/lsp/mod.rs`
39+
- `src/lsp/server.rs`
40+
- Formatting:
41+
- `src/fmt/mod.rs`
42+
- Existing examples:
43+
- `examples/*.cell`
44+
- `examples/acceptance/*.cell`
45+
- `examples/language/*.cell`
46+
- Existing tests:
47+
- Rust integration tests under `tests/*.rs`
48+
- CKB compatibility fixtures under `tests/compat/ckb_standard/*.json`
49+
- Existing CI runs `cargo test --locked --manifest-path Cargo.toml -- --test-threads=1`.
50+
51+
## iCKB Architecture Map
52+
53+
- Proposal:
54+
- `proposal/README.md`
55+
- `proposal/2024_overview.md`
56+
- Script workspace:
57+
- `v1-core/scripts/Cargo.toml`
58+
- `v1-core/scripts/README.md`
59+
- `v1-core/scripts/capsule.toml`
60+
- iCKB Logic script:
61+
- `scripts/contracts/ickb_logic/src/entry.rs`
62+
- `scripts/contracts/ickb_logic/src/celltype.rs`
63+
- `scripts/contracts/ickb_logic/src/constants.rs`
64+
- `scripts/contracts/ickb_logic/src/utils.rs`
65+
- `scripts/contracts/ickb_logic/src/error.rs`
66+
- Limit Order script:
67+
- `scripts/contracts/limit_order/src/entry.rs`
68+
- `scripts/contracts/limit_order/src/error.rs`
69+
- Owned-Owner script:
70+
- `scripts/contracts/owned_owner/src/entry.rs`
71+
- `scripts/contracts/owned_owner/src/error.rs`
72+
- Shared utilities and schemas:
73+
- `scripts/contracts/utils/src/utils.rs`
74+
- `scripts/contracts/utils/src/dao.rs`
75+
- `scripts/contracts/utils/src/constants.rs`
76+
- `scripts/contracts/utils/src/c256.rs`
77+
- `schemas/encoding.mol`
78+
- iCKB test harness:
79+
- `scripts/tests/src/lib.rs`
80+
- `scripts/tests/src/tests.rs`
81+
82+
## Commands Run
83+
84+
CellScript discovery:
85+
86+
```bash
87+
ast-outline digest src
88+
git status --short --branch
89+
find .github -maxdepth 3 -type f -print
90+
sed -n '1,220p' .github/workflows/ci.yml
91+
```
92+
93+
iCKB checkout:
94+
95+
```bash
96+
rm -rf /tmp/cellscript-ickb-audit
97+
mkdir -p /tmp/cellscript-ickb-audit
98+
git clone --depth 1 https://github.com/ickb/proposal.git /tmp/cellscript-ickb-audit/proposal
99+
git clone --depth 1 https://github.com/ickb/v1-core.git /tmp/cellscript-ickb-audit/v1-core
100+
git -C /tmp/cellscript-ickb-audit/proposal rev-parse HEAD
101+
git -C /tmp/cellscript-ickb-audit/v1-core rev-parse HEAD
102+
```
103+
104+
iCKB source inspection:
105+
106+
```bash
107+
ast-outline digest scripts/contracts scripts/tests/src
108+
ast-outline scripts/contracts/ickb_logic/src/entry.rs
109+
ast-outline scripts/contracts/limit_order/src/entry.rs
110+
ast-outline scripts/contracts/owned_owner/src/entry.rs
111+
ast-outline show scripts/contracts/ickb_logic/src/entry.rs main
112+
ast-outline show scripts/contracts/ickb_logic/src/entry.rs check_input
113+
ast-outline show scripts/contracts/ickb_logic/src/entry.rs deposit_to_ickb
114+
ast-outline show scripts/contracts/ickb_logic/src/entry.rs check_output
115+
ast-outline show scripts/contracts/limit_order/src/entry.rs main
116+
ast-outline show scripts/contracts/limit_order/src/entry.rs validate
117+
ast-outline show scripts/contracts/limit_order/src/entry.rs extract_order
118+
ast-outline show scripts/contracts/owned_owner/src/entry.rs main
119+
ast-outline show scripts/contracts/owned_owner/src/entry.rs extract_owned_metapoint
120+
```
121+
122+
Baseline tests before benchmark changes:
123+
124+
```bash
125+
cargo test --locked -p cellscript
126+
```
127+
128+
Result: passed. The run executed 529 Rust tests across library and integration
129+
targets plus doc-tests with no failures.
130+
131+
iCKB tests:
132+
133+
```bash
134+
cd /tmp/cellscript-ickb-audit/v1-core/scripts
135+
cargo test --locked
136+
```
137+
138+
Result: Rust crates compiled, but the `tests` crate failed both tests because
139+
the loader expected contract binaries under `scripts/build/debug` and they were
140+
not present. `scripts/tests/src/lib.rs:53-67` constructs that path. The iCKB
141+
README requires Capsule/Cross release builds first:
142+
143+
```bash
144+
cargo install cross --git https://github.com/cross-rs/cross --rev=6982b6c --locked
145+
cargo install ckb-capsule --git https://github.com/nervosnetwork/capsule --rev=04fd58c --locked
146+
capsule build --release
147+
```
148+
149+
`docker` was installed locally, but `capsule` and `cross` were not available.
150+
I did not install global tooling or run Docker builds as part of this benchmark.
151+
152+
Benchmark tests after implementation:
153+
154+
```bash
155+
cargo test --locked -p cellscript --test ickb_benchmark
156+
```
157+
158+
Result: passed, 4 tests.
159+
160+
## Assumptions And Gaps
161+
162+
- iCKB source references are to the shallow clone commit listed above.
163+
- The CellScript benchmark is a partial semantic model. It is not a byte-for-byte
164+
or VM-behaviour-equivalent port.
165+
- Current CellScript can compile the benchmark specs to RISC-V assembly, but the
166+
benchmark fixtures are model-level checks rather than generated CKB VM
167+
executions.
168+
- iCKB's own reusable CKB test harness could not be run to completion without
169+
a prior Capsule build producing `build/debug` or `build/release` binaries.

‎docs/0.17/ickb_final_report.md‎

Lines changed: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,121 @@
1+
# iCKB CellScript Completeness Benchmark Final Report
2+
3+
## Executive Summary
4+
5+
CellScript is **partially complete but not ready** for iCKB-grade CKB protocols.
6+
7+
It can express useful iCKB-style resource, receipt, linear-consumption,
8+
owner-pairing, transfer, and limit-order arithmetic patterns. It cannot yet
9+
express several production-critical iCKB invariants natively: HeaderDep
10+
accumulated-rate binding, script lock/type role introspection, exact
11+
transaction-wide computed accounting, xUDT args construction, DAO maturity, CKB
12+
OutPoint/index relations, C256 arithmetic, and signed relative distances.
13+
14+
The benchmark is an iCKB-inspired semantic model. It is not a faithful port and
15+
does not prove behavioural equivalence with the audited iCKB Rust scripts.
16+
17+
## Implemented Artifacts
18+
19+
- `examples/ickb_benchmark/README.md`
20+
- `examples/ickb_benchmark/ickb_logic.cell`
21+
- `examples/ickb_benchmark/limit_order.cell`
22+
- `examples/ickb_benchmark/owned_owner.cell`
23+
- `tests/ickb_benchmark.rs`
24+
- `tests/benchmarks/ickb_positive/*.json`
25+
- `tests/benchmarks/ickb_negative/*.json`
26+
- `tests/benchmarks/ickb_diff/matrix.json`
27+
- `docs/0.17/ickb_discovery.md`
28+
- `docs/0.17/ickb_semantics.md`
29+
- `docs/0.17/ickb_cellscript_gap_matrix.md`
30+
- `docs/0.17/ickb_diff_results.md`
31+
- `docs/0.17/ickb_final_report.md`
32+
33+
CI integration is through the existing Cargo test workflow: `tests/ickb_benchmark.rs`
34+
is a normal integration test, so the existing `cargo test --locked ...` CI step
35+
will run it.
36+
37+
## Coverage Table
38+
39+
| Semantic item | CellScript support | Test coverage | Remaining gap | Severity |
40+
|---|---|---|---|---|
41+
| Deposit phase 1 receipt creation | EXPRESSIBLE_WITH_PATTERN | positive + forged receipt/capacity negatives | executable output-group aggregate lowering | HIGH |
42+
| Deposit phase 2 mint | EXPRESSIBLE_WITH_ESCAPE_HATCH | positive + inflation/deflation/header/xUDT negatives | HeaderDep and xUDT binding | BLOCKER |
43+
| Receipt consumption/no double use | NATIVE plus model duplicate check | duplicate receipt negative | true prior-cell lineage API | MEDIUM |
44+
| iCKB transfer | NATIVE for token resource model | positive transfer | xUDT ABI binding | HIGH |
45+
| Withdrawal/redeem | EXPRESSIBLE_WITH_ESCAPE_HATCH | positive withdrawal, immature redeem negative | DAO maturity and since/header primitives | HIGH |
46+
| Exact accounting | EXPRESSIBLE_WITH_ESCAPE_HATCH | inflation/deflation negatives | executable computed aggregate invariants | BLOCKER |
47+
| Owned-Owner pairing | EXPRESSIBLE_WITH_PATTERN | positive + wrong owner negative | signed distance and source index APIs | HIGH |
48+
| Limit Order fulfilment | EXPRESSIBLE_WITH_PATTERN | positive + underpayment/wrong asset negatives | C256 and MetaPoint support | HIGH |
49+
| Script role confusion | NOT_EXPRESSIBLE | negative model fixture | current script role/source scans | BLOCKER |
50+
| Witness malformation | EXPRESSIBLE_WITH_PATTERN | negative model fixture | full witness/Molecule parser and auth primitives | HIGH |
51+
| CellDep substitution | EXPRESSIBLE_WITH_PATTERN | negative model fixture | deploy/runtime dep verification integration | HIGH |
52+
53+
## Test Results
54+
55+
Commands run before benchmark changes:
56+
57+
```bash
58+
cargo test --locked -p cellscript
59+
```
60+
61+
Result: passed, 529 Rust tests plus doc-tests.
62+
63+
iCKB test attempt:
64+
65+
```bash
66+
cd /tmp/cellscript-ickb-audit/v1-core/scripts
67+
cargo test --locked
68+
```
69+
70+
Result: crates compiled, but the iCKB `tests` crate failed 2 tests because
71+
Capsule-built binaries were missing under `scripts/build/debug`.
72+
73+
Benchmark command:
74+
75+
```bash
76+
cargo test --locked -p cellscript --test ickb_benchmark
77+
```
78+
79+
Result: passed, 4 tests.
80+
81+
The positive fixture set contains 6 model-level cases. The negative set contains
82+
15 adversarial model-level cases. The differential matrix contains 9
83+
model-level rows.
84+
85+
## Compiler Changes Made
86+
87+
No compiler implementation changes were made. The benchmark intentionally records
88+
the current compiler gaps instead of weakening invariants to make a production
89+
claim.
90+
91+
## Unresolved Blockers
92+
93+
1. HeaderDep accumulated-rate binding.
94+
2. Lock/type script-role introspection and script args scanning.
95+
3. Executable transaction-wide aggregate invariants with computed values.
96+
4. Native xUDT owner-mode args and token amount layout support.
97+
5. DAO deposit/withdrawal/maturity primitives.
98+
6. CKB OutPoint, output index, occupied capacity, and CellDep surfaces.
99+
7. Signed integer types and checked 256-bit arithmetic.
100+
8. Stable per-invariant diagnostics and runtime error codes.
101+
102+
## Recommended Next Steps
103+
104+
1. Add typed CKB source primitives for headers, outpoints, script role, script
105+
args, occupied capacity, and cell deps.
106+
2. Lower aggregate invariants into executable CKB runtime checks for exact
107+
equality and bounded inequality over typed cell groups.
108+
3. Add `std::dao` and `std::xudt` modules with deployed ABI-compatible helpers.
109+
4. Add signed integer and checked `u256`/`C256` arithmetic support.
110+
5. Build an actual CKB testtool differential harness once iCKB Capsule binaries
111+
and CellScript generated binaries can be run against the same fixtures.
112+
6. Use a Rosen-style bridge settlement invariant benchmark after iCKB to test
113+
multi-party cross-chain accounting and replay prevention.
114+
115+
## Honesty Statement
116+
117+
This benchmark is a semantic model and partial port. It proves that selected
118+
iCKB-style positive and adversarial scenarios can be represented and checked at
119+
the model level while the CellScript specs compile. It does not prove CKB VM
120+
behavioural equivalence, production readiness, cycle bounds, transaction size,
121+
occupied capacity, or under-capacity safety.

0 commit comments

Comments
 (0)