Skip to content

new interleaving prover/circuit matching the compiler/runtime - #232

Draft
ecioppettini wants to merge 31 commits into
mainfrom
enzo/new-interleaving-prover
Draft

new interleaving prover/circuit matching the compiler/runtime#232
ecioppettini wants to merge 31 commits into
mainfrom
enzo/new-interleaving-prover

Conversation

@ecioppettini

@ecioppettini ecioppettini commented Sep 17, 2026

Copy link
Copy Markdown
Contributor

No description provided.

@ecioppettini
wip: new interleaving prover (matching new quint spec)
13b0cdc 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
remove broken import
4141bad 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
wire spec conformance tests (circuit sat iff quint sat and sat ?= exp…
c4b2c7d 
…ected)

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
bump nightstream branch (get continuity sanity checker)
7c1b685 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
starstream-interleaving-proof-legacy nightstream compat
5da6e6e 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
circuit: add check_continuity_rows to verify_sat
1fa9f7c 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
deps: bump nightstream again (neo-application range check 'gadget')
5516b74 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
spec: tighten the phase <> opcode/action preconditions
8cb857f 
add a few more tests in test.qnt

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
circuit: add phase <> opcode + range checking
71dce68 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
Cargo.lock
470defe 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
prover: enforce method id matching on call -> enter
5c763d6 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
prover: enforce returned value matching on call -> return
046811d 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
prover: add sanity checker for terminal condition (still proving)
6ada28a 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
prover: wire coroutine id repr and resource resolution/curr control flow
335ce36 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
prover: use push_gated_linear_zero from neo_application's builder
9f9b4bb 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
quint spec: make register_method idempotent and more test coverage
c0134ab 
it makes it much easier to the circuit to just ignore a duplicated
registration than to forbid it, and it shouldn't change things
semantically (although performance may degrade)

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
prover: enforce enabled-method relation (register-method -> yield -> …
fe8695d 
…call-method)

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
spec: remove YieldBegin (triggered by context.resume) from utxo const…
c866ccd 
…ructor

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
prover: remove YieldBegin from constructor traces (spec match)
01f67de 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
spec: add test_method_call_without_resume_preserves_abi
f0e1cb0 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
prover: reject rows after root-level coord script return
cbd96dd 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
prover/spec: add more coverage method registration and multi-utxo traces
e3b3960 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
prover: add batched (fixed size) relation suppport
f7468c6 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
prover: add e2e test folding test (no memory)
56e9046 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
quint spec: change starstream-value to 4-limb field elements (opaque …
8df295b 
…repr) and add multi-block encoding

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
prover: add trace commitment binding logic to the circuit (and adjust…
a977e03 
… rust wrappers for quint changes)

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
(quint) spec: add tx input/output handling with init and finalize phases
dc79c2a 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
prover: implement tx phases io/binding (storage, abi sets)
d28ea7d 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
prover/spec: add transaction statement binding including comm commitm…
08a0e7c 
…ents

(limited to at most one coord script)

Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
prover: (wip) add proving (folding) api/entrypoint (no nebula)
9023f11 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini
cleanup: unify EventKind impls and extract tag() function
1a754e0 
Signed-off-by: Enzo Cioppettini <48031343+ecioppettini@users.noreply.github.com>
@ecioppettini ecioppettini self-assigned this Sep 17, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@ecioppettini ecioppettini

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@ecioppettini