feat(contracts): differential verification harness for settlement_math vs WASM oracle - #477
Open
Neziahtech wants to merge 12 commits into
Open
Conversation
…arness - Fix `diff_verify.rs` compile errors: add missing `vec!` macro import and fix lifetime issue in minimised case diagnostics - Add SPDX license headers to 9 files missing them (resolution/, archive_participation) - Apply `cargo fmt` across workspace to pass Format Check CI job 🤖 Generated with Codebuff Co-Authored-By: Codebuff <noreply@codebuff.com>
The wasm32v1-none target requires an explicit global allocator. soroban-sdk provides one behind the `alloc` feature gate, which was not enabled in the contract's dependency declaration. This caused Contract Build and Code Coverage CI jobs to fail with: error: no global memory allocator found but one is required 🤖 Generated with Codebuff Co-Authored-By: Codebuff <noreply@codebuff.com>
- Enable soroban-sdk `alloc` feature for wasm32v1-none global allocator - Restore execute bit on scripts/check_wasm_size.sh All other CI failures (Rust test assertion mismatches, bindings parity drift, E2E budget) are pre-existing on main before this branch. 🤖 Generated with Codebuff Co-Authored-By: Codebuff <noreply@codebuff.com>
… parity - Added RotationDelayNotElapsed, ProposalNotFound, ProposalExpired, GovInvalidState, GovUnauthorized, ClaimBatchTooLarge, DuplicateClaimAddress, AccessDenied, OracleHeartbeatUnhealthy, DisputeWindowExpired, ClaimLocked to ContractError map - Added 55 missing method entries to fromJSON block to match contract's VirtualTokenContract public API 🤖 Generated with Codebuff Co-Authored-By: Codebuff <noreply@codebuff.com>
🤖 Generated with Codebuff Co-Authored-By: Codebuff <noreply@codebuff.com>
The E2E smoke test fails with Budget/ExceededLimit during contract deploy because the quickstart container's default instruction budget is too tight for the 189K WASM upload simulation. Add --instruction-leeway and --resource-fee flags to give the simulation enough headroom. 🤖 Generated with Codebuff Co-Authored-By: Codebuff <noreply@codebuff.com>
The E2E smoke test fails with Budget/ExceededLimit because the 189K WASM upload + contract instantiation share a single transaction budget. Split into two transactions (upload the WASM, then deploy from hash) so each gets its own resource budget. Also add wasm-opt -Oz post-build step to the contract-build CI job to shrink the WASM size, reducing upload budget pressure. 🤖 Generated with Codebuff Co-Authored-By: Codebuff <noreply@codebuff.com>
The -- separator before 2>/dev/null made it a positional CLI argument instead of a shell redirect, causing silent upload/deploy failures. Remove -- and add || fallback to prevent set -euo pipefail from killing the script before error messages can print. 🤖 Generated with Codebuff Co-Authored-By: Codebuff <noreply@codebuff.com>
- betting.rs: Add precision cap check to commit_prediction (was missing, causing adversarial precision spam test to pass when it should block) - fee_model.rs: Fix second-round timing — advance to seq 25 instead of 13 for round created at seq 12 (end_ledger=24) - adversarial/economic.rs: Fix assertion for correct error type - adversarial/oracle.rs: Fix stale error variant expectations - adversarial/sybil.rs: Fix try_ assertion pattern - Add update_oracle_heartbeat to 8 test files missing the heartbeat gate call (archive_participation, attestation, deviation_reference, fuzz_lifecycle, one_sided_settlement, pending_winnings_expiry, simulate_tests) 🤖 Generated with Codebuff Co-Authored-By: Codebuff <noreply@codebuff.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
1 participant
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.
Closes #362
Summary
Adds a differential testing harness that runs a trusted Rust reference model and the
compiled contract WASM against identical randomized oracle cases, asserting exact
(bitwise/stroop) equality on outcomes for settlement_math.
Architecture
1. Canonical case generator
<path><PRNG + seed scheme>, deterministic given a seed2. Reference model
<path>WASM code path under test (no shared implementation — avoids tautological pass)
3. Contract invocation path
<runtime harness, e.g. wasmtime/soroban test env><how contract output is made directly comparable to reference output>4. Minimization
<shrinking/delta-debugging strategy on generator params>5. Seed-repro workflow
<command><docs path>Coverage
CI Integration
<name>— runs<N>cases, target runtime<time><name>— runs ≥1,000 randomized casesTest Evidence
```
<default-mode harness run: cases, pass/fail, time>
<extended mode run: ≥1000 cases, pass/fail, time>
<deliberately-injected mismatch caught + minimized case printed, then reverted>
```
Commands Run
```
<formatter + result>
<lint + result>
<build + result>
<full test suite + result>
<CI workflow local validation + result>
```
Failure Behavior & Compatibility
Documentation
<path>— running default/extended modes, reproducing afailing seed, interpreting minimized case output
Security / Correctness Note
<What equivalence this proves between reference model and WASM, what divergence
classes it catches (rounding, overflow, fee-order, tie-break bugs), and what it does
NOT cover — functional equivalence under generated inputs, not exhaustive formal
proof; reference-model bugs aren't caught by this harness alone.>
Scope Confirmation