FEAT-084 (scry#126): interpret the i32 bitwise family through the proven bits domain - #156
Merged
Merged
Conversation
…ven bits domain i32.and/or/xor and constant-count i32.shl/shr_u get real interpret_op arms: interval -> BitsCong (sound approximation) -> the FEAT-037 domain's own transfer (mechanized admit-free in BitsCongruence.v) -> interval (sound projection). The headline case, `x & M` with M a non-negative constant, projects to [0, M] — tight enough for the in-bounds decision, so the masked-address idiom turns PROVEN-SAFE, and i32.and (433 fallbacks in the 468-module corpus) stops scrubbing whole functions to top. Sound by construction, never a false bound: - a sign-bit mask straddles 2^31 in the unsigned reading -> top; - a variable shift count -> top (count 0 leaves the value unbounded); - any operand shape outside the two justified conversions -> top for the RESULT only, never a function-wide degrade; - these ops write no locals/memory, so octagon (classify_store: Other -> forget) and the FEAT-058 memory domain are untouched. NOT modelled (still the honest unsupported-op fallback): the i64 bitwise family, i32.shr_s, rotl/rotr. Red-first: all six positive tests measured failing on unmodified main (PotentialTrap where ProvenSafe required); the negative tests (unbounding mask 0x1FFFF, sign-bit mask 0x80000FFF, variable shift count) pass before AND after — they encode the sound status quo the reduction must preserve. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc
…outstanding Status proposed -> implemented, with implementation-notes recording exactly what was modelled (i32.and/or/xor + constant-count shl/shr_u through the proven scry-sai-bits domain) and what deliberately was NOT (i64 bitwise family, i32.shr_s, rotl/rotr; variable shift counts and sign-bit masks push top for the result only). AC#4 — the corpus "modules where ALL memory accesses are provable" figure — needs avrabe's re-run and is named as the gap keeping this short of verified. rivet validate PASS (exit 0). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc
📐 rivet artifact deltaPR: #156 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
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.
Implements FEAT-084 (
artifacts/roadmap-v3.6.yaml, filed in #154): makei32.and— the top named operator behind the corpus unsoundness-fallbacks (433 of them; 97% of 468 real modules hit fallback, only 18% of memory-touching modules fully provable) — model-able insideinterpret_op, so a masked address gets an interval tight enough for the in-bounds decision.What is modelled
interpret_oparms fori32.and,i32.or,i32.xor, andi32.shl/i32.shr_uwith a constant count, each a round-trip through the PROVEN known-bits × congruence domain (scry-sai-bits, FEAT-037, mechanized admit-free inproofs/rocq/BitsCongruence.v):interval →
BitsCong(only two justified conversions: an i32 singleton → the exact constant; a non-negative interval → known-0 high bits) → the domain's own transfer (and/or/xor/shl/shr_u— no mask reasoning reimplemented) → interval (sound projection of the unsigned[umin, umax]; a range straddling 2^31 projects to ⊤).The headline case
x & M(M a non-negative constant) projects to[0, M], so the bounds-check idiom proves, andi32.andstops scrubbing whole functions to ⊤.What is deliberately NOT modelled
i32.shr_s,rotl/rotr— still take the honestunsupported-opfallback.x & 0x8000_0FFF): the unsigned range straddles 2^31; result is ⊤. i32 is sign-agnostic — a negative M does NOT bound x above by M in the signed reading.unsupported-opgap is removed only for the five operators genuinely modelled.classify_store→Other→forget) and the FEAT-058 memory domain are untouched — no lockstep change needed.Red-first evidence (measured on unmodified main)
All six positive tests written first and run against unmodified code — actual failure, quoted:
(6 failed on main: masked/downstream/or/xor/shl/shr_u; the 3 negative tests passed on main, as they encode the sound status quo.) After the change: 9/9 pass.
Negative tests (the ones that keep this honest)
feat084_unbounding_mask_stays_potential_trap—x & 0x1FFFF(reaches 131071 ≥ 65536) stays POTENTIAL-TRAP.feat084_negative_mask_stays_potential_trap—x & 0x80000FFFstays POTENTIAL-TRAP.feat084_variable_shift_count_stays_potential_trap—x >> ystays POTENTIAL-TRAP..expect(...)), so none can pass vacuously.Mutation checks (each mutation run, confirmed red, reverted)
I32Andarm (fall back to unsupported path) → the 5 and-dependent tests go red;shr_u(noand) and all negatives stay green.hi: umax→hi: umin) → killed by exactly and onlyfeat084_unbounding_mask_stays_potential_trap(falsely proves[0,0]) — the negative test alone catches an implementation that over-claims.feat084_negative_mask_stays_potential_trap.Local verification (by exit code)
cargo test -p scry-sai-core -p scry-sai-viz→ exit 0 (123 + 37 pass, 0 failed; no regressions)cargo clippy -p scry-sai-core -p scry-sai-viz --all-targets -- -D warnings→ exit 0cargo fmt --all --check→ exit 0rivet validate→ exit 0 (PASS; the newimplementation-notesfield is INFO-level, same pattern asresidualon FEAT-074..077)python3 tools/claim-check.py→ exit 0 (7/7 claims hold)Verified locally only — CI has not been observed on this branch and no claim is made about it.
Not verified here (named honestly)
implemented(notverified) until that lands, whichever way it goes.🤖 Generated with Claude Code
https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc