Two-phase SMT abstraction for symbolic division/modulo and multiplication by gustavo-grieco · Pull Request #1075 · argotorg/hevm

gustavo-grieco · 2026-06-22T07:29:24Z

Combines the two stacked proof-of-concept PRs into a single branch against main, for easier review:

[PARKED] Use uninterpreted functions for 2-phase solving approach #996 — uninterpreted div/mod for two-phase solving
[PoC] Abstract symbolic multiplication (abst_evm_bvmul) for vault-style verification #1073 — abstract symbolic multiplication (stacked on [PARKED] Use uninterpreted functions for 2-phase solving approach #996)

Together they add an opt-in SMT arithmetic abstraction (--abstract-arith) that lets hevm prove multiply-then-divide properties — vault share prices, swap quotes, fixed-point math — that otherwise never return because the solver bit-blasts a 256-bit symbolic multiplier/divider.

The problem

For symbolic a, b the only decision procedure SMT has for a * b / a / b over (_ BitVec 256) is bit-blasting: a full 256×256 multiplier (~10^5 gates) or a divider, per operation. Multiply two unknowns and divide by a third — the shape at the heart of vault accounting — and the query explodes (unknown/OOM).

The approach (two phases)

Abstract bvmul/bvudiv/bvsdiv/bvurem/bvsrem over symbolic operands with uninterpreted functions (abst_evm_*), so the solver never bit-blasts them.
Constrain with only sound facts:
- div/mod is refined against the native op via an absolute-value + shift-bound + congruence encoding (unsigned results exact; signed reconstructed from magnitudes).
- multiplication is kept fully uninterpreted (no ground truth) plus a catalogue of sound algebraic lemmas: commutativity, 0/1 identities, mul/div/divisor monotonicity, the div–mul link (a/b)*b ≤ a, mulDiv bounds, and the constant-scaling family — const-cancellation (c1·x)/c2 == (c1/c2)·x, fraction-reduce, nested-division collapse, ceilDiv-cancel, and scaled-product telescoping.

Soundness

Every lemma is true of ordinary arithmetic, so anything proved from them holds for the real operations (in effect you prove the property about a more general contract and the deployed one is a special case). Because abst_evm_bvmul has no ground truth, a satisfying model may assign it values real multiplication never would — so SAT is downgraded to Unknown whenever an abstract product is present (hasAbstractMul); the abstraction never reports a false counterexample.

Structure

The lemma machinery lives in three modules so the lemmas are reviewable in one place:

EVM.SMT.AbstractBase — SMT primitives, signed helpers, the div/mod taxonomy, term collectors/matchers, and saturate (closes the set of div/mul terms the lemmas range over).
EVM.SMT.AbstractLemmas — the lemma catalogue: a LemmaInst sum type, collectLemmas (triggers), and emitLemma (SMT emission + per-lemma soundness note), one banner per lemma; GHC exhaustiveness ties each constructor to its emitter.
EVM.SMT.DivModEncoding — orchestration (mulEncoding) + the div/mod ground-truth encoding.

Usage

Opt-in via hevm test --abstract-arith (off by default); also drivable through echidna's verification mode.

Validation

Representative properties prove under --abstract-arith (const-cancel, scaled const-cancel, fraction-reduce, nested-div, mul/div monotonicity, mulDiv bound, telescoping), and deliberately false identities correctly fail, confirming no lemma over-fires. The abstraction has been used to verify the full stateless conversion math of a production vault (Spark PSM3) and a large subset of the ABDK Math 64.64 property suite.

Supersedes #996 and #1073 (left open for now).

Try it on a real target: spark-psm

The Spark PSM3 verification mentioned above is public and wired for one-command repro, so it is easy to experiment with and without the abstraction on real production code:

git clone --recurse-submodules -b symbolic-conversion-proofs https://github.com/gustavo-grieco/spark-psm
cd spark-psm    # needs foundry + bitwuzla on PATH, and hevm built from this branch

# all ~60 prove_* properties, with the abstraction (~30 min; most prove in seconds)
make verify-hevm

# one property or a family, by name regex
make verify-hevm M=prove_convertToAssets_susds
make verify-hevm M=roundtrip

# the same queries WITHOUT the abstraction: mul/div bitblast natively and the
# nonlinear properties come back unknown instead of PASS
make verify-hevm M=roundtrip HEVM_FLAGS="--solver bitwuzla --smt-timeout 300 --max-iterations 5000"

make verify-hevm runs forge build --ast followed by hevm test --root . --match "<M>" --solver bitwuzla --abstract-arith --smt-timeout 300 --max-iterations 5000; set HEVM=/path/to/hevm to pick the binary. Every prove_ assumes only the abstraction's operand budget, require(x <= type(uint128).max) per input. The properties in test/symbolic/ProveOriginals.t.sol delegate to the repo's unmodified testFuzz_* functions, so what is proven is Spark's own test content; test/symbolic/README.md documents the full property set, the lemmas each one exercises, and the eleven known-out-of-reach cases.

🤖 Generated with Claude Code

The 2-phase refactor's sendScript requires every command to return "success", which the empty solver (no-op process, no print-success) can't satisfy, so it failed before check-sat; the merge from main added SMT content that exposed this. Short-circuit EmptySolver in getOneSol to return Unknown with the same message main produces (and that the 'empty solver is always unknown' CLI test expects). The 'maybe it got killed' diagnostic stays on the real error paths. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Extend the abstraction+refinement div/mod encoding to unsigned Div/Mod, mirroring the existing signed (SDiv/SMod) path: - Declare abst_evm_bvudiv / abst_evm_bvurem uninterpreted functions and route Div/Mod through divModOp so they honor AbstractDivMod (the concrete path stays byte-identical via op2CheckZero). - Split DivModKind into signed/unsigned variants so the absolute-value and sign-reconstruction machinery is never applied to unsigned operands, and signed/unsigned groups never share a congruence pool. - For unsigned, the magnitude is the raw operand (no smtAbsolute) and the reconstruction is just the EVM divide-by-zero guard around the result var. The ground-truth axiom is zero-guarded (ite (= b 0) 0 (bvudiv a b)) to match EVM's x/0 = 0 semantics, since SMT-LIB's native bvudiv/bvurem return non-zero on a zero divisor. Add unsigned tests to the Abstract-Arith group, including a vault-preview-shares example (ERC-4626-style (assets << 64) / price) that the shift-bounds encoding proves instantly but native bvudiv leaves at "unknown". Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Extend the arithmetic abstraction to multiplication, so vault-style properties involving symbolic*symbolic products become provable while keeping hevm SOUND. Encoding (src/EVM/SMT/DivModEncoding.hs, src/EVM/SMT.hs): - Route only symbolic*symbolic Mul through an uninterpreted abst_evm_bvmul (concrete/0/1/power-of-two factors stay native). No mul ground truth, so the solver never bit-blasts a symbolic product. - Sound lemmas only: commutativity; 0/1 identities; div x mul link (quotient*divisor <= dividend); div monotonicity; and mul monotonicity guarded by a bound-free no-overflow predicate (high half of the 512-bit product is zero). Bounding (e.g. require(x < 2**128)) is supplied in Solidity, not hardcoded here. Soundness (src/EVM/Solvers.hs): - A QED is a real proof (the lemmas over-approximate real EVM arithmetic). - Because abst_evm_bvmul is uninterpreted, a SAT model may use product values inconsistent with real multiplication, so a counterexample cannot be trusted: when the mul abstraction is active, SAT is downgraded to Unknown. div-only counterexamples (div is exact via its ground truth) are unaffected. Tests (test/test.hs, group "Mul-Abstraction"): mul monotonicity, 0/1 identities, div x mul link, ERC-4626 share-price monotonicity (QED with abstraction, unknown natively); plus soundness cases: unbounded overflow must not yield a bogus QED, the cross-divisor round-trip's spurious model must not be reported as a counterexample, and div/constant-mul counterexamples remain reported. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Extends the set of vault-style properties the multiplication abstraction proves, beyond plain monotonicity. Both lemmas are sound (true of real EVM arithmetic) and were each validated to unlock their target via the CLI. - Division anti-monotonicity in the divisor: y1 <= y2 && y1 != 0 => x/y2 <= x/y1. Unlocks divisor-ordering ("a cheaper price gives at least as many units"). - mulDiv bound: for (x*y)/z, if y <= z (or x <= z) then the result is <= x (resp. <= y), guarded by no-overflow of x*z (resp. y*z). Unlocks the common DeFi pattern, e.g. a fee of feeBps/10000 never exceeds the principal. A third lemma (multiplication cancellation, m(x,z)<=m(y,z)=>x<=y) was tried and reverted: it does not help bound-style properties such as (x*s)/s <= x, because the abstract product is unpinned, so the division result is unbounded and the no-overflow guard never discharges. Those need the product pinned (i.e. bit-blasted), which the abstraction deliberately avoids. Soundness is unchanged: QED remains a real proof, and properties that the lemmas cannot discharge (or that are false) stay Unknown rather than producing a bogus proof or counterexample. Tests (group "Mul-Abstraction"): div-divisor-monotone, muldiv-fee-cap (QED), and muldiv-fee-uncapped-not-unsound (must stay Unknown). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

CI (solc 0.8.31) canonicalises `a * b` with the shared operand FIRST (e.g. Mul (SLoad slot) (ReadWord arg)), whereas solc 0.8.2 put it second. mul-monotonicity paired products by a shared *second* operand only, so under the 0.8.31 ordering the lemma was not generated, the abstraction could not prove the property, and the spurious model was (soundly) downgraded to Unknown — making `vault-shares-monotonic` fail with "expected QED, got Unknown". Fix: feed both operand orders into the monotonicity pairing (multiplication is commutative and we already assert it, so the generated term links back to the one in the props). The division lemmas remain order-sensitive, as they must. Verified on the exact failing CI bytecode: now QED (was Unknown); full local regression unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Two changes that let realistic vault queries (operand magnitudes ~2^100, e.g. token amounts up to 1e30) prove in seconds instead of timing out: 1. mulNoOverflow now uses the cheap *sufficient* condition `x <= 2^128-1 && y <= 2^128-1` instead of the exact bound-free predicate `extract 511 256 (bvmul (zext x) (zext y)) = 0`. The exact form forced the solver to bit-blast a full 512-bit multiply for every lemma instance, which was the dominant cost: monotonicity over operands bounded by 2^96+ timed out, while 2^64 proved instantly. The sufficient condition is sound (when it holds there is genuinely no overflow) and is the same width-budget idea Halmos uses. All realistic token amounts, share counts and conversion rates are far below 2^128. 2. New const-mul monotonicity lemma (mkConstMulMono): for a literal constant c, `x <= y => c*x <= c*y`. Multiplication by a constant stays a native bvmul, but a symbolic operand times a large constant (e.g. 1e27 in sUSDS rate conversions) is still costly to bit-blast and compare. Since c is concrete we compute the exact no-overflow bound floor((2^256-1)/c) at encode time, so the guard is a single constant comparison. This is what unblocks `value * 1e27 / rate`-style conversions, which div-monotonicity could not close without first ordering the two const-mul dividends. Adds a constmul-div-monotone test mirroring spark-psm convertToAssets(sUSDS). Existing Mul-Abstraction tests are unaffected (the 2^128-bounded ones discharge the cheap guard exactly; soundness tests stay Unknown/Cex). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

When an abstract product a*b has a factor that is also used as a divisor elsewhere in the query, synthesize the exact division (a*b)/factor and add it to the div set. The existing sound lemmas then bridge nested divisions: mulDiv-bound gives (a*b)/b <= a, and div-monotonicity carries that bound across a shared divisor. This proves the cross-divisor round-trip convertToAssetValue(convertToShares(x)) <= x, i.e. ((x*ts)/ta)*ta/ts <= x — the stateless core of inflation-attack safety — which single-level lemmas could not discharge (the bridging term (x*ts)/ts was simply absent from the query). Soundness: the synthetic terms are exact EVM divisions and every lemma asserted about them is a true fact, so a QED remains a real proof. Verified that the downgrade-soundness checks (mul-overflow-not-unsound, muldiv-fee-uncapped) still report Unknown and the counterexample tests still report Cex — the added lemmas are consistent (an inconsistency would have turned those into spurious QEDs). The former roundtrip-spurious-cex-suppressed test now proves the property, so it becomes the positive roundtrip-no-inflation test; downgrade soundness stays covered by the two *-not-unsound tests. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

The round-trip (cancellation synthesis) and the const-mul-div monotonicity (large 1e27 constant multiply) are reliably discharged by z3 but not by bitwuzla. Both solvers are sound; this is purely a capability pick. Since withBitwuzlaSolver runs with no SMT timeout, an unprovable-for-bitwuzla query would hang the test rather than fail fast, so prefer the solver verified to close these. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

…e round-trip Reverts the round-trip and const-mul-div tests from z3 back to bitwuzla. The earlier switch was made when bitwuzla was missing from the local PATH and every query spuriously returned unknown; with bitwuzla actually present it discharges all of these in well under a second (and is the bit-vector solver hevm defaults to). On the checked-arithmetic round-trip bitwuzla is in fact the *stronger* solver — z3 is the one that struggles there. Adds roundtrip-checked-realcode: the inflation-attack round-trip on real-code- shaped Solidity — ordinary checked arithmetic (so each `*` carries the 0.8 overflow guard div(mul(a,b),a)) and the conversions are real functions called as in the contract. Confirms the cancellation synthesis survives the overflow-guard divisions, i.e. the property proves on the code as written, not only on raw assembly ops. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

…t test - Reword the no-overflow guard comment in generic terms (large operands ~2^100) instead of naming specific token/amount domains. - Drop the spark-specific note from the const-mul-div test comment. - Remove the redundant roundtrip-checked-realcode test: roundtrip-no-inflation already covers the cross-divisor round-trip; the cancellation synthesis still discharges Solidity's overflow-guard divisions (described in the encoding). No functional change to the abstraction; comments and test surface only. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Multiplication by a literal constant stays a native bvmul, but the surrounding division is abstracted (uninterpreted), so a divide-by-the-same-constant wrapper like `amount * 1e18 / 1e18` (e.g. ERC-4626 precision scaling) is not provably the identity. This lemma pins it: for a division (c*x)/c by the same literal c, assert the result is x, guarded by the exact no-overflow bound floor((2^256-1)/c) computed at encode time (a single constant comparison, like const-mul-mono). Sound: (c*x)/c == x exactly whenever c*x does not overflow, which the guard ensures. The lemma only fires when the divisor literal equals the multiplier literal, so a near-miss like (x*1e18)/(1e18+1) is left uninterpreted (verified: it still yields a counterexample, not a spurious QED). Adds a const-cancel test. This discharges constant-precision wrappers in isolation; it does not by itself close the largest composite queries (e.g. a full previewDeposit/convertToAssets round-trip), where the surrounding structure remains beyond the solver. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Two sound lemmas that discharge precision-scaling closed forms (exact-value spec-conformance), which the abstraction otherwise leaves uninterpreted: 1. Generalize const cancellation from (c*x)/c == x to (c1*x)/c2 == (c1/c2)*x when the literal divisor c2 divides the literal multiplier c1 (c2 | c1). The same-constant case (c1==c2, k=1) is unchanged; the general case covers lossless scaling between decimals, e.g. amount*1e18/1e6 == amount*1e12. Guarded by the exact no-overflow bound floor((2^256-1)/c1). 2. Nested-division collapse: (A/c1)/c2 == A/(c1*c2) for literals c1,c2 whose product fits in 256 bits. A floor identity, sound unconditionally; collapses chained constant divisions like x*rate/1e9/1e18 to x*rate/1e27. Both verified sound (correct form proves; a wrong constant yields a counterexample, never a spurious QED) and non-regressing. Adds const-cancel-scaled and nested-div-collapse tests. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Mirror of the generalized const-cancel (which needs c2 | c1): this covers the c1 | c2 direction (multiply by a small constant, divide by a large one), e.g. x*1e6/1e18 == x/1e12 -- precision scaling DOWN (the convert-to-usdc step). Sound because, under the no-overflow guard x <= (2^256-1)/c1, c1*x is exact and floor(c1*x/(c1*k)) = floor(x/k). Adds fraction-reduce and fraction-reduce-cex unit tests. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

The ceilDiv sibling of const-cancel. OpenZeppelin Math.ceilDiv(c1*x, c2) is (c1*x == 0) ? 0 : (c1*x - 1)/c2 + 1, so the abstracted divide is over the (c1*x - 1) dividend. When c2 | c1 the product is always a multiple of c2, so ceil == floor and the whole ceilDiv collapses to (c1/c2)*x. The lemma pins the inner divide: for x >= 1, (c1*x - 1)/c2 == (c1/c2)*x - 1 (sound: c1*x = c2*m*x, floor((c2*m*x - 1)/c2) = m*x - 1), under the encode-time no-overflow bound floor((2^256-1)/c1). Discharges round-up multiply-up swap-out closed forms (e.g. previewSwapExactOut usds->usdc == amountOut*1e12). Adds ceildiv-cancel and ceildiv-cancel-cex unit tests. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

…e div set Two related additions to the multiplication abstraction: 1. Scaled-product telescoping (sound, no-overflow guarded): for products sharing a factor a whose other factors differ by a literal k that the common divisor c divides, floor(a*b/c) == floor(a*(b-k)/c) + a*(k/c). This is the only lemma that relates two DISTINCT abstract products, so it discharges value-change accounting identities such as susds*rate/1e27 - susds == susds*(rate-1e27)/1e27 (rate and rate-1e27 otherwise give unrelated abst_evm_bvmul terms). Sound because a*b = a*(b-k) + a*k and a*k is an exact multiple of c, shifting the floor by exactly a*(k/c). Validated: SMT soundness (m=1 and m=2) and wrong-RHS rejection, plus necessity/efficacy against the existing lemma set. 2. Collapse a nested constant division (A/c1)/c2 into a synthetic single divide A/(c1*c2) added to the div set, so the single-divide lemmas (telescoping, const-cancel, fraction-reduce) match code that splits precision across two divides — e.g. _getSUsdsValue's x*rate/1e9/1e18, whose collapsed x*rate/1e27 is what those lemmas key on. Sound: nested-div-collapse already asserts the two forms equal, so the synthetic divide is exact. Additive (never removes a term), so it cannot introduce a false QED. Tests: scaled-product-telescope (QED) and scaled-product-telescope-not-unsound (wrong difference stays Unknown, never QED) in the Mul-Abstraction group. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Split the 624-line DivModEncoding into three modules, following the EVM.Expr simplifier idiom (pattern-directed rules + per-constructor emit), so the lemmas live in one reviewable file: - EVM.SMT.AbstractBase: shared SMT primitives, signed helpers, the div/mod taxonomy, term collectors/matchers, and `saturate` (the abstract-term closure that was tangled in mulEncoding's `let`). - EVM.SMT.AbstractLemmas: the lemma catalogue and review surface. A `LemmaInst` sum type, `collectLemmas` (triggers), and `emitLemma` (SMT emission + soundness notes), one banner per lemma. GHC exhaustiveness now forces every constructor to have an emitter, replacing the old silent positional concat. - EVM.SMT.DivModEncoding: slimmed to orchestration (mulEncoding) plus the div/mod ground-truth encoding. Behavior-preserving: emitter bodies are verbatim and the emission order is unchanged, so generated queries are identical. Public API unchanged. Validated: lib + exe build clean (GHC 9.6.6); seven representative lemma properties (const-cancel, scaled const-cancel, frac-reduce, nested-div, mul-mono, mul-div-bound, telescope) prove under --abstract-arith, and a false identity correctly fails, so soundness is preserved. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

msooseth · 2026-06-24T13:42:12Z

Ah, thankfully the majority of the LoC change is in test.hs, I was getting extremely worried for the +1000 LoC.... 😆

msooseth

My light review :) First of all, this is very-very cool! I just wanna make sure I can read it all and understand it all, so we can merge!

I think most of the things I highlighted could be fixed via LLM relatively easily? I hope at least! Basically, stuff I think can be maybe trimmed down? Perhaps the SMT helper functions could be extracted to another module, and shared? And the lemmas should be checked if they are all needed. I'd like to make sure only to review the ones that are needed :) They are hard to check so I wanna economise on my time :) Perhaps an LLM can figure out which ones are absolutely necessary and then we can review those only :)

Review feedback on #1075: sp/zero/one/wordAsBV now live once in EVM.SMT.SMTLIB (re-exported by EVM.SMT, so downstream imports are unchanged); the abstract UF declarations sit under a single comment; obvious comments removed and wordy ones tightened across AbstractBase, AbstractLemmas and DivModEncoding, keeping the per-lemma soundness notes. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Conflicts: hevm.cabal (keep both text and vector in the test/rpc-tests build-depends), cli/cli.hs and src/EVM/Effects.hs (keep both maxDynSize from main and abstractArith from this branch). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

gustavo-grieco and others added 30 commits February 17, 2026 17:10

proof of concept of of div-encoding

038d31a

axioms

536e063

avoid unsoundness

0513779

fixes and tests

b687ca8

fixes

113a25a

Update src/EVM/SMT/DivEncoding.hs

f3e103e

fixes

3d995ed

Remove warning

21cd753

Cleanup

e73af5a

Cleanup

45b71c5

Rename, lineup

8716a51

Fix code repetition

f4d7fdf

Cleanup

e60173a

Waaay cleaner setup

df399c6

Update cabal

81d2690

Less obvious comments

e03cd05

Cleanup

1c48980

Cleanup

1dad96c

Cleaner

c3112cd

Cleanup

40bd88c

Cleanup

d9c5089

Cleanup

d1f5333

Cleanup

d24dfdd

Cleanup

7554795

Update

ce537e1

Cleanup

d20beeb

Fixing

b07ee28

assertProps is now abst+axioms+refine

de82732

Update

3ad2715

Proper 2-phase

6816fc9

gustavo-grieco and others added 19 commits April 30, 2026 18:42

Merge branch 'main' into poc-div-encoding

7f991f6

Merge remote-tracking branch 'origin/main' into poc-div-encoding

63b6538

Merge remote-tracking branch 'origin/main' into poc-div-encoding

1eac9d3

This was referenced Jun 22, 2026

[PoC] Abstract symbolic multiplication (abst_evm_bvmul) for vault-style verification #1073

Closed

[PARKED] Use uninterpreted functions for 2-phase solving approach #996

Closed

gustavo-grieco added 3 commits June 22, 2026 14:32

Add uint256 abstract mul regression

81a6588

reduced code

d5ae200

reduced code

6349a3a

msooseth requested changes Jul 6, 2026

View reviewed changes

gustavo-grieco and others added 4 commits July 20, 2026 18:36

Merge origin/main into arith-abstraction

b3db09a

Conflicts: hevm.cabal (keep both text and vector in the test/rpc-tests build-depends), cli/cli.hs and src/EVM/Effects.hs (keep both maxDynSize from main and abstractArith from this branch). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Merge remote-tracking branch 'origin/main' into arith-abstraction

52c9f66

Merge branch 'main' into arith-abstraction

06b5bf4

Navigation Menu

Uh oh!

Two-phase SMT abstraction for symbolic division/modulo and multiplication - #1075

Two-phase SMT abstraction for symbolic division/modulo and multiplication#1075
gustavo-grieco wants to merge 157 commits into
mainfrom
arith-abstraction

gustavo-grieco commented Jun 22, 2026 •

edited

Loading

Uh oh!

msooseth commented Jun 24, 2026

Uh oh!

msooseth left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

gustavo-grieco commented Jun 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

The problem

The approach (two phases)

Soundness

Structure

Usage

Validation

Try it on a real target: spark-psm

Uh oh!

msooseth commented Jun 24, 2026

Uh oh!

msooseth left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

gustavo-grieco commented Jun 22, 2026 •

edited

Loading