invariant / 3

RustSimState.map_memory(addr, size, perm_bits) Python perm encoding is the Permission::from_bits scheme (NOT Linux mprotect bits): bit 0x4 = read, 0x2 = write, 0x1 = execute. So 0x4=R, 0x6=RW, 0x7=RWX, 0x5=RX. Mismatch (e.g. passing PROT_READ=1 thinking it's read) silently maps execute-only pages because bit 0x1 = execute. Used in test_cross_page_permission_write_returns_error (commit 3159ccfcd) and several Rust unit tests in memory.rs::tests.

Python→Rust memory page permissions are CURRENTLY coarse: angr/exploration/rust_state_sync.py maps binary regions and section overlays with perm=7 (RWX) at lines 277, 290, 311, 343. Stack pages are mapped with perm=6 (RW, no X) at lines 213, 398, 415. So with STRICT_PAGE_ACCESS, the NX check primarily catches: (a) execution of stack/heap memory (perm=6), (b) execution of unmapped pages (existing memory unmapped check). It does NOT yet enforce per-section .text vs .data distinctions because both are mapped RWX. Improving this would require teaching rust_state_sync to read the loader's per-page permissions and pass them through instead of the hardcoded 7.

RustStateProxy.del + RustExplorationManager.drop_copy(state_id) reclaim _copies stash entries (angr-yhe0, commit 4cd70b323). Architecture: (1) RustStateProxy.copy() sets _owns_copy=True on the returned proxy; (2) del best-effort calls python_mgr.drop_copy(state_id) when _owns_copy is True — proxies for live exploration states never auto-drop; (3) drop_copy invokes the new Rust API drop_state_from_stash(id, '_copies'), which is the only place that removes a single state from a stash by id (move_state/clear_stash existed but neither dropped individuals). It clears _py_state_options/_py_state_globals/_stdout_tracker and calls clear_state_metadata. Safety invariant: drop_copy refuses if the state is NOT currently in 'copies', so passing an active-state id is a no-op. Idempotent: second drop returns False. Tests: TestStateProxyCopy::test_drop_copy*, test_proxy_copy_del_drops_state_from_copies, test_proxy_copy_chain_gc_releases_all_copies (5 new tests). Replaces the v1.0 no-GC caveat from rust-proxy-copy-design.

RustStateProxy sub-proxies (solver/memory/posix) now SHARE one forked solver context, minted lazily by RustStateProxy._get_shared_solver_ctx and injected via the shared_ctx_getter ctor arg (angr-yodz, 2026-06-15). This makes proxy.add_constraints(c) visible to proxy.posix.dumps(0) and proxy.memory.load(symbolic_addr) on the SAME proxy. Still VIEW-LOCAL: the constraint lands on the forked context, NOT the underlying Rust state solver (state_constraint_count unchanged), so it neither perturbs live exploration nor survives into a freshly built proxy. To persist onto the state, use mgr._rust_mgr.add_constraints_to_state(state_id,[...]) (the RustSolverProxyPlugin write-through path used in SimProc callbacks). Standalone sub-proxy construction (no getter) still forks its own context, preserving low-level unit-test behavior.

Rust's RustSimState defaults are not always equal to angr's loader-set defaults — for posix_brk specifically, Rust hardcodes 0x1B00000 while angr's SimUserland sets state.posix.brk to (binary last_addr + page) which is typically below 0x1B00000 (e.g., 0x602000 for fauxware). A naive max(rust, python) Rust→Python sync therefore clobbers Python's correct value with Rust's stale default. Why: Rust's defaults were copied from angr's static-default constants, but angr overrides them on state creation based on binary layout. How to apply: any Rust→Python sync of a field that the loader can override must (a) push Python's value into Rust at state creation (in _add_rust_state) so defaults agree, OR (b) gate the sync on whether Rust's value has been advanced from its known default. mmap_base happened to work without this because the loader doesn't touch state.heap.mmap_base.

Any monkey-patch of angr.factory.AngrObjectFactory.simulation_manager that returns a RustExplorationManager MUST guard the call stack: fall through to the original SimMgr when the caller frame is under /angr/analyses/ or /angr/exploration_techniques/. Why: angr internals (CFG jumptable resolver, exploration techniques) call factory.simulation_manager(state, resilience=True) with internal SimStates that carry DO_RET_EMULATION etc. RustExplorationManager._check_raise_options (rust_manager.py:2580) rejects those options and aborts the analysis. Same bug pattern hit run_single.py (fixed earlier, see memory strcpy-find-regression-root-cause) and test_rust_integration.py (angr-dmqr, fixed 2026-05-17 commit 96a23b64d). How to apply: when adding any new test fixture or runner that needs to redirect the default SimMgr to Rust, copy the traceback.extract_stack() guard from tests/benchmarks/run_single.py:136-158.

RustSolverProxyPlugin must expose SimSolver convenience aliases (angr-8oiw, 2026-06-04). When installing the proxy as state.solver during callbacks, SimProcedures call these methods that aren't on the basic 'eval/satisfiable/add/min/max' surface: simplify(e) — claripy.simplify delegation; single_valued(e) — returns not self.symbolic(e) (non-static mode); min_int/max_int — SimSolver aliases for min/max (libc/memcmp.py); eval_to_ast(e, n) — returns claripy.BVV list; unique(e) — eval_upto(e, 2) cardinality check; downsize/reload_solver — no-op stubs (no Python solver to clear/reload); unsat_core — returns []. Without these the SimProc raises AttributeError. Discovered failures during full pytest gate-ON: strncmp.run uses single_valued, memcmp.run uses min_int, default_filler uses simplify. SimSolver._adjust_constraint pattern (SimActionObject unwrap) also needed in add().

posix.dumps(0) under the Rust engine is assembled by _inject_rust_stdin_inner (angr/exploration/rust_callback_dispatch.py), which splices a concrete eval of the state's Rust stdin symbol list into posix.stdin.content. Two invariants any change here must keep (angr-psrxs): (1) the Rust stdin symbol list is CUMULATIVE — a forked child's list already contains every symbol its parent read; (2) a materialized child SimState is a .copy() of the parent's CACHED SimState (parent-root path in rust_state_export._materialize_state), so it starts out already holding the packet Rust injected for the parent. Therefore injection must be idempotent/authoritative, never a blind append: each injected claripy.BVV is tagged with a relocatable _RustInjectedStdin annotation (class defined at top of rust_callback_dispatch.py) and _drop_stale_rust_stdin_packets strips ONLY tagged packets before appending the fresh full packet. Provenance-by-annotation, NOT by byte value (angr-p8jyz iter36): the old manager-wide set[bytes] _rust_stdin_packets dropped any Python-side concrete packet whose bytes collided with a prior eval — e.g. an all-zeros materialization eval put b'0'*N in the set, silently stripping any zero preseed. Annotation survives the SimState .copy() (relocatable=True) so child streams stay correctly tagged. Packets Python itself appended (a bounced SimProcedure reading stdin) are never tagged and survive. Regression tests: tests/engines/rust/test_stdin_dump_forks.py (fork double-count) + test_stdin_packet_provenance.py (collision-by-value drop).

RustExplorationManager test isolation: tests in tests/engines/rust/ share the module-scoped fauxware_project fixture, which keeps the shared Z3 thread-local context alive across tests. After test 1 calls mgr1.run(), the SymContext's solver assertions persist in the Z3 backend in some form — when test 2's mgr2 calls export_state_constraints, it returns a leaked constraint from test 1 ALONGSIDE its own. The BVS variable name changes (fresh-id) but the leaked Bool's structure carries through. Workaround in tests that inspect exported constraints: filter by op AND a unique pattern (e.g. op in gt/lt AND inner add) before asserting per-constraint properties. Naming the BVS uniquely is not enough — angr renames consistently across tests. See TestClaripyAnnotationRoundtrip.test_annotation_on_expression_via_export_constraints for the pattern.

INVARIANT (angr-9ke6b.223): the Z3 term Rust builds for a claripy LEAF must be the same Z3 declaration claripy's own z3 backend builds for it — same name AND same sort. Reason: RustSolverContext::add_constraint_ast (solver.rs) has a raw-passthrough fast path that calls extract_z3_ast_ptr and, if the AST is Bool-sorted, hands claripy's Z3 term straight to ctx.add_constraint_raw, bypassing claripy_to_rustbv entirely. Any leaf reached both ways must therefore agree, or a constraint added through the fast path names a variable the imported leaf does not and silently fails to bind (no error, just an under-constrained model). Verified encodings: claripy BVS('x',1,explicit_name) -> BV(1)-sorted const 'x'; claripy BoolS('x',explicit_name) -> Bool-sorted const 'x'. Z3 treats those as DISTINCT declarations (same name, different sort). Rust has no Bool sort in RustBV, so RustBV::from_parts special-cases the SymbolKind::rust_symbol_name Bool tag and emits Bool::new_const(claripy_name).ite(BV(1,1),BV(0,1)) — the tag is stripped so the constant carries claripy's name, which is exactly what makes the passthrough path bind. Before .223 a Bool leaf became BV::new_const(name,1) and a bare BoolS constraint added via add_constraint_ast never bound at all. Pinned by tests/engines/rust/test_claripy_bridge.py::test_explicit_name_bool_keeps_its_own_identity_across_imports.

RustBV::Symbolic.name is Arc and RustBV::Expression.operands is Arc<[RustBV]> (an Arc-shared inline slice — NOT Arc<[Arc]>). The inner per-operand Arc was removed when Expression operands went inline. Cloning Expression is alloc-free + NO FFI: just an Arc<[RustBV]> refcount bump (the operands themselves are not recursively cloned). Cloning Symbolic is alloc-free but DOES incur ONE z3::ast::BV clone = ONE Z3_inc_ref FFI call (per z3-rs 0.19.7 src/ast/mod.rs:492). Constructor signatures: impl AsRef for names, Arc::<[RustBV]>::from([...]) for operands. Hot path: RdTmp clones on every temp read in a VEX block — but most VEX temps hold Expression (or Concrete/Constrained), not raw leaf Symbolic, so RdTmp clone is dominated by Arc bumps (no FFI). The Symbolic FFI clone cost matters only when volume is high (memory/load.rs measured 2026-06-03 at <0.05% of bench wall-time — see gan1-memory-load-clone-not-hot).

rustbv_to_claripy export (native/angr/src/claripy_bridge/export.rs::rustbv_to_claripy_memo, post zel8z.5 split; was claripy_bridge.rs): when a binary op has claripy Bool operands (length=None, e.g. from Eq/Ult/Sub rebuilt via eq), convert EACH Bool to BV(1) via If(cond,1,0) and FALL THROUGH to the normal op-dispatch match — never special-case which op to call inside the Bool arm. The old code early-returned: (None,None) returned args[0] (dropped op + 2nd operand); (None,Some)/(Some,None) catch-all rebuilt every non-And/Or/Xor op as add (Eq/Ult/Sub silently became additions). Round-trip unit tests live in claripy_bridge::tests (claripy_bridge_tests.rs) and import claripy under Python::attach (skip-if-unimportable); run via 'cargo test --release claripy_bridge::tests::' with venv activated. Test non-vacuity check: a real claripy import makes the test take ~0.1s not ~0.00s. Fixed in angr-c3rd (commit 2c2802180).

RustBV::Expression { id: u64 } is NOT a content hash or interner id. Every Expression constructor sets id = RustBV::EXPRESSION_ID (u64::MAX) sentinel — see symbolic/value.rs:549. Identity for caching is keyed by other surfaces: Arc::as_ptr(operands) for EXPRESSION_BY_OPERANDS_PTR, caller-computed content hash for EXPRESSION_CACHE. Two structurally distinct Expression values share the same id sentinel. Rationale: avoiding per-construction id allocation overhead and keeping the claripy-side registry tracking only real leaf symbols. Anyone touching expression caching MUST NOT rely on the id field for keying.

RustBV IR rewrites can be bypassed: extract_into / truncate_into / extract_no_ctx all exist as ways to construct Extract nodes in value.rs. Only extract_into runs the canonicalization rules (Rule 1-5 at value.rs:1540-1605). truncate_into (used heavily by vex/ops.rs at 309, 356, 3023) and extract_no_ctx (used by arch/mod.rs register slicing) build BVOp::Extract directly. Any IR rewrite that only fires inside extract_into therefore has a coverage gap. The fix from angr-p8cz: add a second hook point at Z3 emission (emit_extract_z3_cached in value.rs) that re-applies the rules. Pattern for future rewrite additions: hook at BOTH construction (extract_into) AND emission (emit_extract_z3_cached) to be self-correcting.

RustBV::Concrete is u128-backed (max 128 bits). Any Python->Rust memory or register sync that takes 'data: &[u8]' and packs all bytes into a u128 via 'value |= (b as u128) << (i * 8)' is BUGGY for data.len() > 16. In release mode, shifts >= 128 mask to 7 bits — bytes 16..31 OR back into low bytes, then store_concrete's page-fill loop replays the same masking, painting a 16-byte-repeating pattern across the claimed width. Found via angr-5aj8 (2026-06-06): baby-re under ANGR_RUST_USE_CALLBACK_MEMORY_PROXY=1 corrupted stack with witness pattern. Safe pattern: split into 16-byte chunks per RustSimState::apply_changes in state/mod.rs (loop 'while offset < bytes.len(): chunk_size = remaining.min(16); ...'). Fixed sites: _set_state_memory_concrete (state_api.rs), _pending_memory_store (pending_api.rs), RustSimState::memory_store (state.rs).

Same width cap applies on the store side generally: store_concrete (memory/store.rs) computes value.to_u128(), and bv_to_bytes/bytes_to_bv (interpreter/helpers.rs) also funnel through u128, so a concrete store wider than 16 bytes (V256/AVX) cannot live in one RustBV. To store wide concrete values, chunk into <=16-byte RustBV writes via SymbolicMemory::store_concrete_le_bytes_automap_internal, which places chunks at endianness-correct addresses (LE: addr+off; BE: addr+(total-off-cs)) so the full-width layout matches a single store. pending_stores hold little-endian value bytes (bv_to_bytes is LE).

REMAINING SITE TO AUDIT (confirmed still present as of angr@152040696, 2026-08-04): the register-write path in RustSimState::apply_changes (native/angr/src/state/mod.rs, 'Apply register writes' loop, ~line 643) still packs bytes into a u128 directly with NO 16-byte chunking — unlike the memory_writes loop immediately below it in the same function, which does chunk. This would corrupt YMM (32B) / ZMM (64B) wide-register writes if StateChanges.register_writes is ever asked to carry them. NOTE: the previously-flagged sibling bug in claripy_bridge.rs's 'bytes_to_u128' (silently dropping bytes above index 16) has SINCE BEEN FIXED — that helper is now extract_int_value in native/angr/src/claripy_bridge/mod.rs, and for integers needing >128 bits it raises BridgeError::InvalidArgs loudly instead of silently truncating (angr-cxw7).

RustBV with width=0 is supported on the concrete path: RustBV::concrete(value, 0) collapses the mask to 0 so any value normalizes to 0; the resulting handle preserves length=0 and is_concrete. The symbolic path (via Z3) would fail since Z3 rejects 0-width BV sorts. Implication: PyO3 callers should not assume create_symbolic(name, 0) is safe — only create_concrete(0, 0) is.

Rustdoc intra-doc links in native/angr/src: a bare [method_name] never resolves — rustdoc only resolves names in the module scope, so associated items need [m](Self::m) or [Type::m]. That was the root cause of all 3 'unresolved link' warnings in angr-9ke6b.225 (has_symbolic on MemoryPage, write_at on FileSystem, set_register_symbolic on PyRustSimState) — the symbols all existed, the paths were just unwritable as bare names. The other 13 warnings were 'links to private item': either a genuinely private helper, or a pub item inside a pub(crate) module (exploration, procedures, solver are pub(crate) in lib.rs; memory/state/symbolic/vex/stash/automaton/concretize are pub). Convention chosen: plain code span, never widen visibility just to make a doc link resolve. Gated since then by the 'Rustdoc link check' step in ci.yml::rust_check (cargo doc --no-deps --all-features under RUSTDOCFLAGS=-D warnings), so this class cannot regrow.

When adding a new field to RustSimStateSnapshot, prefer #[serde(default = "...")] with a free function returning the canonical default over bumping SNAPSHOT_VERSION. Reason: bumping the version (constant in state.rs around the snapshot machinery) invalidates everyone's on-disk snapshot cache and forces re-execution on next pip install. serde defaults achieve forward compatibility (old snapshots restore to fresh defaults) without that pain. Used in angr-rdgs to add cgc_allocation_base + cgc_sinkholes. The default function must be a top-level fn returning the field type (e.g. fn default_cgc_allocation_base() -> u64 { 0xB800_0000 }); attribute path is the function name as a string literal.

z3_saved_check_total (symbolic/stats.rs::get_solver_stats, angr-op0dn.9.5) deliberately EXCLUDES z3_ast_memo_hit. The key aggregates only families that avoid a Z3 check() call — z3_branch_concrete, z3_assume_concrete, zext_cmp_trivial_decide_count, and the three model-hit counters — so every summand is commensurable (one saved check each). z3_ast_memo_hit saves Z3 node construction, not a check, and is an order of magnitude larger; folding it in would drown the check-avoidance signal the key exists to protect. Same distinction the 9.6 census turned on (see invariant-memo-payoff-is-repeats-not-share). If you add a new saved-work counter, put it in this total only if it removes a check().

Scan-cap policy for native SimProcedures (procedures/): a caller-supplied length n that exceeds the module scan cap (MAX_STRING_SCAN / MAX_SCAN = 4096) must NOT be silently clamped -- clamping yields a truncated answer that diverges from libc and the Python engine. Bail with Err(ProcedureError::MaxIterations(n)) so the call defers to Python. Three shapes, pick by whether the capped prefix can pin the true answer: (1) UNCONDITIONAL bail (NativeStrncpy in strcpy.rs; NativeMemrchr in strchr.rs) -- use when no prefix result survives truncation. memrchr wants the LAST match in n bytes, so a match past the cap would override whatever the prefix found. (2) CONDITIONAL on the cap outcome being unobservable (NativeStrncat in strcat.rs) -- scan_concrete_bounded returns (buf, null_found), so it bails only when !null_found; an oversized n whose src terminator lands inside the cap produces exactly the unbounded copy. (3) CONDITIONAL on the prefix pinning the answer (NativeMemchr/NativeRawmemchr in strchr.rs, via helper forward_match_is_conclusive) -- a concrete non-NULL address is the true FIRST match regardless of the unscanned tail, so it stays native; a concrete NULL (absent from prefix) or a symbolic ITE chain (may still be NULL) bails. rawmemchr is always in the capped case since its bound is unbounded; its contract guarantees the byte is present, so 'absent from the first 4096' means past the cap, never NULL. Prefer (2)/(3) when applicable -- they keep the native path for the common case. Delivered by angr-9ke6b.109 (strncat) and angr-9ke6b.108 (memchr family).

scanf.rs::read_format_string (procedures/) delegates to strings::scan_concrete_bounded so memory_load faults propagate as Err (Python fallback) rather than the old 'Err(_) => break' silent-truncation that committed symbolic stores on a corrupted format. read_format_string takes &mut RustSimState now (scan_concrete_bounded needs it; do_scanf already holds &mut). extract_concrete_arg on a symbolic format byte already errored via ? before this fix; only the memory_load-failure path was swallowed.

scanf/printf length modifiers: BOTH consumers must resolve conversion width through LengthModifier::int_conv_bits(arch_bits) in procedures/format_common.rs — parse_scanf_format (procedures/scanf.rs, takes arch_bits) and format_string (procedures/sprintf.rs, reads state.arch().bits() once). Widths mirror format_parser.py int_len_mod's sim_types: hh->8, h->16, none->32, ll/j->64 always (SimTypeLongLong), l/z/t->arch_bits (SimTypeLong / SimTypeLength, so 32 on ILP32 x86/arm32). Two failure modes if this is hardcoded: ScanfSpec.bits drives state.memory_store(ptr, sym_val) (writes bits/8 bytes) and record_stdin_symbol, so an over-wide bits silently clobbers adjacent guest bytes with unconstrained symbols; on the sprintf side an over-wide mask renders %ld of a bit-31-set value as the zero-extended 64-bit number where Python prints the sign-folded 32-bit one. Regression test patterns: assert_scanf_store_width_arch in scanf_tests.rs (pre-fills 8 concrete 0xAA guard bytes, asserts exactly N low bytes symbolic and the rest still 0xAA) and sprintf_one_arch in sprintf_tests.rs; both take an arch string so ILP32 is covered. Fixed in 4a1dcf6fd (angr-vfhyx, hh/h) and angr-9ke6b.111 (l/z/t arch width).

scanf numeric conversions (%d/%i/%u/%x/%o) cannot serve harness-seeded stdin natively: Python's format_parser.py::FormatString.interpret models the parse (reads max_digits stream bytes and constrains each to the ASCII rendering of the stored value, base 10/16/8), so there is no byte-for-byte map from seed bytes to the minted BVS. procedures/scanf.rs::do_scanf therefore defers the WHOLE call to Python when stdin_common::stdin_seed_unconsumed(state) and any spec is numeric — checked BEFORE any memory_store so the Python SimProcedure sees a pristine state (an earlier %s in the same format must not have consumed the seed). %c is the exception: one input byte -> one stored byte, so it goes through mint_stdin_bytes like %s. Corollary invariant: any new native stdin reader either maps the seed byte-for-byte (use mint_stdin_bytes) or falls back — never mint free symbols while a seed is unread. angr-ggb66.

Scheduler serde budget (angr-8shhe): scheduler_worker.rs::offload_is_affordable gates Trigger A load-sharing offloads on SERDE_BUDGET_DIVISOR=4 — migration serde (detach+reattach, timed via detach_timed and the reattach site in dispatch_next) may consume at most 1/4 of the pool's accumulated step_ns. Rationale: a migration is a full Z3 AST round-trip through SMT-LIB2 whose cost scales with the state's CONSTRAINT SET, while a step's cost does not — so no fixed offload rate fits both a solve-heavy frontier (fork_solve_trap: migration is cheap next to the solve it unblocks) and a fat-constraint divergent one (CADET: migration costs more than the step it hands off). Invariants future work must respect: (1) Trigger B (LOCAL_HWM memory cap) is deliberately NOT budget-gated — it bounds per-worker memory and must fire even when serde has blown its budget; (2) both counters start at 0 so the first migrations are always allowed (the budget is unjudgeable before there is anything to measure); (3) the check is pool-wide and monotone by design — a worker cannot know a migration's cost before paying it, and a migration-dominated frontier stays that way. Trigger A now offloads ONE state per starving sibling (not len/2); that also matches record_migration_sample (helpers.rs), which models one steal per dispatch, so honest_steal_fraction still lines up with the gate's f_model.

x86g_use_seg_selector (native/angr/src/vex/ccall/mod.rs, inside handle_ccall_with_ctx) returns a 64-bit value whose LOW 32 bits are the linear address and whose BIT 32 is the error flag. The empty-descriptor-table flat-addressing fast path must compute (seg_selector<<16)+virtual_addr with a mod-2^32 wrap, matching Python's engines/vex/claripy/ccall.py x86g_use_seg_selector which does the add over 32-bit BVs then .zero_extend(32). Doing the add in u64 (the pre-d7f2db812 bug) lets a carry out of bit 31 land on bit 32 and be misread as a bad-selector error — reachable with ANY negative displacement off a segment register (mov %gs:-0x4,%eax => va=0xFFFFFFFC), not just exotic inputs. General lesson: when porting a claripy-BV computation to Rust u64, the BV width IS part of the semantics; any place the native path widens the arithmetic can leak a carry into a neighbouring ABI field. Pinned by test_use_seg_selector_gdt_empty_wraps_mod_2_32 in vex/ccall_tests.rs. Also noted: Python's own bad() builds BVV(1<<32, 32), which claripy truncates to 0 before zero_extend — the native path deliberately returns the ABI-correct 1<<32 instead of mirroring that upstream quirk.

SegmentList (native/angr/src/segmentlist.rs) is a RangeMap keyed by address, so getitem is an O(idx) ordinal walk, NOT O(log n) — rangemap exposes no positional index. Never call it in a loop over consecutive indices; that is how _nodecode_bytes_ratio in cfg_fast.py became O(n*k) (angr-9ke6b.200). Use SegmentList::iter_backward_from(addr) for the search-then-walk-backwards pattern: it yields the segment search(addr) names plus every earlier one in descending address order, snapshotted in one O(idx) pass, and yields nothing when addr is past the last segment (mirroring search -> None). Residual: the snapshot is unbounded, so a caller needing only k segments still pays O(idx) clones; measured 5.4x over the indexed form at n=16000 rather than the ~k-fold an early-stopping lazy iterator would give. A lazy version was rejected — a pyclass iterator cannot borrow the map, and re-querying via RangeMap::overlapping(..).next_back() re-pays an O(n-idx) skip per step.

Selection-seam order-determinism contract (angr-op0dn.10.5, single-worker only). Two chokepoints decide dispatch order: SelectionPolicy::select (only pop site, run_loop.rs) and SelectionPolicy::on_fork (only push site, via helpers.rs::push_to_active_or_drop -> StashManager::push_active). Invariants any new policy MUST hold: (1) terminate the ranking key with the front index i so ties break by insertion order; (2) on_fork push_back so deque order is a pure function of forks_out Vec order from core_outcome_handlers.rs; (3) NEVER iterate the per-policy HashMap/HashSet fields (CoverageGuided::seen, FindDirected::seen, LoopHeadRoundRobin::dispatched, DirectedCfgDistance::{distances,dispatched}) — only get/contains/entry. Rust HashMap seeds a fresh hasher per INSTANCE, so a single 'for (k,v) in map' in a select path makes dispatch order vary run-to-run within one process. Guarded by test_selection_trace_deterministic_across_runs in selection_policy.rs: a scripted fork program driven through both hooks, 7 built-in policies x 3 repeats, each repeat rebuilding the policy (fresh hasher seed) and comparing the label trace; test_selection_traces_differ_across_policies keeps it from passing vacuously. Contract does NOT extend to the parallel scheduler — steal order is design-nondeterministic, contract there is set-equality.

The fetch-page servable-page filter (angr-gorvf.4.6) must NOT be a blanket 'decline everything natively' — that is unsound. RustStateSyncMixin._sync_extra_python_pages has a zero_eager_cap=200: when a state has MORE than 200 all-zero pages it deliberately leaves them ALL lazy (the mma_howtouse path, angr-9maq — eager-mapping 2000+ zero pages per state x 45 short-lived states blew RSS to 1.9GB). Python CAN serve those lazy zero pages, so Rust must keep crossing for them. Two further conservatism rules baked into _install_python_servable_pages: (1) a page whose fast classifier verdict is None (not a 4096-byte UltraPage — e.g. page_no 1024, the binary base, on every AMD64 bench measured) is kept SERVABLE so it keeps crossing, rather than disabling the whole snapshot; the first draft bailed out of the snapshot entirely on such a page and the filter silently never installed; (2) under ZERO_FILL_UNCONSTRAINED_MEMORY, Python synthesizes a zero page for ANY address, so no finite set describes what it can serve — skip the snapshot altogether.

python_servable_pages (angr-gorvf.4.6) is a FETCH oracle, NOT a load oracle — do not reuse it to decide whether Rust may serve a load natively. It answers 'could _cb_fetch_page hand back concrete bytes for this WHOLE page'. Two page classes are declined by it yet answer a memory_load perfectly well, and treating a decline as 'Python has nothing here' silently fabricates symbols over real data: (1) a page holding SYMBOLIC bytes is declined for a concrete page fetch but loads fine from its symbolic data (the field's own doc comment in callbacks/mod.rs already warned: 'must never be turned into a native zero-fill: these pages carry symbolic stdin'). Caught by tests/engines/rust/test_error_stash.py::test_dcas_cmpxchg16b_no_python_fallback — the DCAS compare went symbolic and rust_store_stmt_count fell to 0. (2) a LOADER-BACKED page is served straight from the CLE backer; angr materializes it into state.memory._pages only on first touch, so an untouched loader page is absent from _pages. Caught as a stable 27% csgames2018 regression (0.96s -> 1.22s): the fabricated symbols turned concrete loads symbolic, which dragged in z3 time (397->543ms) and SimProcedure bounces (0->430ms). The load-side oracle is the separate python_page_universe (angr-gorvf.4.7): state.memory._pages UNION every page of the loader lazy_regions. Both sets fail OPEN (predicate returns true when no snapshot is installed) and are skipped entirely under ZERO_FILL_UNCONSTRAINED_MEMORY, where Python answers with zeros rather than a symbol. Anchors: PythonCallbacks::python_can_serve_page vs ::python_has_page (callbacks/dispatch.rs), VEXInterpreter::synthesize_unservable_load (interpreter/mod.rs), RustExplorationManager::_install_python_servable_pages (angr/exploration/rust_manager.py).

RustSimState::set_register (in state/registers.rs, moved from state/mod.rs main impl block by god-object decomp angr-0mqkc.5; originally state.rs split into state/ dir module, angr-zel8z.1) historically did NOT sync self.pc — only registers.put_reg. set_ip/set_pc sync both, but set_register did not. The RustRegisterProxy write-through gate writes the IP via set_state_register_symbolic_ast -> set_register('rip'), so pc diverged from the rip register (pc stale/0, rip correct), causing get_state_pc_by_id()=0 and 'Lift error at 0x0' while the full-export path masked it (reads rip into state.addr). Fixed 2026-06-13 (angr-4rq7, commit 8c29a17de): set_register now re-syncs self.pc when name's offset == arch.ip_offset(). INVARIANT: any Rust path that writes the IP register by name must keep self.pc consistent. Reads (get_state_register vs get_state_pc_by_id) were already consistent — the bug was write-side.

Native SimProcedure dispatch is now ONE fn: exploration/native_proc_dispatch.rs::dispatch_native_proc (angr-ph300.73, commit e3a59dec9). Both callers consume it -- step_one's hook arm (run_loop.rs) and handle_simprocedure_core (core_outcome_handlers.rs). NativeProcDisposition + NativeProcCounters + segfault_message live in native_proc_dispatch.rs too; core_outcome_handlers re-exports segfault_message under #[cfg(test)] so core_outcome_tests' 'use super::handlers::segfault_message' still resolves.

TWO deliberate caller-parameterized divergences -- do NOT 'simplify' them away without a behavior review:

1. mirror_segfault: only the core/parallel path terminal-errors a STRICT_PAGE_ACCESS unmapped-page fault natively (NativeProcDisposition::Segfault). step_one passes false and still bounces to Python via the ordinary fallback counters. Unifying is a real behavior change.
2. The SubCall (ProcOutcome::CallAndResume) counter bump is NOT done inside dispatch_native_proc -- core bumps native_calls/call_counts the moment call_ex returns, step_one only once setup_native_subcall succeeds (and books a python_fallback + other_fallbacks_by_name on failure). Both preserved by leaving the bump caller-side.

The LANDING (return-reg write, PC/SP) also stays caller-owned on purpose: step_one resolves the return address via the calling convention (get_return_addr + pops_return_addr, so ARM/ARM64/MIPS LR/X30/$ra work) while the core path is handed return_addr by the interpreter.

Borrow gotcha in step_one: the registry entry must be .cloned() (cheap Arc) before calling, because the dispatcher needs &mut self.profiling.native_proc_stats alongside it.

Rust unit tests that need claripy's Z3 context (the shared-context handshake rust_manager.setup_shared_z3_context does in production) CANNOT run under libtest's default multi-threaded runner. engine.rs::install_shared_z3_context sets a THREAD-LOCAL context from Python's z3.main_ctx() pointer, but the effect is process-global in practice: libtest gives each test its own thread, and a test that installs Python's context races the Rust-owned thread-local contexts sibling tests build. Two observed failure modes: (1) all 5 tests installing it -> SIGSEGV on the test binary; (2) only one installing it -> the rescued constraint intermittently lands where the state's own solver never sees it, so an UNSAT state reads SAT (~1 run in 3, reproduced by pairing sync_constraints_fp_rescued_via_z3_pointer with sync_constraints_typed_convert_binds_constraint). Pattern: keep such a test but mark it #[ignore = "...needs --test-threads=1"] with the run recipe in its doc comment; tests that only need claripy_to_rustbv (no raw Z3 pointer crossing) must NOT install the context -- they are stable in parallel because their ASTs are built in the thread's own Rust-owned context. See sync_constraints* in exploration/helpers_tests.rs.

Test setup gotcha (rust-symex): RustExplorationManager built from angr.load_shellcode + proj.factory.blank_state does NOT propagate Rust-side register/memory writes back to the Python state after run. Tests using state.regs. or state.memory.load() to verify Rust execution semantics will read the pre-run Python values. Two paths that work: (1) use a real binary + factory.entry_state(), or (2) verify execution via mgr.stats counters with profiling enabled — rust_step_count > 0, rust_stmt_count > 0, rust_store_stmt_count for store-fired-N assertions, dcas_unsupported_count for fallback regression. This bit the angr-ufez DCAS test design — initial attempts to verify cmpxchg16b semantics via state.memory and state.regs all returned the original Python values regardless of what Rust did. The two DCAS tests now use counter assertions + Python-side memory unchanged checks (which DO work, since they verify the absence of writes).

sign_extend_to (symbolic/value_ops.rs, private free fn feeding RustBV::sign_extend_into) had a (1u128 << to_width)-1 overflow at to_width==128: SIGABRT under panic=abort, silent zero-extend in release (shift wraps mod 128 -> mask collapses to 0). Guest-reachable via any signed widening to 128 bits (MullS64 etc). Fix: saturate the to-mask to u128::MAX when to_width>=128 (from_width<to_width guarantees from_width<128 so the 1u128<<from_width shifts stay safe). GOTCHA that hid it: boundary_sign_extend_matches_reference used sign_extend_to as its OWN reference (tautological) — regression test sign_extend_to_128_matches_i128_reference instead compares against the independent sign_extend i128 helper. When width-parameterized folds have >=128 boundary cases, the reference in the test must be a genuinely different code path, not the same helper.

BVOp::SignExt(n) and BVOp::ZeroExt(n) in native/angr/src/symbolic/value.rs encode the NUMBER OF BITS ADDED, not the target width. For 'sign_extend_into(target_w, ctx)' on a value of width w, the resulting expression carries op=SignExt(target_w - w). Tests asserting on the discriminant must use the difference (e.g. ashr by 4 on a 32-bit value extracts 28 bits then SignExt(4), not SignExt(28)).

rust_engine.rst SimOption coverage matrix is now guarded by TestRustSimOptionMatrixConsistency (tests/engines/rust/test_misc.py): it parses the rst list-table rows, classifies each by status-cell text ('raise NotImplementedError' / 'explicitly reject'), and asserts doc-raise == _RAISE_OPTION_NAMES exactly and _REJECTED_OPTION_NAMES subset of doc-reject. Extra doc-reject rows are allowed ONLY if the option is in angr.sim_options.modes['symbolic'] (default bundle, warn-on-read via _RustOwnedSimStateHistory, e.g. TRACK_CONSTRAINT_ACTIONS/TRACK_MEMORY_MAPPING). When you add/remove a member of either frozenset in rust_manager.py, update the matrix row's status text in the same commit or this test reddens.

self.call() continuation push is LOST in the Rust callback path unless the grown stack region is captured. Root cause: angr SimProcedure.call() runs cc.setup_callsite on a COPY of the executing state (sim_procedure.py), so the continuation return-address store bypasses CallbackMemoryTracker (rust_identity.py) which only wraps the TRACKED state's memory.store. For zero-length hooks not in _MEMORY_WRITING_PROCS (e.g. pthread_once), _snapshot_orig_state returns a register-snapshot dict -> is_snapshot=True -> _extract_memory_changes is SKIPPED -> only tracked_writes used -> continuation push never reaches Rust. sp still rides in via reg_changes (it's a register diff), so the callee frame gets correct sp but a STALE return slot -> ret jumps to a stack address -> deadend. Fix (commit 165195ca4): _resume_with_state captures the grown region [succ_sp, orig_sp) from any Ijk_Call successor and adds to mem_changes; _snapshot_sp (rust_state_sync.py) reads sp from a SimState or snapshot dict. This is the correct replacement for the removed _push_continuation_address, which double-decremented sp. Diagnostic: cross-engine stack dump at the init-routine entry (PROBE_DUMP_REGS in tools/xmllint_probe.py) - Python [rsp]=continuation addr (0x33000xx), broken Rust=garbage stack ptr. DO NOT manually re-push the continuation in rust_callback_dispatch.py: the former _push_continuation_address (removed iter35, commit 6fbf0bf0e) ALSO re-decremented sp -> callee stack off by 8 -> ret pops garbage -> deadend. Removing that double-push fixed sp but left the return slot stale (still deadended) until the grown-region capture above landed. The earlier claim that 'the push is captured by the callback memory tracker' was FALSE (iter36 correction) — setup_callsite runs on a state COPY, bypassing CallbackMemoryTracker, and register-snapshot mode skips the mem diff, so the continuation VALUE was lost entirely (only sp rode in via reg_changes). __libc_start_main avoids all this via the native Rust procedure (libc_start_main.rs).

When SimProcedures return a value via cc.teardown_callsite -> SimRegArg.set_value, and the return type is smaller than the full register (e.g. int return in rax/eax pair), set_value emits TWO stores: state.registers.store('rax', 0) (clear) then state.registers.store(offset_of_eax, val, size=4) (sub-reg). Any plugin that caches register values per-name (RustRegisterProxy) must invalidate overlapping aliases or the parent register reads stay stale. Caching by integer offset alone is not sufficient — partial writes leave the parent name cached.

SimState plugin presence check: state.plugins is a DICT (returns _active_plugins, sim_state.py::plugins property), NOT a PluginHub. To test whether a plugin is registered WITHOUT triggering auto-instantiation, use state.has_plugin(name) (SimState.has_plugin) or 'name in state.plugins'. NEVER use hasattr(state, name) — PluginHub.getattr auto-instantiates a factory-default plugin on the probe, so hasattr is ALWAYS True (this made _restore_plugins_to_state's guard vacuous, angr-9cjmg). And do NOT write state.plugins.has_plugin — 'dict' has no such method; the AttributeError gets swallowed by surrounding try/except and silently copies nothing.

GAP-6 zero-length-hook skip tokens are a true LIFO stack, not a set. Consumption lives in ONE place: RustExplorationManager::consume_skip_hook (exploration/pending_api.rs), called from step_one in run_loop.rs. It expires stale entries (expiry <= steps) then pops only the topmost match via rposition+remove. Do NOT reintroduce a retain()-based removal there: _set_skip_hook_addr pushes without dedup, so nested zero-length hooks at the same PC hold multiple tokens, and a blanket retain collapses them all at once, leaving the second occurrence unskipped and re-arming the infinite loop GAP 6 prevents (angr-9ke6b.47). _clear_skip_hook_for_addr intentionally KEEPS clear-all semantics -- it is an explicit Python-side reset, not a consumption. A non-empty skip_hook_stack also forces must_run_serial (angr-04tw3.1), since no parallel path consumes it.

skip_hook_stack (zero-length/stale-hook anti-loop, RustExplorationManager::mod.rs) is populated by Python set_skip_hook_addr (rust_callback_dispatch.py) but READ/CONSUMED in exactly ONE place: run_loop.rs step_one's GAP-6 block, reached ONLY by the single-threaded loop. parallel_process_state runs run_interpreter_step_core with skip_addr=None. Invariant: any parallel/steady path must fall back to serial while skip_hook_stack is non-empty, else a resumed state re-fires the same hook -> callback->resume->callback loop with no path-side break. Enforced in must_run_serial() (angr-04tw3.1, commit 086308458), alongside the native-technique and find/avoid-predicate serial carve-outs. skip_hook_stack is populated between run_loop() calls (one callback returned to Python per call), so the entry-point gate is the correct chokepoint.

PARALLEL SNAPSHOT INVARIANT (angr-op0dn.13.10): the wave path parks bounce states OUTSIDE every stash. process_parallel_bounce_queue (run_loop.rs) surfaces at most one need_callback event per run() and stores the undispatched rest in RustExplorationManager::pending_parallel_bounces — a Vec<(RustSimState, BounceKind, u64)> that is in NO stash. StashManager::dump_snapshot only serializes stashes, so any snapshot taken while bounces are parked silently loses those states AND their whole subtree; stash_counts() and the active-PC fingerprint both look healthy because the parked states were never counted. Symptom: an in-memory resume reaches every leaf while a snapshot resume of the same frontier reaches far fewer (pbounce synthetic, workers=4: 8/8 in-memory vs 3/8 from the snapshot). FIX: dump_snapshot_bytes calls flush_parked_bounces_to_active (run_loop.rs), which set_pc's each parked bounce to bounce_target_addr(kind) (Hook / SimProcedurePython entry — the state is parked AT the call site with the callback not yet run, so re-entry is a faithful replay) and route_successor's it back to active. SAME SHAPE for live steady parallel sessions (angr-op0dn.13.6): under RUST_PARALLEL_STEADY the frontier is resident in worker Z3 contexts and belongs to NO stash, so dumping StashManager mid-session silently truncates the search (snapshot looks valid, resumes with a smaller frontier). Fix: RustExplorationManager::dump_snapshot_bytes (manager_methods.rs) takes &mut self and calls steady_config_guard(); Python dump_snapshot calls _finalize_parallel_session() first. RULES for future work: (1) any NEW pymethod that reads self.sm must call the steady guard — reading self.sm without it is the silent-data-loss shape; (2) any manager-level Vec/Map that holds owned RustSimStates outside self.sm (pending_parallel_bounces, pending_callbacks) is invisible to the snapshot — a new one MUST either be serialized or flushed into a stash by the dump guard, next to steady_config_guard.

Snapshot dump/load must be SYMMETRIC on the finalize contract. dump_snapshot_bytes (manager_methods.rs) calls steady_config_guard() + flush_parked_bounces_to_active() before serializing self.sm; load_snapshot_bytes (angr-ph300.21) must equally steady_config_guard() and clear pending_callbacks / pending_parallel_bounces / current_stepping_state_id BEFORE swapping self.sm. Otherwise the next run() finalizes the OLD steady session into the RESTORED stashes (two explorations merged) and a parked need_callback can resume a discarded pre-load state. Any future field added to the parked/pending set (things referencing live/worker states outside a stash) must be cleared here too. Regression: test_load_snapshot_clears_parked_pending_callback in test_manager_core.py parks a callback via symbolic SimProc arg then asserts pending_callback_ids() empty post-load.

Snapshot restore and the global state-id counter (angr-op0dn.13.14, commit 3ab14cfce): RustSimState::from_snapshot imports state_ids minted under a FOREIGN counter epoch, but NEXT_STATE_ID (state/mod.rs) is a process-global AtomicU64 starting at 0. A cold-resumed manager's counter sits at ~1 (its throwaway seed state), so its first fork re-minted an id that was live in its own restored stashes -> silent clobber of StashManager's state_index/state_roots and the Python shadow maps, violating the documented state-id-never-reused invariant. fork_with() only asserts monotonicity under debug_assert, so release builds never caught it. Fix: from_snapshot calls state::reserve_state_id(id) (fetch_max). Same bug class one level up from the SymContext::next_id fix (13c50741c) -- when auditing snapshot code, check EVERY global monotonic counter for restore-epoch awareness. NOTE: this did NOT move the .13.14 leaf count (cold resume still 6/8), so it is a latent-correctness fix, not that bug's root cause. Pinned by Rust test test_from_snapshot_reserves_foreign_state_id.

RustSolverContext owner-thread teardown (angr-87e56): close()/drain_solver_graveyard can free an owned fork ONLY on its owning thread (SolverInner is non-Send). All six Python fork_state_solver holders are instrumented via _release_owned_ctx/del (RustSolverProxy, RustSolverProxyPlugin, the ~1226 proxy, RustPosixProxy._eval_stdin finally, RustStateExportManager.del, _shared_solver_ctx). RESIDUAL (angr-87e56.1): a context forked ON a worker thread during a Python callback under RUST_PARALLEL_WORKERS>1 can NEVER be dropped after the worker pool joins — pyo3 emits the leak-safe 'is unsendable, but dropped on another thread' warning when a later GC drops the shell off-owner. Diagnostic signature: 0 warnings per parallel-worker test FILE run alone, but 1-2 when several run in one process (non-deterministic GC frame). CORRECTION (iter 53): the scheduler-drain fix is IMPOSSIBLE — see [[pyo3-unsendable-drop-content-independent]]. pyo3 can_drop warns on the shell regardless of payload; real fix is Python-side: don't cache forks created off the coordinator thread. Bead angr-87e56.1 downgraded P4 (benign leak-safe warning).

RustSolverFallback.attach() (angr/exploration/rust_state_export.py) must REFRESH the already-bound instance on re-attach, not no-op. It patches eval/min/max/satisfiable onto state.solver and caches a forked Rust Z3 ctx. _sync_cached_state re-attaches routinely for the SAME state_id after Rust steps further (_invalidate_state_export_cache clears rust_fully_synced). The old idempotent _ATTACH_FLAG guard left the original instance (with a stale _cached_rust_ctx forked BEFORE the extra stepping) bound → progressively staler wrong-answer solves that silently violate Rust-side constraints invisible to the Python mirror (see invariant-mirror-solver-constraints-not-authoritative). Fix: attach() stores the live instance under _INSTANCE_ATTR and, on re-attach, calls _rebind_for_resync(state_id) which releases+nulls _cached_rust_ctx and rewinds _synced_constraint_count to _initial_constraint_count so caller Python constraints re-replay onto the fresh fork. Regression: tests/engines/rust/test_solver_fallback_resync.py (angr-hv4lt.9).

RustSolverContext.pop()/pop_to_level() panic-safety (angr-ph300.48): a bare pop() reaches SymContext::pop -> scope_savepoint_pop, whose None-lineage branch calls z3::Solver::pop(1) which PANICS on under-pop (abort/PanicException from Python). Fix = SymContext::try_pop() (transaction_ops.rs) returning bool: refuse only when lineage is None AND bare_z3_push_depth()==0. Must be lineage-AWARE: bare_z3_push_depth (lineage_ops.rs) counts ONLY None-branch pushes; the Some (shared-lineage) branch records on scope_savepoints and already IGNORES mismatched pops harmlessly, so a depth-only guard would wrongly refuse legit Some-branch pops. pymethods pop()/pop_to_level() now return PyResult and raise PyValueError. Internal _with_extra_constraints (rust_state_proxy.py) is always balanced, unaffected.

RustSolverProxyBase.min/max width>128 big-int fallback (_resolve_none_extremum) must be fed the SAME constraints the primary Rust min/max path saw on the FORKED context, not export_state_constraints (state-only). Standalone RustSolverProxy.add() is VIEW-LOCAL (writes only to _solver_ctx, never the state), so state constraints miss them — it tracks adds in _added_constraints and overrides _fallback_constraints() to union them. RustSolverProxyPlugin.add() is WRITE-THROUGH (add_constraints_to_state), so its self.constraints already reflects adds and it uses the base _fallback_constraints() default. Any new solver-proxy op that re-derives constraints for a claripy fallback must go through _fallback_constraints(), not self.constraints. See invariant-rust-solver-fallback-class. Fixed angr-hv4lt.5.

solver.rs unwrap/expect deny-lint is REAL & enforced, not aspirational doc. Inner attr #![deny(clippy::unwrap_used, clippy::expect_used)] at solver.rs top-of-module fires as a hard compile error under clippy (proven by probe injection into SolverInner::ctx). CI enforces via ci.yml 'cargo clippy --all-targets --all-features -- -D warnings'. Same deny is present in 10 more py-boundary/exploration-hot-path modules: state/export.rs, exploration/{run_loop,manager_methods,state_api,resume,pending_api,state_id,state_lifecycle,stats_api,event}.rs. Reviewed exceptions use scoped #[allow(..., reason=...)] (e.g. SolverInner::i use-after-close). To re-verify any module: inject a throwaway .unwrap() and run clippy --lib.

arch alias tables: 'sp'/'bp' are the ARCHITECTURE-INDEPENDENT full-width stack/base pointer on every arch, NOT the legacy 16-bit x86 sub-registers. archinfo: AMD64 sp=(48,8) bp=(56,8); X86 sp=(24,4) bp=(28,4). Rust's amd64.rs/x86.rs ALIASES had them at 2 bytes on the same offset, so RustSimState.set_register('sp', full_width) silently truncated to the low half (angr-6qzik, fixed 2026-07-22 commit 609f7a7da). The legacy 16-bit sp/bp are now unreachable by name — deliberate, archinfo cannot express them either. The SIBLING 16-bit aliases (ax/bx/si/di) DO keep 2-byte widths; archinfo agrees. Same family as invariant-ip-is-pc-not-r12: generic register-name aliases follow archinfo, not the per-ISA ABI reading. Pinned by the 'aliases' column of ARCH_EXPECTATIONS in native/angr/src/arch/mod_tests.rs, swept by test_all_arches_resolve_their_alias_spellings (angr-9ke6b.215 folded the old per-arch test_sp_bp_aliases_are_full_width copies in amd64_tests.rs/x86_tests.rs into that table), and by the now-empty KNOWN_DRIFT in tests/engines/rust/test_arch_offset_parity.py.

Sphinx is NOT installed in the angr venv and cannot be added because the venv pip is broken (see avoid-pip-install-broken-venv). For docs builds, install outside the venv (e.g. pipx install sphinx or python3 -m pip install --user --break-system-packages sphinx furo) then run 'cd docs && sphinx-build -W -b html . _build/html'. Acceptance criteria that mention 'sphinx-build warning-free' need this workaround.

Proxy fast-path pattern in RustExplorationManager filter()/move()/drop() (post angr-9jly, 2026-05-22): each predicate-path stash operation must (1) construct RustStateProxy(self._rust_mgr, state_id, self._project, python_mgr=self), (2) call filter_func(proxy) inside try/except (AttributeError, TypeError, NotImplementedError), (3) fall through to _snapshot_to_angr only on those three exception types. Other exceptions reraise into the outer try-block that keeps the state on error. ALL three (filter/move/drop) now follow this exact shape — if you add a new predicate-style stash op, mirror it. Tests asserting isinstance(s, RustStateProxy) live at tests/engines/rust/test_solver_output.py near test_prune_with_filter_func.

StashManager has two remove-by-id helpers with distinct contracts (stash.rs): take_state(id) resolves via state_index then falls back to an all-stash scan and RELOCATES from wherever it finds the state — used by out-of-band step_state; take_state_from(id, stash) is stash-SCOPED, returns None (does NOT relocate) if the state lives elsewhere, unindexes on success, and leaves ROOT bookkeeping to the caller. Root handling is caller-specific and must not be baked into the helper: drop_state_from_stash clears the root (state gone for good), _move_state preserves it. _merge_states forks in place (sources survive for Python _merge_drop) so it uses find_state (index fast-path) not take_state_from. Single-sourced in angr-ph300.27; before that these were 4 open-coded loops, merge's being O(states^2) and index-blind.

After angr-kwpi.2, mgr.active/found/etc return _LazySimStateRef wrappers (angr/exploration/rust_state_export.py). Accessing ANY non-private attribute via the wrapper goes through _materialize_single_state, which calls _sync_cached_state if rust_fully_synced is False. This means: after mgr.step(), reading wrapper.scratch.X re-syncs the cached SimState and re-sets rust_fully_synced=True. To observe the stale/cleared sentinel state, peek at mgr._state_cache[state_id] directly. Tests that asserted post-step sentinel-cleared invariants via the wrapper must inspect _state_cache instead — see test_state_export_cache_invalidated_on_step for the pattern.

Stat-family arch coverage is defined in exactly one place: write_stat_for_arch in native/angr/src/syscalls/file_path.rs (5 arms: AMD64/ARM64/X86/ARM/MIPS32). Each handler's own guard then narrows it: NativeStatSyscall and NativeLstatSyscall reject ARM64 (its asm-generic ABI has no legacy stat/lstat number, only newfstatat 79), so they are AMD64+X86+ARM+MIPS32; NativeFstatSyscall and NativeNewfstatatSyscall accept all 5. The 32-bit arches reach the writers via their LFS *64 syscall numbers (i386/ARM 195/196/197, MIPS32 4213/4214/4215/4293); the legacy pre-LFS numbers (i386 106/107/108, MIPS32 4106/4107/4108) are deliberately left unregistered in syscalls/mod.rs because their old struct-stat layout has no writer. When adding an arch or a stat-shaped syscall, update write_stat_for_arch AND the module doc block in file_path.rs together — the angr-9ke6b.151 audit found three module-doc blocks still claiming 'AMD64 only' long after four arches were wired.

invariant-state-cache-mirror-id: RustExplorationManager._state_cache is NOT a bijection — one Python SimState frame can legitimately land under several Rust state ids (successive callbacks along a lineage reuse the same frame via _resume_with_state; the symbolic-branch fork path caches parent_state.copy() under each new child id). Because RustRegisterProxy binds ._state_id at sync time, syncing a SHARED frame in place silently rewrites what every other id sees (this was angr-ibx8j: mgr.active[i].addr reported a sibling's pc). INVARIANT: every write into _state_cache must go through RustStateExportMixin._cache_state_mirror, which stamps scratch.rust_mirror_id = state_id and clears rust_fully_synced; every read path that syncs (_materialize_single_state) must de-alias by copying when scratch.rust_mirror_id != the id being materialized. Do NOT add a raw self._state_cache[id] = state assignment — it reintroduces the alias.

_state_cache pinning rule (angr-qm7w, 2026-05-08): _cleanup_state_cache must always pin (a) every root state in self._state_roots.values(), (b) self._current_callback_state_id and its effective ID via _get_effective_state_id, and (c) self._current_stepping_state_id. Without those pins, plugin mutations made in one callback would not be visible to the next callback on the same state — the post-callback cache write would survive cleanup but the in-flight pin protects the freshly-mutated state from racing eviction. _max_state_cache_size = 8 (was 500). Cleanup is called from _dispatch_callback exit.

Endness invariant: every Arch impl in native/angr/src/arch/ hardcodes is_little_endian() -> true, including the bi-endian ARM/ARM64/MIPS32/MIPS64. It is NOT the authoritative byte order for a state. The real one is RustSimState::is_little_endian() (state/memory.rs, reads SymbolicMemory::endness), seeded by RustSimState::with_solver_endian from the little_endian override that angr/exploration/rust_manager.py computes off project.arch.memory_endness. Any code whose result is observable state behaviour (SimProcedures, syscalls, memory encoding) must use the state accessor. angr-9ke6b.1 fixed two such sites: host_network_swap (procedures/byteorder.rs, backs htonl/htons/ntohl/ntohs) and NativePipe (procedures/fileops.rs) -- both were silently wrong on BE ARM/MIPS. CallingConvention::endness (arch/calling_conventions.rs) still returns a hardcoded Endness::Little for MIPS but currently has no consumers outside its own tests; if one appears it needs the same treatment.

Audit of state_id-keyed Python caches for the stale-serve-after-Rust-steps shape (angr-qwyti.10). Full inventory of caches keyed on state identity that could serve stale data after Rust advances the same state_id: (1) RustRegisterProxy._cache — fixed angr-4rq7, cleared+rebound in _sync_rust_registers_to_state; (2) RustSolverFallback._cached_rust_ctx — fixed angr-hv4lt.9, _rebind_for_resync on re-attach; (3) RustCallStackProxy._frames_cache — fixed angr-qwyti.10, now reads live. All OTHER caches are NOT this shape: _z3_ptr_cache (keyed on immutable claripy AST ptr), _loader_pages_cache (project/binary pages, immutable), _reg_offset_cache (arch-static), _init_cache/_disk_key_cache (binary digest), _mem_cache (consume-once). Memory/callstack PROXY PLUGINS installed on materialized states (RustMemoryProxy, RustCallStackProxyPlugin) are minted FRESH per _sync_cached_state and read live, so no persistence. CONCLUSION: a dedicated epoch/generation counter is unnecessary — the de-facto generation guard already exists: _invalidate_state_export_cache() clears the rust_fully_synced sentinel on every cached state on each Rust step, and re-materialization re-runs _sync_cached_state (single chokepoint) which rebinds/clears the two materialized-path caches. INVARIANT for future caches: any new state_id-keyed cache on a materialized-state plugin must be cleared/rebound inside _sync_cached_state; any lightweight-view sub-proxy must read live, not cache.

INVARIANT (angr-r4r7, 2026-05-10): Rust state IDs are monotonically allocated and never reused. Once a state ID is absent from every Rust stash (active|found|avoid|deadended), it is unreachable forever. This is what makes it safe to drop Python-side shadow mappings keyed by state_id (_state_roots, _predicate_matched_ids, _py_state_options, _py_state_globals) inside _cleanup_state_cache (rust_manager.py:2980). Future shadow structures keyed by state_id should follow the same pattern: prune against any_stash in _cleanup_state_cache rather than inventing per-structure LRU caps.

RustSolverProxy.timeout setter writes BOTH to the underlying state's SymContext (via mgr.set_state_solver_timeout) AND to the proxy's already-forked solver. This dual write is needed because: (1) future forks of the same state must inherit the new timeout (the fork copies timeout_ms via Atomic), and (2) the cached proxy solver — already forked when the user did proxy.solver. earlier — would otherwise keep the old value. The state's solver context is reachable through find_state which covers both stash states and pending callback state.

invariant-stateset-content-eq: StateSet (native/angr/src/automaton/state.rs) must NEVER #[derive(PartialEq, Eq, Hash)] — the derive delegates to FixedBitSet, whose own derives include the length/capacity field alongside the data blocks (verified on the pinned fixedbitset 0.4.2 that Cargo.lock resolves, despite Cargo.toml asking for 0.5). with_capacity(16)+insert(3) then hashed != singleton(3,100), so identical NFA subsets would mint duplicate DFA states in subset_construction. Fixed in angr-9ke6b.180: manual impl PartialEq comparing bits.ones() iterators, and impl Hash writing len() first (prefix-freedom) then each member. Same trap applies to any future wrapper over FixedBitSet or any container whose backing type stores a capacity — do not trust derives there. Note subset_construction still keys its IndexMap on to_vec(); that stays because the DFA inverse state mapping needs the Vec form anyway, not because Eq is still broken.

The steady parallel loop's SteadyOutcome::Budget arm (run_loop_steady.rs::steady_pump / run_loop_parallel_steady) is reachable from Python ONLY via the address-based full-batch path with a step budget: RustExplorationManager._explore_with_addresses keeps frontier residency ON only when until is None and no techniques are active, so any 'until' predicate silently drops you out of steady mode. The way to drive repeated budget yields in a test is a LOOP of mgr.explore(find=..., max_steps=1) calls, not one explore with a small max_steps (that is a single run()). Each such call yields once through Budget -> finalize_steady_session -> session re-creation. Observable via the parallel_steady_budget_yields stat (added angr-ph300.14); assert on it, since without it a test can pass by exiting the pump through Quiesced/Bounces instead. Also: bounce_queue is provably empty at steady_pump's loop top (every arm that pushes returns in the same breath), so the old '&& bounce_queue.is_empty()' budget guard was dead and is now a debug_assert.

The RustExplorationManager config mutators that touch worker-snapshotted state MUST call steady_config_guard() FIRST so a live steady parallel session is finalized before the snapshotted view goes stale. As of angr-9ke6b.53 the guarded set is: add_hook, add_hooks, register_simprocedure, register_simprocedures, unregister_simprocedures, set_deterministic, set_vex_opt_level, set_solver_timeout, set_os_name, set_max_active_states, set_find_addrs, and the other set_/register_ in manager_methods.rs. clear_hooks is currently UNGUARDED (no known live-session caller). Without the guard a mid-session add_hook leaves workers stepping the stale hook set (new hook silently never fires) and set_deterministic only reaches stashed states, not resident/parked frontiers. set_max_active_states is the subtlest case: ensure_steady_session (run_loop.rs) hands the cap to RunSession::new_with_policy ONCE for the session's whole life -- unlike the wave loop's per-wave rebuild -- and a steady session never rounds its frontier through STASH_ACTIVE, so an unguarded mid-session change was invisible to the live frontier while get_max_active_states reported the new value. steady_config_guard is defined in run_loop.rs (z3 variant finalizes; non-z3 is a no-op stub). Regression coverage: run_loop_tests.rs::config_mutators_apply_and_are_guard_safe_without_session pins the no-session path for each guarded setter.

finalize_steady_session (native/angr/src/exploration/run_loop_steady.rs) takes() the SteadySession out of self.parallel_session BEFORE draining worker Paused acks. Any early return from the drain loop therefore drops sess -- and with it every residual already received, sess.shared's counters, and sess.prof -- because the routing + fold block sits AFTER the loop. angr-e4cys fixed the Timeout arm to break-and-salvage; keep that shape: never return Err from inside that while loop, set a flag and surface it after the fold. Drain deadline comes from steady_finalize_deadline(solver_timeout_ms) = max(2x timeout, 60s), because scheduler::CancelToken is task-boundary-only and cannot interrupt a worker mid-Z3-solve.

Steady-session counter folding (angr-offd5): a RustExplorationManager steady session stays LIVE across every need_callback return, so finalize_steady_session is NOT the only fold point — run_loop_parallel_steady calls fold_steady_counters_incrementally before each mid-session event return. Repeat folding is safe BY CONSTRUCTION, not by accident: both halves of fold_parallel_shared_counters are M2 (shared.stepped.swap(0) + mem::take of shared.counters), so a second fold with no worker activity contributes 0. Any new accounting added to ParallelShared MUST use the same swap/take shape or it will double-count across the incremental folds. Separately, ParallelShared::root_map is only partially prunable: route_steady_terminal removes the routed terminal's OWN entry (safe — a terminal never re-enters a worker under the same id, and a re-injected bounce is re-stamped by steady_inject_resumed), but Continue successors' entries must be retained for the session lifetime since nothing signals when a subtree finishes; they are freed when the session drops.

thiserror conversion in Rust engine (commit 923c3a6ca, 2026-05-01): 10 of 11 manual error enums converted to thiserror derives. StepError in exploration/stepping.rs deliberately left as a non-thiserror enum because it carries RustSimState as a control-flow signal (Deadended/NeedCallback/Unconstrained variants) rather than as a true error — RustSimState has no Display impl. ProcedureError keeps a manual From impl that stringifies via to_string() (changing this to #[from] would change the wire format of the error message).

When monkey-patching SimulationManager.step (or any method that may be hooked by ExplorationTechniques), use types.MethodType(func, manager) to produce a bound method. ExplorationTechnique.use_technique calls HookSet.install_hooks which wraps the current step in a HookedMethod. HookedMethod.call does 'current_hook(self.func.self, *args, ...)' — accessing self on a plain function raises AttributeError('function object has no self'). This breaks any solve.py that calls simgr.explore(find=..., avoid=...) (Explorer technique). The error surfaces in subprocess as 'function object has no attribute self'.

Under the Rust manager, a step_state() ExplorationTechnique hook that delegates to simgr.step_state(...) DECLINES rather than raising. dispatch_step_state_with_hooks (angr/exploration/rust_techniques.py) swaps the RustSimulationManagerProxy base step_state for a _declined_base that raises the internal _StepStateDeclined sentinel BEFORE HookSet installs technique hooks, so the sentinel unwinds the whole composed chain. Consequence: for Tracer and Slicecutor the technique's pre-delegation side effects run (Tracer: self.predecessors, state.globals, RepHook install; Slicecutor: nothing) and everything AFTER the simgr.step_state call -- the actual trace enforcement / slice pruning -- never executes; the state is then advanced by a plain native run(). A hook that raises for any other reason is caught and only l.warning'd ('step_state() hook raised ...; leaving it in place'). Net: these techniques SILENTLY DIVERGE under Rust, they do not fail loudly. Only a technique that computes its own successor dict without delegating (Veritesting, via its nested Python SimulationManager) actually APPLIES. Do not document or rely on a NotImplementedError here.

_step_state (exploration/stepping.rs) error arms must park their RustSimState in STASH_STEP_OUT before returning Err, never drop it. The NeedCallback arm originally returned PyNotImplementedError while dropping the PendingCallback (freeing pending.state) — a silent frontier loss: state in no stash, not in pending_callbacks, unrecoverable. Fix parks pending.state via index_state(id, STASH_STEP_OUT) + ensure_stash().push_back before raising. Rule: any new StepError arm in _step_state must extract its state and park it (Deadended/Error/Unconstrained already do). Recover parked ids with get_state_ids('_step_out').

E1.a step_state() design (native/angr/src/exploration/stepping.rs::_step_state, pymethod in manager_methods.rs): out-of-band single-state stepping does NOT auto-stash. Successors/terminals are parked in the _step_out quarantine stash (stash.rs::STASH_STEP_OUT, created on demand and deliberately NOT in STANDARD_STASHES — putting it there made restore_from_snapshot pre-create it and broke the stash-shape round-trip test; ensure_stash exempts it from the typo warn instead). Buckets: 'flat' for live successors, else the destination stash name. Two knobs added to the step core: step_state_inner(extra_stops, terminal_sink) — extra_stops are unioned into the CLONED StepContext.stop_addrs so they apply to one call only; terminal_sink diverts apply_core_outcome steps 5-6 (pruned + side-effect terminal pushes) to the caller so the run() path's stash mutations are not double-applied. StepError::NeedCallback raises NotImplementedError (E1.b owns the callback protocol). Caller places states with move_state(id, '_step_out', ...).

The deferred-fork materialization logic exists in FOUR intentionally-distinct variants (2 sequential x 2 profiling levels), and the fork counters do NOT tally uniformly across them: (1) fork_materialize::materialize_deferred_forks (exploration/fork_materialize.rs) — the full-profiling materializer used by resume.rs (3 callback-resume sites) and run_loop_single.rs. Per-fork solver_fork_time_ns/solver_fork_count + solver_sat_* + a batch deferred_fork_time_ns/deferred_fork_count timer. Only variant that calls reconstruct_deferred_fork_condition when the condition is absent from stored_conditions. (2) core_outcome_handlers::materialize_deferred_forks_core — parallel-scheduler mirror of (1) via ParallelProfiling::add; stored conditions ONLY, no reconstruct fallback. (3) SimulationLoop::process_deferred_forks_into (exploration/stepping.rs) — the simpler helper used by SimProc-native resume, SymbolicJumpTarget, P21 generic skip. Bumps deferred_fork_count only; tallies NO solver forks on either branch. (4) core_outcome_handlers::process_deferred_forks_into_core — parallel mirror of (3). Functionally equivalent for correctness; do NOT unify without an explicit decision (would either lose profiling or add it everywhere). solver_fork_count therefore has exactly THREE tally sites: (1), (2), and SimulationLoop::dispatch_bounce's BounceKind::Hook arm (the pre-callback state-snapshot fork before bouncing to a Python SimProcedure — NOT a deferred fork). The no-condition conservative state.fork() in (1)/(2) DOES clone a solver but is never tallied, so deferred_fork_count and solver_fork_count are siblings, not sub/superset (see also avoid-early-return-on-empty-deferred-forks). run_loop.rs no longer mentions deferred forks at all — pre-angr-nbim4.3 citations pointing there are stale. Doc comments on both counters live on the stats-macro fields in interpreter/mod.rs and were re-anchored to these symbol names in angr-9ke6b.86 (commit 5b2c58432).

SymbolicMemory store_concrete has TWO independent overwrite-cleanup obligations at the same base address, and they are easy to fix in only one branch (this is exactly how angr-9ke6b.95, .98 and angr-7qon each arose). Whenever a store overwrites a base that already holds a wider tracked object, the ABANDONED TAIL [addr+size, addr+old_size) must be retired in BOTH sidecars: (1) symbolic_spans entries naming (base, old_width) — a load that follows one into an out-of-range extract returns MemoryError::SymbolicAddress 'symbolic bytes not fully tracked', i.e. a readable byte becomes a hard error, not a silently wrong value; (2) the page symbolic_bitmap bits, which page.store_concrete only clears inside [0, size). The symbolic branch also has to clear pre-existing multi_objects cells first (angr-9ke6b.95). Chosen semantics for the tail is RECLASSIFY AS CONCRETE (the wider tracking is already lost; page data bytes were never touched by mark_symbolic), consistent across both branches. Use SymbolicMemory::clear_symbolic_bitmap_range (memory/store.rs) for the bitmap half — it walks page boundaries, so never inline a single-page clear_symbolic call. Must run BEFORE the symbolic branch's page-cloning mark loop, which would otherwise flush a stale bitmap back over the clear.

VEXInterpreter::get_return_addr (interpreter/simprocedures.rs) must mirror load_concrete_addr's buffer precedence: pending_symbolic_stores, pending_stores, all_flushed_symbolic_stores, all_flushed_stores, then calling_convention.get_return_addr. Since angr-ofyh symbolic stores push NO zero-placeholder bytes into the concrete buffers, so any fast path that consults only the concrete maps is blind to a symbolic value at that address and silently answers with stale pre-write bytes. Any other [sp]/address peek added to the interpreter needs the same four-map ladder. A symbolic hit returns None (as_u64()) — matching what CallingConvention::get_return_addr already yields for a symbolic [sp].

handle_storeg (native/angr/src/interpreter/statements.rs) originally reimplemented store dispatch inline and skipped code-cache invalidation + overlapping-symbolic-shadow eviction (the angr-slbsd/srk4b/vvzf5/02jwz fix cluster). Fixed angr-myzjx.26: unconditional guard arms (symbolic always-true, concrete-true) now route through shared store_value() helper in statements_store.rs (try_rust_memory_store then fallback_to_python_store — same as IRStmt::Store); symbolic-guard ITE arms keep load-current/ITE build but call invalidate_and_evict_concrete_store (concrete addr) or invalidate_code_on_store before the concretization match (symbolic addr, mirrors handle_symbolic_store). INVARIANT: any new manual store dispatcher must go through store_value or invalidate_and_evict_concrete_store, never raw pending_stores.push/call_memory_store, or SMC + overlap-load soundness breaks. The old clone also had two latent bugs now gone: always-true guard + symbolic address silently dropped the store, and concrete-data + symbolic-address hit call_memory_store(0,..) with a hard-coded address 0.

strcmp/memcmp return-value convention in the Rust engine (angr-e71o4 + angr-u8gm8): BOTH the concrete path (procedures/strcmp.rs::compare_bytes' ConcreteStep::Stop closure) and the symbolic path (strcmp.rs::build_diff_chain) return the SIGN -1/0/1, never glibc's raw byte difference. build_diff_chain emits ITE(c1 <u c2, -1, 1) per position. This covers five procs at once (strcmp, strncmp, strcasecmp, strncasecmp, memcmp) because both helpers are shared -- memcmp.rs calls compare_bytes with stop_at_null=false. TRAP for future parity work: there is NO convention that matches every Python proc. angr/procedures/libc/memcmp.py uses ite_cases over BVV(-1)/BVV(0)/BVV(1) (matches us), but angr/procedures/libc/strncmp.py's non-static symbolic path constrains ret_expr to 0 or 1 and NEVER yields a negative value. We deliberately follow memcmp.py and internal consistency; do not 'fix' the symbolic strcmp path to 0/1 to chase strncmp.py. Comparison is UNSIGNED (ult) because C compares as unsigned char, and for strcasecmp the case fold happens BEFORE the sign is taken ('D' vs 'b' must be +1, not -1 from 0x44 <u 0x62). Regression pins live in strcmp_tests.rs (symbolic_pinned_result helper, byte pairs >1 apart so a raw-diff regression shows as +/-2) and memcmp_tests.rs::test_memcmp_symbolic_byte_solver_evaluation.

Strict-deterministic mode (angr-op0dn.10.x) originally canonicalized only SymContext::eval (unsigned-min) and eval_upto (ascending prefix). The MULTI-PART eval paths were missed and stayed nondeterministic until angr-op0dn.10.7: SymContext::eval_wide (single wide BV, read straight off an arbitrary Z3 model) and SymContext::eval_many (backing RustSolverContext::eval_batch). Those two are exactly what a USER's post-exploration eval hits: RustSolverFallback._rust_eval (angr/exploration/rust_state_export.py) sends any expr wider than 64 bits through a byte-Extract decomposition into eval_batch, so posix.dumps(0) / solver.eval(x, cast_to=bytes) on an exported found state got an arbitrary witness even in strict mode. Fix: SymContext::lex_min_witness minimizes parts in order with each earlier part pinned (bsearch_min + assert equality inside one push/pop scope) — one assignment, canonical. min_wide byte-splits big-endian so eval_wide is canonical at ANY width, unlike min() which reports None above 128 bits (angr-cxw7). Lesson: when adding a canonical-witness rule, sweep EVERY eval entry point in solving_ops.rs, not just the single-BV one.

angr-lf108 fix: try_detect_stride (native/angr/src/concretize.rs) sampled-GCD stride can exceed the true stride, so the Strided grid {base+i*stride} silently EXCLUDES feasible addresses; downstream ITE load/store builders assume the grid is complete → wrong reads/dropped writes. FIX: new helper stride_grid_excludes_feasible does ONE SAT check can_be_true((addr-base)%stride != 0). This is COMPLETE (not just heuristic) because base=true min: any off-grid feasible addr in [min,max] must be off-stride — an on-stride addr past the last grid cell would exceed max. When SAT, return None → caller emits TooLarge. Without vex-engine-z3 feature, can_be_true is conservatively true (disables abstraction, safe). detect_stride_from_solutions (within-limit path) was already sound via expected_count==len check.

SchedulerCounters::record_summaries (native/angr/src/exploration/scheduler.rs) has FOUR per-disposition split slots, not three: Avoided is reachable in-worker because parallel_process_state (run_loop.rs) matches a successor pc against ctx.avoid_addrs before the coordinator's avoid-routing ever sees it. Any new TerminalDisposition must get its own slot AND a fold in fold_scheduler_dispatch_stats (helpers.rs) into the matching sm.*_count, or parallel runs under-report vs serial (worker-count variance). Note the split only restores COUNT parity — the summarized states themselves are dropped in-worker, so mgr.avoid/deadended stash CONTENT is still parallel-vs-serial divergent.

Symbol ids (RustBV::Symbolic id, minted by SymContext::next_id) MUST be unique per PROCESS, not per SymContext. The maps that resolve an id back to its claripy AST / name / width -- symbolic::registry::GLOBAL_REGISTRY, reached from claripy_bridge export -- are process-global and outlive a manager. Before angr-op0dn.13.16 next_id was a per-context AtomicU64 starting at 0, so a SECOND exploration in one process minted ids the first's symbols still owned; an exported symbol then resolved to a stranger's claripy AST. Symptom: the pbounce synthetic drained 14 dead paths cold and 16 warm (aliased symbols collapse a compare-and-branch to a CONCRETE guard, so IRStmt::Exit stops/starts forking with no visible error). Fix: process-global NEXT_SYMBOL_ID in symbolic/bv_id_ops.rs (reserve_symbol_id / symbol_id_watermark), mirroring state-id-never-reused on NEXT_STATE_ID. Snapshot restore fetch_maxes past the captured watermark instead of pinning. Same bug class as angr-op0dn.13.14 (resume scope). Any future id-keyed process-global map must respect this.

Rust symbol identity across the Python bridge is by NAME, not by id. RustBV::from_parts builds a leaf's Z3 term from its name (BV::new_const(name,width) for a bitvector leaf; since angr-9ke6b.223 a name carrying the SymbolKind::rust_symbol_name Bool tag decodes via symbolic/registry.rs::strip_bool_symbol_name to Bool::new_const(claripy_name).ite(1,0) instead). So two RustBV::Symbolic values sharing an id but carrying different name strings are DIFFERENT variables to Z3 — while looking identical at the RustBV/export layer (export keys its claripy cache by id). That gap caused angr-izov2: claripy.BVS(name, w) renames to name_ unless explicit_name=True, so a Rust-minted leaf (stdin_N_i from procedures/read.rs) exported to a SimProcedure and returned came back with the right id and the WRONG name; every constraint on the original leaf silently stopped binding and the find gate constrained a detached expression (models were all-zero stdin that never reached the target). Fix, in two parts: claripy_bridge/export.rs's Symbolic branch registers the minted AST via store_claripy_ast_with_info under the RUST name AND (angr-9ke6b.222, commit c43565e29) mints it with explicit_name=True so the claripy name IS the Rust name — see invariant-export-mints-with-explicit-name for why that second half matters even though the registration already covers the happy path; claripy_bridge/import.rs::import_symbolic_leaf rebuilds a by-id hit under the canonical name from the registry map rust_id_to_name (symbolic/registry.rs::lookup_name_by_id). COROLLARY of identity-by-name: leaves that deliberately share a name (mem_ for uninitialised memory, ite_default) are already one Z3 variable no matter how many distinct rust_ids they hold. INVARIANT for any future work: never construct RustBV::symbolic_with_id with a name that differs from the one the id was registered under — and note the registered name is the TAGGED one for Bool leaves, so always go through SymbolKind::rust_symbol_name before touching the registry.

SymbolicIdentityRegistry (native/angr/src/symbolic/registry.rs) has NO garbage collector: retain() still has no production caller, but as of angr-9ke6b.222 (commit c43565e29) wiring one to an APPROXIMATE active set is no longer unsound. Dropping a still-reachable id now costs object identity + any annotations on that leaf, nothing more: export mints with claripy.BVS(name, width, explicit_name=True), so a registry miss re-mints under the same Rust name and RustBV::from_parts rebuilds the SAME Z3 constant (see invariant-export-mints-with-explicit-name and invariant-symbol-identity-is-by-name). Before that flag the miss produced name__ -- a brand-new unconstrained variable no constraint bound (angr-izov2 failure mode, silent) -- which is why angr-9ke6b.40 originally ruled the approximate set out. The only production mutation today is the wholesale reset_for_new_exploration clear at exploration start; growth within a run is surfaced by maybe_warn_growth (one-shot at 100k/1M live symbols since angr-9ke6b.224 dropped the useless 10M step -- ~17 GB at the measured per-entry cost; CAS-guarded, re-armed by clear) and by the symbol_registry_size / symbol_registry_registrations keys of mgr.stats (a @property, NOT a method -- invariant I10; PROCESS-GLOBAL, not per-manager -- see avoid-id-keyed-global-symbol-cache). The memory/fidelity trade was MEASURED AND DECLINED in angr-9ke6b.224 (commit 9762c17d6) -- see symbol-registry-memory-cost for the numbers and the two constraints any future GC must respect. A real GC must also clear the thread-local claripy_bridge::cache at the same quiescent point, or a cached RustBV::Symbolic whose entry was collected exports a stale AST.

The symbolic identity registry (symbolic/registry.rs) keys name_to_info with qualified_key(name, width, kind) = "{bv|bool}:{name}_w{width}" — the SymbolKind sort tag was added in angr-9ke6b.38 because claripy's BoolS imports at a hardcoded width of 1, so BVS(name,1) and BoolS(name) with explicit_name collided and the second import aliased to the first's rust_id, making export hand back the wrong-sorted claripy AST. Any new registry writer/reader must pass the right SymbolKind. Since angr-9ke6b.37 BOTH import-side arms funnel through one helper, claripy_bridge/import.rs::import_symbolic_leaf(ast, ast_hash, name, width, kind, ctx) — the BVS/BoolS match arms only supply width+kind, so the hash -> name+width+sort -> mint sequence exists in exactly one place; keep it that way (the .38 fix previously had to be applied twice). The remaining BitVector writer is export.rs's Rust-minted-symbol arm. The .38 residual (registry separated IDENTITY only, both leaves still built BV::new_const(name,1) so they were one variable to Z3) was CLOSED by angr-9ke6b.223: import_symbolic_leaf now applies SymbolKind::rust_symbol_name to the name BEFORE every registry call, and RustBV::from_parts decodes that tag into a Bool-sorted Z3 constant. See invariant-rust-z3-encoding-must-match-claripy.

Symbolic clz/ctz/popcount export from Rust->claripy MUST be tied to the operand AST, not a fresh BVS. claripy_bridge/export.rs::build_sound_bitcount (post zel8z.5 split; was claripy_bridge.rs) emits a sound encoding for width<=64: nested If(Extract(i,i,operand)==1, count, ...) for clz (LSB->MSB so MSB test is outermost) and ctz (MSB->LSB so LSB test is outermost); popcount is sum of ZeroExt(w-1, Extract(i,i,operand)). Result width == operand width (matches the concrete BVV(result,width) fast path). width>64 keeps the fresh-BVS fallback (record_export_unconstrained_clz). Pre-fix a fresh unconstrained BVS per call meant Python-side eval could return Rust-infeasible values AND identity was unstable. See angr-acoq.

symbolic/context.rs is in 'pub mod symbolic' which is NOT feature-gated in lib.rs (unlike claripy_bridge, memory, interpreter, procedures which are all #[cfg(feature='vex-engine')] gated). This means anything in context.rs that references vex-engine-only deps (thiserror) or vex-engine-z3-only fields (solver, timeout_ms, sat_cache, etc.) MUST have its own #[cfg(feature=...)] gate. When adding new functionality to context.rs, check the gating: thiserror requires vex-engine, z3 types require vex-engine-z3.

RustBV::Symbolic{id} export identity: the exporter (claripy_bridge/export.rs rustbv_to_claripy_memo) resolves a Symbolic via get_claripy_ast(id) with NO width check, so any two Symbolic BVs sharing an id alias to the SAME claripy AST on export. NEXT_SYMBOL_ID (symbolic/bv_id_ops.rs) starts at 0, so id 0 is a real allocatable id -- never hardcode id:0 for a minted symbol. Any code building RustBV::Symbolic must allocate a fresh id via ctx.next_id() (== SymContext::next_id, the global NEXT_SYMBOL_ID). Fixed set_register_symbolic (state/pymethods.rs) in angr-ph300.50; set_register_symbolic_ast is still the identity-preserving path (routes through claripy_to_rustbv).

SymbolicMemory::fork() must clone (not share-by-reference) every mutable per-state field. As of 2026-05-05 the fields are: symbolic_objects (HashMap), next_sym_id, default_permissions, endness, dirty_pages (reset to fresh), lazy_regions (Vec), symbolic_spans (HashMap), pending_writes (Vec), zero_fill_unconstrained, imported_addrs (HashSet), enforce_permissions, plus pages (OrdMap COW). memory::tests::test_fork_* asserts isolation for symbolic_spans, imported_addrs, pending_writes, enforce_permissions. If a new field is added to the SymbolicMemory struct, copy it in fork() AND add an isolation test (parent-then-child mutation pattern) — otherwise child mutations leak into siblings.

angr-9ke6b.228 (commit e21ae07ff): SymbolicMemory::load and SymbolicMemory::store -- the two ctx-taking public entry points in memory/load.rs and memory/store.rs that concretize a symbolic address themselves -- have NO production callers; only memory/tests/{basic,symbolic}.rs call them. Every production path (interpreter, procedures, state) enters via load_concrete* / store_concrete* / store_with_concretization instead. Consequence: any instrumentation or invariant placed on those two wrappers is dead in production. That is how mem_lazy_page_fault_count stayed 0 -- both its bump sites lived there, and the store-side one was doubly dead (store_concrete has no lazy classification, so it never yields UnmappedPageInRegion). Fix pattern: put such counters on the producers of the error. The four producers of MemoryError::UnmappedPageInRegion are unmapped_page_error and assemble_load_with_multi (load side), check_pages_mapped_lazy and install_multi_for_candidates_safe (store side). Note this counts faults raised, including ones a caller swallows (load_concrete_or_unconstrained). Contrast the volume counters mem_load/store_count, which live on load_concrete/store_concrete and DO tick -- see invariant-mem-counter-two-paths.

UltraPage.store's symbolic branch does DEAD WORK during a Rust dirty-page replay, and that — not the AST width — was the 8us/entry cost angr-gorvf.11 removed (commit 887282ccb). Every symbolic store re-derives the range it must clear with two SortedDict irange walks over page.symbolic_data plus a SimMemoryObject wrap. During a replay the clear is pointless: RustStateSyncMixin._blit_concrete_page has just zeroed symbolic_bitmap across all 4096 bytes, so NO pre-existing symbolic_data entry is reachable by a load (loads consult the bitmap first), and Rust's symbolic_objects_iter list IS the page's complete symbolic state. RustStateSyncMixin._blit_symbolic_page therefore rebuilds page.symbolic_data as a fresh SortedDict in one pass. INVARIANT it must respect: it is ONLY correct when the concrete blit actually ran for that page (the 'blitted' flag) — that is what makes the stale symbolic_data unreachable — and it must decline straddling/bad-width entries BEFORE mutating the bitmap. MEASURED on csaw_wyvern: 8107 entries over 48 pages, sym replay 66.8 -> 8.6ms. Also measured, killing the bead's own hypothesis: the objects are NOT already wide (6399 of 8107 are 1 byte, 1316 contiguous runs) — but coalescing them with Concat is unnecessary, the per-entry overhead was never the AST.

Native SimProcedures returning a symbolic result must return at arch.bits() width (state.arch().bits()), not at any intermediate width. The concrete path used RustBV::concrete(val, bits) with bits=arch.bits(). Symbolic path must zero-extend the predicate/byte to the same width to keep CFG/register sync invariants intact.

When porting libc SimProcedures from concrete-only to symbolic-arg support, share the ITE-chain construction helpers across siblings (e.g. strcmp/memcmp/strncmp share compare_bytes). Build the chain right-to-left so earlier positions take precedence. The standard pattern: walk byte-by-byte with concrete fast path that short-circuits; switch to ITE-mode the first time a symbolic byte is seen (skipping prior concrete equal positions, which contribute nothing). For strcmp/strchr where a concrete null terminator stops the scan, you can still stop scanning past a concrete null in symbolic mode — positions after the null can never affect the result. Place pub(super) on shared helpers so sibling modules can import via super::sibling::helper.

invariant: a callback's register writes reach Rust ONLY via rust_state_sync.py::_extract_register_changes. Its 'if new_val.symbolic:' branch used to sync the AST only when reg_name was in return_regs (eax/rax); symbolic writes to ANY other register fell through with no else and were SILENTLY DROPPED (fixed d84344559, angr-5rjbq). This is why flareon2015_5's hooks (state.regs.ebx/ecx = ADDR_PW_ENC, where ADDR_PW_ENC = ebp-0x70004 is SYMBOLIC because blank_state leaves ebp unconstrained) never reached the native encoder. Same family as invariant-dirty-pages-survive-migration: a Python->Rust delta channel that silently discards part of the delta. Fix syncs all regs in the arch reg_map; non-return regs gated by _symbolic_reg_changed (AST hash diff) so untouched symbolic regs aren't re-exported every callback. Rust side needed NO change: pending_api.rs::_set_pending_register_symbolic_ast -> state.set_register(name, bv) is already generic by register name.

Symbolic store/load forwarding in the VEX interpreter (native/angr/src/interpreter) has a soundness invariant fixed in angr-ofyh (commit 5c4974162): the buffered fast path must NOT push bv_to_bytes(bv) into the byte-indexed pending_stores for symbolic data — bv_to_bytes yields all-zeros for symbolic values, so an offset load inside the store would silently return concrete 0. Three coupled pieces enforce it: (1) handle_concrete_store symbolic branch only inserts into pending_symbolic_stores (no zero push); (2) evict_overlapping_symbolic_stores drops symbolic shadows from BOTH pending_symbolic_stores and all_flushed_symbolic_stores whenever a concrete store overwrites their byte range (else a later load returns a stale symbolic value); (3) symbolic_overlap_load (expressions.rs) handles offset/overlap loads into a wider symbolic store via low-bit extract (byte k = bits [k8,k8+8)), guarded by map.is_empty() so the all-concrete hot path pays nothing. load_concrete_addr precedence is unchanged: pending_sym exact -> pending_sym overlap -> pending concrete -> flushed_sym exact -> flushed_sym overlap -> flushed concrete; eviction maintains the invariant that no concrete store coexists with an overlapping symbolic entry. EVERY insert site into pending_symbolic_stores must call evict_overlapping_symbolic_stores first: statements_store.rs (handle_concrete_store + buffer_store_for_rust_memory, angr-vvzf5) AND cas_store_symbolic_data in statements_cas.rs (concrete-addr/no-callback branch, angr-myzjx.27 — the last un-evicted clone site). Limitation: eviction is whole-entry, so a concrete store partially overlapping a symbolic store drops the entire symbolic value (no byte-level merge). UPDATE (angr-9ke6b.19, commit 69c0ef344): cas_store_symbolic_data's concrete-addr/no-callback branch is now reachable only for CONCRETE data_bv — a symbolic value there hard-errors via reject_symbolic_byte_store before the pending_symbolic_stores insert. The evict-first requirement on that site still holds (the insert still runs, just with a concrete BV). See invariant-no-zero-fill-symbolic-store.

ultrapage's symbolic_bitmap (angr/storage/memory_mixins/paged_memory/pages/ultra_page.py) is a bytearray of ONLY 0x00 (concrete) or 0x01 (symbolic) values — set via b'\0'*size or b'\1'*size in store(). This means '1 in sb' is the correct fast-path check for 'has any symbolic byte'. Don't substitute 'any(sb)' (truthiness loop) or '0xFF in sb' — both are wrong or much slower.

SymContext now has TWO Arc<Vec<...>>/Mutex<Vec<...>> shared/local pairs: z3_assertions_shared/local (cached Z3 Bool for solver replay) and assumed_constraints_shared/local (RustBV tracked for Python export). On fork() both freeze parent's local into shared (Arc::clone if local empty, otherwise merge into new Arc). Transaction rollback uses parallel push_local_cache_lengths and push_assumed_local_lengths stacks to restore both locals. Readers (get_assumed_constraints, assumed_constraint_count, solver materialization) must walk both shared.iter().chain(local.iter()). Pre-existing quirk: transaction_commit only pops push_constraint_counts, NOT push_local_cache_lengths or push_assumed_local_lengths — likely a pre-existing bug but out-of-scope to fix.

SymContext::push() is solver-only and is NOT cache-aware. assume_true/false caches the constraint into z3_assertions_local UNCONDITIONALLY, but push()/pop() only manipulate the Z3 solver level — the local cache survives a pop. This means: an assume_*() inside a push frame leaks into the cache permanently. fork() captures the cache (not the live Z3 frame), so a snapshot taken inside a pushed frame includes the pushed constraints. The block-level branch feasibility code (interpreter/statements.rs:330-358) relies on this: it pushes once per block, accumulates fork constraints inside the push, snapshots inside the push (which therefore captures cumulative prior fork constraints), then pops at block end. transaction_begin/commit DO track local cache lengths for proper rollback, but plain push/pop do not.

x86/amd64 symbolic ccall flags (native/angr/src/vex/ccall/x86_symbolic.rs) are COMPLETE as of angr-9ke6b.219 (commit d8ef908d2): sym_flags_for_category has a builder for all 13 non-Copy OpCategory variants and its match is deliberately exhaustive (no '' arm); SymFlagsError lost its Unsupported variant and now only carries CopyHandledByCaller. The eflags_c symbolic-CF arm in ccall/mod.rs handle_ccall_with_ctx is likewise exhaustive and routes Adc/Sbb/Shl/Shr/Rol/Ror/Umul/Smul through the shared builder (.ok().map(|f| f.cf)) instead of re-deriving per-category carry formulas. INVARIANT: adding a new OpCategory must fail to compile until it gets a symbolic builder — do NOT restore a wildcard arm or an Unsupported variant, because after angr-9ke6b.88 a decline routes to Python at ~30x wall-clock (see ccall-fallback-perf-gap-method). TESTING GOTCHA: the diff_fuzz_sym_flags* tests feed CONCRETE RustBVs, so RustBV constant-folding answers them and Z3 never sees the expression — for builders that create unusual sorts (sym_flags_umul/sym_flags_smul widen to a 2*nbits = 128-bit product at nbits=64) add a symbolic-operand + ctx.eval round-trip test as well (sym_flags_wide_mul_roundtrips_through_z3 in vex/ccall_tests.rs).

RustStateSyncMixin (angr/exploration/rust_state_sync.py) has TWO per-arch register tables that must BOTH list every 'Supported' arch, or SimProcedure register writes are silently dropped on Python->Rust sync-back: _get_reg_map_and_return_regs (offset/size map + return_regs) and _get_arch_register_names (names for export_callback_bundle). Missing arch => _extract_register_changes returns [] after only l.warning('Unknown architecture ...'), so e.g. $v0/$v1 return value is lost. MIPS32/MIPS64 were absent until angr-hrcds (fixed 7d89be669). Offsets are the VEX guest layout — ground-truth them against archinfo arch.registers[name], never hand-guess; MIPS GPR file is contiguous (MIPS32 base 8/stride 4, MIPS64 base 16/stride 8). Sibling of invariant-symbolic-register-writes-sync.

Synchronous Rust→Python callbacks (_cb_memory_load/_cb_memory_store/_cb_fetch_page/_cb_memory_load_batch/_cb_memory_store_batch/_cb_batch_fetch_pages/_cb_memory_load_symbolic_full/_cb_memory_store_symbolic_value/_cb_memory_store_symbolic_full) fire from INSIDE _rust_mgr.run() which holds &mut self on the PyCell. Under ANGR_RUST_USE_CALLBACK_MEMORY_PROXY=1, the cached state's memory plugin IS a RustMemoryProxy (cache pollution after SimProc completes — line 1301 in rust_callback_dispatch.py: self._state_cache[state_id]=succ_state, where succ_state inherits the proxy). Calling state.memory.load/store on a proxy invokes self._mgr.get_state_memory_ast/set_state_memory_concrete — same PyCell, fails with PyBorrowError 'Already mutably borrowed'. Async callbacks (_dispatch_callback → _handle_simprocedure_callback) DON'T have this issue because run() has already returned by then. Detect via type(plugin).name == 'RustMemoryProxy' (avoid circular import at module top). Fix in angr-hcok commit 710b22efd: loads synthesize filler BVS, stores no-op (Rust already wrote), fetch_page declines so Rust uses its own page source.

sync_constraints_from_python (exploration/constraint_sync.rs) has TWO SAT gates, P12 and P14, and P14 is unreachable under the vex-engine-z3 feature: P12 SAT-checks unconditionally and returns Ok(false) on UNSAT, so by the time control reaches P14 (which re-checks only when failed_count>0 && success_count>0) the state is already known SAT. P14 is defence-in-depth for a build where P12's check is compiled out -- do not write a test that claims to distinguish them. sync_constraints_partial_failure_unsat_is_pruned (helpers_tests.rs) pins the OBSERVABLE contract (partial conversion + contradictory constraints => Ok(false) => resume.rs prunes), not which gate fires.

Native syscall handlers receive args from extract_syscall_args (fn in exploration/helpers.rs), NOT extract_procedure_args (sibling fn in the same file). The two differ on amd64 starting at the 4th arg: syscall ABI uses r10, SystemV (procedure) uses rcx. This matters for any handler with num_args() >= 4 — e.g. rt_sigaction's 4th arg sigsetsize comes from r10, matching the kernel ABI. The legacy comment in syscalls/mod.rs that referenced extract_procedure_args was stale and has been corrected (the module doc now says the dispatcher uses extract_syscall_args). Why: the 4th-arg ABI mismatch is silent; if someone copies a procedure's arg-extraction pattern into a syscall handler, args[3] reads the wrong register and the handler appears to work for low-num_args cases. How to apply: when adding any new native syscall, num_args() returns the argc, and the dispatcher (the syscall-handler arm in exploration/stepping.rs, where handler.num_args() feeds extract_syscall_args) hands you args[] indexed by syscall ABI position. (Symbol-anchored 2026-06-25 iter51: prior raw line refs helpers.rs:576 / stepping.rs:153 had drifted to :796 / :271 — see refactor-memory-sweep-rule.)

Native syscall byte caps: every handler that bounds a concrete byte count before falling back to Python MUST source it from syscalls/mod.rs::MAX_IO_SIZE (4096), not a local literal. Convention is an alias-import so each call site keeps its own vocabulary: read.rs 'MAX_IO_SIZE as MAX_READ_SIZE', write.rs 'as MAX_WRITE_SIZE', cgc.rs 'as MAX_CGC_BYTES' (transmit/receive/random), startup.rs 'as MAX_GETRANDOM'; fd_io.rs uses the bare name and applies it PER SEGMENT for readv/writev. angr-myzjx.18 established this for read/write/fd_io; angr-9ke6b.157 swept in cgc/startup, which had independently redefined 4096 and would have silently desynced on a cap bump. New handlers: alias, don't redefine.

Native syscall fallback-on-collision pattern: when Rust semantics can't faithfully reproduce a Python error path, return SyscallError::Other so the dispatcher routes to the Python callback. Example: brk's set_brk relies on SimMemoryError.args[1] for the alternate-brk address on heap collisions. Rust's SymbolicMemory::map is idempotent (silently leaves already-mapped pages alone), so the brk handler scans the to-be-mapped range and falls back to Python if any page is already mapped. CRITICAL: do NOT mutate state before the fallback — caller expects state untouched on Err. See native/angr/src/syscalls/brk.rs::call.

Native syscall handlers must NOT mint symbolic returns with fixed names via RustBV::symbolic: z3::ast::BV::new_const(name,sort) returns the SAME Z3 constant for identical name+sort, so two time()/stub calls on one path are solver-equal (ret1!=ret2 UNSAT), unlike claripy BVS. Fix: syscalls::fresh_symbolic(ctx,prefix,width) appends procedures::symbol_counter(prefix). Test solver-distinctness (assert ret1!=ret2 is SAT via a fresh z3::Solver), NOT just distinct RustBV ids. angr-8o7w.

SyscallOutcome::ContinueSymbolic { ret: RustBV } added 2026-05-08 to native/angr/src/syscalls/mod.rs for syscalls returning a symbolic value via the return register (rax on amd64). Dispatcher in exploration/stepping.rs writes the BV directly with set_register_by_offset(ret_reg, ret) — no concrete wrap. Use this for time(2), and for any future syscall whose canonical Python procedure constructs a fresh BVS as its return value.

Native syscall handlers (native/angr/src/syscalls/) follow a SymbolicArgument convention: each call to RustBV::as_u64() that returns None is mapped to SyscallError::SymbolicArgument(" <arg_name>".into()) with the arg name embedded in the message. Tests assert the message contains the arg name (e.g. "addr", "length", "prot", "new_brk") so future handlers can grow without losing diagnosability. Handlers with num_args()=0 (exit/exit_group) cannot produce SymbolicArgument because the dispatcher passes an empty slice — document via a test that asserts the outcome is still Exit even if a symbolic arg is hand-supplied.

When splitting a test file DEEPER into a package subdir, file-relative path computations break by the depth delta. test_rust_exploration.py -> tests/engines/rust/test_misc.py moved one dir deeper, so: os.path.dirname()-chains to reach tests/ need +1 dirname, and pathlib Path(file).parents[N] indices need +1 (parents[2]->parents[3] to reach repo root for docs/advanced-topics/rust_engine.rst). Symptom: FileNotFoundError for tests/docs/... or tests/benchmarks/run_single.py not found. The doc-consistency + counter-parity tests in test_misc.py (TestRustSimOptionMatrixConsistency, TestCounterParity) are the ones that read external files this way. Always grep the moved file for file/parents[/dirname( before assuming a pure move is behavior-preserving.

SymContext transaction API (transaction_begin/commit/rollback, current_push_level, in_transaction) was DELETED in angr-ph300.44 (dead code + latent corruption: commit popped only push_constraint_counts, never the Z3 frame or the push_local_cache_lengths/push_assumed_local_lengths stacks). Consequence: SymContext.push_level has NO incrementer anymore — it is permanently 0. fork()'s 'in_transaction = push_level > 0' gate in snapshot_fork_ops.rs and freeze_into_shared's in_transaction copy-branch are therefore dead (always false/unreachable) but retained as generic fork infrastructure. debug_push_level (used by exploration/state_api.rs) also always returns 0. If a future feature needs real transactional scoping, use bare push()/pop()/try_pop() (still live in transaction_ops.rs) — do NOT resurrect push_level bumping without re-auditing the fork freeze gate. Removed alongside: PushStack type alias (context.rs) + smallvec import, and the ConstraintSyncError enum + mod.rs re-export (both had no other users).

Two pinned address solutions whose difference is a power-of-2 / multiple of page size hit the Strided concretization branch in load_symbolic_unified, NOT the Multiple branch. Reason: detect_stride_from_solutions(addrs) computes GCD of differences; for [a, b] with diff=stride, expected_count = (b-a)/stride+1 = 2 == addrs.len(), so it returns Strided{base=a, stride, count=2}. Tests targeting the multi-solution Multiple+ITE path with stride-aligned solutions therefore actually exercise the Strided ITE tree path (build_strided_ite_tree). To force the Multiple branch, use solutions that are NOT a regular stride pattern (e.g. [0x1FFC, 0x3FFC, 0x5000]).

Two's-complement signed-min bit pattern (-2^(w-1)) construction pitfall: NOT(x) = -x-1, so !(half-1) ALREADY equals -half where half=1<<(w-1). Do NOT add +1 (that gives -half+1). angr-36vvn.2 fixed saturate_lane_symbolic in vex/ops_vec_saturate.rs which had (!(half-1)+1) & mask, mis-clamping the true dest-minimum (e.g. -128 for I16->I8S narrow) up to -127 for SYMBOLIC inputs only. Canonical correct forms already in the same file: vec_int_saturating's smin and vec_qshl_sat's smin both use 'let smin = sign_bit;' (i.e. 1<<(w-1) reinterpreted). Prefer the sign_bit-style construction over hand-derived NOT arithmetic.

invariant-unsat-at-find-is-pruned: a state reaching a find address on an UNSAT path must land in STASH_PRUNED, never be dropped. Two sites enforce it: check_terminal_conditions (run_loop.rs, popped-state path) and route_successor's find arm (helpers.rs, successor path, gated on gate_found_on_sat) — plus route_materialized_terminal's Bounce-at-find arm (run_loop.rs). route_materialized_terminal's untagged residual arm inherits it by delegating to route_successor(state, true). Any NEW find-routing site must do the same or pruned_count becomes arrival-path dependent and parity debugging between serial and parallel explorations breaks. The resume.rs call sites pass gate_found_on_sat=false (satisfiability already established upstream) so their prune arm is unreachable by construction. Regression: unsat_successor_at_find_pc_routes_to_pruned / sat_successor_at_find_pc_still_routes_to_found / untagged_unsat_residual_at_find_pc_routes_to_pruned in exploration/run_loop_tests.rs; the unsat_state fixture pins one symbol to two constants.

UNSAT state stepping: the engine does NOT check parent-state satisfiability before stepping; it only checks satisfiability at fork points (deferred fork pruning in stepping.rs:312/342/876/886). So an UNSAT state with linear (non-branching) successors will still execute one block and then end up in deadended (not pruned) once it has no successors. Asserting state eviction post-step should check 'active count == 0' rather than naming a specific stash like pruned/errored. Verified 2026-05-05 with a shellcode that ends in 'ret' to a symbolic stack — UNSAT state went to deadended, not pruned.

USE_SYSTEM_TIMES is warn-once rejected (in _REJECTED_OPTION_NAMES, angr/exploration/rust_manager.py) not honored: native sim_time handlers (syscalls/sim_time.rs gettimeofday/time/clock_gettime) always write fresh symbolic timeval/timespec and never consult it. Policy decision was (b)reject over (a)Python-fallback: no benchmark demand for host-time, and warn-once beats silent divergence. Pattern for native-dispatch tests: set rax+args=0 so each handler hits its no-write early return (null ptr -> -1, etc.), assert stats['syscall_python_fallback_count']==0. Doc/code drift is gated by TestDocSimOption*-style matrix parser (rust_engine.rst rows must match the frozensets); use exact phrase '(b) explicitly reject' / '(c) raise NotImplementedError' in the status cell.

INVARIANT (commit 971d35545, angr-v5ht): when LINEAGE_DISMANTLED is true, SymContext::fork MUST set child.lineage = None (NOT Arc::clone parent.lineage). Why: Arc::cloning parent's lineage gives child a shared solver whose loaded_path/base reflects the lineage as it was at mint time. Child starts with EMPTY scope_path. Child's next query routes through switch_to(empty) which pops the shared solver back to its base — but the base does not include the parent's post-mint accumulated constraints. The child's query then runs against a STALE constraint set, returning underconstrained SAT solutions (manifested as chr() ValueError on baby-re where unconstrained flag_chars exceeded 0x110000). Per-context solver fallback IS correct because it builds from frozen_shared which carries the parent's FULL accumulated constraints. Any future complex dismantle variant (see angr-0dgq for tear-down-in-flight) must preserve this: either inherit parent's scope_path TOO (descendants-share-Arc semantics) or fall back to per-context solver, NEVER just Arc::clone with empty scope_path.

IROp::VCmpGT carries signed:bool (angr-9ke6b.160) — libVEX has both Iop_CmpGT{N}Sx{M} and Iop_CmpGT{N}Ux{M}; the unsigned half (ARM NEON VCGT.U*, SSE unsigned packed compare) was unmapped for a long time because the opcode table used vec_arms! (no signed slot) instead of vec_signed_arms!. General rule when auditing native/angr/src/vex/opcode_map.rs: a vec_arms! invocation whose suffix strings contain a literal S (e.g. "8Sx8") is a smell — it means only one polarity of a signed/unsigned libVEX family is mapped and the U twin silently falls back to Python. Cross-check the family against native/angr/vendor/pyvex_ffi.h before assuming the omission is deliberate; genuine absences do exist (there is no Iop_CmpGT64Ux1 D-reg lane).

VEX interpreter chain-break invariant (commit ed600427b, angr-027h): run_until_event chains up to max_blocks blocks per call. It MUST break the chain when a chained block boundary lands on an address-based find OR avoid target, else run_loop's step-boundary find/avoid filter never observes that pc and the target is skipped. Mechanism: RustExplorationManager.stop_addrs (union of find_addrs+avoid_addrs, kept in sync by rebuild_stop_addrs() called from set_find_addrs/set_avoid_addrs) is passed to run_until_event(.., stop_addrs: &HashSet); execution.rs loop breaks on 'blocks_executed>0 && !stop_addrs.is_empty() && stop_addrs.contains(&self.pc)'. The blocks_executed>0 guard lets a state that STARTS at a stop addr still progress (already checked at prior step boundary). This mirrors the pre-existing steps_limit=1 guard for CALLABLE find/avoid predicates in stepping.rs (find_needs_python/avoid_needs_python). If you add a new way to set find/avoid addresses, you MUST call rebuild_stop_addrs() or the chain will skip targets.

Pattern for adding per-reason VEX fallback counters: (1) define a const REASON: &str = ... in native/angr/src/interpreter/mod.rs alongside DCAS_UNSUPPORTED_REASON; (2) have the call site emit CbExecutionError::NeedPythonFallback with REASON embedded in the format string; (3) add pub(crate) field foo_fallback_count: u64 to RustExplorationManager in exploration/mod.rs (init to 0 in constructor); (4) re-export the const in mod.rs's block; (5) bump the counter inside the CallbackReason::PythonVEXFallback arm in exploration/run_loop.rs (sibling of dcas_unsupported_count); (6) surface in BOTH _stats and _get_fallback_stats in exploration/stats_api.rs. Test follows test_dcas_unsupported_metric_exposed pattern — assert stats[key] == 0 and fallback_stats[key] == 0 on a fresh manager. Confirmed working on angr-2iow for vecret_gsptr_fallback_count.

FCmpKind in vex/ir/ops_def.rs (split out of vex/ir.rs in zel8z.7; re-exported via ir/mod.rs pub use) is shared between FCmpScalarLane (SSE *0x4/0x2) and FCmpVecPacked (Iop_CmpFx{2,4}). When extending FCmpKind (e.g. added Gt/Ge for packed compares), the scalar-lane match in vec_float_scalar_lane_cmp must also handle the new variants — even though the SSE scalar-lane opcode_map never emits them today. Pattern: implement Gt(a,b) ≡ Lt(b,a) and Ge(a,b) ≡ Le(b,a) via operand swap so the shared enum stays exhaustive without dead unreachable!() arms. Z3 has only CmpEq/CmpLt/CmpLe in FloatOpKind.

interpreter/expressions.rs eval_unop/binop/triop/qop: the residual Err arm must NOT fabricate Ok(RustBV::concrete(0,width)) for concrete args (silently-wrong). Pattern: keep fresh-symbolic BYPASS only when args symbolic; for concrete args return Err(CbExecutionError::Op(e)) so op_error_to_typed (engine.rs) surfaces RustUnsupportedVexOpError or routes to Python fallback. UnsupportedNeon/UnsupportedVexOp still propagate unconditionally via named arms above. Fixed in angr-sa3j; same class as angr-ppgx/angr-tkbr.2.

VEX packed FP compare opcodes Iop_Cmp{EQ,LT,LE,GT,GE,UN}{32Fx2,32Fx4,64Fx2} have asymmetric coverage in pyvex: 32Fx2 (ARM NEON, I64 result) only has EQ/GT/GE; 32Fx4 (SSE V128) has all six; 64Fx2 (SSE V128) has only EQ/LT/LE/UN (no GT/GE). 32Fx8/64Fx4 (AVX V256) DO NOT EXIST in pyvex. Verify shapes via pyvex.get_op_retty('Iop_Cmp...'). Implemented as IROp::FCmpVecPacked { kind, elem, count } in native/angr/src/vex/ir/ops_def.rs (commit cf12c4dfd; vex/ir.rs later split into the vex/ir/ directory). Result width = elem.bits() * count.

VEX naming for SSE/AVX packed FP ops: Iop_{32Fx4,64Fx2} for SSE 128-bit; Iop_{32Fx8,64Fx4} for AVX 256-bit. Scalar-in-vector variants are Iop_{32F0x4,64F0x2} (note '0' between elemsize and laneCount). The whole-vector and scalar-lane variants are DIFFERENT IROps (VFAdd vs VFAddS) — opcode_map must distinguish. result_type is V128 for both because the vector destination is V128 even for scalar-lane variants.

VEX Iop_Cmp{EQ,LT,LE,UN}{32F0x4,64F0x2} (SSE CMPSS/CMPSD) returns V128 — NOT I1. Shape: lane 0 = all-1s (0xFFFFFFFF for F32, 0xFFFFFFFFFFFFFFFF for F64) on true, 0 on false; upper lanes pass through from the LEFT operand (matches the existing vec_float_scalar_lane_binop / minmax pattern). Pre-angr-sowx the mapping was wrong (FCmpEQ I1). Implemented as IROp::FCmpScalarLane { kind: FCmpKind, ty: IRType } in native/angr/src/vex/ir/ops_def.rs (vex/ir.rs split into the vex/ir/ directory). The Un (unordered/NaN) variant uses IEEE 754 identity is_nan(x) ⇔ NOT(x == x): both Z3 Z3_mk_fpa_eq and Rust f32::== return false on NaN. Sanity check: pyvex.get_op_retty('Iop_CmpEQ32F0x4') == 'Ity_V128'.

VEX exposes no IROp variants for x87 transcendentals (Iop_SinF64=0x14e6, CosF64=0x14e7, TanF64=0x14e8, 2xm1F64=0x14e9, AtanF64=0x14de, Yl2xF64=0x14df, Yl2xp1F64=0x14e0, ScaleF64=0x14e5) or AArch64 RecpExp (RecpExpF64=0x14fa, RecpExpF32=0x14fb). FFI lifter delivers them as IROp::Raw(opcode). Concrete fast paths now dispatch in VEXOps::binop (binop transcendentals: Sin/Cos/Tan/2xm1/RecpExp) and VEXOps::binop_with_rm (triop transcendentals: Atan/Yl2x/Yl2xp1/Scale) via vex::transcendentals module. Symbolic case has no Z3 backend (no FP transcendental theory) and falls through to expressions.rs unsup_* fresh-symbolic fallback. Adding new transcendentals: extend the match in transcendentals.rs::try_concrete_{binop,triop}_rm with the new opcode constant and a Rust f64 method.

invariant: the parallel wave's post-barrier routing must NEVER propagate a per-payload error. By the time run_loop_parallel reaches routing, job.take_results() + drain_residual_payloads() have already moved every surviving state into the local materialized vec and the job is dropped — that vec is the SOLE handle on the wave's founds/frontier. Any early return (?) on payload k of n silently destroys n-k states with no stash record. The single choke point is RustExplorationManager::route_materialized_payloads (exploration/run_loop.rs), which logs-and-skips and returns the drop count; its steady twins route_steady_terminal and finalize_steady_session do the same per state. Test hook: StateMigrationPayload::corrupt_for_test (state/migration.rs, #[cfg(test)]) yields a payload whose reattach always fails. Fixed angr-ph300.11.

Wheel repair is per-platform, but the RULE is invariant: NEVER let the repair tool vendor a shared lib whose globals must be process-unique into the angr wheel. TWO such libs now: (1) libz3 -- the Rust cdylib and claripy must load the SAME libz3 (AST passthrough hands raw Z3 Ast pointers across FFI; a pointer is only valid in its own Z3_context). (2) libpyvex -- since libvex-ffi is default-ON (angr-3trr7, commit 807bfd74d), the native lifter's byte-parity argument rests on it being the SAME libpyvex.so pyvex loads; a vendored 2nd copy has its own vex_control/arena globals. Mechanics per platform (.github/workflows/wheels.yml): (a) Linux ELF: auditwheel repair --exclude libz3.so --exclude 'libz3.so.' --exclude libpyvex.so --exclude 'libpyvex.so.' then patchelf --set-rpath '$ORIGIN/../z3/lib:$ORIGIN/../pyvex/lib'. aarch64 reuses x86_64 recipe under QEMU. (b) macOS Mach-O: delocate-wheel --exclude libz3 --exclude libpyvex, then install_name_tool -change <build.rs abs path via otool -L> @rpath/ AND -add_rpath @loader_path/../z3/lib + @loader_path/../pyvex/lib, THEN codesign --force --sign - the .so -- install_name_tool invalidates the ad-hoc arm64 signature; forgetting the re-sign is the non-obvious failure. libpyvex leg is guarded by 'if [ -n $pdep ]' (soft, unlike libz3's hard test -n) since Windows/absent-pyvex builds link no libpyvex. (c) Windows: NO mechanism (PE has no RPATH); libvex-ffi auto-degrades there (no libpyvex.so) so only libz3 matters -- needs os.add_dll_directory source change (angr-c4xcs.8). All legs still UNVERIFIED (no Docker in sandbox).

angr-cxw7 wide-BV (>128-bit) fix: RustBV::Concrete value field is u128, so >128-bit concretes can't round-trip. claripy_bridge.rs::extract_int_value now errors (BridgeError::InvalidArgs) when bit_length>128 instead of clamp(1,16)-truncating. SymContext::min/max (symbolic/solving_ops.rs since the angr-wf6f context.rs split, vex-engine-z3 cfg) return None for width>128 because the binary-search bounds lo/hi are u128 and the old u128::MAX cap + low-128-truncated witness gave wrong extrema. The saturating cap itself now lives in ONE place, the module-private fn max_val_for_width in solving_ops.rs (angr-9ke6b.141) — it was copy-pasted at 7 sites; fix width-boundary bugs there, not per-site. KEY GOTCHA: the import-rejection only fires through claripy_to_rustbv (the IMPORT direction). RustSolverContext::add_constraint_ast and eval take a Z3-EXPORT fast path (extract_z3_ast_ptr) that never calls extract_int_value, so they do NOT raise on a wide concrete BVV; min/max DO (they call claripy_to_rustbv with ?). width==128 is fine (range is exactly [0,u128::MAX]); only width>128 is rejected/None. Non-z3 min/max stubs already safe (return as_u128).

Wide (>64-bit) eval on a Rust-engine state must come out of ONE Z3 model. Two historical ways it did not (both fixed in angr-ue4ro, commit b5556cc68): (1) SymContext::eval_wide (symbolic/solving_ops.rs) ran a fresh check()+get_model() per call and ignored model_cache — repeated eval of the same 256-bit stdin BVS returned DIFFERENT models and disagreed with posix.dumps(0); it now reads/populates model_cache like SymContext::eval. (2) RustSolverFallback._rust_eval (angr/exploration/rust_state_export.py) decomposed an unconvertible wide expr into byte Extracts and called eval() once PER BYTE — each byte satisfied its byte-local constraints while the concatenation could violate a CROSS-BYTE one (checksum, or a find gate over a mixed accumulator). Any new part-wise eval must route through RustSolverContext::eval_batch -> SymContext::eval_many -> eval_all_in_model, which does one check-sat and reads every part off that single model. Rule: never reassemble a value from N independent solves.

Native SimProcedures returning a value wider than the arch's integer return register (e.g. strtoll/strtoull 64-bit long long on ILP32 x86/arm32) MUST return Err(ProcedureError::NotImplemented) to defer to Python, NOT truncate. The dispatcher (run_loop.rs / stepping.rs) sets a SINGLE return register via set_register_by_offset(calling_convention.return_register(), rv) — it has no mechanism to populate the high half of a split-register result (edx:eax on x86, r0:r1 on arm32). Returning only the low 32 bits would silently corrupt values above 2^32. The guard 'if state.arch().bits() < 64 { return Err(NotImplemented) }' in strtol.rs::NativeStrtoll/NativeStrtoull is the canonical pattern. Pinned by test_strtoll_ilp32_falls_back_to_python in procedures/strtol_tests.rs.

with_pending(_mut)/with_state(_mut) helpers in native/angr/src/exploration/helpers.rs deduplicate the 'check pending or return PyRuntimeError' and 'find state by ID or return PyValueError' patterns. find_state already checks pending_callback first, so explicit pending fallback after a find_state lookup is dead code. find_state_mut does NOT check pending_callback (only stashes), so methods that need mutable access to a pending state must use an explicit fallback (e.g. export_state_flushed). Closures borrowing self for self.sm work because with_pending takes &self.

Parallel exploration's early-cancel counter is worker_found_hint (run_loop_worker.rs ParallelShared), NOT authoritative. It is bumped ONLY by a worker's pre-step find arm in parallel_process_state. Coordinator-routed finds (route_materialized_terminal: a bounce whose target is a find addr, or an untagged residual frontier state at a find pc) go through push_found_capped WITHOUT touching the hint. The found-set COUNT is bounded worker-invariantly by push_found_capped's found_count()>=num_find gate + the loop-top finalize check, not by the hint. The hint only affects how early the pool cancels; a run whose finds all arrive via coordinator paths cancels one wave/pump-round later. Do not 'fix' the hint to fetch_add on coordinator pushes -- push_found_capped may reroute a would-be find back to active, which would overstate it.

worker_thread (native/angr/src/exploration/scheduler.rs) MUST call clear_worker_local_caches() before it returns (before its local z3ctx drops). Workers populate the bridge thread-local AST_CACHE with RustBV values whose z3 ASTs are bound to z3ctx (via claripy_to_rustbv on interpreter paths). Rust runs thread_local! destructors at thread teardown AFTER z3ctx (a local) has dropped, so without the explicit clear those RustBVs dec_ref against a freed Z3 context (UAF — the angr-bjk8 hazard). The clear runs while z3ctx is still the live thread-local context. Do NOT remove this call. Pinned by test_worker_local_clear_empties_ast_cache (cache_tests.rs). Fixed in commit 89526a569 (angr-bjk8/angr-1yge9.9).

Write-address concretization gate (angr-9ke6b.194, commit 4ccb8fcb9): Rust's write strategy chain is NOT unconditionally Range->Max. AddressConcretizer::write_range_applies(multiwrite) mirrors Python's _create_default_write_strategies: Range(write_range_limit) is in the chain only when SYMBOLIC_WRITE_ADDRESSES is on OR the address carries a MultiwriteAnnotation. Rust never sees the annotation (RustBV has none) and does not need to: annotated stores arrive through a SEPARATE entry point (rust_manager._cb_memory_store_symbolic_full -> _try_multi_cell_store -> state_memory_store_symbolic_multi -> SymbolicMemory::store_symbolic_unified_multi), which calls concretize_write_multiwrite; every natively-computed address goes through concretize_write and gets the Max-only chain (a SINGLE address, the maximum satisfying one, pinned via pin_fallback_addr). CONSEQUENCE for future work: any Rust unit test that wants a symbolic-address store to fan out to Multiple/Strided candidates (Multi cells, eager-ITE depth counters, address disjunction hoisting) MUST construct AddressConcretizer{symbolic_write_addresses:true,..} or use the _multi entry point — the default concretizer now yields Single. Helpers exist: memory/tests/multi.rs::multi_write_concretizer and interpreter/statements_tests.rs::new_interp_multiwrite.

Raw Z3 AST extraction (solver.rs extract_z3_ast_ptr) returns a Z3_ast with NO sort check. Consumers must verify sort before wrapping: BV::wrap over a Bool-sorted node (or Bool::wrap over a BV) is a wrong-sort Z3 call that trips Z3's error handler = PROCESS ABORT, not a recoverable PyErr. claripy Bools that claripy_to_rustbv cannot lower (e.g. fpEQ float comparisons) have length=None and reach these raw fast paths. Fix pattern: Z3AstPtr::sort_kind()/is_bool()/bv_width() (in symbolic/z3_ast_ptr.rs, via z3_sys::Z3_get_sort+Z3_get_sort_kind+Z3_get_bv_sort_size). NOTE (angr-9ke6b.202, 2026-08-02): the old is_bv() predicate was DELETED -- use bv_width(), which returns Some(width) exactly when the AST is BV-sorted, i.e. one call gives both the wrap precondition AND the authoritative width. Never read the width from claripy's .length instead: the sort is what BV::wrap is constrained by, and .length can be absent/disagreeing.

UPDATE (angr-9ke6b.203, commit 988144fc1): on the EVAL paths this whole dance is now centralized in the free fn solver.rs::z3_ast_to_eval_bv(&Z3AstPtr) -> Option. It is the single place that builds the anonymous 'RustBV::Symbolic { id: 0, name: "" }' eval sentinel and the only place that holds the BV::wrap/Bool::wrap unsafe on this path: Bool -> 1-bit BV via ite(BV::from_u64(1,1), BV::from_u64(0,1)); BV -> wrapped at its own sort's width; anything else -> None so the caller reports sort_kind() in its own PyErr. Its 3 callers are eval_upto, eval_z3_ast_ptr and ast_to_bv_for_eval. TRAP when touching it: ast_to_bv_for_eval must keep DECLINING Bool (explicit early 'if z3_ast.is_bool() { return None }') rather than adopting the shared lowering -- its caller eval_batch falls back to Python, which yields a Python bool for a Bool-sorted AST, so returning 0/1 from Rust would silently change eval_batch's result type.

In add_constraint_ast/add_constraints (NOT an eval path, so not covered by z3_ast_to_eval_bv), gate the raw add_constraint_raw fast path (Bool-by-contract) on is_bool() and fall through to the slow path (lowers BV to !=0) otherwise. z3-rs wrap() takes its OWN ref, so wrapping a Z3AstPtr's as_z3_ast() does not double-free. Precedent: state_api.rs _import_z3_constraint_ptrs already did this Bool-sort validation (angr-33t9). LIMIT of pointer validation: calling Z3_get_sort on an arbitrary integer (e.g. 0xdeadbeef) dereferences the pointer before Z3 can detect anything - Z3 does NOT magic-byte-validate AST headers up front. A pure C-API sanity check therefore catches wrong-sort/foreign-context misuse but cannot defend against truly garbage integers; the only sound defenses are (a) an opaque newtype handle, (b) a thread-local set of blessed exported ptrs, or (c) a Z3 error handler + signal handler combo.

Z3's bvshl/bvlshr/bvashr handle the 'shift >= operand width' edge case natively: bvshl/bvlshr return 0, bvashr replicates the sign bit. So vex/ops symbolic shift fallbacks do NOT need extra ITE bounding to mirror the concrete 'if shift >= elem_width return 0/sign-fill' branches. Just resize the shift count to operand width and dispatch.

Z3 const identity is (name, sort/width): RustBV::symbolic(ctx, name, W) lowers to BV::new_const(name, W) (value.rs), so reconstructing a symbol by name at the WRONG width mints a distinct, UNCONSTRAINED const — eval returns a garbage model value, not the recorded symbol's solution. _eval_stdin_symbol (exploration/state_api.rs) hit this: hardcoded width 8 broke scanf %d/%ld stdin symbols recorded at 32/64 bits (angr-ph300.18). Any name-based Z3 symbol reconstruction MUST pass the recorded width. Claripy-imported BVS also lower by name (claripy_bridge/import.rs BVS arm), so a test can constrain claripy.BVS(name,W,explicit_name=True)==v, build RustExplorationManager, and eval_stdin_symbol(sid,name,W)==v round-trips.

Z3 solver counters in native/angr/src/symbolic/stats.rs (Z3_EXTREMA_MODEL_HIT_COUNT / MISS_COUNT, Z3_BRANCH*, Z3_SAT_COUNT, ...) are PROCESS-WIDE AtomicUsize and cargo's test harness runs tests in parallel threads in one process. A unit test may therefore only assert >= deltas on them, never exact equality. test_min_max_use_cached_model_unsigned (context_tests/solver.rs) violated this with assert_eq!(miss_after - miss_before, 0) and failed in 5/20 consecutive suite runs once another test in the binary started doing an uncached min()/max() — the assertion is unfalsifiable-by-design, not a real regression signal. Removed in commit e78137536; its sibling >=2 HIT assertion is the sound form. Same trap applies to any new counter-delta test.

INVARIANT: If a SAT model M satisfies parent constraints C, then C∧cond is SAT (witnessed by M) iff M(cond)=true. Symmetrically C∧¬cond is SAT iff M(cond)=false. So cached models are sound shortcuts for branch feasibility — but ONLY if the model is from the current constraint set. invalidate_model_if_inconsistent enforces this: any add_constraint that the cached model violates drops the cache. This invariant must be preserved by any future change to model_cache lifecycle (clearing, propagation across forks, etc).

codegate_2017-angrybird, sym-write, unmapped_analysis produce BENIGN output divergence between Python and Rust engines. Both reach the same find_addr but Z3 finds different valid models for unconstrained bytes. Example: Python codegate stdin = 'Im_so_cute&pretty_:)', Rust stdin = gibberish that ALSO reaches FIND_ADDR. NOT a regression. The regression suite handles this by marking them rust_only=True. To verify a new mismatch is benign vs a real bug, run solve.py end-to-end and check whether the find_addr actually fires (vs random crash).

Process-wide Z3 profiling counters live in native/angr/src/symbolic/stats.rs as pub(crate) static AtomicU64s (Z3_CHECK_COUNT, Z3_CHECK_TIME_NS, Z3_SAT_COUNT, Z3_UNSAT_COUNT, Z3_TIMEOUT_COUNT, Z3_MATERIALIZE_, Z3_ASSUME_, Z3_BRANCH_, Z3_AST_BUILD_COUNT, plus per-CheckSite arrays) — moved there by context.rs split slice 1 (angr-ugc2). All solver.check() calls must go through timed_check(solver, CheckSite::), which since context.rs split slice 2 (angr-a2br.2.1) lives in native/angr/src/symbolic/solver_build.rs alongside build_solver/build_solver_params/sample_simplify_skip — bypassing timed_check leaves the SAT/UNSAT/TIMEOUT counters and per-site arrays unincremented and silently breaks observability. Counters are global across SymContexts; reset via mgr.reset_solver_stats() before measuring.

Z3 Unknown (timeout) must NOT be conflated with Unsat anywhere in native/angr/src/symbolic/solving_ops.rs. matches!(timed_check(...), SatResult::Sat) treats Unknown as 'not sat', which is a correctness bug (angr-ph300.43): (1) bsearch_min/bsearch_max swallow Unknown as 'nothing at/below/above mid' -> fabricated extremum; (2) is_sat/eval/eval_many/lex_min_witness pin sat_cache=Some(false) permanently after one transient timeout; (3) check_branch_feasibility's None-arm returns (false,true) on a cond-check timeout, pruning the feasible true branch. FIX PATTERN: bsearch_* return Option (None on Unknown, callers propagate via ?); is_sat returns Option internally and only self.sat_cache.set on decided Sat/Unsat (Unknown leaves it unset for retry, returns false to caller un-pinned); branch checks use !matches!(_, SatResult::Unsat) so only a decided Unsat prunes. INVARIANT for any new solver query: only a DECIDED result may write sat_cache; only Unsat may prune a branch or move a bisection bound. TEST PATTERN (deterministic timeout): SymContext::with_timeout(1) + hard semiprime factoring (product of two ~63-bit primes, x*y==N widened to 128-bit) so every Z3 check is Unknown; prime sat_cache(true) to skip the is_sat gate and drive bsearch directly (legit: a factorization exists). See test_min_aborts_to_none_on_bisection_timeout in context_tests/solver.rs.

SymbolicMemory page-range calc (native/angr/src/memory/mod.rs): end_page=(addr+size+PAGE_SIZE-1)>>12 OVERSHOOTS start_page by one page when size==0 AND addr is non-page-aligned, spuriously (un)mapping a page. Python's paged_memory_mixin loop never runs for length==0 → always a true no-op. Fixed in map()/unmap() (angr-n0irt.5) via early 'if size==0 { return; }'. NOTE: add_lazy_region() at ~line 819 uses the SAME formula and is NOT guarded — latent only (callers pass real cle segment sizes, never 0); add the guard there if it ever becomes reachable with size==0.

PRODUCE_ZERODIV_SUCCESSORS is a LIFTING-path divergence, not a memory one, and Rust can never honor it without a feature. Python's zero-div successor is manufactured during lifting: engines/vex/claripy/irop.py raises SimZeroDivisionException on a concrete zero divisor, the resilience mixin (engines/vex/heavy/resilience.py::_check_zero_division) converts it into an Ijk_SigFPE_IntDiv exit, and engines/successors.py::SimSuccessors.add_successor KEEPS that successor only when the option is set (drops it otherwise). The Rust interpreter has no such path at all: IROp::DivS/DivU lower to Z3 bvsdiv/bvudiv (native/angr/src/vex/ops.rs), which are TOTAL functions -- Z3 defines x/0 -- so no SigFPE exit is ever produced and the option has nothing to keep. Resolved (angr-op0dn.14.9) by promoting it into _RAISE_OPTION_NAMES: it ships only in the 'tracing' mode bundle, which is an opt-in mode=, so the raise is dispatcher-routable. Anyone implementing it must add an explicit zero-divisor guard + successor fork in the Rust div ops; do NOT expect Z3 to signal it.

ZeroPy gate levers are ranked by CROSSING COUNT, not by ns — and three existing memories will mislead you into thinking otherwise. The gate predicate is gil_work_time_ns == 0, so ONE surviving crossing fails a bench no matter how cheap it is, and a 10x-cheaper bounce is worth EXACTLY ZERO to the gate. Ranking a gate lever by ns is a category error.

Two memories argue bounce reduction is low-ROI and are routinely misread as killing the work: 'simprocedure-bounce-service-dominates' (service 70% / proc body 30%, so adding native procs does not buy back the ms) and 'bounce-reduction-low-roi-corpus' (only ~20 corpus bounces cleanly reducible). BOTH are ns/throughput-ROI claims about aggregate wall time. NEITHER refutes a count-driven gate lever. Measured 2026-07-14 (iter143, from the checked-in tests/benchmarks/zeropy_attribution.json): SEVEN FAIL benches are bounce-SOLE (bounce is their only nonzero gil_by_class), and FOUR of those bounce a SimProcedure EXACTLY ONCE — cmu_binary_bomb_partial(2), defcon2016quals_baby-re(13), ekopartyctf2016_rev250(1), fauxware(1), google2016_unbreakable_0(1), securityfest_fairlight(1), unmapped_analysis(2). Killing one proc's fallback flips a bench to PASS; the service/body split is irrelevant to that.

The REAL constraint those memories carry (and the one that can actually defund the work) is different: a fallback that is a USER Python hook (my_scanf / get_flag / UserHook) is IRREDUCIBLE per rust-python-boundary-audit — such a bench can NEVER reach gil==0 and must leave the gate DENOMINATOR rather than be 'fixed'. So always classify a bounce (A: no native proc / B: native proc declines on symbolic args / C: irreducible user hook) BEFORE funding an impl. That is bead angr-gorvf.12; the impl is angr-gorvf.13.

Corollary for reading the attribution JSON: posix and find_predicate crossings are SETUP-time, not gate-blocking — they appear on PASS benches at gil==0 (all 8 PASS benches show posix, strcpy_find shows find_predicate=97). Do not count them as blockers.

ZeroExt(k, x) ⊙ BVV fold lives in native/angr/src/symbolic/value_ops.rs::try_zext_const_cmp_fold and runs from each cmp op before Expression construction. Signed comparisons (Slt/Sle) deliberately NOT covered — sign-bit handling is delicate when k bits of zero meet a negative const. SignExt is also not handled. If extending: add Slt/Sle support requires reasoning about whether high zero bits force the value into positive range.