catch / 2

rust-symex branch clippy gate state (2026-06-06, iter 510): 'cargo clippy --all-targets -- -D warnings' fails locally with 232 warnings on rust-symex@9f92ca217 (down from 285 after angr-vi8o to_string cleanup). Top remaining buckets: 81 needless_borrows_for_generic_args (regression from angr-qgbw which fixed 56 instances 2026-06-02), 41 deprecated z3 ::eq (use ::eq instead — z3 crate post-0.19 deprecation), 18 unnecessary>=_y+1, 14 Arc not Send/Sync, 13 deprecated pyo3::prepare_freethreaded_python (use Python::initialize, pyo3 0.27+ deprecation). CI in .github/workflows/ci.yml::rust_check runs the same command with -D warnings but rust-symex never goes through CI (autonomous loop doesn't push). Implication: clippy gate has been broken on rust-symex without breaking master. Either (a) merge rust-symex through PR cycle to fix, or (b) clear warnings in autonomous-loop sessions. Most remaining warnings are in test/bench code (216 in lib test, 13 in benches, 2 in lib).

clippy bucket counts on rust-symex after iter 514 (angr-z3jb.2 done). Cargo clippy --all-targets --release per-message buckets: 81 needless_borrows_for_generic_args (REGRESSION RISK from angr-qgbw — DO NOT autofix), 14 Arc-not-Send-Sync (may be intentional), 10 needless_range_loop (idx-style), 8 'this operation has no effect' (likely 0-lane intentional, needs #[allow]), 5 unnecessary u128 cast, 4 type_complexity, 3 cloned vs from_ref, 2 each: useless_conversion to Py, needless_range_loop on solvers/e_lanes/a_lanes, manual_div_ceil, doc_quote, ok_then_expect. Order any future child task by mechanical-safety: 5 u128 cast and 8 no-effect are next-easiest; range_loop needs case-by-case; needless_borrows AVOID.

Iter 594 (angr-0b3f) silenced the 14 clippy::arc_with_non_send_sync warnings by adding a module-level #![allow(clippy::arc_with_non_send_sync)] to the #[cfg(test)] mod in native/angr/src/symbolic/context.rs. Rationale (in-source comment): all 14 sites construct Arc<Mutex> to match production lineage_arc() type; SharedLineageSolver is intentionally non-Send/Sync (thread-local Z3 ctx). Switching tests to Rc would diverge from prod type. Final clippy state on rust-symex: 81 warnings = 81 needless_borrows_for_generic_args (AVOID per clippy-needless-borrows-avoid; angr-qgbw regression risk). The needless_borrows bucket is now the ONLY remaining clippy work, and it is fully gated by the avoid-rule. Commit f0346c8d1.

Clippy too_many_arguments slice (10 sites cleared 2026-06-02, angr-rq8s) — verdict: #[allow] beats arg-struct refactor for ALL 10 sites in this codebase. The args fall into 3 categories: (1) PyO3 callback contracts where signature is dictated by Python side (4 call_inspect_* sites); (2) constructors that mirror struct fields verbatim (PendingCallback::with_context, ExplorationEvent::need_simprocedure) — a builder would just relocate the same fields; (3) step-result residue passed once from one dispatch site (handle_simprocedure, handle_unmodeled_call) where the triple (deferred_forks, stored_conditions, fork_snapshots) IS cohesive but only flows through ~6 lines, so structification cost > benefit. Cohesive ForkResidue struct WOULD help if more handlers spring up — defer to that point. Codebase pattern: 5 prior sites in fuzzer.rs/statements.rs/expressions.rs already use #[allow]. Lib warnings now 13, remaining: too_many_arguments=0, result_large_err=6 (Err size — HOT-PATH gate first), arc_with_non_send_sync=4 (try Rc), large_enum_variant=2 (RISKY — StepError boxing), only_used_in_recursion=1.

clippy unnecessary_cast u128 fix pattern (angr-z3jb.3, 2026-06-06): cargo clippy --all-targets --release flags '(0xCAFE as u128) << N' as 'casting integer literal to u128 is unnecessary' — replace with '0xCAFE_u128 << N'. The cast-to-u128 form was idiomatic before Rust got the underscore-typed-suffix syntax. All 5 sites in vex/ops.rs were in test code computing expected u128 payloads for V128 SIMD lane manipulation tests. Mechanical Edit replacement, no behavior change. Verified by running affected tests (test_vget_elem_16x8_concrete, test_vset_elem_*, test_vdup_32x4_concrete). Commit 2cb1526dc.

angr-z3jb epic auto-closed 2026-06-10 (iter 592) — all 232 original clippy warnings on rust-symex either fixed or AVOIDED. Final bucket counts: 81 needless_borrows_for_generic_args (AVOID — angr-qgbw regression risk), 14 Arc-not-Send/Sync (likely Z3-context-bound, intentional), 4 type_complexity (needs type Foo = aliases), 1 too_many_arguments. Total: 100 remaining warnings, all in 'AVOID/intentional' buckets. To pick up clippy cleanup again, first audit the 81 needless_borrows for angr-qgbw regression-safe sites, OR file new sub-tasks under z3jb for the 4 type_complexity / 1 too_many_arguments mechanical fixes.

When closing infrastructure work whose acceptance criteria specifies a downstream benchmark target (e.g. 'X moves to >=1.0x' or '>=10% bimodal win'), file a SEPARATE validation bead at close-time rather than leaving the AC pending against the original bead's close_reason. Working examples in this repo: angr-518z (infra) -> angr-gra3 (measured 0% gain, prediction invalidated); angr-tlvl (Reverse fix) -> angr-p8cz (broader pre-Z3 rewrite); angr-9maq (lazy-zero opt) -> angr-8t45 (bisect+workaround for hackcon regression caused by it). Audit pass 2026-05-21 (angr-3ch3) found this pattern was applied consistently across 10 hedged-close beads; all verification loops closed. Continue the pattern.

VERIFIED: try_read_concrete_memory does NOT intercept 0x1000-0x1020 loads in codegate. All loads go through load_from_callback. 7 addrs return symbolic BVS (0x1000,0x1008,0x100a,0x1011,0x1018,0x101c), but 0x1019-0x101b return is_symbolic=false from Python callback (concrete). The issue of missing XOR(stdin,mem_fill) constraints is NOT caused by concrete memory interception.

Symbol identity mismatch (mem_1018_24_8 vs mem_1018_13_8) FIXED in current code. Both loads consistently return mem_1018_13_8. Only mem_1018_13_8 appears in 2/316 constraints. Other mem_* variables (mem_1000_14_8, mem_1008_15_8, mem_1011_17_8, mem_100a_18_8, mem_101c_16_8) are correctly loaded as symbolic BVS from load_from_callback but their values disappear from the constraint system during VEX interpreter processing. Some addrs (0x1019-0x101b) return is_symbolic=false from Python callback, meaning Python memory treats those as concrete.

VEX tracing for codegate at XOR+CMP blocks: 422/435 cc_dep1 values are symbolic, 13 concrete. Only 6/422 contain mem_* variables from 0x1000-0x1020 fill regions. All symbolic operations (XOR, store to [rbp-0x30], reload, comparison) correctly preserve symbolic expressions through rust_memory round-trip. The 316-vs-382 constraint divergence is a PATH divergence (different branch outcomes accumulate different constraint sets), not expression simplification/concretization. The binary has ~65 unique XOR blocks, each processing different combinations of stdin bytes and occasionally mem_fill values.

god-module/complexity audit of rust-symex (2026-06-20, bead angr-zel8z). 8 oversized files, skeptic-verified behavior-preserving decomposition proposals: state.rs(3692)->6 submodules(filesystem/inspection/types/snapshot/export/fork; needs pub(crate) fields + a fork_with() builder to collapse 4x fork-literal dup), callbacks.rs(2748)->4(events/config/inspect-dispatch/io-dispatch), exploration/mod.rs(2551)->3(event/callback_types/native_technique), vex/ccall.rs(2440)->4(arm32/arm64/x86_symbolic/x86_concrete + split handle_ccall_with_ctx 440ln), claripy_bridge.rs(1986)->3(cache/import/export), interpreter/statements.rs(1910)->3(cas/store/inspect), vex/ir.rs(1780)->5(ops_def/ast/arch/types/aux) [LANDED commit 327f12229 — vex/ir.rs is now the native/angr/src/vex/ir/ directory with ops_def/ast/arch/types/aux + mod], interpreter/mod.rs(1757)->5. Load-bearing constraint: PyO3 single-#[pymethods]-block (entry points cannot move; inherent impls split freely). Precedent angr-a2br (CLOSED context.rs split): pin invariants in rustdoc+debug_asserts FIRST. OUT OF SCOPE: context.rs(done a2br), value.rs(~4734, deferred by a2br close-note - needs own bead).

RustBV::concat_balanced (value.rs:1771) is NOT a hot path on the angr bench matrix. Measured 2026-05-22 via bvop_concat_count (--counters-json):

bvop_concat_count increments once per internal node of every concat tree, so csaw_wyvern's 581 maps to maybe a few dozen wide-load concat_balanced calls — well under 1ms total even at ~10us per call.

CRITICAL: don't re-file an angr-7ulb-style 'optimize concat_balanced' bead. Premise rejected:

1. Recursion uses &parts[..] slice refs — zero-cost, no per-level cloning.
2. Only LEAVES clone (each leaf once). Per invariant-rustbv-clone-cheap, RustBV clone is allocation-free for Symbolic/Expression variants (Arc bumps only).
3. Cold benches (mma_howtouse, sokohashv2, fairlight) don't exercise this path at all — optimizing it cannot move them.
4. The N-1 Arc<[RustBV;2]> allocs per balanced concat tree are intrinsic; iterative-vs-recursive changes nothing.

If a future audit profiles the AST-construction layer and finds wide-load concat cost dominating, MEASURE FIRST. The empirical counter check kills the speculative claim cheaply.

Why: angr-7ulb was filed 2026-05-21 on a 'likely contributes to mma_howtouse/sokohashv2 slowdown' hypothesis. Measurement on iter 10 (2026-05-22) refuted it. How to apply: when reviewing concat-related optimization beads, run --counters-json on representative benches first and check bvop_concat_count before any code work.

Rust concretizer now has separate read/write strategies matching Python. Read: Range(1024) → Any (eval single solution). Write: Range(128) → Max (range().max). ConcretizationMode enum selects strategy. concretize_cached_read/write on interpreter, concretize_read/write on AddressConcretizer. Config propagated: RustExplorationManager.concretizer_config → stepping.rs interp.set_concretizer(). Python reads strategy limits from state.memory.read_strategies[0]._limit at init time.

RustBV value.rs already has concrete constant folding in ALL operations (add, sub, mul, div, mod, and, or, xor, not, neg, shifts, rotations, comparisons, extract, concat, sign/zero extend, truncate, clz, ctz, popcount, ITE, reverse). Each method checks as_u128() and returns Self::concrete() when both operands are concrete. The 'constant folding' task was really about interpreter-level optimization: ITE short-circuit (skip dead branch eval) and #[inline] hints for cross-module inlining. Commit 6c11435d0.

angr-tvpk (2026-06-03): _add_rust_state used to make up to THREE constraint installer calls per state at init — (1) Z3 ptr transfer from old_rust_mgr, (2) claripy round-trip via export_state_constraints when Z3 unavailable, (3) post-Z3 Python solver.constraints re-sync. The (2)+(3) combo was the 'didn't trust Rust as source of truth' tell. Collapsed to ONE installer call: Z3 ptr transfer when crossing managers (state has rust_mgr/rust_found_state_id on scratch AND early-reuse branch in init didn't take), else Python solver.constraints install. Mutually exclusive — no more bidirectional export_state_constraints->add_constraints_to_state cycle. RustSolverFallback's replay path (rust_state_export.py:155-170) handles user-added post-attach constraints on the wrapper side, so we don't need to re-install them here. Verified 683 tests still pass and fauxware bench unchanged. Net: 99 lines -> 31 lines.

angr-2zwy (2026-06-03, commit b2f10cd1e) chose option (b): RustStateProxy.copy() now raises NotImplementedError instead of returning a shallow proxy. The shallow copy aliased _state_id and silently corrupted the parent on any mutation — the foot-gun behind the Veritesting incompatibility (angr-dv24). Acceptance from the bd description allowed either (a) real Rust fork + plumb back through manager bookkeeping (stash placement, options/globals dicts, stdout tracker) OR (b) raise with a clear error. We took (b) because (a) requires answering 'where does the forked state live?' (stash placement governs whether step()/find_state see it, neither default is right for Veritesting-style consumers) and duplicating per-state Python metadata (options dict keyed by state_id in python_mgr.get_state_options_py, globals dict via get_state_globals_py, stdout_data on the proxy itself). The error message names bd angr-2zwy, docs/advanced-topics/rust_engine.rst, and the use_rust_engine=False fallback. Tests in TestStateProxyCopyRaises pin the raise + the surfaced message fields + that the source proxy stays usable after a failed copy(). Spiller row in docs promoted to 'Likely broken'.

Counter-attribution sweep (2026-07-16, 8 non-bimodal benches via run_single.py --counters-json) to find fillable env-independent optimization backlog: the corpus is MATURE. Only ONE net-new drainable lever survived dedup -> filed as angr-gorvf.19 (per-crossing simprocedure bounce SERVICE residual: sync_back+sc_bundle FFI marshalling, ~8% on baby-re only, gorvf.10 successor). Everything else is COVERED/settled: z3 materialize-on-fork (angr-y2o closed + shared-lineage decided opt-in, unbreakable_0 is the anti-case + per-fork-solver-share-infeasible), z3 check on hard SAT (irreducible, belongs to ovqja epic), bounce-FREQUENCY reduction (settled NO by bounce-reduction-low-roi-corpus), mma_howtouse >100%-wall z3 is a Callable-eval artifact routing to the PYTHON engine (angr-dva9j.7 not a Rust target), xmllint fallbacks are is_in_binary misroutes (gorvf-3.x). CONCLUSION: env-independent optimization work is nearly exhausted; the ralph loop's real productivity bottleneck is the two GATES (xmllint corpus PR angr-75mc / x86 pypcode sleigh angr-udo91), which unblock the M3/M5/M4 empirical program. Idling when only gated work remains is CORRECT loop behavior, not a grooming failure -- do not manufacture beads to avoid it.

fork-tree characterisation (angr-uf0g, 2026-06-03 sweep N=2..9): hypothesis 'Python deep-copies on fork = hockey stick, Rust im::OrdMap = linear' is FALSE. Both engines are linear in 2^N leaf states. Python's SimMemory does page-level CoW. The Rust win is constant-factor: ~15x faster CPU per leaf state (~10ms vs ~150ms), ~2x lower RSS per state (~3.7MB vs ~7.2MB). At 4GB RLIMIT_AS Python OOMs in Z3 at N=9 (512 states, 2.7GB+) while Rust completes in 1.85GB. Curve in tests/benchmarks/characterization/cow_fork_scaling/results.csv.

CRITICAL: Python/claripy comparisons (ULT, ULE, etc.) produce native Z3 Bool nodes via Z3_mk_bvult etc. Our Rust build_z3_ast() wraps every comparison in ITE(bvult(a,b), BV(1,1), BV(0,1)) then assume_true does ._eq(BV(1,1)) to convert back to Bool. This round-trip creates 3-4 extra Z3 nodes per comparison. Fix: add to_z3_bool() method that pattern-matches comparison ops to produce Bool directly. Use in assume_true/assume_false/check_branch_feasibility. Files: value_z3.rs (to_z3_bool), context.rs.

Symbolic-aware ctype.h native procedures (commit ebb606c98): bits[7:0] extraction matches concrete as u8 truncation. Predicate shape: ranges_predicate / set_predicate (range-OR or set-eq-OR), case_shift (ITE on shifted byte). Result always zero-extended to arch.bits(). Pattern is reusable for future single-byte-input symbolic SimProcedures. Helper functions live in native/angr/src/procedures/ctype.rs.

angr-czph (lazy LOAD Phase 1) closed 2026-05-14 after all 4 sub-beads landed: angr-me3z (MultiPayload data structure, 1.1) → angr-n082 (load_concrete_lazy_inner Multi collapse, 1.2) → angr-aija (store_symbolic_unified_multi helpers, 1.3) → angr-5zw8 (MultiwriteAnnotation routing in _cb_memory_store_symbolic_full, 1.4). All plumbing in place; default store path still eager. Next phase: angr-qh5u (Phase 2) flips Multiple/Strided in store_symbolic_unified to use Multi cells unconditionally — that is where the sym-write 2× target lands. angr-qh5u is currently P3 and is the direct successor — fresh session recommended due to surface area (touches store_conditional_multiple, store_strided, the eager ITE path).

angr-czph (lazy LOAD Phase 1) is broken into 4 sequential sub-beads after ca509f925: angr-me3z (Phase 1.1, MultiPayload data structure) is CLOSED; angr-n082 (Phase 1.2, load_concrete_lazy_inner Multi-cell collapse via balanced ITE builder) is next-ready; angr-aija (Phase 1.3, store_concrete_multi / store_symbolic_unified_multi helpers + flush_pending_writes update) depends on 1.2; angr-5zw8 (Phase 1.4, wire strchr SimProcedure via MultiwriteAnnotation detection) depends on 1.3 and closing it closes angr-czph. Dependencies wired so 'bd ready' surfaces the right next step. Reference doc: docs/advanced-topics/rust_lazy_memory_design.rst.

DCAS implementation trick (interpreter_cb/statements.rs:execute_cas_stmt): to load the second half at addr+sizeof(half) without mutating the per-IRSB tyenv, synthesise an IRExpr::Binop { op: IROp::Add(addr_ty), left: addr.clone(), right: Box::new(Const(U(sizeof_half))) } and pass it as the addr to a fresh IRExpr::Load. This avoids the cas-llsc-recursion-limit pitfall (RustBV cannot be wrapped back into IRExpr) by keeping everything at the IRExpr level. The same pattern reuses the Store path for cmp-true concrete writes (synth IRStmt::Store with the synthesised addr_hi_expr).

x86-64 cmpxchg16b shellcode for DCAS testing: '48 0f c7 0f' = cmpxchg16b [rdi]. VEX lifts this to a CAS statement with old_hi/expdHi/dataHi populated (the DCAS form: 'CASle(addr :: (rax,rdx)->(rbx,rcx))'). VEX inserts an alignment guard before the CAS: 'if rdi & 0xf != 0, Ijk_SigSEGV', so test memory must be 16-byte aligned. To avoid exploration explosion from the trailing 'ret' popping a symbolic rsp, set rsp to a concrete writable address. Used by test_dcas_increments_unsupported_counter (angr-f58x).

Dead-code placeholder semantics in MIPS arch (2026-06-01): the '#[allow(dead_code)] // see angr-NNNN' pattern on register-offset modules (e.g. native/angr/src/arch/mips.rs:18 was offsets32, :101 is offsets64) does NOT always mean the entries are unreachable from dispatch — it may also mean 'no end-to-end Python test exercises this family yet'. The pattern was inherited from the 2026-05-31 dead-code-bd-ticket-policy audit. Before doing wiring work, first verify by removing the attribute and running cargo check --release: if the build is clean, the dispatch is already complete and the task is reduced to adding integration tests. If warnings appear, then the per-entry wiring (canonical or alias tables) actually needs to be expanded. This shortcut saved ~30 min on angr-w2gj.1.

RustSimState::export_changes existed as the symmetric counterpart to apply_changes but had zero live callers — only apply_changes is used (in exploration::pending_callback_complete to write Python-side register/memory deltas back to Rust). Removed in angr-xvnz. If you need the export side again, rebuild it on top of memory's get_dirty_page_addrs() path; do NOT reintroduce a register dirty bitset on RustSimState.

Deletion safety check for dead boundary-code: when bd points at a 'may diverge but is not used' fallback path, verify the callsite is truly gone before deletion (not just commented out). For angr-jufh, _sync_exported_constraints had its only callsite replaced with a 3-line skip comment in angr-34w.22; the dead method stayed for 4+ months. After deletion verify by (1) grep -n for the method name (only definition remains), (2) the FFI it uses (export_state_constraints) still has live callers via RustStateProxy and rust_manager, (3) full pytest tests/engines/test_rust_exploration.py is green. Pattern reusable for the rest of rust-write-through-supersedes-diff-push paths: rust_state_export.py:715-747 memory writeback, 618-662 callstack reconstruction, 2906-2948 triple-pass constraint sync (angr-tvpk).

When a bd ticket describes 'wire up dead function X', first check whether X has been SUPERSEDED by a related function (e.g. X_cached, X_v2). Pattern in this repo: lazy/cached refactors leave the original behind under #[allow(dead_code)] because the surrounding doc-comments still reference it by the dead name. If superseded: delete dead copy + refresh stale doc-comments + close ticket as 'intent realized elsewhere'. Don't try to 'wire it up' if the wiring already exists on the better copy. Two cases observed: angr-hyj0 (build_z3_ast vs build_z3_ast_cached, iter 27) and any future X_cached pattern. The dead-code-bd-ticket-policy memory covers the bd-ticket discipline; this memory covers the 'is it really dead, or is it a stale duplicate of live code' distinction.

deadend_pending_callback() was dropping deferred forks — unexplored branches accumulated during VEX block execution before exit/abort calls were silently lost. Fixed in commit 25b3244f4 by processing deferred forks before deadending. Both copies fixed (resume.rs and mod.rs). Same pattern exists in resume_after_error() but left unfixed as errors are exceptional.

Debugging tip from angr-ryf6 (2026-06-06): When tracking a Rust callsite via std::backtrace::Backtrace::force_capture(), the trampoline backtrace frames show the entry function name correctly BUT verifying that the entry-point eprintln fires is necessary. If the backtrace shows path X but the entry trace of X never fires, the call is most likely going through an UNINSTRUMENTED Python caller that passes through a DIFFERENT entry point (e.g., a PyO3 method on PyRustSimState wasn't checked, or set_state_memory_concrete's caller passes addr inside a 4096-byte range that chunks into 256 16-byte stores — the entry log shows addr=PAGE_BASE but the chunked store sees PAGE_BASE+offset). Always look at the FULL entry-log addresses and compute if any could chunk-to-hit the target. Specifically: in baby-re investigation, set_state_memory_concrete(addr=0x7ffffffef000, len=4096) chunks into 256 stores; the clobber addrs 0x7ffffffeff00-0x7ffffffeff40 lie inside this page so all 5 clobbers come from ONE Python call, not 5 separate calls. Iter 8's elimination of FFI sites missed this because the entry trace only checked addr in clobber range, not addr+offset hitting clobber via chunk loop. Lesson: when chunked, the entry trace must check addr <= TARGET < addr+data.len(), not addr in TARGET range.

Decision-brief offline-prepare pattern (Pattern D in tools/OFFLINE_WORKFLOWS.md). Use when a bd bead is blocked on a binary decision between two viable paths, neither safe to apply autonomously from the loop (e.g. flipping a default Cargo feature with unverifiable wheel-build risk, vs. a cross-repo alternative with friction). Blocker is judgement, not access/data/sibling. Artifacts: tools/decisions/_.md with required sections (Status / Context / Options / Recommendation / Implementation sketch / Resolved). UNLIKE patterns A-C: no new slice bead filed. The brief IS the slice deliverable; bead notes updated to point at the brief; bead stays blocked until the next interactive iter applies the chosen path and appends a Resolved: line. First use: angr-75mc 2026-06-06 iter 284 (xmllint fuzzer-feature decision). Pattern doc landed alongside in tools/decisions/README.md and OFFLINE_WORKFLOWS.md decision matrix updated to four rows.

DECISION: DEFER-AGAIN for angr-6zxx (Full RustPosixState ownership) as of 2026-06-06 (loop iter 85, bead angr-7zzc).

WHY DEFER-AGAIN:

1. Practical wins ARE already captured by incremental offload. Native syscall handlers cover 30+ syscalls including the entire fd table (read/write/open/openat/close/fcntl/fcntl64/ioctl/pipe/dup/dup2/dup3, stat/fstat, brk, mmap, sim_time, signals). The Rust FileSystem struct replicates the fd table (known_paths, fd_info). Per-state stdin/stdout buffers landed (angr-nnov). Env vars, cwd, and brk are offloaded.

2. No benchmark regression traces to posix. syscall_python_fallback_count is zero on the current 22-bench corpus (per xtse.1-most-callback-types-never-fire, 2026-05-23). state.posix is only touched outside the exploration hot loop by user predicates calling .dumps(), and RustPosixProxy.dumps() already routes to get_state_fd_output() for non-stdin/stdout fds.

3. No correctness blocker from merge/widen. Posix's widen() raises SimMergeError ('Widening the system state is unsupported') in the Python plugin itself, so the merge surface has not been needed in production. SimSystemPosix.merge() is fd-by-fd merge logic that would be wholly new Rust code with no demanding consumer.

4. Risk/cost vs payoff is wrong-signed. Per angr-6zxx description: ~2k Rust LoC + ~100 Python proxy glue to replace ~700 Python LoC, multi-week. The codebase has grown substantially since c3zm (rust_state_proxy.py 2918->3153 lines, rust_manager.py 5104->5259 lines) — adding more Rust maintenance burden without observable benefit is the wrong move.

5. The (a) trigger is necessary but not sufficient. angr-c3zm's GO trigger list was '(a) angr-0z34+angr-3tek both close, proving state-sync correctness gap solved'. Those closed, BUT the implicit assumption was completion would also expose either (b) a perf regression or (c) a correctness blocker. Neither has materialized. (a) alone is the right gate to re-evaluate, not to act.

TRIGGERS TO FLIP DEFER -> GO NEXT TIME:

• A real bench shows >5% wall in posix Python paths during exploration (would need a posix_callback_count counter — could be added cheaply by instrumenting RustStateProxy.posix accesses).
• Veritesting + posix merge surfaces as a correctness blocker on a user workload.
• The fd-table divergence (Rust dup doesn't update Python state.posix.fd) breaks a real consumer (currently a documented known divergence, not blocking).
• The ~2k Rust LoC estimate shrinks to <1k due to library/helpers already added in subsequent work.

ACTION ITEMS:

• angr-6zxx remains DEFERRED — do NOT auto-reactivate.
• No new bead split.
• Replace angr-6zxx's 'NOTES' citation pointer to this memory key (decision-c3zm-2-rustposixstate-2026-06-06).

DECISION 2026-05-09 (195th loop session): RustPosixState full-migration checkpoint angr-c3zm — verdict DEFER-AGAIN. (Re-evaluation gate before angr-6zxx 'Full RustPosixState ownership: fds, files, env, cwd'.) Findings: (1) Prereqs not all closed — angr-xg0o (FD SimProcedures) closed 2026-05-08, angr-qm7w (state_cache lazy/evict) closed 2026-05-08, angr-nnov (RustStateProxy fill-out) closed 2026-05-07, BUT angr-0z34 (native amd64 read/write syscall handlers, P4) still open and explicitly blocked on Rust-side write→Python sync, AND angr-3tek (re-enable native read/write SimProcedures, P2) auto-deferred after 3 dirty iterations and gated on the same 'symbolic_objects stale cache' issue (see avoid-enabling-native-read memory). The two missing prereqs both block on the same underlying state-sync correctness gap that would also dominate a RustPosixState migration. (2) Posix surface audit (angr/state_plugins/posix.py = 702 lines): already-Rust ops are fd lifecycle (open/close/lseek/dup/dup2/pipe, all live in native/angr/src/procedures/fileops.rs), getenv/setenv/putenv (procedures/getenv.rs), posix_brk (state.rs:691), stdin_symbols (state.rs:704), environment (state.rs:718). Still-Python: full SimFileDescriptor/SimFile abstraction with claripy-backed content, stream merging (stdin/stdout/stderr SimPacketsStream), sockets + socket_queue, fstat/fstat_with_result (returns claripy BVS for size/mode), sigmask/sigprocmask (claripy AST ops), merge() (58 lines, walks fd table + streams calling SimFileDescriptor.merge), copy() (31-line deep copy). The merge/widen path is the hardest piece — touches claripy ASTs through abstractions that don't have a clean Rust mirror. (3) LoC trade re-estimate: remove ~700 Python LoC (matching bead estimate), add ~2000 Rust LoC for SimFile/SimFileDescriptor/SimPacketsStream/SimSocketStream re-implementation + merge/widen logic + claripy bridge for fstat/sigmask. Net +1300 LoC. Cost-benefit unfavorable when most callback-frequency wins (fd ops, env, brk) are already captured. (4) Test coverage: 9 posix-specific tests in test_rust_exploration.py (posix_brk round-trips, init/export sync, fd mutation across callbacks, native pipe). Coverage exists for what's already migrated, not for the proposed migration scope. (5) No bug class motivates the work — no bug memories implicate posix-plugin coupling; angrybird/asisctf/sym-write bottlenecks all pointed elsewhere. Re-evaluation triggers (flip DEFER-AGAIN → GO if any holds): (a) angr-0z34 and angr-3tek both close, demonstrating the state-sync gap is solved, OR (b) a benchmark regression traces to posix-plugin Python overhead (callback frequency for posix paths), OR (c) merge/widen for posix becomes a correctness blocker on a real example. Until then, the incremental Rust offload (fd ops, env, brk) captures the practical wins; full ownership stays deferred.

Decision (angr-vulw, 2026-06-03): RustPosixProxy will NOT add dump_fd(fd, target_fd) (writeback-to-real-OS-fd) API in v1.0. Reason: Python angr's SimSystemPosix has no such API either — it exposes dumps(fd) -> bytes and dump_file_by_path(path) only. Adding dump_fd would be a Rust-only convenience that breaks behavioral parity (the contract that lets RustExplorationManager drop in for SimulationManager). Recommended caller workaround: data = state.posix.dumps(fd); os.write(target_fd, data) — one line, works on both engines. Documented in docs/advanced-topics/rust_engine.rst v1.0 scope section (lines 113-131 as of commit c5c8b6d8b). Companion to decision-v1-single-threaded (angr-02m1, iter 57) and decision-v1-no-real-multiprocess (angr-uw2y, iter 58).

v1.0 scope decision (angr-uw2y, 2026-06-03): the Rust engine does not model real multi-process semantics (execve = state replacement with new program image, clone = kernel-level thread/process forking with shared address space, wait4 = parent blocking on child exit). This matches Python angr: angr/procedures/posix/fork.py returns a symbolic If(BoolS('fork_parent'), 1338, 0) rather than spawning a second SimState, and there are no execve/wait4 SimProcedures in angr/procedures/linux_kernel. A binary that calls execve to swap its program image is not analyzable end-to-end on either engine. Recommended workarounds: hook the syscalls to redirect control flow, or drive each constituent binary as a separate angr.Project from fuzzer-style orchestration (libafl is the documented example). Adding real multi-process modeling would require a process-table abstraction in the kernel-syscall layer that is shared with Python angr — not a Rust-engine-private feature. Doc lives in docs/advanced-topics/rust_engine.rst::v1.0 scope (lines 94-111). Companion to decision-v1-single-threaded. Closes angr-uw2y.

v1.0 scope decision (angr-02m1, 2026-06-03): the Rust engine ships single-threaded. Rationale: three independent architectural constraints block parallel exploration: (1) Rc<RefCell> in RustSimState requires Send+Sync refactor of every fork site, (2) z3-rs 0.19+ thread-local Z3 contexts mean AST handles are bound to creating thread (cross-thread shipping requires SMT-LIB serialization round-trip), (3) intentional thread_local! AST caches in claripy_bridge.rs (4 caches). Two shortcuts proven non-viable: Z3 parallel.enable=true is correctness-breaking on 4 of 6 sampled benches (angr-gfay, avoid-z3-parallel-enable), and Rc->Arc + RefCell->Mutex alone does not lift Z3 thread-locality. Recommended v2 path: snapshot-transport via the already-Send+Sync ExplorationStateSnapshot type (angr-zidj). Multi-process is also v1.0 out of scope — users distribute via fuzzer-driven orchestration (libafl). Doc lives in docs/advanced-topics/rust_engine.rst::v1.0 scope, with full audit detail in the Concurrency / Send-Sync audit section (angr-8fo6) below it. Closes angr-02m1.

declare_proc! migration batches: ...strstr/strtod 6223f6079, 12 fileops 58625274f, puts-family 53a378c58, printf/memset/strcat/strcpy 8ca0e17e5, getenv-family/read/write/rand 7877c6c16, fgets-family/strset f4c98667b. Batch 8 (fgets.rs fgets/fgetc/getchar/getc + strset.rs strpbrk/strspn/strcspn): fgets=concrete buf/size + ignored '_stream: bv'; fgetc='_stream: bv'; getchar zero-arg; getc binds 'stream: bv' and delegates NativeFgetc.call(state, std::slice::from_ref(&stream)). KEY GOTCHA -- MACRO HYGIENE: a user 'call |state| {...}' body CANNOT reference the macro-generated 'args' fn param (E0425 cannot find value args); the macro deliberately exposes only the named per-arg bindings. So a delegating proc must rebuild the slice from its named bv binding (std::slice::from_ref), not pass 'args'. ALSO: a proc body that calls ANOTHER proc's .call() (getc->NativeFgetc) resolves WITHOUT a NativeSimProcedure import in the lib (trait reachable via the macro-generated impl's def-site path) -- so fgets.rs dropped its NativeSimProcedure import entirely, but sibling _tests.rs still need explicit 'use crate::procedures::NativeSimProcedure' (and RustSimState where the proc file dropped it) since super:: no longer re-exports them. strset dropped NativeSimProcedure only (build_byte_set free fn keeps RustSimState). REMAINING convertible: strchr-family (strchr/strrchr/memchr MIXED: addr concrete + needle/char raw &args[1] -> 'bv' arg). EXCLUDE variadic. DECIDE exit arity still open.

declare_proc! migration COMPLETE (cudgw.19 closed). Final batches: fgets-family/strset f4c98667b, strchr-family 587a1d9cc, exit-family 689a1049c. EXIT-ARITY RESOLVED: exit/_exit declare '_status: bv' (NOT concrete) so symbolic status is ignored, no Python fallback -- preserves always-deadend; abort/__stack_chk_fail zero-arg; all 'no_return = true' with closure param named '_state' since bodies are just Ok(None) (avoids unused-var under -D warnings). strchr/strrchr/memchr bind search byte 'c: bv' so symbolic targets flow into ITE-chain helpers. KEY MACRO-HYGIENE RULE: a 'call |state| {...}' body CANNOT reference the generated 'args' fn param (E0425); only named per-arg bindings are visible -- a delegating proc must rebuild the slice (std::slice::from_ref(&named_bv)). When a proc file's ALL impls become macro-generated and no free helpers remain, ALL module-level imports (NativeSimProcedure/ProcedureError/RustBV/RustSimState) become unused -- drop them; sibling _tests.rs (which used super::) then need explicit 'use crate::procedures::NativeSimProcedure' plus RustSimState/RustBV as the tests reference them. EXCLUDED (still hand-written): variadic scanf/sscanf/sprintf.

test_add_constraint_raw_dedup_repeat_skips_push and test_add_constraint_raw_dedup_seeds_from_shared at native/angr/src/symbolic/context.rs both assert against the GLOBAL atomic ADD_CONSTRAINT_RAW_DEDUP_HIT_COUNT counter ('hits_after - hits_before == N'). This is racy under cargo test parallelism: the counter is process-global, so concurrent tests pollute the diff. Confirmed flaky on the rust-symex baseline (2026-06-01) at ~40% failure rate even WITHOUT any changes, just rerunning 'cargo test --release --lib add_constraint_raw_dedup'. Tests pass serially ('--test-threads=1') and Python integration is unaffected. Fix is either (a) drop the counter assertion since per-context z3_assertions/dedup_set checks are sufficient, or (b) wrap the test window in a Mutex. Not blocking — angr-6zpl shipped on top of this pre-existing flakiness.

Deep-loop harness recipe (angr-11djq.2/T1b) is documented in rust_engine.rst 'Deep-input-loop binaries (grub-class)' subsection: full four-knob stack = exploration_strategy='dfs' (set_state_selection_lifo) + LengthLimiter(drop=True) (register_length_limiter) + disable_uniqueness_filter (T1a knobs: register/disable/enabled/set_size; filter is OFF BY DEFAULT) + ZERO_FILL_UNCONSTRAINED_MEMORY/REGISTERS with a bounded BVS stdin. Smoke tests: test_deep_loop_recipe_dfs_plus_length_limiter (2-knob) and test_deep_loop_recipe_full_knob_stack (4-knob) in tests/engines/rust/test_strategy_vex.py. NOTE the uniqueness filter defaults off, so disable_uniqueness_filter() is only needed if a prior step enabled it.

defcamp_r100 baseline drift (0.229 -> 0.27 median, 17-21% over) bisected to commit 07630755c on 2026-05-11 (angr-383x 'warn-on-read for state.history.actions/.events'). That commit added _install_rust_history_warning(state) in restore_plugins_to_state, which runs on every materialized Rust-owned state. The hook is the LARGEST single contributor; disabling at HEAD recovers ~0.01s (most of the 0.04s drift is diffuse across 80+ subsequent commits). The introducing commit fixes a legitimate silent-divergence bug (TRACK*_ACTIONS users) so reverting is not appropriate. Baseline refreshed in 31a7e1846. defcamp_r100 has 0 callbacks/fallbacks, so this is pure plugin-restore overhead on a fast 0.23s bench.

defcamp_r100 trailing bytes (\xf5) in Rust output: NOT a bug. Z3 model nondeterminism — unconstrained stdin bytes get different fill values between Python (0x00) and Rust (0xf5) solver instances. Both are valid Z3 model values. posix.dumps(0) returns ALL stdin bytes including unconstrained ones. Python solve scripts use strip(b'\0\n') which removes Python's zeros but not Rust's 0xf5. Fixed in run_regression.py with output normalization.

angr-027h CADET: materializing deferred_forks at the UnconstrainedJump arm of step_state_with_skip (route main->unconstrained via push_or_drop_terminal, return forks via handle_block_end). iter-28 (clean HEAD) it diverged ~1.6 states/step unbounded -> OOM-killed the ralph runner. iter-63 UPDATE: with the new chain-break-at-find/avoid guard (commit ed600427b) in place, the SAME materialization no longer diverges catastrophically — active plateaus ~210 then climbs slowly (351@step194) instead of 493@step300 — but it STILL never reaches the easter-egg target 0x804833E and active still grows unbounded, so it remains a non-fix and was reverted again. Do NOT ship deferred-fork materialization at the unconstrained ret until the THIRD issue is solved (no fork actually takes the byte0==0x5e easter-egg path; see benchmark-cadet-convergence-two-bugs). Characterize ONLY under systemd-run --user --scope -p MemoryMax=4G -p MemorySwapMax=0 with bounded mgr.step(n=1) loops + a divergence guard (active>N abort).

Deps-bump investigation for upstream 9.2.222.dev0 (closed 2026-06-05 as 'stay pinned'). Findings: (1) z3-solver SONAME unchanged — both claripy 9.2.209 and latest released 9.2.221 pin z3-solver==4.13.0.0, so the originally-feared shared-Z3-context break is dormant. (2) Upstream's 9.2.222.dev0 isn't on PyPI; reproducing it needs source builds of angr/{archinfo,claripy,cle,pyvex}. (3) Upstream also bumps pypcode 3.x→4.x — major version, requires-python>=3.12 (we're already there). (4) Our .venv/ is hand-assembled via cargo-direct-copy ('pip list' shows only pip/platformdirs/rust-demangler), so any pin change requires venv rebuild not 'pip install -U'. (5) z3-solver itself has since shipped 4.14.0.0 and 4.15.0.0 on PyPI — if a future claripy release ever pins 4.14+, the SONAME concern reactivates. Decision: stay pinned at 9.2.209 until upstream cuts a stable 9.2.222+ tag on PyPI OR we migrate the venv to pip-managed. CLAUDE.md note and pyproject.toml comment updated to reflect this.

Detailed history (HistoryEntry struct) lives parallel to the existing Vec history. HistoryEntry has addr, jumpkind (u8 enum: 0=Boring,1=Call,2=Ret,3=Syscall,4=Other), jump_target. Recorded in interpreter_cb/execution.rs BlockResult::BlockEnd handler. Transferred via stepping.rs same as call_stack and registers. API: get_state_detailed_history(state_id) on manager, get_detailed_history()/get_detailed_history_str() on snapshot. Both old Vec and new Vec coexist — old is used by uniqueness filter and existing code.

angr-iaol.2 (2026-05-31, commit 47bee1722) added RustExplorationManager(deterministic=True). The PyO3 binding lives at native/angr/src/engine.rs::set_z3_global_param (cfg-gated on vex-engine-z3), a thin wrapper over z3::set_global_param (re-exported from native/z3-patched/src/params.rs:97). Python wrapper at angr/exploration/rust_manager.py::_apply_deterministic_z3_globals pins smt.random_seed=0 + sat.random_seed=0 with a module-level _z3_deterministic_applied boolean guard so repeated manager construction is a no-op. The pin is process-global once applied — solvers already in flight are NOT retroactively pinned, but every new Solver::new picks up the pin. End-to-end test TestDeterministicMode::test_fauxware_explore_stable_under_deterministic confirms fauxware (find=0x4006ed, avoid=0x4006fd) produces stable found-stash size + posix.dumps(0) across two fresh managers. Z3 4.13 still retains variable / restart heuristic latitude NOT bounded by these seeds — defcamp_r100 trailing-byte mismatch remains the canonical residual case (run_regression.py normalizes). If the fauxware test ever flakes on stdin equality, weaken to padding-tolerant equality rather than disabling. Don't add FxHashMap conversion — the existing std::HashMap audit (docs/advanced-topics/rust_engine.rst Iteration-order audit) already confirmed no site leaks iteration order into exploration output.

P4-spike-A (angr-9w6ad.10) measured whether RustExplorationManager(deterministic=True) — pinning Z3 smt/sat.random_seed=0 via Z3_global_param_set, infra from iaol.2 — collapses bimodal benchmark variance. Verdict: NARROWS but does NOT collapse. On google2016_unbreakable_1 (cheapest bimodal bench, N=8/mode): default cv=0.97 (OUTLIER, min2.07/med2.33/max12.55s) vs deterministic cv=0.61 (still BIMODAL, min0.96/med1.42/max4.49s). Seed-pin removes the worst slow flier and ~halves cv but residual multi-modality persists (Z3 4.13 variable/restart heuristic latitude unbound by random_seed; matches iaol1-seed-pin-empirically-broken). DECISION: do NOT switch the bench gate to deterministic mode — single-shot timings stay untrustworthy, slow-mode-pinned baseline + --skip-bimodal + 15% threshold still required. run_single.py and bimodal_variance.py now carry a --deterministic pass-through flag, retained as a DIAGNOSTIC knob (reproduce a slow path / A-B a candidate with one fewer noise source), not a gating default. Full table in docs/advanced-topics/rust_bimodal_variance.rst 'Deterministic-seed spike' section.

angr-df57 (.cargo/config.toml hardcoded paths) was already resolved by commit e2f9d921 (angr-8fsl) on 2026-05-08, but the bead lingered as ready/open. Verification: 'grep -rn /home/ubuntu .cargo/ native/angr/.cargo/' returned nothing, and 'cargo check --release' succeeds without any path overrides. Pattern: when a fix bead and its acceptance criteria can be answered by inspecting current files (and confirming no hardcoded paths remain), close as already-resolved rather than redoing the fix. Cross-link: angr-8fsl was the actual fix bead.

angr-dgz6 (commit 4e1077c6c, 2026-05-22): With pending_python_constraints removed, the constraint-sync flow is now ASYMMETRIC. Python→Rust: sync_constraints_from_python (helpers.rs) — claripy_to_rustbv primary, Z3 ptr fallback for FP/etc. Used by resume.rs:57 to push constraints from Python into Rust after SimProcedure callbacks. Rust→Python: there is NO direct push. Instead rust_callback_dispatch._install_rust_solver_on_callback_state monkey-patches state.solver on the Python callback state to delegate to the Rust solver context — constraints never cross the FFI in this direction. The 'rust_ctx_missing' counter in mgr.stats is the lone defensive telemetry: increments when Path A can't install (rust_ctx is None), in which case the path returns silently rather than falling back to FFI replay (the fallback removed in angr-h0dv). Net diff over dgz6: -364/+15 lines, 8 files (constraints.rs deleted entirely).

disk-cache-symbolic-guard

Persistent disk cache for Python init at ~/.cache/angr_rust_init/. Key: MD5 of binary file content. Stores: addr, register values, stack page bytes, continuation addrs. Restore: ~3ms via blank_state + register/memory set. Cache file: ~356 bytes. Cold init: ~180-250ms. Warm init: ~3ms. Only caches concrete state data — symbolic args from user state are transferred via solver.constraints. Works across processes (unlike the in-process _init_cache).

DivModU128to64 (0x146A) and DivModS128to64 (0x146B) were missing from the Rust VEX interpreter until commit 51e46b325. Any x86_64 binary using 'div r64' or 'idiv r64' (common for VLA alignment, struct size computation, etc.) would silently get zero from the division, corrupting downstream calculations. The VEX IR decomposes these as: 64HLto128(rdx,rax) then DivModU128to64(dividend128, divisor64), with 128to64/128HIto64 to extract quotient/remainder.

angr-11djq.7 (RustPosixState fd/file sync) evidence gate is NOT satisfiable by write_stream_heavy. That bench exercises WRITE-side stdio (fputs/fputc/fwrite) against cle stdout/stderr FILE* externs -> ProcedureError::Memory fallbacks in read_fileno_for_stream; it never opens/reads real files, so it produces ZERO syscall fd-sync fallbacks. .7 needs a harness that open()/read()s a pre-seeded FILE on one side and checks cross-side visibility (T2-MEASURE punted grub for this; xmllint_getenv showed 0 syscall fallbacks too). Do NOT 'measure write_stream_heavy to justify .7' — wrong layer. See t2-measure-xmllint-fallback-profile, write-stream-heavy-bench.

doc/citation-rot audit of rust-symex (2026-06-20/21, bead angr-hd71z, COMPLETE). 23 verified stale citations. CODE doc-comments (angr-hd71z.1, 5): claripy_bridge.rs:91 interpreter_cb/->interpreter/; _constants.py:4 memory.rs->memory/page.rs; rust_manager.py:269 SimSymbolicMemory->memory_mixins/address_concretization_mixin.py; rust_state_proxy.py:1622 detailed_history exploration/mod.rs->state.rs:3313; rust_manager.py:316 load_concrete_lazy line drift. DOCS (angr-hd71z.2, 7): rust_vex_ops.rst ir.rs->ir/ops_def.rs & VEXOps::triop->ternop; rust_engine.rst py_get_execution_stats->get_execution_stats & add_constraint_tracked_ast line drift; CLAUDE.md:65/172 & rust_bimodal_variance.rst:545 'four bimodal'->FIVE (adds CADET_00001_partial). BD-MEMORY BODIES (angr-hd71z.3, 11): 2x libpyvex_ffi.rs GONE->pyvex_bridge.rs (invariant-cas-oldhi-sentinel, invariant-non-ffi-unsafe-safety-comments); many vex/ir.rs->vex/ir/ (commit 327f12229 split landed: gotcha-endness-variants, invariant-vex-fcmpkind/packed-fp/sse-scalar/binop-misroute/vsetelem); memory/tests.rs->memory/tests/ dir (pending-writes-scaffold, invariant-multi-vs-symbolic). REJECTED: rust_engine.rst:1342 lineage_assumptions.rs (intentional deleted-spike historical citation). Bucket fully verified - no re-run needed.

docs/advanced-topics/rust_engine.rst now has a 'Counter prevalence across the fast-tier corpus' subsection (commit a031ee509, after 'Pipeline instrumentation counters', before 'ANGR_Z3_TACTIC') that consolidates the 5 fast-tier sweep findings (syscall/simproc fallback zero, concretize/add_constraint_raw dedup/mem ITE concentrated on 2-3 outlier benches) into a single user-facing reference table. When future sweeps land, update that table rather than duplicating into a new section. Avoids fragmenting corpus-profile info across the docs.

docs/extending-angr/native_coverage_matrix.rst is the in-tree authoritative index for native SimProcedure registry contents AND per-arch syscall coverage (AMD64/X86/ARM/ARM64/MIPS32/MIPS64). Sourced from bd memories bench-simprocedure-fallback-distribution (angr-twyr) and bench-syscall-fallback-zero-coverage (angr-0wam). Refresh whenever NativeProcedureRegistry::new or any register_syscalls!() block in syscalls/mod.rs changes — those code edits are the source of truth, the doc tracks them. Cross-linked from docs/extending-angr/index.rst toctree and from the Overview bullets of docs/advanced-topics/rust_engine.rst.

Docs .rst cross-ref audit (iter61) — CLEAN. Method: extract ':doc:...' and ':ref:...' from docs/advanced-topics/rust_.rst + docs/extending-angr/rust_.rst + simprocedures.rst; verify each :doc: target resolves to a .rst file, each :ref: label has a matching '.. _label:' def (grep across all docs), and explicit cross-doc section-title refs (e.g. 'advanced-topics/structured_data:Working with Calling Conventions', 'core-concepts/loading:Loading a Binary') point at headings that exist. All 9 :doc: targets, 5 named :ref: labels, and 2 section-title refs resolved. Zero stale. Completes the citation-hygiene sweep series: docs file-paths (iter58), bd-memory file-paths (iter59), bd-memory symbol anchors (iter60), docs .rst cross-refs (iter61). Remaining un-swept surface: memory->memory cross-refs ('see X'/[[wikilink]] keys still exist?).

Docs sweep audit cadence: after every test/benchmark refresh commit, re-grep 'def test_' and re-count baseline_timings.json keys to verify CLAUDE.md is in sync. The two values drift quickly because new tests / benchmarks land frequently. The previous angr-k25z refresh on 2026-05-11 was already 4 tests stale by 2026-05-13 (3 unsat_core via angr-w2je + 1 NEON via angr-bkcs.2). When auditing the arch matrix, the AMD64 column is approximate (~110 unit, ~268 integration) but the experimental-arch columns are exact and should be derived by hand-counting tests in TestMultiArchSupport plus any per-arch outliers in other classes (e.g. test_x86_native_procedure_returns_to_eax_not_edx in TestRustExplorationManagerUnit).

RustVEXEngine and NativeVEXLifter are dormant scaffolding, not the active exploration path. vex_engine.RustVEXEngine is exposed via PyO3 (execute_irsb_json/step/start_block/add_imark) but no Python code in angr/ imports or calls it — grep 'RustVEXEngine' across angr/*.py returns nothing. NativeVEXLifter (native/angr/src/vex/lifter.rs) is only re-exported in vex/mod.rs and never instantiated. The production hot path: stepping calls into interpreter_cb (native/angr/src/interpreter_cb/mod.rs) whose block_cache is already LruCache<u64, Arc>, and exploration/stepping.rs::updated_block_cache is also Arc. Future 'IRSB clone' beads should profile the hot path first — do not assume engine.rs or lifter.rs are hot. Closed angr-0ie2 on this basis 2026-05-22.

Drift-detector one-liner for symbolic/context.rs cfg-gating hygiene (angr-iclt audit): 'for f in "" vex-engine automaton; do echo === ===; cargo check --manifest-path native/angr/Cargo.toml --no-default-features --features "$f" 2>&1 | grep -E "never (used|read)"; done' — should print nothing under each combo. Non-empty output means a new Z3-only symbol leaked out of cfg gating (or a stub became dead and should be removed). The 'vex-engine,vex-engine-z3' combo never has this problem because Z3 paths are the live code.

DRY-test audit 2026-06-12 (branch rust-symex): filed 6 beads labeled tests,dry-tests — angr-3bth (hoist 354 inline RustExplorationManager imports + 92 skipif decorators in test_rust_exploration.py, P2), angr-evu3 (collapse 6 Gate classes' 24 verbatim gate-toggle tests into one parametrized table, P2; coordinate with vacuous beads angr-azsh/angr-e548 same regions), angr-7gdp (create tests/engines/conftest.py: availability guard x6 files, fauxware_project fixture x2, path resolution x4, BufferedStringIO x2, P2), angr-k8pc (merge two factory monkey-patch impls keeping caller-stack fallback, P3, deps angr-7gdp), angr-zdih (Rust: file_path.rs 62x state setup + 30x error-match blocks; promote 8 procedures setup_ helpers to shared builders, P3), angr-ec82 (Rust: vex/ops.rs ~57 SIMD lane tests / 123 pack lines -> pack/unpack/assert helpers; exp arrays MUST stay inline independent constants, P3). DELIBERATELY EXCLUDED — do not re-file: wrapping SymContext::new_mock() (410 calls but one idiomatic line, no gain); macro-based test generation (hurts debuggability); tiny 3-test parametrize in test_factory_rust_inheritance.py (churn > win, angr-9dvt touches same file); splitting the 18k-line test_rust_exploration.py (high churn — revisit as its own decision bead only after angr-3bth + angr-7gdp land, noted in angr-3bth). Agent counts were inflated again (claimed 481 inline imports, actual 354) — always re-verify by grep.

DRY-tests trio complete: angr-7gdp (conftest dedupe), angr-evu3 (parametrized *Gate toggle table), angr-3bth (module-level RustExplorationManager import + pytestmark skipif). test_rust_exploration.py imports RustExplorationManager from tests.engines.conftest now — do NOT re-add in-body 'from angr.exploration import RustExplorationManager' in new tests, and do NOT decorate test classes with @pytest.mark.skipif(not RUST_EXPLORATION_AVAILABLE) (the module-level pytestmark covers it). A whole-file split into themed modules was deliberately deferred (high churn) — revisit as its own decision bead.

DS-spike.3 (angr-11djq.14.3) decision: NO-GO/DEFER on native directed-search priority-queue (DS-impl angr-11djq.15). Native priority-queue cannot beat BFS on peak memory by reordering alone — a real state-count win requires DISCARDING beam overflow (not deferring), which risks completeness (greedy trap drops the only viable path when correct/wrong successors share CFG distance). RSS on small binaries is Z3/CFG-warmup-dominated, no signal. The Python DirectedSearch technique (angr/exploration_techniques/directed_search.py, .14.2) is the SHIPPED directed-search deliverable — it captures the only measured win (smaller per-round active frontier => stepping CPU) at the orchestration layer with no engine change. .15 deferred (until 2026-12-01) behind an undefer GATE: a CF-divergent real target (xmllint/grub proxy, NOT data-dependent CTF) where beam>1 + bounded discard beats BFS/DFS on peak_total/RSS. Merging (.10) NOT reopened: directed search is unmeasured at scale, not proven insufficient.

angr-dtrl (commit 216d764e2, 2026-06-01): add_constraint_raw_dedup counter audit. Hit-rate is BIMODAL across the fast-tier corpus, not null. 4/15 benches show 31–92% dedup hits (defcon2016quals_baby-re 92.3%, csaw_wyvern 82.5%, whitehatvn2015_re400 50%, flareon2015_5 31.3%); 11/15 are 0% (mostly benches with small or zero add_constraint_raw_total). The original angr-sfp9 wall-clock A/B was null because Z3 internally dedups asserts so the saved solver.assert is a no-op — but the skipped Bool::clone + z3_assertions.push keep constraint-export and lineage-switch work proportional to unique facts. Counter+HashSet retained. Decision documented in docs/advanced-topics/rust_engine.rst::Pipeline instrumentation counters under Constraint add path.

emit_extract_z3_cached (value_z3.rs) cannot be deduped against RustBV::extract_into by delegating 'inner.extract_no_ctx(high,low).to_z3_ast_cached()': that INFINITE-LOOPS. extract_no_ctx returns a RustBV::Extract node for the default case; to_z3 of an Extract node re-enters build_z3_ast_cached's BVOp::Extract arm -> emit_extract_z3_cached with the SAME (inner,high,low) -> loop. RESOLVED in angr-ph300.81: the dedup uses value_ops::drive_extract driven by the ExtractTarget trait; ExtractTarget::recurse routes back through drive_extract (NOT to_z3 of a reconstructed node), and the Z3 default terminal applies z3 .extract() to the built inner AST directly. See extract-driver-unified. The concrete fold is also shared via bv_concrete::concrete_extract_u128 (moved from bv_codec into ungated symbolic/bv_concrete.rs in angr-1yge9.14 so it builds under --no-default-features; angr-ph300.36).

When you need RUST_LOG-style per-module log filters in the Rust extension WITHOUT pulling env_logger's full default features (termcolor/atty/humantime/regex), depend on 'env_logger = { version = "0.8", default-features = false }' and use only the public env_logger::filter::{Builder, Filter} types. Builder::parse(spec) handles single-word levels and full specs like 'rustylib::stash=warn,info'; Filter::enabled/matches gate the log path; Filter::filter() returns the max LevelFilter for log::set_max_level(). The 'regex' feature gates only the /regex part of the spec syntax — basic and per-module filters work without it. env_logger 0.8.4 is already in Cargo.lock as a quickcheck transitive dep so adding a direct version=0.8 dep is offline-safe.

Env-var toggle audit (angr-0mqkc.4): all rust-symex env toggles are LIVE, none dead. Z3 toggles (ANGR_Z3_SIMPLIFY_STRIDE/PARAMS/TACTIC/QFBV_THRESHOLD) documented in docs/advanced-topics/rust_engine.rst; parallel toggles (ANGR_PARALLEL_WORKERS, RUST_PARALLEL_WORKERS/SHADOW_PROBE/STEADY, ANGR_MIGRATE_PHASE_TIMERS) in rust_parallel_design.rst + tests/gates. ANGR_Z3_PARAMS is wired via extra_params_spec()->apply_extra_params in solver_build.rs build_solver_params (production, called every fresh solver); it is an A/B param-survey knob for angr-ovqja, appends comma-sep key=value after baked defaults, unparseable entries skipped silently.

Environment has no working virtualenv — networkx and other angr dependencies are missing. Python tests cannot be run. Only Rust cargo check and Python AST parse validation are possible. Previous sessions (angr-ir12, angr-87ya) had the same constraint.

env-venv-recovery-procedure

error-handling consistency audit of rust-symex (2026-06-20, bead angr-ghwsd). 12 error enums, mostly clean (6 Result<,String>, 3 map_err(||)). CONFIRMED (boundary, medium): 'invalid handle id' PyRuntimeError in 34 sites vs PyValueError in 1 (solver.rs:754/815, pending_api.rs:159 - standardize via helper); From for PyErr flattens 4 variants to PyRuntimeError (solver.rs:74, claripy_bridge.rs:409/425 - map per-variant); RustExecError->PyErr taxonomy (errors.rs:103) wired only to test harness not live path. CONFIRMED (low): ExtractionError+ConstraintSyncError hand-roll Display vs thiserror; SnapshotError::Decode mislabels unknown-arch (add UnknownArch variant); DeserializeError->CbExecutionError::LiftError bypasses InvalidIR taxonomy; CbExecutionError::TypeMismatch is a DEAD variant dup of OpError::TypeMismatch. REJECTED (do NOT re-flag): CbExecutionError::Memory String-flatten (routes to Panic by design), #[non_exhaustive] split (documented API group angr-irwe), DeserializeError no-Clone (serde_json forced), register-not-found PyKeyError vs PyValueError.

eval_expr_with_callbacks_inner refactor (angr-u7v5, commit e6c81f093): the original 411-LOC match in native/angr/src/interpreter/expressions.rs was split into 8 per-arm helpers on VEXInterpreter (eval_load, eval_unop, eval_binop, eval_ite, eval_geti, eval_triop, eval_qop, eval_ccall). The Load arm got two additional sub-helpers — load_concrete_addr (fast paths: pending_symbolic_stores -> pending_stores.try_load -> all_flushed_symbolic_stores -> all_flushed_stores -> load_prefetch_cache -> try_read_concrete_memory -> load_from_callback, must stay in THIS ORDER) and load_symbolic_addr (concretize -> dispatch by ConcretizationResult shape). Why so many helpers vs one giant 'eval_op_dispatch': IROp is Copy but each arity (unop/binop/triop/qop) has different result_type/fallback-counter/format-string logic, so a single helper would need a giant match on arity inside. Small arms (Const/RdTmp/Get/VECRET|GSPTR, all <=6 LOC) stay INLINE in the dispatcher — extracting them would add boilerplate without reducing nesting. Required imports added to expressions.rs: use crate::vex::ir::{IRCallee, IRRegArray} (mod.rs only re-exports IRType/IROp/etc, not these). Pattern: when iropclass(op) was &IROp in the original match, pass IROp by value into the helper (Copy) and call iropclass(&op) inside.

eval_upto returned Vec which truncated BVS > 128 bits to lower 128 bits. For whitehatvn (296-bit arg1), first 21 bytes were zeros. Fixed by adding eval_upto_wide path in solver.rs that uses extract_bv_value_wide (full precision via Z3 string parsing) and returns PyObject. Also needed make_bv_from_bytes for exclusion constraints. eval() already had eval_wide path — only eval_upto was missing.

extract_concrete_arg helper was defined in native/angr/src/procedures/mod.rs:97 but had zero callers. Spread across 21 procedure files using the verbose ok_or_else pattern instead. Refactor to use the helper saved 261 lines net (139+/400-) without changing any tests. Lesson: check existing helpers before assuming inline boilerplate is necessary.

Exit continuation cache: after first SimProcedure callback where ALL successors have Ijk_Exit jumpkind, cache that address in _exit_continuation_addrs. Subsequent callbacks at same address skip state creation entirely and use deadend_pending_callback(). Key example: __libc_start_main after_main→exit(0). Reduced ais3 from 118 to 47 callbacks, 1.58s→0.73s. Combined with deadend_pending_callback() Rust method that directly pushes pending state to deadended stash (vs resume_after_simprocedure(0,None,None) which goes through full apply_changes path).

exploration dedup cluster 2 (angr-24pv4.5, iter33): prepare_shared_callback_solver(state: &RustSimState, deferred_forks: &[DeferredFork]) -> (Option, RustSolverContext) in exploration/helpers.rs (free fn, called as super::helpers::prepare_shared_callback_solver). Collapses the snapshot-if-deferred-forks + from_shared_sym_context prelude duplicated at 4 stepping.rs Python-callback exits. DELIBERATELY NOT migrated: the Hook arm (handle hook path) keeps its inline copy because it brackets the snapshot with solver_fork_time_ns/solver_fork_count profiling timing — folding it in would either drop that timing or add it to the other 4 sites (a stats behavior change); symbolic-branch + VEX-fallback exits pass (None,None) and never wrap a solver. Free helpers in exploration/helpers.rs are NOT glob-re-exported (mod.rs has bare 'mod helpers;'), so siblings must call them as super::helpers::NAME.

exploration dedup cluster 4 (angr-24pv4.5, iter34, FINAL cluster — bead now closed): free fn build_unexplored_fork(base: &RustSimState, fork: &DeferredFork, condition: &RustBV, snapshots: &mut FxHashMap<u64, crate::interpreter::BranchSnapshot>) -> RustSimState in exploration/helpers.rs. Encapsulates the byte-identical 3-way deferred-fork core: snapshot.remove -> fork_from_snapshot + assume_OPPOSITE side | path_taken -> fork_false | else -> fork_true; then set_pc(unexplored_target). Replaced 6 open-coded copies: materialize_deferred_forks + process_deferred_forks_into (stepping.rs), run_loop.rs callback-resume loop, resume.rs x3 (resume_after_simprocedure final loop, deadend loop, resume_after_symbolic_branch deferred_successors). Callers KEEP their own surrounding logic the helper does NOT absorb: base assume_true/false of taken-path cond, set_root lineage, profiling counters, P11 claripy_to_rustbv reconstruction, and SAT/UNSAT routing (returned Vec / push_to_active_or_drop / route_successor / deferred_successors+pruned). BranchSnapshot must be fully-qualified crate::interpreter::BranchSnapshot (helpers.rs use super::* does NOT re-export stepping.rs's import). Called as super::helpers::build_unexplored_fork.

exploration dedup helpers (angr-24pv4.5): root_or_self on StashManager (stash.rs, near get_root) collapses get_root(id).unwrap_or(id) lineage idiom — used by ~8 sites in resume/stepping/run_loop. apply_deferred_fork_constraints is a FREE fn in exploration/callback_types.rs (re-exported via exploration/mod.rs), NOT a &self method on PendingCallback: the resume_after_simprocedure site calls it AFTER pending.state is moved out (let mut state = pending.state), so a &self method fails to borrow; it takes (state, &deferred_forks, &stored_conditions) borrows instead. u128_to_le_bytes is the read-side LE unpack counterpart of store_concrete_bytes_chunked's pack loop — both moved from exploration/helpers.rs to symbolic/bv_chunk.rs in angr-9ke6b.230 (see invariant-chunked-concrete-memory-read).

exploration helpers_tests.rs unit-test patterns (szg45.3): all 4 RustExplorationManager helper gaps are pure-Rust-unit-testable without a .so rebuild or Python integration harness. (1) extract_procedure_args stack-spill — mirror extract_syscall_args tests: set 6 amd64 arg regs (RDI=72,RSI=64,RDX=32,RCX=24,R8=80,R9=88) via set_register_by_offset, map_memory+set_sp+memory_store args 7,8 at sp+8/sp+16 (stack_arg_offset=8 skips return addr), request 8 args; symbolic SP -> ExtractionError::SpSymbolic; concrete-but-unmapped SP -> StackUnmapped{arg_index:6, addr:sp+8}. (2) compute_register_tuple_hash — set mgr.constraint_tracker.uniqueness_registers=vec![reg] directly (pub(crate)), call mgr.compute_register_tuple_hash(&state); symbolic sentinel (MAX+1u8) != concrete u64::MAX, missing register (bogus name -> 0u64) distinct from both. (3) apply_uniqueness_filter — mgr.sm.push(STASH_ACTIVE,state) dup register values, mgr.sm.set_drop_terminal_states(true/false) toggles move-to-'not_unique' vs discard. (4) _resume_after_error — construct PendingCallback{state,reason:CallbackReason::Error{message},rest None/default,FxHashMap::default()}, set mgr.pending_callback=Some(..), assert get_errors()==[(pc,msg,state_id)] and STASH_ERRORED stash; no-pending -> PyRuntimeError (needs Python::initialize() then Python::attach, NOT deprecated with_gil).

exploration/helpers.rs has two dedup helpers added for 24pv4.5: (1) route_successor(&mut self, state, gate_found_on_sat: bool) centralizes the find_addrs->STASH_FOUND / avoid_addrs->push_or_drop_terminal(STASH_AVOID) / else->push_to_active_or_drop PC-dispatch triplet. gate_found_on_sat=true for run_loop.rs successor+loop-exit sites (gate FOUND on lazy_solves||satisfiable()), false for resume.rs sites where sat is already established upstream. NOTE: the active_states-buffering sites in resume.rs _resume_after_symbolic_branch (true/false pair + deferred loop) were intentionally NOT migrated — they buffer into a local Vec drained later, and switching to route_successor's immediate push changes pruned/active interleave ordering (the audit flagged this as the only non-trivial part). (2) store_concrete_bytes_chunked(addr, data, sink) — the canonical angr-5aj8 u128-overflow-safe 16-byte-chunk pack+store loop; sink closure abstracts the memory API + error mapping. Used by _set_state_memory_concrete, _pending_memory_store, _set_pending_memory (the last had a latent >16-byte truncation bug, now fixed) and state/pymethods.rs::memory_store. RELOCATED: since angr-9ke6b.230 it lives in symbolic/bv_chunk.rs (re-exported as crate::symbolic::store_concrete_bytes_chunked), NOT exploration/helpers.rs — see invariant-chunked-concrete-memory-read. Remaining 24pv4.5 clusters: 2 (need_callback_with_shared_solver in stepping.rs, Hook arm has profiling complication), 4 (deferred-fork materialization, delegate to process_deferred_forks_into), plus others.

ROOT CAUSE: _explore_with_predicates() in angr/exploration/rust_manager.py historically only checked _predicate_found (Python predicate matches) for termination. But when find=int is used with use_technique() — even non-predicate techniques like DFS — _active_techniques is non-empty, so explore() routes through _explore_with_predicates instead of _explore_with_addresses. _explore_with_addresses checks event.event_type=='found' AND event.found_count>=num_find; _explore_with_predicates didn't, causing infinite loops. Fixed in commit ea19b178d by switching the check to _found_count() which counts both Rust-native and Python-predicate finds. INVARIANT for future work: any new exploration loop in rust_manager.py must terminate on EITHER (a) Python predicate match OR (b) Rust-native find_addr hit (event_type=='found') OR (c) all paths exhausted (active_empty / has_active_states=false).

export.rs BVOp::Reverse arm (rustbv_to_claripy_memo) is only reachable from a native RustBV Reverse node — symbolic htonl/htons via procedures/byteorder.rs host_network_swap (reverse(extract).zero_extend). A CONCRETE arg folds the reverse to a BVV, and claripy.Reverse imports as a Concat-of-extracts that exports verbatim from the reverse cache, so neither the concrete proc path nor an import roundtrip hits it. Test harness: TestSymbolicLibcProcedures in tests/engines/rust/test_procedures.py (hook posix htonl, symbolic rdi constrained, run 1 step, read s.regs.rax). Assert s.regs.rax.variables non-empty to guard against a silent concrete-fold that would bypass the export arm.

Implemented 5 expression canonicalization rules in value.rs extract() and build_z3_ast(): (1) Extract(Extract)→fused, (2) Extract(Concat)→distributed, (3) Extract(Reverse)→byte-reindex eliminates Reverse, (4) identity Extract(w-1,0,x)→x, (5) Reverse(Concat)→Concat(Reverse(b),Reverse(a)). These match claripy's automatic simplifications. Concat flattening is separate (in build_z3_ast BVOp::Concat case).

RustBV value.rs now has 17 eager simplification rules applied during expression construction: x+0→x, x-0→x, x0→0, x1→x, x&0→0, x&1s→x, x|0→x, x|1s→1s, x^0→x, not(not(x))→x, neg(neg(x))→x, reverse(reverse(x))→x, shift-by-zero→x, 0-shift→0, sign_extend(same_width)→identity, Extract(ZeroExt)→simplified, Extract(SignExt)→simplified. These complement the existing Extract canonicalization (Extract(Extract), Extract(Concat), Extract(Reverse)). Added in commit 6f5518426.

angr-1q6h fix (commit d5671f249, 2026-05-31): extract_procedure_args / extract_syscall_args in exploration/helpers.rs now return Result<Vec, ExtractionError> instead of silently pushing RustBV::zero on symbolic SP / unmapped stack / register-overflow. Reuses arch::calling_conventions::ExtractionError + adds new RegisterOverflow{requested,available} variant. Callers at stepping.rs:209 (syscall), stepping.rs:559 (simproc), run_loop.rs:229 (simproc) all treat Err the same as ProcedureError from native_proc.call: bump python_fallbacks counter, log debug, fall through to Python callback. This is the production path that mirrors the angr-ydli trait-method fix (c858f7e5b) — same conceptual silent-fabrication bug, parallel code path. The trait method is unused in production (only caller is interpreter/mod.rs::extract_simprocedure_args wrapper) so the helpers.rs fix is where it actually matters.

Discovered while fixing angr-ydli (calling_conventions::extract_args silent symbolic fabrication, 2026-05-31): the trait method CallingConvention::extract_args is effectively dead code in production — its only caller is the unused wrapper VEXInterpreter::extract_simprocedure_args in interpreter/mod.rs. Real procedure-arg extraction goes through RustExplorationManager::extract_procedure_args / extract_syscall_args in exploration/helpers.rs:570/614 (callers: stepping.rs:559, run_loop.rs:229). Those have a SEPARATE silent-fabrication footgun (push RustBV::zero on stack-load failure, not symbolic). Same conceptual bug, different code path. Fix for the trait method landed; helpers.rs path still needs the same Result-based API. Worth a follow-up bead if procedures grow rely on real stack args.

extract_ite_targets (interpreter/helpers.rs) unit-test pattern: build inputs with a local ite_bv(t,f) helper -> RustBV::Expression{id:RustBV::EXPRESSION_ID, width:64, op:BVOp::Ite, operands:Arc::from(vec![dummy_cond, t, f])}. The fn never inspects operands[0] (condition), only pushes [1]/[2], so cond can be any RustBV::concrete. Constrained leaf {id,value,width} counts as a concrete target; any non-Ite Expression (e.g. BVOp::Add) or Symbolic leaf hits the _ => None arm. max_targets cutoff fires when targets.len() exceeds it mid-walk (>, not >=). Tests live in helpers_tests.rs (use super::*; pub(super) fn is in scope).

Extract(Reverse(x)) multi-byte rewrite bug (fixed 2026-05-19 in angr-p8cz, commit 2870a3429): the original Rule 3 in value.rs::extract_into returned plain Extract(w-1-low, w-1-high, x) for byte-aligned Extract over Reverse(x). Correct only for a SINGLE byte. For multi-byte ranges the byte ordering needed reversing too — the correct rewrite is Reverse(Extract(w-1-low, w-1-high, x)), which a single-byte case still trivially collapses to plain Extract because Reverse on 8 bits is identity. The original rule was latent because no test or production path triggered it with multi-byte byte-aligned bounds. Whenever a rewrite mentions byte-aligned-only, ask whether the byte ORDER also needs adjustment, not just the bit range.

fairlight Z3 bottleneck (per-site profiling 2026-05-05 HEAD=fee4ea333, run_single.py): Total 12.9-14.0s; Z3 ~95% of total. z3_check umbrella 12.3-13.3s across 35 calls. Top sites: z3_site_branch_true 9.1-10.6s/13 calls (~700-820ms/call), z3_site_branch_false 1.2-2.1s/2 calls, z3_site_satisfiable 1.0-1.3s/16 calls. Interpreter is negligible: expr_eval 11109 calls/14ms, lift 51ms, python_callback 109/46ms, FFI crossings 3. Binary has 616 xmm instructions — confirmed FP-theory dominates. branch_true high per-call cost suggests path-condition accumulation is the lever, not raw FP-op cost.

fairlight 0.47x regression is dominated by Rust VEX block_exec (13.9s for 8102 stmts). 28 rand() calls now handled natively (saved 9s Python callback overhead). 14 exit() calls use fast-path deadend (saved 3s state creation). But Rust interpreter execution time grew proportionally — total time unchanged at 22s. The Rust VEX interpreter is slower than Python's SimEngine for symbolic-heavy blocks. Not fixable without fundamental interpreter optimization (constant folding, expression simplification, or replacing interpreter with JIT).

Fallback parity harness (angr-op0dn.14.1.2): tests/engines/rust/test_fallback_parity.py diffs a bounced/native SimProcedure call on RustExplorationManager against the pure-Python engine from the SAME blank_state, hooking angr's Python proc at fauxware's 0x4008C0 (mapped-but-unexecuted, so run_python_init_if_needed short-circuits). Observables that actually compare cleanly across engines: solver.min/max of rax (works for symbolic returns like time/getenv), solver.eval(memory.load(...), cast_to=bytes) (RustStateProxy's solver supports cast_to), and posix.dumps(1). Do NOT compare heap_location — RustHeapProxy exposes only mmap_base/allocations/freed; compare the malloc/calloc RETURN POINTER instead. Vacuity guard: for names Rust has no native handler for, assert the name appears in mgr.stats['simprocedure_fallback_by_name'], else a future native handler silently makes the row prove nothing. Gotcha: pthread* and getenv/open live in SIM_PROCEDURES['posix'], not ['libc']; fwrite/fputc/fprintf need a fake FILE* with a 32-bit fd at offset 112 (io_file_data_for_arch(AMD64)['fd']).

fallback_to_python_store refactor pattern (angr-1ezg, commit 747e86c1a): the 159-LOC monolith in native/angr/src/interpreter/statements.rs cleanly splits along 4 axes — (1) invalidate_loads_at(addr, size) for concrete-addr prefetch+IRSB invalidation, (2) handle_concrete_store for the 32-bit non-stack symbolic-callback heuristic + pending_stores fast path, (3) handle_symbolic_store for the prefetch.clear() + flush + 5-way ConcretizationResult match, (4) dispatch_multi_store as shared 16-addr ITE-chain vs Python multi-addr callback for Multiple/Strided. Orchestrator becomes 15 LOC, 2-level nest. Same pattern applies to any sibling 'fall back to Python on hard case' function that mixes addr concretization shapes with buffering. Note: the pre-refactor file contained a dead empty 'if ... {}' at the start of the concrete branch — dropping it is provably no-op (condition is side-effect-free).

SUPERSEDED (see parallel-worker-stack-overflow-root-cause): the CADET_00001_partial W=2 'zero completed waves' observation was NOT an intra-wave per-task perf collapse. The first wave never quiesced because a worker thread had DIED — 2 MiB default Rust thread stack overflowed on deep CGC symbolic-stdin ASTs (dmesg: 'angr-worker-N ... segfault'). Fixed in commit 4131a8e27 (16 MiB WORKER_STACK_SIZE). Do not chase GIL contention / block-cache duplication / bounce round-trips off this memory.

faorh root cause: CADET_00001_partial hangs ~19x at RUST_PARALLEL_WORKERS=2 because the parallel WAVE loop pays full Z3 detach/reattach serde per cross-worker state move, and CADET's wide divergent frontier maximizes those moves. Mechanism (all in native/angr/src/exploration/scheduler.rs + run_loop.rs): (1) run_loop.rs run_loop() routes workers<=1 to run_loop_single_threaded (ZERO serde, all states in one Z3 ctx); workers>=2 => run_loop_parallel wave loop. So the entire W1->W2 cost delta IS parallel serde+coordination overhead. (2) In worker_loop, offload_surplus() Trigger A fires on EVERY task completion whenever idle_workers>0 && local.len()>=2, shedding HALF the local queue via state.detach_for_migration() (full Z3 AST serialize). The idle sibling steal_from_injector()s + payload.reattach(ctx) (full Z3 rebuild). (3) On a divergent frontier that keeps forking (CADET leaks states, angr-027h) the two workers are chronically imbalanced, so a large fraction of the growing frontier round-trips detach->inject->steal->reattach, each a full Z3 translate the single-worker path never pays. Serde swamps compute => throughput collapse (7.75s W1 -> >150s SIGTERM W2). Secondary suspect: steal_from_injector busy-spins std::thread::yield_now() while pending>0, so an idle worker burns a core while the productive worker holds a heavy solve (CPU starvation on a small box). NOT a deadlock/livelock (both workers make forward progress on distinct states) and NOT OOM (SIGTERM). Fix directions filed on follow-up bead: bound/rate-limit Trigger A offload; replace the yield_now spin with a backoff. Do NOT blind-tune the scheduler (a8epx lesson: worktree-isolated A/B required).

OPTIMIZATION: prune() and filter() were exporting full Rust states to Python (expensive: full memory/register/constraint sync) just to check satisfiable() or state.addr. Fixed: prune default uses Rust state_satisfiable() directly, filter uses lightweight RustStateProxy first. This dramatically improved Callable flow (flareon10: 10.2s → 5.5s) because Callable.step_func calls prune() after every step.

fauxware's Callable (concrete_only=True) on authenticate() RAISES AngrCallableMultistateError under the VANILLA Python engine — verified 2026-07-14. Rust used to return a concrete 0 there only because the read of the natively-opened pwfile fd bounced to Python, found no such fd in state.posix (Rust fds are not mirrored, angr-8j16), and silently wrote nothing, leaving stored_pw concrete. Once native read mints symbolic bytes for a contentless fd (angr-gorvf.15), the strcmp branch splits and Rust matches Python. tests/engines/rust/test_solver_output.py::TestCallableStepFunc::test_callable_with_rust_engine now asserts the raise. Do NOT 'fix' this back to a concrete return — that would be a divergence from angr, not a feature.

fauxware callback breakdown (6 callbacks, ~57ms total = ~14% of 0.4s runtime): read 4x ~20ms (no native impl registered — read.rs/write.rs commented out at procedures/mod.rs:245-246 due to fd-tracking coordination concerns); strcmp 1x ~19ms (NativeStrcmp falls back because user input bytes are symbolic — by design, can't avoid); open 1x ~17ms (NativeOpen registered but falls back — likely because pathname memory has symbolic taint from default fill or external-address-space hook context). Native dispatch DOES work for puts (2x successful native calls). Project registers 16 unique procs, 4 match native (open/printf/puts/strcmp). The 12 missing names are mostly angr-internal stubs (CallReturn, LinuxLoader, dl*, _vsyscall, ReturnUnconstrained, __libc_start_main) that don't have natural Rust impls. Biggest actionable opportunity: enabling NativeRead would eliminate 4 callbacks ~20ms ~5% of fauxware. Blocked on posix-plugin/fd-tracking design.

fauxware callback profiling (2026-04-28): 6 callbacks, 127ms total. Breakdown: Python SimProcedure execution 99ms (78%), state create 9.5ms, sync back 17.5ms, state copy 0.9ms. Per-procedure: open 60ms(1x), strcmp 20ms(1x), read 19ms(4x). Init overhead: 15ms (disk-cached blank_state creation). The 99ms execute time is irreducible — it's Python angr SimProcedure code running identically in both engines. The only FFI-specific overhead is 28ms (state create + sync back). Optimization: skip callee-saved register sync saved ~6 reg ops per callback direction.

fauxware (Rust engine) cost breakdown @ 0.38s total (commit a589c0708): 124ms in 6 SimProcedure callbacks — open: 59ms (1x), strcmp: 21ms (1x), read: 16.6ms (4x). 17.6ms sync back per callback. 9.2ms state create. fauxware is 0.9x (slower than Python) because Python's angr SimProcedures themselves run in Python and the per-callback FFI dance still costs ~30ms total of the 380ms. Win-paths to investigate: (1) native SimProcedure for read (4x/16.6ms each), (2) reduce sync_back time of 17.6ms (constraint export?), (3) reduce state_create of 9.2ms (state copy).

fauxware quirk: rejected() ends with 'call exit@plt' at 0x400718, post-call address 0x40071d. Coincidentally 0x40071d is also the START of main() (rejected and main are adjacent in this binary). When debugging exit-handling bugs, this overlap can cause symptoms that look like 'main re-enters infinitely' when really the exit deadend logic is broken.

fauxware-rust-empty-output bug (angr-q7ij, 2026-05-14): the rust state at sm.active[*].posix.dumps(0) returned b'' on the SOSNEAKY-finding path. Debug method: write a subprocess-safe debug script that runs entry_state + sm.run(until=len(active)>1) with both engines, prints posix.dumps, addr, constraints, stdin.pos. Diagnostic: Python had 3 constraints (strlen + strncmp_ret==0/!=0) and SOSNEAKY in dumps; Rust had only 1 constraint (strlen) and empty dumps. Root cause: native/angr/src/procedures/read.rs::NativeRead never called record_stdin_symbol. See invariant-record-stdin-symbol-required.

RESOLVED 2026-05-14 (commit 4e9032f85). Was: Rust engine outputs empty string while Python finds 'SOSNEAKY' on fauxware. Fix: NativeRead now calls state.record_stdin_symbol() for each created stdin byte (was the only native stdin source missing this — fgets/fgetc/getchar/scanf all already do it). posix.dumps(0) on Rust-forked fauxware states now contains 'SOSNEAKY' bytes. Property fuzzer still reports exact-mismatch (different stdin packet layout between python & rust), but the SOSNEAKY content is present. Promoting fauxware to rust_only=False is a separate (not-yet-done) decision.

fcntl(72)/ioctl(16)/pipe(22)/pipe2(293) are INTENTIONAL syscall stub-fallthrough (syscalls/mod.rs register_syscalls! AMD64 block, see the doc comment above register_syscalls!), NOT a missing-impl gap. Rationale: angr's posix/fcntl.py defines an fcntl SimProcedure but linux_kernel.py NEVER binds it into the kernel library, so Python's own syscall path is a pure stub too -> the Rust stub is exact parity. Don't 'fix' these by adding native handlers; that would DIVERGE from Python. This is why epic angr-11djq.5 (T2-B5 fall-through syscalls) closed with fcntl/ioctl as documented stub-parity rather than native impls. The stat family (stat/lstat/fstat/newfstatat) WAS extended natively via write_stat_for_arch to i386/ARM/MIPS32 (children 11djq.5.1/.2/.3).

Characterization tasks ('investigate X% speedup') can be satisfied by the OR clause in the acceptance criteria ('root cause documented in docs/advanced-topics/rust_engine.rst'). When a benchmark gap turns out to be more interesting than expected (e.g., it's actually a regression, not the documented gap), separate the characterization (close THIS task with docs/baseline updates) from the fix (file a NEW task with the investigation scope). Why: the original task wasn't about fixing a regression — extending its scope hides the regression and conflates two unrelated workstreams. How to apply: any time you discover that 'expected gap' is actually 'unexpected regression', do both — close characterization, file follow-up — rather than reopen-with-scope-creep.

angr-gorvf.4.5 (commit 33830be3c): the residual batch_fetch_pages GIL was NOT the concrete-page solver.eval the bead assumed. Probe on google2016_unbreakable_1: the callback fires ONCE with 7 pages and all 7 are SYMBOLIC (declined). The cost was state.memory.load(page,4096) — a 32768-bit AST build done only to answer 'is this page symbolic?' — thrown away on the decline. Fix: RustExplorationManager._fetch_page_from_ultrapage classifies off UltraPage symbolic_data/symbolic_bitmap/concrete_data (same fast path as _sync_extra_python_pages); both _cb_fetch_page and _cb_batch_fetch_pages call it, load+eval stays as the non-UltraPage fallback. 2,346,151ns -> 29,144ns (80x). COROLLARY (a trap): a 'let Rust zero-fill the lazy stack natively' fix would silently ZERO symbolic stdin bytes living on those very pages — the lazy-stack pages that miss are the ones holding user symbolic data. Literal counter==0 is unreachable via callbacks; only the memory-proxy gate (angr-grji4) gets there.

Native fgetc/getchar EOF model (procedures/fgets.rs NativeFgetc + NativeGetchar): under has_option("SHORT_READS") they return eof.ite(&neg_one_32, &byte_ze, &ctx) — a fresh symbolic 1-bit eof BVS over-approximating simfd.eof() and -1 as 0xFFFFFFFF (32-bit). Mirrors Python procedures/libc/fgetc.py: If(real_length==0, -1, data.zero_extend(int-8)). getc aliases fgetc. Default path (option off) returns a bare zero_extend(byte,32) in [0,255] so the EOF sentinel is never a solution and the path stays non-forking/byte-identical (perf unaffected, fast-tier 20/20). Counterpart to the fgets short-read work (see fgets-short-read-design / angr-efvao). angr-qx81x, commit 4de3f75f1.

RESOLVED (angr-efvao, commit 960b1eff9): native fgets short-read/EOF modeling is now LANDED. Gated behind has_option("SHORT_READS") (the kzjv6 accessor). Symbolic real_size in [0,size-1], per-byte newline/EOF ITE constraints, NUL-at-real_size via concrete-position ITE stores, returns symbolic real_size. Default (SHORT_READS off) stays byte-identical/non-forking. See fgets-short-read-design for the full design and avoid-symbolic-addr-store-for-concrete-readback for the ITE-store technique. NOT YET done: NativeFgetc/getchar still always return a fresh symbolic byte and never model single-char EOF (-1); that getc-EOF gap is unaddressed (would need bounded-stdin EOF tracking, low value since default stdin is unbounded). Newline-constraint half: e898ae13a (fgets-newline-constraint).

Native fgets (native/angr/src/procedures/fgets.rs, NativeFgets call closure) now adds a newline path constraint: after creating the (size-1) free symbolic stdin bytes, it constrains every byte EXCEPT the last data byte to != '\n' (via RustBV::ne + state.add_constraint). Rationale: a FULL read of read_count bytes means real fgets never hit a newline before the final byte (it stops at and includes the first newline), so an embedded-newline-then-more-data state is infeasible; the last byte (index read_count-1) stays free since a line can exactly fill the buffer ending in newline. This PRUNES the over-approximation native used to keep vs Python's procedures/libc/fgets.py SimFile model. KEY INSIGHT: a BLANKET 'no newline anywhere' constraint would be WRONG (it under-approximates by excluding short-line inputs); constraining all-but-last is the correct, only-prunes-impossible-states formulation relative to native's full-read model. fgetc/getchar need NO newline constraint (a single-byte read of any byte incl newline is valid). Perf: O(read_count) cheap byte!=newline constraints, NO regression (defcamp_r100 0.33 vs 0.32 baseline, fast-tier 20/20). Commit e898ae13a, test test_fgets_newline_only_at_last_byte. EOF/short-read (variable-length) modeling is the remaining gap -> angr-efvao.

file_read_kernel fixture (angr-w5llj) build notes: raw open()/read()/close() syscalls (NOT stdio FILE*) so the measured fallback is the fd path itself, not fopen/fread on top. Built gcc -O2 -fno-stack-protector -no-pie (stable non-PIE addrs); main at 0x401090, ret at +0x5c. solve.py uses entry_state(addr=main) + state.fs.insert(path, SimFile(path, content=..., size=len)) to pre-seed, then sm.explore(find=main+RET_OFFSET, n=200). Single non-forking path because the pre-seeded magic compare is concrete. Same vendor-the-binary pattern as fp_simd_kernel/write_stream_heavy (see fp-simd-fixture-build). Test fn asserts found==1.

FileSystem struct in state.rs replaces fd_buffers. FileDescriptor has name/position/flags/content/is_open. Standard fds 0-2 pre-registered in Default::default(). FileSystem cloned on all 5 fork methods. Backward compat: stdout_buffer/write_fd/fd_buffer delegate to FileSystem. Native open/close/lseek in procedures/fileops.rs (registered by default). Manager API: get_state_open_fds, get_state_fd_content. Snapshot: open_fds field. Commit 2bb436e06.

Adding a field to FileSystem (native/angr/src/state/filesystem/ — split into mod.rs/fd.rs/ops.rs/query.rs/symbolic.rs/persist.rs by angr-nbim4.4) requires touching SIX sites, all mirroring the known_paths precedent: (1) struct FileSystem [filesystem/mod.rs], (2) struct FileSystemData serde shadow [filesystem/persist.rs] (with #[serde(default)] for back-compat + a BTreeMap/BTreeSet for deterministic wire order), (3) impl From for FileSystemData [persist.rs], (4) impl From for FileSystem [persist.rs], (5) impl Default for FileSystem [mod.rs], (6) the manual clone in FileSystem::translate_into [persist.rs] (uses Arc::clone for string-set fields). Miss any and it either won't compile (struct-literal sites) or silently drops the field on snapshot/worker-migration round-trip (serde sites). demoted_paths (angr-qluof) followed this exactly.

FindDirected SelectionPolicy (native/angr/src/exploration/selection_policy.rs, angr-lnzcu) is the num_find=1 find-first ordering. Ranking key: (novelty, distance-to-find, front-index) — novelty PRIMARY (0=novel block,1=seen) is the anti-greedy-trap mechanism, NOT a beam (contrast DirectedCfgDistance which uses a beam+per-pc round-robin FAIRNESS; FindDirected is deliberately the greedy opposite). At a char-check fork both equal-distance successors are novel so both dispatch before either re-treads. Unmapped blocks get u64::MAX, sink last but never dropped. seen-set behind a Mutex for Send+Sync. Opt-in via set_exploration_strategy('find_directed', distances=cfg_distance_map(cfg, find_addr)); default inert. Per ilq8-post-cancel-waste the raw speculative-waste win is ~0 on real benches, so it's justified as a directed feature not a waste fix; same untractable-divergent-target gate risk as a32jl.4 (75mc keystone).

tests/engines/rust/test_solver_ops.py::TestSolverOperations::test_model_stability_constraint_order is order-dependent flaky: fails in full-file pytest run (e.g. 'eval(x) order-stable; got 128 vs 130') but passes in isolation. Z3 model-completion picks differ depending on solver/context state warmed by prior tests in the run. NOT a regression signal — re-run in isolation to confirm before bisecting. Observed iter15 during a pure test-reorg (angr-evu3) that touched no solver code.

Scheduler unit test test_post_cancel_steps_counts_peer_speculation (in exploration/scheduler_tests.rs) is FLAKY under the parallel cargo-test runner on a core-constrained box: it asserts post_cancel_steps>0, which needs a peer worker to commit a step in the window after another worker cancels. When all 16 scheduler tests run concurrently they contend for the few cores and that speculation window can collapse -> post_cancel_steps=0 -> spurious FAIL. It passes reliably in isolation and with 'cargo test scheduler -- --test-threads=1'. A single failure of ONLY this test under a full parallel run is a scheduling artifact, NOT a regression -- re-run single-threaded to confirm before bisecting.

Cargo test symbolic::context::tests::test_add_constraint_raw_dedup_repeat_skips_push is flaky under parallel test execution because it reads a process-global atomic ADD_CONSTRAINT_RAW_DEDUP_HIT_COUNT before+after and asserts an exact delta of 2. Other tests in parallel can also bump the counter. Verified flake: 3 runs in a row -> FAIL/PASS/FAIL. Test passes 100% in isolation. Pre-existing; not caused by interpreter_cb rename (angr-sy4g).

tests/engines/test_rust_exploration.py::TestSolverOperations::test_model_stability_constraint_order is flaky when run as part of the full suite. Seen 2026-05-20 during angr-kg58: failed once (eval(x) returned 128 vs 160 for two solvers with same constraints in different order), then passed on rerun both in isolation and in the full suite. Test asserts Z3 deterministic eval but Z3 internal heuristics (random seed, simplification cache) can vary across solver instances even with identical assertions. Treat single failures as flake unless reproducible.

flareon2015_5 gate-on IndexError root cause CORRECTED (iter65, overturns iter64 flareon-5rjbq-store-visibility-disambiguated which was WRONG). EMPIRICAL PROOF via env-gated eprintln in SymbolicMemory::store_concrete (symbolic branch) + load_concrete (ANGR_DBG_MEM_ADDR=[:span] window; instrumentation reverted after). Native VEX hash loop DOES read the symbolic pw bytes — store AND native load both hit the SAME memory instance at addresses 0x0..0x21 with sym_hit=true. So it is NOT a store-visibility / callback-state-vs-execution-state coherence gap. REAL cause: ADDRESS-WITNESS COLLISION. The buffers are all unconstrained ebp-relative (blank_state ebp symbolic): ADDR_PW_ORI=ebp-0x80004, ADDR_PW_ENC=ebp-0x70004, ADDR_HASH=ebp-0x40000. Each is a DISTINCT claripy AST, so RustMemoryProxy concretizes each INDEPENDENTLY via self._solver_ctx.eval(addr) with no pin — and Z3 returns witness 0 for every unconstrained expr, so ENC-base==HASH-base==0. Evidence: STORE_SYM shows count=2 stores at each of 0x0..0x21 = two rounds BOTH at base 0 (round1 hook copies pw->ENC(0); round2 native writes hash->HASH(0), overwriting ENC/pw). The buffers ALIAS at addr 0 -> hash computed over pw gets clobbered mid-flight -> found-state hash constraint unsat -> solver.eval empty -> IndexError solve.py:69. Gate-off works because native Rust concretizer keeps ebp consistent across the whole run; the gate-on PROXY eval path does independent per-AST concretization with no shared ebp pin. FIX DIRECTION: proxy concretization must pin the symbolic base consistently so distinct ebp-relative buffers get distinct non-aliasing witnesses (mirror angr write-addr concretization) — but respect constraint-export-no-pre-pin (pinning a symbol to a wrong/arbitrary model breaks solves). Safer: concretize all ebp-relative addrs against ONE shared solver that accumulates addr==witness constraints, OR route proxy addr concretization through the Rust native concretizer/state solver (same one native uses) instead of a forked _solver_ctx.

flareon2015_5 callback-memory-proxy gate-on residual — refined root cause (angr-5rjbq, supersedes flareon-5rjbq-witness-mismatch framing). The blank_state ebp is SYMBOLIC. solve.py captures ebp-relative buffer addresses as GLOBALS at setup: ADDR_PW_ORI = state.regs.ebp - 0x80004 etc. So every hook_duplicate_pw_buf / final-eval address is the claripy expr (python_ebp - k). Under the gate these symbolic-addr loads/stores are concretized by RustMemoryProxy against a solver, but the pw setup writes (state.mem[ADDR_PW_ORI+i]=BVS('pw')) went into the pre-swap PYTHON DefaultMemory at whatever witness Python's write-concretization picked, while the Rust engine's emulated XOR/hash loop reads/writes the ENC and HASH buffers at whatever witness the RUST solver picks for the same unconstrained ebp. There is no constraint pinning ebp, so the Python-fallback solver and the Rust engine solver need not agree on ebp's value -> the pw the callback reads, the ENC it stores, and the HASH the engine computes can land at mutually-inconsistent addresses -> found state unsat -> IndexError at solve.py:69. FIX DIRECTIONS not yet done: (a) pin ebp to a single concrete value in BOTH the Python entry state and the exported Rust state at setup so all buffer addresses are concrete and aligned (most faithful, matches how real harnesses avoid symbolic SP/BP); or (b) ensure the Rust engine and the Python fallback share ONE concretization witness per symbolic base (cross-solver witness sync), not just per-proxy as _addr_witness_cache does. Contained per-proxy witness cache (commit this iter) makes proxy symbolic-addr STORE->LOAD round-trips self-consistent but does NOT bridge the Python-fallback<->Rust-engine gap.

flareon2015_5's ebp is NOT unconstrained, despite blank_state: angr's address-concretization mixin ADDS a pinning constraint when Python stores to a symbolic address. solve.py's setup loop 'state.mem[ADDR_PW_ORI+i].byte = BVS(pw)' therefore pins 'reg_ebp_0_32 == 0x80003' in the state's constraint list, making ORI=0xffffffff (byte0 lands on page 0xfffff000, bytes 1-33 wrap onto page 0x0), ENC=0xffff, HASH=0x40003 — all UNIQUE. Consequence: any 'Rust and Python concretize the symbolic ebp differently' hypothesis for angr-5rjbq is DEAD (measured iter6: found-state ebp = 0x80003 under both the memory-proxy gate on and off). Also note state.memory.get_symbolic_addrs() returns EMPTY for this state, so rust_state_sync.py's _find_user_symbolic_pages / _scan_user_symbolic_pages only find the pw bytes via their page.symbolic_data fallback branch. The real 5rjbq frontier is the base64 encoder's OUTPUT store 'mov [esi+idx],al' at a symbolic esi (=HASH AST): gate-off yields symbolic base64 ITE trees at HASH, gate-on yields structurally-concrete BV8 0 (never written), and mem_store_count explodes 118 -> 10494 while constraint_sharing_unique_shapes collapses 8312 -> 9 — consistent with the Rust solver missing the ebp pin under the gate so store_symbolic_unified_multi's concretize_write returns Multiple and installs sidecar cells that the concrete readback path cannot reconstruct (see avoid-symbolic-addr-store-for-concrete-readback).

angr-5rjbq flareon2015_5 gate-on: the RustMemoryProxy.load fallback-witness fix (commit 25c5e2646) is NECESSARY-BUT-NOT-SUFFICIENT. Fixed a real coherence bug: _load_from_fallback re-concretized the SYMBOLIC orig_addr against the pre-swap Python SimMemory's OWN solver, but after the memory swap the ebp-pin constraint migrated to the Rust solver, so Python picked witness B != the Rust-lookup witness A -> Rust-miss-at-A + Python-read-at-B incoherence. Now reads the fallback at the already-computed concrete witness A (rust_state_proxy.py RustMemoryProxy._load_from_fallback signature changed to (conc_addr, orig_addr, size, endness); load site passes the concretized addr). 340 proxy/memory/callback tests green. BUT flareon2015_5 gate-on STILL IndexErrors at solve.py:69 -> the residual is now proven DOWNSTREAM of the pw read: the native VEX hash loop (executed by the Rust engine between hooks 0x4011E7..0x4011EC) reads ENC (stored via proxy at A) and writes HASH at ebp-0x40000, and the final eval reads ADDR_HASH. NEXT: instrument whether ENC store (proxy) and the native hash-loop ENC read land at the same witness, and whether ADDR_HASH readback sees the Rust-computed hash. Consider whether pinning ebp to a concrete value at gate-on setup (fix direction a) is needed so ALL of pw-read/ENC-store/native-hash-loop/HASH-eval share one witness end to end.

flareon2015_5 (angr-5rjbq) iter72 STATIC disassembly of 'sender' pinpoints the hash-input data flow — supersedes the 'native reads elsewhere, unknown why' framing. Chain (ebp pinned 0x80003 => ORI=0xFFFFFFFF, ENC=0xFFFF, HASH=0x40003): (1) fn 0x401250 (called 0x4011a0, ecx=ORI): hook_duplicate_pw_buf fires at 0x401259 (length=0), copies ORI->ENC and sets ebx=ENC; native scramble loop 0x401260-0x401287 does 'add BYTE PTR [esi+ebx],al' — a read-modify-write on ENC INDEXED BY ebx (the hook's register write). (2) hash/base64 encoder fn 0x4012a0: stores its input ptr as ecx into [ebp-0x54] at 0x4012c8, then reads input ONLY via that: 0x401322 'movzx edx,[eax+esi-1]', 0x40132e '[esi+eax]', 0x401341 '[esi+eax+1]' (eax=[ebp-0x54]); writes base64 output to [ebp-0x50]=ADDR_HASH via 0x401366 'mov [edi+ecx],al'. CRUX: native's LAST write to ecx before the encoder call is 0x4011dd 'lea ecx,[ebp-0x80004]'=ORI. ecx=ENC is supplied ONLY by Python hook_use_dup_pw_buf at 0x4011E7 (length=0, just before 'call 0x4012a0'). So native reading its hash input at 0x40003=HASH (not ENC=0xFFFF) PROVES native's encoder-input ecx != ENC => the hook's ecx=ENC register write is NOT reaching the native encoder read. Both hooks' REGISTER writes (ebx=ENC in dup-hook, ecx=ENC in use-hook) are load-bearing — the buffers are indexed through them. iter71's register-proxy (reg_writes 0->6) should have fixed exactly this but hash stayed constant => NEXT: bounded trace logging concrete ecx+ebp at encoder entry 0x4012a0 and read site 0x401322 to confirm native ecx value, and verify the register proxy writes ecx at the RIGHT boundary (0x4011E7, before the call, not after).

flareon2015_5 gate-on address-witness collision FIX (commit 84eed3b68, angr-5rjbq iter66): two mechanisms needed. (1) CONSISTENT PINNING — RustMemoryProxy._pin_addr_witness pins addr==conc on BOTH the state solver (add_constraints_to_state, so NATIVE execution stays consistent) AND the proxy _solver_ctx fork (add_constraint_ast, so the PROXY's own next eval stays consistent). Pinning ONLY the state solver is insufficient: the proxy concretizes via _solver_ctx which is a separate fork and re-picks witness 0, re-aliasing. Called from load symbolic-concretize branch + store fallback. This does NOT violate constraint-export-no-pre-pin: that rule is about EXPORT-time pinning of a RECOVERED model; here we commit to a write address WE chose (angr DefaultMemory does the same), on a scratch stack pointer not in any goal constraint. All behind the callback-memory-proxy gate. (2) AUTOMAP — once ebp pins low the concretized buffer lands outside every lazy region; set_state_memory_ast/memory_store only auto-maps pages already inside a lazy region, so it dropped stores as Unmapped. New RustSimState::add_memory_lazy_region + set_state_memory_ast_automap FFI widen the lazy region to cover the target page first. Anchor symbols: RustMemoryProxy._pin_addr_witness, RustSimState::add_memory_lazy_region, InnerExplorationManager::set_state_memory_ast_automap.

flareon2015_5 gate-on RESIDUAL after the pin+automap fix (angr-5rjbq iter66, commit 84eed3b68): the address-witness aliasing is FIXED (ORI/ENC/HASH now at distinct 0x0/0x10000/0x40000) and the ENC page is now mapped, but gate-on STILL FAILs — found state is UNSAT after solve.py:63-65 adds the printable hash constraints, so found_s.solver.eval returns empty -> IndexError solve.py:69. This is a SEPARATE deeper bug from the aliasing. Investigate in order: (1) do the 32 multi-cell ENC stores at 0x10001..0x10021 actually LAND with the pw symbols (only 2 fallback stores fire now; the rest route through state_memory_store_symbolic_multi — verify they land, dump ENC after the hook). (2) store-visibility: does native hash ENC AFTER the hook's stores commit, or over a pre-store resume snapshot? (3) symbol identity: the hook reads pw from the Python FALLBACK memory via RustMemoryProxy._load_from_fallback (get_state_memory_ast returns None); are those pw BVS the SAME AST instances that native hashes in ENC, or disconnected copies — if disconnected the hash constraint ties different symbols than the final ORI read. Baseline: gate-off passes -> b'Sp1cy_7_layer_OSI_dip@flare-on.com'.

flareon2015_5 callback-memory-proxy gate-on residual (angr-5rjbq) — CORRECTED root cause, OVERTURNS the ebp cross-solver / witness framing (flareon-5rjbq-ebp-cross-solver-root-cause + fallback-witness memories). PROOF: pinning ebp to a single concrete value (state.solver.add(state.regs.ebp==0x7fff0000)) in solve.py — making EVERY ebp-relative buffer addr concrete and shared end-to-end — gate-OFF rust PASSES (OK, 3.4s) but gate-ON still IndexErrors. So the residual is NOT a cross-solver ebp witness disagreement. DECISIVE test: hook_duplicate_pw_buf stores a CONCRETE 0x41 pattern to ADDR_PW_ENC via the proxy; proxy readback at h_dup AND at the later hook_use_dup_pw_buf (0x4011E7) both see 0x41, and the found-state readback of ENC is symbolic/present — yet the native VEX hash loop still computes HASH == all-zero (concrete). i.e. the proxy STORE to callback_state_id (RustMemoryProxy.store -> set_state_memory_concrete / set_state_memory_ast) is visible to later PROXY reads on the same state_id but is NOT seen by the resumed NATIVE VEX interpreter that continues execution after the length=0 hook returns. HASH=0 (from ENC=0 as native sees it) -> constrain HASH==GOAL_HASH is unsat -> sm.found[0] state unsat -> solver.eval empty -> IndexError at solve.py:69. This is a callback-state<->execution-state MEMORY-WRITE coherence gap, isolated to the proxy gate: gate-off's CallbackMemoryTracker diff-and-push replays hook writes into the executing Rust state; gate-on forces tracked_writes=None (direct-write) but the direct proxy write to callback_state_id does not reach the interpreter's resume-time memory. NEXT: inspect the resume path (does the native interpreter continue on callback_state_id or a pre-hook snapshot?) and ensure proxy writes commit to the state execution resumes on. Repro scripts: /tmp/flareon_dbg.py (symbolic) and /tmp/flareon_dbg2.py (concrete-0x41 decisive).

flareon-5rjbq FIX LEAD (append to flareon-5rjbq-proxy-store-not-seen-by-native-root-cause): the proxy-store-not-seen-by-native coherence gap most likely originates in native/angr/src/exploration/resume.rs. _resume_after_simprocedure and route_resume_successors reference a pending.pre_callback_snapshot captured BEFORE the callback ran; resume.rs:88 comment 'NOT inherit callback constraints. Use pre_callback_snapshot as fork base.' If the resumed MAIN successor (not just forks) rebuilds memory from pre_callback_snapshot, any proxy memory write the hook made directly to callback_state_id is discarded on resume -> native reads pre-hook memory (zeros for ENC). Under gate-OFF the CallbackMemoryTracker diff-and-push replays hook writes AFTER snapshot restore, masking this; under gate-ON tracked_writes=None so nothing replays. Next iter: trace whether the length=0 hook resume for flareon rebuilds the executing state's memory from pre_callback_snapshot, and if so, make proxy writes commit to (or the resume preserve) the post-callback memory. Verify with /tmp/flareon_dbg2.py (concrete-0x41 -> expect native HASH nonzero once fixed).

flareon2015_5 gate-on (angr-5rjbq) CORRECTED diagnosis (supersedes prior addr claims). Repro: mirror solve.py main() under RustExplorationManager + ANGR_RUST_USE_CALLBACK_MEMORY_PROXY=1 (run_single hides the traceback; write a standalone harness that prints found count + concretized ORI/ENC/HASH + hash .symbolic/.variables). MEASURED (iter68): ebp concretizes to ~0x80003 so ADDR_PW_ORI=0xffffffff (WRAPS the 32-bit boundary), ENC=0xffff, HASH=0x40003 — and these addresses are IDENTICAL gate-on vs gate-off, so the wraparound is NOT the differentiator (prior notes guessed ENC=0x10000/ebp=0x80004 — WRONG). The ONLY difference: gate-ON found-state HASH loads back CONSTANT (0 claripy vars; solve first byte b'\x00'); gate-OFF HASH is SYMBOLIC (34 vars; solve first byte b'\xb9', real pw symbols). So the pw symbols are lost between the proxy ENC store and native's hash read ONLY under the proxy gate. NEW decisive native-instrumentation finding (temp log in load_concrete_lazy_inner + load_symbolic_unified Single branch, reverted): during native execution under the gate there are essentially NO native reads at ENC (0xffff/0x10000) or HASH (0x40003) — only 2 lazy reads at 0xffffffff (ORI; sym_hit=true multi_hit=false). i.e. native's hash loop does NOT read ENC where the proxy stored it; the 34-byte hash-input read is missing from the native lazy path entirely. NEXT: instrument store_symbolic_unified_multi to log where the proxy ENC store actually lands, and add a total native-read counter, to find where the hash loop reads its input (it is not the ENC region). Found=1 in both modes; explore DOES reach 0x4011EC.

flareon2015_5 gate-on residual (angr-5rjbq) — iter64 DISAMBIGUATED the two competing hypotheses with clean experiments (/tmp/flareon_repro.py, gate-on RustExplorationManager, proxy stats + found-state hash inspection). (1) REFUTED pure address-witness-mismatch: pinning ebp==0x7fff0000 end-to-end drops proxy_mem_symbolic_addr_fallback 34->2 (addresses now concrete) yet gate-on STILL IndexErrors — so it is NOT (only) a store-vs-native-read address concretization disagreement. (2) CONFIRMED store-visibility gap even for CONCRETE addr+data: found[0] HASH[0] evaluates CONCRETE and is pw-INDEPENDENT (h0.concrete==True, no 'pw' vars) — the native VEX hash loop (0x4011E7..0x4011EC) computed the hash over CONCRETE-ZERO ENC bytes, never seeing the proxy's 34 symbolic pw stores. So the found state's constraints add cleanly one-by-one but the goal-hash CONJUNCTION is unsat (hash inputs are uninitialized/zero, not pw). Path: zero-length hooks resume via rust_callback_dispatch.py::_resume_with_skip_hook, which under the proxy gate passes mem_changes=None (writes went DIRECT to Rust via RustMemoryProxy.store->set_state_memory_ast) then Rust resume.rs::_resume_after_simprocedure reuses pending.state. The OPEN question for next iter: does set_state_memory_ast(callback_state_id,...) actually land in the SAME RustSimState (pending.state) that the native interpreter resumes AND reads on? NEXT: add env-gated eprintln in state_api.rs::_set_state_memory_ast + the interpreter memory-load at the concrete ENC addr (run pinned-ebp so addr concrete), rebuild, confirm whether the store page and the native read page are the same state instance. Repro: /tmp/flareon_repro.py (PIN_EBP=1 for concrete-addr variant). See [[flareon-5rjbq-proxy-store-not-seen-by-native-root-cause]].

flareon2015_5 gate-on (angr-5rjbq) iter71 measured findings — RULES OUT two prior hypotheses. Repro: /tmp/flareon_repro.py (memory-proxy gate). Under ebp-pin=0x80003: ADDR_PW_ORI=0xFFFFFFFF (wraps), ADDR_PW_ENC=0xFFFF, ADDR_HASH=0x40003. NEW facts via env-gated native trace in load_concrete + store_concrete_automap_internal (window 0xF000..0x50010, ANGR_5RJBQ_TRACE, REVERTED after): (1) The proxy STORE of all 34 pw bytes into ENC SUCCEEDS — bytes 0,1 land at 0xFFFF/0x10000 via the symbolic-addr automap fallback (matches _stats_proxy_mem_symbolic_addr_fallback=2), bytes 2-33 (0x10001..0x10020) land via store_symbolic_unified_multi -> store_concrete_automap after page 0x10 auto-mapped by byte-1's fallback. Python reload of ENC+0 right after hook_dup returns pw_1_8 symbolic. So store/load round-trip WORKS. (2) Native execution's hash activity is entirely at 0x40003 (ADDR_HASH region): 144 one-byte load_concrete calls, ALL sym_at_addr=false (zeros). Native NEVER reads ENC (0xFFFF) in the traced window. (3) DISPROVED register-asymmetry hypothesis: enabling ANGR_RUST_USE_CALLBACK_REGISTER_PROXY=1 (reg_writes 0->6, ecx/ebx/eax buffer-ptr writes now write-through to Rust) STILL yields HASH[0] concrete / unsat. So the register diff-and-push path is NOT the cause. CONCLUSION: bug is NOT proxy store, NOT proxy load, NOT register routing. The pw at ENC(0xFFFF) is simply never consumed by native's hash — native reads its hash input from a region the pw never reaches (ADDR_HASH 0x40003 and/or ORI 0xFFFFFFFF per iter68). NEXT: disassemble flareon 'sender' hash fn at ~0x4011xx to identify WHICH register/buffer the hash actually reads its input from (hook_use sets ecx=ENC but native may read a stack-local or ORI directly); and check whether the Python-SETUP pw writes at symbolic ADDR_PW_ORI ever synced into Rust at native-concretized 0xFFFFFFFF (iter68 saw sym_hit there but hash still constant). Supersedes flareon-5rjbq-store-visibility-diagnosis on the store-side question (store works).

flareon2015_5 callback-memory-proxy gate-on residual (angr-5rjbq): after adding RustMemoryProxy.load fallback to the pre-swap Python SimMemory (fallback_memory kwarg, commit 2ce45a84a), the fallback fires 96x (proxy_mem_fallback_python_load==96) yet flareon STILL FAILs IndexError unchanged. Likely deeper cause: symbolic ebp-relative addresses concretize to DIFFERENT witnesses between the copy STORE and the later hash LOAD. RustMemoryProxy.store's symbolic-addr path (p1s02) concretizes+automaps at witness A; RustMemoryProxy.load concretizes independently at witness B -> get_state_memory_ast(B)==None -> falls back to Python (which never got the ENC store) -> zeros -> hash constant -> found unsat. FIX DIRECTION: pin/cache the concretization witness per symbolic base so store and load agree, OR route symbolic-addr stores+loads both to the SAME Python SimMemory instead of Rust. The Python-fallback mechanism itself is correct and gate-guarded (only _install_callback_memory_proxy passes fallback_memory).

flareon2015_10 had THREE bugs: (1) _sync_rust_memory_to_state used arch.memory_endness (Iend_LE) which byte-reversed entire pages — must use Iend_BE for raw snapshot bytes; (2) apply_changes in state.rs truncated memory writes >16 bytes because RustBV uses u128 — must chunk into 16-byte pieces; (3) run(step_func=...) only called step_func once after explore(), but Callable needs it per-step for pruning — implemented proper loop with drop_terminal_states=false.

flareon2015_2 fast-tier baseline rust_time=3.94 was an optimistic snapshot, NOT a target the current code regressed from. Verified 2026-06-21: checked out kvn0.1 commit 2bd351453 (which recorded 3.94) and pre-24pv4.1-cluster commit e127f0707, rebuilt+timed each -> both run 4.5-4.68s on this box, same as HEAD. So the 24pv4.1 symbolic-dedup refactors (all codegen-identical) are innocent of the iter-17 gate failure. Refreshed baseline to 4.57 in commit 9067d8a23. Lesson: a gate failure on a codegen-identical refactor is baseline drift, not a real regression -- bisect by re-timing the baseline-setting commit, do NOT chase the refactor.

flareon2015_5 wrong output root cause: Rust solver fallback (eval_with_fallback) was the ONLY solver path for cached found states. When user adds constraints post-exploration (add_constraints(char == hash_byte)), they only went to Python solver. Rust solver returned values satisfying exploration constraints only (all zeros). Fix: track constraint count at attach time, sync new constraints to Rust solver on eval. File: rust_state_export.py _attach_rust_solver_fallback.

flareon2015_5's 660ms memory_store_symbolic_value GIL site does NOT come from the 32-bit use_sym_store heuristic in handle_concrete_store (interpreter/statements_store.rs) — forcing use_sym_store=false leaves it unchanged. It comes from handle_symbolic_store -> ConcretizationResult::Single -> call_memory_store_symbolic_value, the symbolic-ADDRESS path (the base64 encoder's output writes, angr-5rjbq shape). ~40 crossings, all 8-bit values, ~9ms AST export + ~6ms Python state.memory.store EACH: the values are deep DAGs over symbolic input, so per-crossing tree size — not crossing count — is the cost. Fix the export, not the count.

Fleet-level resource profile for fauxware (angr-ayrq, 2026-06-03): rust per-proc peak ~206 MB vs python ~231 MB (12% lower), rust per-proc wall ~10-20% faster than python at fauxware (modest). Aggregate-peak RSS scales linearly with concurrency on both engines (no shared-page collapse). At conc=16 on 8-core box: rust 2.80 GB / 5.09s wall vs python 3.26 GB / 6.05s wall, both with count=32. Per-proc wall ~doubles past nproc; optimal scheduling at conc=nproc. Bigger gap workloads (mma_howtouse, csaw_wyvern) likely needed to surface Rust's steady-state Z3 savings. Harness at tests/benchmarks/characterization/fleet_resource_profile/.

fopen/fdopen native mode parser only accepts r/r+/w/w+/a/a+ (with b/t suffix stripped and any c/e chars removed). Anything else (including the rarer 'rx' GNU extension and bare 'b') returns ProcedureError, falling back to Python. The libc Python proc raises SimProcedureError on unsupported modes too, so behavior matches — but if binaries actually use unusual modes, they will get a fallback rather than a hard error. Also: we do NOT honor O_CREAT/O_APPEND semantically (no truncation, no append-on-write) because FileSystem is a flat content buffer with no truncate/append concept. If a binary depends on those semantics, this is a known divergence.

native fopen mode parsing (parse_fopen_mode in procedures/fileops.rs) must be ORDER-INDEPENDENT for the flag chars. glibc: first char = base mode (r/w/a); +/b/t/c/e/m/x follow in ANY order; only + upgrades to read+write. The old positional parser (pop trailing b/t, strip c/e, match fixed strings) silently missed valid modes like 'rb+'. Fixed in commit 840b2e56b (angr-06yhf). Unrecognized base or flag chars still return None -> Python fallback. When extending: keep the unknown-char -> None fallback so weird modes defer to Python rather than guess.

SymbolicMemory::fork (native/angr/src/memory/mod.rs::fork) now starts wider_load_cache COLD (FxHashMap::default()) instead of deep-cloning the parent's up to WIDER_LOAD_CACHE_CAP=1024 entries. Safe because the cache is a fingerprint-validated, rebuildable read-side memo with NO correctness role — from_snapshot already restores it empty and re-validates loads against page fingerprints. General rule: fork-path eager-copy beads (epic angr-6t8z3) can drop any cache that the snapshot/restore path already proves correct when cold. Caveat: the memory_fork criterion bench does NOT pre-populate wider_load_cache (only store_concrete, no wider loads), so it won't show the clone savings — real savings appear on warm-cache production forks. angr-6t8z3.2, commit 94c015db5.

Fork-counter semantics in native/angr/src/interpreter/mod.rs (angr-95up.2, commit dc89a7baf, 2026-05-31): solver_fork_count and deferred_fork_count are NOT summable. (1) solver_fork_count is incremented at exactly 3 sites: stepping.rs:151 (pre-callback SimProcedure snapshot fork — counts 1 only when pre_callback_snapshot.is_some()), stepping.rs:493 (per-deferred-fork in handle_block_end_or_max_blocks when condition available), run_loop.rs:513 (per-deferred-fork in callback resume when condition available). It EXCLUDES the P15 conservative-fork fallback (stepping.rs:531 + stepping.rs:1200) which does state.fork() but is not tallied. (2) deferred_fork_count is incremented at 3 sites unconditionally with deferred_forks.len(): stepping.rs:550, stepping.rs:1211, run_loop.rs:539. (3) ALL fork-counter increments at the 6 sites except stepping.rs:1211 are gated on profiling_enabled (they share the same Instant::now() block as their *_fork_time_ns siblings). Without enable_profiling() the counters stay at zero even when forks happen. fauxware exploration shows solver_fork_time_ns > 0 with solver_fork_count = 0 because the entry hit was a non-deferred-fork path (pre_callback_snapshot None, so fork_count = 0). Test test_fork_counters_exposed_and_non_summable verifies structural well-formedness only — no count assertion since count is a function of binary branch geometry.

On fauxware (RustExplorationManager + enable_profiling + explore find=0x4006ED), get_execution_stats() reports solver_fork_count=0 AND deferred_fork_count=0, but deferred_fork_time_ns>0 and solver_fork_time_ns>0. The counts stay 0 because fauxware's forks route through the conservative state.fork() path (interpreter), which is TIMED inside the profiling-gated 'if let Some(start)=..._fork_start' block but NOT tallied by the *_fork_count counters. Consequence for tests: to assert fork instrumentation actually ran on fauxware, check *_fork_time_ns > 0 (proves the gated block executed), NOT *_fork_count >= 1 (that arm never fires on fauxware). See test_fork_counters_exposed_and_non_summable in tests/engines/rust/test_manager_core.py.

fork() freezes local→shared in place ONLY when push_level==0. Inside a push/pop transaction, transaction_rollback truncates local back to its pre-transaction length and pops the Z3 solver frame — if we drained local during the transaction, those constraints would still be in shared (and the Z3 solver's pop wouldn't remove them because the solver replay still runs from shared+local on materialize). Skipping freeze inside transactions falls back to allocating a new merged Vec (current behavior, costs O(N+M) Bool clones). Helpers: freeze_z3_assertions / freeze_assumed_constraints in native/angr/src/symbolic/context.rs (lines 2024+).

Fork hot-path audit (angr-0mqkc.7): the RustSimState fork path is already cost-optimized, NOT a clone-cost problem. Config fields hooks/environment/sim_options are Arc<...>-CoW (make_mut); arch is Box over ZST singletons (arch_from_vex clone ~free); concretizer is POD memcpy; inspection holds an empty Vec in production; solver is Rc-forked (unavoidable); fs shares file content via internal Arc. The remaining genuinely-deep clones (history, detailed_history, call_stack, heap_metadata, native_resume_stack) are per-state data APPENDED EVERY STEP, so converting to Arc-CoW gives no win -- make_mut copies on the next append anyway, only adds Arc overhead. Do NOT Arc-ify these. The real smell was DRY: 6 near-identical struct literals in state/fork.rs. fork/fork_true/fork_false/fork_from_snapshot now delegate to a shared fn fork_with(registers, memory, solver, child_id); merge + translate_state keep own literals (they merge/Z3-translate fields). A new RustSimState field must be threaded through fork_with once instead of 4x. All 7 non-test arc_with_non_send_sync allows already carry parallel-design comments.

Memory-model + VEX-interp + slow-bench/arch mining session (2026-06-23, sibling to z3 epic angr-ovqja): 3 research agents -> adversarial peer review (all claims verified vs source). RESULT: the productive vein was the FORK PATH eager-copy asymmetry (SymbolicMemory pages are O(1) CoW but registers/caches/py-maps are eagerly cloned per fork). FILED epic angr-6t8z3 'fork-path eager-copy perf' with children: 6t8z3.1 Arc-wrap RegisterFile::data CoW (arch/mod.rs RegisterFile::fork deep-copies 1060B GUEST_STATE_SIZE every fork; spike, watch serde RegisterFileData shadow + symbolic FxHashMap clone); 6t8z3.2 reset wider_load_cache empty on fork (rebuildable memo, from_snapshot already restores empty); 6t8z3.3 skip Python::attach in state/fork.rs clone_py_metadata when symbolic_pages/hook_symbolic_memory/addr_to_ast all empty. Plus standalone angr-kdyfx guard load_concrete sidecar probes behind is_empty() (load-path, related to epic). All provable via state_fork/memory_fork/load_8bytes criterion benches (no run_single needed); shared faithfulness gate = fork isolation preserved. REJECTED: per-op counter fetch_add collapse (overhead measured below noise floor, pdq8-counter-overhead-validated); persistent to_z3_ast FFI cache (DUPLICATE of ovqja.3, premise bounded by closed angr-behq). CONFIRMED NOT-ACTIONABLE (do not re-litigate): VEX dispatch already well-tuned (Z3 dominates wall-clock); mma_howtouse 0.65x + android_arm 0.42x both attributed by closed campaign angr-9w6ad to NON-engine fixed cost (angr-core CLE page-init / one-time PyO3+Z3 init) with candidate engine fixes rejected on faithfulness (benchmark-w4oo3-register-sync-noop); callbacks not the bottleneck (callback-bottleneck). Only open arch item = ig3o.2 AArch64-BE, blocked upstream on archinfo (angr-b3sc).

SUPERSEDED 2026-07-14 by [invariant-fork-metadata-arc-not-py] (commit 27f44e7f4). The empty-map early-return it describes NO LONGER EXISTS: state/fork.rs::clone_py_metadata no longer calls Python::attach AT ALL — the overlays hold SharedPyAst = Arc<Py>, so cloning them is a GIL-free atomic refcount bump in every case, empty or not. Do not re-add the early-return guard; there is nothing left to guard. The observations that remain TRUE and worth keeping: (1) the criterion state_fork bench forks with empty maps and had NO initialized Python interpreter, so ANY unconditional Python::attach on the fork path PANICS under cargo bench — that bench is a standing tripwire for a reintroduced GIL attach in fork; (2) clone_py_metadata is called from fork/fork_true/fork_false/fork_from_snapshot/merge, so all five inherit whatever the fork path does.

Float format specifiers %f/%e/%g (printf + scanf) must NOT be implemented natively in procedures/{sprintf,scanf}.rs — same faithful-reimpl wall as %n (see format-n-no-native-parity). Python angr's format_parser.py::FormatString does NOT support floats: replace() (printf path) only handles {s,d,i,u,c,x,o,p} and hits 'raise SimProcedureError(Unimplemented format specifier ...)' for anything else; the addr-based interpret() (sscanf-from-memory) only handles {d,i,u,o,x,p,s,c} and raises on the rest. The %f/%e/%g entries in format_parser's SPECIFIER_MAP (SimTypeDouble) are calling-convention metadata for the PARSER only — the OUTPUT formatter still errors. A native float formatter/reader would succeed where Python errors, diverging from the engine we mirror. The existing catch-all _ => ProcedureError::Other arms in sprintf.rs format_string + scanf.rs parse_scanf_format already reproduce Python exactly for free. Pinned by regression tests test_sprintf_float_specifiers_fall_back / test_scanf_float_specifiers_fall_back. Closed angr-11djq.19 as won't-implement (commit f8ce2cc04). REOPEN only if upstream Python angr adds float formatting to format_parser AND a real workload needs it.

format %n (printf/scanf) must NOT be implemented natively in procedures/{sprintf,scanf}.rs — it would diverge from Python and break the faithful-reimplementation invariant. Python angr's format_parser.py::FormatString does NOT support %n uniformly: replace() (printf path) has no %n arm and hits 'raise SimProcedureError(Unimplemented format specifier n)'; the addr-based interpret() (sscanf-from-memory) hits 'raise SimProcedureError(unsupported format spec n in interpret)'; only the SimPackets interpret() path (scanf-from-stdin/file) treats %n as a numeric read. A single native behavior cannot match all three, and writing the byte/char count would succeed where Python errors. The existing ProcedureError->Python fallback (b'n' arms in sprintf.rs format_string + scanf.rs parse_scanf_format) reproduces Python exactly for free. Pinned by regression tests test_sprintf_percent_n_falls_back / test_scanf_percent_n_falls_back. Closed angr-11djq.17 as won't-implement on these grounds (commit 3524883df). Same principle likely applies to any spec Python's format_parser raises on.

format_parser.py interpret() has TWO internal dispatch sites that must BOTH be patched when fixing a scanf spec: (A) the SimPackets/stdin-packet-stream path (~line 156-163 in the 'if simfd is not None and isinstance(simfd.read_storage, SimPackets)' block, sets base via if x->16 elif o->8 else->10) and (B) the addr-based path (~line 286-292, 'if fmt_spec.spec_type in [d,i,u,o,x,p]'). The %p fix 2f8deb4ca patched ONLY (B), leaving (A) parsing %p as base 10; fixed in feb38d5e0 (bead angr-rgcfx) with binary-free test_scanf_p_spec_simpackets (feed concrete stdin to scanf, %2p '10' -> 0x10 with fix, 0xa without). Lesson: sscanf tests exercise path (B); only scanf-from-stdin with a SimPackets/SimPacketsStream stdin exercises path (A). Related: format-parser-three-dispatch-sites.

FormatSpecifier.spec_type (angr/procedures/stubs/format_parser.py) returns self.string[-1:].lower() — it ALWAYS lowercases the conversion char. So %X is indistinguishable from %x at every dispatch site (parsing routes both to base 16); case-distinct output (%X uppercase hex) requires branching on the case-preserving fmt_spec.string[-1:], NOT spec_type. Corollary: adding b"X"/uppercase branches keyed on spec_type is DEAD CODE. Also: commit 129bd9e645 (2025-09-22) introduced a digit-strip regression in FormatString.replace() printf path by refactoring hex(c_val)[2:]/oct(c_val)[2:] -> f-string{c_val:x}[2:]/{c_val:o}[2:]; hex()/oct() have 2-char prefixes ('0x'/'0o') that [2:] stripped, but f-strings have none, so [2:] dropped 2 significant digits (0xFF->''). Fixed in 2b9099b29 (bead angr-vp1dg) by dropping [2:]. Related: format-parser-three-dispatch-sites.

glibc.json/glibc_decls.txt fortify _chk prototypes have had wrong arg order more than once. __sprintf_chk omitted flag/slen (angr-tx7ec.1); __fprintf_chk listed [flag, STREAM, TEMPLATE] but real glibc ABI is __fprintf_chk(FILE *fp, int flag, const char *fmt, ...) = [STREAM, flag, TEMPLATE] (angr-iv0hv, fixed in b5aefdc53). When adding a native fortify wrapper, DIVERGENCE-CHECK the proto in BOTH angr/procedures/definitions/common/glibc.json and glibc_decls.txt against the actual glibc bits/stdio2.h signature, not the JSON. The native wrapper (NativeFprintfChk in procedures/fortify_printf.rs) and Python subclass (__fprintf_chk in libc/fprintf.py) both drop the injected flag and DRY-forward to the base proc; run() arg order is what actually drives extraction, but fix the proto too for CFG/decompiler consistency.

Fortify _chk libc variants (__memcpy_chk/__memmove_chk/__memset_chk/__mempcpy_chk, and the str family) must IGNORE the trailing destlen arg and forward to the base proc — that is exactly what Python angr does (procedures/libc/{memcpy,memmove,memset,mempcpy}.py: each _chk subclass calls super().run() dropping _destlen). Do NOT emulate the glibc runtime bound check (__chk_fail abort): it would diverge from the Python engine and prune paths angr otherwise explores, creating a cross-engine divergence bug. Native impls live in procedures/fortify_mem.rs, registered in procedures/mod.rs NativeProcedureRegistry::new. __mempcpy_chk has no native mempcpy base, so it reuses NativeMemcpy.call then returns dst+n (dst_bv.add(size_bv)). Pattern: declare_proc! with the 4th arg named _destlen (underscore prefix avoids the unused-binding warning under -D warnings).

Native fortify str _chk family (__strcpy_chk/__strncpy_chk/__strcat_chk/__strncat_chk/__stpcpy_chk, procedures/fortify_str.rs) required adding Python procs TOO, unlike the mem family. CRITICAL ASYMMETRY: Python angr ships __memcpy_chk etc as subclasses in libc/memcpy.py, but had NO str _chk procedures — those names hit SimLibrary.get_stub -> ReturnUnconstrained. A native-only _chk impl that actually copies DIVERGES from the Python engine's stub (native copies real bytes; pure-Python/fallback returns unconstrained), a cross-engine bug. Fix: mirror memcpy.py by adding Python subclasses in libc/{strcpy,strncpy,strcat,strncat,stpcpy}.py (run(...,_destlen)->super().run(...) dropping destlen) so BOTH engines copy. LESSON for remaining tx7ec _chk beads: before implementing a native _chk, grep Python angr (grep -rn NAME_chk angr/procedures/) — if absent, add the Python subclass in the SAME commit or you create divergence. __stpcpy_chk has no native stpcpy base, so it reuses NativeStrcpy.call then returns dest+strlen(src) via find_null_addr.

RESOLVED by angr-62ar5 (commit 1cdd4f219) — see invariant-fork-prior-guard-replay for the mechanism and the standing rule. Historical: pbounce found states could be UNDER-CONSTRAINED, carrying none/some of the width-region branch guards, so the exported witness replayed to acc&0xff != 0xee. Diagnosis method still worth reusing: do not trust the engine's own witness — export the Rust constraint set with mgr._rust_mgr.export_state_constraints(id) and re-solve independently, then print only the non-byte-binding constraints. Affected serial AND parallel; serial passed the content gate only because Z3 happened to pick a satisfying model.

Audit (2026-05-07, HEAD=d2752ebe0): every FP op in native/angr/src/vex/ops.rs has a concrete fast path. Coverage: float_neg/abs (bitwise, always fast), float_sqrt/add/sub/mul/div/madd/msub (as_u128 guards lines 1215-1407), vec_float_scalar_op/sqrt/max/min (as_u128 guards lines 1409-1559), vec_float_op/unop/minmax (total_width<=128 && as_u128 guards lines 1739-1937), float_to_int/float/i{32,64}{s,u} and rm-aware variants (as_u128 guards lines 2316-2621), binop_with_rm/unop_with_rm RNE-concrete short-circuit to Self::binop/unop (lines 442-477). TWO INTENTIONAL GAPS not worth filling: (1) non-RNE concrete rm + concrete operands in binop_with_rm/unop_with_rm route through Z3 (no portable Rust rounding-mode intrinsics); (2) AVX 256-bit packed FP (total_width>128) falls through to symbolic Z3 path because as_u128 caps at 128 bits. Neither matters for fairlight (xmm-only) and per fairlight-bottleneck-2026-05 the 95% bottleneck is Z3 path-condition accumulation (z3_site_branch_true 700-820ms/call), not single-op FP cost. This anchors the angr-faws Option-A wontfix decision: do NOT add a RUST_FP_LEGACY opt-out (would re-introduce the silent-constraint-drop correctness bug fixed by 769d1ee54/fcf33c14c/37983a77b/d0377abb9).

Z3 has no FloatOpKind::IsNan but the IEEE 754 identity is_nan(x) ⇔ NOT(x == x) gives the same answer cheaply. Both Z3_mk_fpa_eq and Rust f32::== / f64::== return false when either operand is NaN, so building (NOT (Cmp_eq x x)) produces a 1-bit BV that's true iff x is NaN. Used in FCmpScalarLane (Un variant) and FComCC for the unordered branch. Avoids adding a new FloatOpKind variant.

cudgw.5 (symbolic FP non-RNE rounding fallback) was already resolved by angr-tfjl before the task was worked: binop_with_rm/unop_with_rm in vex/ops.rs and the conversion fns route concrete-non-RNE AND symbolic rm (and symbolic operands) through Z3 via build_fp_arith_rm_cached/build_fp_f_to_i_cached/build_fp_f_to_f_cached in symbolic/value_z3.rs. OpError::SymbolicFloatUnsupported was dead (never constructed) and was removed. All FP paths mask rm & 0x3, deliberately collapsing VEX tie-away modes 4-7 to 0-3 — the native f64 fast path can't do tie-away anyway, and the masking is consistent across concrete and Z3 paths.

fp_simd_kernel synthetic bench (angr-amtxu, tests/benchmarks/synthetic_examples/fp_simd_kernel/) fills the one corpus gap from the iter50 hzd9e audit: no FP/SIMD-heavy workload existed, so vex_fallback_count/vecret_gsptr_fallback_count read ZERO everywhere (see benchmark-vecret-gsptr-corpus-zero). RESULT: native VEX handles ALL SSE FP/SIMD ops natively — collector reports vex_op_fp=3, vex_op_vec=90 dispatched, both vex_fallback_count=0 and vecret_gsptr_fallback_count=0. So FP/SIMD is NOT a native-coverage gap. Rust 1.04s vs Py 0.12s (characterization fixture, not a speed win). FIXTURE-BUILD PITFALLS (all hit during amtxu): (1) gcc -O3 constant-folds scalar FP when the input is a compile-time constant — declare the input as a VOLATILE seed so sqrtsd/divsd/mulsd survive into the binary; (2) __builtin_sqrt with a runtime arg emits a libm sqrt-symbol call (errno) — compile with -fno-math-errno to lower it to the sqrtsd instruction; (3) blank_state leaves rsp SYMBOLIC, and -O3 vectorized loops fork on stack-pointer alignment-peel checks — set state.regs.rsp to a concrete 16-aligned CANONICAL addr (0x7FFFFFFFF000; a non-canonical >47-bit addr like 0x7FFFFFFFFFF0000 makes runs hang/timeout); (4) keep N small (16) + few scalar iters so the kernel reaches main ret within MAX_STEPS=200 (non-unrolled loops cost 1 block-step each).

Pattern for testing symbolic-rm float ops (RoundF32/F64toInt, ConvertFtoIRm, ConvertFtoFRm): pick a concrete value whose rounded result differs across all 4 VEX rounding modes (0=RNE, 1=floor, 2=ceil, 3=trunc). Then constrain the result BV equal to one specific target, and assert (ctx.eval(rm) as u32) & 0x3 == expected mode index. Useful values: -2.5f32→{RNE:-2, floor:-3, ceil:-2, trunc:-2}, 2.5f64→{RNE:2, floor:2, ceil:3, trunc:2}. Z3 only sees the low 2 bits (extract(1,0) in build_fp_round_to_int_cached) so don't constrain the upper 30 bits — use a mask in the assertion.

cb_execution_error_to_typed in native/angr/src/engine.rs cannot use From for RustExecError because the mapping needs runtime context (addr, arch) that From cannot carry. The mapping for OpError::UnsupportedNeon/UnsupportedVectorOp/UnsupportedVexOp all fold in arch_name, and InvalidIR/LiftError mappings need the block addr. Wrapping in a ContextualizedError struct was considered and rejected as more noise than value. Instead, angr-qga2 (commit 8d97db0ab, 2026-05-31) split the function into two exhaustive matches (CbExecutionError + OpError) without a _ wildcard, so adding a variant now fails to compile until triaged. This achieves the same compile-time guarantee as From + ? without the wrapper overhead.

When a VEX op is exposed as a Binop with rm but modeled as a unop in IROp, the cleanest fix is to add an arm to VEXOps::binop that delegates to unop_with_rm. Why: keeps the special-case centralized in one file (vex/ops.rs), makes the routing directly unit-testable via VEXOps::binop(IROp::FSqrt, rm, value, &ctx), and avoids touching interpreter_cb/expressions.rs Binop dispatch. How to apply: any future case where opcode_map collapses a (rm, val) Binop into a unop IROp variant can follow the same pattern — add a binop arm that calls Self::unop_with_rm(op, left, right, ctx).

tests/benchmarks/property_fuzzer.py has 17 eligible examples but only 2 (flareon2015_10, mma_howtouse) are NOT in the rust_only-derived KNOWN_DIVERGE allow-list. Default sampling will produce ~88% expected-diverge / ~12% pass trials. The fuzzer is a regression GUARD (catches new divergences) not an oracle. Long-term improvement: audit rust_only=True flags and promote stable cases to broaden the pass-eligible set.

tests/benchmarks/property_fuzzer.py revealed defcamp_r100 in BFS mode produces matching Rust/Python output, yet it is flagged rust_only=True in run_regression.FAST_SUITE. Either marked conservatively or DFS-only divergent. Audit the rust_only=True FAST_SUITE/MEDIUM_SUITE entries with the fuzzer to identify promotion candidates (move off rust_only, restore Python output comparison). The fuzzer's KNOWN_DIVERGE set is computed from the same flag, so promoting examples will tighten the gate.

Cannot place runnable scripts at tests/property_fuzzer.py (or any tests/foo.py invoked as 'python tests/foo.py'): the tests/types/ subpackage shadows the stdlib types module because Python prepends sys.path[0]=tests/ when running a script from that dir. argparse → re → enum → from types import MappingProxyType fails immediately. Fix: place runnable scripts in tests/benchmarks/ (or any non-tests subdir). Pytest invocation works fine because the script dir is not on sys.path.

Native fwrite (procedures/stdio.rs) resolves FILE._fileno at an arch-specific offset matching cle.backends.externs.simdata.io_file.io_file_data_for_arch: AMD64=112, X86=56, ARM=14, ARM64=20, MIPS32=56, MIPS64=112. Read as 4-byte int via state.memory_load(file_ptr + offset, 4). Negative _fileno propagates -1 per fwrite spec; non-1/non-2 fd falls back to Python (current native dispatch only knows stdout/stderr buffers). Other archs not in the table also fall back. The Python proc returns byte count (size*nmemb), not nmemb, because it forwards to SimFileDescriptor.write_data which returns size — match that exactly.

interpreter_cb hook_addrs / simprocedure_registry / vex_opt_level_overrides (Arc<HashMap|HashSet>) and exploration::RustExplorationManager.vex_opt_level_overrides are now FxHashMap/FxHashSet (commit a37018771, angr-teo2). Per-block .get()/.contains() in execution.rs:32,134,178,358,394 / interpreter_cb/mod.rs:1175 benefit from FxHasher on integer keys. Remaining std HashMap candidates noted in invariant-fxhash-internal-keys but not yet swapped: claripy_bridge::CLARIPY_AST_CACHE (RefCell<HashMap<u64, Py>>), symbolic::registry::rust_id_to_py (RwLock<HashMap<u64, Py>>), symbolic::table::symbols (RwLock<HashMap<u64, RustBV>>), stash::state_index/state_roots, exploration::helpers::counts (cold).

Despite presenting as 'MIPS32 $t0 collapses to concrete zero in accumulation chain', the angr-g9hy bug was NOT MIPS-specific and NOT in the symbolic register file or the IRSB execution. Root cause: disk init cache invalidation logic (_state_has_user_symbolic) only checked memory for user symbolic, not registers. When a user did 'state.regs.a0 = BVS()' the cache key was still valid, the cached blank_state replaced the user's state, the symbolic a0 was lost, and Rust executed the entire chain with concrete a0=0. Reproduces on MIPS32 because that arch lacks Python fallback paths that would have masked the issue on AMD64. The non-determinism in the bead description (N=5,20,50 failing; 10,30 passing) was actually fluke: with a0=concrete 0 in Rust, the only states reaching FOUND came via accidental fork paths or solver default-value coincidences (eval(a0) on unconstrained var returns 0 or first-tried value). Lesson: bug reports describing arch-specific symbolic-register collapse may actually be cache-coherence bugs upstream of the engine.

angr-vhot triage (2026-06-04, HEAD c0d706acf): the reported 'state.solver=None' AttributeError on defcon2016quals_baby-re under ANGR_RUST_USE_CALLBACK_MEMORY_PROXY=1 is NOT a dangling reference in angr code. The literal source is solve.py:36 — 'flag = chr(sm.one_found.solver.eval(c))' — accessing .solver on None. sm.one_found returns None when the 'found' stash is empty: sim_manager.py:845 'return self._stashes.get(stash[4:], [None])[0]'. The exploration deadends fast (1 deadend, 0 found, 0 active) at corrupted PC 0xf2aff9eee1eeffff after just 2 of 13 my_scanf SimProc calls; the 8-byte deadend PC resembles a concatenation of two 32-bit witnesses for flag_0+flag_1. Gate-OFF baseline: OK in 0.46s. DECISION: do NOT add a guard in angr (would mask the real gate-on regression) and do NOT 'fix' the dangling reference (it's user-code accessing documented None semantics). Follow-up task angr-5aj8 created to investigate the actual deadend cause (likely either Iend_LE byte-order asymmetry in proxy.store for symbolic ASTs, or symbolic-PC concretization picking a bad witness in Rust). Original hypothesis in angr-vhot about SimProc callbacks seeing a successor with state.solver=None was wrong.