Parallelize NDJSON analysis, Kani harnesses for vulnerable-contract, docs troubleshooting + CSS tests - #1487
Open
Smoothjane wants to merge 3 commits into
Open
Conversation
Closes HyperSafeD#1472 The batch JSON/SARIF path (run_analysis) was already parallelized with rayon's par_iter (Arc<RuleRegistry>/Arc<Analyzer>, one independent registry.run_all/analyze_ledger_size/scan_storage_collisions pass per file). stream_ndjson — the --format ndjson streaming path — still walked rs_files with a plain sequential for loop. Converts it to rs_files.par_iter().for_each(...), sharing the same Arc<RuleRegistry> across threads. Output is still written one file's findings at a time: Stdout::lock() from multiple threads simply blocks until available, so each file's findings stay contiguous on the page, just not necessarily emitted in directory-walk order — which is fine for NDJSON, since every line already carries its own "file" field and a streaming consumer doesn't depend on file ordering. Write errors from any worker thread are captured via a Mutex<Option<io::Error>> and surfaced after the parallel pass instead of being silently dropped (the sequential version's `?` on writeln!/flush inside the loop can't be replicated directly inside a par_iter closure, which can't return early from the enclosing function).
Closes HyperSafeD#1471 Extracts the vulnerable-contract's balance mutation (previously inline plain +/- in credit()/debit()) into pure functions (credit_pure/ debit_pure and their checked_add/checked_sub-based secure counterparts), following the same "Core Logic Separation" pattern contracts/kani-poc already establishes: Kani can exhaustively reason about pure u64 arithmetic with no Env/Host dependency, so the proof harnesses live in a #[cfg(kani)] module gated the same way kani-poc's are. Four harnesses (Z3 is Kani's default solver backend): - verify_credit_pure_can_overflow / verify_debit_pure_can_underflow prove a (balance, amount) pair exists that breaks each invariant (balance + amount <= u64::MAX, balance - amount >= 0) for the vulnerable, unchecked version — the exact bug class this contract exists to demonstrate. - verify_credit_pure_checked_rejects_overflow / verify_debit_pure_checked_rejects_underflow prove the checked_add/ checked_sub-based secure versions can never silently violate either invariant, for every possible u64 pair. vulnerable-contract's Cargo.toml already had `unexpected_cfgs = { check-cfg = ['cfg(kani)'] }` configured — evidence this crate was set up to receive a cfg(kani) harness that was never added. Note: a bare `#[invariant = "..."]` attribute (S011's SMT-backend annotation format, tooling/sanctifier-core/src/smt/invariants.rs) is not usable directly on this file — it's an unregistered attribute macro from Sanctifier's own text-scanning parser, not real Rust, so it breaks `cargo check` the moment it's placed on code that's part of the compiled workspace (verified locally: `cargo check -p vulnerable-contract` fails with "cannot find attribute `invariant` in this scope"). The Kani approach here achieves the same "explicit invariants a solver backend can analyze" goal without that conflict.
Closes HyperSafeD#1468, closes HyperSafeD#1473 HyperSafeD#1468 — adds a Troubleshooting section to docs/getting-started.md covering the errors a new user is most likely to hit while following that guide: cargo/rustc not on PATH after rustup install, missing wasm32-unknown-unknown/wasm32v1-none target, soroban-sdk build failures from an outdated toolchain, sanctifier binary not on PATH after `cargo install`, "No Soroban project found" path mistakes, stale-looking findings (the CLI re-reads from disk every run — a stale result almost always means the wrong path was scanned), and Z3/Kani solver timeouts (a timeout finding is not proof of a bug). Cross-links docs/kani-integration.md for the solver-timeout case. HyperSafeD#1473 — adds frontend/app/globals.css.test.ts. Since globals.css has no exported JS surface to import and happy-dom's CSS engine doesn't reliably compute cascaded custom-property values, these are structural/content tests over the raw stylesheet text (matching this repo's existing vitest + RTL convention, see app/components/ThemeToggle.test.tsx) rather than a rendered-DOM test. Covers: the file parses (balanced braces) and imports Tailwind; the dark: variant is wired to .dark (a regression guard for the exact failure the file's own leading comment warns about); light-theme --background/--foreground are defined and mapped into Tailwind's @theme inline block; the dark-theme override targets both [data-theme="dark"] and .dark and actually changes both colors (not a no-op copy) plus sets color-scheme: dark on <body>; the high-contrast mode defines every custom property the base theme uses plus primary/border/ring, using pure black/white/yellow; and every @Keyframes referenced by an animation utility class (animate-in, slide-in-from-bottom-3) is actually defined with both a start and end state — the edge case where a class references a renamed/removed keyframe, which CSS accepts silently with no animation rather than erroring. Note: could not run this suite locally to confirm a green pass — `npm install` in frontend/ fails in this environment on an EBADPLATFORM error for an optional dependency (@commitlint/message wants linux, this environment is darwin) unrelated to this change. The test follows the same vitest describe/it/expect structure and Vite path aliasing already used throughout frontend/app/components/*.test.tsx.
|
@Smoothjane is attempting to deploy a commit to the gbangbolaoluwagbemiga's projects Team on Vercel. A member of the Team first needs to authorize it. |
|
@Smoothjane Great news! 🎉 Based on an automated assessment of this PR, the linked Wave issue(s) no longer count against your application limits. You can now already apply to more issues while waiting for a review of this PR. Keep up the great work! 🚀 |
This was referenced Aug 27, 2026
This was referenced Aug 27, 2026
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.
Summary
Closes #1472
closes #1471
closes #1468
closes #1473.
#1472 — parallel processing. The issue pointed at
tooling/sanctifier-core/src/analyzer.rs,which doesn't exist — the batch JSON/SARIF analysis path (
run_analysisintooling/sanctifier-cli/src/commands/analyze.rs) was already parallelized with rayon'spar_iter.The
--format ndjsonstreaming path (stream_ndjson, same file) still used a plain sequentialforloop, so that's what this converts topar_iter().for_each(...), sharing the sameArc<RuleRegistry>across threads. Output is still written one file's findings at a time —Stdout::lock()from multiple threads just blocks until available — so each file's findings staycontiguous per write, just not necessarily in directory-walk order (fine for NDJSON, since every
line already carries its own
filefield). Write errors from any worker thread are now captured viaa
Mutex<Option<io::Error>>and surfaced after the parallel pass, since apar_iterclosure can't?-return out of the enclosing function directly.#1471 — formal verification assertions. Extracts
vulnerable-contract's balance mutation intopure functions (
credit_pure/debit_pureand checked-arithmetic counterparts), following the"Core Logic Separation" pattern
contracts/kani-pocalready establishes, and adds four#[cfg(kani)]harnesses proving the vulnerable versions can overflow/underflow and the secure versions never do,
for the invariants
balance + amount <= u64::MAX/balance - amount >= 0.Important scope note: I initially tried the
#[invariant = "..."]attribute formatS011's SMT/Z3 backend (
smt/invariants.rs) already parses, since the issue mentions "the Z3 solverbackend" — but that's an unregistered attribute macro from Sanctifier's own text-scanning parser,
not real Rust, and placing it on code in a compiled workspace member breaks
cargo checkoutright(verified locally:
cannot find attribute 'invariant' in this scope).vulnerable-contract'sCargo.tomlalready hasunexpected_cfgs = { check-cfg = ['cfg(kani)'] }configured, which isstrong evidence this crate was meant to receive a
cfg(kani)harness (Kani's default solver backendis also Z3) rather than the S011 annotation — that's the approach here, and it compiles cleanly.
#1468 — troubleshooting docs. Adds a Troubleshooting section to
docs/getting-started.mdcovering the errors most likely to come up while following that exact guide: PATH issues after the
rustup install, missing wasm targets,
soroban-sdkbuild failures from an old toolchain, "No Sorobanproject found" path mistakes, stale-looking findings, and Z3/Kani solver timeouts (not a bug proof).
#1473 — CSS tests. Adds
frontend/app/globals.css.test.ts. The file has no exported JS surfaceand happy-dom's CSS engine doesn't reliably compute cascaded custom-property values, so these are
structural/content tests over the raw stylesheet text, matching this repo's existing vitest + RTL
convention (
app/components/ThemeToggle.test.tsx). Covers Tailwind import + balanced braces, thedark:variant wiring (a regression guard for the exact failure the file's own comment warnsabout), light/dark theme custom-property definitions actually differing,
color-schemeon<body>,every high-contrast custom property, and that every
@keyframesan animation class referencesactually exists with both a start and end state.
Note on file pointers: two of the four issues' "File Pointer" links were stale —
frontend/styles/globals.cssis actually atfrontend/app/globals.css, andtooling/sanctifier-core/src/analyzer.rsdoesn't exist (the relevant loop is intooling/sanctifier-cli/src/commands/analyze.rs). Verified against the actual repo layout beforemaking changes.
Test plan
cargo check -p sanctifier-clipasses (rayon change)cargo check -p vulnerable-contractpasses (confirms the Kani module, gated behind#[cfg(kani)], doesn't affect normal compilation)cargo kani --harness verify_credit_pure_can_overflowetc. — not run (Kani not installed inthis environment); harnesses follow the same pattern as
contracts/kani-poc's existing,passing harnesses
npx vitest run app/globals.css.test.ts— not run;npm installinfrontend/fails in thisenvironment on an
EBADPLATFORMerror for an optional dependency(
@commitlint/messagewantslinux, this environment isdarwin) unrelated to this change