catch / 4

Updated: native exit/abort SimProcs ARE now safely registered (commit 7cd3d7431). Required honoring no_return in both native dispatchers — see invariant-no-return-deadend. Supersedes the no-native-exit-simprocs memory which warned against registration.

angr-nt4q (commit 23f1d1016, 2026-05-25): RustStateProxy.memory.store NotImplementedError documented as a deferred limitation, not implemented. Reason: rust_proxy_writes_design.rst (existing design doc) evaluated proxy-backed register/memory writes (Option A) end-to-end and recommended Option C (status quo). Measured per-callback diff-and-push cost: 1-14 ms; aggregate at most ~7% wall on the fastest bench, <1% on the rest. Risk surface (plugin substitution) is the same class that 'avoid-state-copy-optimization' caught silently regressing ais3 3s->11s. Reopen conditions: callback density 10K+/bench OR angr-2k64 (per-state plugin restoration) revives Option A as a prerequisite. The bead's 'common Python angr idiom (mutate memory in a hook)' framing was mismatched: proj.hook() routes to SimProcedure which DOES get a full SimState (memory.store works via diff-and-push); the proxy is only used for find/avoid predicates and inspect BPs where mutation isn't idiomatic.

angr-okca (StateId newtype for exploration/) is a single ATOMIC refactor of 419 non-comment state_id sites across 8 files, NOT incrementally splittable. Unlike borb.1/memory/Address (self-contained: addresses defined+keyed inside memory/), the state-id identifier is DEFINED in state.rs (next_state_id/state_id()->u64), STORED in stash.rs (StashManager.state_roots: HashMap<u64,u64>, set_root/get_root/find_state keyed on u64), and ENTERS exploration/ via PyO3 pymethods as u64. An exploration/-only StateId newtype thus needs conversions at BOTH edges (Python-in via FromPyObject, stash.rs-out via .raw()) with type safety only in the thin middle. Doable in address.rs style (FromPyObject extracting u64 lets pymethods take StateId directly; .raw() at stash edges) but the all-or-nothing nature + slow cargo-only rebuilds (venv pip broken) make it unfit for a single capped loop iteration. Recommend: do off-loop in one focused sitting, OR re-scope borb's StateId half to land StateId in stash.rs+state.rs together (more correct home than exploration/).

RustOomError exists in the Rust exception hierarchy (errors.rs:63) but is currently only raised by an explicit test hook at engine.rs:312 ('oom' test variant). Real Rust allocation failures via Vec/Box default to alloc::handle_alloc_error which ABORTS the process in cargo release profile — not propagate through PyO3 as RustOomError. Python-side MemoryError DOES propagate normally through the FFI boundary. Documented in docs/advanced-topics/rust_engine.rst 'Memory pressure and OOM > Behavior on exhaustion' (angr-zidj, commit c714e9e15). Implication: if we want graceful Rust-side OOM recovery, need to switch to fallible allocations (Vec::try_reserve etc.) and surface them through RustExecError::Oom — not a trivial refactor.

run_single.py was running in-process with no memory isolation — OOM-killed Claude orchestrator on 8GB/0-swap machine. Fixed: now uses multiprocessing.spawn with RLIMIT_AS=4GB. run_comparison_10.py reduced from 6GB to 4GB limit. Loop prompt forbids running run_comparison_10.py entirely.

op0dn ralph-sizing review (2026-07-11): every moonshot bead audited against the ralph-iteration constraint (1 agent, <=1h, tree clean+committed). Rubric: right-sized = one seam, one deliverable, crisp gate, ~1-3 iterations; too big = bundles independent deliverables, mixes investigation with productization, or carries an unresolved design fork. RESULT: 32 beads unchanged; 9 split into 19 children (E1 .1.1/.1.2; E2 .2.1/.2.2; S-C1 .6.1/.6.2; S5 .11.1.1/.11.1.2; B9 .11.2.1/.11.2.2; HC-2 .12.2.1/.12.2.2; M6.5 .14.1.1/.14.1.2; M6.3 .14.4.1/.14.4.2; M6.4 .14.5.1/.14.5.2); Bug M1 drain-on-cancel extracted to .13.8 (kill-proof, was buried in .13.3/.13.6); ype54 rewritten + split into ype54.1 decision spike / ype54.2 fix (guard-serialization refuted, see avoid-ype54-guard-serialization). Umbrella parents retyped to epic so ralph does not claim them (bd rejects task->epic dep edges; spike gates therefore point at terminal verdict LEGS: .6.2, .11.1.2). PREMISE CORRECTIONS found: E2 wiring already DONE (NativeLibVEXLifter fully wired behind libvex-ffi; NativeVEXLifter in vex/lifter.rs is a dead stub — E2 is verify+promote); E1 stepper exists (step_state_with_skip pub(crate)) — E1 is pyo3 exposure + extra_stop_points + proxy stubs. Borderline beads .11.5/.13.4/.9.2 left whole with stall-split notes (user decision). HUMAN GATE: angr-75mc (xmllint) blocks S6+S7; PR staged at tools/upstream_patches/angr_examples_xmllint_solve_symex.patch — needs the user to file it cross-repo.

vex/ops_tests.rs split (angr-9hleg): the 5288-line monolithic test file is now 14 by-family ops_tests_.rs siblings + shared ops_test_helpers.rs. Design that worked: helpers (pack_lanes_, unpack_lane, assert_lanes, eval_v128/i64/i32, make_v128_lane0*, pack_4xf32/2xf64/2xf32_64) hoisted to ops_test_helpers.rs as pub(super) fns with 'use super::'; each family file does 'use super::' (reaches ops private items via the child-of-ops rule) + 'use super::ops_test_helpers::*' ONLY when it uses a helper (else unused-glob warns under -D). FCmpKind import lives ONLY in ops_tests_float_cmp.rs. Module decls in ops.rs are '#[cfg(test)] #[path=...] mod tests_'. Split was scripted (brace-match on ^}$, classify by fn-name prefix); 188 tests, all green under 'cargo test vex::ops'.

angr-otjw spike (2026-05-20) ranked SimProcedure Python-fallbacks across 14 benches with callback_count>0. Top contributors: __libc_start_main (50 calls, 3 benches — ais3_crackme=47, sym-write=2, csgames2018=1); ReturnUnconstrained (26, 2 benches — angr generic catch-all); fwrite (22, csgames2018); fflush (14, 2 benches); my_scanf (13, defcon-baby-re — user-named binding). Aggregation script at tests/benchmarks/collect_simproc_fallbacks.py (committed 59ded1c93). Follow-ups: angr-yrhh (libc_start_main native), angr-70no (fwrite/fflush/setvbuf), angr-ilsr (audit symbolic-arg fallbacks). KEY: ais3_crackme's entire 47-callback budget is __libc_start_main; killing that fallback drops ais3 to 0 callbacks. strcpy_find has 0 fallbacks despite 97-callback budget — all native dispatch.

P15 conservative-fork fallback in stepping.rs (lines 524-545 and 1198-1207, identified 2026-05-31 angr-95up.2): when a deferred fork lacks both a stored condition AND a reconstructed condition, the 'else' branch creates a fork via successors[0].fork() to explore the target without a constraint. This DOES clone the Z3 solver (state.fork() at state.rs:1672-1708 invokes solver.borrow().fork()) but does NOT increment solver_fork_count. So solver_fork_count is a structural UNDERCOUNT of actual solver clones for the rare P15 path. Fix is small — add 'self.profiling.accumulated_stats.solver_fork_count += 1' inside the P15 else-branch in both stepping.rs locations, profiling-gated to match the other sites. Not fixed in angr-95up.2 (task was documentation-only); leave a bead if drift becomes a measurement problem. Code search anchor: 'P15: Missing condition for deferred fork'.

P1b bounded-harness pass (angr-9w6ad.2) results — 15 benches, rust engine, 100s timeout, 3500MB cap (driver /tmp/p1b_driver.py, raw /tmp/p1b_results.jsonl). OUTCOMES: OK(3)=hackcon2016_angry-reverser 26.8s, tumctf2016_zwiebel 56.9s*, 0ctf_trace 27.7s. TIMEOUT(6)=sharif7_rev50, 0ctf_momo_3, hitcon2017_sakura, asisctffinals2015_fake, defcamp_r200, CADET_00001. OOM(1)=insomnihack_aeg (~92s MemoryError@3500MB). FAIL(5). FAIL buckets: (a) unsupported SimOption NotImplementedError SYMBOL_FILL_UNCONSTRAINED_REGISTERS — fast-fail, NOT a perf bug: b01lersctf2020_little_engine, whitehat_crypto400, simple_heap_overflow. (b) 'IndexError: list index out of range' — REAL rust-engine bug, actionable: asisctffinals2015_license (0.4s fast-fail), ekopartyctf2015_rev100 (84s fails LATE). Z3-vs-engine split (OK benches via counters-json): angry-reverser ~84% Z3-bound (z3_check_time_ns 22.6s of 26.8s) -> P2c profiling target is Z3 not engine; 0ctf_trace ~0 z3/engine timing counters (tracing/concrete path, symbolic engine barely exercised); zwiebel BIMODAL (56s under driver, TIMEOUT@180s on standalone re-run). CATALOG DRIFT: hitcon2017_sakura rust_ok=True but TIMES OUT@100s (stale-optimistic); zwiebel notes '~2.5h' but sometimes finishes ~1min (bimodal, overly pessimistic).

RustMemoryProxy.store() (angr/exploration/rust_state_proxy.py) unbounded-symbolic-address fallback (angr-p1s02, commit 58daadb20): when state_memory_store_symbolic_multi returns not-ok (address has too many/zero satisfying solutions, e.g. an unconstrained operator new/malloc return pointer with a 0x7fff.. high prefix), the store NO LONGER raises NotImplementedError. It concretizes the addr via self._mgr.fork_state_solver(state_id).eval(addr) (angr's Max write-concretization strategy) and re-issues the store with a concrete claripy.BVV addr through the SAME state_memory_store_symbolic_multi entry point (its concrete fast path -> store_concrete_automap). KEY GOTCHA: store_concrete_automap in native/angr/src/memory/store.rs is MISNAMED -- it does NOT auto-map; it errors on unmapped non-lazy pages so Python can handle the store. So a concretized garbage high page (0x7fff00000000) still fails -> the fallback SILENTLY DROPS it (matches AVOID_MULTIVALUED_WRITES + observable gate-off outcome: nobody reads back a garbage pointer) rather than raising, keeping the SimProc state alive. New counter mgr._stats_proxy_mem_symbolic_addr_fallback (stats key proxy_mem_symbolic_addr_fallback). Fixed csaw_wyvern gate-on regression (3.66s vs gate-off 3.59s, was 0.86s dead). flareon2015_5 still regresses under the gate with a SEPARATE SimUnsatError (angr-xs4rj), so callback-memory-proxy default-on is STILL not fidelity-safe. Diag method: temporarily print addr/eval/eval_upto in the not-ok branch, run ANGR_RUST_USE_CALLBACK_MEMORY_PROXY=1 run_single.py --engine rust.

Page::clear_symbolic(offset, size) added to native/angr/src/memory/page.rs: clears symbolic_bitmap bits in [offset, offset+size) WITHOUT touching the data buffer, and drops the bitmap allocation when empty (matches the in-line block inside store_concrete). Use this when you've already lost wider-sym tracking and need to reclassify orphaned symbolic bytes as concrete — NOT when you want to actually overwrite data (use store_concrete for that). Sister method to mark_symbolic. Only public method for clearing arbitrary bitmap ranges as of 2026-06-03.

angr-panhl.1 Phase-0 kill-gate RESULT = PASS (proceed to Increment 2 angr-panhl.2 RustBV::translate_into). Profiled with the work-stealing migration model (see parallel-migration-model): Z3-bound trio all clear the gate -> hackcon2016_angry-reverser 710ms/task 0 migr, securityfest_fairlight 319ms/task 0 migr, ekopartyctf2016_sokohashv2 173ms/task 0 migr (all >100ms/task AND <10 migr/bench). GIL/callback fraction tiny everywhere (0.2-1.3%). State-heavy unmapped_analysis is fine-grained (39.6ms/task, 1 migr) so that class would NOT amortize cross-thread translate cost - but only >=1 favourable target class needed. Coarse-task low-migration shape confirmed for the Z3-bound class. Full table in bd note on angr-panhl.1.

angr-panhl.2 (parallel kill-gate Increment 2) RESULT = PASS-leaning GO (2026-06-23, commit e4033ac0e). Cross-context RustBV translate measured at 355 ns/node / 709 ns/leaf-translate on a 64-byte memory-load-shaped tree (Reverse(Concat(64 BVS))) — WITHIN the 390-677 ns/node synthetic spike, far from the 10x kill ceiling. CRITICAL favorable finding: only Symbolic LEAVES do Z3_translate; Expression nodes rebuild lazily (near-free), so real-state translate cost scales with LEAF count not total AST nodes — better than the spike's per-node assumption. Both panhl.1 (migration cadence) + panhl.2 (translate_into) now PASS. Remaining before reopening angr-1ilq (Phases 3-5): whole-state translate_state + real-trio capture = follow-up angr-ahypj. See [[translate-into-primitive]], [[panhl1-killgate-pass]], [[parallel-go-nogo-panhl]].

panic=abort is set in workspace [profile.release] (Cargo.toml:33, commit 493b67547, 2026-06-02). Implication: Rust panics no longer cross the PyO3 FFI boundary as catchable PanicException — they SIGABRT the Python process. Tests / external code that previously caught PanicException via 'except BaseException' will now see process death. None of the 661 existing tests broke; only documentation references PanicException (lines 7316, 13319 of test_rust_exploration.py are historical commentary, not assertions). The subprocess-style test_unknown_pipeline_name_fails_fast at line 8857 accepts either non-zero exit OR Exception/Error in stdout, so both unwind and abort paths satisfy it. Dev/test profile is unchanged — only release builds (pip install -e .) get panic=abort, so cargo test still uses unwind.

panic-audit-2026-05-03: After 2026-04-20 audit + 72 commits, native/angr/src has 509 unwrap() calls but only 4 in production code (rest inside #[cfg(test)]). All 4 fixed in commit 9192bc506. Verification command: 'awk "/^#[cfg(test)]/{in_test=1} in_test==0 && /.unwrap()/{print FILENAME":"NR}" file.rs'. Codebase is and remains well-disciplined about error handling — test-bound unwraps dominate the count.

RustBV::to_u128() (panicking as_u128().expect) was removed in angr-j60q0.1; use as_u128()->Option instead. The 3 prod callers degrade gracefully: memory/store.rs::store_concrete returns new MemoryError::UnexpectedSymbolic (concrete path is is_symbolic-guarded so unreachable, defense-in-depth); state/mod.rs::memory_load + exploration/pending_api.rs::_get_pending_memory return PyValueError. PITFALL when hardening the symbolic/ value->concrete panics: the value_z3.rs FPA NULL .expect sites (item 1) CANNOT be cheaply converted — to_z3_ast/to_z3_ast_cached return z3::ast::BV (not Result) and ripple to solver.rs+claripy_bridge; split to angr-j60q0.3.

Panic-hardening pattern (angr-j60q0.2): in vec_float dispatch, kept the dev-time debug_assert AS a tripwire AND added a graceful Err return for release. Two distinct gaps: (1) unreachable!() arms in elem/kind match expressions — replace with _ => return Err(...) (the ! of return unifies with the arm's value type, so no signature change needed; lane.rs uses InvalidFloatType(elem), scalar.rs uses UnsupportedVectorOp(format!)). (2) a debug_assert!(arity <= FLOAT_LANE_OP_MAX_ARITY) guarding fixed-size buf32/buf64 arrays indexed by arity — promote to a real if arity > MAX { return Err } BEFORE the loop, since over-arity is an index-panic abort even in release. No InvalidIR/InvalidArity variant exists in OpError (ops.rs:1589); use UnsupportedVectorOp(String) for arity/kind, InvalidFloatType(IRType) for elem.

Parallel 2-worker A/B ship-gate (angr-1ilq.5) FAILED (iter69). Measured RUST_PARALLEL_WORKERS=1 vs 2 via run_single subprocess on the retargeted gate corpus: cmu_binary_bomb_partial 1.42s->2.25s (1.58x SLOWER), codegate_2017-angrybird 3.68s->4.46s (1.21x SLOWER), CADET_00001_partial (high-width stress) 7.75s->did-not-finish-in-150s across 3 attempts (>19x/hang, SIGTERM not OOM). Gate needed >=1.5x speedup at 2 workers; got net regressions everywhere. Do NOT ship parallel default-on. Signal: translate_state-on-steal + per-worker Z3 context overhead dominates at these widths; codegate w=2 main-proc peak_mem collapses 2049MB->~325MB (wide frontier held worker-local, not accumulated by coordinator) = per-steal migration churn, not useful parallelism. The CADET high-width hang is a distinct pathology (see new bead). Entry points: exploration/scheduler.rs (num_workers, steal path), helpers.rs parallel_num_workers homing.

Per angr-59jk.1 design comparison (commit 5ad385aef, docs/advanced-topics/rust_parallel_design.rst), the recommended threading model for Rust-engine parallel exploration is Option A: shared-nothing per-worker Z3 contexts with Z3_translate at coarse task boundaries. Migration cost stays <5% of runtime when scheduler-task granularity is >100 ms (10K-node state translates in 4-7 ms per angr-59jk.2 spike). Option B (single Z3 context + mutex) is rejected: every Z3 call must hold the lock, so a slow solver.check() on a bimodal bench (~21s slow mode on fairlight) would block all other workers for the full check duration; locks all forward progress, not just parallel speedup. Z3 parallel.enable=true is OUT OF SCOPE here — it's a fan-out inside SAT, not parallel state stepping, AND it's correctness-breaking in this codebase (see avoid-z3-parallel-enable memory). Migration path proposed: 5 phases — instrumentation, per-context cache partitioning, translate helper, work-stealing pool gated by RUST_PARALLEL_WORKERS env var (default 1, single-worker remains current path), Python callback dispatch handling (GIL is the cap for SimProcedure-heavy benches like mma_howtouse), A/B regression. Single-worker fallback is free under Option A but expects a small regression under Option B from unconditional lock acquisition. PARENT angr-59jk should only be promoted from deferred when parallelism is committed to; current single-threaded gaps (mma_howtouse Callable per-init memory sync, sokohashv2 Z3 nondeterminism, hackcon angr-tlvl Z3 shape) have lower-risk single-threaded fixes.

Parallel-exploration GO/NOGO sharpened (2026-06-23): design is DONE (angr-59jk closed, docs/advanced-topics/rust_parallel_design.rst) — verdict Option A (shared-nothing workers + per-task Z3_translate), Option B (single-context-mutex) rejected (slow check() blocks all workers), Z3 parallel.enable out of scope (avoid-z3-parallel-enable). Implementation bead angr-1ilq stays DEFERRED. Sharpened recommendation: CONDITIONAL GO — commit to learning not building. The GO assumption (>100ms/task, <10 migrations -> translate <5%) is UNVERIFIED on real workloads (spike 390-677ns/node used SYNTHETIC AST shapes; CTF-reverser tasks are 10-50ms where 5ms translate = 10-50% and kills economics). Filed de-risk epic angr-panhl (blocks 1ilq) with 2 threading-free kill-gated increments: panhl.1 migration-cadence profile (Phase 0; KILL if Z3-bound trio fairlight/sokohashv2/angry-reverser + unmapped_analysis lack coarse-task shape), panhl.2 translate_into + real-state validation (Phase 2; KILL if real-state cost >> spike or lazy-memory Arc-ancestor translation unsafe). panhl.1 blocks panhl.2. Full GO (reopen 1ilq, Phases 3-5, ship-gate >=1.5x at 2 workers on trio + zero single-threaded regression) ONLY if both pass. Sequencing: complementary to ovqja z3-hotpath (that lowers per-check cost; parallelism distributes independent checks = only lever beating the bimodal Z3 FLOOR). Parallelism is the one genuine 'beyond what Python angr can do' (GIL precludes in-process parallel symex) per beyond-parity-no-motivator-closure-pattern's carve-out (bjk8 clear future path).

ParallelProfiling (core_outcome.rs) holds a Mutex step_stats accumulator: parallel workers call accumulate_step(&step.step_stats) after each dispatch so ALL sum-typed interpreter counters (lift_time_ns, cache_hit/miss, load/store/expr timings, block_exec) surface in mgr.stats() at RUST_PARALLEL_WORKERS>1, mirroring single-threaded accumulated_stats.merge(&step.step_stats) in stepping.rs. Solver fork/sat/deferred counters stay on the SEPARATE atomics in ParallelProfiling because the POST-STEP arms (run_post_step_core, core_outcome.rs) populate them, NOT the interpreter step_stats -- so the full-stats merge cannot double-count them. INVARIANT for future counters: if a counter is set inside the VEX interpreter step it flows automatically via the step_stats merge; if it is set in a post-step coordinator arm it needs an explicit atomic + fold_into/drain_into line. blocks_executed reads 0 in mgr.stats() on BOTH W=1 and W=2 (interpreter never populates that step_stats field) -- pre-existing, not a parallel-path gap.

parallel_tasks in RustExplorationManager stats() is NOT a 'real parallel ran' signal — the panhl.1 work-stealing MIGRATION MODEL (record_migration_sample, native/angr/src/exploration/helpers.rs) bumps parallel_tasks (and parallel_migrations) on the SINGLE-THREADED run loop too (run_loop.rs run_loop_single_threaded calls record_migration_sample at dispatch). The unambiguous discriminator for whether the real work-stealing pool ran is parallel_worker_dispatch: an EMPTY list on the serial path, populated only by the two real parallel loops (stats_api.rs comment 'empty list on the serial path'). Use sum(stats['parallel_worker_dispatch'])>0. Learned in angr-op0dn.13.5 when a callable-find fallback test asserted parallel_tasks==0 and got 84.

RESOLVED (angr-q1mwl, fix 8906de8a5): test_parallel_wave.py hang was NOT the scheduler backoff commit 97b0cbdd7 and NOT a thread deadlock. Root cause: the run-loop 'active exhausted' path returned a 'found' event with a partial count (found_count<num_find), which the Python _explore_with_addresses loop can never break on, so run() spun forever on an empty active stash. See invariant-active-empty-not-partial-found. Underlying trigger: the parallel wave surfaced only 1 of fauxware's 2 accepting paths (found_count stuck at 1) — the angr-027h phase-2 eager retry now recovers the 2nd, so the test passes, but the wave-mode completeness gap is tracked separately.

CADET W=2 collapse root cause (angr-h92bx, NOT offload serde): scheduler worker threads in PersistentPool::new (native/angr/src/exploration/scheduler.rs) were spawned with Rust's DEFAULT 2 MiB stack, while the serial run loop runs on CPython's main thread (8 MiB). The stepping path recurses over AST shape (claripy_bridge::import self-recurses per operand; Z3 emission walks the RustBV tree), so deep symbolic-stdin ASTs (CGC/CADET_00001) overflow 2 MiB on a worker at RUST_PARALLEL_WORKERS>=2. Symptom is NOT an exception: dmesg shows 'angr-worker-N ... segfault ... error 6 in rustylib...so' with the fault address one word below sp (guard-page write). A dead worker never reports wave completion, so the coordinator's first wave never quiesces -> the 'zero completed waves in 100s' observation that looked like an intra-wave perf collapse. Fix: WORKER_STACK_SIZE=16 MiB via thread::Builder::stack_size (commit 4131a8e27). CADET_00001_partial W=2: >180s timeout -> 7.34s (W=1: 7.0s). DEBUG LESSON: when a parallel Rust run 'hangs' or is mysteriously slow, check 'sudo dmesg -T | grep segfault' FIRST — a worker-thread stack overflow presents as a hang, not a crash trace.

Crate-wide clippy too_many_arguments allows are DONE (angr-0mqkc.6 got to 9; angr-inieg.2 finished the tail). Only 2 remain and BOTH are API-boundary-constrained keeps, not debt: fuzzer.rs::py_new (every arg is a distinct Python kwarg — bundling breaks the Python API) and the module-level allow in vex/libvex_ffi.rs (generated FFI bindings). Do NOT 'fix' those. The retired 8 are the pattern reference: CasArgs + CasWriteback (statements_cas.rs x3), LoadGArgs (statements.rs::handle_loadg), [&IRExpr; 4] instead of arg1..arg4 (expressions.rs::eval_qop), StridedPattern (memory/ite_builder.rs::build_strided_ite_tree), ForkBundle for the deferred_forks/stored_conditions/fork_snapshots trio (exploration/callback_types.rs, consumed by PendingCallback::with_context + stepping.rs::handle_unmodeled_call), and SimProcCall (MOVED core_outcome.rs -> callback_types.rs, now pub(crate), shared by handle_simprocedure_core + ExplorationEvent::need_simprocedure). Reuse rules that worked: (1) prefer bundling into an EXISTING struct over inventing one (parallel_process_state took the CoreCtx it already built; setup_native_subcall reused NativeSubcall); (2) a fixed-arity operand list is better as an array than a struct; (3) when a struct moves into a module a child glob-imports (core_outcome_handlers.rs does 'use super::*'), the child still resolves it via the parent's re-import — no edit needed there; (4) struct-field init IS a deref-coercion site, so 'prof: &wave_prof' with wave_prof: Arc coerces fine.

parity_census.py's docs-matrix parser is POSITIONAL: it classifies a SimOption by which list-table section its row physically sits in (docs/advanced-topics/rust_engine.rst), not by what the row's prose says. So an option whose row still lives in the 'Ignored -- divergence-risk' table counts as a flip blocker even when the row text already reads 'Honored as of angr-XXXX'. That is exactly why 3 of the 4 angr-op0dn.14.9 options looked like open work but needed zero code: AVOID_MULTIVALUED_READS/_WRITES (honored since angr-tfic) and ZERO_FILL_UNCONSTRAINED_REGISTERS (matches-by-default since angr-rhe2). The intended fix is an entry in parity_census.py's _EXONERATED dict with a live-code citation -- NOT moving the row -- because _EXONERATED is the audited subtract-from-silent list. Before treating a census 'silent' option as work, always read its docs row AND grep the bridge for the option name; the matrix is stale in the conservative direction.

Parity-audit gap-diff has a false-positive trap: many native procs use the hand-rolled 'impl NativeSimProcedure { fn name(&self) -> &'static str { "x" } }' form (stdio.rs: fwrite/fputs/fflush/setvbuf/feof/ferror; sprintf.rs: sprintf/snprintf/scanf) NOT the declare_proc! 'name = "x"' macro form. A diff that only greps 'name = "..."' (or even +aliases) FALSELY flags these as gaps — wasted an iter starting a duplicate fwrite. Correct native-name extraction must union THREE forms: declare_proc 'name = ".."', hand-rolled 'fn name(&self)' return string (grep -A2), and 'aliases = [..]'. Even then, ALWAYS confirm a candidate is truly absent with 'grep -rl ""PROC"" native/angr/src/procedures/ | grep -v tests' before implementing.

The pbounce synthetic (tests/benchmarks/synthetic_examples/fork_solve_pbounce_W3_S2_M8_B1) has only 6 FEASIBLE leaves, not 8 — do not write a test or acceptance criterion asserting all 2^W=8 found states are solvable. Leaves s=0 and s=4 both force b[0]==0 and b[1]==0 in the width region, which makes the accumulator a CONSTANT whose low byte is 0x66 (s=0) / 0x36 (s=4); the find gate is (acc & 0xff) == 0xee, so neither can ever hold. The engine nevertheless reports 8 found states — the 2 extra ones have solver.satisfiable()==False (false-positive find, filed as angr-3ag1l). A Python-mirror of main() for checking whether a candidate stdin really reaches reach_target lives in tests/engines/rust/test_wide_eval.py::_reaches_target. angr-ue4ro built its acceptance on the wrong "all 8 leaves" premise; check feasibility before trusting a leaf count.

Fork-bench perf attribution (angr-dva9j.6, measure-first): fork_solve_W6_S8 (73s/9 steps) is 99.5% z3_check_time_ns (78 satisfiable checks, ~0.94s each) — the M=20-mask/S=8-mix hard SAT the bench is built to be slow at; fork machinery is ~free (rust_deferred_fork_count @100ns, rust_solver_fork_count=0, z3_materialize 0.2%). cow_fork_scaling (2.6s/513 steps) is 47% z3_materialize (256 leaf solvers lazily minted on first access), forks deferred @0ns. Wide-fork redundant-work hypothesis REFUTED: child_lineage=None by default (use_shared_lineage_solver off, SymContext::fork snapshot_fork_ops.rs), freeze_into_shared (context.rs) is Arc::clone when local empty. Both bounded by inherent Z3 solve, not fork/snapshot/lineage — any speedup belongs to z3 hotpath epic angr-ovqja not the fork path.

perf dashboard pipeline (angr-myty, commit 540313127): nightly-ci.yml emits bench_history_record.json per run, uploaded as artifact bench-history- (90-day retention). perf-dashboard.yml uses workflow_run trigger after Nightly CI, downloads last 60 artifacts via 'gh run list' + 'gh run download', aggregates via tools/aggregate_bench_history.py to docs/dashboard/data.json (gitignored), deploys static Chart.js site to GitHub Pages via actions/deploy-pages@v4. Featured tiles: fauxware/ais3_crackme/csaw_wyvern. CRITICAL: workflow_run fires on any conclusion — the job 'if:' guard checks event.workflow_run.conclusion=='success' before proceeding.

angr-op0dn.13.12: the angr-027h phase-2 eager retry (RustExplorationManager._maybe_phase2_eager_retry) re-seeds self._initial_seed_states = the states the manager was CONSTRUCTED with. After load_snapshot those are the pre-load PLACEHOLDER, not the restored frontier, so a resumed find-based explore that exhausts would silently re-run the whole exploration from a path the caller never asked to resume (and flip use_deferred_forks off globally, which drops stored branch conditions on the parallel path -> unconstrained fallback forks). Fix: load_snapshot now sets _initial_seed_states=None and _phase2_retried=True, retiring phase 2 for any resumed manager. THE TRAP: this silently MASKED snapshot frontier loss. TestParallelCheckpointFrontier's serial arm asserted 8/8 leaves and passed — but only because phase 2 re-ran the exploration from the placeholder (a valid pbounce entry state) and back-filled the leaves the snapshot had lost. With phase 2 retired the true restored-frontier yield is 4/8 (angr-op0dn.13.14). Lesson: any test whose green depends on an implicit retry/fallback path is not testing what its name says — suppress the fallback before trusting the assertion.

MultiPayload::collapse(default_byte, ctx) caches the right-folded ITE keyed on default_byte. Cache is RefCell<Option>, invalidated by push(). Clone propagates cache (Z3 ASTs are refcounted, cheap). set_multi_alternatives always installs a FRESH payload so the merge path in install_multi_for_candidates is automatically safe. Future code that mutates alternatives via any path other than from_alternatives + set_multi_alternatives MUST call invalidate_cache or break this invariant.

Phase 3 collapse cache (angr-j0n4, commit 3bf156896) landed but the Phase 2 gate stays off. Cache helps gate-on sym-write 1.76s→1.72s but gate-off remains 1.55s — ~10% residual gap. Profiling: z3_check≈144ms either way, load_stmt only 8ms of 1.55s. The bottleneck is NOT load-time ITE rebuild (that's what the cache fixes). It is (1) per-byte iteration in assemble_load_with_multi — even cache hits do N page lookups + N byte concats, vs eager's single symbolic_objects.get(addr) returning a width-N BV; (2) flush_multi_cells writes per-byte symbolic_objects so state export volume 4-8x larger than eager. Fixing the gate requires wider-load collapse cache + per-byte flush coalescing — do NOT re-attempt the gate flip based on collapse caching alone.

Phase 4.1 (angr-mmdh.1, commit a1d9f5593) closed the load-time portion of the sym-write gate-on regression: gate-on load_stmt 10ms vs gate-off 9ms (1ms gap). But wall-time gap is still ~10% (1.78s gate-on vs 1.62s gate-off measured 2026-05-15). The remaining gap is in Z3 work, NOT in load assembly: z3_site_eval_upto 55→136ms (+81ms), z3_check 86→158ms (+72ms), z3_check_count 126→310. Root cause: flush_multi_cells writes per-byte symbolic_objects entries that downstream concretization (state export) iterates over individually. Each per-byte entry triggers its own eval_upto + sat check. Fix is Phase 4.2 (angr-mmdh.2: coalesce adjacent per-byte entries on flush). DO NOT try wider-load cache tweaks to close the residual — load_stmt is already <1ms over baseline.

Phase 4.2 (angr-mmdh.2, commit 278fc5223) coalesces adjacent Multi bytes in flush_multi_cells into a single wider symbolic_objects entry (capped at 16 bytes per run). Detection: cond-fingerprint match across consecutive byte addresses (Arc::as_ptr of MultiAlternative::cond's operands — install_multi_for_candidates clones one cond per candidate into each byte, so neighbours from the same store-call share Arcs). For each run: per-alt wider value = concat per-byte alt.value endian-correctly; wider default = concat page bytes; right-fold (cond, wider_value) into one ITE of width 8N; install at symbolic_objects[run_start] with symbolic_spans for interior bytes. sym-write gate-on 1.78s -> 1.70s (avg 4 runs), z3_check 158->147ms, z3_site_eval_upto 136->125ms. Closed ~35% of the gate-on/gate-off gap (1.78->1.62 baseline). Residual ~10% gap is in state-export downstream eval that doesn't scale linearly with symbolic_objects count — Phase 4.3 candidate.

Phase 4.3 (angr-mmdh.3, commit e5c594fe1, 2026-05-15) made Multi-cell lazy stores the only path for symbolic-address Multiple/Strided store concretizations. Removed the use_multi_cell_stores gate field, getter/setter on SymbolicMemory + State, PyO3 bindings (set_use_multi_cell_stores / use_multi_cell_stores), and the now-dead store_conditional_multiple helper. store_symbolic_unified and store_with_concretization always call install_multi_for_candidates_safe now. Old eager store_symbolic (line 168 of store.rs) is still used by tests and is unchanged — it doesn't go through the unified path.

Iop_GetMSBs8x16 (x86 PMOVMSKB) IS testable binary-free, contrary to the iter-50/51 handoff claim that it 'needs an SSE-strlen/PMOVMSKB binary'. A single shellcode blob 660fd7c0 (pmovmskb eax, xmm0) + c3, with xmm0 set via state.regs.xmm0 = claripy.BVV(v,128), drives the op end-to-end through the Rust interpreter. Read s.regs.rax & 0xFFFF for the 16-bit MSB mask (bit i = byte i's bit 7). Pattern: TestVexGetMSBsInstruction in tests/engines/rust/test_strategy_vex.py (commit 657b1b211, bead angr-xhbka). Setting xmm0 from the Python state DOES export into Rust on the input side (not just readable post-procedure as in the strtod test). Same load_shellcode template as test_misc.py TestRust*MemoryStore.

Lazy symbolic memory design (angr-pogf, 2026-05-14) recommends Option A: per-byte MultiValues port (Python-equivalent), NOT Option B (Z3 array primitive) or Option C (Python fallback hybrid). Rationale: A reuses existing balanced ITE builder, concretization strategy chain, fork/merge plumbing; only the page byte cell representation changes. B has unknown perf cliffs with no in-codebase template. C caps gains at Python's number. Two-phase plan: Phase 1 (angr-czph) introduces Multi cells + read-time collapse, Phase 2 (angr-qh5u) makes store_symbolic_unified emit Multi cells by default. Phase 0 prerequisite: ite_depth_max counter as gate metric. See docs/advanced-topics/rust_lazy_memory_design.rst.

posix callback counters (callback_posix_count/total_ns, angr-afbx) only increment during state EXPORT/materialization to Python SimStates (rust_state_export._sync_cached_state + snapshot_to_angr, rust_state_cache), NOT during the Rust step loop. A bare mgr.run() leaves the count at 0; it goes nonzero only once terminal states (deadended/found) are materialized (e.g. accessing state.posix). Implication for angr-6zxx's '>5% wall in posix' DEFER->GO trigger: the wall measured is export-time posix injection, not per-step posix work. Counter feeds python_callback_count via the callback-prefix loop in RustExplorationManager.stats.

Removed _sync_exported_constraints post-sync satisfiable() check (commit 5d22a70a5). Was a diagnostic that called Z3 on full constraint set — took 66s for hackcon (LAZY_SOLVES 20x20 system) with zero benefit. The same Z3 solve happens in eval() anyway. Net savings: 0-1.5s (Z3 solve moves from sat_check to eval, no double-solve).

RESOLVED 2026-05-13 (angr-ruay). The DCAS test_dcas_cmpxchg16b_no_match_keeps_memory + 2 native FD tests (pipe/dup2) were failing because they predated commit 974e2daeb (angr-3uye.2), which changed ret-with-empty-callstack routing from 'deadended' to 'unconstrained'. Fixed by passing save_unconstrained=True and including 'unconstrained' in the survived/inspected stash list. See invariant-ret-empty-callstack-test-fixture.

AVOID pre-pinning constraints: Adding ast == BVV(concrete) for tracked symbols overconstrained states. REVERTED in v2 commit 2f0e8164f. Use Rust solver eval fallback instead.

CRITICAL BUG FIXED: _evaluate_predicates_on_active only iterated self._state_cache, which only contains states created during SimProcedure callbacks. States forked purely in Rust (e.g., symbolic branch at cmp instruction) were NEVER evaluated by callable predicates. Fix: also query Rust stashes (active + deadended) for all state IDs and create lightweight Python states from cached ancestors for uncached ones via _create_state_for_predicate(). This fixed sym-write from FAIL to correct (70 solutions).

Callable predicate evaluation (find/avoid as callables) had a bug: _evaluated_state_ids permanently prevented re-evaluation of states. When stdout grew between batches (e.g. puts executes after state first seen), predicate was never re-checked. Root cause: _evaluate_predicates_on_active used a permanent set. Fix: replaced with _predicate_matched_ids that only tracks states already moved to found/avoid. States in active/deadended are always re-evaluated. Fixed csgames2018 (0 found → 1 found).

Load prefetch (use_load_prefetch in VEXInterpreter) defaults to false at interpreter/mod.rs:729 (fn with_config) with comment 'Disabled by default - adds overhead for most workloads'. set_load_prefetch (prefetch.rs:6) is the only toggle but is never called from anywhere — Python doesn't enable it. So prefetch_loads_for_block early-returns on every block in practice. Optimizations targeting only the prefetch path (e.g., expr-eval LRU, scan-loads memoization) have ~zero measurable impact. The prefetch_loads/unique/dedup/callback scratch buffers added in angr-dtiy still help if anyone re-enables prefetch, but don't move benches today.

prefetch.rs get_stack_pointer had wrong VexArch->offset table for ARM (used 52, actual sp_offset 60) and ARM64 (used 52, actual 264). The bad offsets meant is_stack_region() never matched real ARM/ARM64 stack addresses, silently disabling stack-aware prefetch on those archs. Lesson: hand-coded arch register tables drift from the canonical arch impls. Anywhere you see a 'match self.arch { VexArch::... => offset }' pattern in interpreter_cb/, prefer routing through self.registers.arch().sp_offset() / .ip_offset() / etc.

3 tests in tests/engines/test_rust_public_api.py::TestClassPublicAttrs::test_class_public_attrs_match_inventory (params RustExplorationManager, RustRegisterProxy, RustMemoryProxy) FAIL on rust-symex HEAD as of 2026-06-13 (commit fd3cc6325/743834cb1) with 'public surface drifted' — the runtime proxy classes expose methods (copy, merge, set_state, store, etc.) not listed in angr/exploration/_public_api.py inventory. These are PRE-EXISTING, not caused by test refactors. Fix = update _public_api.py inventory. Don't blame an unrelated change for these.

printf/scanf/sprintf symbolic-format boundary is asymmetric on symbolic format BYTES (address is uniform: all extract_concrete_arg the format ptr -> SymbolicArgument fallback). scanf::read_format_string and sprintf::read_string call extract_concrete_arg on every byte, so the FIRST symbolic byte raises SymbolicArgument and falls back to Python. But NativePrintf::call (printf.rs) does NOT fall back: its byte loop just breaks on a symbolic byte, writes the concrete prefix to stdout, and returns success (it only does raw-copy, no specifier substitution). No symbolic-format substitution path exists for any of them. Documented in docs/extending-angr/simprocedures.rst 'Worked example 4: format strings'.

ProcedureError and SyscallError both carry Memory(crate::memory::MemoryError) variant (added angr-7xhx 2026-05-31). thiserror's #[from] attr provides From, so .memory_load()? / .memory_store()? propagate directly. Don't reintroduce .map_err(|e| Pe::MemoryError(e.to_string())) — that was the boilerplate this refactor removed. Display still shows 'memory error: '. Pattern-match consumers can now drill into MemoryError::Unmapped { addr, size } / Permission / Symbolic etc.

procedures cluster-5 dedup (commit a444fa02f): the concrete-fast-path-then-symbolic-collect string scans (scan_for_null_symbolic in strings.rs, scan_for_byte/scan_for_byte_last in strchr.rs, compare_bytes in strcmp.rs) share one generic driver scan_concrete_then_collect<B,R> in strings.rs. B=per-position load (RustBV for single stream, (RustBV,RustBV) for strcmp's two streams); R=concrete early-return result. concrete closure returns ConcreteStep::{Continue,Stop(R),BeginCollect}; collect_stop decides when to halt collecting (concrete null). Returns ScanResult::{Stopped(R),Exhausted,Collected(Vec<(u64,B)>)}. GOTCHAS: (1) memory_load returns MemoryError not ProcedureError so the load closure must wrap Ok(...?); (2) symbolic-target paths use ConcreteStep::::BeginCollect turbofish since R is otherwise unconstrained, and Stopped(_)=>unreachable!; (3) scan_for_byte_last threads last_match via a &mut capture in the concrete closure, readable after the driver returns (NLL).

procedures/format_common.rs is the canonical home for printf/scanf leaf parsers. parse_width_digits returns (width, bytes_consumed); parse_length_modifier returns (LengthModifier, bytes_consumed). LengthModifier enum has 8 kinds (None/Char/Short/Long/LongLong/SizeT/IntMax/PtrDiff) with the single width helper LengthModifier::int_conv_bits(arch_bits) — it replaced the old boolean is_64bit() in angr-9ke6b.111 because l/z/t are arch-dependent. sprintf and scanf each keep their own top-level state machine — only leaves are shared. When adding a new printf/scanf-family procedure (e.g. fscanf, vsprintf), use these helpers; do NOT inline new ad-hoc digit-loops or length-modifier matches.

procedures::strings (created angr-arf5, commit b10f0785c) is the canonical home for null-terminated-string scanning helpers shared by libc string procedures. Two concrete-only variants: scan_concrete_until_null (errors on max) and scan_concrete_bounded (returns null_found bool). Two symbolic-aware: scan_for_null_symbolic + build_strlen_chain. find_null_addr returns the null position for strcat-style use. Add new str* procedures here, not as ad-hoc loops in the procedure file.

Symbol-counter unification (angr-alhy, 2026-05-31, commit 82df4781b): native SimProcedure fresh-symbol counters now live in procedures::symbol_counter(prefix: &'static str) -> u64, backed by OnceLock<Mutex<HashMap<&'static str, u64>>>. To add a new procedure with symbolic outputs, call symbol_counter("my_prefix") instead of defining a per-procedure static AtomicU64. Picked per-prefix (each prefix has its own counter at 0) over single-global because changing IDs would alter every existing symbol name and could break tests that assert specific names. Lock contention is negligible at procedure-call rates (microseconds vs milliseconds per state).

procedures/ write-side + symbolic-addr shared helpers (angr-24pv4.7, rust-symex). strings.rs now owns the write counterparts to its read/scan helpers: write_concrete_bytes(state,addr,&[u8]) (the per-byte memory_store(addr+i,RustBV::concrete(byte,8)) loop) and write_cstr(state,addr,&[u8]) (bytes + trailing NUL at addr+len). Use write_cstr for always-NUL-terminating C-string writers (strcpy/strdup/strcat/strncat/getenv/sprintf); use write_concrete_bytes for no-terminator or caller-placed-terminator writers (strncpy/snprintf truncated slice/fread/read). NEW module procedures/mem_common.rs owns the symbolic-DEST-address preamble shared by memset+memcpy: consts MAX_SYMBOLIC_ADDR_CANDIDATES=64/MAX_SYMBOLIC_ADDR_SIZE=256/MAX_SYMBOLIC_ADDR_STORES=4096, check_symbolic_addr_size(size_bv)->Result<Option> (None=>size0 noop, Err on symbolic/over-cap), enumerate_addr_candidates(state,ptr,name)->Result<Vec> (eval_upto cap+1, empty/unbounded reject). The candidatessize (memset) vs |dst||src|size (memcpy) store-budget guard stays caller-side. Do NOT re-add per-file MAX_SYMBOLIC_ADDR_ consts.

profile_python_bench.py harness (tests/benchmarks/profile_python_bench.py, landed 2026-06-06 commit 60bbac47d for angr-trsg). Runs one angr-examples bench in-process under cProfile, then dumps {pstats, text top-50 cum+tot, folded collapsed-stack}. Use: python tests/benchmarks/profile_python_bench.py
--engine {python,rust} --cprofile --out /tmp/PREFIX For perf record on Rust frames, run WITHOUT --cprofile: perf record -F 99 -g -- python tests/benchmarks/profile_python_bench.py
--engine rust Why the harness exists: profile_rust_bench.sh wraps the criterion micro-benches in native/angr/benches/vex_engine.rs, NOT actual bench solve.py scripts. cargo-flamegraph/py-spy were unavailable in the build env (no network for cargo install, venv pip broken). The folded format is the input format for flamegraph.pl — render SVG offline.

angr-5aj8 investigation findings (2026-06-06, iter 4 incomplete): With ANGR_RUST_USE_CALLBACK_MEMORY_PROXY=1 on defcon2016quals_baby-re, the deadended state has PC=0xf2aff9eee1eeffff (corrupted). Root-cause narrowed to: between two consecutive Python SimProc callbacks (e.g. printf then fflush), the value at the stack return-address slot (mem[sp=0x7ffffffefef8]) goes from the correct concrete value (e.g. 0x402614 from the call's push) to a specific concrete witness 0xf2aff9eee1eeffff. The corruption window is during VEX interpreter execution BETWEEN callbacks. Key observations: (1) the corruption value is a stable CONCRETE BVV, suggesting a Z3 witness for some unconstrained symbolic that got hardened into Rust memory. (2) Adjacent stack addresses (0xfee0, 0xfee8, 0xfef0, ...) show ALTERNATING pattern 0xc0aefffffffeffff/0xf2aff9eee1eeffff at 16-byte period. (3) No _cb_memory_store / _cb_memory_load fires for stack addresses during the corruption window (verified by Python-side instrumentation wrapping the methods) — it's NOT a Python-mediated write. (4) Same state_id (1) across all callbacks — no fork. (5) Bug reproduces even with a no-op my_scanf SimProc — the symbolic write at flag_0/flag_1 slots is NOT the trigger. (6) Reproduces with just a TracePrintf hook (return 0) and TraceFflush hook (return 0), so default angr SimProc behavior isn't the trigger either. The unconstrained fill at _start writes 3976 bytes at 0x7ffffffef000..0x7ffffffefF88 (filler_mixin) — this region INCLUDES 0xfef8. Hypothesis: during VEX interpreter execution between callbacks, the rust_memory (taken from state.take_memory) ends up with UNCONSTRAINED symbolic at 0xfef8 instead of the concrete value the call instruction's STle pushed. Maybe the interp.flush_stores_to_rust_memory at end of step (stepping.rs:1148) is not committing the pending concrete writes, or the state.replace_memory(mem) at stepping.rs:104-106 is restoring stale memory. Next investigation: add Rust-side eprintln in store_concrete and store_concrete_automap_internal to log writes at addr=0x7ffffffefef8, and verify that the call's STle actually stores 0x402623 there. Also check if RustSimState memory differs from interp.rust_memory at the moment of recovery. Repro: ANGR_RUST_USE_CALLBACK_MEMORY_PROXY=1 python tests/benchmarks/run_single.py defcon2016quals_baby-re --engine rust → FAIL with 'Lift error at 0xf2aff9eee1eeffff' in 0.16s. Reference: bd-key gate-baby-re-attribute-error-triage (referenced in task description, doesn't exist anymore).

RustCallStackProxyPlugin._manage() must exist (return None) as a no-op stub — angr.engines.successors.add_successor (~line 199) unconditionally calls state.callstack._manage() during SimProc successor add. If the proxy lacks _manage, every callback-driven explore (e.g. fauxware find=0x4006ed) AttributeErrors before any state reaches the found stash. The Rust interpreter drives the canonical call stack so a write-through _manage would diverge — keep it inert. Same logic: push/pop/call/ret should also return self / be no-ops since SimProcs don't manually push or pop frames in practice.

Cache-pollution pattern under proxy gates: angr/exploration/rust_callback_dispatch.py:1301 and :1143 do self._state_cache[state_id] = state/succ_state after a SimProc callback. The state was created from cached_state.copy() at line 2045 and had its memory plugin REPLACED with RustMemoryProxy at line 2270 (via _install_callback_memory_proxy). The successor inherits the proxy via plugin copy() (RustMemoryProxy.copy returns another RustMemoryProxy). So the cached state persists with the proxy installed, and any subsequent code that reads state.memory (or state.registers if register-proxy gate is on, state.callstack if callstack-proxy gate is on) gets a proxy plugin pointing at Rust. This is fine during async callbacks (where mgr is unborrowed) but breaks synchronous Rust→Python callbacks invoked from inside run(). Don't 'fix' the cache pollution by restoring the original plugins — the proxy is what makes the gate's write-through semantics work during the NEXT SimProc callback. The right fix is at the consumer side: detect the proxy and bypass.

callback-memory-proxy gate (ANGR_RUST_USE_CALLBACK_MEMORY_PROXY=1) fidelity bug: RustMemoryProxy.store (rust_state_proxy.py) rejected a bare-int value without size=, but angr's SimMemory.store infers a bare int's width from the arch word size. asprintf (angr/procedures/libc/asprintf.py) writes a malloc'd pointer back via memory.store(strp, dst, endness=memory_endness) with NO size -> raised TypeError under the gate, diverging from the tracked-writes path. FIX (commit 5fafd7915, angr-92e17): default size to self._arch.bytes in BOTH the concrete-store int branch AND _data_to_ast (symbolic-addr path). Precedent already in-file: load path + RustRegisterProxy.store default size=arch.bytes. Test test_memory_write_int_value_requires_size encoded the OLD wrong contract (int always needs size) -> rewrote to test_memory_write_int_value_defaults_to_arch_word. Full tests/engines/rust green under gate-on (1093 passed, was 1 fail). Lesson for 92e17 default-on: run the FULL rust suite under the gate to surface these clobber hazards (ryf6-style), not just benches.

RustMemoryProxy.load() must default to Iend_BE, NOT arch.memory_endness. angr's standard memory.load() defaults to BE regardless of architecture. Using arch.memory_endness (Iend_LE on x86) byte-reverses loaded data, breaking callable predicates that compare memory contents (e.g. strcpy_find 'HAHAHAHA' becomes 'AHAHAHAH'). Fixed in commit 5af22cde6.

test_rust_public_api drift for Rust{Register,Memory}Proxy is the SimMemory plugin protocol (STRONGREF_STATE, SUPPORTS_CONCRETE_LOAD, category, copy, init_state, merge, set_state, set_strongref_state, store, widen; +compare/find/permissions on memory) added under the write-through gate angr-qj30; RustExplorationManager drift is drop_copy/fork_state_for_copy CoW plumbing. All INTENTIONAL public surface -> add to angr/exploration/_public_api.py CLASS_PUBLIC_ATTRS, not rename-to-underscore. Precedent: get_state_globals_py/get_state_options_py plumbing already pinned. Fixed in 1d488466a (angr-ytu9).

Per angr-pufm audit (2026-05-06): the three originally-described gaps are largely closed. StoreG/CAS/Load all check has_memory_*_symbolic_full(). Remaining session-sized gaps (now closed by angr-8mh1, commit 0c90d4962): LoadG symbolic-addr Failed, Load expr Failed, fallback_to_python_store Failed. The bigger work remaining for pufm: lazy guarded entries in symbolic_objects+spans for >N solutions (so symbolic-store doesn't have to enumerate addresses) — this needs Z3 array/lambda theory and is multi-session. Recommend opening that as a separate child rather than reopening pufm.

PyO3 supports exporting raw constants via m.add("NAME", VALUE). E.g. m.add("PAGE_SIZE", crate::memory::PAGE_SIZE)? in #[pymodule] makes angr.rustylib.vex_engine.PAGE_SIZE importable. Used in 71st loop session to centralize PAGE_SIZE/PAGE_MASK across Rust↔Python boundary (angr-cr8y). Rust struct constants (BITMAP_WORDS) can guard derived array sizes via const _: () = assert!(BITMAP_WORDS * 64 == PAGE_SIZE as usize) — compile-time check, no runtime cost.

PyO3 FFI trust model (angr-9l9j audit, 2026-06-01): the Rust engine assumes cooperative non-adversarial Python. State IDs go through find_state() → Option/PyValueError, never panic. Callbacks are Py (owning refcount, no dangle); cb.call1(py, ...)? propagates exceptions and type/arity errors. RustBVHandle is a pure value (id/width/concrete, no raw ptr). Address args reach SymbolicMemory (guest-VM addr, not host ptr). Stash names silently create new stashes on typo (footgun, not unsafe — filed angr-630x).

ONE unsafe Python-callable FFI surface: import_z3_constraint_ptrs(state_id, ptrs: Vec) at exploration/state_api.rs:102. Body calls unsafe { ctx.add_constraint_raw(*ptr) } if *ptr != 0. add_constraint_raw (symbolic/context.rs:1524) requires a valid Z3_ast Bool in active thread-local context — NonNull::new_unchecked + Ast::wrap = UB on any non-Z3 integer. Production caller (rust_manager.py:2876) always pairs with prior export_z3_constraint_ptrs so trust holds today. Filed angr-33t9 (P3) to harden via Z3_get_ast_kind sanity check or opaque newtype.

add_constraint_raw on RustSolverContext is NOT directly Python-callable; only reachable through add_constraint_ast which extracts via claripy's z3 backend (solver.rs:26 extract_z3_ast_ptr) — safe by construction.

Spike report in docs/advanced-topics/rust_engine.rst 'PyO3 API trust model' section.

PYTHON_BASELINE_TESTS audit (2026-06-06, iter 503): added tests/sim/test_state.py (10 tests). Coverage gap identified — SimState merge (basic/static/3-way), pickle round-trip, with_condition/global-condition, arbitrary-interrupt handling in SimSuccessors, BYPASS_ERRORED_IRSTMT — not exercised by any of the previous 9 files. test_simsolver/test_symbolic cover eval+concretization but not merge; test_callable runs SimulationManager indirectly but not SimState lifecycle. Estimated ~25s CI cost (4 binary-free tests = ~1s locally; 2 explore-and-merge on state_merge_0 = ~5-10s each in CI). Rejected candidates: tests/sim/test_simulation_manager.py (7 multi-arch fauxware + CFGEmulated would risk 5-min budget), tests/state_plugins/inspect/test_inspect.py (Rust raises NotImplementedError so Python path matters but lower fundamental priority), tests/sim/test_state_customization.py (3 tests, low yield). Periodic re-audit cadence: every ~50 iters or when CI budget changes. Commit: c05cd8586.

python-bridge dedup (angr-24pv4.4): shared solver-proxy primitives now live module-level in rust_state_proxy.py — _cast_eval_result, _with_extra_constraints(ctx, fn, *args, extra=(), **kwargs), and _SolutionCountMixin (eval_one/eval_exact/eval_atleast). Both RustSolverProxy and RustSolverProxyPlugin inherit _SolutionCountMixin and assign _cast_result = staticmethod(_cast_eval_result). rust_callback_dispatch.py imports _with_extra_constraints from rust_state_proxy (no circular import: rust_state_proxy only imports claripy + rustylib). GOTCHA: _with_extra_constraints widened to forward *kwargs so min/max can pass signed=. Env-gate boilerplate consolidated via resolve_env_flag(kwarg, env_var) in rust_manager.py (7 ANGR_RUST_USE gates). rust_callback_dispatch helpers: _resolve_next_pc(state, fallback_addr=None) for symbolic-IP eval_one->eval fallback (3 sites), _merge_tracked_writes/_filter_symbolic_addrs/_merge_symbolic_imports for both resume paths.

Init-prefix find/avoid under the Rust manager (angr-lyvf2 + angr-bdeqa). The Python init skip (_run_python_init_if_needed, rust_manager.py) fast-forwards an entry-point seed to main BEFORE Rust ever sees it, so the seed's own PC -- and every address in the init prefix -- is invisible to Rust's pre-step find_addrs/avoid_addrs checks (Rust's step_one and parallel_process_state both DO check find/avoid pre-step; the state just never arrives with those PCs). Debug tell: mgr.active[0].addr != proj.entry immediately after construction, with stats()['steps'] == 0. Seed-PC leg (angr-lyvf2): init parks (pre-init addr, un-advanced SimState, advanced sid) in _preinit_seeds and address-based explore() calls _route_preinit_seed_finds to push the seed into FOUND unstepped + drop_state_from_stash the advanced counterpart from active. Find addresses strictly INSIDE the prefix (__libc_csu_init/_init/frame_dummy/.init_array) match via rust_manager.py::_replay_preinit_prefix_for_find (angr-bdeqa). Key design points: (1) NO cache-version bump was needed -- the un-advanced seed SimState is already parked in _preinit_seeds by _phase_activate regardless of whether the init cache short-circuited stepping, so the prefix can simply be re-stepped on demand. (2) The replay is LAZY: it runs only after an address-based explore() ends with an empty found stash, so the common (find past main) case pays zero. (3) Two traps hit while implementing: assigning sm.active=[...] on a SimulationManager shadows the dynamic stash attribute with a frozen list (the manager keeps stepping stashes['active'] but reads never update) -- use sm.move(from_stash=...,to_stash=...,filter_func=...); and the angr-027h phase-2 eager retry re-runs _phase_activate mid-explore, which parked a SECOND copy of the seed and double-reported the find -- guarded with the existing _phase2_reseeding flag. (4) Residual divergence, documented in docs/advanced-topics/rust_engine.rst (init-prefix section) + pinned by TestFindInsideInitPrefix::test_avoid_inside_init_prefix_does_not_match: an avoid address only the init prefix executes does NOT kill the seed under Rust.

The Rust manager's Python init skip (_run_python_init_if_needed, rust_manager.py) fast-forwards an entry-point seed to main BEFORE Rust ever sees it, so the seed's own PC — and every address in the init prefix — is invisible to Rust's pre-step find_addrs/avoid_addrs checks. Rust's step_one and parallel_process_state both DO check find/avoid pre-step; the state just never arrives with those PCs. angr-lyvf2 fixed the seed-PC leg only: init parks (pre-init addr, un-advanced SimState, advanced sid) in _preinit_seeds and address-based explore() calls _route_preinit_seed_finds to push the seed into FOUND unstepped + drop_state_from_stash the advanced counterpart from active. STILL BROKEN: a find/avoid address strictly INSIDE the init prefix (e.g. inside __libc_csu_init) is unreachable under Rust — the init-cache short-circuit means the prefix's address trace is not even recorded. Debug tell: mgr.active[0].addr != proj.entry immediately after construction, with stats()['steps'] == 0.

register_python_procedure(name, num_args, no_return, callable) on RustExplorationManager (PyO3) lets Python attach native procedures. The callable receives list[int] of concrete args and returns Optional[int] (None=no value). Implementation: PythonNativeProcedure in native/angr/src/procedures/python_proc.rs wraps Py, extracts concrete u64 from RustBV args (symbolic args -> SymbolicArgument error, dispatcher falls back to Python's SimProcedure path), then Python::attach + cb.call1((args,)) and converts result to RustBV at arch_bits width. Hooked into the existing dispatcher at exploration/mod.rs:2598 — no dispatch-loop changes needed.

Python integration test pattern for native syscall handlers in tests/engines/test_rust_exploration.py: load_shellcode(b'\x0f\x05' + b'\x90'*N, arch='AMD64', load_address=0x1000), blank_state(addr=0x1000), set rax=<syscall_num> and the ABI args (rdi/rsi/rdx/r10/r8/r9), wrap in RustExplorationManager([state]) then call mgr.run(max_steps=1). Verify the native fast path took effect by asserting mgr._rust_mgr.stats()['syscall_python_fallback_count'] == 0. Pre-seed memory in all states via mgr._rust_mgr.active_states_map_memory(addr, bytes, perms_u8). DO NOT depend on post-state register values — max_steps=1 may carry execution past the syscall block, and the state may land in deadended after running through nops. The Python integration test exists to lock in the no-fallback contract; behavior verification belongs in the rust unit test.

Python VEX fallback for unsupported Rust ops: CbExecutionError::Unsupported and NeedPythonFallback now return RunResult::NeedPythonVEX instead of RunResult::Error. This creates a PendingCallback with CallbackReason::PythonVEXFallback, dispatched to _handle_python_vex_fallback in rust_callback_dispatch.py. The handler creates a full SimState, steps it via proj.factory.successors(), and syncs register/memory/constraint changes back to Rust. Multiple successors (symbolic branches in fallback blocks) only sync the first successor — others are logged as warnings. Commit 9e5f4600f.

ARCHITECTURE: rust_manager.py is 5059 lines with 115 methods, 4 separate caches, and ~50 FFI boundary crossings per exploration step. Per-callback cost is 30-150ms (state creation + register sync + memory proxy + plugin restore). This is the main bottleneck for simple examples.

Phase 2 (angr-qh5u, commit bce90fef4) installed Multi-cell STORE path but gated OFF by default. With gate ON, sym-write 1.76s vs 1.58s gate-off (10% regression). Cause: load-time ITE rebuild — assemble_load_with_multi runs the right-fold per load over every Multi byte's alternatives, so read-heavy workloads pay the collapse cost repeatedly. Eager store_conditional_multiple builds the ITE once at store time and reuses the BV across loads. Fix path: per-load collapse cache (memo collapsed BV in MultiPayload, invalidate when alternatives append). Until that lands, the gate stays off and Phase 2 is plumbing-only. Soft blocker hit was foreseen in the design doc (rust_lazy_memory_design.rst Phase 2 acceptance criteria); the gate is the documented response.

Native read(fd=0) stdin short-read modeling (angr-kf0uy, commit ba598033c): read.rs::read_stdin_symbolic returns a symbolic real_size BVS (read_realsize_N) constrained .ule(count) ONLY under state.has_option("SHORT_READS"); default path returns concrete count. KEY: unlike fgets (efvao), read has NO newline/NUL/buffer semantics — Python's storage/file.py SimPacket path (line ~539) just replaces the returned size with a symbol <= orig_size and still fills the full packet, so the lone change is the symbolic RETURN value (the fork source); the count symbolic stdin bytes filling buf are byte-identical to the default. Default-off path stays non-forking so fast-tier gate unaffected (20/20). This completes stdio read-side SHORT_READS modeling: fgets+fgetc+getchar+getc+read all done.

When the ralph clean-state ready queue is fully blocked on external decisions (no concrete code task), do NOT spin re-confirming 'blocked' each iteration (iters 74-78 did this 5x). Instead escalate the decision-blocked beads via 'bd label add <ids...> human' + a crisp 'bd comment' decision question, so they surface in 'bd human list' and the human can unclog 'bd ready'. iter79 flagged csyy9 (won't-fix vs loader-symbol infra, low ROI), xumwf (add paste dep y/n), 75mc (fuzzer-a vs simproc-b + cross-repo PR). Distinguish human-DECISION blocks (use bd human) from DATA/network/upstream blocks (ywu7/439q coverage baseline, 3gjm CI Docker, ig3o.2 upstream archinfo b3sc, kq43 crate-registry) which stay tracked-by-blocker, not human-flagged.

Real-binary readiness roadmap = epic angr-11djq (15 beads, tiered for ralph). Goal: PRACTICAL on WELL-HARNESSED real binaries, NOT unbounded symex (both engines explode unharnessed; honesty contract angr-4n26m). Two failure modes: grub=deep-loop SEARCH (DFS: angr-xel4/angr-smxp), xmllint=glibc-init+HARNESSING (parser path via fuzzer). Tier 1 (ready): .1 expose uniqueness/search knobs to Python (native exists, unwired), .2 deep-loop harness recipe doc, .3 xmllint bounded find=getenv bench. Tier 2 gated behind .4 T2-MEASURE counter evidence: .5 syscalls/.6 symbolic-files/.7 fd-sync/.8 hot-libc/.9 format gaps. CHOSEN primary anti-explosion track for reachability: DIRECTED/GUIDED SEARCH = CFG-distance state prioritization, .14 spike -> .15 native priority-queue impl (sidesteps merge-fidelity minefield). DEFERRED/contingent (only if directed search insufficient + high reconvergence): auto-merging .10 (needs cost-guard), veritesting .11; also deferred TLS-generality .12, constraint-pruning .13.

Verified 2026-06-01 (angr-uprs): real VEX opcodes that route to IROp::Unmapped via execute_irsb_for_test's JSON parser AND surface as RustUnsupportedVexOpError include: (1) x87 transcendentals — Iop_SinF64/CosF64/TanF64/AtanF64/Yl2xF64/Yl2xp1F64/ScaleF64/2xm1F64/RecpExpF64/RecpExpF32 (these only get the libm fast path when arriving as IROp::Raw(code) via the FFI lifter — JSON path can't carry the numeric opcode), (2) NEON saturating shift-by-immediate Iop_QShlNsatS{U,S}{8,16,32,64}x{1,2,4,8,16} — note Iop_QShl8x8 / Iop_QSal8x8 etc. (vector-by-vector) ARE mapped to IROp::VQShlSat in angr-tukg.8, (3) FP/decimal conversions like Iop_F128toD32 / F128toI128S / RoundF32x4_R{M,N,P,Z} / SignificanceRound{D64,D128} / F32ToFixed32S* / Fixed32SToF32x*, (4) crypto+poly like Iop_PolynomialMulAdd{8x16,16x8,32x4,64x2} / Iop_CipherV128 / NCipherV128 / SHA256 / SHA512. The lone NeonUnimplemented entry is Iop_PwAdd32Fx2 (binop, arm64-only via Iex_Binop construction). Probe pattern: build single-Unop or single-Binop IRSB JSON with Ity_I64 args; dispatch hits IROp::Unmapped before any width/type validation.

angr-a32jl.3 Stage-1 reconvergence collision-frequency report (measure-first gate for state-merging angr-11djq.10). Source: stats_api.rs reconvergence_rate = reconvergence_collision_states/reconvergence_active_observed, sampled per active-stash observation in run_loop.rs::record_reconvergence_sample (a 'collision' = 2+ states sharing (pc, callstack-return-chain)). Measured via run_single.py --counters-json, rust engine, 2026-07-04. RESULTS (rate / colliding / observed / maxgroup): CADET_00001_partial 62.3% 38/61 grp6 (n tiny); csgames2018 18.8% 234/1245 grp2; ais3_crackme 17.8% 46/258 grp2; defcon2016quals_baby-re 0% 0/66; fauxware 0% 0/7; defcamp_r100 0% 0/2; csaw_wyvern ~0% 0/2; cmu_binary_bomb_partial/google2016_unbreakable_0/flareon2015_2/sokohashv2 0 obs (no forking on partial run). mma_howtouse + defcamp_r100__dfs not measurable (mma solve.py bypasses --counters-json path; __dfs is a param variant, no example dir). VERDICT: reconvergence is highly bench-dependent. It exceeds the ~5% Stage-2 threshold ONLY on data-dependent branchy CTF binaries (csgames2018, ais3_crackme) + the CGC CADET partial (tiny n). Every >5% hit is exactly the 'data-dependent CTF' class the a32jl.3/11djq.15 gate EXCLUDES; straight-line/quick-solve benches are ~0%. Stage-2 precondition (>5% on a REAL non-CTF target = xmllint/grub) is UNMET with available corpus (xmllint blocked on 75mc human-gated; grub OOMs). Implication for 11djq.10 state-merging: potential payoff exists on branchy data-dependent search but real-target evidence is missing; do not start merging work until a real target clears >5%.

When Cargo.toml's only direct deps are std HashMap/HashSet but rustc-hash is needed, add 'rustc-hash = "2.1"' to native/angr/Cargo.toml. It is already transitively present via z3-sys/syn so the lockfile only adds a single line and there is no extra build cost. Use rustc_hash::{FxHashMap, FxHashSet}; both have ::default() constructors and the same API as std HashMap/HashSet.

RustRegisterProxy.setattr must invalidate cached aliases whose (offset, size) overlaps the written register. Bug pattern: SimRegArg.set_value (and any other partial-register write) issues two stores — first clears the full 64-bit reg, then writes the 32-bit sub-reg. Without overlap invalidation, the first write caches rax=BVV(0); the second caches eax=symbolic but leaves rax stale. A later state.regs.rax read returns BVV(0) and the symbolic SimProcedure return value never reaches the solver. Fix uses a per-arch overlap map computed from arch.registers; module-level cache keyed by arch.name. Closed angr-yxar; commit 1a5b2243b.

angr-4rq7 root cause #2: under the register-proxy write-through gate (ANGR_RUST_USE_CALLBACK_REGISTER_PROXY=1), mgr.found_proxies()/active_proxies() enumerate Rust state-ids that point to GENUINELY-EMPTY states (self.pc==0 AND IP register==0), while the full-export path produces the real successors with valid addrs. So proxy.addr=0x0 is a STATE-ID ENUMERATION DIVERGENCE, not a pc-vs-rip stale read. Suspected mechanism: with simproc_fork gate off, _add_forked_state->_add_rust_state reads succ_state.regs.* through the RegisterProxy that is bound to the PARENT callback_state_id (the state.copy() shares the parent-bound proxy), so the pushed regs come from the parent and Rust mints an id whose successor IP was never written. Likely fix: rebind proxy per-successor OR route _add_forked_state through the simproc_fork-via-rust path. Commit 12aad9ce6 fixed the simpler half (get_state_pc_by_id prefers concrete IP when pc==0).

Register snapshot for extern SimProcedure callbacks: _snapshot_registers() captures reg values as dict instead of state.copy(). 2x faster for ais3 (57ms vs 118ms for 118 callbacks). Only used when: NOT UserHook, NOT in _memory_writing_procs, IS zero-length hook. Snapshot dict format: {reg_name: (is_symbolic, concrete_val_or_None, offset, size)}. _extract_register_changes accepts either SimState or snapshot dict.

_sync_registers_to_rust's symbolic register import path (z3_backend.convert + as_ast().value) is NOT a benchmark hot path. Empirical hit/miss for a (hash,length)→ast_ptr cache: fauxware 0/0, ais3_crackme 0/2, csaw_wyvern 0/0, flareon2015_5 0/8, securityfest_fairlight 0/2, sym-write 0/2, strcpy_find 0/2. Reason: SimProcedure callbacks operate ENTIRELY inside Rust state. Register sync from Python only happens during initial state seeding (or disk cache restoration), so per-benchmark there are at most a handful of unique symbolic register conversions, never repeated. Bead angr-nwbx's premise (50µs × 16 regs × N callbacks) was wrong; the actual cost is bounded by the count of distinct seeded states. Keep this in mind before optimizing 'per-callback FFI overhead' in fauxware — the win is in SimProcedure execution itself (open: 59ms, strcmp: 21ms, read: 16.6ms × 4 from rust_profiling), not register sync (~3ms total).

Pre-existing regression-suite flakes on this 8GB box (verified 2026-05-17 against baseline aef3e6ac0): defcamp_r100 occasionally 16-20% over baseline (0.23s); unmapped_analysis occasionally 15-18% over baseline (0.79s). Reproducible BEFORE any working-tree changes — pure ambient noise from Z3 model nondeterminism + system load. When a regression run fails ONLY on these two benches and a new bench's own timing is within threshold, the new change is OK.

PITFALL (2026-05-25, angr-tkbr.3 iter 7): Edit's replace_all matches EXACT string only. When converting 4 'IROp::NeonUnimplemented(name) => panic!(...)' sites in vex/ops.rs, three sites had the comment 'NEON scaffolding: fail loudly rather than silently fall back.' but the fourth (unop, line 535) had the longer 'NEON scaffolding: fail loudly rather than silently fall back to / a fresh-symbolic result. Implementations land in angr-bkcs.2.' My replace_all snippet only matched 3 of the 4. The remaining panic site was caught only when running an end-to-end test that triggered a PanicException. LESSON: when using replace_all with surrounding-context strings, FIRST run a grep to enumerate match candidates and verify count expected vs. found. Better still: use the narrowest unique anchor (just the panic line) per site, or do explicit per-site Edit calls.

Residual NEON placeholders after angr-tukg campaign (2026-06-01): Iop_PwAdd32Fx2 (the last entry in parse_neon_unimplemented at native/angr/src/vex/opcode_map.rs:945) and Iop_QShlN* (saturating shift-by-immediate, not yet parsed). Documented in the new docs/extending-angr/rust_vex_ops.rst 'Unsupported op coverage matrix'. Promote each to a standalone bead only when a benchmark drives a symbolic path through them.

Reverse(x) leaf-case Z3 emission in build_z3_ast (value.rs:2099-2113) and build_z3_ast_cached (value.rs:2350-2364) had a latent semantic bug: a stray parts.reverse() before the result.concat(part) accumulator produced x itself instead of byte-reversed x. Z3's bv_rewriter folded the mis-shaped Concat back to x as a single Extract — masking the bug. Most call sites hit Rule 3 canonicalization (extract_into: Extract(Reverse(x)) → byte-reindexed Extract on x) at value.rs:1568 or the Concat-distribution branch before reaching the leaf case, so 389/389 integration tests stayed green even with the bug present. Three round-trip unit tests (test_reverse_z3_emission_{16,32,64}bit_leaf in value.rs:3306-3340) catch this kind of bug — they pin x to a concrete value and assert that ctx.eval(Reverse(x)) returns the byte-reversed value. Fix: drop parts.reverse() in both branches (commit bbdb2451e, 2026-05-19).

Roadmap housekeeping 2026-07-18 (interactive session, plan we-need-to-do-ancient-pony.md, peer-reviewed): tracker taken to 0 open / 0 ready / 0 in_progress; 1733 closed; 47 status-deferred; 3 status-blocked (angr-439q, angr-b3sc, angr-ig3o.2 -- note bd status 'Blocked: 18' is the dep-aware metric, not status). VERDICT: engine work is DONE. Closed as acceptance-met: op0dn.10 (M2 determinism 7/7), op0dn.13 (M5 parallel impl 17/17), gorvf (zero-Python, milestone hit), ovqja (z3 hotpath). Everything else deferred with event-shaped UNDEFER CONDITION notes (no --until dates; use bd defer not bd update --defer). THREE CHOKE POINTS gate all remaining work: (1) angr-75mc xmllint -- human files the staged angr-examples PR in tools/upstream_patches/; unblocks S6/M3 (op0dn.5), S7/M5 (op0dn.7), 6d3l, sbvcx, 4n26m.12 -- highest-leverage single action. (2) angr-udo91 env restore (x86 pypcode sleigh + ../binaries) -- unblocks the whole M4 concolic line (op0dn.6/.12.*); network IS available in interactive sessions, recipe on the bead. (3) angr-4n26m.11 blog draft -- parked, awaiting user review of docs/blog/rust_symex_showcase.md. Chores gh-auth-gated: ywu7/439q coverage, 3gjm wheels CI, b3sc archinfo PR. Ralph loop: nothing to drain; ready is intentionally empty so MaxNoopIters self-terminates. PORTFOLIO CONTEXT (absorbed in the R4 merge; blueprint doc /home/ubuntu/.claude/plans/we-have-started-thinking-smooth-valley.md): the program was 6 spike-gated moonshots + 2 enablers under epic angr-op0dn. Durable framing that outlives the closures: the engine is no longer the bottleneck anywhere -- attack the Z3 check()/eval floor and how OFTEN it is called, not the interpreter; GO gates ranked on structural counts (z3_check_count/saved-check/callback counts), NOT wall-time; no CV<0.1 determinism gate (Z3 restart-heuristic floor is permanent); resume is search-continuity, not byte-identity; checkpoint/resume + LibAFL fuzzer + icicle already ship in-tree -- do not re-scope them greenfield.

RST docs in this repo: when adding sections with code references, double-backtick everything (RST inline literal). Default-role single backticks render as :title-reference: under Sphinx, which is visually subtle drift. The errors.rs / engine.rs line citation pattern used in rust_engine.rst's 'User-facing error taxonomy' section is the model: cite a stable file:line range so future variant additions surface as visible doc drift. Pre-existing test_class_public_attrs_match_inventory[RustSimulationManagerProxy] failure (step/step_state/successors added but not in _public_api.py inventory) is independent of doc PRs — confirmed by stash-and-rerun.

rST heading underline validation (no sphinx in venv): use .venv/bin/python3 to scan lines with len(set(line))==1 and line[0] in '=-~^"'' then assert len(prev) == len(cur). Found 3 mismatches in angr-gcfa first draft: top-level title with ↔ (U+2194, 1 codepoint, len() matches visual width), and two ~ underlines off-by-one. Sphinx warnings: underline too short → ERROR, underline too long → OK rendered. Fix all to exact-match for consistency. Memory invariant-rst-heading-underline-em-dash also applies but is about em-dash (—) which is also 1 codepoint per len() — no special multibyte handling needed beyond Python len().

RustExplorationManager.run(n=N) historically delegated to explore() whenever step_func was None, and explore() drops n into **kwargs and IGNORES it, running to completion. This violated SimulationManager.run(n=N) semantics (=step N times). For scripts doing sm.run(n=4); sm.step(...); sm.active[0] (ekopartyctf2015_rev100; asisctffinals2015_license uses the find/avoid explore path instead) the over-run drove the lone state into a deadend that drop_terminal_states discarded, emptying every stash -> 'IndexError: list index out of range' on active[0]/found[0]. Fix (commit ca6a48637): in run(), bind to N steps via the incremental step loop whenever n OR step_func is given; only n is None AND step_func is None delegates to explore(). Keep drop_terminal_states(False) across the bounded run so deadended states land in their stash like Python. Repro lives in /tmp/rev100_repro.py: rust run(n=4) gave all-stashes-empty, python kept active=1.

run_single.py's engine-swap monkeypatch (patched_simulation_manager in _run_in_child) intercepts proj.factory.simulation_manager and routes it to RustExplorationManager. Its caller-frame guard skips angr-internal callers so they use the Python engine. The guard MUST include /angr/callable.py: static-glibc binaries (e.g. busybox) carry IFUNC/IRELATIVE relocations that angr resolves AT LOAD TIME by executing the resolver through angr.callable.Callable -> perform_call -> simulation_manager. Those internal resolver states carry default SimOptions incl. SYMBOL_FILL_UNCONSTRAINED_REGISTERS, which the Rust manager hard-rejects in _check_raise_options (_RAISE_OPTION_NAMES) -> the project fails to even load (0.08s FAIL, before any Filling/load logs; child stderr is suppressed by run_single so it looks mysterious). Guard now: analyses/ OR exploration_techniques/ OR callable.py. Fixed in commit b9b56bcef (angr-4n26m.1).

When wrapping tests/benchmarks/run_single.py in a process-tree sampler (e.g. RSS profiling), the angr worker is a GRANDCHILD of the Popen target — run_single uses multiprocessing.spawn (ctx='spawn'). Naive sampling of just the Popen pid underreports VmRSS by ~10x (orchestrator stays small while grandchild does all angr work, ~200 MB). Fix: walk /proc//task//children recursively for each tracked root. See _descendants() in tests/benchmarks/characterization/fleet_resource_profile/run_fleet.py.

BOTTLENECK: When until predicate or techniques active, Python calls rust_mgr.run(1) per step instead of batched run(). This forces FFI round-trip per VEX block. Line 4492-4493 in rust_manager.py.

value_ops.rs by-ref binop wrappers (add/sub/...) forwarding to _into cost NOTHING extra vs _into for reference-holding callers: microbench rustbv_clone (benches/vex_engine.rs, angr-dva9j.4) showed add_byref_leaf==add_into_owned_leaf (84.7 vs 84.6ns). The clone-both-operands pattern is only avoidable when a caller ALREADY OWNS the operand and can move it (VEXOps::binop path, already using _into). RustBV::clone cost over a ~48ns criterion harness floor: Expression clone +3ns (Arc bump + empty-memo RefCell, unmeasurable), Symbolic leaf clone +8ns (Arc + Z3 BV refcount bump). The operand must be owned to enter the result node's Arc<[RustBV]>, so the leaf clone is unavoidable node-construction cost. Conclusion: adding more &self ref-taking op variants is NOT warranted.

rustbv_to_claripy memoizes recursive conversions by RustBV pointer identity (HashMap<*const RustBV, Py>). RustBV::Expression operands stored inline inside a shared Arc<[RustBV]> have stable per-call addresses, so DAG-shared subtrees are only converted once. Without this, sym-write's 25-unique-subtree DAG fans into a 142k-node tree taking 2.7s; with it, ~tens of ms. Implementation: native/angr/src/claripy_bridge.rs split into rustbv_to_claripy (public, allocates fresh memo HashMap) and rustbv_to_claripy_memo (recursive, takes &mut memo). Memoization is gated on Expression variant only — Concrete/Symbolic/Constrained skip the cache. Commit c88947e65.

When fixing CI rustfmt drift, the actual scope is usually larger than what bug reports cite. CI uses 'cargo fmt --all -- --check' so it flags ALL files; reports may only mention one. Always run cargo fmt --all locally first to see the true scope, then fix everything in one mechanical commit (no rebuild needed — formatting doesn't change compiled output).

rustfmt-on-whole-workspace hazard, re-confirmed iter-50 angr-xgef: running 'cargo fmt' (no path arg) reformats 50+ files of unrelated drift (mostly use-statement reordering and trivial chained-call-collapse). This makes review impossible and risks merge conflicts with other branches. AFTER 'cargo clippy --fix' produces machine-applicable edits: (1) immediately 'git stash' if cargo fmt was run by accident, (2) prefer applying rustfmt with explicit file args: 'cargo fmt -- <changed_files>' or 'cd native/angr && rustfmt --edition 2024 src/foo.rs src/bar.rs'. The clippy autofix output is USUALLY rustfmt-clean already; only rerun rustfmt on the changed files if the autofix produced a long line (e.g. 117+ chars from single_match collapsing) or odd indentation. Workflow that worked: 'cargo clippy --fix -- -A clippy::all -W ' → 'git diff --stat' → if any non-clippy file is touched (rustfmt drift), 'git diff --name-only | grep -v <clippy_files>' then 'git checkout HEAD -- <those_files>'. Worked cleanly for the 7-file batch in angr-xgef (single_match + manual_*).

RustSimState field-bucket map (angr-x04s, state.rs:689): 30 fields grouped as (A) trivially serde — pc, state_id, parent_id, history, detailed_history, max_history, heap_brk, posix_brk, mmap_base, stdin_symbols, call_stack, heap_metadata, no_ip_concretization, no_symbolic_jump_resolution, keep_ip_symbolic, vex_arch, fs, inspection counts/bitmask; (B) concrete-with-symbolic-overlay — RegisterFile (Vec+FxHashMap<u32,RustBV>), SymbolicMemory (OrdMap<u64,MemoryPage>+symbolic_objects/multi_objects/lazy_regions/pending_writes); (C) Arc-shared collapse-on-snapshot — hooks: Arc<HashSet>, environment: Arc<HashMap<Vec,Vec>>; (D) cross-FFI Py handles — symbolic_pages, hook_symbolic_memory, addr_to_ast (each addr->claripy AST, needs Python claripy pickle); (E) Rc solver — SymContext with Vec constraints + ScopePath, all RustBV-tree-serializable. Box rebuilds from arch_name string. Useful map when extending RustSimState — anything new must declare a bucket.

angr-ryf6 (closed, commit 2480b2aca) root cause + durable lesson: under ANGR_RUST_USE_CALLBACK_MEMORY_PROXY=1, _replay_rust_dirty_pages (rust_state_sync.py:1787) and _install_rust_memory_proxy (rust_state_sync.py:1726) issued state.memory.store(...) to copy Rust dirty pages back. SAFE under legacy cached-state model where state.memory is a real SimMemory. UNSAFE under callback-memory-proxy gate: the FIRST callback for a state_id installs RustMemoryProxy as state.memory (_create_state_for_callback line 2231) and caches the state. On SECOND+ callback, the cached state already has the proxy; the replay then calls state.memory.store(page_addr, BVV(4096)) which routes RustMemoryProxy.store -> mgr.set_state_memory_concrete -> 16-byte chunks -> SymbolicMemory.store_concrete -> CLOBBERS symbolic_objects. Next-step symbolic restore (sym_entries from pending_memory_load_symbolic_page) reads from now-clobbered Rust state; AST never re-written; downstream constraints become unsatisfiable for original symbols; solver eval returns the witness (0x20 space) instead of the intended flag chars. Fix: early-return both helpers when _is_rust_memory_proxy(state.memory) is True. Architectural distinction worth knowing: set_state_memory_ast requires pages already mapped and does NOT mark imported_addrs; tracked_symbolic_writes replayed via import_symbolic_to_state DOES create pages on demand and DOES mark imported_addrs (so get_state_symbolic_z3_asts can find the entries). Under the proxy gate, the proxy is the single source of truth — no separate Python state needs syncing. Repro: ANGR_RUST_USE_CALLBACK_MEMORY_PROXY=1 .venv/bin/python tests/benchmarks/run_single.py defcon2016quals_baby-re --engine rust.

S1 easy-query census (angr-op0dn.3) verdict: KILL the cheap pre-solver tier as framed. Instrumentation = native/angr/src/symbolic/query_class.rs (classify_bool/classify_eval/classify_eval_many/classify_extrema + ClassScope), attribution hook inside timed_check (solver_build.rs) so per-class counts sum EXACTLY to z3_check_count; enable with ANGR_RUST_QUERY_CLASS=1, counters surface as z3_check_class_* in mgr.stats(). Corpus (11 fast benches, 1320 checks, tests/benchmarks/query_class_numbers.json): addressable = 2.2% (trivial_decide 2, single_var_range 27, forced_value 0) vs KILL gate >=30%. free_witness 25.2%, hard 72.7%. Two load-bearing findings: (1) forced_value == 0 corpus-wide — NO eval query is pinned by an x==const constraint, so there is no soundness-free eval fast path to harvest; every eval win would change concretization (M2 determinism interaction). (2) single-var is bimodal, not rare-uniform: android_arm_license_validation is 94% single_var_range while every other bench is 0-2.5%, so an interval tier is a per-binary-shape win, not a corpus win. Classification runs AFTER the shipped fast paths (as_u128 short-circuits, cached-model hits, constructor folds), so these are NOT double-counted wins.

angr-op0dn.14.8 drained the opt-in half of the S10 flip gate: CONSTRAINT_TRACKING_IN_SOLVER -> _RAISE_OPTION_NAMES (Rust adds constraints with no assumption literals, so unsat_core() returns silently empty — worse than refusing); CONCRETIZE_SYMBOLIC_WRITE_SIZES -> exonerated (its ONLY in-tree SimOption consumer is SimFileBase._prep_generic in storage/file.py — the identically-named memory knob is a SimMemory constructor kwarg in size_resolution_mixin.py, NOT the option — and native write paths fall back to Python on a symbolic count); CGC_NON_BLOCKING_FDS -> honored both ways (see invariant-cgc-fdwait-option-polarity). parity_census.py silent surface 13 -> 10; opt-in silent count now 0. Remaining flip gate: the tri-state dispatcher (14.5.2), the 3 default-bundle silent options (14.7), the 63 flip-blocking bridge sites, and the constraints inspect gap (14.4.1). angr-op0dn.14.2 (unsat_core wiring) is now beyond-parity feature work, not a flip blocker.

S10 (angr-op0dn.8) verdict: the default-engine flip is blocked by SILENCE, not by missing features. Score divergences by loudness, not feature count: anything Rust detects BEFORE it diverges (raise in _RAISE_OPTION_NAMES, raise in RustInspectProxy._check_event, rejected techniques, unsupported arch) is dispatcher-handleable and NOT a flip blocker. 32/44 divergence-risk SimOptions are already loud (14 raise, 10 warn, 8 exonerated -- the docs SimOption matrix is stale in the CONSERVATIVE direction; see _EXONERATED in tests/benchmarks/parity_census.py for the citation clearing each). Silent surface was 13 items. Two inversions: (1) THE RAISE IS THE REGRESSION -- a raise is right for an opt-in engine and fatal for a default one, so the tri-state dispatcher (angr-op0dn.14.5.2) gates all other M6 work; (2) a DEFAULT-BUNDLE option cannot be dispatched around, since routing on it routes everyone -- EXTENDED_IROP_SUPPORT / TRACK_CONSTRAINT_ACTIONS / TRACK_MEMORY_MAPPING ride the 'symbolic' bundle that plain entry_state() hands out, and the latter two are the pair deliberately excluded from the warn set BECAUSE they are default. Minimal parity set = dispatcher + those 3 options + 63 flip-blocking bridge sites (M6.5a) + the constraints inspect gap. The 7 opt-in silent options were ONE-LINE promotions to _RAISE_OPTION_NAMES, not features. Regenerate: python tests/benchmarks/parity_census.py --json. PROGRESS (angr-op0dn.14.8) drained the opt-in half: CONSTRAINT_TRACKING_IN_SOLVER -> _RAISE_OPTION_NAMES (Rust adds constraints with no assumption literals, so unsat_core() returns silently empty -- worse than refusing); CONCRETIZE_SYMBOLIC_WRITE_SIZES -> exonerated (its ONLY in-tree SimOption consumer is SimFileBase._prep_generic in storage/file.py -- the identically-named memory knob is a SimMemory constructor kwarg in size_resolution_mixin.py, NOT the option -- and native write paths fall back to Python on a symbolic count); CGC_NON_BLOCKING_FDS -> honored both ways (see invariant-cgc-fdwait-option-polarity). Silent surface 13 -> 10; opt-in silent count now 0. Remaining flip gate: the tri-state dispatcher (14.5.2), the 3 default-bundle silent options (14.7), the 63 flip-blocking bridge sites, and the constraints inspect gap (14.4.1). angr-op0dn.14.2 (unsat_core wiring) is now beyond-parity feature work, not a flip blocker.

S3 (angr-op0dn.4) determinism-variance attribution verdict — the residual TIMING variance and the RESULT instability are DISJOINT phenomena, and only the second is boundary-fixable. Harness: tests/benchmarks/run_determinism_census.py (run_repeat/summarize; numbers pinned at tests/benchmarks/determinism_numbers.json). It runs N repeats per bench per mode, fingerprints (a) the WORK each run did — path-pure counters only, WORK_COUNTERS: steps/state_creations/found/z3_check_count/... no ns timings — and (b) the RESULT (found-pc multiset + bench stdout hash), then does a between/within one-way variance decomposition on wall clock grouped by work fingerprint. Findings (n=8/6/5): (1) BOTH bimodal benches measured — google2016_unbreakable_1 (deterministic CV 0.31) and ekopartyctf2016_sokohashv2 (CV 0.17) — have work_groups==1 and IDENTICAL results across every repeat. Same questions to Z3, same answers, same reported flag; only the clock moves. So 100% of the bimodal residual CV is Z3's internal restart/variable-selection path: IRREDUCIBLE at the SymContext boundary, confirming perf-campaign-p5-deferral-decision from a second direction. Canonicalizing eval_upto witness order buys ZERO wall clock. (2) The model choice that IS unpinned shows up somewhere else entirely: csgames2018 (multi-solution keygen) has 6 distinct work groups across 6 runs, diverging ONLY in z3_check/sat/unsat, found_pcs identical, and the printed key list differs run to run — model choice, boundary-fixable, worth ~0.026 CV (i.e. nothing). CONSEQUENCE for M2 (angr-op0dn.10): its acceptance clause 'collapse >=half the residual CV' is UNREACHABLE and must be dropped; the 'make found set + evaluated models identical across runs' clause is reachable and is the only thing worth building (10.1 canonical eval_upto witness order + 10.4 result-equality harness). Do not scope M2 as a variance/perf win — it is a reproducibility win with no timing payoff.

angr-s35o (commit 1c6b0fd2b, 2026-05-21): define_unsigned_cmp_pair! + define_signed_cmp_pair! in symbolic/value.rs replaced 8 borrow+consuming method pairs (ult/ule/ugt/uge + slt/sle/sgt/sge). Bead estimated ~250-300 LOC savings; actual net -87 LOC (-231/+144). Same shape as the vec-ops-savings-bottleneck pattern: macro definition overhead (~85 LOC for the two macros with doc strings) plus per-invocation arg-table lines eat into the savings when each method body is small (signed variants were only ~17 lines pre-refactor). Refactor still earns its keep — eliminates 8x duplication and matches house style with width_unop! / define_float_to_float! — but for future similar refactors, target the LOC estimate based on (per-body lines - macro-call lines) * N, not raw body LOC.

S5a memory-merge cost-shape spike (angr-op0dn.11.1.1, commit on rust-symex). Diamond CFG: 16 mapped pages, fork 2 arms, each writes 8 bytes to ONE shared page. BEFORE/AFTER merge cost (measured in native/angr/src/memory/tests/merge_cost_shape.rs): production SymbolicMemory::merge (memory/mod.rs) walks ALL shared pages = 16 pages / 65536 bytes (does load_concrete(0,PAGE_SIZE) x2 + full PAGE_SIZE byte compare per shared page, even ptr-identical ones). A CoW-skip keyed on MemoryPage::shares_data_with (Arc::ptr_eq(data) && bitmaps equal) walks only the 1 divergent page / 4096 bytes = 16x fewer -> merge cost becomes DIVERGENCE-PROPORTIONAL (pages_walked==divergent-page-count). ITE cells already == divergent-byte-count (8==8) because production already does a per-byte continue on equal concrete bytes. KEY FINDING (retires the risk premise behind sibling angr-op0dn.11.2.1): OrdMap<u64,MemoryPage> + Arc<Vec> structural sharing SURVIVES fork->divergent-write->merge; only the written page breaks ptr-sharing (store_concrete uses Arc::make_mut, page.rs). So the primitives for a divergence-proportional native merge ALREADY SHIP; .11.2.1 is impl-only, not a feasibility question. shares_data_with is #[cfg(test)] for now (promote to pub(crate) when .11.2.x wires the skip into merge). FOLLOW-UP (angr-op0dn.11.2.1, commit 71f21bde3): productionized. The skip did NOT promote shares_data_with as this memory originally suggested — that predicate is UNSOUND for merge (admits symbolic-shared pages whose symbolic_objects diverge). Production uses a narrower MemoryPage::is_shared_identical (ptr-eq + no symbolic/Multi overlay). See merge-cow-skip-soundness.

S5b (angr-op0dn.11.1.2, spike 4a347063b) — constraint-merge cost shape + CoW-prefix prototype on a diamond CFG. Sibling of S5a memory spike (s5a-merge-cost-shape-divergence-proportional). FINDING: current SymContext::merge (snapshot_fork_ops.rs::merge, feature vex-engine-z3) iterates shared.iter().chain(ctx_local.z3_assertions.iter()) per arm and emits Or(not merge_cond, assertion) for EVERY constraint -> guarded-Or count == TOTAL constraint count (Sigma shared+local over arms), even though every arm's shared prefix is byte-identical. The fork-freeze-self-invariant is the enabling primitive: fork() drains self local into z3_assertions_shared via freeze_into_shared then hands the SAME Arc<Vec> to the child, so two arms forked from one base hold a PTR-EQUAL frozen prefix Arc to the merge point (verified Arc::ptr_eq across arms==base); post-fork divergence lives only in local.z3_assertions. Because all diamond arms descend from the fork point, the shared prefix holds on every path reaching the merge, so it can be asserted ONCE UNGUARDED, guarding only local suffixes -> guarded == divergent-constraint count + 1 Or. MEASURED on 8-shared/2-per-arm/2-arm diamond: guarded 4 vs 20 (5x), total assertions 13 vs 21 (prefix collapses from N_ARMS copies to 1, saving (N_ARMS-1)*SHARED). CoW-merged stays SAT + admits exactly arm-value union (x=200,300 yes; 100,5 no) == KILL clause passes; matches production merge SAT/eval EXACTLY (test_cow_merge_matches_production_semantics). SOUNDNESS INPUT for .11.3 kill clause: unguarded-prefix is sound ONLY because local is strictly ADDITIVE to the frozen shared prefix (never retracts/shadows) - test_local_never_shadows_shared checks it. VERDICT: GO on the constraint leg - divergence-proportional guarded count is achievable with zero new primitives; both S5 legs (memory=S5a, constraints=S5b) clear. Fidelity gaps deferred to M3-2b impl (angr-op0dn.11.2.2): assumed export pairs (keep assume_class_reconstructible=false), non_bv residual log (unguarded prefix DOES have RustBV form -> could stay reconstructible), memory-side multi_objects/pending_writes/longest-stdout. cf cheap sibling angr-sbvcx (drop-identical dedup).

value.rs FP helpers (build_fp_z3_ast_cached + 5 siblings, native/angr/src/symbolic/value.rs lines ~2660–3230) use a uniform Z3 FFI safety pattern that's worth lifting into a single function-level SAFETY block instead of restating 30 times: (1) raw_ctx = z3::Context::thread_local().get_z3_context() (thread-local context, valid for thread lifetime), (2) all Z3_ast inputs come from .get_z3_ast() on live Float/BV/Bool/RoundingMode/Sort wrappers bound in scope, (3) every Z3_mk_fpa_*.expect(...) converts NULL to panic so escaping ptrs are non-null, (4) raw is immediately handed to Float::wrap/BV::wrap/Bool::wrap (takes Z3's construction-time refcount), (5) nothing escapes the calling thread. The per-block SAFETY comment then just names the specific FFI call + operand wrappers. Pattern in commit de5a5666c (angr-59t3).

Sampler-hook perf test pattern (native/angr/src/symbolic/lineage.rs::test_sampler_hook_overhead_under_budget, commit ec9984782): to exercise the DECISION branch (not the short-circuit 'accumulate window' branch) on every iteration, manually bump LINEAGE_SWITCH_COUNT/LINEAGE_SWITCH_HOT_COUNT inside the loop so each sample window sees switch_delta >= min_switches. The natural pattern of 'switch many times once' folds all switches into the first window only; subsequent sample-step calls then see switch_delta=0 and take the early-return. Also requires SAMPLER_TEST_LOCK + reset_dismantle_state_for_test() since the hook touches global atoms shared across all parallel tests in the lineage module.

satisfiable() returning False on exception is a wrong-answer bug, not a fallback. False means UNSAT, which is a definitive answer about the constraint system. If the solver itself errored, callers need to know — silently claiming UNSAT will mask flag-finding failures and other solver bugs. Fix in commit 4f16e3792: re-raise from satisfiable_with_fallback in rust_state_export.py. Same pattern existed in _attach_rust_solver_primary fixed in 1e00e4919.

Pre-angr-ryw5, scanf's parse_scanf_format silently ignored %z/%j/%t in the length-modifier match arm (no consume), so they fell through to the spec parser and errored as 'unsupported specifier'. Post-ryw5, scanf accepts them (matches glibc). If a test ever fails because it expected an error from %zd-in-scanf, this is the cause — the new behavior is intentional and correct.

scanf %[...] scanset IS implemented natively in procedures/scanf.rs (fn scanset_body_len + the b'[' arm in parse_scanf_format) — handles %[set], %[^set] negation, max-width, assignment-suppression (%*[...]), literal-bracket-as-first-member, and unterminated->ProcedureError fallback. Treated as a string-like conversion: mints fresh symbolic bytes + NUL like %s (no concrete set-membership filtering — faithful to angr's symbolic-byte modeling). 5 tests in scanf_tests.rs: test_scanf_scanset_{basic,negated_newline,with_width_and_literal_bracket,suppressed_then_int,unterminated_falls_back}. This is the IMPLEMENTED third of the format_parser-gaps trio; %n and float %f/%e/%g are won't-implement parity fallbacks (see format-n-no-native-parity, format-float-no-native-parity). Closed angr-11djq.9 (T2-B6) as fully-covered on these three; T2-MEASURE (11djq.4) found 0 format fallbacks on the real xmllint target so no native expansion is motivated.

Native scanf %[...] scanset (procedures/scanf.rs, scanset_body_len fn + b'[' arm of parse_scanf_format) is modeled like %s: it mints UNCONSTRAINED symbolic bytes capped at field width, NOT constrained to the bracketed character class. This matches the existing %s/sscanf simplification (file content not parsed). So %[^\n] does NOT actually exclude newlines from the minted bytes — over-approximation, sound for path-finding but may yield spurious solutions. scanset_body_len handles %[^...] negation + the POSIX leading-']' literal-member rule (']' right after '[' or '[^' is a set member, not the closing bracket); unterminated sets return None -> ProcedureError -> Python fallback. If a future bead needs faithful matching, add per-byte set-membership constraints there.

Native scanf creates symbolic BVS per format specifier: %d/%i/%u/%x/%o=32-bit, %ld/%lld=64-bit, %c=8-bit, %s=N symbolic bytes + NUL. Stdin symbols tracked via record_stdin_symbol(). Format string must be concrete. Pointer args must be concrete. Suppressed specifiers (*) skip pointer consumption. sscanf ignores source string content (creates symbolic values like scanf). Registered for: scanf, __isoc99_scanf, sscanf.

Scheduler dead-code audit (angr-0mqkc.1): the blanket #[allow(dead_code)] on 'mod scheduler' in exploration/mod.rs was angr-1ilq.3 incremental-landing scaffolding; steady-state has landed so it's removable. Pattern for exploration/scheduler.rs: the Lifo-default *::new() convenience ctors (WorkTransport/WaveJob/RunSession) and the ParallelScheduler compat-wrapper struct are TEST-ONLY (production uses *_with_policy + PersistentPool directly) -> gate with #[cfg(test)], not allow(dead_code). WorkTransport::new had zero callers (deleted). WaveDone is a unit barrier token (coordinator only counts num_workers of them, never reads worker_id) -> field dropped. Lifo import is now #[cfg(test)] since only gated ctors reference it. ActiveResidual MatKind variant (run_loop.rs) stays with justified allow: matched/handled but not yet produced (forward scaffolding).

Parallel scheduler policy propagation (angr-x1fya.1, commit 33ea8d1c0): run_loop's SelectionPolicy (mod.rs field self.policy, now Arc not Box) is threaded into the parallel scheduler via WaveJob::new_with_policy / RunSession::new_with_policy (scheduler.rs), called at the two run_loop.rs parallel dispatch sites with Arc::clone(&self.policy). Before this, WorkTransport defaulted to Lifo REGARDLESS of the Python-set policy, so a FIFO/BFS-configured run silently did LIFO/DFS under RUST_PARALLEL_WORKERS>1. Standalone WaveJob::new/RunSession::new keep the Lifo default so run_instrumented + scheduler unit tests stay byte-identical. offload_surplus's pop_front victim choice is worker-local single-threaded, so Fifo select+offload overlap is a load-balancing nuance, not a race.

Parallel scheduler (exploration/scheduler.rs) dispatch routes through the SelectionPolicy seam (angr-1ilq.9, commit b9fc5f002). WorkTransport holds an Arc; dispatch_next calls policy.select(local) (was pop_back), absorb_continues calls policy.on_fork(local, child) (was push_back). Default = Lifo, which reproduces the pre-seam open-coded pop_back/push_back BYTE-IDENTICALLY -> zero regression. POLICY PROPAGATION (angr-x1fya.1, commit 33ea8d1c0) fixed the latent issue where WorkTransport defaulted to Lifo REGARDLESS of the Python-set policy, so a FIFO/BFS-configured run silently did LIFO/DFS under RUST_PARALLEL_WORKERS>1: run_loop's SelectionPolicy (mod.rs field self.policy, now Arc not Box) is threaded into the parallel scheduler via WaveJob::new_with_policy / RunSession::new_with_policy (scheduler.rs), called at the two run_loop.rs parallel dispatch sites with Arc::clone(&self.policy). Standalone WaveJob::new/RunSession::new keep the Lifo default so run_instrumented + scheduler unit tests stay byte-identical. offload_surplus's pop_front victim choice is worker-local single-threaded, so Fifo select+offload overlap is a load-balancing nuance, not a race. A find-aware ordering policy for num_find=1 also plugs in here but its raw waste win is ~0 (see ilq8-post-cancel-waste); justify only as directed search.

SegmentListIter snapshots into Vec<(start,end,sort)> at iterator construction (segmentlist.rs:232). RangeMap is BTreeMap-backed so .iter().nth(k) was O(k); the snapshot makes total iteration O(n). Iterator type has no #[new] — only constructed via SegmentList::iter. Snapshot semantics mean concurrent modifications are not observed, which matches typical Python iterator expectations.

angr-0r5y3 selection-policy measurement matrix VERDICT (a32jl.2d acceptance gate). Ran fifo/lifo/random/coverage/loop_head via run_single.py --strategy (now exposes all 5; commit 0bc3d6393) on the available corpus: fauxware (7 steps/211MB/0.27s/peakW1), defcamp_r100 (2 steps/241MB/0.32s/W1/found1), xmllint_getenv (3.5s/365MB/W2/found1), google2016_unbreakable_1 (~2s/613MB/W1/found1). FINDING: all five policies are byte-identical on steps/found/peakW/peakRSS and within-noise on wall across the ENTIRE corpus, because the active frontier never exceeds width 2 -- with <=1 selectable state, select() returns the same state regardless of policy, so ordering is a no-op. (A one-off 24s loop_head reading on unbreakable_1 did NOT reproduce -- cold-cache/system noise, not a bucket_key O(history) cliff.) The only policy-discriminating workload is a wide/deep divergent frontier (grub/xmllint-parser class), which stays untractable: 75mc human-gated, grub OOMs, xmllint parser path explodes on BOTH engines (xmllint-vanilla-symex-probe). VERDICT: NO policy beats FIFO and NONE regresses -- all are opt-in + default-inert + Rust-unit-tested (selection_policy.rs asserts the ordering divergence on controlled multi-state setups). NO losers deleted: they cost zero on the default path and are the vehicles for a32jl.4 (CFG-distance directed) + lnzcu. The corpus simply lacks a frontier to exploit; the epic's discriminating-target gap is inherited, not a policy defect.

SelectionPolicy trait seam (angr-a32jl.1, commit ae1120f26): active-state selection + fork insertion are pluggable via native/angr/src/exploration/selection_policy.rs. Trait SelectionPolicy{select(&mut VecDeque)->Option, on_fork(&mut VecDeque, state), name()} with Send+Sync supertraits; zero-sized built-ins Fifo (BFS default: select=pop_front, on_fork=push_back) and Lifo (DFS: select=pop_back, on_fork=push_back). Stored as Box field 'policy' on RustExplorationManager (replaced use_lifo:bool); swapped by set_state_selection_lifo/fifo. TWO chokepoints: (1) SELECT is open-coded in run_loop.rs (NOT StashManager::pop_active, which is dead code w/ no non-test callers) as policy.select(deque) via 'let policy=&*self.policy;' bound before the self.sm.get_mut borrow to keep fields disjoint -- and run_loop deliberately does NOT unindex on pop (pop_active does; do not route run_loop through pop_active or you add an unindex behavior change); (2) ON_FORK via new StashManager::push_active(&dyn SelectionPolicy, state) = self.index + policy.on_fork(self.entry(ACTIVE)), called from helpers::push_to_active_or_drop. Future policies (a32jl.2: random-path, coverage-guided, CFG-distance) impl the trait. Byte-identical step traces under default Fifo; run_regression 22/22 green.

set_max_history (state.rs) was non-converging before retroactive trim: add_to_history/add_history_entry only remove ONE entry per push when over cap, so a state with 100 entries pushed at cap=5 would oscillate between 100-101 entries forever. Fix: drain the head down to cap immediately on set_max_history. The manager-level set_max_history cascades into state.set_max_history for every existing state, so the fix automatically works retroactively for both the per-state Python API and the manager comment that promised 'applied to every state already in any stash'.

angr-sfp9 (commit f13fde0b2, 2026-05-25): HashSet ptr-dedup side-table on add_constraint_raw lands as a documented NULL result. Predicted from angr-1joc measurement: csaw_wyvern 83% hit, flareon2015_5 31% hit, others 0%. After implementation, csaw_wyvern is 2.87s±0.03 (baseline 2.85s±0.02); flareon2015_5 is 3.66-3.79s (baseline 3.63-3.68s). Counters confirm dedup is firing correctly (33/40 hits on csaw_wyvern). Why no win: Z3 internally dedups asserts so the skipped solver.assert call is a no-op; the skipped Bool::clone + Vec push are nanoseconds against millisecond bench noise. Bench-regression 15/15 pass. baseline_timings.json shows 0.94s for csaw_wyvern but current env is 2.85s — baseline is stale env drift; the 'fast-tier' refresh in angr-wnjy did not include csaw_wyvern. Future bench-target reference is the live no-change rerun (2.85s, captured via stash/restore A/B in this session).

_concretize_stack_registers (rust_state_sync.py) had a 10ms cold-path cost on blank_state because rbp is filled with an unconstrained BVS by default_filler_mixin, and solver.eval(unconstrained) paid full Z3 ctx init + check + model (~10ms) just to get back 0. Fast path (commit 1a233418b): scan state.solver.constraints for variable overlap with reg_val.variables — if no overlap, return default directly (0 for BP, arch.initial_sp for SP). Z3's model for an unconstrained var is arbitrary anyway, and downstream code only requires some concrete value. Measured fauxware blank_state: 10.04ms->0.29ms (34x). Warm entry_state path unchanged (0.08ms). Constraint scan itself costs <1us when solver.constraints is small. Note: scan cost grows with constraint count, so for heavily-constrained states the worst case is slow scan + solver.eval; the unconstrained fast path is for fresh blank/manual states where the optimization actually matters. (Symbol-anchored per refactor-memory-sweep-rule; raw rust_state_sync.py:804 drifted to ~929 by iter52.)

Block cache was per-interpreter (fresh on every step). Fix: swap exploration-level LruCache<u64, Arc> into each interpreter via swap_block_cache(). ais3: 511→55 lift callbacks, 152ms→11ms lift time. Key insight: interpreters are created fresh via with_config() per step, NOT forked from parents — the fork path clone was irrelevant.

SharedLineageSolver gating policy DECIDED (angr-op0dn.9.3, 2026-07-13): keep use_shared_lineage_solver default-OFF/opt-in. Measured off-vs-on via run_single.py --use-shared-lineage-solver, median-of-5 wall + --counters-json. The feature WORKS: z3_materialize_count halves everywhere (rev250 88->45, unbreakable_0 52->44, unbreakable_1 52->33) so the 'materialize no longer material' VOID gate is NOT met. But it converts to wall time ONLY where the hot ratio (lineage_switch_fast_path_count/lineage_switch_count) is high: rev250 2.74s->2.47s (-10%, 39% hot) vs anti-case google2016_unbreakable_0 0.99s->1.09s (+10%, 4.5% hot; materialize -46ms but z3_check_time +57ms — switch_to push/pop + sat/model-cache invalidation outweighs the saved materialize). KEY: the v5ht dismantle sampler (tick_and_sample_for_thrash in run_loop.rs) CANNOT backstop a default flip — lineage_dismantled==1 on ALL THREE benches, yet (a) unbreakable_0 still regresses 10% because the >=20-switch detection window is most of a 1s bench so the cost is sunk before the valve trips, and (b) it dismantles rev250 despite its eventual 39% hot ratio and 10% win (early window mispredicts steady state; rev250 wins anyway because dismantle only nulls FUTURE forks' lineage per invariant-v5ht-dismantle-child-none). (b) also kills auto-enable-on-workload-shape: the sampler's early hot ratio is the only runtime shape signal and it is wrong on the one workload the feature helps. Full data: tools/decisions/solver_pool_design.md sec 7 + rust_engine.rst 'Gating policy: the kwarg stays opt-in'. Follow-up (angr-g1fev): per-lineage-tree dismantle instead of one global early decision.

Shared solver for callbacks: RustSolverContext now supports SolverCtxStorage::Shared(Rc<RefCell>) variant. borrow_pending_solver() returns O(1) Rc clone instead of ~3ms Z3 Solver::clone. export_callback_bundle defaults to shared_solver=true. Python side skips constraint re-sync when rust_ctx.is_shared() returns True. Constraints added via _rust_add go directly to pending state's solver. Forked states (SimProc multiple successors) still use fork_pending_solver().

sharif7_rev50 fast-tier gate flakiness (iter66 failed 0.99s vs 0.84 baseline) was a STALE baseline, not a regression. Root cause: rust_time=0.84/callback_count=132/steps=120 was recorded at promote (6417b2410), ~140 commits before the stdio native-parity cluster (fgets/fgetc/fputc/fwrite/_unlocked aliases; 878093d15 'serve cle stdin', 3cda07010, 399958bb0). Those intentional+tested commits shifted I/O handling: native procs serve stdin/stream reads inside the SimProcedure callback (callback_count 132->175) instead of stepping libc VEX blocks (steps 120->77). Result stays correct. Diagnosis trick: the most-recent FUNCTIONAL commit (878093d15) already claimed 'fast-tier gate 20/20' with this exact behavior, and only docs/test-file commits followed -> failure must be in-suite memory pressure (gate measures benches in one process; standalone sharif7 is rock-stable 0.90s x4 vs in-suite 0.99s). Fix: refresh baseline_timings.json sharif7_rev50 to rust_time=0.90/callback_count=175/steps=77 (commit 831d8918a), matching flareon2015_2 precedent 9067d8a23. The 0.15 gate threshold absorbs the in-suite delta. See [[avoid-update-baseline-without-verification]].

Concrete-RHS rewrites for Shl/Lshr/Ashr/Mul (angr-5hpn, commit 51ab6ef51) live in native/angr/src/symbolic/value.rs INSIDE the *into methods, NOT in vex/ops.rs as the bead suggested. Reason: every caller benefits (symbolic_pack_eflags in vex/ccall.rs:222-226 chains 4 shl-by-const ops; ccall.rs and claripy_bridge.rs also shift), and the match arm structure was already there for concrete-concrete and identity cases. Pattern: (None, Some(c)) if c < width as u128 → bit-slice form; (None, Some()) → saturated form (0 or SignExt(MSB)).

Rust-symex showcase blog DRAFT lives at docs/blog/rust_symex_showcase.md (angr-4n26m.11, commit 03bdb7011). Markdown, NOT in the Sphinx toctree (it's a blog draft, not API docs). Numbers are sourced from the tests/benchmarks/numbers.json artifacts that show.py emit (NEVER baseline_timings.json, stale by design). If a demo's measured numbers change, re-run that show_*.py and update the corresponding table/figure in the blog. Bead is NOT closeable autonomously: acceptance = user-reviewed draft, so it stays claimed/in_progress until the human signs off. Honesty guardrails baked in: speed='now practical' incl busybox 0.33x loss + bimodal non-wins; multiarch=parity-not-speed; checkpoint/resume='resume the search' w/ value-recovery=observed-bonus; solver-instr=genuinely-new bonus.

Checkpoint/resume showcase demo (show_checkpoint_resume.py, angr-4n26m.8) uses a TWO-PROCESS orchestration: the script re-invokes itself via subprocess with --phase dump / --phase resume over a shared on-disk snapshot. This both (a) authentically crosses a process boundary (the whole point of the demo) and (b) is the in-loop memory-safe pattern — each phase runs angr under its own RLIMIT_AS=3GB guard. The 'guaranteed' claim is SEARCH CONTINUITY, proved by a structural frontier fingerprint {stash_counts, sorted(active_addrs)} captured pre-dump and re-captured immediately after load_from_disk; both are deterministic and independent of Z3 model latitude so an exact match proves restore (not re-run). At snapshot_steps=14 fauxware yields a rich frontier (2 active + 1 deadended). Value-recovery is reported as observed-bonus-not-guaranteed (model equality not preserved across re-solve) per showcase-resume-target-classification.

show_multiarch.py (tests/benchmarks/) is the multi-arch PARITY showcase demo (angr-4n26m.6). Runs the SAME crackme (symbolic input==42 reaches success block) across all 6 Supported arches: AMD64/X86 (blob, 2eax+16==100), ARMEB (BE blob, 2r0+16==100), AArch64 (inline ELF, calls double_it then ==84), MIPS32-LE/MIPS64-LE (inline ELF, ADDIU t0,42 + BEQ). All build in-memory (no external binaries / cross-compiler) — byte encodings lifted verbatim from CI-verified tests in tests/engines/rust/test_multiarch.py. Each run verifies found + solver.eval(sym)==42. Framing: breadth/correctness ONLY, NOT speed (no Python baseline; the one real non-x86 ELF bench android_arm_license_validation is 0.8x slower). Self-caps RLIMIT_AS=3GB; run as subprocess. Durable artifact tests/benchmarks/multiarch_numbers.json for the .11 blog. --quick runs AMD64/AARCH64/ARMEB subset.

Showcase number gate (angr-4n26m.3): tests/benchmarks/measure_showcase.py runs run_single.py --both N>=5 per target, parses 'OK s' lines (regex _OK_RE), reports median+[min,max] per engine + speedup_median=py.median/rust.median. Durable artifact = tests/benchmarks/showcase_numbers.json (consumed by .5/.6/.7/.11). Fresh 2026-06-19 medians, tight ranges: defcamp_r100 3.82x, sharif7_rev50 3.94x, ais3_crackme 3.06x, fauxware 1.74x; busybox_static 0.33x (60-step entry_state breadth demo, ~0.9s PyO3 init tax dominates so Rust LOSES by design - NOT a raw-speed number). BIMODAL set (sokohashv2/fairlight/angry-reverser/unbreakable_1/CADET_00001_partial) is flagged by the harness and excluded from default; heavy winners ekopartyctf2016_rev250(~32s/run)/flareon2015_5(~57s/run) excluded for OOM/time, measure on demand with small -n. NEVER quote baseline_timings.json (stale by design).

Showcase raw-speed harness: tests/benchmarks/show_raw_speed.py builds a reproducible before(python)/after(rust) speed table, reusing measure_showcase.measure() (the angr-4n26m.3 number gate) verbatim — no duplicate measurement logic, no baseline_timings.json quoting. Three tiers via _targets(): headline (ekopartyctf2016_rev250, flareon2015_5 — heavy CTF, ~9min for full N=5, excluded from --quick), fast (sharif7_rev50/defcamp_r100/ais3_crackme — the --quick set), realsoftware (busybox_static — HONESTY row, init-tax-dominated so Rust LOSES ~0.33x, in NOT_A_SPEEDUP, never quote as a win). --json refreshes durable artifact raw_speed_numbers.json (consumed by blog task .11). Fresh N=5 medians 2026-06-19: eko 14.68x, flareon 7.38x, sharif7 4.00x, defcamp 3.79x, ais3 3.06x. Note flareon re-measured at 7.38x (not the ~10x task-desc estimate) and 25.7s python (not ~57s) — the gate corrects stale estimates, which is the point.

Checkpoint/resume demo (angr-4n26m.8) target classification, from angr-4n26m.4 probe tests/benchmarks/show_resume_boundary.py (commit 2b84b0b71). fauxware find=0x4006ed is VALUE-REPRODUCIBLE: across N=5 fresh explores in BOTH deterministic and nondeterministic modes the found posix.dumps(0) is identical (the SOSNEAKY backdoor, hex ...534f534e45414b59..), and a dump_snapshot/load_from_disk round-trip reproduces the same bytes. Found-path stdin AST is already CONCRETE (posix.stdin.content[0][0] is non-symbolic). BUT this is NOT global constraint-uniqueness: 0x4006ed is reachable by other inputs (matching creds path) too. So value-reproduction rests on Z3 consistently LANDING on the same path, not on uniqueness. CONSEQUENCE for .8: frame resume as SEARCH CONTINUITY (reaches the same point); value-reproduction is incidental/empirical, not guaranteed (rust_engine.rst: model equality NOT guaranteed across restore; deterministic=True narrows not closes). deterministic=True is safe but unnecessary for this target. SimPacketsStream has no .load — use .content list of (ast,size) or .read (returns >2-tuple).

Showcase demos (tests/benchmarks/show_*.py) cannot be run as a bare 'python show_X.py' — angr is an editable/namespace package resolved off the repo root, NOT in site-packages, so a script's sys.path[0]=script-dir misses it. They need PYTHONPATH= (matches the documented 'env PYTHONPATH=$PWD .venv/bin/python' invocation). The single runner show_all.py (struct DEMOS registry, fn run_demo) injects this. Exit-code contract shared by every demo main(): 0=pass, 2=corpus-absent (SKIP, not fail), other=FAIL. Nightly job showcase_smoke runs 'show_all.py --quick'.

Showcase solver-instrumentation demo (angr-4n26m.9) = tests/benchmarks/show_solver_instrumentation.py. Brackets explore() with mgr.reset_solver_stats()/get_solver_stats() to surface per-call-site Z3 attribution + lazy-fork materialization counts (the 'look inside the solver' angle). KEY GOTCHA: get_solver_stats() returns the FULL process-wide counter dict (bvop_, lineage_, etc.), not just z3_* — the human report filters to z3_check_, z3_site_{count,time_ns} (sites in SITE_ORDER), z3_materialize, z3_assume_, z3_branch_model_. On defcamp_r100 N=1: 25 check() calls, 43ms (~35% of 0.125s search), satisfiable site=98% of check time, 13 lazy-fork materializations. The final-solution eval() happens AFTER the stats window closes (posix.dumps after get_solver_stats), so eval site shows 0 — window covers explore() only, by design. Self-caps RLIMIT_AS=3GB; run via env PYTHONPATH=$PWD. Durable artifact solver_instrumentation_numbers.json.

csaw_wyvern Rust bottleneck is per-fallback Python SimState materialization, NOT the SimProcedure body. Measured 2026-06-15: rust wall=2.68s, time_in_callbacks=2.073s (77%), callback_simprocedure_state_create_ns=1.98s vs execute_ns=0.064s. ~74% of wall is creating a Python SimState for 30 SimProcedure fallbacks (~66ms each). The xtse.1 hypothesis ('2s inside the body') was WRONG. Of the 30 fallbacks ~24 are angr.procedures.stubs.ReturnUnconstrained (operator new/delete, ostream<<, std::string/allocator ctors/dtors). DEAD-END (angr-8mjd iter46, reverted): a native ReturnUnconstrained fast-path writing a FRESH symbolic BV regressed csaw_wyvern 2.7s->86s. ROOT CAUSE NOW CONFIRMED (iter74) — see native-returnunconstrained-bvv0-gate: Python's solver.Unconstrained returns concrete BVV(0) unless SYMBOLIC_INITIAL_VALUES is set (off by default), so Python writes null not a symbol; the native path minted symbols -> downstream null-checks/address-uses fork and pay concretization -> explosion. CORRECTED RECIPE: gate the native fast-path on SYMBOLIC_INITIAL_VALUES and write BVV(0) when absent. Not a dead-end anymore.

tests/benchmarks/run_regression.py SLA flags: --sla-warn-threshold (default 1.0x = warn), --sla-fail-threshold (default 0.5x = fail with exit 1), --no-sla disables entirely. Uses py_time from current run, else baseline_timings.json[entry].python_time. To populate python_time for rust_only entries (most of FAST_SUITE), the user must run Python alongside Rust manually since rust_only skips Python in run_regression.py. python_time is now preserved across --update runs (was previously clobbered to None).

End-to-end SMC support on the Rust engine has TWO halves: (1) cache invalidation + dirty-page tracking on stores (closed by angr-k67f, commit 3d632bb2b), and (2) lift-side fresh-bytes channel (closed by angr-kwwd, commit 3b0e7690d). The (2) half threads bytes from rust_memory.read_concrete_bytes_for_lift through call_lift_block as a 3rd positional arg into _cb_lift_block, which uses them as factory.block(addr, byte_string=dirty_bytes). Without (2), default builds (no native-lift feature) executed stale cle-binary bytes after a Rust-side store overwrote in-binary code, because backup_state-aware lifting can't see Rust stores until end-of-step _sync_rust_memory_to_state. With both halves landed, default builds now handle SMC binaries (packers, anti-debug, JIT). Native-lift builds had the analogous fast path already (execution.rs:353).

Self-modifying code on the Rust engine has a multi-part story. The cache invalidation + dirty-page tracking (closed 2026-05-09 by angr-k67f, commit 3d632bb2b) handles the FIRST half: stores to in-binary addresses mark page-numbers (addr >> 12) in CallbackInterpreter.dirtied_code_pages and remove cached IRSBs whose [block_addr, block_addr + irsb.size()) range overlaps the write. invalidate_code_at + is_code_range_dirtied are the public API. update_prefetch_on_store hooks both Rust-native and Python-fallback store paths. SECOND half (followup angr-kwwd) is the lift-side: _cb_lift_block calls project.factory.block(addr), which reads from cle's immutable static binary, not from rust_memory or state.memory. backup_state alone doesn't help because Rust-native stores don't sync to Python state.memory until end-of-step. The native-lift feature has a working SMC fast path (reads from rust_memory.read_concrete_bytes_for_lift for dirty pages) but native-lift is OPT-IN and not in default features. So in default builds, SMC binaries still execute stale bytes.

Z3_solver_to_string + Solver::from_string round-trip via SMT-LIB2 has a ~5ms parser-warmup floor regardless of size (measured at 5852us for 5 assertions vs 4812us for 95 assertions — small case is slower because parser setup dominates). Size scales linearly at ~65 bytes/assertion. Verdict: fine for save/restore-on-disk; bad for hot-path serialization. See angr-9o4n.1 + commit 64731bb65.

angr-smxp slice 1 (2026-06-06, commit 873a6f549): DFS + LengthLimiter recipe for grub-class deep-input-loop binaries. The infrastructure was already in place — exploration_strategy='dfs' kwarg in RustExplorationManager.init (rust_manager.py:865) routes through set_exploration_strategy → set_state_selection_lifo (Rust FFI), and LengthLimiter technique registers natively via register_length_limiter (rust_techniques.py:254). The slice 1 deliverable was the composition guidance: docs section in rust_engine.rst (Memory pressure section: 'Deep-input-loop binaries (grub-class)') with the angr-xel4 spike table and the recommended recipe, plus regression test TestExplorationStrategy.test_deep_loop_recipe_dfs_plus_length_limiter pinning that DFS + LengthLimiter compose without overriding each other (max_length=32 respected on fauxware active stash). Real grub measurement deferred — needs >4GB RLIMIT_AS. Heuristic auto-detection (option b) and one-call helper (option c) also deferred.

angr-op0dn.13.14 root cause #1 (FIXED, 2026-07-13): the snapshot envelope dropped the bucket-D per-state Python-AST overlays. RustSimState::from_snapshot sets symbolic_pages / hook_symbolic_memory / addr_to_ast to EMPTY (they are Py, not serde-able), and the old dump_snapshot docstring waved it off with 'the Rust SimProcedures keep those overlays empty' — true for fauxware, FALSE for any state that bounced through a Python SimProcedure. Measured on fork_solve_pbounce_W3_S2_M8_B1: every active state carries 45 addr_to_ast + 45 symbolic_pages entries at dump time; all were silently discarded, so the resumed state read those addresses as unconstrained. Fix: RustExplorationManager.dump_snapshot writes an outer envelope (_SNAPSHOT_MAGIC + u64 rust-blob len + pickled overlays); capture_bucket_d / restore_bucket_d round-trip them through the existing get_state*/set_state* FFI (manager_methods.rs). Legacy bare-Rust files still load. Pinned by test_snapshot_round_trips_bucket_d_overlays in tests/engines/rust/test_parallel_wave.py. IMPORTANT: this is necessary but NOT sufficient — the serial resume still drains only 6/8 leaves with overlays intact, so the deferred-fork loss has a second independent cause.

DEBUG METHOD for 'snapshot restores structurally but loses paths' (angr-op0dn.13.10): the structural fingerprint (stash_counts + sorted Rust PCs) can MATCH while the snapshot still drops states, because states parked outside every stash are invisible to BOTH sides of the comparison. Do not trust it as a completeness check. What actually localized the bug: (1) a phase-marked repro (log markers through the angr logger so they interleave with the WARNINGs — plain stderr prints do NOT order correctly against logging) showed every 'condition N not found in stored_conditions' and 'Lift error at 0x0' fired in the RESUME phase, not the parallel explore; (2) setting mgr._phase2_retried=True to suppress the angr-027h phase-2 eager retry (_maybe_phase2_eager_retry, rust_manager.py) — WITHOUT that, phase 2 re-seeds _initial_seed_states, which after a load_snapshot is the THROWAWAY blank state the manager was constructed with, masking the real loss and inflating/deflating the found count run-to-run; (3) get_state_bbl_history_tail(sid, n) to show the frontier state's history (hook addr then 0x0 = a bounce state whose pc the worker zeroed). NOTE for any post-load_snapshot test: phase-2 eager retry is semantically wrong on a restored manager (it discards the restored frontier and restarts from the constructor's seed) — see angr-op0dn.13.12.

Snapshot Python wrapper API (angr-x04s.1.4): RustExplorationManager.dump_snapshot(path) / load_snapshot(path). Bytes-level PyO3 bindings (dump_snapshot_bytes() returns PyBytes, load_snapshot_bytes(bytes) takes &[u8]) live on the Rust pyclass; Python wrapper handles file I/O. load_snapshot replaces self.sm wholesale via StashManager::load_snapshot, then invalidates the state-export cache; manager-level config (find/avoid addrs, hooks, simprocedures, solver/memory config) is PRESERVED. Empty envelope and stale version byte both surface as ValueError on Python side ('empty snapshot envelope' / 'version mismatch'). Tests: TestSnapshotRoundTrip in tests/engines/test_rust_exploration.py (3 cases — fauxware structural round-trip + 2 error paths). Round-trip preserves stash_counts, state_ids per stash, per-state pc — does NOT preserve full num_constraints count (see snapshot-add-constraint-raw-not-tracked). 677/677 pytest, 16/16 bench gate green at commit.

angr-op0dn.13.14: the serial snapshot-resume leaf loss (4 of 8 pbounce leaves) is NOT in the snapshot data — dump-load-dump is byte-identical. It tracks process-global/thread-local claripy-bridge cache state that the envelope cannot carry: with the SAME snapshot bytes, a resume yields 4/8 when the states were never exported before the dump and 6/8 when every active state was exported through the proxy first. Suspect the global SymbolicIdentityRegistry + CLARIPY_AST_CACHE: an unregistered restored leaf that bounces through a Python SimProcedure is re-imported as a BRAND NEW rust symbol carrying none of its path constraints (see the angr-izov2 comment in claripy_bridge/export.rs::rustbv_to_claripy_memo) — a silently lost fork. Fix direction: load_snapshot should re-register every restored leaf (id, name, width) in the global registry. Do NOT re-chase envelope-data theories (missing pending callbacks, dropped Py overlays, unserialized next_id) — all three are measured and refuted.

snapshot-resume-leaf-loss FALSIFIED THEORIES (angr-op0dn.13.14, iters 40-43). Five theories were killed by experiment before the real cause was found — do not re-chase them: (1) solver identity (each restored state gets its own SymContext vs live siblings sharing one via fork) — not load-bearing; (2) the Python SimProcedure bounce — a hook-free repro fails identically; (3) anything process-global (counters/registries) — a WARM same-process resume fails identically; (4) seed-symbol id collision — a seed state that mints no symbols yields the same leaf count; (5) state-id collision on re-mint — fixed in 3ab14cfce, leaf count unmoved. Three real but independent defects WERE found and fixed along the way (bucket-D overlay drop 22c2ba311, SymContext::next_id 13c50741c, NEXT_STATE_ID restore epoch 3ab14cfce) — none of them moved the leaf count either, which is the tell that the framing was wrong. The actual cause is the phase-2 eager retry: see [[snapshot-resume-leaf-loss-root-cause]]. LESSON: when three consecutive 'fixes' each close a real correctness gap but leave the headline metric unmoved, stop fixing and go measure the metric's provenance — here, diffing mgr.stats counters between the live and resumed runs found it in one shot.

RustSimState snapshot/serialization route (angr-x04s spike, 2026-06-01): RustBV op-tree serialization is the right primitive. The enum (Concrete/Symbolic/Constrained/Expression at native/angr/src/symbolic/value.rs:400) is fully serializable without touching Z3 — Symbolic variant's cached Z3 AST drops out, rebuilds lazily on first to_z3_ast() after load via BV::new_const(name, width). Constraint store (SymContext::assumed_constraints, Vec) follows the same route. SMT-LIB2 round-trip is the alternative (~5ms parser floor, validated cross-context in angr-9o4n.1 + angr-rwzi) but redundant for in-process snapshots. Concrete buckets in RustSimState (state.rs:689): (1) plain data fields trivially serde; (2) RegisterFile/SymbolicMemory concrete halves are bytes + symbolic overlays of RustBV; (3) Arc<HashSet/HashMap> fields (hooks, environment) collapse to owned on snapshot; (4) Py fields (symbolic_pages, hook_symbolic_memory, addr_to_ast) require Python claripy.dumps/loads — soft dependency on live Python at load time. Follow-up bead angr-x04s.1 filed for fauxware prototype.

RegisterFile + MemoryPage serde shadow type pattern (angr-x04s.1.2, 2026-06-02). Same shape as the RustBV pattern: define ShadowTypeData mirror, derive From/Into, use #[serde(from='Data', into='Data')] on the original. Key collapses for this layer: Arc<Vec> -> Vec, Box<[u64; BITMAP_WORDS]> -> Vec (with malformed-length -> None fallback), FxHashMap -> BTreeMap (deterministic ordering + serde-friendly), Box -> arch_name String rebuilt via arch_from_name with AMD64 fallback. RegisterFile needs Clone derive too (serde-into consumes). SymContextSnapshot mirrors get_assumed_constraints() and restore_from_snapshot() replays via assume_true/assume_false — Z3 solver, sat_cache, model_cache, scope_path, push stacks all rederive from the canonical (RustBV, bool) log. ScopePath itself was NOT serialized: lineage is opt-in, scope frames hold non-serializable z3::ast::Bool, and the path rebuilds from constraints once a fresh lineage is installed. See native/angr/src/arch/mod.rs RegisterFileData, native/angr/src/memory/page.rs MemoryPageData, native/angr/src/symbolic/context.rs SymContextSnapshot.

RustStateExportMixin._recover_symbolic_ast lookup order (post-refactor 44ba4fa85): state_id -> parent_id (if >=0) -> root_id (from _state_roots cache, fall back to rust_mgr.get_state_root) -> hook_symbolic_memory[state_id]. ALL lookups require tracked_size == size. AST-only check: hook map is keyed ONLY by snapshot.state_id (not parent/root). The 4 original lookup blocks were near-identical except hook_mem keys only off state_id.

angr-9o4n (commit 778434d0a, 2026-06-03): snapshot codec was fully implemented but undocumented. The 'missing' v1.0 piece per bd description was actually just (1) a classmethod load_from_disk that doesn't need a placeholder state and (2) docs graduation — rust_engine.rst:2669 still claimed 'no built-in snapshot / restore primitive today' even though dump_snapshot/load_snapshot Python wrappers + STASH_SNAPSHOT_VERSION envelope + round-trip test had been in place for weeks. Lesson: when a bd task description predates intermediate work, verify what currently exists before designing the 'missing' piece. Existing API: dump_snapshot(path), load_snapshot(path), and now classmethod load_from_disk(path, project, **kwargs). Known caveats documented: bucket-D Py overlays not captured, manager config not captured (kwargs pass-through), model equality not guaranteed (Z3 nondeterminism).

angr-fv81 (sokohashv2 IndexError after angr-ctct fix) root cause: UltraPage.symbolic_data is a SortedDict keyed by the start offset of each symbolic region — a single 8-byte filler-materialised value stores ONE dict entry but marks 8 symbolic_bitmap bits. angr-ctct's initial fallback walked sd.keys() and extracted only that ONE byte per region; bytes 1..N silently collapsed to concrete zero on the Rust side. For sokohashv2 this turned a 15-term hash AST (using bits [15:0]/[31:16]/[47:32]/[63:48] of every 8-byte input) into a 4-term AST (low byte only) — explored states still reached to_find but the hash conjunction with WIN_HASH was unsat, so solver.eval_upto returned []. Fix walks each entry's contiguous bitmap extent (capped at 64 bytes/entry to skip 4 KB page-fillers that would otherwise tank ais3_crackme/google2016_unbreakable_0 by ~40%).

Survey 2026-05-23 (angr-9l1y closure): counters dump on three sub-1.0x benches shows ZERO x87 transcendental hits — ekopartyctf2016_sokohashv2 (0.4x): vex_op_other=0, vex_op_fp=0, all python_vex_*_fallback_count=0. mma_howtouse (0.6x): vex_op_other=0. securityfest_fairlight (1.0x): vex_op_other=0. solve.py for sokohashv2 hooks every transcendental call site with do_nothing (lines 95-107), bypassing them in the symbolic path. Bottleneck on sokohashv2 is structurally Z3: z3_check_time_ns8.73s + z3_site_eval_upto_time_ns7.62s out of 10s walltime; rust_run_loop_time_ns144ms (Rust interpreter negligible). Implication: angr-9l1y (symbolic transcendental modeling) cannot move any current benchmark; the concrete fast paths in native/angr/src/vex/transcendentals.rs (angr-n28w, 238 LOC) remain useful only as fidelity scaffolding. Updated docs/advanced-topics/rust_engine.rst sokohashv2 section + CLAUDE.md table to reflect the new root cause attribution. Re-open the bead only if a new bench surfaces that actually invokes Iop_SinF64/CosF64/TanF64/AtanF64/Yl2xF64/Yl2xp1F64/ScaleF64/2xm1F64/RecpExpF{64,32} symbolically.

Rust hash AST has only 4 terms using bits [7:0] of each 64-bit input — Python has 15+ terms covering all 16-bit halfwords of all 4 inputs. The do_repmovsd hook copies 32 bytes from esi to edi via memory.load+memory.store, but Rust callback round-trip preserves only the first byte of each 8-byte symbolic chunk; bytes 1-7 become concrete zero. Root cause likely in callback memory tracker or extraction picking only the symbolic_data SortedDict entries that started at the load-base address (since SortedDict[addr] is keyed by exact start address, not range).

Sokohashv2 had TWO bugs: (1) angr-ctct FIXED 2026-05-14 commit c6b2824cb: _extract_symbolic_pages missed filler-materialised symbolic values. (2) angr-fv81 FIXED 2026-05-14 commit 13bb9f741: _extract_from_ultrapage fallback only extracted the head byte of each symbolic_data entry, dropping bytes 1..N as concrete zero, producing IndexError on sm.found[0]. Fix walks each entry's full bitmap extent (capped at 64 bytes). Verified 2026-06-01 (angr-y95g closure): rust engine succeeds in ~15s vs python ~6s — residual 0.4x gap is Z3 nondeterminism per BIMODAL_BENCHMARKS / benchmark-bimodal-variance-rules, NOT a remaining functional bug.

Characterization update (angr-e548): the Rust solver NOW correctly detects equality contradictions. RustSolverContext().add_constraint_ast(x==5) + add_constraint_ast(x==10) -> satisfiable() is False. Earlier docstrings claimed add_constraint_ast 'may not preserve == semantics' and could spuriously return SAT — that is stale; equality constraints route through Z3. test_solver_contradictory_constraints now asserts 'is False' to catch a regression back to spurious-SAT. See characterization-vs-fix-pattern.

Rust↔Python solver-fallback architecture. Canonical reference for how the Rust engine integrates with state.solver across export, fork, and eval.

Eval-time mechanism (canonical). RustSolverFallback monkey-patches state.solver.eval/min/max/satisfiable so post-exploration evals run against the Rust solver. NEVER reintroduce state.solver.add(ast == BVV(rust_eval)) patterns — they overconstrain and were the source of fauxware/flareon2015_5 wrong-answer regressions (revert 2f0e8164f; zombie deleted 70d84f909). See pre-pinning-dangerous and avoid-pre-pinning-recovered-symbols memories for the regression history. Constraint export uses Rust solver eval per constraint-export-no-pre-pin.

_attach_rust_solver_fallback callsites in rust_state_export.py (verified 2026-05-22, angr-7ulb). There are 5: lines 319, 358, 386, 414, 980. Only line 414 is redundant (_snapshot_to_angr already attaches at line 980; duplicate is no-op via _ATTACH_FLAG guard). Lines 358 and 386 look redundant against cached states but are NOT — self._state_cache[parent].copy() invokes SimSolver.copy() (state_plugins/solver.py:452) which creates a fresh _stored_solver via _solver.branch(); the new object does not inherit the prior setattr(solver, _ATTACH_FLAG, True) or the eval/min/max/satisfiable overrides (those were on the OLD object's __dict__). Re-attach IS required at 319/358/386/980. Removing 358 or 386 silently makes solver.eval() use Python-only constraints, regressing post-exploration eval perf and risking UNSAT on identity-mismatch cases.

Proxy semantics. RustStateProxy adds constraints to the fork solver only (not the parent). satisfiable() defers extras to Python. solver.eval fast paths that skip the solver entirely are dangerous — see avoid-concretize-fast-path-skips-solver (folded here).

Why: cluster of overlapping invariants was scattered across 5+ memories. How to apply: sole reference for any code review touching the proxy or solver-attach paths.

State export fallback (eval_with_fallback, etc.) must cache the forked Rust solver. Each fork_state_solver() call costs ~3ms (Z3 solver clone). Before fix, every solver.eval() call on found states forked again. Fixed by caching in _cached_rust_ctx closure variable, fork once per state.

INVARIANT: Solver fork must be O(1) via push/pop, not O(n) constraint replay. Fixed in v2 commit c37058a5c.

Solver fork O(n²) root cause: SymContext::fork() eagerly replays all Z3 assertions into fresh solver. Python angr avoids this via lazy solver materialization (claripy FullFrontend pattern) — constraint list is copied on fork but Z3 solver is only created on first query. Most forked states are pruned/avoided without ever querying the solver, so the replay cost is only paid for states that need it. Fix: make Solver field Option, materialize lazily. Issue: angr-y2o.

RustSolverContext tests MUST call _setup_shared_z3_context() in setup_class when running in isolation. Without the shared Z3 context, add_constraint_ast uses Python's Z3 variables but eval/min/max create NEW Rust Z3 variables — they don't match, so eval returns 0 for everything. The full test suite hides this because earlier tests (via angr.Project) initialize the shared context as a side effect.

Python multiprocessing spawn workers inherit sys.path from the parent process, NOT just env. When you launch 'python /path/to/script.py' (no -c), Python sets sys.path[0] to dirname(script.py); spawn workers inherit that. So a worker invoked from .../tests/benchmarks/run_regression.py has sys.path[0]=tests/benchmarks/, NOT REPO_DIR — which means 'import angr' fails inside the worker even though it would work in the parent. Fix is to set PYTHONPATH=REPO_DIR in the env (PYTHONPATH is honored on every interpreter startup including spawn workers and is independent of sys.path[0]). Discovered while fixing angr-lbze: the loop benchmark gate had been silently failing for 28+ iterations because the gate worker couldn't import angr.

When closing a spike bead, check if a recently-landed sibling spike already satisfies the acceptance criteria. Pattern (2026-06-01): angr-nfjc was filed 2026-05-30 for 'OOM/MemoryError error-recovery contract' characterization; angr-zidj landed the answer in commit c714e9e15 on 2026-06-01 (rust_engine.rst 'Memory pressure and OOM' subsection — Where memory accumulates / Behavior on exhaustion / Recovery contract sub-blocks). Nfjc's 4 characterization questions and 'graceful-drain follow-up bead' AC were both fully covered (the follow-up is angr-x04s.1). Closure took ~10 tool calls: verify zidj landed, re-read the doc section, cross-check the 4 AC bullets against existing prose, close as superseded. Useful triage heuristic — before claiming a spike, grep recent commits + bd ls --status=closed for related work that may have made the spike trivially closeable.