Fix obsolete graph logic - #442
Merged
Merged
Conversation
eigmax
added a commit
that referenced
this pull request
Aug 24, 2026
* BitvmGC V2 (#403) * add bitvm gc msg * gc version init commit * gc update * add verfier contract support & set version to 0.4 * support multi hashlocks for wrongly challenged * Refactor: remove the attestation of the part_stark_vk * feat: add operator wrapper proof * Refactor: remove x_d * feat: commit operator_vk_hash on chain * remove unused constant * feat: update sequencer set hash query to use 'at or before' logic * feat: add operator_vk_hash to sequencer commands and update README * feat: add backward compatibility for operator and commit chain circuits * implement operator wrapper proof functionality * add fixed watchtower public key verification * add bitvm gc msg * gc version init commit * gc update * fix todo * use multi hashlocks * fix rebase * adapt to babe and sig * fix rebase * fix fmt and clippy * fix build * update rpc service * adapt babe state path to configurable env * Only the verifier and the operator need to initialize soldering_builder. * print operator wrapper vk hash during task creation * support bincode serialization for GOATMessage, add legacy JSON deserialization fallback * update BABE_M_CC to 7 * use `par_iter` to parallelize instance creation in babe_adapter * add support for soldering proof chunking, compact payloads, and parallelized setup expansion * implement soldering proof payload range requests * fix missing feature * add soldering upload functionality and deprecate range-based pull logic * allow external socket address override via env * remove soldering proof upload functionality, add s3 and local shared storage * update BitVM and Goat dependencies to new repository and branch * improve error handling in GOATMessage serialization, add JSON fallback on bincode failure * Only the GenCircuits message is encoded using `bincode`, and adds some logs * add BitcoinSPV support for posting single and batch block hashes, fix typo in error message * use the given goat_block_number instead of the one query from the db when init_genesis is true * gc-v2 * replace hardcoded input index with topology helpers * remove unnecessary check * gc-v2 init commit * gc-v2 * gc-v2 * gc v2 --------- Co-authored-by: Blake <blake.h@zkm.io> Co-authored-by: Blake <0xblake.sg@gmail.com> Co-authored-by: ethan <kslashhh@gmail.com> * update validate_pubin_disprove (#405) Co-authored-by: ethan <kslashhh@gmail.com> * Feat: Implement BitVM3 deferred binding. (#404) * build and broadcast operator commit pubin in handler. * change babe_adapter to adapt bitvm3-gc * use operator proof & adapt handler to bitvm3 partial binding. * adjust code after rebase * add tests for babe adapter * update validate_pubin_disprove (#405) Co-authored-by: ethan <kslashhh@gmail.com> * update assert sent verifier * update handle_challenge_assert_sent_operator * update deps --------- Co-authored-by: KSlashh <48985735+KSlashh@users.noreply.github.com> Co-authored-by: ethan <kslashhh@gmail.com> * remove wrapper proofs (#406) * remove wrapper proofs * remove operator vk hash from public inputs * bind graph watchtower public keys at runtime in operator proofs (#408) * fix some problem (#407) * fix musig2 problem * fix some problem * update timelock logic * add DisproveSent monitor * fix watchtower flow check logic * remove unused field/check * update deps --------- Co-authored-by: ethan <kslashhh@gmail.com> * Update operator assert logic (#409) * update operator commit witness * update handle * handle invalid assert extra-data * update goat deps --------- Co-authored-by: ethan <kslashhh@gmail.com> * Feat: validate assert witness in handle sent verifier. (#410) * adapt babe to newest change in gcs * change deps * Fix some problems (#411) * fix verifier check * fix sync graph check * fix endorse sig check * add check for graph sigs * update graph verify logic * fix nonstandard witness * update deps --------- Co-authored-by: ethan <kslashhh@gmail.com> * Fix/gc v2 debug (#412) * Increase max transmit size to 16 MB in gossipsub configuration * Update NODE_TESTNET_TIMELOCK_CONFIG values * Refactor BABE setup state management and soldering proof handling * Add ENABLE_BABE_SETUP_STATE_CLEANUP feature flag and monitor logic * Validate commitment count in GenCircuits setup package * adapt to lastest change of bitvm-gc (#413) * Dev fix (#414) * fix bin * fix prekickoff check & commit pubin logic * update validate graph logic --------- Co-authored-by: ethan <kslashhh@gmail.com> * Fix: handle empty watchtower challenge txids (#415) * audit: use tla+ to formally verify transaction graphs (#417) * fix: use tla+ to detect the graph update race * fix: use tla+ to detect the graph update race * fix: use tla+ to detect the graph update race * fix: use tla+ to detect the graph update race * fix: use tla+ to detect the graph update race * fix: use tla+ to detect the graph update race * fix: use tla+ to detect the graph update race * fix: use tla+ to detect the graph update race * fix: extract_tla_network_table * fix: extract_tla_network_table * fix: rustfmt crates/bitvm-gc/src/timelocks.rs CI's Rustfmt check was failing on the tla_model_matches_shipped_timelock_configs test added earlier - never ran cargo fmt locally since this crate can't be compiled in the dev sandbox (unrelated zkVM build dependency issue). rustfmt itself doesn't need the crate to build, only to parse, so `cargo fmt --all` applied cleanly. No logic changes. * revert: keep the TLA+ audit, revert the applied code fixes This branch is an audit pass: node/tla/*.tla proves several real races/ boundary bugs exist in the current code, and proves correct fix designs for each - but applying those fixes to Rust is separate work the team should review and land themselves, not something to ship silently inside an audit PR. Reverted to gc-v2 (git checkout gc-v2 -- <file>, clean revert since this branch never touched these files before this session): - node/src/utils.rs (update_graph_status_guarded / set_instance_presigned_guarded atomic-CAS guards) - node/src/scheduled_tasks/event_watch_task.rs (routing through the guard) - node/src/scheduled_tasks/instance_maintenance_tasks.rs (TOCTOU fix) - crates/store/src/localdb.rs (GraphUpdate/InstanceUpdate::only_if_status_in) - crates/store/src/schema.rs (reverse-pointer doc comments) - crates/bitvm-gc/src/timelocks.rs (validate_timelock_config strictness, testnet4 connector_d 34->35) Kept as-is: every node/tla/*.tla and *.cfg file - the formal proofs are the actual audit deliverable and remain accurate regardless of whether the fix is applied yet. Updated to stop claiming the reverted fixes are shipped: - README.md's TLA+ table: "current code" -> "current code (still buggy)" for the bug configs, "proposed fix (verified, not applied)" for the fix configs. Also added the MultiActorRace.tla/.cfg row, built after the table was first written. - node/README.md: "Resolved: ..." section reverted back to "Known gap: ...", now pointing at the verified-but-unapplied fix design instead of claiming it's live. - node/tla/GraphLifecycle.md: same current-code correction. - .github/workflows/ci.yml's tla-plus job: relabeled both steps (baseline+proposed-fix vs known-bug) to match, and added MultiActorRace.cfg to the must-pass set (it didn't exist yet when the job was first written). Verified locally before pushing: all 6 must-pass configs still pass, all 3 known-bug configs still fail as expected, cargo fmt --all -- --check is clean. * fix: clippy lints in babe_adapter.rs Pre-existing on gc-v2, never caught before because CI never ran against gc-v2-based PRs until this branch's pull_request.branches fix. Not related to any change in this audit. - too_many_arguments on verify_real_setup: #[allow], 8 semantically distinct crypto-verification params, not a design smell worth a breaking API refactor. - needless_borrow: &package -> package (package is already &CACSetupPackage). - unnecessary_unwrap: is_none()/unwrap() -> ok_or_else(...), same behavior. * fix: resolve remaining clippy lints in node crate (handle.rs, utils.rs) Pre-existing needless-borrow, clone-on-copy, collapsible-if, and needless-borrows-for-generic-args lints in code never touched by CI clippy until the gc-v2 PR-trigger fix. No behavior change. * audit: extend TLA+ round to InstanceBridgeOutStatus and MessageState races Two new confirmed races found while sweeping every remaining stateful enum in the codebase, each with a verified counterexample and a verified (not applied) fix design: - InstanceBridgeOutStatus: three independently-scheduled writers (RPC stale-upsert, GoatChain event watcher, maintenance monitor) can resurrect a terminal Claim/Timeout/Refund back to Initialize. node/tla/InstanceBridgeOutRace.tla - MessageState: upsert_message's unconditional ON CONFLICT DO UPDATE can resurrect a Cancelled message back to Pending and re-dispatch it after its graph already closed. node/tla/MessageStateRace.tla GoatTxProcessingStatus was also audited and found safe (causal ordering via on-chain proof requirement + a processing gate), with two unrelated lower-priority defects noted for follow-up. Also cross-checked against blake-pro/bitvm-node-formal-verification, an independent Ivy-based effort targeting the same source commit - complementary rather than overlapping coverage (see report). CI's tla-plus job and root README's spec table updated to include the two new specs. audit/TLAPlus-20260630.md is the full narrative report. No Rust behavior changes - audit-only branch. * audit: extend TLA+ round to the Bitcoin transaction graph's connectors Mapped every shared/bottleneck Taproot connector in the goat crate's peg-out transaction graph (not just ConnectorD, the original scope), looking for the same margin-race shape Finding 4 found there. - Finding 9 (new bug): ConnectorA (Take1 vs Challenge) has NO margin check anywhere in validate_timelock_config, unlike every other timelock field. Real shipped Regtest value gives a challenger exactly zero reaction margin - same coin-flip-boundary shape as the original ConnectorD/testnet4 finding. node/tla/Take1ChallengeRace.tla (+ Fixed.cfg design, verified) - Finding 10 (verification, not a bug): ConnectorF leaf 1 has two alternative "committee blocks Take2" spenders (Nack and CommitTimeout), but MultiActorRace.tla only proved the margin for one (Nack). Extended it with operator_commit's margin against ConnectorF using real shipped values - holds on all 4 networks, closing a verification-coverage gap (the Rust ensure_lt check was previously unverified at the TLA+ level). - ConnectorZ and AckConnector's un-covered leaves reviewed and found to have no CSV-margin structure to check (documented reasoning, no forced/artificial model). - Take2DisproveRace.tla's header updated to acknowledge ConnectorD's third leaf (PubinDisprove) - zero CSV, can't be slower than the already-proven-safe Disprove path, so no new model needed, but the header no longer implies it doesn't exist. CI's tla-plus job and root README's spec table updated. No Rust behavior changes - audit-only branch. * audit: refine report — fix stale cross-references and counts Tie Finding 4's connector_a observation forward to Finding 9 (same gap, discovered in two passes) instead of leaving it as a redundant, disconnected aside. Fix two positional counts ("seven"/"three of the seven") that went stale once Finding 9/10 were added after them. * ci: gate fmt/clippy/test behind tla-plus, fail fast on TLA+ failure tla-plus is the fastest job (seconds, no Rust toolchain build) and a failure there means either a real regression or a stale/broken spec - not worth burning 30+ minutes of Cargo Test/Clippy compute before finding out. Reordered it to the top of the file since it now gates everything else via needs:. * audit: dedupe shared TLA+ constants into GraphTopology.tla/ShippedTimelocks.tla Extract the two literal value-table duplications found across node/tla/: - AllStatuses/TerminalStatuses/AllowedTransitions (the real Graph.status state machine) was byte-identical across GraphLifecycle.tla, GraphLifecycleFineGrained.tla, and GraphLifecycleFineGrainedFixed.tla. - Networks/ProverConnector/ConnectorD/ConnectorF/MinReactionBlocks (and more) was byte-identical between Take2DisproveRace.tla and MultiActorRace.tla, with MinReactionBlocks also duplicated a third time in Take1ChallengeRace.tla. Both are now single-source-of-truth modules the relevant specs EXTEND, removing a real drift risk (already caught one: MultiActorRace.tla's comment said "shipped values" without noting ConnectorD is actually the post-fix value, inconsistent with Take2DisproveRace.tla's more careful "(post-fix)" annotation on the identical table). Also removed `EXTENDS FiniteSets` from 5 files that never used Cardinality/IsFiniteSet - dead imports. Net: 1033 -> 1000 lines despite adding 2 new files. Every one of the 15 spec+config combinations re-verified via TLC to behave identically to before (same pass/fail outcome, same state counts - e.g. GraphLifecycleFineGrainedFixed.cfg still finds exactly 132 states, matching the audit report's existing claim). No .cfg files touched; CI's working-directory: node/tla resolves the new EXTENDS targets the same way it already resolves everything else. Also strengthens Finding 8 with direct confirmation against the L2 Gateway.sol contract (KSlashh/bitvm-L2-contracts@2173b92, gc-v2): proceedWithdraw requires a Merkle-proven kickoff tx and is onlyCommittee-gated; finishWithdrawDisproved has its own on-chain AlreadyDisproved guard - confirming this report's races are about the local node's bookkeeping drifting from a well-guarded on-chain source of truth, not the L2 contract itself being unsafe. * ci: make tla-plus job fail while documented bugs remain unfixed Previously the "known-bug specs must still fail" step only failed CI if a bug config unexpectedly started passing (spec/code drift). That meant CI showed green despite 6 TLC-proven, unfixed findings still being present in the shipped code - a clean-looking pipeline hiding real, documented gaps. Now the step fails whenever ANY bug config correctly reproduces its finding (the normal, expected case right now), in addition to the original harder failure if one unexpectedly passes. Since fmt/clippy/ test are gated behind tla-plus, this intentionally keeps the whole pipeline red until each finding's verified fix design is actually applied to the Rust code - moving a bug config to the must-pass list (and its Fixed.cfg out of hiding) is how a fix "turns CI green" again. Verified the exact YAML-parsed script (heredoc dedenting etc.) end to end locally before pushing: correctly identifies all 6 open findings and exits 1. Updated the job's top comment and root README to explain this is expected, not broken. * audit: add fix-implementation guide (write-up only, no code applied) Companion to audit/TLAPlus-20260630.md, per request to generate fix suggestions without reversing this branch's audit-only stance. For each of the 6 CI-gated findings (1/1b, 2, 6, 7, 9) plus Finding 4: exact current code (verified against the real source, not from memory), exact suggested change, and why it implements the property the corresponding TLA+ spec proved. Cross-checked every referenced API against the real codebase before writing it down: - GraphStatus doesn't derive EnumIter, so the Finding 1/2 guard's allow-list is hardcoded from GraphTopology.tla's AllStatuses minus TerminalStatuses instead of a speculative .iter() call. - QueryBuilder::and_where_in already exists (crates/store/src/ utils.rs:77-92) and does exactly what the guard needs - used that instead of hand-rolling placeholder-building SQL. - InstanceUpdate is missing all 5 fields Finding 6b's fix needs (bridge_out_amount/goat_tx_hash/goat_tx_height/user_change_addr/ user_refund_addr) - called that out explicitly rather than waving it away as "add whichever are missing". No Rust source files changed. * ci: generate and print fix-suggestions report in CI instead of a committed doc Remove audit/fix-implementation-guide.md - per feedback, this branch stays audit-only with no extra committed artifacts; the fix guidance belongs in CI output, not a standalone file. The "Fail while documented bugs remain unfixed" step now carries a one-line fix direction + affected files per finding directly in its own script (cfg|tla|finding|files|hint rows) and, for each still-open finding, writes a formatted section to $GITHUB_STEP_SUMMARY (rendered as markdown on the run's summary page) in addition to the existing ::warning:: annotations - so anyone looking at a failed run sees exactly what to fix and where, without needing a separate file. Verified the exact YAML-parsed script end to end locally (including simulating $GITHUB_STEP_SUMMARY) before pushing. * ci: print per-finding fix guidance inline instead of a committed doc Follow-up to 29ef86a, which deleted audit/fix-implementation-guide.md but the actual CI script change didn't get staged in that commit (pathspec typo aborted the git add). This is that missing change. The "Fail while documented bugs remain unfixed" step now carries a one-line fix direction + affected files per finding in its own script (cfg|tla|finding|files|hint rows) and writes a formatted section to $GITHUB_STEP_SUMMARY per still-open finding, in addition to the existing ::warning:: annotations. * ci: print the entire fix-suggestions report, not just one-line hints The condensed per-finding hints weren't enough - print the full write-up (exact current code, exact suggested change, and why it implements the property the TLA+ spec proved, per finding) verbatim to both the raw log and $GITHUB_STEP_SUMMARY whenever any bug remains open. Content is the same detail level as the now-removed audit/fix-implementation-guide.md, just generated inline in the CI script instead of living as a separate committed file. The bug-detection loop is back to simple 3-field records (cfg/tla/ finding) since the fix text is no longer threaded through it - the full report is one static heredoc block printed once, not per-finding interpolation. Verified the exact YAML-parsed script end to end locally: correct exit code, full 298-line report written to both stdout and a simulated GITHUB_STEP_SUMMARY, byte-identical head and tail spot checks against the source content. * Dev fix (#418) * Use JSON for graph params hash * add verifier challenge tool * update log * fix tx-size-too-small * fix instance status transition * fix pegin queue * add sqlx cache * update timelocks * fix graph status transition * fix tla 3,6,7,9 * fix clippy --------- Co-authored-by: ethan <kslashhh@gmail.com> * ci: print how to reproduce each open finding, not the fix itself Replace the embedded 295-line fix-suggestions report with generic reproduction instructions: for each open finding, the exact TLC command to reproduce its counterexample locally, plus a pointer to audit/TLAPlus-20260630.md for the verified fix design. The fix content lives in one place (the report) instead of being duplicated in ci.yml where it would drift out of sync. Note: an earlier attempt at this edit used a fragile line-boundary search that matched the wrong closing `fi` and left corrupted duplicate content in the file. Caught before pushing, reset to the last-known-good commit, and redid the edit with exact asserted line boundaries. Verified the final YAML-parsed script end to end locally (correct exit code, clean warnings + step summary, no leftover content) before this commit. * ci: fix broken jar path in printed reproduction commands The repro string printed a bare `tla2tools.jar`, which only resolves if the jar happens to be in the caller's current directory - not where the setup instructions (root README.md) actually put it. Reported by the user copy-pasting a printed command and hitting "Unable to access jarfile". Fixed to the real path, ~/.local/share/tlaplus/tla2tools.jar, matching every other invocation in this workflow and the README. Verified the corrected command actually runs locally before pushing. * audit: update report — all 8 findings fixed and verified in commit 991faaa Every finding this audit formally proved (1, 1b, 2, 3, 4, 6, 7, 9) now has a "What actually shipped" note describing the real applied fix, verified against the actual diff (not the commit message) and, for the two timelock findings, re-checked with TLC using the real new shipped numbers. In several cases the shipped fix goes further than what this audit proposed (per-writer-source transition tables for Finding 1, extra idempotency/collision guards for Finding 6). Finding 8's two adjacent non-race defects were specifically checked and remain unfixed - called out explicitly rather than assumed. node/tla/ShippedTimelocks.tla updated to the real new Testnet4 values (connector_d 35->40, prover_connector 22->20, and others) - re-run through TLC, all properties still hold. Take1ChallengeRace.tla's ConnectorA deliberately left at its historical pre-fix value (a permanent regression-check record); header comments updated to explain this on both files. README.md's spec table reframed: "current code"/"proposed fix" -> "pre-fix code (historical)"/"fix design (applied in 991faaa)". No ci.yml changes - the must-pass/must-fail lists already correctly reflect this state (bug configs still fail against their unchanged historical constants, fix configs still pass against the real current numbers), consistent with CI being designed to keep the bug-reproduction configs as permanent regression checks. * fix: stop tla-plus CI job failing forever on already-fixed historical bugs The "fail while documented bugs remain unfixed" step was designed before commit 991faaa fixed all 8 findings; keeping it failing afterward served no regression-detection purpose (the bug configs' constants are frozen snapshots that never read the real Rust source) while permanently blocking CI. Only an unexpected PASS (a bug config no longer reproducing its counterexample) is a genuine drift signal now, so that's the only case that still fails the job - a config correctly still failing its historical counterexample is now just an informational note in the step summary. * docs: drop the independent Ivy cross-check section from the audit report Keeps the report focused on this audit's own findings; the comparison against the separate blake-pro/bitvm-node-formal-verification project was tangential to the report's purpose. * docs: renamem audit date * add sql cache (#419) Co-authored-by: ethan <kslashhh@gmail.com> --------- Co-authored-by: KSlashh <48985735+KSlashh@users.noreply.github.com> Co-authored-by: ethan <kslashhh@gmail.com> * Fix/flounder audit circuit (#416) * decode prev state from public values * fix(spv): remove latest_sequencer_commit_txid argument from watch_longest_chain * fix(vk): ensure Groth16 verifying key matches immutable vk * fix(vk): bind recursive proofs to authenticated ProgramId history * refactor(cli): make runtime inputs optional for print-only mode * refactor(commit-chain): remove operator_vk_hash and simplify commitment structure * refactor(proof-builder): unify `program_id` implementation * refactor(commit-chain): use hash to avoid the op_return length exceeding 80 bytes * fix clippy * refactor: remove legacy proof handling and improve public value deserialization * feat: add upgrade checkpoint hash to state/header chain and implement upgrade commit loading * fix some problems (#421) * fix commit pubin * add debug logs * add retry logic for pegin * add more retry logic for pegin * add regtest transaction flows tests * fix pubin-disprove tx too small * remove nst related code * feat: add metrics state * update goat deps --------- Co-authored-by: ethan <kslashhh@gmail.com> Co-authored-by: Blake <0xblake.sg@gmail.com> * Feat/pi blake3 (#422) * patch Ziren * add `imm-wrap-vk` feature * patch Ziren to use `blake3` branch * update `imm-wrap-vk` feature dependencies * update zkm-lib dependency to use the blake3 branch * fix some problem & refactor (#423) * add blake3 compile-time check * update timelock verify logic * add debug api for graph * add instance debug api & update graph debug api * add debug logs * add retry logic for p2p message * refactor(node): introduce durable heavy task dispatcher * add durable heavy-task leasing --------- Co-authored-by: ethan <kslashhh@gmail.com> * Refactor/bitvm (#424) * rename instances of 'bitvm2' to 'bitvm' across documentation and scripts * add validation for publisher key set * optimize `fetch_target_block` * fix: add full commit history validation and building functions * update install scripts * feat: implement API authentication with trusted public keys * add missing file * fix clippy * update cleanup_babe_setup_states (#425) Co-authored-by: ethan <kslashhh@gmail.com> * update deps (#426) Co-authored-by: ethan <kslashhh@gmail.com> * Dep/ziren v1.2.7 (#427) * Update Ziren dependencies to version v1.2.7 * Refactor get_sequencer_set_hash_from_db to simplify parameters and logic * Simplify CommitChainProofBuilder logic * update `bitvm-gc` * remove unused code * Get the valid watchtowers and operators from the GOAT contract (#432) * Update deployment scripts and configuration. (#433) * feat: dispatch ephemeral messages immediately (#434) * update deps to AES garbling hash feature. (#440) * fix node index (#441) * Fix obsolete graph logic (#442) * feat: make inbox/outbox batch size configurable * fix obsolete graph logic --------- Co-authored-by: ethan <kslashhh@gmail.com> --------- Co-authored-by: KSlashh <48985735+KSlashh@users.noreply.github.com> Co-authored-by: Blake <blake.h@zkm.io> Co-authored-by: ethan <kslashhh@gmail.com> Co-authored-by: Phạm Gia Việt Anh <vietanhpg2003@gmail.com> Co-authored-by: Stephen Duan <81497928+eigmax@users.noreply.github.com>
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.
No description provided.