feat(sumcheck): add interaction protocol modules - #580

Draft

codygunton wants to merge 146 commits into

Verified-zkEVM:mainfrom

codygunton:cg/quang/core-rebuild-3-upstream

Commits on Mar 28, 2026

Bump CompPoly to latest upstream master (fe33688)
quangvdao
committed
27d04d4
Slim Bivariate.lean by importing CompPoly bridge modules
quangvdao
committed
7008657
Bump VCVio to latest master and drop redundant Q_ne_0
quangvdao
committed
cee9b7d
Slim Prelude.lean imports to avoid pulling in all of VCVio and Mathlib
quangvdao
committed
42f33c2
Address Gemini review: restore Q_ne_0, fix docstrings, add NoZeroDivisors
quangvdao
committed
01f9678
Merge branch 'main' into quang/bump-comppoly
quangvdao
authored
1641cf3
Fix linter warnings in Bivariate.lean
quangvdao
committed
cf58d7a
Add Interaction layer: Spec + RoleDecoration replaces ProtocolSpec
quangvdao
committed
0b39a78
Phase 3: Oracle verifier redesign with growing oracle access
quangvdao
committed
7835883
Role.Refine: centralize role-aware pattern matching for sender decorations
quangvdao
committed
6f2774b
refactor(Interaction): split Basic and TwoParty into submodules
quangvdao
committed
259c579
fix(Interaction): Spec.Decoration.swap for RoleDecoration dot notation
quangvdao
committed
5dea430

Commits on Mar 29, 2026

Commits on Mar 30, 2026

Commits on Mar 31, 2026

Commits on Apr 1, 2026

relax oracle continuation composition for FRI
quangvdao
committed
fff6693
add continuation-native FRI building blocks
quangvdao
committed
b6fcca3
document Lean notation and definition style
quangvdao
committed
3e7b288
prefer existing library combinators over bespoke wrappers

quangvdao
and
claude
committed
c2d56ff
add interaction-native boundary layer

quangvdao
and
claude
committed
f4c7e4c
add interaction-native boundary transport layer
quangvdao
committed
9ff60f7
document oracle execution helpers
quangvdao
committed
4e333cd
split boundary projection and lifting layers
quangvdao
committed
5f3272a
refine interaction security docs and signatures
quangvdao
committed
d0c3943
add interaction blueprint chapter
quangvdao
committed
e1e7bc2
rewrite interaction foundations motivation
quangvdao
committed
3c4c5b0

Commits on Apr 2, 2026

add generic interaction shape core
quangvdao
committed
c95ec52
add interaction-native fiat-shamir core
quangvdao
committed
a06d666
document interaction fiat-shamir transform
quangvdao
committed
c624573
rename decoration over and strengthen generic core
quangvdao
committed
d47b0cf
refactor interaction core around node contexts
quangvdao
committed
133a8b9
add schema bridge for node decorations
quangvdao
committed
0e7c627
extend schema decoration calculus
quangvdao
committed
3190fb6
add schema maps and context reindexing
quangvdao
committed
9c88d9f
add functorial laws for schema reindexing
quangvdao
committed
3bbb86a
extend schema maps and displayed transport
quangvdao
committed
5845eaa
add shape helpers for two-party cutover
quangvdao
committed
cbd343d
split interaction syntax from functorial shapes
quangvdao
committed
a9742ca
cut over two-party interaction types to syntax core
quangvdao
committed
8f9d0a2
cut over two-party execution to interaction core
quangvdao
committed
92deb0a
route counterpart family transport through shape core
quangvdao
committed
95741d0
promote role monad contexts in two-party layer
quangvdao
committed
8b427d6
make two-party sender nodes uniformly monadic
quangvdao
committed
08ab023
polish ownership syntax builder
quangvdao
committed
b1bee16
trim compose simp noise
quangvdao
committed
2411971
generalize passive two-party observations
quangvdao
committed
a35d0b6
propagate effectful passive observations
quangvdao
committed
3b746e4
adjust sumcheck interactions for effectful observations
quangvdao
committed
57aa966
keep sumcheck oracle fixed across rounds
quangvdao
committed
d1b183b
add stateful sumcheck oracle prover variants
quangvdao
committed
0e96281
remove stateless sumcheck residual sorry
quangvdao
committed
2aefe08
strengthen sumcheck oracle execution equivalence
quangvdao
committed
6819676

Commits on Apr 3, 2026

prune interaction alias surface and oracle umbrellas
quangvdao
committed
b8839ec
simplify boundary oracle context records
quangvdao
committed
5072524
trim two-party composition surface
quangvdao
committed
c9a164f
trim basic composition sugar
quangvdao
committed
5724d41
remove boundary oracle routing sorrys
quangvdao
committed
cb8ad34
split oracle continuation execution core
quangvdao
committed
2795c19
add raw boundary oracle pullback theorem
quangvdao
committed
73e0d8b
complete interaction round-by-round security proofs
quangvdao
committed
989d243
weaken pure composition soundness assumptions
quangvdao
committed
51fd362
move interaction soundness under verifier namespaces
quangvdao
committed
56f84e0
separate fixed and dependent oracle verifier APIs
quangvdao
committed
0158f32
remove fixed oracle verifier specialization
quangvdao
committed
11ebeeb
rework verifier soundness surfaces
quangvdao
committed
de02116
generalize oracle verifier input families
quangvdao
committed
662aa8f
document oracle continuation as specialization
quangvdao
committed
f9651fe
promote interaction core to input localstmt api
quangvdao
committed
03f3dc4
update fri and sumcheck for input localstmt api
quangvdao
committed
c9b0cd4
refactor(multiparty): cut over to local-view profiles
quangvdao
committed
e177fc2
refactor(oracle): canonize continuation-shaped core
quangvdao
committed
c3a0aed
refactor(proofsystem): cut over oracle protocol builders
quangvdao
committed
ae6de96
feat(interaction): add concurrent execution core
quangvdao
committed
75df074
refactor(interaction): align plain shared spine api
quangvdao
committed
0e02e66
feat(interaction): add concurrent trace semantics
quangvdao
committed
30288d9
feat(interaction): add concurrent trace policies
quangvdao
committed
0ae3e74
refactor(interaction): generalize composed statement input
quangvdao
committed
c56fce2
refactor(interaction): lift round-by-round security over shared input
quangvdao
committed
ef73c18
refactor(interaction): generalize state-chain statement input
quangvdao
committed
2a9f4db
refactor(oracle): rename shared-index bridge helpers
quangvdao
committed
447b248

Commits on Apr 4, 2026

feat(interaction): add dynamic concurrent process core
quangvdao
committed
1cae4e0
refactor(oracle): make security semantics behavior-first
quangvdao
committed
e0277ef
refactor(interaction): center concurrent execution on process
quangvdao
committed
57411fc
refactor(oracle): rename verifier languages
quangvdao
committed
57f1f15
refactor(oracle): rename oracleDeco parameters
quangvdao
committed
1c4ebe9
refactor(interaction): fix non-sorry linter warnings
quangvdao
committed
9baed01
Merge origin/main into quang/core-rebuild
quangvdao
committed
77463dc
chore(ci): enforce interaction warning budget
quangvdao
committed
0ace158
feat(concurrent): add run and liveness layers
quangvdao
committed
7e5c106
refactor(oracle): clean continuation composition constructors
quangvdao
committed
f2c02b2
theorem(oracle): extend theorem surface
quangvdao
committed
3bb2b03
feat(concurrent): preserve behavior under refinement
quangvdao
committed
3cab7ca
theorem(oracle): derive reified soundness bridge
quangvdao
committed
d111502
feat(concurrent): add bisimulation and equivalence
quangvdao
committed
c4eefbc
docs(interaction): expand concurrency notes
quangvdao
committed
4926202
docs(interaction): add bracha verification note
quangvdao
committed
87f0a3f
refactor(oracle): make append oracle transport structural
quangvdao
committed
48a4924
fix(interaction): clear remaining non-sorry warnings
quangvdao
committed
050fc40
docs(concurrent): clarify semantic docstrings
quangvdao
committed
831d4cb
refactor(concurrent): finish process-over cutover
quangvdao
committed
be709b4
feat(concurrent): add interface boundary primitives
quangvdao
committed
9873da4
feat(concurrent): add open composition laws
quangvdao
committed
989147d
feat(concurrent): add boundary equivalences
quangvdao
committed
21b0603
feat(concurrent): add equivalence-aware open laws
quangvdao
committed
c819710

Commits on Apr 5, 2026

fix(oracle): prove composed simulator bridge
quangvdao
committed
246a7fa

Commits on Apr 7, 2026

Commits on Apr 11, 2026

Commits on Apr 13, 2026

Commits on Apr 14, 2026

Commits on Apr 18, 2026

refactor(interaction): unify oracle counterpart rewriting via mapOracles
quangvdao
committed
f6093a6

Commits on Apr 30, 2026

Merge branch 'main' into quang/core-rebuild
quangvdao
committed
da43723
fix(lean): repair oracle merge fallout
quangvdao
committed
43a68c7
Merge branch 'main' into quang/core-rebuild
quangvdao
committed
eaa8c41

Commits on Jun 9, 2026

Merge upstream v4.30 dependency bump
codygunton
committed
17629f1

Commits on Jun 10, 2026

Update PR 10 for v4.30 dependencies
codygunton
committed
fd3923d
Update PR 11 for v4.30 dependencies
codygunton
committed
3d5c987

Commits on Jun 11, 2026