Open
Conversation
Co-authored-by: lisandrasilva <lisandrasilva18@hotmail.com>
coverage info for it
verifyInteropMessages fuzzing
timestamp instead of randomly assigning to them.
and it's easier to work with)
Hand testing.T logger to Interop for debugging
Build a five-layer pipeline that enforces the Supernode invariants from
overview.md under a single stable ID catalog (SPEC.md). Every layer cites
the same I1..I12 / T1..T5 / A1..A5 identifiers so a failure in any layer
is greppable back to the specification.
Layers:
1. Dafny formal models (dafny-models/SupernodeState.dfy,
SupernodeView.dfy). AllInvariants over an abstract SupernodeState
datatype (LogsDB, DenyList, Verified) with predicates I1..I11 and
I12_InitialStateSatisfiesInvariants lemma. Types.dfy gains
BlockWithLogs, DenyListEntry, IsParentOf. Supernode.dfy's three
{:axiom}-ensured abstract methods (applyRewindPlan, sameL1Chain,
resolveFrontierVerificationView) are replaced with trivial no-op
stubs; axioms removed, postconditions now proven. Dafny 4.11.0
verifies 66 / 0 errors.
2. Go invariants package (invariants/invariants.go, snapshot.go).
Structured *Error type carries the SPEC ID in every failure;
CheckAll composes with errors.Join. Covers the structural
invariants (I2, I4, I5, I6, I7, I8, I10, I11).
3. Environmental oracle (invariants/env.go). Env interface +
CheckAllWithEnv for the hybrid invariants I1, I3 (initiating
message existence + Tarjan cycle detection), I8-ancestry, I9.
4. Reference model + fuzzer (invariants/reference_model.go,
fuzz_test.go). Pure Go ApplyAdvance / ApplyInvalidate / ApplyRewind
matching SPEC T3/T4/T5. FuzzReferenceModel drives the model with a
stateful byte sequence. Fuzz immediately surfaced an A4 precondition
gap (ApplyAdvance silently accepted denied blocks); fixed by
rejecting at the reference-model boundary. 2.9M executions over
30s with zero violations.
5. Runtime assertions (invariants/runtime_on.go, runtime_off.go).
Build-tagged Assert / AssertWith / SetPanicOnFailure /
SetFailureSink / AssertionFailureCount. Zero-cost no-ops in
release builds; full checks under -tags=supernode_invariants.
Bridge + trace corpus:
- invariants/bridge.go: StateView interface and SnapshotFrom lifter.
Pull-based design decouples the package from the Supernode class
(no import cycle) and avoids needing a whole-state enumeration API
on interop.LogsDB or chain_container.DenyList, which is blocked on
upstream changes tracked in SPEC.md §5 items 13-18.
- invariants/trace.go: Trace JSON format with steps + expected
failures. TestTraceCorpus replays testdata/traces/*.json. Three
canonical traces generated by TestRegenCanonicalTraces.
Tooling:
- justfile targets: verify-dafny, verify-invariants-go,
verify-invariants-go-tagged, fuzz-invariants (FUZZTIME env var),
regen-traces, and verify-invariants which runs all of them as a
single CI gate.
- CLAUDE.md documents the five layers and the stable-ID contract.
- SPEC.md §5 open-items list tracks Step 2c / 3c follow-ups (real
applyRewindPlan, LogsDB / DenyList enumeration APIs, Supernode-side
adapter wiring).
Verification:
$ just verify-invariants
Dafny: 66 verified, 0 errors
Go: ok (default)
Go: ok (-tags=supernode_invariants)
Fuzz: 2.9M executions, 0 failures, 85 interesting inputs retained
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…w documentation Adds `overview.md` detailing the Supernode's architecture, components, state management, cross-validation logic, and assumptions on L1/L2 chains. Includes a mermaid diagram for visualizing relationships and a breakdown of invariants.
…s in `chain_fuzz_utils.go`
…ultichain fuzzing - Introduced CheckI7_NoHigherL2Block for validating no L2 block exists with timestamp ≤ verified timestamp beyond the expected head (I7 hybrid clause). - Improved I9 checks to ensure DeriveL1 results are ancestors of the verified L1 inclusion, fully validating "minimal covering" constraints; reorg-safe by verifying BlockID equality. - Optimized I3 acyclicity detector with an iterative DFS to prevent stack overflows. - Added `cloneVerifiedSlice` and `cloneBlockWithLogsSlice` for deep-copying snapshot slices safely. - Enabled multichain state-machine fuzzing (`FuzzReferenceModelMultiChain`) to test I3, I6, and I9 paths under cross-chain interactions. - Updated `justfile` fuzz target to run both single-chain and multichain fuzzers. - Augmented test coverage with regression tests for new I7 and I9 constraints (`TestCheckI7_`, `TestCheckI9_` cases). - Addressed SPEC.md gaps for I3 LogIdx validation and traced new assumptions in §5 item 19. - Enhanced runtime assertion logic: explicit failure sink, improved nil handling, synchronization for thread safety.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Builds the five-layer invariant verification pipeline for op-supernode (Dafny → structural Go → environmental Go → reference model → fuzz → build-tagged runtime assertions). Single source of truth:
op-supernode/invariants/SPEC.md.See
SPEC.md §6 Change logfor the per-step diff (Step 1 → Step 6). Highlights:dafny-models/SupernodeState.dfywithI1–I11predicates,I12_InitialStateSatisfiesInvariantslemma,SupernodeView.dfybridge layer. 66 verified, 0 errors.Snapshotmirroring the Dafny datatype, structuralCheckI2/I4/I5/I6/I7/I8/I10/I11, env-oracle hybridCheckI1/I3/I7-env/I8-env/I9, andCheckAll/CheckAllWithEnvcomposition.ApplyAdvance/ApplyInvalidate/ApplyRewind(T3/T4/T5).FuzzReferenceModel(single-chain) andFuzzReferenceModelMultiChain(cross-chain executing messages, exercising I3 acyclicity and I9 plumbing).Assert/AssertWithbehind thesupernode_invariantsbuild tag; zero-cost no-op in release builds.invariants/testdata/traces/*.json, replayed byTestTraceCorpus.Review fixes (this push)
Following the PR review pass:
CheckAllWithEnvviaCheckI7_NoHigherL2Block. The previously orphanedEnv.HasHigherL2BlockAtOrBelowis no longer dead.BlockID(not just.Number) and to require every per-chainDeriveL1be an ancestor of the recordedL1Inclusion. Two distinct L1 blocks at the same height after a reorg no longer pass.findExecMsgCycleis iterative with an explicit DFS stack so deep exec-msg graphs cannot blow the goroutine stack and panic the supernode under runtime assertions.Assertzero-value fast-path removed soActivationTS == 0is no longer silently skipped.SetFailureSinkis mutex-guarded;trace.collectIDsuseserrors.Asso wrapped errors in joined trees are still discovered.CloneSnapshot,StaticStateView.Verified, andStaticStateView.LogsDBFor— every map and inner slice is now caller-owned per the doc string.ApplyInvalidatededuplicates so T4 is idempotent.FuzzReferenceModelMultiChainadded — runs two L2 chains in lockstep with cross-chain executing messages, exercising I3 acyclicity, I6 monotonicity under multiple chains, and I9 plumbing. ~2.1M execs in 30s, 0 violations.LogIdxmodeling gap (state-local check ignoresLogIdxbecauseBlockWithLogsonly stores executing messages).Out of scope (deferred)
SPEC.md §5items 13–18 — supernode-side adapter (StateView→ live Supernode) plumbing. Blocks on:EnumerateSealed(from, to)toop-supervisorlogs DB (item 13).ForEachtochain_container.DenyList(item 14).*supernode.Supernode → *interop.Interopaccessor or type-assertion bridge (item 16).SnapshotFromfromprogressAndRecordafterapplyPendingTransition(item 17).Verification
The
just fuzz-invariantsrecipe was updated to run both fuzz targets sequentially (Go's-fuzzaccepts only one target per invocation).Test plan
just verify-dafny— 66 / 0just verify-invariants-go— passjust verify-invariants-go-tagged— passFuzzReferenceModel30s — ~2.6M execs, 0 violationsFuzzReferenceModelMultiChain30s — ~2.1M execs, 0 violations