From 06a354321637a684eb39758ee4b883d43dbd80f7 Mon Sep 17 00:00:00 2001 From: "sm.wu" Date: Thu, 23 Apr 2026 10:00:16 +0800 Subject: [PATCH 1/2] [docs] mem continuation check --- docs/src/SUMMARY.md | 1 + docs/src/architecture-overview.md | 8 ++- docs/src/memory-continuation-checks.md | 87 ++++++++++++++++++++++++++ 3 files changed, 95 insertions(+), 1 deletion(-) create mode 100644 docs/src/memory-continuation-checks.md diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index 1d6a2c7fb..fe23681b8 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -18,6 +18,7 @@ - [Differences from RISC-V](./differences-from-risc-v.md) - [Technical Overview](./technical-overview.md) - [Architecture Overview](./architecture-overview.md) + - [Memory Continuation Checks](./memory-continuation-checks.md) - [Prover Workflow](./prover-workflow.md) - [Optimizations](./optimizations.md) - [Appendix](./appendix.md) diff --git a/docs/src/architecture-overview.md b/docs/src/architecture-overview.md index e8116d59c..33731cc40 100644 --- a/docs/src/architecture-overview.md +++ b/docs/src/architecture-overview.md @@ -102,6 +102,13 @@ compose into a single consistent execution: $\text{shard}_i.\text{end\_pc} = \text{shard}_{i+1}.\text{init\_pc}$ (and likewise for other `GlobalState` fields) at every shard boundary. +- **Dynamic heap/hint continuity.** Shards also expose the start + address and length of the dynamic heap and hint init regions. The + verifier checks that these segments stay within the platform's heap + and hint windows and that each shard starts exactly where the + previous shard ended, so dynamic init data cannot skip, overlap, or + move out of range across shard boundaries. See + [Memory Continuation Checks](./memory-continuation-checks.md). - **Cross-shard memory consistency.** Memory written in shard $i$ must remain readable in any later shard $j > i$. The within-shard RAM grand product $\prod R = \prod W$ cannot be reused across @@ -154,4 +161,3 @@ compose into a single consistent execution: $\sum_{\text{shard}} \Sigma_{\text{shard}} = \mathcal{O}$ (the point at infinity) directly. The number of shards is at most in the hundreds, so this is a few hundred EC additions. - diff --git a/docs/src/memory-continuation-checks.md b/docs/src/memory-continuation-checks.md new file mode 100644 index 000000000..1907850d5 --- /dev/null +++ b/docs/src/memory-continuation-checks.md @@ -0,0 +1,87 @@ +# Memory Continuation Checks + +When execution is split into multiple shards, Ceno must check not only +that control flow continues correctly, but also that the dynamic memory +regions exposed through public values remain consistent across shard +boundaries. + +The two dynamic regions are: + +- **Heap** +- **Hints** + +Each shard exposes the start address and length of its current heap and +hint segment. The verifier then checks that these segments form one +continuous sequence over the full trace. + +

+ +```text +heap / hint address space + + shard 0 shard 1 shard 2 +┌──────────────┐ ┌──────────────┐ ┌──────────────┐ +│ start = s0 │ │ start = e0 │ │ start = e1 │ +│ len = l0 │ │ len = l1 │ │ len = l2 │ +│ end = e0 │───▶│ end = e1 │───▶│ end = e2 │ +└──────────────┘ └──────────────┘ └──────────────┘ + +Requirements: +- every start/end stays inside the allowed platform range +- next shard starts exactly at previous shard end +- proof table length matches the public length +``` + +

+ +## What Is Being Checked + +For both heap and hints, full-trace verification enforces: + +- **Range correctness**: each shard's start and end must stay inside the + configured memory window +- **Continuation**: shard `i + 1` must start exactly where shard `i` + ended +- **Length consistency**: the dynamic init table proved inside the shard + must have the same length as the public value + +These checks rule out three classes of errors: + +- a shard claiming memory outside the allowed heap or hint range +- a gap or overlap between consecutive shards +- a mismatch between the public memory length and the table actually + proved + +## How This Fits with the Other Memory Checks + +These continuation checks are different from the cross-shard RAM +consistency check. + +- **RAM consistency** checks that reads and writes across shards compose + to one valid memory history +- **Memory continuation** checks that the dynamic heap and hint segments + themselves are chained correctly from shard to shard + +Both are needed: + +- RAM consistency protects the memory contents +- continuation checks protect the public memory layout + +## Full-Trace vs Single-Shard Verification + +Continuation is a **full-trace** property. + +- In full-trace verification, heap and hint segments are chained across + all shards +- In single-shard debug verification, Ceno only checks that the selected + shard is internally valid; it does not claim that the shard forms a + complete continuation of the whole execution + +## Where This Lives in the System + +- the platform defines the allowed heap and hint ranges +- the native verifier checks shard-by-shard continuation +- the recursion verifier enforces the same bounds in aggregation + +This keeps the memory-state invariant aligned across both native and +recursive verification. From fc8fc48bd439a42cd6f06e318d0be310187f8771 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 23 Apr 2026 03:32:56 +0000 Subject: [PATCH 2/2] docs: clarify lazy dynamic init and no-overlap continuation Agent-Logs-Url: https://github.com/scroll-tech/ceno/sessions/301be933-f753-4a8d-a421-7f92a024053d Co-authored-by: kunxian-xia <1082586+kunxian-xia@users.noreply.github.com> --- docs/src/memory-continuation-checks.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/docs/src/memory-continuation-checks.md b/docs/src/memory-continuation-checks.md index 1907850d5..5e411b57e 100644 --- a/docs/src/memory-continuation-checks.md +++ b/docs/src/memory-continuation-checks.md @@ -14,6 +14,12 @@ Each shard exposes the start address and length of its current heap and hint segment. The verifier then checks that these segments form one continuous sequence over the full trace. +Intuitively, this supports lazy dynamic init: early shards can expose +zero length for heap/hints, and the segment only extends once those +addresses are first accessed. Because every next segment must start at +the previous end, the exposed ranges are append-only and non-overlapping, +so an address cannot be initialized twice across shards. +

```text @@ -29,6 +35,7 @@ heap / hint address space Requirements: - every start/end stays inside the allowed platform range - next shard starts exactly at previous shard end +- segments are append-only (no overlaps or rewinds) - proof table length matches the public length ```