catch / 5

procedures/scanf.rs::NativeSscanf passed record_stdin=true to do_scanf until angr-ggb66 (commit 1223da0a8), so sscanf — which reads a memory buffer, never fd 0 — consumed harness-seeded stdin bytes (post-ptf54, via mint_stdin_bytes on the %s path) and recorded its minted symbols into the stdin reconstruction. Python's sscanf calls FormatString.interpret(addr=...) with NO simfd and touches stdin not at all. Now source='sscanf', record_stdin=false. Lesson: do_scanf's record_stdin flag gates BOTH stdin recording and seed consumption — set it only for readers that genuinely read fd 0 (scanf/__isoc99_scanf, and fscanf only when fileno==0).

vec_float_scalar_lane_binop / vec_float_scalar_lane_minmax / vec_float_scalar_sqrt in native/angr/src/vex/ops.rs do extract+concat per call on the symbolic-fallback path. Closed as wontfix (angr-8f7d, 2026-05-07): on fairlight (the only FP-heavy benchmark), prerequisite profiling (angr-q2dk) found expr_eval = 14ms over 11109 calls and Z3 = 95% of runtime (branch_true alone is 9-11s of ~13s total). The whole interpreter side is well under 1% of wallclock — there is no headroom to chase in SSE scalar lane extraction. Concrete fast paths in these ops already exist (left.as_u128() / right.as_u128() guard). Future FP work should target Z3 path-condition accumulation, not interpreter micro-ops.

Stack page init sync bottleneck: _extract_symbolic_regions scans 4096 bytes byte-by-byte via memory.load(addr,1) = 137ms. Fix: (1) Use UltraPage.concrete_load(0, 4096) for concrete bytes (<0.1ms vs solver.eval 20-150ms). (2) Use page.symbolic_data dict to find symbolic offsets, scan only those ranges instead of all 4096. AVOID: importing wide symbolic objects via symbolic_data values — causes 2.5x state_create regression because downstream import_symbolic_to_state handles wide objects differently. Must import individual bytes to match the original behavior.

angr-630x stash-name validation landed: StashManager::ensure_stash() centralizes the entry().or_insert_with() pattern across _create_state/_add_state/_merge_states/_move_state/_move_states. log::warn! fires once per fresh non-standard name (standard = active/found/avoid/deadended/errored/pruned/unconstrained). Default log level is 'off' so it's opt-in via set_rust_log_level('warn') or ANGR_RUST_LOG=warn. Behavior is typo-tolerant — state still placed in the new stash. Adding a new stash-mutation method? Use sm.ensure_stash(name) instead of sm.stashes_mut().entry(name).or_insert_with(VecDeque::new) so future typos go through the same warn.

Cache-write sites in rust_callback_dispatch.py that grow _state_cache during exploration (kept intact in angr-qm7w but candidates for future migration to plugin-overlay): line ~980 _resume_with_state, ~1123 _resume_with_skip_hook, ~1296 _handle_syscall_callback, ~1474 _handle_symbolic_branch_callback (the high-volume per-fork copy). _add_rust_state at rust_manager.py ~1862/1912 writes the initial root state. The mixin _cleanup_state_cache in rust_state_cache.py is dead code — overridden by rust_manager.py's version per MRO.

BUG (fixed in 7fe7baf79): _cleanup_state_cache had a two-phase design where the LIVE filter (active|found|live-roots) ran BEFORE the pinned/overflow step. The pinned set protected entries during overflow eviction but NOT during the live filter. So when state 0 (root) left active_set after forking, the live filter deleted it before pinning could save it. This wasn't visible until qm7w (67d46f940) (a) tightened cap to 8 and (b) called cleanup after every callback, surfacing the bug. Manifested as 'No cached state for ID N, using blank state fallback' followed by fwrite on a blank state filling thousands of 4096-byte pages. Fix: live |= set(self._state_roots.values()) before the live-filter delete loop. INVARIANT: any state-cache cleanup must merge roots into 'live' OR the pinned set must be enforced at every deletion site, not just overflow.

State export: _sync_exported_constraints takes 5.9s for sym-write (O(n) constraint conversion + identity checks). Skipped entirely since Rust solver fallback (eval_with_fallback, eval_upto_with_fallback) handles all common solver operations. The fallback tries Python solver first, falls back to rust_mgr.fork_state_solver(state_id) on failure.

Documentation pattern for state.inspect limitations in rust_engine.rst: instead of redirecting users to a Python-only fallback, enumerate three workarounds in priority order: (1) recast the analysis as a supported event — e.g., 'call' BP → 'exit' BP filtered on jumpkind=='Ijk_Call'; reg_read/write/instruction/irsb/exit/mem_* cover most low-level observation; (2) drop to use_rust_engine=False for events that fundamentally require Python plugins; (3) use coarse manager-level hooks (set_progress_callback at rust_manager.py:3105) + post-run stash iteration when per-statement granularity is unnecessary. The substitution table is useful guidance because angr-d46u (2026-05-22) already wired enough events that most BPs have a structural equivalent.

2026-06-11 multi-agent state review (workflow wf_7e5ea602-f71): 10 review angles (3x rust core, python-bridge, tests, bench, docs, backlog, memories, desired-state-gap) -> 61 raw findings -> dedup -> 58 candidates -> 2-lens adversarial peer review (batched 5/agent after per-candidate review proved too token-hungry) -> 56 confirmed, 2 refuted (notably: 'uninit registers read zero' divergence empirically disproved — register sync triggers Python default filler). Created 49 beads labeled state-review-2026-06: 48 findings + angr-dqo2 (8 audited updates to existing beads). Top P2s: angr-21am (LoadG width), angr-37d4 (arm64g ccalls), angr-p05r (floordiv signedness), angr-c3rd (Bool rebuild), angr-8o7w (syscall BVS aliasing), angr-pfbu (MIPS $a3), angr-iu40 (identity-tracker leaks), angr-rpqk (write-through gates), angr-vx8p.3 (CGC stdin sync). Full audit trail: /tmp/rust-symex-review/result.json (ephemeral). Lesson: batch peer-review lenses (5 candidates/agent) and digest-in/decisions-out dedup to survive session token limits; workflow resume cache preserved all 10 reviewers across 4 rate-limit windows.

StateId newtype carve-out (angr-okca, exploration/) differs from the memory/address.rs precedent in a key way: exploration/ owns NO state-id-keyed collections — the state_index and state_roots maps live in StashManager (stash.rs), a different module whose public API is all u64 and is OUT of scope. So unlike address.rs (which migrated address-keyed HashMaps to the newtype), StateId has no owned-map to migrate. The adoption that IS faithful: (1) accessor APIs (find_state/find_state_mut/with_state/with_state_mut/index_state/unindex_state) take impl Into so all ~150 u64 callers — especially the Python-boundary _xxx(state_id: u64) #[pyclass] methods in state_api.rs — compile unchanged; (2) exploration-owned fields like current_stepping_state_id become Option; (3) transient locals that immediately round-trip through the u64 StashManager stay raw u64 and convert at the boundary via StateId::raw(), exactly as address.rs keeps page numbers raw. Python-facing getters keep u64 (convert via .map(StateId::raw)). Lesson for the remaining borb children: check whether the subsystem actually OWNS id-keyed storage before promising a full HashMap migration; if storage lives in another module, the win is API-signature type-safety, not collection migration.

Stdio status/write SimProcs reuse the FILE._fileno dispatch pattern from fwrite (fileops::read_fileno + fd_offset_for_arch): NativeFeof returns 1 if fd_info().pos >= content_len else 0 (negative fd → 0, not -1, to mirror Python's None-on-missing-simfd short-circuit collapsed by caller); NativeFerror always returns 0 because FileSystem doesn't track per-fd I/O errors (decl-only in glibc.json — native dispatcher is the ONLY path that handles ferror); NativeFputs reads up to MAX_FPUTS_LEN=4096 bytes (matches MAX_FWRITE_SIZE), appends to state.write_fd(fd), returns 1 on success / -1 on negative fd. All at native/angr/src/procedures/stdio.rs.

stdio-fwrite-fputs-arbitrary-fd's caveat that state.write_fd/FileSystem::write is 'NOT position-aware — a seek-then-write would diverge' is now FIXED (commit 994707c63): FileSystem::write is POSIX positioned-write. See memory write-fd-position-aware. The rest of stdio-fwrite-fputs-arbitrary-fd (fwrite/fputs resolve _fileno, require concrete src, fwrite generalized from fd1/2 to any fd in b670c) still holds.

Per-state stdout_buffer in RustSimState (Vec), cloned on all 5 fork methods. Native puts/printf read strings byte-by-byte from memory (max 4096 bytes) and append to buffer. get_state_stdout(state_id) exposed via PyO3. Python _inject_rust_stdout() writes to posix.stdout via SimPacketsStream.write(None, BVV(data), events=False). Called during predicate eval and state export.

Steady-state parallel loop's found over-collection is FIXED (angr-op0dn.13.17, commit 1685784b9). Root cause: several resident workers reach a find addr (or finalize drains a residual frontier state sitting at one) before the num_find cancel propagates, and route_successor's find-gate re-collects them. Fix: RustExplorationManager::push_found_capped (helpers.rs) pushes a parallel found terminal into STASH_FOUND only while found_count()<num_find; surplus -> push_to_active_or_drop (re-findable on resume). Wired at the 3 parallel found-routing sites in route_materialized_terminal (Found arm, Bounce->find-addr arm, None/residual arm). Single-threaded route_successor is UNTOUCHED so serial stays byte-identical. MEASURED post-fix on M5 fork_solve_pbounce_W3_S2_M8_B1: steady==serial==8 (num_find=8) and ==1 (num_find=1) across workers {2,4}; was 12/3-4. Regression test: TestParallelSteadyFoundCap in test_parallel_wave.py. NOTE (retained from a retired R4-merged memory): the parallel_workers= kwarg still engages the WAVE loop only and does NOT auto-arm steady — that is now for PERFORMANCE reasons (steady net-negative on corpus, hurts num_find=1), NOT the found accounting, which is fixed. steady_state_eligible() stays env-gated (parallel_steady_env).

OBSOLETE — steady found over-collection is FIXED as of angr-op0dn.13.17 (commit 1685784b9, push_found_capped). See steady-found-cap-fix for the current state. Historical: steady OVER-COLLECTED the found stash (steady=12 vs serial=8 num_find=8; steady=3 num_find=1) on M5 fork_solve_pbounce_W3_S2_M8_B1. The parallel_workers= kwarg still engages the WAVE loop only and does NOT auto-arm steady — but that is now for PERFORMANCE reasons (steady net-negative on corpus, hurts num_find=1) NOT the found accounting, which is fixed. steady_state_eligible() stays env-gated (parallel_steady_env).

store_concrete_lazy cleanup at store.rs:153 now handles same-base wider-sym truncation (angr-7qon): when old_bytes > size, the surviving tail bytes [addr+size, addr+old_bytes) have their page bitmap bits explicitly cleared via Page::clear_symbolic. The symbolic_spans entries for those bytes were already removed by the pre-existing 1..old_bytes loop, but the page bitmap clearance was missing — page.store_concrete only clears bits within the concrete write range. Without this, surviving bytes appeared symbolic in the bitmap with no symbolic_objects/symbolic_spans entry, breaking subsequent loads with 'symbolic bytes not fully tracked'. Walk handles cross-page tails by iterating page-by-page. Companion to angr-jvjf (load-side bitmap guard) — same root-cause family (sidecar drift vs page bitmap).

store_stmt_time_ns in interpreter_cb/statements.rs IRStmt::Store is recorded ONLY on the first-try Ok(()) success path through try_rust_memory_store — not on retry-after-page-fetch success, not on Python callback fallback. This may be an oversight in the original code but is preserved exactly across the angr-6ls8 refactor. If you are touching that timing in future work, decide deliberately whether to extend it to the retry path or leave the divergence.

Strategy for SimOptions that ship in default bundles but are silently ignored under Rust (e.g. TRACK_CONSTRAINT_ACTIONS, TRACK_MEMORY_MAPPING): can't warn-on-add without spamming every entry_state(). Solution (angr-383x, 2026-05-11): promote state.history's class to _RustOwnedSimStateHistory in restore_plugins_to_state — overrides .actions/.events properties with a process-wide warn-once latch. Fires only when user code actually reads the empty stream, so default-bundle users see nothing. Code in angr/exploration/rust_state_export.py; tests under TestEdgeCases::test_history*_warns_under_rust.

STRICT_PAGE_ACCESS Python→Rust wiring (commit 924113068, extended in 888c5c8bf): (1) RustExplorationManager._add_rust_state checks angr_state.options before add_state and calls rust_state.set_enforce_permissions(True). (2) _apply_state_metadata also copies the option from src to dst on init-cache hits. The flag survives Rust-side fork() (per memory.rs invariant). To query a state's flag from Python: rust_mgr.state_enforce_permissions(state_id) -> bool. With the flag on, both load/store check R/W AND basic-block fetch checks X (per invariant-nx-block-fetch). Pattern parallels how LAZY_SOLVES is wired.

strnlen is a poor target for TestSymbolicLibcProcedures-style integration tests: the harness hooks at an IN-BINARY address (0x4008C0, fauxware .fini) so Python-init short-circuits, but that same is_in_binary guard means native procs (incl. NativeStrnlen) are intentionally SKIPPED there -- the Python SimProcedure always runs. vanilla Python strnlen IGNORES maxlen when the string is longer (returns full strlen, not min(len,maxlen)), so strnlen(buf='ABCDEFGH\0', maxlen=3) returns 8 via both engines -- faithfulness preserved but no rax assertion expresses correct C strnlen semantics. The native impl itself is correct (cargo test_strnlen_at_limit). ROOT CAUSE of the in-harness fallback is now CONFIRMED + tracked in [[strnlen-fallback-root-cause]] (the is_in_binary skip, NOT a strnlen defect, NOT a divergence). NOTE: per-variant native_proc_stats fallback buckets (native_proc_symbolic/not_implemented/other_fallbacks_by_name) ARE surfaced via mgr.native_procedure_stats() / mgr.stats() since angr-ilsr -- the older claim that they aren't is stale. By contrast strncmp/strcasecmp ARE good targets (angr-n6vm8) because their correct contract matches Python's.

strstr integration tests (TestSymbolicLibcProcedures) must use CONCRETE haystack/needle: the Python strstr SimProc (angr/procedures/libc/strstr.py) forks per candidate position on symbolic input (max_symbolic_strstr loop), so _run_one_step's exactly-one-post-call-state assertion fails. Concrete strings keep it single-path. Pattern: rax-only asserts (return is haystack+offset for a hit, 0 for not-found) per rust-proc-integration-test-rax-only. Tests landed in f5a6cdfa4 (angr-qa7my).

strtod native SimProc is amd64-only: FP return on SysV ABI uses xmm0 low 64 bits (offset 224 in the amd64 register file). On x86 it would be st0 (x87 stack), on aarch64 it would be d0 — neither slot is in the integer-return path our dispatcher uses, so we punt to Python via Err(ProcedureError::NotImplemented). The native procedure SUPPRESSES the dispatcher's default integer-return rax store by returning Ok(None). See native/angr/src/procedures/strtod.rs and AMD64_XMM0_OFFSET=224 constant — mirrors crate::arch::amd64::offsets::XMM0 (kept local to avoid one-constant cross-module reach).

strtoll/strtoull width caveat: on LP64 (amd64/aarch64) long long == long == 64 bits, so the shared run_strtol engine produces the right result. On ILP32 (x86/arm32) long long is 64 bits but the integer return register is 32 bits — caller would expect a split eax:edx return our dispatcher doesn't model. Both procedures gate on state.arch().bits() < 64 and return ProcedureError::NotImplemented for ILP32, letting Python handle the wide-return ABI. See native/angr/src/procedures/strtol.rs near 'NativeStrtoll'.

Sub-1.5x bench perf attribution (dva9j.1): buckets by counter/run_wall ratio. Z3-floor: fauxware, unmapped_analysis, flareon2015_2, CADET_00001, angry-reverser, sokohashv2, fairlight. boundary-tax/GIL-dominated (gil_work_time 0.56-0.93 of wall -> Zero-Python/gorvf targets): xmllint_getenv, android_arm_license_validation, cmu_binary_bomb_partial, google2016_unbreakable_1. interp-bound: google2016_unbreakable_0. UNATTRIBUTABLE (Callable-driven, mgr.stats() empty so run_single --counters-json emits nothing -> see angr-dva9j.7): mma_howtouse, flareon2015_10. Method: run_single.py --counters-json, ratios = z3_check/gil_work/python_callback _time_ns over run_wall_time_ns.

sym-write 7s bottleneck is 275 Z3 concretization calls (one per symbolic store). Per-block caching doesn't help since each store has unique address expr (buf+0, buf+1, etc). Would need lazy symbolic memory model like Python to avoid upfront concretization.

sym-write performance spike (angr-12vc, 2026-06-05): the premise of the bead was a math error. Bead claimed '0.436x speedup, Rust 2.29s slower than Python 1.0s' and that sym-write was documented in rust_engine.rst 'Known slower benchmarks'. ALL FALSE. baseline_timings.json fields rust_time/python_time are ABSOLUTE SECONDS, not ratios. For sym-write: rust_time=0.436s, python_time=1.0s, so speedup = 1.0/0.436 = 2.29x FASTER. Live measurement (HEAD 1a5b2243b) Rust 0.56s / Python 1.02s = 1.82x speedup, peak_mem 200MB vs 185MB. The bench is one of the faster ones in the corpus, not slower. rust_engine.rst 'Known slower benchmarks' section (line 2844) lists mma_howtouse, sokohashv2, fairlight, unbreakable_1 — sym-write is NOT in it. The 4 sym-write mentions in rust_engine.rst are all in characterization tables (concretize sweep, mem_ite_depth, sym_write SimOption row). DECISION: no implementation work needed, no rst doc change needed. Closed angr-12vc as not-an-issue. Memory lazy-memory-load-overlay-fails, symwrite-eager-vs-lazy-memory, and symwrite-rustbv-to-claripy-bottleneck describe a HISTORICAL slowness (6.9x, 5.9s bottleneck) that has since been fixed by prior commits (notably the deferred-fork rustbv_to_claripy skip).

sym-write 30s timeout bisected (May 2026) to commit 85c59c7a0 ('fix: route unsupported non-eflags CCalls to Python VEX'). Pre-regression rust_time ~0.4s/0.42s (benchmark-arc-concretize-cache memory); post-regression ~1.6s (benchmark-phase41-symwrite memory). Methodology was the same as 9maq-bisect-method: subprocess wrapper with RLIMIT_AS=4GB, narrow over 8 git checkouts. (NOTE: this memory was accidentally overwritten 2026-05-17 by running bd remember --key without a content arg — restored from inference of related memories. If detail needed, run git log --oneline -- benches/baseline_timings.json or read CLAUDE.md sym-write row history)

SymContext.symbol_table on context.rs is essentially dead data. It is only ever populated by merge() (which writes to a freshly-constructed merged context) and read by merge() (which copies entries between contexts). new()/with_timeout() create empty maps; no live runtime path inserts into it during BV creation or constraint addition. Could be removed entirely; meanwhile Arc avoids the per-fork clone cost.

The eager-mode symbolic-branch Python bounce (CallbackReason::SymbolicBranch) was a pure no-op round trip: handle_symbolic_branch_callback (angr/exploration/rust_callback_dispatch.py) converted the guard to a claripy AST and passed true/false constraint lists to resume_after_symbolic_branch, which STARTS with 'let _ = (true_constraints, false_constraints);' — it sources the guard from stored_conditions instead. Retired 2026-07-14 (angr-gorvf.14, commit cad2e0ab9) by handle_symbolic_branch_core in exploration/core_outcome_handlers.rs. LESSON for future bounce retirements: before designing a native replacement, read the Rust resume* pymethod first — several of them ignore what Python computes, so the 'Python work' is only the FFI round trip. The only producer of RunResult::SymbolicBranch is the !use_deferred_forks path in interpreter/statements.rs (IRStmt::Exit), i.e. the angr-027h phase-2 eager retry; deferred mode never emits it. NOTE the Python handler + resume_after_symbolic_branch pymethod are now unreachable dead code, deliberately left in place.

11djq.6.1 (symbolic file content for non-stdin fds) shipped as the STREAM slice, not the FILE slice. FileDescriptor.symbolic:bool flag (#[serde(default)]) + FileSystem::open_symbolic/is_symbolic (native/angr/src/state/filesystem.rs); NativeReadSyscall (syscalls/read.rs) routes a flagged read-fd with no concrete content through the shared read_symbolic() helper (prefix sys_read_fd), minting fresh unconstrained bytes exactly like stdin. This faithfully models a SimPackets STREAM (no EOF, returns count every read). The harder BOUNDED symbolic FILE case (finite symbolic size -> short reads/EOF parity with Python SimFile) is STILL deferred: it needs storing symbolic ASTs in the FS, but FileSystem serde is Vec-only and the snapshot system handles symbolic only via Bucket-D Py overlays (state/snapshot.rs) -- a large ripple, NOT just an 'EOF trap'. Zero production blast radius: open_symbolic has no Python caller (open/openat syscall still uses content-less open), same test-only-reachable status as open_with_content (see fread-python-boundary-unreachable-content). Future state-export wiring is the natural next step to make it reachable.

Symbolic-file export observability (angr-4ref8 pt2, HEAD after commit): export-skip decisions live ENTIRELY Python-side in RustExplorationManager._export_fs_files_to_rust (rust_manager.py), NOT in Rust — so their counters are Python-side too, unlike symfile_reads_native/symfile_write_demotions which are Rust AtomicU64 in symbolic/stats.rs (reads/demotions happen natively). Counters: self._stats_symfile_exports (int) + self.stats_symfile_export_skips (dict pre-seeded with reasons subclass/has_end/not_seekable/file_exists/endness/size/path_utf8/error/preamble), bumped at each scope-gate 'continue', merged into the stats @property as symfile_exports + symfile_export_skip. KEY FACT: Python-side self.stats* counters DO feed --dump-counters and bench_diff because run_single.py dump_counters_table/json read mgr.stats (the @property) which merges Python + Rust counters — no FFI needed to make a Python-side count bench-visible (proxy*/callback* work the same way). Pattern for a Python-side decision counter: init attr in init near self.stats_proxy*, bump at site, add to stats() result dict.

angr-qluof pt1 (lineage-aware symbolic-file demotion, merge path): FileSystem (state/filesystem/ — struct in mod.rs, demotion impl in symbolic.rs; see filesystem-module-layout) carries a persistent demoted_paths: Arc<HashSet> that ACCUMULATES (never removed) cwd-normalized paths demoted by native writes. Recorded in demote_symbolic_content (the registry key) and demote_all_symbolic_content (all current file_contents keys before nuke). Exposed via FileSystem::demoted_paths()->Vec and FileSystem::demote_path(path)->bool (re-applies a demotion WITHOUT bumping record_symfile_write_demotion — it's a re-add correction not a guest write). FFI: RustExplorationManager.get_demoted_paths / demote_file_path (mod.rs + pending_api.rs _get_demoted_paths/_demote_file_path). Python merge() (rust_manager.py) queries each source lineage's demoted paths BEFORE the _merge_drop, pairs them per group with the merged state (via sid_by_state_key/id() map, since merge_func/base.merge produce NEW state objects), and after _add_rust_state (now RETURNS the resolved sid) re-applies via demote_file_path, counting self._stats_symfile_redemotions (exposed as symfile_redemotions in stats()). COVERED: merge re-add only. NOT covered: legacy-fork-push (rust_callback_dispatch) + cross-manager-transfer re-add sites. WHY: re-export re-arms the write-demotion (harmless content-wise but reverts guest write→-1). See symfile-export-skip-counters, symfile-native-export-design.

angr-qluof pt2 (u9tc6) closed: lineage-aware symbolic-file demotion now covers ALL re-add sites. Single-source helper RustExplorationManager._reapply_demoted_paths(source_mgr, source_sid, target_sid) (rust_manager.py) queries source native mgr's get_demoted_paths and re-applies via self._rust_mgr.demote_file_path, bumping _stats_symfile_redemotions. source_mgr is a NATIVE mgr handle (scratch.rust_mgr = self._rust_mgr, set in rust_state_export.py) — demoted paths are cwd-normalized strings so they port across managers. Wired at: (1) legacy-fork-push _add_forked_state (rust_callback_dispatch.py, after _add_rust_state, parent=event.callback_state_id); (2) cross-manager transfer in _add_rust_state (rust_manager.py, after _export_fs_files_to_rust, source=old_rust_mgr/old_state_id from angr_state.scratch). merge() does NOT use this helper — it must query BEFORE its _merge_drop and unions across lineages. Python-only change, bench-inert. See symfile-lineage-demotion-qluof (pt1).

Bounded symbolic file content native serving (angr-0xyq2, shipped 2026-07-03, commits ee7ea9c/e352549/2a683d4+Phase4). DESIGN: FileDescriptor.content_sym (Option<Arc<Vec>>, one 8-bit BV per byte) + path-keyed FileSystem.file_contents registry; Python export at _add_rust_state (_export_fs_files_to_rust in rust_manager.py) pushes fs.cwd (UNCONDITIONALLY — review-confirmed getcwd/path-normalization parity) then per-file byte ASTs via register_file_content PyO3; native open() attaches; read/fread/sys_read/pread64/readv serve via read_sym/read_sym_at. Bridge BVS-identity preservation means NO constraint sync-back needed — native branch constraints bind the original Python ASTs on the found state. V1 SCOPE GATE: exactly-SimFile, has_end is True, seekable, file_exists is True, endness Iend_BE (LE files' Python read windows are address-reversed per read — no fixed byte order matches), size eval_one-unique in (0, 65536], UTF-8 path. SERVE CLAMP: MAX_SYMFILE_SERVE_SIZE (filesystem.rs) = 65536 = export cap — MUST stay >= the export cap or reads >4096 silently truncate and fread items>clamp return 0 forever (review-CONFIRMED bug, fixed pre-commit). KNOWN V1 LIMITS: writes demote to Python ownership (demote_symbolic_content); position not synced back to state.fs; mid-run re-adds (merge/legacy-fork/cross-manager) re-register content and re-arm the demotion limitation (verified harmless content-wise — the refused write never landed in either model). REFUTED optimization: one-wide-AST bridge crossing instead of per-byte — wide concrete BVV import is u128-capped (angr-cxw7), would regress concrete files; per-byte cost amortized by bridge AST cache. Proof: asisctffinals2015_license TIMEOUT->0.9s. Tests: tests/engines/rust/test_symbolic_files.py + read_tests/fread_tests serve counterparts. Docs: rust_engine.rst 'Bounded symbolic file content' bullet.

sym-write's 30x regression is NOT caused by symbolic stores (ITE chains fixed, only 2 callbacks). The bottleneck is per-step predicate evaluation: state.posix.dumps(1) is called every step for callable find/avoid predicates, taking 17s of the 30s total. Fix requires per-state stdout buffer (task angr-34w.10).

sym-write regression 0.42s→3.22s (angr-q7r0) was NOT memory__symbolic_full callbacks (audit hypothesis was wrong; only 3 mem-load callbacks fired). True bottleneck: callback bundle export of pending state's edx register. After main runs, edx contains a deeply-shared ITE-chain DAG (142,133 expanded nodes from only 25 unique Arc-shared subtrees). rustbv_to_claripy walked the tree without memoization, creating 142k Python objects (~2.7s for one register). __libc_start_main's 'after_main' continuation triggers a SimProcedure callback, create_state_for_callback exports all symbolic registers eagerly, and edx's conversion alone consumed the entire regression budget. Fix: pointer-identity memoization in rustbv_to_claripy. The audit's bisect candidate (commit 30702fa5a memory_symbolic_full wiring) was a red herring.

sym-write 5.9s bottleneck was rustbv_to_claripy() in deferred fork Exit handler. The guard expression contains deeply nested ITE chains from symbolic stores. Converting to Python claripy ASTs recursively creates millions of Python objects. Fix: skip the conversion — condition is already stored in stored_conditions as RustBV (the claripy AST was only a P11 fallback). Impact: 12.18s → 6.46s.

Two paths into Rust memory from a Python seed state with mixed symbolic+concrete on the same page (rust_state_sync.py): (a) _sync_extra_python_pages now pushes the page via concrete_load even if symbolic_pages includes it — concrete bytes interleaved with the symbolic store reach Rust correctly. The previous skip was based on the (wrong) assumption that the symbolic-import path covers the whole page; it only covers symbolic byte ranges. (b) Symbolic positions are still rewritten by _pending_symbolic_imports applying import_symbolic_to_state in _add_rust_state, so the symbolic identity survives unchanged. Loader symbolic pages (rare) still skip _map_loader_pages because mapped_page_addrs filters them — they fall through to _sync_extra and get the same treatment.

tests/benchmarks/synthetic_examples/ holds in-repo benchmark workloads for arches whose binaries are not in angr-examples (MIPS, etc). run_single.py::_resolve_examples_dir falls back to this dir when EXAMPLES_DIR//solve.py is missing. baseline_timings.json works as before (one entry per name); rust_only=True + python_time=null in baseline skips the SLA gate for trivial workloads where PyO3 init dominates.

syscalls::extract_concrete_arg(arg: &RustBV, name: &str) -> Result<u64, SyscallError> lives at native/angr/src/syscalls/mod.rs (added angr-h7yo, commit 9063dcd97). Mirror of procedures::extract_concrete_arg with SyscallError::SymbolicArgument(name) variant. Use it for all symbolic-arg fallthrough sites in new syscall handlers — don't open-code args[i].as_u64().ok_or_else(|| ...). Naming convention for the 'name' string: ' ' (e.g. 'mmap addr', 'rt_sigaction signum') — preserves test assertions like msg.contains("addr").

Closed in commit 5f7dbb19b (angr-pqgu, iter 21). setuid/setgid native handlers now landed via SyscallOutcome::ContinueSymbolic returning fresh RustBV::symbolic of arch.bits() width, matching Python syscall_stub.py::syscall semantics. The 'setuid_setgid_intentionally_absent' cargo test was replaced by 'setuid_setgid_registered_on_all_arches' in syscalls/mod.rs. The invariant stands: native syscall handlers for syscalls with no Python SimProcedure should mirror the stub-fallback (fresh symbolic, NOT Continue { ret: 0 }) — see key 'syscall-stub-fresh-symbolic-pattern' for the macro recipe.

T2-MEASURE (angr-11djq.4 iter17) xmllint_getenv fallback profile via run_single.py --counters-json: bounded find=getenv slice => 27 Python SimProc fallbacks {strcmp:10, pthread_once:4, pthread_mutex_lock:4, pthread_mutex_unlock:3, malloc:3, calloc:1, getenv:1, time:1}, 112 native simproc dispatches succeed, and ZERO syscall fallbacks / native_proc fallbacks / vex fallbacks. Tier-2 verdict: pthread_* half of angr-11djq.8 JUSTIFIED (11 hits) but __ctype_b_loc NOT (0 hits); angr-11djq.7 (fd/file sync) and .9 (format gaps) NOT justified by this slice (0 syscall, 0 format fallbacks) — the bounded getenv path does no file I/O or printf. SURPRISE -> angr-oppte: strcmp/malloc/calloc fall back to Python WITHOUT incrementing native_proc_symbolic_fallbacks (=0), so they bypass native dispatch entirely (angr use_sim_procedures hook owns the symbol, Rust runs the Python hook instead of substituting its native proc). grub half punted (>4GB RLIMIT_AS OOMs the 6G ralph scope).

ExplorationTechnique compatibility with RustExplorationManager (angr-zidj, 2026-06-01): 6 native (DFS, BFS, Explorer-int-only, LengthLimiter, Timeout, CheckUniqueness-x86/amd64), 1 fallback (LoopSeer), 2 raising/unsupported (Veritesting via EFFICIENT_STATE_MERGING raise; Threading blocked on angr-8fo6 Send/Sync audit), 1 semantics-mismatch (Oppologist), 10 untested (Spiller, MemoryWatcher, Tracer, Director, Slicecutor, Stochastic, Bucketizer, DrillerCore, ManualMergepoint, StubStasher, Suggestions). Anything not in the dispatch ladder in rust_techniques.py:30-194 falls through to ordinary filter()/complete()/successors() dispatch via RustStateProxy — accepting silently rather than raising. Documented matrix at docs/advanced-topics/rust_engine.rst:1660. When asked 'does X technique work with Rust?' check the matrix first; if untested, vet against the proxy read-only invariant before assuming yes.

Oppologist exploration technique has a SEMANTICS MISMATCH with the Rust engine that surfaces silently: it catches angr.errors.SimError to single-step around unsupported instructions, but the Rust engine raises typed RustError exceptions (RustUnsupportedVexOpError, RustMalformedIRSBError, etc.) which are NOT subclasses of SimError. The except clause misses them, so the user sees a RustError bubbling up unhelpfully instead of the oppologist taking over. Documented in docs/advanced-topics/rust_engine.rst 'Exploration technique compatibility' section (angr-zidj, commit c714e9e15).

Oppologist is structurally incompatible with the Rust engine for a deeper reason than just exception-class inheritance: the technique ONLY overrides successors() (no step/setup/etc — confirmed via Oppologist.dict membership = {'successors'}), and RustSimulationManagerProxy.successors() raises NotImplementedError. So the recovery hook never executes under Rust, regardless of whether the typed RustError inherits from SimError. Even if we exposed successors() dispatch, two MORE issues remain: (1) RustError doesn't inherit from SimError so the except clause misses, (2) Rust*Error has no .executed_instruction_count / .ins_addr so _delayed_oppology would AttributeError. The chain-of-three is documented in docs/advanced-topics/rust_engine.rst 'Exploration technique compatibility' table (Oppologist row) and 'Known incompatibilities' section (commit de3bc9528, angr-v4qi closed).

simprocedure_fallback_by_name (angr-97l8, 2026-05-17): per-procedure Dict[str,int] fallback counter exposed via mgr.stats() and mgr.get_fallback_stats() under key 'simprocedure_fallback_by_name'. Sum of values == scalar simprocedure_python_fallback_count. Use this to prioritize next round of native SimProcedure implementations — top entries are the procedures still falling through to Python. The Python-side perf report (get_performance_summary) prints the top 10 entries inline. NOTE: not exposed via get_solver_stats() (that's process-wide Z3 counters only).

The CLAUDE.md test-count line uses 'grep -c def test_' which UNDERCOUNTS vs pytest. Today: grep returns 484, pytest collects 492 (8 extra from @pytest.mark.parametrize expansion). Prior refreshes (angr-k25z 2026-05-11 and angr-rap4 2026-05-22) used the grep number. Going forward keep using the grep number (matches the embedded command) but note the pytest expansion delta inline so readers don't trip on the discrepancy. As of 2026-05-22 the gap was 8 (484 → 492).

test-coverage audit of rust-symex (2026-06-20/21, bead angr-szg45, COMPLETE). All 5 areas scan+verify done. Confirmed gaps: python-bridge 1 (rust_callback_dispatch.py:2431 _create_blank_state_fallback cache-miss reconstruction; szg45.1); exploration 4 (helpers.rs apply_uniqueness_filter:218 run-but-unasserted, compute_register_tuple_hash:188 sentinel branches, extract_procedure_args:641 stack-spill+SpSymbolic/StackUnmapped uncovered while extract_syscall_args has tests, resume.rs:277 _resume_after_error callback-raise path HIGH); memory 3 (mod.rs:928 SymbolicMemory::merge all ITE/page-adopt/symbolic-union/pending branches short-circuit in tests HIGH, load_concrete_or_unconstrained, +1); interpreter 8 (2 high); symbolic 2 (1 high). REJECTED/covered-indirectly (do NOT re-flag): ALL rust_disk_cache.py save/load/extract family (_save_init_to_disk_cache, _load_init_from_disk_cache, _deserialize_init_state, extract*) - exercised by repeated entry_state-fauxware runs, ~/.cache/angr_rust_init/ has 12 populated .pkl; apply_native_techniques Timeout arm (test_explore_with_timeout_technique); _set_pending_register_symbolic (legacy fallback); _move_states filter_fn branch (unreachable, Python filters instead). CAVEAT: a resume re-verify of python-bridge contradictorily re-flagged the disk-cache fns - that re-verdict was DISCARDED; disk-cache fns ARE covered.

test_rust_exploration.py was split (angr-yg2m) into the tests/engines/rust/ PACKAGE: 14 modules grouped by area (manager_core, proxy, proxy_gates, solver_ops, solver_output, multiarch, syscalls, procedures, plugins, state_sync, strategy_vex, annotations_edge, error_stash, misc) + init.py. 774 def test_, 912 parametrized; multiset of test names identical to the old monolith. Shared fixtures/helpers (RUST_EXPLORATION_AVAILABLE, RustExplorationManager, RustSimState, fauxware_project, etc.) come from tests/engines/conftest.py (angr-7gdp), NOT duplicated per file. To find which file holds a given test cited in an old memory/comment as 'test_rust_exploration.py::Foo::test_bar': grep -rl 'def test_bar' tests/engines/rust/ (names are unique across the package). Run the suite via 'pytest tests/engines/rust/' (Makefile RUST_TESTS, make test-quick).

Test pattern for python-registered native procedures (see test_rust_exploration.py::_setup_amd64_python_proc_test): build amd64 RustSimState with 4KB stack, write 8-byte return addr at [rsp], populate RDI/RSI/RDX/... per arg_values, register procedure + hook addr, set callbacks. After mgr.run(N), inspect via mgr.native_procedure_stats() ('native_calls', 'python_fallbacks', 'call_counts') and the returned ExplorationEvent. For symbolic args use claripy.backends.z3.convert(bvs).as_ast().value to get the Z3 ptr for set_register_symbolic.

Threading.Thread subclasses must NOT define methods named .stop() or fields named ._stop — both shadow Python's threading.Thread internals (._stop is set by _bootstrap as the join-coordination event). Symptom: TypeError 'Event' object is not callable raised from threading.py during join(). Use .halt() / ._halt instead. Hit this 2026-06-03 in fleet_resource_profile/run_fleet.py RssSampler.

angr-tkbr.1 audit (2026-05-30, iter 1): the bd description's '48 panic sites in syscalls/' was stale — every panic!/unwrap()/expect() in native/angr/src/syscalls/ is inside #[cfg(test)] blocks. Production code already: (a) defines SyscallError enum at mod.rs:42 with SymbolicArgument/Other variants, (b) returns Result<SyscallOutcome, SyscallError> from NativeSyscall::call (mod.rs:66-70), (c) routes Err(_) → fall-back-to-Python in exploration/stepping.rs:252-256 (intentional silent fallback; documented at mod.rs:38-40 'Returning Err falls back to the Python _handle_syscall_callback path so semantics remain identical'). The only production assert-equivalent is one debug_assert! at mprotect.rs:103 (compiles to nothing in release; documented as a sanity check for already-verified pages-mapped invariant). RustExecError::UnsupportedSyscall variant + RustUnsupportedSyscallError Python class exist (engine.rs:1670, errors.rs::register); they fire via _raise_typed_test_error helper for pytest.raises coverage. The bd description's 'bubble through engine.rs into RustExecutionError' contradicts the intentional fast-path/slow-path pattern: native handler Err means 'fall back to Python', not 'fail the state'. Conclusion: tkbr.1 is moot; 0hif.1 can proceed against existing SyscallError contract.

angr-tkbr.2 (commit 8b9ff2713, 2026-05-25): parse_opcode no longer silently rewrites unmapped opcodes to IROp::Raw(0). New IROp::Unmapped(&'static str) variant captures the original pyvex op name; dispatch in VEXOps::{unop,binop,ternop,qop} returns OpError::UnsupportedVexOp{op_name:String}; interpreter_cb/expressions.rs forwards via Err(e @ OpError::UnsupportedVexOp{..}) => CbExecutionError::Op(e) BEFORE the silent fresh-symbolic Err(_) arm; execution_error_to_typed maps to RustExecError::UnsupportedVexOp{op_name,arch}. The &'static str is interned (Box::leak into a OnceLock<Mutex<HashSet<&'static str>>>) so IROp can keep deriving Copy and repeated lookups don't leak duplicates. Test: vex::opcode_map::tests::test_unmapped_opcode (asserts std::ptr::eq across repeated calls). Python test: TestRustExecutionErrorHierarchy::test_raise_unmapped_op_via_execute_irsb.

tkbr3-typed-error-api

tools/rebuild-rust.sh provides deterministic Rust .so rebuild: deletes angr/rustylib*.so + build/, cargo clean, pip install. Modes: --keep-cargo-cache (skip cargo clean), --cargo-only (skip pip, build via cargo + cp librustylib.so → angr/rustylib.<EXT_SUFFIX>.so — recovery for corrupt venv). The .so target name comes from sysconfig.EXT_SUFFIX so it matches setuptools-rust output. Uses python -m pip not pip directly (some venvs lack the pip executable script). Commit 987898f65, 2026-05-09.

TooLarge symbolic address concretization in memory.rs had 3 silent failure paths: (1) load_symbolic_unified returned fresh unconstrained BVS 'mem_unbounded_*' with no relation to actual memory, (2) store_with_concretization returned Ok(()) doing nothing, (3) store_symbolic_unified returned Ok(Some(result)) doing nothing. All now return Err(MemoryError::SymbolicAddress) which triggers Python fallback. interpreter_cb.rs store path needed explicit SymbolicAddress handler to fall through to Python (previously caught by Err(e) => CbExecutionError::Memory which errored the state).

translate_state wall cost (bench_translate_state_scaling in native/angr/benches/vex_engine.rs, angr-9pwjd): at realistic leaf counts the cost is dominated by a ~3ms FIXED per-state floor, NOT leaf count. Measured leaves_8=3.00ms, leaves_64=3.22ms, leaves_256=3.71ms => per-leaf slope only ~2.5-4us/leaf (each leaf carries a memory cell + constraint AST + Z3 assert, so ~3-4x the bare 709ns/leaf translate_into primitive from panhl.2). The ~3ms floor is target-solver create + assertion seeding via add_constraint_raw. CONSEQUENCE for Option-A worker pool (angr-1ilq): every cross-context state migration pays a ~3ms fixed tax regardless of state size, so work-stealing must amortize migration over substantial work — do NOT migrate states cheaply/frequently. panhl.2's 'leaf-count-dominated' prediction holds only asymptotically (very large states).

RustSimState::translate_state(target_ctx:&z3::Context)->RustSimState (state/fork.rs, commit 9ca2fce61) is the whole-state cross-context twin for shared-nothing parallel (Option A). Composes RustBV::translate_into per component: RegisterFile::translate_into (arch/mod.rs, symbolic overlays), SymbolicMemory::translate_into (memory/mod.rs: symbolic_objects+multi_objects+pending_writes; pages/bitmaps/spans are ctx-independent, wider_load_cache starts cold), MultiPayload/PendingWrite::translate_into, SymContext::translate_into (snapshot_fork_ops.rs), last_time. Identity preserved (state_id/parent_id carry over - same state, new context, NOT a fork). INVARIANT: target_ctx MUST be the active thread-local z3 ctx (new SymContext solver + add_constraint_raw build against thread_local) AND distinct from source (Z3_translate panics same-ctx). Production runs it on the target worker thread after set_thread_local. Py overlay maps (symbolic_pages/hook_symbolic_memory/addr_to_ast) are claripy Python ASTs = ctx-independent, clone_ref'd like fork.

fauxware perf flipped from 0.9x to 1.36x (rust 0.28s vs python 0.38s, 5-run median, 2026-05-11). Root cause of the flip: NativeRead/NativeWrite default-registration in angr-3tek.2 (2026-05-10) eliminated 4 read() callbacks (~80ms) and let strcmp/open also benefit from the page-replay fix. Callback count went 6→1 (only open() now). Profile breakdown of the 280ms rust runtime: init 20.9ms (7%), open SimProc 59ms (20%, 43ms execute + 13ms sync + 3ms create), lift_block x14 ~3ms (1%), and the remaining ~205ms (72%) is Rust VEX interp + Z3 — no FFI hot path remains. Lesson: stale 0.9x bead descriptions should be re-measured before pursuing optimization work; the underlying cause (read callbacks) was already fixed elsewhere. baseline_timings.json rust_time updated 0.385→0.28.

angr-uahs (mremap full semantics) closed won't-fix 2026-06-06 (iter 278). Pattern: 'beyond-Python-parity greenfield extension with no current motivator'. Evidence: (a) zero benches grep-match mremap in tests/benchmarks/; (b) Python angr also stubs it (no angr/procedures/.../mremap.py, only syscall_stub fallback); (c) current Rust handler at native/angr/src/syscalls/memory_extras.rs:30 (NativeMremapSyscall) is at parity with Python's stub. Reopen criterion: a workload that actually invokes mremap AND branches on the returned address such that stub-symbolic semantics produce wrong constraints. Generalization: same template as angr-528r close — Beyond-parity greenfield work without a motivating workload is YAGNI for the symex engine. Other tickets in the same family that may close on this basis: angr-bjk8 (worker pool teardown, gated on parallel infra), angr-j7kn (theory propagator, sweep already proved no bench benefits). Apply this template before doing speculative implementation work.

context.rs split slice 1 (angr-ugc2): the solver perf-counter block lived at context.rs lines ~203-963 and was cleanly extractable to symbolic/stats.rs because every counter is a module-level atomic with zero self./SymContext refs. Mechanics that worked: make statics/consts pub(crate), keep record_/get/reset fns pub, add 'use super::stats::' (plain glob) in context.rs for the ~50 internal fetch_add sites + timed_check/sample_simplify_skip, repoint mod.rs re-exports and value.rs imports to 'stats', and change the context test-module's 'use super::Z3_EXTREMA_' to 'use super::super::stats::'. CheckSite is #[cfg(feature=vex-engine-z3)]-gated but NUM_CHECK_SITES/SITE_NAMES/site arrays are not (get_solver_stats uses arrays not the enum). NOTE: venv pip is broken (resolvelib ImportError) -- must rebuild via tools/rebuild-rust.sh --cargo-only.

After closing umbrella beads, the 'consolidation memory' worth keeping is the design verdict in the close reason itself — bd close --reason captures it permanently in the closed-bead log, and the cross-referenced bd memories are the load-bearing artifacts. No extra memory file needed when the close reason already names every relevant memory key.

Audit of unwrap()/panic!() in native/angr/src (2026-04-20): 306 unwrap() and 13 panic!() total, but only 1 panic (solver.rs sym_context()) and 1 unwrap (icicle.rs set_isa_mode) were in production code. All others are in #[cfg(test)] blocks or are safe expect() calls on known-good invariants (NonZeroUsize literals, validated arch names, guaranteed-Some Options). The codebase is already well-disciplined about error handling in production paths.

angr-uprs (commit 5dfd42f5b) added TestRustUnsupportedErrorParametrized at tests/engines/test_rust_exploration.py:12491-12758, with 4 parametrized lists pinning the typed-exception surface against silent regressions: _UNMAPPED_X87_TRANSCENDENTALS (10), _UNMAPPED_NEON_QSHL_IMM (12), _UNMAPPED_FP_DECIMAL (10), _UNMAPPED_CRYPTO_AND_POLY (8), _NEON_UNIMPLEMENTED (1: Iop_PwAdd32Fx2 only), _UNSUPPORTED_SYSCALLS (23). The 40 unmapped VEX ops go through execute_irsb_for_test (lightweight mock-context path) and assert exact-subclass RustUnsupportedVexOpError. When an op gets a real dispatch arm, MOVE IT OUT of the relevant list (don't just delete) — the lists are the contract that says 'these are the ones still missing'. The count-floor assertion test_total_case_count_meets_acceptance enforces total>=50 so a thoughtless trim still fails fast.

uq4n.3 mem_read dispatch wiring (2026-05-16): instrumented IRExpr::Load in native/angr/src/interpreter_cb/expressions.rs via dispatch_mem_read_inspect helper. Approach: collapse 8 internal early-return sites into a single labeled 'load: block; each 'return Ok(value)' became 'break 'load value;'. The block's value is the trailing expression from the load_from_callback or build_ite_load_from_callbacks paths (which now use ? since the block carries the function's Result context). Single dispatch site after the block. Concrete-address only — symbolic addresses are skipped. State_id plumbed via CallbackInterpreter::current_state_id (set in stepping.rs::run_interpreter_step). NOT YET wired: state.rs::memory_load wrapper (used by SimProcedures — same plumbing gap as mem_write side; state.rs has no PythonCallbacks reference), IRExpr::LoadG (guarded load at statements.rs:549), simple VEXInterpreter path (legacy, out of MVP scope).

uq4n.4 mem_write inspect dispatch wiring (2026-05-16): instrumented IRStmt::Store in native/angr/src/interpreter_cb/statements.rs via dispatch_mem_write_inspect helper. Plumbed state_id via new CallbackInterpreter::current_state_id field set from stepping.rs::run_interpreter_step. Dispatches when=after only with concrete-address only for MVP. NOT YET wired: (a) IRStmt::StoreG (guarded stores), (b) symbolic-address stores, (c) state.rs memory_store* wrappers (used by native SimProcedures — state.rs has no PythonCallbacks reference so needs different plumbing). When wiring mem_read (uq4n.3 follow-up), the survey memory inspect-mem-dispatch-surfaces enumerates 8 sites in IRExpr::Load fast paths (expressions.rs:49-170) that all need the dispatch_mem_read_inspect helper — single state.rs surface won't cover them.

In memory/load.rs, the slow-path scan at site 1 (~line 209) and site 2 (~line 675) for a wider symbolic object containing the load range is effectively dead in real usage: it only fires when has_inner_overlap=true AND try_byte_merge_load returns None. byte_merge consults symbolic_spans per-byte; for byte_merge to fall through, some load byte must lack BOTH symbolic_objects and symbolic_spans entries — meaning the wider sym does not fully cover. So the wider-containment search at the slow path rarely succeeds in production. The angr-uwtj fix (commit a66e2c33a) replaces the O(n) scan with O(1) spans-first lookup + linear fallback; the speed win comes from avoiding the iteration cost when symbolic_objects is large, not from changing the result. Bench impact was modest (~8% mma_howtouse, ~12% noisy unbreakable_1).

angr-v5ht (commit 971d35545, 2026-05-24 iter 8): runtime thrash detection for use_shared_lineage_solver SHIPPED. Sampler hooks at TOP of run_loop iteration (every 10 iters, threshold 35% hot ratio over >=20 lineage_switch events), flips global LINEAGE_DISMANTLED atom on regression. SymContext::fork honors flag by skipping lineage minting AND parent-lineage-arc inheritance (child gets per-context solver from frozen_shared). 5-sample medians: baby-re 3.17s->1.03s (still 1.54x over 0.67s; needs FULL variant angr-0dgq for in-flight teardown); ais3 0.72s (preserves win); unbreakable_0 1.06s (FASTER than 1.39s baseline). Counters: lineage_dismantled, lineage_dismantle_count, lineage_sample_call_count, lineage_sample_decision_count.

angr-v5ht dismantle threshold of 35% justified on N=4 data points (angr-1gfa, 2026-05-25, commit 4ec879419). Measurements: run run_single.py <name> --use-shared-lineage-solver --counters-json, compute lineage_switch_hot_count / lineage_switch_count. LOSE: defcon2016quals_baby-re 30.2%. WIN: ais3_crackme 44.7%, defcamp_r100 51.0%, csaw_wyvern 84.2%. 35% sits in the gap (4.8 pp above LOSE, 9.7 pp below closest WIN). Both new measurements left lineage_dismantled=0 (correct, sampler kept lineage on). If a future bench drifts a WIN below 44.7% or a LOSE above 30.2%, revisit; otherwise the threshold is empirically stable. Hardcoded at native/angr/src/exploration/run_loop.rs:58 — tick_and_sample_for_thrash(10, 20, 35).

Subprocess-based perf-named tests (e.g. test_rust_no_worse_than_3x in tests/engines/test_rust_integration.py) that only assert success and print a ratio should be RENAMED to reflect reality (test_both_engines_succeed_and_report_timing), NOT given a hard ratio assertion. The authoritative perf gate is tests/benchmarks/run_regression.py + CI with bimodal-variance handling; a hard ratio in a subprocess test fights CI/subprocess timing variance and duplicates that gate. angr-x2d0, commit 479386f63.

Vacuous-test audit 2026-06-12 (branch rust-symex): filed 6 beads labeled tests,vacuous-tests — angr-x2d0 (3x-perf test asserts nothing, P1), angr-azsh (5 callstack-proxy tests pytest.skip on deterministic explore miss + 'if raw:' guards, P1), angr-o5jb (bare matches! x2 in interpreter/expressions.rs tests, P2), angr-e548 (5 assertion-free behavioral tests incl. unfalsifiable test_move_state_nonexistent, P2), angr-w9zj (tautological >=0 on unsigned counters, P3), angr-9dvt (factory/public-api strengthening, P3). REJECTED false positives — do not re-file: claim of '109 zero-assert tests' (AST scan says 24, most are legit no-raise smoke tests that fail by raising); 'if expected:' in test_rust_produces_correct_output (only sym-write has empty expected, deliberate+commented); except-Exception blocks at test_rust_exploration.py 2251/2349/7454/7467 (deliberate, contracts documented, final asserts falsifiable); SIMD exp-oracle concern in vex/ops.rs (expected values are independent constants — clean).

Vacuous-test cleanup pattern (label vacuous-tests, e.g. angr-azsh closed 2026-06-13): in tests/engines/rust/ many exploration tests used 'if not mgr.found: pytest.skip(...)' and 'if raw:' guards. fauxware explore(find=0x4006ed) is DETERMINISTIC (0x4006ed is inside main, reached via __libc_start_main from the ELF entry stub) — so a skip masks a real find-regression and an 'if raw:' guard masks an empty-exported-callstack regression. Fix: replace skips with 'assert mgr.found, ...' and 'if raw:' with 'assert raw, ...' then dedent so frame-shape asserts always run. Sibling open beads: angr-x2d0, angr-e548, angr-o5jb.

Recurring same-justification pattern in value.rs FP helpers: 'let raw = unsafe { Z3_mk_fpa_to_ieee_bv(raw_ctx, fp.get_z3_ast()).expect(...) }; unsafe { BV::wrap(&z3_ctx, raw) }' appears 5x (line ~2807/2811, 2889/2893, 2996/3000, 3043/3047, 3218/3222). Similarly Z3_mk_fpa_to_fp_bv→Float::wrap appears 5x. Could be lifted into 'fn fp_to_ieee_bv(z3_ctx,&Float)->BV' and 'fn bv_to_fp(z3_ctx,&BV,&Sort)->Float' safe wrappers in symbolic/value.rs to reduce audit surface; both helpers would internally hold one unsafe block with the same SAFETY justification. Not done in angr-59t3 (comments-only scope), but candidate for follow-up if reviewer asks for further consolidation. The wrap functions are themselves unsafe in z3-rs, so the wrappers would still contain unsafe — they just centralize the comment.

value.rs hot-path accessor #[inline] coverage (angr-m63z, 2026-05-31): all 11 accessors at lines 645-727 (width, is_concrete, is_symbolic, is_expression, as_u128, op, operands, into_arc, to_u128, as_u64, to_u64) already carry #[inline]. Both arms of define_unsigned_cmp_pair! (line 463: ult/ule/ugt/uge borrow+consume) and define_signed_cmp_pair! (line 512: slt/sle/sgt/sge borrow+consume) carry #[inline]. Workspace [profile.release] in /Cargo.toml sets lto='fat' + codegen-units=1, so LLVM has whole-program info for inlining decisions even on unannotated intra-crate forwarders. BVOp::is_unary/is_binary/is_ternary lack #[inline] but have ZERO callers in the codebase — speculative annotation has no benefit. Do not re-file as a perf bead without disassembly evidence (objdump showing call site emits 'call rustbv_width' rather than the matched-arm load).

value.rs god-object split (epic angr-7hwz) mirrors the finished context.rs split (a2br). DONE: .1 (commit 46800f02d) extracted the test module into sibling value_tests.rs (4734->3523). .2 (commit after 46800f02d) extracted the 2587-line 'impl RustBV' body into two sibling modules declared in symbolic/mod.rs: value_ops.rs (1497 lines: define_unsigned/signed_cmp_pair macros, canonicalize_commutative/canonical_sort_key, arithmetic/bitwise/compare/extend/extract/concat/ite/bit-count ops, plus free helpers ZExtCmp/try_zext_const_cmp_fold/sign_extend/sign_extend_to) and value_z3.rs (1220 lines, cfg vex-engine-z3: to_z3_ast/to_z3_ast_cached/to_z3_bool/to_z3_bool_cached/emit_extract_z3_cached/build_z3_ast_cached + build_fp_* builders). value.rs now 849 lines (enums+From+Debug/Display/PartialEq+accessors+test decl). all_ones_mask promoted to pub(super) (used by both value.rs 'ones' ctor and value_ops bitwise); canonicalize helpers MOVED to value_ops; Z3 reaches stats via qualified super::stats:: so no import churn. Inherent impls may live in any module of the same crate; siblings reach RustBV via 'use super::value::{...}'. Epic acceptance MET: every value-derived prod file <~1500 lines, clippy --all-targets clean, cargo fmt, 914 rust tests pass, fauxware --both correct. Symbol-move citation sweep done same iter (to_z3_ast_cached/to_z3_bool->value_z3.rs; try_zext_const_cmp_fold->value_ops.rs; test refs->value_tests.rs).

VAvg (Iop_Avg{N}{S/U}x{M}) rounding halving add pattern (angr-tukg.3): single IROp::VAvg { elem, count, signed } variant — both D-reg (total=64) and Q-reg (total=128); both signed (SRHADD) and unsigned (URHADD/PAVG). parse_vector arm uses vec_signed_arms!. Dispatched in binop() → Self::vec_rounding_avg(). Per-lane impl widens each lane to elem+1 bits (sign- vs zero-extend per signed flag), sums + adds 1, lshr by 1, extracts low elem bits. The +1 carry never overflows in elem+1 bits — this is the whole trick that makes the implementation match URHADD/SRHADD exactly. Distinct from claripy _op_generic_HAdd which is truncating (a+b)>>1 and uses bit-slice [vector_size:1]. Claripy has no op_generic_Avg so universality tests use z3-spec-replay-test-template (build reference inline with same widen/add/+1/lshr primitives). Tests added at native/angr/src/vex/ops.rs::tests::test_vavg*. ARM ref: DDI 0487 C7.2.420 (URHADD) / C7.2.353 (SRHADD).

VCnt/VClz/VCls per-lane unary count pattern (angr-tukg.6): three IROp variants in vex/ir.rs — VCnt { count } (only I8 lanes; ARM CNT only emits 8x{8,16}), VClz { elem, count }, VCls { elem, count }. Result type entries: VCnt 8→I64 / 16→V128; VClz/VCls match elem.bits()count → I64/V128. Parse routing: VCnt uses an explicit match (only two suffixes); VClz/VCls use vec_arms!. Unop dispatch routes Clz/Cls to a shared Self::vec_lane_count(arg, elem, count, kind, ctx) helper switched by LaneCountKind { Clz, Cls } enum. Symbolic shape mirrors claripy's op_generic_Clz ITE-chain (irop.py L700) applied per-lane: default value n (Clz) or n-1 (Cls); iterate bit positions a=0..n-1 (Clz) or a=0..n-2 (Cls), at each step build ITE(bit_a == 1, then_value, current) — Clz: then=n-a-1; Cls: cond is bit_a != sign_bit, then=n-2-a. Concrete fast-path uses u128 lane masking + .leading_zeros() with a -(128-N) adjustment. Tests at native/angr/src/vex/ops.rs::tests::test_vcnt, test_vclz_*, test_vcls_8x8_concrete.

SSE scalar MAXSS/MINSS/MAXSD/MINSD vector ops have no FloatOpKind::Max/Min variant. The Rust concrete branch uses '>' and '<' which return false for NaN — so Z3's fpa_max/fpa_min (IEEE 754 — return non-NaN if exactly one is NaN) do NOT match. Encode SSE max/min symbolically as ITE(FCmpLt(..., ...), l, r): max(l,r)=ITE(r<l,l,r), min(l,r)=ITE(l<r,l,r). FCmpLt returns false for NaN, so the ITE picks r (right operand) — same as Rust's '>' / '<'. See vec_float_scalar_lane_minmax in vex/ops.rs (commit fcf33c14c).

Vec_mul_lo concrete sign-extension chains like (l_elem as u32 as i32 as i64) as u64 for elem_width<64 do NOT fully sign-extend to u64 — they sign-extend to 2*elem_width and zero-extend the rest. This is bit-equivalent for downstream u64 wrapping_mul + low-elem_width mask, since only the low elem_width bits of the product depend on the operands' low elem_width bits. Replacing with full sign-extension to u64 is safe (verified manually against original behavior for {-1,8/16/32-bit} × {-1}). See vex/ops.rs:vec_mul_lo and Self::sign_extend_low_to_u64.

angr-q1oq vector op dispatch macro task estimated 250-350 line savings. Actual: -33 lines (net). Reason: each vec_* function has a unique CONCRETE bit-manipulation path (different per op: arithmetic vs comparison vs shift vs interleave), and a unique SYMBOLIC per-element loop (different .into method called per op). Only the concat-tail was identical across all 9 sites. A 'mega macro' that subsumed concrete+loop+tail would obscure ops that have intentional per-op specialization (e.g. signed widening in vec_mul_lo, sign-extend-to-mask in vec_cmp). The estimated savings overcounted what was actually duplicated.

Pattern for SSE scalar-in-vector ops (lane 0 = scalar op, upper bits = passthrough from left): in vex/ops.rs, after the concrete short-circuit, do: let l_lo = left.extract(lane_bits-1, 0, ctx); let upper = left.extract(127, lane_bits, ctx); let res_lane = build_float_expr(kind, prec, vec![l_lo, r_lo]); Ok(upper.concat_into(res_lane, ctx)). RustBV's existing extract/concat already canonicalize Extract(Concat(..)) so the pattern composes cleanly when the operand is itself a Concat. lane_bits = prec.bits() (32 for F32, 64 for F64).

The /home/ubuntu/repos/angr/.venv directory can lose its bin/ pyvenv.cfg and include/ entries while keeping site-packages intact (happened 2026-05-07 between sessions). To restore without reinstalling deps: python3 -m venv --without-pip --copies /tmp/ref then cp /tmp/ref/bin .venv/bin && cp /tmp/ref/include .venv/include && write .venv/pyvenv.cfg manually (home=/usr/bin, version=3.12.3). Site-packages already has angr editable install + claripy + z3-solver — they survive. Don't run pip install -e . to fix this — that risks reinstalling pinned angr deps from PyPI.

This venv (.venv on the loop machine, 2026-05-09) ships WITHOUT a /pip executable in .venv/bin/. Only python/python3/python3.12 are present. Any tooling that calls .venv/bin/pip will fail with 'No such file or directory'. Use .venv/bin/python -m pip instead — that always works. Discovered while building tools/rebuild-rust.sh.

Venv pip + setuptools-rust install path is currently broken on 2026-05-06: pip install -e . fails with ImportError: cannot import name 'RequirementInformation' from 'pip._vendor.resolvelib.structs' because resolvelib was repacked as .pyc only and lacks the new symbol. The .pth file for editable angr is also missing — only an __editable___angr_finder.pyc exists. Workaround for build/test cycles: (1) Z3_SYS_Z3_HEADER=/usr/include/z3.h cargo build --manifest-path native/angr/Cargo.toml --release, (2) cp target/release/librustylib.so angr/rustylib.cpython-312-x86_64-linux-gnu.so, (3) for run_single.py prefix with PYTHONPATH=/home/ubuntu/repos/angr since the editable install is broken. z3.h also missing from .venv/lib/python3.12/site-packages/z3/include/ so Z3_SYS_Z3_HEADER must point at /usr/include/z3.h.

Broken venv pip recovery (2026-05-25): when .venv/bin/pip is missing or .venv/lib/.../site-packages/pip is broken with 'ImportError: cannot import name RequirementInformation from resolvelib.structs', use tools/rebuild-rust.sh --cargo-only as the fallback. This invokes cargo build --release + copies librustylib.so directly into angr/, bypassing pip entirely. Verified working 2026-05-25 (angr-0hdq.2 session) — pytest tests/engines/test_rust_exploration.py runs 495/495 green after the cargo-only rebuild.

venv at /home/ubuntu/repos/angr/.venv/ is stripped down: only python/python3.12 binaries; pip is broken (ImportError: cannot import name RequirementInformation from pip._vendor.resolvelib.structs). To rebuild the .so use tools/rebuild-rust.sh --cargo-only — it bypasses pip entirely (cargo build --release + cp librustylib.so to angr/rustylib.cpython-312-x86_64-linux-gnu.so). Confirmed 2026-05-21.

Cargo-only rebuild path (tools/rebuild-rust.sh --cargo-only) remains the fallback when pip in .venv is broken (RequirementInformation import error from resolvelib). Symptom: '.venv/bin/pip3 install -e . --no-build-isolation --no-deps' fails with ImportError mid-resolver. Workaround: tools/rebuild-rust.sh --cargo-only builds via cargo + copies librustylib.so directly to angr/rustylib.cpython-312-x86_64-linux-gnu.so. Verified 2026-06-01 in angr-l4bs iter. The disk Z3 + venv site-packages remain intact; only pip's resolver is broken.

venv pip in /home/ubuntu/repos/angr/.venv is broken: pip._vendor.resolvelib.structs ImportError when running .venv/bin/python -m pip install. Use tools/rebuild-rust.sh --cargo-only --keep-cargo-cache for incremental Rust .so rebuilds. .venv/bin/python itself works fine for running tests — only pip is broken.

Cargo-only rebuild path: when .venv/bin/pip is broken (ImportError on resolvelib), use 'tools/rebuild-rust.sh --cargo-only' to skip pip entirely — it builds via cargo build --release and copies the .so into angr/. Verified working 2026-05-09 (191st loop session, angr-qrhl.2). The venv pip itself is broken but '.venv/bin/python -m pytest' still works for test runs. As of commit 99901512d (angr-ony8, 205th session), run_single.py and run_regression.py self-heal sys.path so PYTHONPATH=/home/ubuntu/repos/angr is no longer required for benchmark runs.

When writing standalone scripts under tests/benchmarks/ that 'import angr', sys.path[0] is the script's own directory (NOT cwd) when invoked as 'python /path/to/script.py'. Solution: prepend the repo root explicitly: REPO_ROOT = os.path.abspath(os.path.join(HERE, '..', '..', '..', '..')); sys.path.insert(0, REPO_ROOT). angr is not pip-installed in the venv — only the editable repo on '.' resolves it.

When .venv is missing site-packages/z3/include/z3.h, override the cargo z3-sys path: 'Z3_SYS_Z3_HEADER=/usr/include/z3.h cargo build --manifest-path native/angr/Cargo.toml --release'. The system z3 dev headers (apt-installed libz3-dev) work fine. After cargo build, copy target/release/librustylib.so to angr/rustylib.cpython-312-x86_64-linux-gnu.so since 'pip install -e .' is broken on this venv.

Veritesting under Rust manager — failure-mode split between analysis and technique (angr-dv24, 2026-06-03): The angr.analyses.Veritesting Analysis and angr.exploration_techniques.Veritesting technique have DIFFERENT incompatibility patterns under RustExplorationManager. The TECHNIQUE auto-adds EFFICIENT_STATE_MERGING at step_state time (exploration_techniques/veritesting.py:20-21), and EFFICIENT_STATE_MERGING is in _RAISE_OPTION_NAMES — but _check_raise_options only fires at manager init / _add_rust_state, not on state.options.add(). So seeding a state with EFFICIENT_STATE_MERGING already set raises; runtime addition by the technique does NOT raise. The ANALYSIS (analyses/veritesting.py:214,246) does input_state.copy() then mutates the copy inside its own SimulationManager(self.project, ...). The analysis does NOT auto-add EFFICIENT_STATE_MERGING. Its real Rust foot-gun is that RustStateProxy.copy() (rust_state_proxy.py:1426) returns a shallow proxy sharing _state_id — mutations to the copy propagate back to the source Rust state. The analysis runs in pure Python (no RustExplorationManager involvement), so attaching a Rust manager doesn't change anything about the analysis itself; the user has to actively pass a RustStateProxy as input_state to get burned. Documented in docs/advanced-topics/rust_engine.rst as 'Unsupported (v1.0)' with the workaround: pass a SimState (not a proxy), or run on a project without a Rust manager attached. Locked by TestStateProxyCopyIsShallow in tests/engines/test_rust_exploration.py — guard fires if angr-2zwy deep-copy work lands so docs get re-evaluated.

VEX binop() dispatch is now split into 6 per-family helpers in native/angr/src/vex/ops.rs (commit dbb314a32, 2026-05-31): binop_arith, binop_bitwise_shift_cmp, binop_float, binop_vec_int, binop_vec_float, binop_misc. Top-level binop() is a flat dispatch match using |-patterns over IROp variants delegating to one helper. When adding a new binop IROp variant: (1) add it to the top-level pattern in the right family, (2) add the arm to the corresponding helper. The unreachable!() in each helper catches forgotten family routing. binop_misc is also the dispatch fallback returning OpError::NotBinary. The unop() match is NOT yet split this way — symmetric refactor remains as future work.

VEX dispatch-fabricate BYPASS (Perm/Pclmul/Crc32C) closed in angr-s6miz (commit 4489348bb). eval_binop in interpreter/expressions.rs now matches is_dispatch_fabricate_family(op) on the Err arm BEFORE the generic fabricate, routing VPerm/PclmulLQLQ/HQHQ/LQHQ/HQLQ/Crc32C to Python via CbExecutionError::NeedPythonFallback(crate::interpreter::DISPATCH_FABRICATE_REASON) for both concrete+symbolic args. The route only fires on the Err(_) path so it never intercepts a working dispatch. Separately, a vex_bypass_fabricate_count 'sum' field in interpreter/mod.rs define_execution_stats! macro is bumped in the any_sym/arg_is_sym fabricate arm of eval_binop AND eval_unop (NOT the routed-3, which return before it) - surfaces via ExecutionStats::to_hashmap in mgr.get_execution_stats(). It's a strict subset of python_vex_op_fallback_count (excludes the concrete-arg typed-error arm). Test: test_per_category_fallback_counters_exposed asserts ==0 on fresh mgr. Supersedes the 'no counter / inert' framing in vex-dispatch-bypass-inventory.

VEX dispatch-fabricate BYPASS inventory (angr-cudgw.9): exactly THREE op families parse to a concrete IROp variant (opcode_map.rs) but have NO dispatch arm in ops.rs, so VEXOps::binop routes them to binop_misc's 'other => Err(OpError::NotBinary)' catch-all. interpreter/expressions.rs eval_binop then fabricates RustBV::symbolic('unsup_binop_') on symbolic operands (the silent BYPASS, no counter) but propagates the typed OpError -> RustUnsupportedVexOpError on concrete operands (angr-sa3j). The three: Iop_Perm8x{8,16,32}=>IROp::VPerm{elem:I8}; Iop_Pclmul{LQLQ,HQHQ,LQHQ,HQLQ}=>IROp::Pclmul* (iropclass files them Arith but binop's Arith arm omits them); Iop_Crc32C=>IROp::Crc32C (same Arith-classified-but-undispatched). All MUST-FALLBACK (deterministic fns); none fabricate-ok. Audit confirmed NO other concrete IROp lacks a dispatch arm - every remaining variant is dispatched or a sentinel (NeonUnimplemented/Unmapped/Raw). Inert today (no corpus bench drives symbolic path). Documented in docs/extending-angr/rust_vex_ops.rst.

Integration tests for x87 symbolic ops use #![cfg(feature = "vex-engine-z3")] (file-level) since ctx.eval and ctx.assume_true require Z3. Symbolic test pattern: (1) SymContext::new() (NOT new_mock — assume_true needs the Z3-feature variant), (2) RustBV::symbolic(&ctx, name, 64), (3) optionally pre-constrain via ctx.assume_true(x.eq(&bv64(target), &ctx)) to make the test deterministic, (4) call the under-test fn, (5) assert via extract_f64. For unconstrained tests, just assert that the result is concrete and matches libm on the sample chosen by eval. UNSAT propagation tests assert that the fn returns None when ctx.is_sat() is false. Public API access requires pub mod transcendentals in vex/mod.rs which already exists; the test file imports via rustylib::vex::transcendentals::{IOP_, try_}.

After angr-sy4g (2026-05-31, commit 3ca759588) the Rust VEX interpreter lives at native/angr/src/interpreter/ (was interpreter_cb/) and the type is VEXInterpreter (was CallbackInterpreter). Files: mod.rs, execution.rs, expressions.rs, statements.rs, exits.rs, helpers.rs, pending_store.rs, prefetch.rs. Test helper from angr-febn is angr.rustylib.vex_engine.execute_irsb_for_test, which constructs VEXInterpreter via CallbackInterpreter::new... wait the new() is now VEXInterpreter::new. Re-anchors B27-B33 line references for downstream beads (angr-0o7j, angr-xheq, angr-1ezg, angr-qrw2, angr-u7v5).

Doc invariant (2026-06-01): the 'Unsupported op coverage matrix' tables in docs/extending-angr/rust_vex_ops.rst should be refreshed whenever a campaign-child bead closes that flips a row from Placeholder -> Implemented. Source-of-truth columns: 'NEON op families' is sourced from parse_neon_unimplemented (opcode_map.rs) + dispatch arms in ops.rs; 'x87 transcendental ops' is sourced from the angr-i5lj campaign children. Status column has three valid values: Implemented / Placeholder / Stubbed-symbolic (Stubbed-symbolic = fresh-symbolic return per lane, currently only URECPE / URSQRTE).

angr-24pv4.1 symbolic dedup clusters: as of iter19, clusters DONE = 1 (expr_node), 2 (from_parts/make_symbolic), 3 (make_bv_const reuse — all 6 sites use super::bv_codec::make_bv_const), 4 (cmp_bool_for_cached), 5 (z3_binop!), 6 (FloatPrec::z3_sort), 14 (merged Concrete|Constrained arms in to_z3_ast_cached + to_z3_bool_cached, value_z3.rs), 16 (contains_or_insert_ptr private helper sharing seed_and_check_z3_dedup + check_z3_dedup_if_seeded tail, constraint_ops.rs — SCANNED counter stays at call site). All codegen-identical. Remaining: #7 bv_to_z3_float, #8 vex_rm_to_z3+rm_ite4, #9 bsearch_extreme, #10 eval_upto enum loop, #11 u128_to_be_bytes_width, #12 dispatch_assert, #13 forward_to_into! macro, #15 float_to_ieee_bv. Build via make rebuild-cargo (venv pip PEP668-broken).

angr-24pv4.1 (symbolic dedup, 16 clusters) COMPLETE. Final cluster #8 (value_z3.rs FP rm-builders): two module-private cfg(vex-engine-z3) free fns near bv_to_z3_float — (1) vex_rm_to_z3(vex_rm:u8)->RoundingMode collapses the 4-way concrete-rm match copied in build_fp_{round_to_int,arith_rm,f_to_i,f_to_f}_cached; (2) dispatch_symbolic_rm<T:z3::ast::Ast, F:Fn(u8)->T>(rm_bv,cache,build)->T holds the symbolic-rm ITE fanout (r0..r3 then nested rm_low2.eq().ite() chain), generic so it serves both Float and BV (f_to_i) builders. Gotcha: in dispatch_symbolic_rm the .eq (on BV) and .ite (on Bool) are INHERENT in the z3-patched fork, so 'use z3::ast::Ast' is NOT needed there and clippy -D flags it unused; but BV::wrap/Float::wrap DO need Ast in scope, so the per-builder use-lists still import Ast where wrap() is called. The where-clause 'T: z3::ast::Ast' uses the full path, no import. build closures don't capture cache (rm_bv.to_z3_ast_cached(cache) runs inside the helper). All clusters DONE: 1-9,11,12,14-16; #10 already in place; #13 reviewer recommended against.

angr-24pv4.1 cluster 4 (comparison-op dedup, value_z3.rs): new private fn cmp_bool_for_cached(op,operands,cache)->Option centralizes the BVOp->bv*-comparison-method mapping (Eq/Ne/Ult/Ule/Ugt/Uge/Slt/Sle/Sgt/Sge; Ne=eq().not()). Returns None for non-cmp ops. Used by BOTH build_z3_ast_cached (10 arms collapsed to one that wraps result in .ite(&BV(1,1),&BV(0,1))) and to_z3_bool_cached (Expression arm checks it first, falls through to Not/eq-1 fallback). Killed intra-fn ite-wrap dup AND cross-fn mapping dup. Codegen identical, no public API. Committed fbe80c1c9.

vex-ops consolidation: the ops_*.rs files are #[path=...] mod children of ops.rs, each an 'impl VEXOps' block, so Self::helper() resolves across all of them. Visibility rule that bit cluster 1: a helper defined in the PARENT module ops.rs (e.g. sign_extend_low_to_i128) is already callable from every child via Self:: with no visibility change; a helper defined in a CHILD module (e.g. low_bit_mask_u128 in ops_int_arith.rs) is private to that child and must be bumped to pub(super) to be callable from sibling children. Mechanical dedup playbook proven in angr-24pv4.2 iter 6: replace inline low-bit masks ((1u128<<w)-1 and the if w==128{u128::MAX} guarded form) with Self::low_bit_mask_u128(w); replace if signed{x.sign_extend_into}else{x.zero_extend_into} with RustBV::extend_into(w,signed,ctx); replace inline 'if x&sign_bit!=0 {(x|!elem_mask) as i128} else {x as i128}' with Self::sign_extend_low_to_i128(x,w). After removing sign-extension inline blocks, the local sign_bit binding may go dead -> clippy -D warnings catches it, remove only if truly unused (elem_mask usually still used).

value_ops.rs: all symbolic Expression nodes now built via private RustBV::expr_node(width, op, operands: impl Into<Arc<[RustBV]>>) (defined after canonicalize_commutative). Centralizes the EXPRESSION_ID sentinel — do NOT write inline RustBV::Expression { id: Self::EXPRESSION_ID, .. } literals; call expr_node. Arrays of any arity ([x]/[lhs,rhs]/[c,t,e]) coerce via Into<Arc<[_]>>. Landed angr-24pv4.1 cluster 1 (bf89cf6dc), 33 sites collapsed.

vex-ops FP-compare dedup (angr-t5l4x cluster 1, commit a198fddfd): the concrete IEEE-754 truth table and symbolic 1-bit predicate for packed/scalar-lane FP compares now live in two private VEXOps assoc fns in ops_float_cmp.rs: fcmp_truth(ty,kind,l,r)->Result (F32/F64 from_bits + 6-variant FCmpKind match) and fcmp_predicate_1bit(kind,prec,l,r,ctx)->RustBV (Eq/Lt/Le direct, Gt/Ge swapped Lt/Le, Un=isNaN-or). Callers vec_float_scalar_lane_cmp and vec_float_packed_cmp route through them. Distinct from float_cmp_scalar (scalar Iop_FCmp path, only Eq/Lt/Le, done earlier in bb9ebaf67).

value_z3.rs FP-builder Sort selection is now centralized in FloatPrec::z3_sort() (value.rs, cfg(vex-engine-z3), next to bits()). It returns the OWNED z3::Sort wrapper, not the raw Z3_sort handle: every call site must bind 'let sort = prec.z3_sort();' then 'sort.get_z3_sort()' on the next line so the wrapper outlives the raw handle across unsafe Z3 calls. Do NOT collapse to prec.z3_sort().get_z3_sort() (drops the temporary). Adding F16/F128 = single-site change here. Cluster 6 of angr-24pv4.1, commit 6207c32e2.

VEX packed-integer per-lane ops share one driver: VEXOps::vec_int_lane_op in native/angr/src/vex/ops_vec_int_lane.rs, mirroring vec_float_lane_op. Takes args:&[RustBV], elem:IRType, count, op:&dyn IntLaneOp, ctx. IntLaneOp trait (in ops.rs, alongside FloatLaneOp): arity(), concrete_lane(&[u128],elem_width)->u128 (driver re-masks to elem_width, so impls need not mask low bits), symbolic_lane(&[RustBV],elem_width,ctx)->RustBV (must be elem_width wide). Op structs in ops.rs: IAdd/ISub/IMul (impl_int_lane_arith macro: wrapping_/_into), ICmpEq, ICmpGt{signed} (eq/sgt/ugt then sign_extend_into elem_width; concrete returns low_bit_mask_u128 or 0; was ICmpGtS, signed-only, until angr-9ke6b.160), IMinMax{signed,is_max}, IAbs. INT_LANE_OP_MAX_ARITY=2. Replaced vec_binop (ops_vec_binop.rs, deleted), vec_cmp (was ops_vec_compare.rs), vec_int_minmax+vec_int_abs (were ops_vec_int_arith.rs, which keeps vec_polynomial_mul). Tier-B poly_mul/widen/dup stay separate. Cluster 4 of angr-t5l4x, commit e127f0707.

VEX NEON narrow ops share one driver: VEXOps::narrow_lanes in native/angr/src/vex/ops_vec_lane.rs. It takes inputs:&[&RustBV], from_width, to_width, per_input, and two closures (concrete_lane: u128->u128, symbolic_lane: &RustBV->RustBV). Owns the concrete-u128-fast-path vs symbolic-concat split and unary(per_input=count)/binary(per_input=count/2, left=low half, right=high half) layout. vec_narrow_un/bin (truncate: lane&to_mask) live in same file; vec_qnarrow_un/bin (saturate via saturate_lane/saturate_lane_symbolic) live in ops_vec_saturate.rs and call Self::narrow_lanes cross-sibling (pub(super)+descendant-module rule). Cluster 3 of angr-t5l4x, commit 8139ff2e6.

Deduping a family of near-identical scalar binary ops that differ ONLY in the concrete operator: pass fn-pointers, not a kind-matched closure. Proven in angr-24pv4.2 iter 8 for scalar FP arith: float_add/sub/mul/div collapsed to one private float_arith_scalar(left,right,ty,kind:FloatOpKind,op32:fn(f32,f32)->f32,op64:fn(f64,f64)->f64) in ops_float_arith.rs; the F32/F64 bit-cast + InvalidFloatType guard + symbolic build_float_expr(kind,...) fallback live there once, and the four pub(super) entry points become one-line wrappers passing |a,b| a+b etc. (closures capturing nothing coerce to fn pointers). fn-pointer params avoid an unreachable match-arm that a single 'kind' param would force on the concrete path. Did NOT route through vec_float_lane_op count=1 (the audit's suggested architectural approach) — the local helper gives identical dedup at far lower risk. 24pv4.2 CLOSED after 8 clusters; remaining architectural clusters (PACKED fcmp truth-table, lane-0 splice, narrow_lanes driver, IntLaneOp trait) spun into angr-t5l4x.

vex/ops.rs SIMD lane test helpers (angr-ec82) now live in native/angr/src/vex/ops_test_helpers.rs (the inline test mod was first extracted to an ops_tests.rs sibling per angr-l4dx, then ops_tests.rs was split into 14 by-family ops_tests_.rs siblings + shared ops_test_helpers.rs per angr-9hleg; the helpers were hoisted into ops_test_helpers.rs as pub(super) fns). Shared helpers: pack_lanes_f32/f64(&[T])->u128, pack_lanes_uint(&[u128],lane_bits) (masks each value, so pass sign-extended ints as 'x as uN as u128'), lane_mask, unpack_lane(+_f32/f64), assert{f32,f64}_lanes_approx(got,&exp,tol), assert_f32_lanes_bits (exact bit eq for sign/NaN ops like VFAbs), assert_int_lanes_eq(got,&exp_u128,lane_bits). New packed-SIMD lane tests should REUSE these, not re-roll the pack/unpack loop. Keep expected arrays inline at the call site (vacuous-test audit property: never derive exp via tested code). pack_4xf32/pack_2xf64/pack_2xf32_64 delegate to them.

t5l4x cluster 2 DONE (commit 4529cec13): SSE scalar-in-V128 lane-0 splice deduped. New pub(super) fn splice_lane0_u128(orig:u128,lane:u128,lane_bits:u32)->u128 in ops_vec_set_lo.rs = (orig & !mask)|(lane & mask) where mask=Self::low_bit_mask_u128(lane_bits). Replaces 6 inline concrete splices in ops_vec_float_scalar.rs (vec_float_scalar_op/_sqrt/_minmax, F32 pass 32, F64 pass 64) + set_v128_lo's concrete path. The 3 ad-hoc lane-mask literals (set_v128_lo, vec_float_scalar_lane_cmp, vec_float_packed_cmp) now call existing Self::low_bit_mask_u128. packed_cmp kept its early Err guard as an explicit 'if elem_width!=32&&!=64 {return Err}' before the helper. No rename of a public symbol -> no memory sweep was needed despite the task note. clippy -D clean, 77 cargo float + 962 pytest green.

angr-24pv4.1 (symbolic dedup, 16 clusters) progress: clusters 2 (RustBV::from_parts ctor, value.rs) and 3 (reuse bv_codec::make_bv_const for u128->Z3 hi/lo split, 6 sites) DONE in 7256ec883. from_parts(id,name:Arc,width) is pub(super), owns the cfg(vex-engine-z3) BV::new_const ast-rebuild + Symbolic{} construction, routed from symbolic/symbolic_with_id/From. make_bv_const already existed pub(super) in bv_codec.rs; just swapped inline if width<=64{from_u64}else{hi.concat(lo)} blocks. Cluster 1 (biggest, ~33 RustBV::Expression{id:EXPRESSION_ID,..} literals in value_ops.rs -> private expr_node/unary_expr/binary_expr ctors) NOT done — error-prone, do whole or not at all. 13 clusters remain. No rename-sweep needed (all private/pub(super), no public renames).

value_z3.rs build_z3_ast_cached: the 15 plain binary BVOp arms (Add/Sub/Mul/UDiv/SDiv/URem/SRem/And/Or/Xor/Shl/Lshr/Ashr/RotL/RotR) are collapsed via a fn-local macro_rules! z3_binop!($m:ident) that expands operands[0].to_z3_ast_cached(cache).$m(operands[1].to_z3_ast_cached(cache)). signed/unsigned is fully encoded in the bv* method name so the macro is sound. Neg/Not stay inline (unary). Comparison arms use cmp_bool_for_cached (see vex-ops-cmp-bool-dedup-24pv4). cluster 5 of angr-24pv4.1.

rust_vex_ops.rst parse_opcode chain has 10 sub-routers (not 9 as docs claimed pre-angr-1cnv): parse_arithmetic, parse_bitwise, parse_shift, parse_comparison, parse_conversion, parse_float, parse_vector, parse_vreverse, parse_special, parse_neon_unimplemented. parse_vreverse was added between parse_vector and parse_special for the NEON reverse family (angr-tukg.4) and is easy to miss when teaching the pipeline. When a new sub-router is added the rust_vex_ops 'Pipeline overview' file table AND the parse_* code block in the 'parse_* family pattern' section both need a row added — they drift independently.

VEX NEON Iop_QNarrow* opcodes have a 4-tuple naming convention: Iop_QNarrow{Bin|Un}{srcW}{srcSign}to{dstW}{dstSign}x{count}. Bin = pair of input vectors interleaved, Un = single input. 'src_signed' flag determines how the source lane is interpreted (sgt/slt vs ugt/ult); 'dst_signed' determines the saturation range (signed: [-2^(w-1), 2^(w-1)-1], unsigned: [0, 2^w-1]). The S-to-U variants (e.g. Iop_QNarrowUn16Sto8Ux8) are the most subtle — a negative source clamps to 0. For VEX symbolic clamps, build constants in source width so comparisons match widths, then truncate after the ITE. See vex_qnarrow_un and saturate_lane_symbolic in native/angr/src/vex/ops.rs for the reference implementation (commit 7630b1d66, angr-hzs0).

ops.rs by-family split (angr-cudgw.18) — when a family is driven by codegen macros (define_float_to_float/define_int_to_float/define_float_to_int_signed/define_float_to_int_unsigned) that are invoked ONLY by that family, move the macro_rules! defs INTO the child module alongside the invocations and change the emitted methods to 'pub(super) fn' so the generated stubs (f32_to_f64, i32s_to_f32, f32_to_i32s, *_rm variants, etc.) stay callable from the unop/binop dispatch in ops. macro_rules in a child file are textually in scope for invocations later in the same file — no #[macro_export] needed. Helpers called only within the cluster (int_to_float/float_to_int/float_to_float/round_ties_to_even_f32/f64/apply_rounding_f32/f64/float_to_int_rm/float_to_float_rm) stay private fn. Tests call via the public VEXOps::unop/binop API so ops_tests needs no change. iter23: conversions -> ops_conversions.rs (commit c72a1c1b6), ops.rs 4574->4213.

Splitting the VEXOps god-file (vex/ops.rs): extract a family into a SIBLING file but declare it as a CHILD module inside ops.rs via '#[path = "ops_int_arith.rs"] mod int_arith;'. This keeps the moved impl block a descendant of module ops, so: (1) methods the binop/unop dispatch still calls must be 'pub(super)' (parent-visible); (2) shared helpers/free-fns that STAY in ops.rs and are called from the moved code (e.g. Self::sign_extend_low_to_i128, the private free fns build_float_expr/float_prec_of) remain visible to the child by the descendant rule with NO visibility bump - import them with 'use super::{build_float_expr, float_prec_of}'; (3) helpers only called within the moved group stay private. Use explicit 'use super::{...}; use crate::symbolic::{...}; use crate::vex::ir::IRType;' rather than 'use super::' to dodge wildcard_imports lint; cargo fmt reorders the super import list alphabetically. ops_tests.rs (also a child of ops via #[path]) keeps reaching everything via 'use super::'. Extractions: iter21 int widening-mul/divmod -> ops_int_arith.rs; iter22 scalar float arith (float_neg/abs/sqrt/add/sub/mul/div/madd/msub) -> ops_float_arith.rs (ops.rs 4774->4574). KEEP in ops.rs (shared by vector/RM paths): concat_le_elements, sign_extend_low_to_u64/i128, FloatLaneOp trait + FAdd/FSub/FMul/FDiv/FSqrt/FAbs/FMin/FMax structs + impl_float_lane_* macros + float_minmax_symbolic. Next candidate families: vector lane ops (biggest, depends on concat_le_elements), conversions (int_to_float/float_to_int/float_to_float/round_), float_cmp_ + float_com_cc.

ORPHANED-IMPORT GOTCHA (from vexops-split-orphaned-import): when a moved family was the ONLY user of an enum/type imported in ops.rs (e.g. FCmpKind from super::ir), clippy's unused-imports flags it after the move, but ops_tests.rs still reaches the symbol transitively via 'use super::*', so deleting the ops.rs import breaks the test compile. Fix: delete it from ops.rs AND add an explicit 'use crate::vex::ir::FCmpKind;' to ops_tests.rs. Seen iter25 extracting float compares (float_cmp_eq/lt/le, vec_float_scalar_lane_cmp, vec_float_packed_cmp, float_com_cc) -> ops_float_cmp.rs (commit 9ccab957f, ops.rs 4213->3873).

MACRO-DRIVEN FAMILIES (from vexops-conversions-macro-split): when a family is driven by codegen macros (define_float_to_float/define_int_to_float/define_float_to_int_signed/define_float_to_int_unsigned) invoked ONLY by that family, move the macro_rules! defs INTO the child module alongside the invocations and change the emitted methods to 'pub(super) fn' so the generated stubs (f32_to_f64, i32s_to_f32, f32_to_i32s, *_rm variants, etc.) stay callable from the unop/binop dispatch. macro_rules in a child file are textually in scope for invocations later in the same file - no #[macro_export] needed. Helpers called only within the cluster stay private fn; tests call via the public VEXOps::unop/binop API so ops_tests needs no change. iter23: conversions -> ops_conversions.rs (commit c72a1c1b6, ops.rs 4574->4213).

VEXOps god-file split (vex/ops.rs) — when a moved family was the ONLY user of an enum/type imported in ops.rs (e.g. FCmpKind from super::ir), clippy's unused-imports flags it after the move. But ops_tests.rs reaches that symbol transitively via 'use super::*', so deleting the ops import breaks the test compile. Fix: delete it from ops.rs AND add an explicit 'use crate::vex::ir::FCmpKind;' to ops_tests.rs. Seen iter25 extracting float compares (float_cmp_eq/lt/le, vec_float_scalar_lane_cmp, vec_float_packed_cmp, float_com_cc) -> ops_float_cmp.rs (commit 9ccab957f, ops.rs 4213->3873). See vexops-god-file-split-pattern.

Iop_PwAdd32Fx2 (NEON pairwise FP add) is implemented as IROp::VFPwAdd{elem,count}, routed via parse_float in opcode_map.rs (NOT parse_neon_unimplemented — parse_float runs first in parse_opcode). Execution: VEXOps::vec_float_pairwise_add reuses the single-lane vec_float_lane_op(&[a,b],elem,1,&FAdd) per pair so concrete+symbolic match packed VFAdd. Output interleave matches integer VPwAdd: [a0+a1, b0+b1], total 64 bits -> Ity_I64. This was the LAST NeonUnimplemented scaffold op; parse_neon_unimplemented now always returns None (kept as scaffold for next NEON op, with historical coverage NOTEs in a block comment). Python tests test_misc.py _NEON_UNIMPLEMENTED is now empty; the two unsupported-op probes that used PwAdd32Fx2 were repointed to Iop_QShlNsatSU8x8 (still Unmapped). To add the next NEON-unimplemented op: re-add a match arm in parse_neon_unimplemented returning Some(IROp::NeonUnimplemented(name)) and list it in _NEON_UNIMPLEMENTED.

view

VPolynomialMul GF(2) carry-less multiply pattern (angr-tukg.6): IROp::VPolynomialMul { count, widen } single variant covers all three libVEX opcodes — Iop_PolynomialMul8x{8,16} (widen=false, 8-bit lanes out) and Iop_PolynomialMull8x8 (widen=true, 16-bit lanes out). Result type: widen=false preserves total (8count); widen=true doubles per-lane to 16 so 8x8 → V128 and 8x16 → V256. Only I8 input lanes — libVEX doesn't emit wider polynomial muls. Parse routing uses an explicit match (3 opcodes, mixed widen field). Binop dispatch → Self::vec_polynomial_mul(left, right, count, widen, ctx). Per-lane algorithm: XOR of (b << bit) where bit-th bit of a is set, over bits 0..7. Implementation builds in 16-bit accumulator (max shift is 7, so all addends fit); non-widening truncates to 8 bits after. Symbolic uses literal bit_a.eq(1).ite(b_wide.shl(bit), zero) folded into XOR. Claripy has NO _op_generic_Polynomial — universality tests use z3-spec-replay-test-template against the same XOR-shift inline reference. ARM ref: PMUL/PMULL DDI 0487 C7.2.281. Tests at native/angr/src/vex/ops.rs::tests::test_vpolynomial_mul_*.

VPwAdd/VPwAddL/VPwMin/VPwMax pattern (angr-tukg.2): four IROp variants in vex/ir.rs. VPwAdd { elem, count } binary; VPwAddL { elem, count, signed } unary widening; VPwMin/VPwMax { elem, count, signed } binary. parse_vector arms: VPwAdd uses vec_arms!, others use vec_signed_arms!. Iop_PwAdd32Fx2 stays NeonUnimplemented (FP). Dispatch: VPwAddL in unop, VPwAdd/VPwMin/VPwMax in binop. PwOp enum (Add/MinS/MinU/MaxS/MaxU) + pw_combine helper near VecShiftKind. vec_pairwise_binop builds count/2 pairs from a then count/2 from b — output[0..count/2] from a-pairs, output[count/2..count] from b-pairs. vec_pairwise_add_long sign/zero-extend per lane to 2elem then add. Tests follow z3-spec-replay-test-template (claripy has no _op_generic_Pw).

VQAdd/VQSub pattern (angr-tukg.1): IROp::VQAdd{elem, count, signed} / VQSub variants in vex/ir.rs. Parser uses vec_signed_arms! in parse_vector for {N}{S/U}x{M} suffix. Dispatch in VEXOps::binop -> Self::vec_int_saturating(left, right, elem, count, signed, is_sub, ctx). Concrete fast path: sign-extend lanes to i128, compute raw, clamp into [-2^(N-1), 2^(N-1)-1] (signed) or [0, 2^N-1] (unsigned). Symbolic path mirrors claripy _op_generic_QAdd at irop.py:879 — sign-bit overflow flag (signed: '(top_a XOR top_b) [XOR-inverted-for-add] & (top_a XOR top_r)') + cap = ITE(top_r==1, INT_MAX, INT_MIN); unsigned uses ult/ugt comparisons with resa as the overflow condition, cap = UINT_MAX or 0. Tests use the same Z3 universality push/pop pattern as VReverse.

VQShlSat (angr-tukg.8) pattern for NEON saturating left shift by vector (Iop_QShl/QSal): single IROp::VQShlSat { elem, count, signed } variant. Signedness encoded in the prefix (Shl=unsigned, Sal=signed), NOT in a S/U infix in the suffix — vec_signed_arms! doesn't fit; route Iop_QShl and Iop_QSal via two separate strip_prefix matches in parse_vector. Dispatch in VEXOps::binop -> Self::vec_qshl_sat(left, right, elem, count, signed, ctx). Concrete fast path: per-lane sign-extend amt; if amt>=0 do left shift with overflow detected by (raw > umax) [unsigned] or (raw outside [smin,smax]) [signed via i128 arithmetic]; if amt<0 do right shift (lshr/ashr) by -amt with OOR collapse to 0/sign-fill. Symbolic path: per-lane shl_v=shl(a,amt); round-trip check no_overflow = (lshr|ashr)(shl_v, amt) == a; cap for signed is ITE(a_is_neg, smin, smax) keyed on sign of operand. Branch on sign of amt via top-bit extract + .ite(right_branch, left_branch). 521/521 pytest pass; no claripy reference exists for QShl/QSal so universality test is spec-replay, not Python parity.

VReverse implementation pattern (angr-tukg.4): Iop_Reverse{sub_width}sIn{elem.bits()}_x{count} reverses the order of sub_width-bit sub-units within each elem-wide lane. Works for sub_width in {1,8,16,32}. Encoded as IROp::VReverse { sub_width: u8, elem: IRType, count: u8 } in vex/ir.rs. Parser parse_vreverse in vex/opcode_map.rs (separate fn — naming pattern Reverse{N}sIn{M}_x{K} doesn't fit the vec_arms! macro's {N}x{M} suffix shape). Dispatch in VEXOps::unop → Self::vec_reverse. Concrete path: per-lane integer mask+shift loop. Symbolic path: extract each sub-unit, push into Vec in LSB→MSB order (index 0 → LSB), call concat_le_elements. For sub_width=1, sub-units are single bits so no recursive reversal needed.

VEX shift-by-vector vs shift-by-immediate parser collision avoidance: Iop_Shl{N}x{M} (vector by vector, 2 full-width operands) is parsed in parse_vector AFTER parse_shift falls through. parse_shift has Iop_Shl prefix matched against suffixes ['8','16','32','64'] (scalar Shl) so 'Iop_Shl8x8' strips to '8x8' which doesn't match any scalar arm — falls through cleanly. Iop_ShlN{N}x{M} (vector by I8 immediate) is in parse_shift via vec_arms! 'Iop_ShlN' which can never match 'Iop_Shl8x8' (different prefix). So adding vec_arms!('Iop_Shl') in parse_vector doesn't collide with the existing scalar/by-immediate handlers.

VShl/VShr/VSar (angr-tukg.7) pattern: 3 IROp variants {elem, count} in vex/ir.rs, total=64→I64 / 128→V128 result type. Parser uses vec_arms! in parse_vector for {N}x{M} suffix; Iop_Sal{N}x{M} aliases to VShl (bit-equivalent on left shift). Dispatch in VEXOps::binop → Self::vec_shift_vec(left, right, elem, count, VecShiftKind, ctx). Concrete fast path: per-lane u128 mask + shift, OOR (count≥elem_width) returns 0 (shl/lshr) or sign-fill (sar) matching Z3 bvshl/bvlshr/bvashr. Symbolic path: extract both operands per-lane and dispatch shl_into/lshr_into/ashr_into. Reused Z3 universality parity pattern (push/add_constraint(got._eq(py).not())/pop) against inline claripy reference for Iop_Shl/Sar (operation_map['Shl']='lshift' etc → _op_vector_mapped → per-lane Extract + bvshl). Note: Iop_Sal and Iop_QShl/QSal have NO claripy reference (no _op_generic_Sal / _op_generic_QShl exist); semantics inferred from VEX naming conventions.

vt0t-2 categorization stats (rust_state_sync + rust_state_export, 101 except blocks total): cat-(a) EXPECTED CONTROL FLOW = 21 blocks (21%); cat-(b) FALLBACK WITH LOSS = 56 blocks (55%); cat-(c) WRONG-ANSWER RISK = 25 blocks (25%). 9 new (c) blocks promoted from silent/debug to WARN: per-state/outer export_stash convert, per-chunk/full-page concrete memory write, get_state_symbolic_z3_asts outer, _replace_with_rust_snapshot, found_states convert, get_state_by_id, _load_snapshot_pages per-page. The (c) skew is much higher than vt0t-3 (4%) because state-bridge files are core correctness path — many silent fallbacks here mean Python sees stale data. Some (c) sites stay debug-only (e.g. _concretize_stack_registers SP) because higher-level callers already warn-log the user-visible divergence; rationale comments tie them to the visible warn site. Tests: 357/357 pass.

vt0t-3 categorization stats (rust_techniques + rust_state_proxy + rust_state_cache + rust_identity, 46 except blocks total): cat-(a) EXPECTED CONTROL FLOW = 13 blocks (28%); cat-(b) FALLBACK WITH LOSS = 31 blocks (67%); cat-(c) WRONG-ANSWER RISK = 2 blocks (4%). The strong (b) skew suggests these files mostly handle FFI/state-lifecycle errors gracefully, with only 2 places where silent fallback could mislead callers. None warrant re-raise; both (c) are now logged at warn.

Warm-cache init path optimizations (angr-87ya): 3 class-level caches added to RustExplorationManager: (1) _disk_key_cache: Dict[str,str] for MD5 binary hashes, (2) _blank_state_cache: Dict[tuple, SimState] for blank_state(addr) results, (3) _precomputed_regs passed from _load_init_from_disk_cache to _sync_registers_to_rust via self._precomputed_regs field (consumed once). All caches are class-level (survive across instances) with size limits.

Parallel wave loses the non-taken side of a SYMBOLIC BRANCH because the guard RustBV is never serialized across the thread::scope join. Mechanism (angr-lq9rz, fix filed angr-ype54): a worker parks a BounceKind::SymbolicBranch terminal; terminal_states are fully serialized across the join but the guard lives in the worker's OWN Z3 context and is never serialized (scheduler.rs module doc). The coordinator's process_parallel_bounce_queue (exploration/run_loop.rs) rebuilds PendingBounce with stored_conditions: FxHashMap::default() (EMPTY), so Python's _handle_symbolic_branch_callback_inner -> _rust_mgr.get_pending_branch_condition (pending_api.rs::_get_pending_branch_condition) raises 'condition N not found in stored_conditions' and degrades to an unconstrained resume_after_symbolic_branch(None,None) that loses the feasible path. Proven on fauxware find=0x4006ED num_find=2 with phase2 disabled: workers=1 phase1 finds BOTH accepting paths, workers=2 phase1 finds only the backdoor. NOT Bug M1 (num_find never reached, so no CancelToken frontier-drop). Masked in practice: the angr-027h phase-2 eager retry recovers the 2nd path, so mgr.explore()/test_parallel_wave pass; only raw _rust_mgr.run() exposes it. The 'condition N not found in stored_conditions' noise and the path-loss are the SAME root cause. See invariant-active-empty-not-partial-found for the sibling wave-completeness invariant.

AST-passthrough wheel smoke test lives at tests/smoke/wheel_ast_passthrough.py (fn check_ast_passthrough + test_wheel_ast_passthrough). It mints a claripy BVS, hands the Z3 AST across FFI via RustSolverContext.add_constraint_ast, and reads it back with satisfiable/min/max/eval plus an UNSAT contradiction. A correct round-trip proves claripy and the Rust engine share ONE libz3.so (the point of wheels.yml --exclude libz3.so + $ORIGIN/../z3/lib RUNPATH). Wired into wheels.yml CIBW_TEST_COMMAND as 'python {project}/tests/smoke/wheel_ast_passthrough.py'. Needs _setup_shared_z3_context() before RustSolverContext, same as tests/engines/rust/test_solver_ops.py setup_class. In-container CI execution still gated by angr-3gjm (no Docker/network in dev sandbox).

wheels.yml (angr-3gjm/ivwn) static-audited clean iter 48: CIBW stages + --exclude libz3.so + patchelf RUNPATH $ORIGIN/../z3/lib + abi3 cp310 single-wheel all match docs/advanced-topics/rust_wheel_distribution.rst. Smoke test tests/smoke/wheel_ast_passthrough.py (check_ast_passthrough) runs GREEN locally vs editable build (shared-libz3 round-trip: min10/max20/eval17, x==18 UNSAT). NOTE: running it as a bare script from repo root fails ModuleNotFoundError angr — direct-script puts tests/smoke on sys.path[0] not cwd; run with PYTHONPATH=repo-root or via pytest. In CIBW it works because the wheel is installed. Only Docker-gated manylinux build+auditwheel+readelf RUNPATH check remains; bead correctly stays open.

Wheel distribution for the Rust engine (angr-ivwn): a prebuilt manylinux wheel MUST NOT bundle libz3.so. The Rust cdylib (NEEDED libz3.so, SONAME unversioned) and claripy must load the SAME libz3.so for AST passthrough — Z3 Ast pointers are only valid in their own Z3_context. auditwheel's default (vendor every non-system lib into angr.libs/) would give the extension a private second Z3 context and silently break passthrough. Correct recipe: auditwheel repair --exclude libz3.so, then patchelf --set-rpath '$ORIGIN/../z3/lib' on rustylib*.so (rustylib lives at site-packages/angr/, z3-solver's libz3 at site-packages/z3/lib/). z3-solver==4.13.0.0 stays a runtime dep (transitive via claripy 9.2.209) — the unversioned SONAME means the linker can't catch an ABI break, so the pin is the only guard (see avoid-pip-install-deps). pyo3 0.27.2 currently has no abi3 feature => version-specific .so; abi3-py310 would collapse the matrix if it compiles with py-clone+full pymethods. Design memo: docs/advanced-topics/rust_wheel_distribution.rst; prototype .github/workflows/wheels.yml (UNVERIFIED, no Docker in sandbox); blockers angr-3gjm/6f0i/9eit.

wheels.yml z3-header gap FIXED in commit e7c1d9789 (iter21, angr-3gjm). CIBW_BEFORE_BUILD_LINUX now: pip install z3-solver==4.13.0.0 patchelf && (yum install -y epel-release || true) && yum install -y z3-devel && test -f $Z3_SYS_Z3_HEADER guard. Z3_SYS_Z3_HEADER=/usr/include/z3.h pinned in CIBW_ENVIRONMENT_LINUX. The failure-masking '|| pip download z3-solver' is GONE. Remaining unverified gaps are Docker-only (manylinux build + auditwheel --exclude libz3 repair + patchelf RUNPATH + clean-venv install + AST-passthrough smoke). Bead angr-3gjm stays OPEN pending a CI run.

Windows is the ONE wheel leg with no header/import-library source: the z3-solver win_amd64 wheel ships z3.dll and nothing else -- no z3.h (so z3-sys bindgen dies) and no import library (so link.exe has nothing to link). CIBW_BEFORE_BUILD_WINDOWS therefore fetches the MATCHING official z3 4.13.0 release archive purely for its include/ and libz3.lib (build-time only; the DLL loaded at runtime is still the user's z3-solver copy, found via os.add_dll_directory). The version must match what claripy pins (4.13.0.0) or the exports drift. Predicted first-failure point when the leg actually runs in CI: z3-sys asks the linker for 'z3' (i.e. z3.lib) while the archive names it libz3.lib -- hence the 'copy libz3.lib z3.lib' step. Second candidate: LIBCLANG_PATH for bindgen. Neither is verified; there is no Windows runner or network in the dev sandbox (see angr-3gjm).

RustMemoryProxy.store symbolic-addr fallback (rust_state_proxy.py, RustMemoryProxy.store) must re-issue the concretized write through set_state_memory_ast (state_id, conc_int, data_ast), NOT state_memory_store_symbolic_multi with a concrete BVV. Reason: for a concrete addr, memory_store_symbolic_multi short-circuits to store_concrete_automap (memory/store.rs), which is MISNAMED — it does NOT auto-map, it check_pages_mapped_lazy-errors on any unmapped page. set_state_memory_ast funnels through RustSimState::memory_store -> store_concrete_automap_internal, which DOES auto_map_zero_page lazy pages. So an ebp-relative blank_state stack slot (inside the lazy stack region but never mmap'd) lands via set_state_memory_ast but was silently dropped by the multi path. Genuinely non-lazy garbage pages (operator-new 0x7fff.. outside any lazy region) still Err from store_concrete_automap_internal -> swallow with contextlib.suppress to keep the SimProc state alive (p1s02 semantics). Commit 50c3dbaa9 (angr-wi50c).

wi5m bimodal-bench counter soak (2026-05-22 iter 6): ran google2016_unbreakable_1, securityfest_fairlight, ekopartyctf2016_sokohashv2 via run_single.py --counters-json. All 5 legacy constraint-sync counters (cb_sync_calls, cb_sync_constraints, cb_sync_failures, rust_ctx_missing, pending_ast_sync_calls) stay at 0. Combined with 14 fast-tier + 3 quick (z2nt session) = 20-bench soak with no callback hits. desc-string reconstruction parsers in _cb_sync_constraints removed in commit af7c9bb90 — handle_id Path A still wired but itself dead; follow-up angr-h0dv drops the entire callback chain.

INVARIANT: Wide symbolic loads (>64 bit) use Iend_BE + claripy.Reverse() to preserve BVS identity. Iend_LE wraps in Reverse(), breaking FFI identity. v2 commit bb1a908dc.

Wide-symbolic partial-load extract path (memory.rs ~line 552-554 and the symbolic_spans path ~line 568) is hardcoded BE: hi = total_bits - 1, lo = total_bits - size*8 (and analogues for offset>0). For BE memory this is correct; for LE memory, partial reads of a wide symbolic_object stored at addr will return the MSB-side byte where the LSB-side byte is expected. Full-width loads round-trip correctly because the exact-match branch returns the symbolic object as-is. The bug was masked because the existing partial-overlap test (angr-wyxb) only checks evaluability, not byte values.

wider_load_cache (memory/load.rs:744) uses per-byte fingerprint comparison (ByteFingerprint::Multi { version, default_byte }) recomputed on every load. Version bumps via bump_multi_version ARE correctly detected — fingerprint mismatch -> rebuild. The cache key (addr, size) does not need a version tag. Confirmed against bd-1tes false premise (closed 8649ab3c7). Test: test_phase4_wider_load_cache_invalidated_on_multi_install already proves the mechanism. Real correctness gaps live UPSTREAM of the cache (orphaned multi_objects on concrete writes, fixed in 8649ab3c7).

rust_manager.py disk-cache decomposition (angr-wqao) is split across wqao.1 (SAVE) and wqao.2 (LOAD), both landed in ONE shared mixin angr/exploration/rust_disk_cache.py (RustDiskCacheManager). wqao.1 moved SAVE: _disk_cache_dir, _disk_cache_key + _disk_key_cache memo, _save_init_to_disk_cache, 6 module-level extract* snapshot helpers + _RUST_CACHE_VERSION/_PYTHON_METADATA_VERSION. wqao.2 (commit 2e17cdda4) moved LOAD: _load_init_from_disk_cache, _load_init_pickle, _deserialize_init_state, _apply_init_side_effects, and the _state_has_user_symbolic load-guard. KEY: _get_cached_blank_state STAYS in rust_manager.py because it owns the host-class _blank_state_cache pool; the mixin reaches it via self through the MRO. The mixin needs claripy + PAGE_MASK imports; rust_manager.py dropped now-dead pickle/PAGE_SIZE/PAGE_MASK imports. Disk-cache subsystem now fully isolated. Mixin pattern keeps all call sites self._x() unchanged - zero behavior change, no Rust rebuild. Next: wqao.4 (sequence init pipeline into explicit phases) was blocked by wqao.2, now unblocked.

rust_manager.py init is sequenced into 4 phase methods (angr-wqao.4, commit 9d1cf392a): _phase_boot (Z3/deterministic setup, RustExplorationManager ctor, os name, solver_timeout, max_active/max_history, exploration_strategy), phase_config (all kwarg-or-env gate flags use_callback*/use_export/use_simproc_fork, perf counters/caches, _setup_callbacks/_load_binary_regions/_register_simprocedures, inspect registry), _phase_link_state (multi-stage-reuse short-circuit; RETURNS True to stop init when old Rust mgr reused, False otherwise), _phase_activate (add initial states). init is now a thin orchestrator: boot; config; if link_state(): return; activate. KEY invariant: _init_start was the ONLY cross-phase local -> promoted to self.init_start so link_state/activate can stamp the 'total' timer. The description's 'step_N -> phase' rename was moot (no _step_N helpers existed). Acceptance dropped the under-1000-lines target. Pure code-motion, zero behavior change, no Rust rebuild.

angr-x6ol audit (2026-06-03): vex/ops.rs has 23 panic! sites — ALL inside #[cfg(test)] mod tests (after line 4867 boundary). They are 'panic!("expected X, got {:?}", other)' match-arm test-failure messages, idiomatic Rust test patterns. The runtime (non-test) portion of vex/ops.rs lines 1-4864 has ZERO panic!/unimplemented!/todo! sites. Conclusion: task premise was a false positive from grep-only counting; closed as no-action. For future panic-audit tasks, always exclude #[cfg(test)] modules first.

x86-32 promoted Experimental → Supported in docs/advanced-topics/rust_engine.rst (angr-duta.1, 2026-05-17). The doc's prior 'x86 (32-bit) | 1 (flareon2015_2) | Experimental' row was severely outdated. Reality: 8 x86-32 benches passing in regression (3 FAST + 5 MEDIUM). FAST: flareon2015_2 1.11x, csgames2018 1.64x, whitehatvn2015_re400 2.56x. MEDIUM: sym-write 2.29x, flareon2015_5 10.27x, flareon2015_10 1.36x, mma_howtouse 0.65x, ekopartyctf2016_sokohashv2 0.36x. Per the doc's own Supported criterion (>=1 benchmark in baseline_timings.json staying green), x86-32 was over-qualified.

Cdecl is still the only Rust-side CC in calling_conventions.rs. Windows i386 benches work because the CC boundary is Python-side: entry_state() and Callable place args via angr's Python SimCC (SimCCStdcall32 for SimWindows), and the Rust engine just executes the state. No bench triggers a Rust-native SimProcedure from a stdcall caller.

Follow-up filed as angr-duta.5 (deferred 2026-08-01, no current consumer). Adding stdcall/fastcall requires (1) CallingConvention impl + (2) callee_arg_cleanup_bytes() on the native dispatcher (current dispatcher only handles caller-cleans cdecl/SystemV).

x86 (32-bit) e2e test pattern using cle Blob backend: test_x86_explore_blob in tests/engines/rust/test_multiarch.py (formerly in the monolithic tests/engines/test_rust_exploration.py before the angr-yg2m split) ships 25 bytes of i386 code via blob_path.write_bytes(code), then angr.Project(str(blob_path), main_opts={'backend': 'blob', 'arch': 'x86', 'base_addr': 0x400000}, auto_load_libs=False). Asserts proj.arch.name == 'X86' and proj.arch.bits == 32. Same pattern as test_armeb_explore_blob (ARMEB) and test_aarch64_explore_blob — gives full e2e coverage of VEX interpretation, register sync, branch resolution, and solver eval without needing a cross-compiler or pre-built binary. The 2*x+16==100 → x==42 program is the canonical micro-test across all three blob tests for cross-arch parity comparison.

x86 segment-base dispatch status (angr-5spy.2, 2026-06-01): All 4 segment-base slots — fs_const (320, 4B), gs_const (324, 4B), ldt (304, 8B), gdt (312, 8B) — are wired in arch/x86.rs ALIASES. ldt/gdt match archinfo exactly; fs_const/gs_const remain Rust-only PLACEHOLDERS because archinfo does NOT define fs_const/gs_const for x86 (verified: state.regs.fs_const raises AttributeError on x86, but state.regs.ldt/gdt return 64-bit zero). The placeholder offsets 320/324 collide with archinfo's emnote/cmstart at the same offsets — no current callers read those by name so the collision is benign. Coverage: Rust unit test arch::x86::tests::test_segment_base_aliases + Python integration test TestMultiArchSupport::test_x86_segment_bases_dispatch. The #[allow(dead_code)] is now removed from the offsets module — every constant it declares is referenced. Real fs_const/gs_const lives on amd64 (208/1032 per archinfo) and is wired through arch_prctl syscall (syscalls/arch_prctl.rs).

x86 segment-selector dispatch status (angr-5spy.1, 2026-06-01): All 6 16-bit selectors (CS/DS/ES/FS/GS/SS) are wired in arch/x86.rs ALIASES (lines 126-131) with offsets 288/290/292/294/296/298. They are NOT in CANONICAL (so register_name(offset) does not return them), but register_offset(name)/register_size(name) do via the ALIASES fallback. Test coverage in tests/engines/test_rust_exploration.py::TestMultiArchSupport::test_x86_segment_selectors_dispatch. LDT/GDT (offsets 304/312) are still NOT in ALIASES — that wiring is the .2 subtask (segment bases + LDT/GDT placeholders). FS_CONST/GS_CONST (offsets 320/324) are already in ALIASES.

Rust ccall handler for x86g_use_seg_selector (native/angr/src/vex/ccall.rs::handle_ccall_with_ctx) implements concrete fast path only: when args [ldt, gdt, seg_selector, virtual_addr] are all concrete and the descriptor table selected by tiBit (bit 2 of seg_selector) is zero, returns flat addressing ((seg_selector & 0xFFFF) << 16) + (virtual_addr & 0xFFFFFFFF) at ret_bits=64. Bad selectors (high bits set) return 1<<32 (the libVEX bad() value). Symbolic args or non-empty descriptor tables fall through to Python (still triggers the multi-successor drop bug — track separately). Needed because sym-write hits this CCall at 0x804847c (mov %gs:0x14 canary read) and would otherwise spin on the multi-successor drop fallback path. Commit aaaa25779.

x87 transcendentals concretize-and-pin pattern (angr-i5lj.1 + angr-i5lj.2 closed 2026-06-01): try_concretize_{binop,triop}rm in native/angr/src/vex/transcendentals.rs handles symbolic operands for x87 ops via opcode-filter matches!. CURRENT COVERAGE: binop = Iop{Sin,Cos,Tan,2xm1}F64; triop = Iop_{Atan,Yl2x,Yl2xp1,Scale}F64. Out-of-scope: Iop_RecpExp* (closed-form), Iop_PRemF64 (FP remainder, no benchmark driver), Iop_FxamF64 (NOT A VEX IROP — was in bd description but doesn't exist in pyvex/libvex). Pattern: (1) early-return None if opcode out of scope, (2) defer to try_concrete_rm if all operands are concrete, (3) ctx.eval(input) -> u64 -> f64 sample, (4) compute libm op on sample via inner match opcode, (5) pin EACH symbolic input via ctx.assume_true(input.eq(&concrete(sample), ctx)) for path consistency, (6) return RustBV::concrete(result_bits, 64). Lose symbolic precision but path stays consistent. Wired in ops.rs::binop_misc IROp::Raw arm (binop) and ops.rs::binop_with_rm IROp::Raw arm (triop) AFTER existing try_concrete*_rm. To extend further: add opcode constants + matches! arm + libm match arm. The strategy choice (option 1) lives in module rustdoc.

x87 transcendentals have two-path status in the Rust engine: (1) FFI lifter path with numeric IROp::Raw(opcode) — concrete-only libm fast path in native/angr/src/vex/transcendentals.rs plus symbolic concretization fallback (sample-pin-replace input strategy from angr-i5lj). (2) JSON string opcode path — falls through parse_opcode and surfaces as IROp::Unmapped(name) -> RustUnsupportedVexOpError. The asymmetry is intentional: the JSON path can't carry the numeric opcode that drives the libm dispatch. Implication for tests: a test using execute_irsb_for_test's JSON-based IRSB construction cannot exercise the libm fast path; you must go through the FFI lifter to hit it. Documented in rust_vex_ops.rst:'x87 transcendental ops' (commit 83cff296e, angr-l0lm).

angr-xel4 spike result (2026-06-06, deep_loop_search characterization): DFS dominates BFS for deep-input-loop binaries (grub-class). On synthetic proxy with N=14 iteration cap, 300 step budget: BFS depth=11 with 191 active states (976MB RSS); DFS depth=32 with 31 active states (645MB RSS). BFS depth PLATEAUS at 9-12 regardless of step budget or N — the wide low-depth frontier consumes the budget. DFS reaches the iteration cap before exhausting steps. Implication for angr-smxp: default to DFS for binaries with input-loop bound >=10. Harness at tests/benchmarks/characterization/deep_loop_search/. Prioritized-search comparison not done — needs Rust manager hook that doesn't exist yet.

angr-xfvf push/pop spike conclusion (iter 20, 2026-06-03): the spike's proposed mechanism — wrap assume_true/assume_false with push() at branch entry and pop() at branch exit — is structurally broken and cannot help bimodal benches. Three independent reasons:

1. Semantics mismatch. assume_true/assume_false at the call sites (interpreter/exits.rs branch constraints, interpreter/statements.rs CAS/conditional stores, exits via solver.rs eval) add PERMANENT constraints to the current SymContext's solver. They define the state, they are not probes. Wrapping with push()/pop() either (a) loses the path constraint after pop (wrong semantics — the forked child would no longer see the branch it took), or (b) is equivalent to plain assert if you never pop (zero gain).

2. The proposed mechanism IS Option C of the angr-hk7k design tree (memory invariant-hk7k-design-options). Option C ('push/pop at lineage boundary only') was explicitly considered and rejected: degenerates at 3+ level forks. Option A (shared-lineage Z3 solver with scope-path tracking) was the recommended path and is implemented in native/angr/src/symbolic/lineage.rs::SharedLineageSolver, with runtime thrash-detection (angr-v5ht, commit 971d35545) and an opt-in flag use_shared_lineage_solver on RustExplorationManager. Push/pop scoping for branch constraints already exists in the codebase — at a higher abstraction level than the spike proposes.

3. Bimodal slow-tail root cause is Z3 SAT-heuristic nondeterminism, not solver-state accumulation. Memories angr-pfy4-resolution (unbreakable_1), benchmark-bimodal-variance-rules, and the rust_engine.rst classification all converge on category (c): the SAT-search heuristic explores different branch-decision paths on different runs with IDENTICAL constraint sets. Push/pop wraps do not change the constraint set Z3 sees during check(), so they cannot shift SAT-heuristic variance.

Corroborating null result: avoid-lazy-fork-assume-no-impact memory documents the adjacent angr-hk7k attempt (lazy-solver materialization for assume_*) showing zero impact on fauxware/mma_howtouse. The save-by-deferring-materialization paid back on the next solver query. Same logic applies here: the next solver query rebuilds the same SAT search.

Decision: close angr-xfvf as no-action with this reasoning. Close angr-xhhq (impl bead) for the same reason. Future bimodal-bench perf work should target either (a) enabling SharedLineageSolver more aggressively (gated on workload heuristics — see v5ht-landed memory for what's safe) or (b) Z3 tactic experiments that reshape SAT-search structure (e.g. qfbv_smart, mul2concat, bv_extract_prop — all already enabled via build_solver_params in symbolic/context.rs:1040). The per-assume push/pop mechanism is NOT a viable lever.

xmllint cross-engine (angr-6d3l) CONVERGES post-aca6y. Under tools/xmllint_probe.py PROBE_SIM_PROCS=1, both Rust and Python engines: grind the 0x406883<->0x406896 option-parse loop, enter libxml2 init (0x561xxx region), fork+prune, run the full 120-step budget bounded with ZERO errored states. The iter32 Rust stack-PC deadend (bug aca6y) is gone. A secondary blocker was format_parser.interpret() raising on scanf %p (only s/d/i/u/x/c handled) — fixed commit 2f8deb4ca by adding b'p' to the base-16 atoi branch in angr/procedures/stubs/format_parser.py (mirrors the sprintf output-path %p->hex). Rust ~360MB/4.5s vs Python ~245MB/3.6s; the ~1.5x RSS/wall gap is block-chaining vs single-step granularity, not a divergence. This finding is now WRITTEN UP in docs/advanced-topics/rust_engine_characterization.rst .2 section (iter48), which let angr-p65i close (force-closed past 6d3l). 6d3l formal close + baseline_timings.json bench integration still gated on 75mc fuzzer-feature human a/b decision.

angr-75mc.1 (xmllint solve_symex.py offline-prepare) DONE iter7, commit fcdb3819d. Cross-repo angr-examples PR staged under tools/upstream_patches/angr_examples_xmllint_solve_symex.{patch,_PR.md} (upstream-pr-offline-prepare-slice-pattern). solve_symex.py = symbolic sibling of the fuzzer solve.py: use_sim_procedures=True, 16B symbolic stdin, bounded explore(find=getenv,n=400), single-state ~185 steps. RECOMMENDED find=getenv (NOT a parser callsite): fread/xmlReadFd explode as plain symex on BOTH engines per the 75mc_xmllint_fuzzer_decision.md addendum (Z3 OOM Python / symbolic-pointer concretization Rust; concrete XML stdin explodes identically). CAVEAT: getenv is pre-stdin so does NOT exercise syscall_python_fallback (vx8p step-4 premise) — inherent to any tractable symbolic xmllint target. Parent 75mc stays human-gated (needs cross-repo PR + bench-add); recommendation added as a 75mc comment. Patch applies cleanly + py_compiles (ruff binary not in venv; .patch/.md not linted).

xmllint vanilla-symex probe (angr-75mc path-b): vanilla symbolic execution of any real-glibc-linked binary (auto_load_libs=True, use_sim_procedures=False) errors at startup on 'operation error: unmapped VEX opcode: Iop_GetMSBs8x16' — a SSE PMOVMSKB hit inside glibc's SSE strlen/memchr during init (~step 3 under RustExplorationManager). Iter30 implemented VGetMSBs (fn vec_get_msbs in vex/ops_vec_count.rs; parse arms in opcode_map.rs; IROp::VGetMSBs in ir.rs) which removes THIS blocker (errored 1->0, advances to step 5 then deadends). But path-b is NOT cheaply unblocked: full-glibc symex without sim procedures still deadends early and will hit a chain of further missing ops/syscalls. A real xmllint bench needs use_sim_procedures=True (libc stubs) or a blob/main_opts load — but that changes what syscall-fallback surface it exercises (the original vx8p premise). Diagnostic tool: tools/xmllint_probe.py (bounded, RLIMIT_AS, stash-watching; run under nested capped scope).

Surprising finding from angr-xtse.1 (2026-05-23): in the current 21-bench corpus, FOUR of the five 'callback' types we measure NEVER fire — syscall, avoid_predicate, symbolic_branch, and python_vex_fallback all reported zero on every bench. Reasons: syscalls now go through native Rust handlers (post angr-7xms), CTF benches use addr-based not callable predicates, branches are mostly single-feasible (not both-feasible) so they don't need Python-side forking, and the Rust VEX interpreter covers every op in the corpus. ONLY simprocedure (and find_predicate via lightweight RustStateProxy) actually fire. Future plugin-API discussions for angr-xtse should weight this: the dispatch overhead of those four paths is theoretical — no live benches exercise them. Of the two that DO fire, find_predicate is already cheap (~17us per call via the lightweight proxy path); only simprocedure dispatch is expensive (csaw_wyvern: 68ms per call x 30 calls = 2052ms = 77% of wall). The csaw_wyvern simprocedure cost is INSIDE the Python procedure body, not in the FFI/dispatch — porting those procedures to native Rust would close the gap without a plugin API.

angr-xtse.1 (Quantify per-callback Python overhead) closed 2026-05-23. Added perf_stats fields and try/finally timing wrappers to the five public handle*_callback entry points in rust_callback_dispatch.py that were previously uninstrumented: syscall, find_predicate, avoid_predicate, symbolic_branch, python_vex_fallback. SimProcedure callbacks were already instrumented; memory_load/fetch_page/lift_block are pure FFI plumbing (not Python callbacks per se) and were left alone. Counters are surfaced through run_single.py --counters-json (via stats dict) and perf_report(). MEASUREMENT (21 benches, 1 sample each, rust engine): only SimProcedure and find_predicate callbacks fire in the current bench corpus. syscall/avoid_predicate/symbolic_branch/vex_fallback never fired on any bench — the rust corpus exercises CTF binaries where syscalls already go through native Rust handlers, predicates are addr-based not callable, branches are mostly single-feasible, and the VEX interpreter covers all the ops in the corpus. CALLBACK OVERHEAD DISTRIBUTION (21 benches): 4 with >=5% wall in callbacks (csaw_wyvern 77.2%/2052ms, fauxware 34.4%/58ms, google2016_unbreakable_0 21.9%/199ms, defcon2016quals_baby-re 10.9%/50ms), 6 with 1-5%, 11 with <1%. SPEEDUP CEILING (Python/Rust without callbacks): csaw_wyvern would jump 5.98x → 26.17x (+337.8% relative), google2016_unbreakable_0 1.47x → 1.88x (+28.0%), fauxware 2.23x → 3.40x (+52.5%). All others net under +5%. CONCLUSION FOR PARENT angr-xtse: callback overhead matters for a small number of SimProcedure-heavy benches; an in-Rust plugin API would deliver outsized wins on csaw_wyvern but marginal gains on the median bench. The parent's GO/DEFER call when its 2026-06-01 review hits should weight: (a) csaw_wyvern's 2-second callback cost is dominated by per-procedure execution time inside the Python SimProcedure body, NOT by the dispatch overhead — porting the procedures to native Rust would deliver the same win without a plugin API; (b) find_predicate callbacks are already cheap (~17us/call via the lightweight RustStateProxy path). NO regression risk from the instrumentation itself: 488/488 tests pass; the try/finally wrapping is zero-cost except for the perf_counter_ns calls (negligible).

angr-ymoe (2026-05-22, instrumented in commit pending): two orphan-BVS fallback paths in rust_manager.py (1337 mem_thunk_, 1886 sym_load_full_fail_) measured 0 fires across 21 fast-tier benches: fauxware, ais3_crackme, defcamp_r100, csgames2018, csaw_wyvern, codegate_2017-angrybird, defcon2016quals_baby-re, ekopartyctf2016_rev250, flareon2015_{2,5,10}, google2016_unbreakable_{0,1}, mma_howtouse, strcpy_find, sym-write, unmapped_analysis, whitehatvn2015_re400, securityfest_fairlight, ekopartyctf2016_sokohashv2. Decision: KEEP both fallbacks; counters (orphan_bvs_mem_thunk, orphan_bvs_sym_load_full_fail in mgr.stats()) act as watchdogs. Hard-error rejected because path is dead in practice — no benefit, and test_cb_memory_load_symbolic_full_swallows_sim_memory_error explicitly locks in the swallowing behavior (Rust upstream wraps the result in a sym_pyref_* placeholder via expressions.rs). Rust-side fresh symbol pattern (angr-4pm1's _set_state_register_symbolic_ast FFI shim) is the escalation path if counters ever go non-zero. AUDIT FINDING (item C in original bead): a 3rd orphan-BVS site exists at rust_state_export.py:1041 in _restore_symbolic_regions ('Fallback for symbols created in Rust without a tracked AST'). It only runs at snapshot-export time, not in the hot exploration loop, but should be tracked separately if it becomes a fidelity concern.

ype54 DECISION (iter46, decision spike angr-ype54.1) — BOTH candidates (a) and (b) as written are REFUTED; the 45-iteration premise 'the parallel wave loses the deferred fork' is FALSE. Method: env-gated (ANGR_DUMP_RESUME) eprintlns at four points — worker NeedsPython arm (run_loop.rs parallel_process_state), coordinator route_materialized_terminal find-addr arm, dispatch_bounce (stepping.rs, shared by seq+par), and _resume_after_simprocedure (resume.rs) — printing sid/pc/num_constraints/n_deferred/n_forks/sat. ALL instrumentation reverted; tree clean.

HARD EVIDENCE (fauxware, num_find=2, phase2 off):

• W=2 worker bounce sid=1 @0x700028 (SimProc): n_deferred=1 -> materialize_bounce_forks mints n_forks=1 (sid=2) and applies the taken assume (nc 0->1). The fork IS created.
• sid=2 steps, bounces Hook @0x4006ed (= the find addr), and route_materialized_terminal's MatKind::Bounce find-addr arm evaluates sat=TRUE and pushes it to STASH_FOUND. found=1 after wave 1. THE FORK IS NOT LOST — the single found state in W=2 IS the fork.
• What IS lost is the MAIN continuation (sid=1). It survives migration but is UNDER-CONSTRAINED: at each SimProc bounce the Python callback contributes +2 constraints in seq but only +1 in par. Trace: seq DISPATCH nc=0 -> RESUME nc=2 (+2) -> +1 apply_deferred = 3; DISPATCH nc=3 -> RESUME nc=5. par DISPATCH nc=1 -> RESUME nc=2 (+1); DISPATCH nc=2 -> RESUME nc=3 (+1). new_constraints from Python is EMPTY (n_py=0) in BOTH — the constraints are written through the SHARED solver context during the callback, not synced via sync_constraints_from_python. Under-constrained sid=1 then dies (active 1->0) without reaching 0x4006ed a second time.

RULED OUT this iter: (i) has_active_states() ignoring pending_parallel_bounces — patched, no effect (the bounce queue is not where the state dies); (ii) materialize_bounce_forks applying the taken assume to base BEFORE the Python callback (seq applies it AFTER, at resume) — A/B'd via ANGR_NO_BASE_ASSUME, found_count still 1, so the ordering divergence is real but NOT causal.

NEXT (owner: angr-ype54.2, re-scoped): find the ONE constraint the Python SimProcedure callback writes into the shared solver on a NON-migrated state but not on a detach/reattach'd one. Instrument SymContext::assume_true (symbolic/constraint_ops.rs) with an env-gated backtrace during callbacks and diff seq vs par. Strongly suspect state-fidelity-through-the-Python-proxy on a reattached state (same family as angr-5rjbq: proxy loads returning Rust zeros instead of Python-installed symbols).

ype54 fauxware wave-loss: W=1 ground truth + why Python-side probing is infeasible. W=1 (single-thread) explore(find=0x4006ED,num_find=2) yields found=2: found[0]=backdoor stdin '...SOSNEAKY', found[1]=normal-auth computed pw; BOTH found states have solver.constraints len==1 (the accept-path branch collapses to a single combined constraint), plus deadended=1 at 0x700030 (strcmp-return trampoline). W=2 (RUST_PARALLEL_WORKERS=2) yields found=1 (the documented bug). BLOCKER for probing: the W=2 fauxware run is ~90s..>120s and NON-DETERMINISTIC on this 6G box (faorh serde-thrash), sitting right at the tool timeout boundary. Worse, post-explore Python state inspection in parallel mode is unreliable: s.posix.dumps(0), s.solver.constraints, and even mgr.stash_counts() hang/time-out on found states (only len(list(mgr.found)) reliably returns). CONCLUSION: do NOT try to characterize this bug via Python-side inspection in W=2 — every probe cycle costs ~2min and is variable. The next probe MUST be a native env-gated trace (log assumed_constraints at insn 0x4006dd inside the strcmp bounce, in resume.rs / run_loop.rs parallel_process_state), gated behind an env flag, rebuilt via tools/rebuild-rust.sh --cargo-only --keep-cargo-cache. See [[ype54-taken-constraint-hypothesis-disproven]] and [[ype54-second-branch-feasibility-divergence]].

ype54 iter35: CONCRETIZATION HYPOTHESIS DISPROVEN. Env-gated probe (ANGR_YPE54_TRACE) + #[track_caller] std::panic::Location::caller() at both assume sites shows: on BOTH W=1 and W=2, every guard at apply_deferred_fork_constraints (callback_types.rs) and build_unexplored_fork (helpers.rs) is SYMBOLIC (width=1, is_concrete()=false, as_u128()=None, cid=0). There is NO concrete-0x0 poison at these sites. The bug is a DROPPED FORK, not concretization. Caller trace: W=1(seq,found=2) fires apply_deferred n_forks=1 @resume.rs:78 -> build_unexplored @resume.rs:145, then apply_deferred n_forks=0 @resume.rs:78 -> build_unexplored @core_outcome_handlers.rs:202 = TWO cid=0 forks. W=2(par,found=1) fires build_unexplored @core_outcome_handlers.rs:202 ONCE (via worker in-thread materialize_bounce_forks @run_loop.rs:406) + apply_deferred n_forks=0 twice = ONE cid=0 fork. The missing fork is the one seq builds at resume.rs:145 from pending.deferred_forks. Parallel SimProc bounce resume (process_parallel_bounce_queue, run_loop.rs:933) hardcodes deferred_forks=Vec::new() by design (worker materializes in-thread), but the worker's PendingBounce.deferred_forks (populated step_core.rs:334 -> run_loop.rs:315) contains ONE FEWER deferred fork than seq's PendingCallback.deferred_forks. NEXT: instrument deferred_forks.len() at PendingBounce construction (run_loop.rs CoreReturn::NeedsPython ~399) vs seq PendingCallback::with_context to find where the fork count diverges to 1-vs-2.

ype54 lost-fork: root-cause facts from iter45 stand — (1) the migrated non-backdoor state is src_sat=TRUE at to_snapshot (a VALID feasible fork, NOT unsat-at-source; overturns iter44); (2) the restore-side concrete-false assume (restore_from_snapshot, Concrete(0x0,1) guard) is a SEPARABLE RED HERRING — patching restore to skip concrete-folding assumed guards zeroes the false asserts but W=2 still found_count=1; (3) the observable failure is empty stored_conditions after migration ('condition 1 not found') degrading to an unconstrained fallback fork. FIX GUIDANCE CORRECTED 2026-07-11: iter45's 'NEXT: implement the description guard-serialization fix' is WRONG — iter43 already implemented exactly that and it FAILED (path loss unchanged + test_parallel_wave regresses 4/7), because parallel_process_state advances set_pc BEFORE the NeedsPython bounce so the coordinator forks a state already PAST the branch; see avoid-ype54-guard-serialization. Live candidates + decision process now live in the rewritten angr-ype54 description and child angr-ype54.1 (decision spike): (a) fork at the pre-branch state, or (b) preserve the worker-side constraints so the fork is born before migration.

CORRECTED (iter27): ype54 fauxware wave path-loss (workers=2 finds 1 of 2 accepting paths) is NOT Bug M1 and NOT SymbolicBranch guard serialization. Both prior root-causes are disproven.

Bug M1 (the wave-cancel frontier drop in scheduler_worker.rs::worker_loop, the is_cancelled arm that returns without draining the worker-local queue) is RULED OUT: request_cancel fires ONLY when found_counter+1 >= num_find (run_loop.rs parallel_process_state find-addr arm). The repro is find=[0x4006ED] num_find=2 and found is STUCK at 1, so request_cancel NEVER fires and that cancel-drop code is never executed. Wiring drain_local_upstream into the wave-cancel path (iter26 plan) is a NO-OP for fauxware. iter26 conflated natural quiescence (active_empty: Continue root=0x8 -> 0 successors, END found=1) with the cancel path. agrees with lq9rz iter9 note 'num_find=2 never reached, so CancelToken frontier-drop is NOT the trigger'.

Guard serialization across the thread::scope join (lq9rz/iter24) is ALSO not it: iter24 found NO SymbolicBranch bounce ever crosses the join for fauxware, and the guard-carry fix regressed test_parallel_wave 4/7 (net-harmful, reverted).

REAL surface: the non-backdoor deferred fork IS materialized in-thread (parallel_process_state NeedsPython arm -> materialize_bounce_forks -> process_deferred_forks_into_core, core_outcome_handlers.rs) with its guard applied via build_unexplored_fork+assume_false, returned as continue_states, absorbed into worker local, stepped in-wave to quiescence -- yet never registers Found at 0x4006ED. Two candidates to bisect NEXT (instrument, no risky code first): (1) satisfiability-prune: fork evaluates UNSAT in worker Z3 ctx at the find-addr pre-step check (lazy_solves || state.satisfiable()) or inside process_deferred_forks_into_core (lazy_solves || forked.satisfiable()) and is Pruned instead of Found -- check whether lazy_solves is on; if off, worker-ctx satisfiable() mismatch vs sequential is prime suspect. (2) path-divergence: stored_condition keyed by condition_id missing from worker map so the wrong/no guard is applied and the fork steps a dead path. Full detail on bead angr-ype54 iter27 note. Repro: /tmp/repro_lq9rz.py, /tmp/repro_sep.py.

ype54 fauxware wave-mode lost-path ROOT CAUSE (iter29, CONFIRMED via branch-feasibility probe): the parallel wave loses the non-backdoor accepting path because the SECOND symbolic branch diverges in feasibility, NOT a sat-prune, NOT Bug M1, NOT the deferred-fork machinery. Pinpointed at authenticate()'s serial-auth check (insn 0x4006dd, 'test eax; jne 4006e6' -> 0x4006df accept / 0x4006e6 reject). Probe results (add log::debug at interpreter/statements.rs execute_stmt_with_callbacks Exit-arm right after ctx.check_branch_feasibility, logging current_insn_addr + can_be_true/false + ctx.num_constraints): SEQUENTIAL workers=1 found=2: branch 0x4006dd can_true=true can_false=true ncon=5 -> FORKS -> serial-accept reaches accepted()@0x4006ED. WAVE workers=2 phase2=off found=1: branch 0x4006dd can_true=FALSE can_false=true ncon=3 -> does NOT fork -> only reject -> id=1 falls into rejected()@0x4006FD (0x400713 = exit inside rejected). The backdoor branch (0x400690) forks identically in both (ncon=0) and its deferred fork (id=2) reaches accepted() and IS pushed to STASH_FOUND correctly (route_materialized_terminal MatKind::Bounce find-addr arm, run_loop.rs ~L862, sat_found=true). So the wave state id=1 arrives at the serial branch with a DIFFERENT constraint SET (3 vs 5 constraints) that makes the accept side infeasible. The divergence is upstream of the branch, traceable to the serial strcmp simproc bounce (bounce target 0x700010) which id=1 hits between 0x4006c8 and 0x4006db -- the bounce constrains the symbolic input differently in the wave vs sequential. NEXT (fix-scoping): dump the actual constraint STRINGS at 0x4006dd in both modes (not just count) to see which constraints differ; investigate how dispatch_bounce / the strcmp simproc bounce return re-integrates the comparison result constraints into the continuing wave state. Repro: /tmp/repro_ype54_w2.py (forces RUST_PARALLEL_WORKERS=2) and /tmp/repro_ype54_w1.py; RUST_LOG=rustylib::interpreter=debug for branch feasibility.

ype54 fauxware wave-mode lost-path: taken-constraint hypothesis DISPROVEN (iter30). Hypothesis was: process_parallel_bounce_queue (run_loop.rs:930-937) reconstructs the PendingBounce with EMPTY deferred_forks/stored_conditions, so resume_after_simprocedure's apply_deferred_fork_constraints(main_state,...) is a no-op in parallel mode -> the main bounce state never gets its own taken-path branch constraints applied (unlike single-threaded resume.rs:78). FIX TRIED: in the worker's CoreReturn::NeedsPython arm (run_loop.rs ~L395-436, parallel_process_state), clone deferred_forks+stored_conditions before materialize_bounce_forks, then apply_deferred_fork_constraints(&bstate, &deferred_forks, &stored_conditions) in-worker (correct Z3 ctx) AFTER forks snapshotted. Clippy-clean, rebuilt via tools/rebuild-rust.sh --cargo-only. RESULT: repro /tmp/repro_ype54_w2.py STILL found_count=1 (w1 control=2). Change was INERT for fauxware -> the strcmp SimProcedurePython bounce (0x700010) carries NO deferred_forks (the accept/reject fork is at 0x4006dd AFTER strcmp returns, a separate step). So the divergence is NOT the main-state taken constraints. REVERTED (tree clean). Note: the zeroed-deferred_forks-in-parallel-bounce IS a real latent gap for bounces that DO carry deferred forks (symbolic branch deferred in same block before a simproc call), just not exercised by fauxware -- unverified. NEXT (still measure-first): dump the actual assumed_constraints STRINGS (ctx.get_assumed_constraints(), snapshot_fork_ops.rs) at insn 0x4006dd in both w1/w2 to see WHICH constraint pins strcmp's return so accept(can_be_true) goes FALSE in wave; suspect sync_constraints_from_python over-constrains, or the strcmp simproc runs on a differently-constrained input in wave. Repro files: /tmp/repro_ype54_w{1,2}.py; RUST_LOG=rustylib::interpreter=debug.

angr-ype54 (parallel wave loses fauxware's non-backdoor accepting path on workers=2): the lq9rz 'serialize the SymbolicBranch guard across the thread::scope join' root-cause is WRONG for this symptom. Instrumenting the worker CoreReturn::NeedsPython arm (run_loop.rs) shows kind_sb=false for ALL parked bounces on fauxware workers=2 — NO BounceKind::SymbolicBranch ever crosses the join, so the empty-stored_conditions/ValueError is a PHASE-2-only re-seed artifact, not the phase-1 loss. A full guard-carry impl (last_condition->RustBVData through MatKind::Bounce/kind_map, rebuilt in the coordinator ctx) compiles clippy-clean but does NOT recover the path AND regresses 4/7 test_parallel_wave (phase2 then dupes the backdoor because the guard over-constrains a fallback fork that previously recovered the path). Real loss is in deferred-fork materialization (materialize_bounce_forks / worker pre-step route), NOT condition serialization. Add a workers=1-vs-2 phase1 fork-count assert before touching serialization.

z087y Stage-2 bench-gate proof (inc3, angr-z087y.1): the native libVEX cold-block lift seam FIRES end-to-end and is byte-for-byte faithful. Method: build .so with --features libvex-ffi via cargo-direct (Z3_LIBRARY_PATH_OVERRIDE=/lib/python3.12/site-packages/z3/lib, else system-vs-venv libz3 mismatch segfaults), cp target/release/librustylib.so -> angr/rustylib.cpython-312-x86_64-linux-gnu.so. GOTCHA: libvex_ffi_enabled() is registered on the rustylib.VEX_ENGINE SUBMODULE (engine.rs register_module builds the vex_engine submodule, NOT top-level rustylib) -> call r.vex_engine.libvex_ffi_enabled(), NOT r.libvex_ffi_enabled(). Counter keys in mgr.stats(): rust_native_lift_count / rust_native_lift_fallback_count / callback_lift_block_count (NOT native_lift_count). A/B via new run_single.py --native-lift flag (use_native_lift kwarg). fauxware result: OFF native=0/callback=14; ON native=14/callback=0/fallback=0; full-output diff = ONLY the 14 python_callback->native_lift swap, solution+active=2 identical. RESIDUAL: perf win (xmllint init-storm gil drop) still unmeasured; and native lift only covers cold-block lifts, warm cache hits unaffected.

z087y Stage-2 inc2 (native-lift Python wiring): RustExplorationManager gets a use_native_lift kwarg (default False), threaded through _phase_boot (NOT init body directly — construction of self._rust_mgr lives in _phase_boot, so any new ctor config kwarg must be added to _phase_boot's param list AND the _phase_boot(...) call in init, else NameError). Flag flips manager-level set_native_lift_enabled (exploration/mod.rs) which sets MemoryConfiguration.native_lift_enabled -> StepContext.native_lift_enabled (step_core.rs step_context()) -> interp.set_native_lift_enabled(ctx.native_lift_enabled) in run_interpreter_step_core. Python gate: from angr.rustylib.vex_engine import libvex_ffi_enabled (new #[pyfunction] in engine.rs returning cfg!(feature=libvex-ffi)) AND project.arch.name=='AMD64'. Default .so: probe False + interp setter is no-op stub -> byte-for-byte unchanged. Commit a9c5777be.

z087y Stage-2 native libVEX engine seam (commit d133003ea): VEXInterpreter::get_or_lift_block calls try_native_lift(addr) (both in interpreter/execution.rs) BEFORE the Python lift_block callback, gated on #[cfg(feature="libvex-ffi")] + a native_lift_enabled bool field (interpreter/mod.rs struct VEXInterpreter). try_native_lift reads concrete block bytes via rust_memory.read_concrete_bytes_for_lift(addr, 5000) and lifts with NativeLibVEXLifter (vex/libvex_lifter.rs); returns None -> Python fallback on: disabled, opt-level-override/global-opt-level set (parity: shim uses pyvex compiled defaults), missing rust_memory, symbolic/empty bytes, or LiftError. Counters native_lift_count / native_lift_fallback_count. Toggle via set_native_lift_enabled() (no-op stub for a feature-off build). GOTCHA: NativeLibVEXLifter is a UNIT struct (no ::default() -- clippy default_constructed_unit_structs); import the trait as crate::vex::VEXLifter (re-export) since vex::lifter module is private. PYTHON WIRING (inc2, commit a9c5777be): RustExplorationManager takes a use_native_lift kwarg (default True since Stage-3, commit 63d201a88), threaded through _phase_boot — NOT the init body directly: construction of self._rust_mgr lives in _phase_boot, so any new ctor config kwarg must be added to _phase_boot's param list AND the _phase_boot(...) call in init, else NameError. Flag flips manager-level set_native_lift_enabled (exploration/mod.rs) -> MemoryConfiguration.native_lift_enabled -> StepContext.native_lift_enabled (step_core.rs step_context()) -> interp.set_native_lift_enabled(ctx.native_lift_enabled) in run_interpreter_step_core. Python gate: from angr.rustylib.vex_engine import libvex_ffi_enabled — a #[pyfunction] registered on the vex_engine SUBMODULE (engine.rs register_module), NOT top-level rustylib — AND project.arch.name=='AMD64'. Feature-off .so: probe returns False + interp setter is a no-op stub -> byte-for-byte unchanged. Shipping status, perf table and counter-reading traps: docs/advanced-topics/rust_libvex_ffi.rst (libvex-ffi is default-ON in the pip build since angr-3trr7).

z087y Stage-2 inc3b (angr-z087y.2) PERF PROOF: native libVEX cold-block lift measurably cuts GIL work on AMD64 init-storm. Method: cargo-direct build --features libvex-ffi (Z3_SYS_Z3_HEADER=/usr/include/z3.h since venv z3/include/z3.h does NOT exist; Z3_LIBRARY_PATH_OVERRIDE=/z3/lib), cp target/release/librustylib.so -> angr/rustylib.cpython-312-x86_64-linux-gnu.so. A/B on xmllint_getenv via run_single.py --native-lift --counters-json. RESULT: rust_native_lift_count 0->135, callback_lift_block_count 135->0, rust_native_lift_fallback_count=0 (every cold lift went native, no fallback); gil_work_time_ns 81.3ms->56.0ms (-31%); rust_lift_time_ns 31.5ms->0. Fidelity preserved (found=1 both). WALL ~flat (3.49->3.45s) — xmllint is init/solver-dominated so GIL-lift is a small wall fraction; the win is the GIL-share drop + removing a serialization point (matters for PARALLEL warmup, the original ROI thesis). Stage-2 perf gate MET. Stage-3 (AMD64 default-on) is the remaining z087y work. --counters-json preamble is 2 lines ('OK rust ...' + '> ...') before the JSON; skip to first line starting with '{'.

angr-z2nt (2026-05-22, closed without code change): proposed delta-only constraint sync in sync_before_callback (interpreter_cb/constraints.rs:85-99) was filed before the angr-bs71 counter telemetry landed. Counter evidence shows mgr.stats()['cb_sync_calls'] = 0 on fauxware/defcamp_r100/mma_howtouse this session (plus 14 fast-tier benches in the wi5m baseline). The sync_before_callback and engine.rs:1037 post-loop sync paths never push constraints in production — delta-only optimization is moot. Lesson: when a bead proposes optimizing a code path, verify the path is hot via counters BEFORE writing code. Stronger follow-up angr-wi5m (remove path entirely, blocked on nightly counter soak) is the active item. If counters ever go non-zero across the bimodal benches that the PR-time gate skips, re-open.

Profile of _sync_registers_to_rust on fauxware (2026-05-11, 100 fresh entry_states):

Wall-clock breakdown per state (43 registers, 17 BVV + 26 symbolic at entry_state): TOTAL _sync_registers_to_rust: 4.40 ms (cProfile-inflated to ~7.9 ms) getattr(state.regs, name) ×43: 2.98 ms (68%) + z3_backend.convert (×26): 0.76 ms (17%, on top of getattr) FFI set_registers_bulk(): 0.003 ms (~0%) FFI set_register_symbolic ×26: 0.007 ms (~0%)

68% of cost is angr's register-plugin pipeline — getattr(state.regs, name) walks the 14-level memory-mixin stack (view → name_resolution → size_resolution → actions → bvv_conversion → ... → ultra_page.load). For 26 unconstrained registers (xmm0-15 + cc_op/dep/ndep + flags), it ALSO invokes default_filler_mixin._default_value which creates a fresh BVS and writes it back to the register page (~3 ultra_page.store per state).

FFI cost is negligible (~10 µs/state across 43 set ops). The bead's premise that FFI dominates was wrong; the cost is upstream of the Rust boundary.

_add_rust_state (and therefore this function) is called once per seed state added to the Rust manager (and once per merged state re-add) — NOT per exploration step, NOT per callback. Real benchmarks run for 0.1–10+ seconds; saving 3 ms per init is below noise floor (<0.5% even on fauxware).

Potential optimizations and why they were declined:

• Bulk-read register file (single ~1.2 KB load instead of 43 getattrs): fragile, requires bypassing angr's mixin stack; symbolic bytes mixed with concrete bytes would force per-register splits anyway.
• Skip unconstrained-default registers: correctness risk — if user code later reads xmm0 from the Python proxy, the BVS won't match what Rust uses.
• Cache the precomputed_regs dict across seed states: works only when the same binary's entry_state is added repeatedly; entry_state() mints new BVS names each time, so cached AST pointers would carry stale symbol IDs.

Disk-cache fast path (precomputed_regs from disk init cache) already short- circuits this whole function to 7 µs/call (verified with 200 calls). When the disk cache is warm, _sync_registers_to_rust is effectively free.

DECISION: Close as no-action. The slow path runs only on cache misses (first-ever load of a binary into RustExplorationManager), happens once per seed, and the cost is in code outside the Rust extension's control. Existing memory register-sync-bottleneck already documented that the symbolic-conversion sub-portion is not a benchmark hot path; this adds the per-getattr breakdown that confirms FFI is irrelevant too.

angr-zdho measurement (2026-05-20): RustBV structural-duplicate rate across asserted-constraint graphs on 8 fast-tier benches is 25-85% (median ~40%). Definition: structural_duplicates / unique_pointers, where structural_duplicates = pointers that hash-cons WOULD collapse.

Key numbers (from RustExplorationManager.analyze_constraint_sharing()):

• fauxware: 27.3% (44/161)
• csaw_wyvern: 53.4% (124/232)
• defcamp_r100: 30.2% (78/258)
• ais3_crackme: 39.7% (686/1730)
• ekoparty_rev250: 25.5% (694/2719)
• whitehatvn2015_re400: 57.3% (349/609)
• sym-write: 60.9% (789/1295)
• codegate_2017-angrybird: 84.8% (6811/8033)

The per-call to_z3_ast_cached hit-rate (z3_ast_cache_hit / (hit + miss)) is BIMODAL: 0-3% on 6 of 8 benches, 19% on csaw_wyvern, 38% on sym-write. The per-call cache catches almost no within-call sharing on simple benches, but is meaningful on dense-ITE workloads. Don't conflate the two metrics: per-call hit-rate is about Arc reuse WITHIN one to_z3_ast() invocation; structural-duplicate rate is about distinct Arcs ACROSS the exploration that hash-cons would merge.

Bead promoted angr-behq from P4 to P3 on this signal.

[STATUS iter136: the angr-gorvf.8 fix HAS LANDED (ab0ed7459 + 5f8d936e4). gil_work_time_ns now INCLUDES the park-and-bounce excursion as GilClass::Bounce, so the 'blind to simprocedure' caveat below is historical: the gate is self-sufficient again. Honest corpus result is PASS=4/36, not the 10/36 or 6/36 quoted below — use benchmark-zeropy-pass-count-iter136 for the current numbers and invariant-bounce-gil-accounting for the mechanism. The in-loop gil_by_site ranking below is still valid for the IN-LOOP callback class.]

ZeroPy (gil_work_time_ns==0) milestone attribution, MEASURED 2026-07-14 (angr-gorvf.4) via tests/benchmarks/run_zeropy_gate.py. Harness: drives run_single.py --counters-json over baseline_timings.json's 36 benches; gate = gil_work_time_ns==0 AND run_wall_time_ns>0.

TRAP 1 (cost the first read): baseline_counters.json entries for 7 benches (CADET_00001_partial, sokohashv2, flareon2015_10, unbreakable_1, angry-reverser, mma_howtouse, fairlight) LACK the gil_work_time_ns key entirely, so a .get(k,0) read fabricates 7 fake passes. A missing key means the profiled run loop never ran on the stats-reading thread => UNMEASURED, never PASS. The gate encodes this.

TRAP 2 — the callback_* Python-side counters are process-wide and tick OUTSIDE the profiled run-loop window (during setup/export/predicates), so a raw callback COUNT does not track in-loop GIL cost. Canonical example: fauxware reports posix=5/simprocedure=1 yet scores zero in-loop GIL. Rank IN-LOOP levers by the gil_work_ns_/ split, never by callback counts.

[CRITICAL iter135 AMENDMENT to trap 2 — do not over-apply it.] 'Not in-loop GIL' is NOT the same as 'not real Python work'. callback_simprocedure_total_ns specifically IS genuine exploration-time Python: it times the park-and-bounce handler (handle_simprocedure_callback: state_create + execute + state_copy + sync_back), which runs with the Rust loop EXITED — so it is invisible to gil_work_time_ns AND to run_wall_time_ns by construction, not because it happened at setup. Measured: fauxware run_wall=10.5ms vs callback_simprocedure_total_ns=59.6ms (5.7x the window), gil contribution 0. Blanket-dismissing the callback* column as noise is what let a 2623ms corpus-wide lever sit unactioned for several iterations, AND it means the gate can score a bench as a ZeroPy PASS while it runs Python. See zeropy-gate-blind-to-simproc-bounces (the full evidence) and angr-gorvf.8 (the fix).

TWO FALSIFIED HYPOTHESES (still hold): (1) the claripy AST bridge is NOT the residual GIL — ~0ms, despite import.rs/export.rs holding GilWorkGuards. (2) callback counts do not track in-loop GIL cost.

LEVER RANKING (libvex build, FAIL benches, by in-loop GIL ns): callback=3746ms, fork_metadata=4ms, claripy_import=0ms, claripy_export=0ms.

ZeroPy gate blindness to SimProcedure bounces — RESOLVED 2026-07-14 (iter136) by angr-gorvf.8, commits ab0ed7459 + 5f8d936e4. The blindness was REAL: gil_work_time_ns could read 0 while a bench executed a 59.6ms Python 'open' SimProcedure, because the park-and-bounce handler runs with the Rust run loop EXITED (RunLoopWallGuard dropped, no GilWorkGuard live) so both the numerator and denominator were stopped across it. FIX: GilClass::Bounce in gil_profile.rs — see invariant-bounce-gil-accounting for the mechanism and the rule new callbacks must follow. CONSEQUENCE: gil_work_time_ns is now self-sufficient; run_zeropy_gate.py needs NO special case and its gil==0 predicate again means 'no Python ran during exploration'. Corrected corpus result: PASS 4/36 (was reported 6/36 pre-fix) — see benchmark-zeropy-pass-count-iter136. This memory is kept as the historical root-cause record; do not re-derive the dead end of hunting a 'simprocedure dispatch site' in callbacks/dispatch.rs (there still is none — the bounce is bracketed at the pymethod boundary in exploration/manager_methods.rs::run + exploration/resume.rs).

[STATUS iter136: the angr-gorvf.8 fix HAS LANDED (ab0ed7459 + 5f8d936e4). gil_work_time_ns now INCLUDES the park-and-bounce excursion as GilClass::Bounce, so the 'blind to simprocedure' caveat below is historical: the gate is self-sufficient again. Honest corpus result is PASS=4/36, not the 10/36 or 6/36 quoted below — use benchmark-zeropy-pass-count-iter136 for the current numbers and invariant-bounce-gil-accounting for the mechanism. The in-loop gil_by_site ranking below is still valid for the IN-LOOP callback class.]

ZeroPy lever ranking, MEASURED 2026-07-14 (iter132, post-angr-gorvf.4.6, libvex-ffi feature build, run_zeropy_gate.py; SUPERSEDES zeropy-lever-ranking-iter131). Gate reported PASS=10/36. Residual IN-LOOP callback GIL across the 25 FAIL benches, by dispatch site: lift_block 702ms (appears=18) > memory_store_symbolic_value 666ms (appears=1 — a SINGLE bench, flareon2015_5; owned by angr-gorvf.7, now dep-blocked on the memory-proxy policy bead angr-grji4) > memory_load 186ms (appears=10) > resolve_function 11ms (appears=4) > memory_store 1ms > batch_fetch_pages 0ms (RETIRED — do not spend another iteration here). lift_block still dominates the named callback sites even on a libvex-ffi build because that feature only covers AMD64 cold blocks — the arm/mips/aarch64 arch benches still lift through Python; retiring it is the human policy bead angr-3trr7.

[CORRECTION iter135 — READ THIS BEFORE USING THE RANKING.] The line this memory used to carry — 'by crossed surface: simprocedure count=87 / 2788ms is the biggest remaining class overall' — was TRUE but MISLEADING, and it caused several iterations to re-derive a dead end. Two facts reconcile it: (1) That 2788ms IS real exploration-time Python (callback_simprocedure_total_ns is the Python-side timer around the bounce handler: state_create + execute + state_copy + sync_back). It is NOT the setup-counter noise that zeropy-gate-attribution warns about. (2) But it can NEVER appear in the gil_by_site table, because the simproc fallback is the park-and-bounce path (run loop EXITS -> Python -> resume) and gil_work_time_ns is stopped throughout. There is no gil_work_ns_callback_simprocedure key and none of the 18 GilWorkGuard sites in callbacks/dispatch.rs is the bounce. So: ranking levers by gil_by_site is correct for IN-LOOP GIL and blind to the single biggest Python cost in the corpus. Do not 'find the simprocedure dispatch site' — it does not exist. See zeropy-gate-blind-to-simproc-bounces; the fix is angr-gorvf.8.