invariant / 2

Extracting a helper out of an exploration/.rs extension-impl module (super:: glob) into a leaf module like exploration/constraints.rs loses the glob's pyo3 trait imports: the body compiles inside the impl but fails with E0282 'type annotations needed' on Bound::call_method0/getattr once moved. Fix is a function-local 'use pyo3::prelude::*;' (plus explicit crate::symbolic::/crate::claripy_bridge:: paths) rather than widening the leaf module's top-level imports — keeps the leaf free of pyo3 surface it does not otherwise need. Seen in import_python_constraints (angr-9ke6b.71).

Leak-gate self-test caught a bug in the GATE, not the engine (angr-c4xcs.4). A deliberate leak injector written as std::mem::forget(Box::new([0u8;64])) is ELIDED ENTIRELY by release-mode LLVM: the allocation is never read and never dropped, so it is dead code. Result: valgrind saw nothing, the self-test reported clean, and the leak gate was silently incapable of failing. Fix: Box::into_raw(vec![0u8;64].into_boxed_slice()) + std::hint::black_box(ptr) -- opaque to the optimizer, unreachable to memcheck, so it lands in 'definitely lost'. Now measures exactly 64.00 B/iter. INVARIANT: any leak/perf gate must ship a self-test that proves it can fail, and that self-test must be run BEFORE the real check in CI (nightly-ci.yml::valgrind_leak_check does this). See inject_leak() in native/angr/examples/leak_probe.rs.

Legacy (pre-LFS) stat-family syscall numbers must stay UNREGISTERED in the Rust native registry on every 32-bit arch: i386/ARM 106/107/108, MIPS32 4106/4107/4108. The Rust writers (write_i386_stat / write_arm_stat / write_mips32_stat, dispatched by write_stat_for_arch in syscalls/file_path.rs) emit only the LFS 'struct stat64' layout used by the *64 numbers (195/196/197, 4213/4214/4215) — st_size at 0x30, 64-bit st_ino at 0x0C. Registering a legacy number to NativeStat/Lstat/FstatSyscall writes a correctly-sized but wrong-offset struct instead of falling back to Python, which DOES have procs for these numbers (angr's linux_kernel.py i386/arm/mips-o32 maps all define 106/107/108). angr-9ke6b.226 fixed exactly this for ARM 107. Older comments claiming 'angr's i386/arm maps have no legacy entry' were false — the correct rationale is the layout mismatch. mod_tests.rs::file_path_stubs_registered_on_all_arches now asserts all nine are absent.

Native SimProcedure duplication: when two libc names share semantics (glibc macro alias, or Python angr does x_unlocked = x), register ONE struct and list the other names in the aliases() trait method / declare_proc's aliases = [...] — do not copy the impl. Precedents: NativeFputc covers fputc/fputc_unlocked/putc/putc_unlocked (angr-9ke6b.113); NativeScanf covers scanf/__isoc99_scanf and NativeFscanf covers fscanf/__isoc99_fscanf (angr-9ke6b.112); strcoll->strcmp; printf->vprintf; fprintf->vfprintf. Registry.get(alias) returns the base proc, so proc.name() is the BASE name — tests that need to exercise the alias must go through NativeProcedureRegistry::get(alias).call(), not a struct literal (scanf_tests.rs test_isoc99_scanf / test_isoc99_fscanf_basic show the pattern; scanf_tests.rs needs an explicit use crate::procedures::NativeProcedureRegistry; since use super::* only reaches the scanf module).

When integration-testing a SimProcedure via RustExplorationManager, the hook address MUST be inside a real loaded binary segment (e.g., fauxware's 0x400000-0x400a74 .text/.fini range), NOT in cle## loader objects (TLS at 0x900000, kernel at 0xa00000) or in unmapped gaps. Otherwise rust_manager.py:_run_python_init_if_needed sees: obj is None or obj.binary starts with 'cle##' AND addr is in proj._sim_procedures, then runs Python init to main, ignoring the hook entirely. Use 0x4008c0 (in fauxware's .fini area) — find_object_containing returns the fauxware ELF, init short-circuits, the hook fires.

The native libVEX lifter (NativeLibVEXLifter::lift in native/angr/src/vex/libvex_lifter.rs) accepts AMD64, ARM, ARM64, MIPS32 and MIPS64. The arch gate is fn ffi_vex_arch: it returns None -> LiftError::InvalidArch (caller falls back to the pyvex-callback path) only for X86, PPC32, PPC64 and S390X. AMD64 was Stage-1; the other four were added by angr-qwyti.20 (commit 195e25ca3), which also grew the corpus parity gate beyond AMD64. fn archinfo_for is arch-generic: every archinfo.Arch emits baseline hwcaps 0, empty cache info and x86_cr0=0xFFFFFFFF, so the sole per-arch difference is endianness (MIPS big, rest little) -- keep parity with gen_libvex_corpus.py. Pinned by libvex_lifter_tests.rs::test_supported_arches_are_not_rejected and ::test_unsupported_arches_rejected. Adding a new arch = add the ffi::VexArch mapping in ffi_vex_arch (archinfo_for needs no change) plus corpus blocks. Superseded the old 'AMD64-ONLY' claim, which was stale from 2026-07-25 to 2026-08-02 (angr-9ke6b.171).

libVEX encodes Ico_V128 / Ico_V256 as a RESTRICTED 'one bit per byte lane' pattern (16-bit for V128, 32-bit for V256): bit i set => byte i is 0xff, clear => 0x00. pyvex EXPANDS this in IRConst.V128._from_c / V256._from_c before the const reaches the engine, so any native marshaller (libvex_lifter.rs::marshal_const, feature libvex-ffi) MUST expand too — see expand_v128 / expand_v256. Passing the raw pattern through is a silent VALUE divergence, not a shape one (pcmpeqd xmm0,xmm0 => native V128(0xffff) vs pyvex V128(0xff..ff)); the structural-Debug parity gate DOES catch it once a V128-const block is in the corpus. pyvex ships as .pyc only — disassemble with dis.dis(pyvex.const.V128._from_c) to read its semantics.

Rust run loop deadend-vs-errored routing is by MESSAGE SUBSTRING, not error type. exploration/stepping.rs RunResult::Error arm: 'if message.contains("No bytes in memory") || message.contains("lift") || addr==0 => Deadended else Error'. The Python lift callback rust_manager.py _cb_lift_block returns the literal "{}" as a designed sentinel when a block can't be lifted (catches SimEngineError/ClaripyError/PyVEXError, warns 'Lift error at 0x..', returns "{}"). That "{}" fails deserialize_irsb on the Rust side; the resulting CbExecutionError::LiftError Display ('lift error: ...') matches the 'lift' substring -> graceful deadend no-op. CONSEQUENCE: do NOT reclassify the deserialize-failure site (interpreter/execution.rs, the irsb deserialize map_err) from LiftError to InvalidIR/MalformedIRSB without first making stepping.rs route on a typed signal -- MalformedIRSB's Display lacks 'lift' so unliftable blocks route to errored, breaking Callable ('No paths returned') and test_strict_page_access_alone_does_not_block_nx_fetch. This is why angr-ghwsd.5 fix2 was deferred.

SymContext per-lineage flags (deterministic, use_shared_lineage_solver) are inherited by fork() so a whole diamond stays in one witness-selection mode. with_timeout() hardcodes BOTH to false. Any code that builds a SymContext via with_timeout/new and represents a continuation of an existing lineage MUST re-propagate these flags. Known sites that must: merge() (snapshot_fork_ops.rs, OR across all input arms) and to_snapshot/restore_from_snapshot (SymContextSnapshot carries them as serde-default fields, angr-ph300.46). Missing propagation silently reverts deterministic eval to arbitrary-Z3 witnesses -> run-to-run nondeterminism returns at the merge/restore point with no error. Accessors: is_deterministic/set_deterministic (solving_ops.rs), use_shared_lineage_solver/set_use_shared_lineage_solver (lineage_ops.rs, z3-gated).

Linux mprotect PROT bits (PROT_READ=0x1, PROT_WRITE=0x2, PROT_EXEC=0x4) and Rust Permission::from_bits encoding (read=0x4, write=0x2, execute=0x1) are REVERSED on bits 0x1 and 0x4. Any native code ingesting raw Linux PROT values (mprotect syscall, future mmap) must translate explicitly — do NOT pipe through Permission::from_bits. See native/angr/src/syscalls/mprotect.rs::linux_prot_to_permission for the canonical conversion.

angr-9ke6b.97: SymbolicMemory's two concrete-load entry points are now ONE body — load_concrete_common(addr, size, ctx, lazy) in native/angr/src/memory/load.rs. load_concrete = record_mem_load + common(lazy=false); load_concrete_lazy_inner = common(lazy=true). Do NOT re-fork them: the split is exactly why Multi-cell gating (angr-9ke6b.96), the angr-3zhl partial-overlap merge and the endianness-aware containing_wider_sym extract each shipped in only one copy. The lazy flag feeds ONE decision, unmapped_page_error(page_num, lazy, fallback): lazy + is_in_lazy_region -> UnmappedPageInRegion (interpreter fetches the page), else the caller's hard Unmapped, whose shape differs per call site (whole page on the single-page fast path, one byte on the cross-page walk). Second invariant: record_mem_load stays on load_concrete ONLY — the lazy path is reached from ite_builder leaves and store_concrete's read-modify-write, so bumping it there double-counts (see invariant-mem-counter-two-paths). Any new load feature belongs in load_concrete_common, never in a wrapper.

VEX LoadG (guarded load) cvt string encodes BOTH source and destination width (e.g. ILGop_16Uto32 = load 16 bits, zero-extend to 32). The destination temp type alone is ambiguous: an 8->32 and a 16->32 load both target a 32-bit temp. Rust's IRLoadGOp must carry src_bits (parsed in pyvex_bridge::parse_loadg_op) so interpreter/statements.rs derives load_size=src_bits/8. VEX only defines the *to32 widening ops (8Uto32/8Sto32/16Uto32/16Sto32); *to64 forms are handled defensively. Unknown cvt -> IRLoadGOp::Unknown which errors InvalidIR at exec (do NOT default to Identity — silently truncates).

Hand-built IRSB JSON via lift_block callback is the cleanest way to test specific VEX statement dispatch paths (LoadG, StoreG, CAS, Dirty) from Python without needing a real binary that emits them. Pattern: _RustExplorationManager + RustSimState + PythonCallbacks; lift_block returns a static JSON string with the target IRStmt. Caveat: forcing a specific ConcretizationResult shape (TooLarge / Failed) is hard from outside — concretize.rs uses fast-enum (16 solutions) + range-seeded binary search + stride detection. An unconstrained 64-bit BVS often resolves to Multiple via fast-enum, and tests that need TooLarge specifically should set configure_concretization_strategies(False, 0, 0, False) AND construct a value with > 16 distinct solutions whose differences have GCD = 1 (defeats stride detect). Tests in tests/engines/rust/test_error_stash.py for angr-2q5k assert the dispatch reached resolve_loadg_load by accepting either memory_load_symbolic_full firing (sym-shape branches) OR memory_load firing for a non-source address (Single/Multiple).

native/angr/src/symbolic/context.rs has a private LocalConstraints struct that combines both assumed (Vec<(RustBV, bool)>) and z3_assertions (Vecz3::ast::Bool, gated on vex-engine-z3) under one Mutex. This replaced the prior two separate Mutex<Vec<...>> fields (assumed_constraints_local + z3_assertions_local). Why: hot path (assume_true/assume_false/add_constraint_raw) used to acquire 2 locks per call; now 1. How to apply: when adding new assumed/z3_assertion writes, lock once via self.local_constraints.lock() and access fields via .assumed and .z3_assertions. Reads should follow the same pattern; never reintroduce separate Mutexes for these two vectors. The shared Arc<Vec<...>> prefixes (assumed_constraints_shared / z3_assertions_shared) remain as separate fields — only the local additions are combined. Fork-time freeze: context.rs::freeze_into_shared<T: Clone> is the generic helper that replaced the prior two specialized fns (freeze_z3_assertions, freeze_assumed_constraints). It takes a &Mutex<Arc<Vec>> shared prefix plus a &mut Vec local — the caller already holds the LocalConstraints lock and passes a mutable ref to the field. This avoids a redundant lock/unlock cycle inside fork() and lets fork freeze both vectors under one local-lock acquisition. Never re-introduce per-vector freeze fns or have freeze acquire the local Mutex itself — fork() (z3 and non-z3 paths) is the single caller, and it locks LocalConstraints once and passes &mut local.assumed and &mut local.z3_assertions. Cloning-vs-moving discipline: in_transaction always clones (rollback needs local intact); otherwise Arc::get_mut+append moves elements without per-element clones.

LoopHeadRoundRobin::select (exploration/selection_policy.rs) memoizes bucket_key via a state_id-keyed key_cache Mutex<HashMap<u64,u64>>. INVARIANT: a state's bucket key is fixed while it sits in the active deque (history/callstack change only after select removes+steps it), so cache once per sighting and EVICT the dispatched state's entry on removal (forked children re-enter with fresh state_ids -> no stale reuse). Bounds cache to ~active.len(); collapses full drain from O(active^2) key computations to O(active). key_cache MUST stay only-indexed (get/insert/remove, never iterated) to preserve the no-hash-order-in-selection determinism contract. #[cfg(test)] key_computations AtomicU64 counts cache misses for the O(active) assertion.

On link-register ABIs (ARM/ARM64/MIPS, CallingConvention::pops_return_addr()==false) the return address is NOT at [sp] — nothing is pushed at the call, so [sp] holds an unrelated caller local. Any interpreter fast path that peeks at the stack for a return address must gate on pops_return_addr() and defer to CallingConvention::get_return_addr (which reads link_register()) otherwise. VEXInterpreter::get_return_addr had this bug until angr-9ke6b.87: its pending_stores/all_flushed_stores probe ran unconditionally, so a buffered write at [sp] was returned as the ARM return address.

Rust macro_rules CANNOT expand to multiple match arms when invoked in arm position (i.e. between two commas inside match). Rust parses macro_invocation, as a single arm-pattern, then expects => expr. Got 52 'match arm with no body' errors when trying macro!() , macro!() , inside match cc_op {}. WORKAROUND that works (used in vex/ccall.rs::cc_op_match!): wrap the WHOLE match (including 'match cc_op {' and '_ => return None,}') in the macro. The macro takes per-family data and emits the entire match expression. Limitation matters whenever you try to dedup match arms across categories.

materialize_deferred_forks (exploration/fork_materialize.rs) is the single source of truth for the SERIAL deferred-fork pipeline: condition lookup -> P11 condition_ast reconstruct -> P15 conservative fork -> build_unexplored_fork -> SAT split. Callers: step_one's find/avoid arm (run_loop.rs) + _resume_after_simprocedure / _deadend_pending_callback / _resume_after_symbolic_branch (resume.rs). Per-caller variation lives in MaterializeForkCtx: guard_sink (Some = continuing state receives the taken-path guard) and stats (Some iff profiling). set_root stays caller-side (needs &mut StateManager) and MUST be applied to BOTH the sat and unsat vectors — every legacy copy registered lineage before the SAT check. Two quirks preserved on purpose: run_loop + deadend DROP unsat forks (no pruned-stash push), and the batch timer is charged even for an EMPTY fork list. The parallel mirror materialize_deferred_forks_core (core_outcome_handlers.rs) is NOT folded in — no P11 fallback, fires the constraints inspect BP, atomics not ExecutionStats (angr-ph300.73).

angr-9ke6b.100 (commit b3efadc99): SymbolicMemory::materialize_pending_ite's 'Err(_) => zero' fallback for the ITE else-arm was NOT observable through the public API — store_concrete_lazy immediately re-checks the identical page range via check_pages_mapped_lazy, so a load that fails with UnmappedPageInRegion is always followed by a store that fails with the same error. Consequence for anyone auditing this family: you cannot write a before/after discriminating test for load-vs-store error classification inside materialize_pending_ite; tests there are contract pins only. A discriminating case would need PendingWrite.size to disagree with value.width()/8 (load spans a page the store does not), which is a malformed write. The fix is still worth having: it drops a wasted Z3 ITE build and stops the wrong 'current' from becoming reachable if a store path ever auto-maps.

Rust engine state materialization (_materialize_single_state in angr/exploration/rust_state_export.py) has FOUR paths: (1) cached SimState in _state_cache, (2) parent-root copy when the root is cached, (3) currently-stepping-state copy, (4) full export_state() as last resort. INVARIANT: any per-state fixup you want applied to EVERY materialized state must go in _finalize_materialized_state — that is the only tail all four paths share. Two things this rules out, both tried and failed in angr-op0dn.13.14: (a) putting the fixup in _restore_plugins_to_state — it only runs on the full-export path, so it silently never fires for a Python-SimProcedure-bounce workload whose found states come back through a cached path; (b) 'fixing' a missing plugin by seeding _state_roots/_state_cache so restored states take path 2 instead of path 4 — that DOES restore plugins but hijacks materialization away from the export path and LOSES THE CONSTRAINTS ENTIRELY (state.solver.constraints == []). Note also that _restore_plugins_to_state's copy guard is 'only copy if not already present', and SimState auto-registers a default posix on attribute access, so it is a near-noop for posix on a freshly-built state.

max_active_states enforcement has TWO sites, not one. Serial: RustExplorationManager::push_to_active_or_drop (exploration/helpers.rs) against sm.active_count(). Parallel: worker::absorb_continues (exploration/scheduler_worker.rs) against WorkTransport::pending (queued + in-flight), the in-wave/in-session analogue -- the parallel frontier lives in worker-local VecDeques + the injector and only reaches STASH_ACTIVE at a wave boundary, so push_to_active_or_drop never sees it (angr-9ke6b.48). Any NEW frontier-push site must go through one of the two. absorb_continues discounts the parent task still counted in pending (pending-1) so a saturated frontier still admits one replacement child, matching serial where the stepping state is already out of STASH_ACTIVE; without that discount a cap of 1 halts the wave after one step. The bound is SOFT by up to workers-1 (each peer's in-flight parent is only discounted by its own worker). Over-cap parallel forks are counted as Pruned TerminalSummary entries (SchedulerCounters::summarized_pruned) and DROPPED -- unlike serial, they are NOT recoverable in STASH_PRUNED, so a Python-level test asserting counts['pruned']>0 (see max-active-states-test-pattern) does NOT work under RUST_PARALLEL_WORKERS>1.

When adding global memory-volume counters to the Rust engine, there are TWO independent execution paths and bumping policy MUST account for both: (1) Rust-memory fast path: try_rust_memory_{load,store} → SymbolicMemory::{load,store}concrete → counter bump (lives at the SymbolicMemory layer). (2) Callback fallback path: try_rust_memory* returns None → load_concrete_addr/load_symbolic_addr/fallback_to_python_store, all of which bypass SymbolicMemory. To get parity, bump the counter at the cb-interpreter level in the post-try-rust branch — NOT at the top of eval_load (would double-count path 1) and NOT inside SymbolicMemory ONLY (misses path 2). State.rs hot path (native simprocs calling memory_load/memory_store) is path 1. Counters validated: mem_load_count/mem_store_count/mem_load_bytes/mem_store_bytes.

Phase 1+ lazy-memory work (angr-czph Multi cells, angr-qh5u STORE) MUST call symbolic::record_mem_ite_depth(depth) on every Multi cell insertion / load-time collapse — otherwise the Phase 0 baseline comparison breaks silently. The function is in native/angr/src/symbolic/context.rs and is the dual of the eager record_mem_ite_depth() calls already placed in memory/store.rs (store_strided, store_conditional_multiple, store_symbolic Multiple branch). Counter is global atomic, reset by reset_solver_stats() / mgr.reset_solver_stats(). Tests that read the counter MUST use delta-based assertions (pre vs post) because cargo test runs tests in parallel and the atomic is process-global.

Memory permission enforcement in Rust SymbolicMemory is opt-in via set_enforce_permissions(true), default OFF. This mirrors angr Python's STRICT_PAGE_ACCESS state option. Why off by default: existing tests/benchmarks frequently map RWX or rely on Python side enforcement; flipping default would silently break callers that map regions with restricted perms expecting them to be ignored. To enable per-state, call state.inner.set_enforce_permissions(true) or via the PyState method.

LoadG (and any future VEX statement that reads memory) must call VEXInterpreter::load_layered / load_layered_at, NOT load_from_callback. load_from_callback is the LAST rung of the ladder: it only tries synthesize_unservable_load then the raw Python memory_load callback, skipping try_rust_memory_load, pending_stores, pending_symbolic_stores, all_flushed_stores and try_read_concrete_memory. In production use_rust_memory=true and stores are never synced to Python (statements_store.rs 'Rust owns memory'), so a direct load_from_callback reads stale/unrelated data for any address written earlier in the same step. angr-9ke6b.83 fixed this for LoadG by extracting eval_load's ladder into load_layered (expressions.rs) and calling it from resolve_loadg_load. Regression tests: statements_tests.rs loadg_sees_pending_store_from_same_block / loadg_sees_rust_memory_store_from_same_block / loadg_single_concretization_sees_rust_memory_store.

angr-9ke6b.229 (commit 6bbef3e00): mem_load_symbolic_addr / mem_store_symbolic_addr now tick from the PRODUCTION concretizer entry points, not SymbolicMemory::{load,store} (which nothing calls -- see invariant-symbolic-memory-load-store-wrappers-unused). Bump sites: SymbolicMemory::load_symbolic + load_symbolic_unified (load side), store_symbolic + store_symbolic_unified + store_symbolic_unified_multi + store_with_concretization (store side), each just past its concrete fast path; store_with_concretization tests addr.as_u64().is_none() instead, because the interpreter (try_rust_memory_store) concretizes one step earlier and hands the result in. THREE semantics traps for anyone reading these counters: (1) they are a SIBLING of mem_{load,store}_count, NOT a subset -- the counted load_concrete/store_concrete are not on the symbolic path at all (it reaches memory via the _automap/lazy variants, which per invariant-mem-counter-two-paths deliberately skip the volume bump). (2) they count ENTRIES into concretization, so the UnmappedPageInRegion page-fetch retry in try_rust_memory{load,store} ticks twice for one guest op. (3) a bench reading 0 is usually genuine -- fauxware/ais3_crackme/defcamp_r100 have concretize_read_count=concretize_write_count=0 too. Validate on sym-write, where all four read 8.

Every SymbolicMemory write path must call check_perms_range(.., Permission::W) itself — there is no chokepoint. store_concrete does it; install_multi_for_candidates (the Multiple/Strided arm of store_symbolic_unified, via install_multi_for_candidates_safe) did NOT until angr-9ke6b.94, so a symbolic-address store silently mutated read-only pages whenever the concretizer happened to return >1 candidate. Two gotchas when adding such a check to a path that auto-maps: (1) run it BEFORE the auto-map loop, since auto-mapped pages are created RW and would make the check vacuously pass; (2) check_perms_range skips pages not present in self.pages, so pre-checking is safe for candidates whose pages don't exist yet. Check every candidate up front so a rejected store installs nothing (no partial mutation). See also invariant-mem-perm-default-off.

Sizing a CACHE/MEMO's payoff: the addressable share is REPEAT conversions, never the path's share of total work. angr-op0dn.9.6 census (m1d_bool_rebuild block of tests/benchmarks/query_class_numbers.json, 11 fast-tier benches): RustBV::to_z3_bool (symbolic/value_z3.rs) is 66.7% of z3_ast_build top-level calls and 88.2% of all constructed Z3 nodes — a naive read says 'huge, memoize it'. But the ovqja.3 per-Expression BV memo (see expression-z3-ast-memo) already serves every compound OPERAND subtree, so a repeat top-level to_z3_bool of a compound-operand node builds exactly ONE node (the mk_eq/cmp itself) and lands in counter z3_bool_memoized_subtree by construction. Memo-addressable work = 442 nodes = 6.5% of corpus node builds, one hash-consed node each => KILLed angr-op0dn.9.4 by its own gate. The 5,564 other nodes the Bool path builds are FIRST conversions, which no memo removes. Measurement pattern to reuse: bracket the top-level entry point with the (z3_ast_cache_miss, z3_ast_memo_hit) atomics in symbolic/stats.rs — built = Dmiss - Dmemo_hit, reused = Dmemo_hit (fns ast_node_counters / record_z3_bool_build). Caveat: process-wide atomics, so the bracket is only exact single-threaded.

RustSimState::merge (state/fork.rs) config-field policy, settled by angr-9ke6b.121: every field a native proc or Python setter can mutate AFTER a fork needs an explicit merge rule, not a self-only carry. Three classes: (1) set-like -> union: hooks and sim_options via the union_arc_set helper (returns self's Arc untouched when all branches are Arc::ptr_eq, so the no-divergence case allocates nothing), environment via a HashMap union with earlier-branch-wins + warn on a conflicting VALUE (mirrors union_overlay). (2) sim-option boolean mirrors (no_ip_concretization, no_symbolic_jump_resolution, keep_ip_symbolic, force_eager_forks) -> logical OR, because they are a second view of the sim_options set that is unioned; self-only carry would revert a branch's set_option. (3) per-path cursors and init-time config with no meaningful union (getopt_optind/optchar, getopt_extern, ctype_loc, concretizer, inspection enabled_mask) -> keep self's value but call warn_config_divergence, the same loud-drop contract the fs longest-stdout merge uses. When adding a new RustSimState field, put it in one of these three classes; the audit found the whole config block was silently in an unstated fourth class. AddressConcretizer/CtypeLocPtrs/GetoptExternAddrs carry PartialEq solely for the class-3 checks.

SymContext::merge (native/angr/src/symbolic/snapshot_fork_ops.rs) must dedup BOTH shared vectors, not just one. fork() freezes into two independent Arcs — z3_assertions_shared AND assumed_constraints_shared — and hands both to the child, so sibling diamond arms are ptr-equal on each. angr-op0dn.11.3 added the Arc::ptr_eq shared-prefix lift for z3_assertions_shared only; angr-9ke6b.139 found assumed_constraints_shared still re-appended per arm, N-fold inflating get_assumed_constraints()/assumed_constraint_count() (what exploration/state_api.rs _export_state_constraints exposes as state.solver.constraints) and compounding multiplicatively across nested merges. The two dedup flags must stay INDEPENDENT: an arm can diverge on one shared vector without diverging on the other (e.g. add_constraint_raw touches only the z3 side). Guard name in code: dedup_assumed_prefix vs use_prefix_fast_path. Tests: context_tests/merge_prefix.rs::test_merge_dedups_shared_assumed_prefix and ::test_nested_merge_does_not_compound_assumed_prefix.

RustSimState::merge (native/angr/src/state/fork.rs::merge) resolves overlay-map key conflicts by earlier-wins iteration order: self > earlier-other > later-other. All three overlay maps (symbolic_pages, hook_symbolic_memory, addr_to_ast) share the identical union loop that only inserts a key if !contains_key, so the FIRST branch to own a key wins. A 2-state test cannot distinguish this from later-wins; needs >=3 states where a conflicting key lives in two DIFFERENT others but not self. Covered by state_tests.rs::test_merge_three_state_overlay_union_and_tiebreak (angr-qwyti.2/n0irt.18): tag entries by provenance (size field for hook/addr_to_ast, int AST value for symbolic_pages) so a reversed others fold flips the merged tag and fails. stdin_symbols unions with dedup-by-name, self-order-first.

SymContext::merge (symbolic/snapshot_fork_ops.rs) builds its result from Self::with_timeout, which hardcodes every per-context setting to a DEFAULT — so any setting that is not an explicit part of the constraint merge must be reconciled ACROSS ALL ARMS at the end of merge(), never inherited from the receiver. Three are handled today: deterministic and use_shared_lineage_solver are OR'd (angr-ph300.46 — any arm that opted in wins, else RustExplorationManager(deterministic=True) silently loses determinism at the merge point) and timeout_ms takes the MIN (angr-9ke6b.140 — a timeout is an upper bound on per-query solver work, so the merged lineage respects the strictest arm's budget). Inheriting from self is a bug of shape 'order-dependent merge': a.merge([b]) and b.merge([a]) must agree. When adding a new SymContext field, decide its merge reconciliation rule in the SAME change and cover it in context_tests/merge_prefix.rs (test_merge_flags_or_across_arms, test_merge_reconciles_timeout_across_arms).

RustSimState::merge (state/fork.rs) uses a documented STDOUT-ONLY FileSystem merge contract (angr-ph300.75): the merged state adopts exactly ONE branch's FileSystem — the branch with the longest stdout buffer, ties keep the earlier branch (self > earlier-other > later-other). Every other branch's fd table, file offsets, writes, and content_sym registry are discarded. merge() now log::warn's for each dropped branch where FileSystem::has_fds_above_stderr() is true (the only case with real non-stdout state to lose). A true per-file ITE merge is out of scope: fd numbers collide across branches so a naive union is ill-defined. Do NOT expect post-merge reads of a file written only on a losing branch to see that write.

RustSimState::merge (native/angr/src/state/fork.rs) must UNION the three Py-AST overlay maps (symbolic_pages/hook_symbolic_memory/addr_to_ast) across self+others, not take self's via clone_py_metadata alone, and take max(heap_brk)/max(posix_brk)/max(mmap_base) — else branch-B symbolic overlay bytes are lost and merged malloc aliases B's live allocations. Conflict policy: keep-earlier (self > earlier-other > later-other) + log::warn. FileSystem/stdout merge (best_fs longest-stdout heuristic) is intentionally still self-only, tracked as a separate ph300 bead. Fixed angr-ph300.51.

RustSimState::merge (state/fork.rs) must union EVERY branch's heap_metadata, not keep self's, because heap_brk is maxed on merge (angr-ph300.51) so a branch-only malloc stays reachable in the unioned memory. If its alloc_size entry lived only on the dropped branch, NativeRealloc (procedures/malloc.rs) defaults copy_len to the FULL new size (old_size.map_or(size, min)) -> over-read past the true old allocation. Fixed by HeapMetadata::union_from (state/types.rs): self-wins on address collision, freed unioned as a set. Same bug class as angr-ph300.51 (watermark max) and angr-n0irt.2 (cgc base/sinkholes): any per-branch heap bookkeeping must combine on merge, never be taken from self alone.

SymContext::min(bv, false) and ::max(bv, false) return Option(u128), but the value is the BVs bit pattern reinterpreted as unsigned and then zero-widened to u128 (NOT sign-extended). For a 64-bit BV holding -42 = 0xffffffffffffffd6, min/max return 18446744073709551574 = (-42i64) as u64 as u128. Tests asserting on signed negatives must use (-42i64) as u as u128, not (-42i64) as u128 (which sign-extends to the high bits and is a totally different value). Hit this in test_atoi_negative_symbolic_digits.

INVARIANT for min/max model-cache seeding (native/angr/src/symbolic/context.rs cached_model_eval + min + max): a cached model M is sound iff it satisfies the CURRENT constraint set — enforced by invalidate_model_if_inconsistent on add_constraint. So M(bv) = v is a feasible value of bv → min <= v and max >= v under both unsigned and signed interpretation. Two seeding rules: (1) tighten initial hi (min) / lo (max) bounds to v. (2) for signed, skip the MinInit (bv<0) / MaxInit (bv>=0) pre-check when v's signed interpretation already proves the predicate. Push/pop scopes do NOT trigger invalidate_model_if_inconsistent, so a model in cache can survive across temporary scope frames as long as the caller doesn't add inconsistent permanent constraints. Future model-cache lifecycle changes must preserve this.

MIPS O32 is the only Linux syscall ABI that spills syscall args to the stack: args 1-4 in $a0-$a3, args 5+ at [sp+16] (the C-ABI 16-byte save area). CallingConvention::syscall_stack_arg_offset() (calling_conventions.rs) returns None by default and Some(16) only for MipsO32; extract_syscall_args (exploration/helpers.rs, a RustExplorationManager method) uses it to read stack args 5+ when present, but ONLY for concrete SP — symbolic SP yields ExtractionError::SpSymbolic and unmapped slots yield StackUnmapped, both of which fall through to the Python syscall callback rather than fabricating zeros. amd64/x86/ARM/AArch64 expose all syscall args in registers, so a >reg-count request stays RegisterOverflow->Python. This unblocked native dispatch of MIPS32 6-arg futex(4238)/epoll_pwait(4313)/mmap2(4210). N64 has 8 reg args so it never needs the stack path.

MIPS Linux syscalls report error in $a3 (0=ok, non-zero=err) separately from $v0 return; glibc branches on it. Rust dispatcher must mirror angr's linux_syscall_update_error_reg: when unsigned ret >= SYSCALL_ERRNO_START (-1133 for both O32/N64), set error_reg=all-ones and ret=-ret (positive errno); else error_reg=0, ret passthrough. $a3 VEX offsets: 36 (MIPS32, base 8 + 74), 72 (MIPS64, base 16 + 78). Implemented via CallingConvention::syscall_error_register()->Option<(offset, errno_start)> in calling_conventions.rs + write_syscall_return() in exploration/stepping.rs (angr-pfbu).

Mirror pattern for cross-mixin invariants in Rust rustdoc (angr-a2br.1.5, 2026-06-01): when the source-of-truth contract lives in a Python module docstring (e.g. angr/exploration/rust_manager.py:10-100 documents I1-I8), the Rust mirror at state.rs/stash.rs/run_loop.rs should: (1) add a module-level rustdoc section listing all invariants with their Rust manifestation (or 'Python-only' tag for orchestration-only invariants — don't pretend Rust enforces them when it doesn't); (2) cross-reference from each Rust enforcement site back to the module-level summary AND back to the Python source; (3) cite the matching regression test name verbatim (TestMmapBaseSync.test_export_path_..., TestStateCacheSizeBound.test_cleanup_state_cache_...) so a future reader can locate it. Debug_asserts are 'where runtime-expressible' — many cross-language invariants aren't (e.g. I7 max() direction is enforced at the Python export site, not Rust). Use them sparingly for genuinely Rust-internal contracts (state_index/state_roots consistency in stash.rs, register size>0 in state.rs::set_registers_bulk). Acceptance: cargo doc --no-deps clean, all tests pass.

Exported SimState mirrors do NOT carry the Rust constraint set in claripy. The authoritative read is _rust_mgr.export_state_constraints(state_id) (or a RustStateProxy); mirror.solver.constraints is whatever claripy list the mirror's base frame happened to have — often 0. A mirror built via rust_state_export.py::_materialize_single_state path 4 (full export_state -> _snapshot_to_angr) starts from project.factory.blank_state() and gets NO constraint import; _attach_rust_solver_fallback routes eval/min/max/satisfiable into the Rust solver instead (re-importing into claripy is expensive + identity-lossy; pre-pinning is UNSAT-prone, see constraint-export-no-pre-pin). Corollary: after load_snapshot the restored ids are absent from _state_cache/_state_roots, so EVERY restored state takes path 4 and every mirror shows 0 claripy constraints. That is by design, not a snapshot bug (angr-wuyo9).

RustSimState.mmap_base field (default 0xC100_0000 = heap_base 0xC0000000 + heap_size 0x00800000 * 2) mirrors Python state.heap.mmap_base for the mmap(2) syscall when addr=0 (kernel chooses). Bumped by NativeMmapSyscall on successful addr=0 mappings; stays unchanged on explicit-addr requests (matches Python mmap.allocate_memory). Mirrored in 3 constructors + 5 fork/merge sites across the native/angr/src/state/ module (mod.rs, fork.rs, snapshot.rs) alongside posix_brk. Accessors: state.mmap_base() / state.set_mmap_base(addr). NOT pushed back to Python's state.heap.mmap_base on syscall fallback today — same drift risk as posix_brk. See native/angr/src/syscalls/mmap.rs.

Linux mmap(2) syscall flag-decision gotcha: Python's procedures/posix/mmap.py compares 'fd[31:0] == -1' (low 32 bits == 0xFFFFFFFF), NOT the full 64-bit fd. Native handler must mask fd & 0xFFFFFFFF before checking for the anonymous sentinel — passing the full 64-bit value compared against u64::MAX silently breaks for callers that zero-extend a 32-bit -1 (gets passed as 0x00000000FFFFFFFF). Bad-flags fast path: when (flags & MAP_SHARED == 0) == (flags & MAP_PRIVATE == 0), Python returns BVV(-1, bits) directly (covers both the zero-bits case and the both-bits-set case). Native handler can mirror this without falling back. PROT bits are taken as prot[2:0] (mask & 0x7) before mapping — high bits are silently ignored. Source: native/angr/src/syscalls/mmap.rs (commit 7391b2426).

Splitting a big Rust module in this crate: the sibling _tests.rs file must be split along the SAME boundaries, and its section-comment markers are NOT trustworthy boundaries. In helpers_tests.rs (angr-9ke6b.76) the '// --- Timeout / LengthLimiter / LoopBound ---' banner covered ~460 lines that also contained the effective_pc tests and the whole materialize_deferred_forks block; slicing on the banners produced dangling doc comments ('error: expected item after doc comment') and cross-file fixture references. Reliable method: (1) list every top-level 'fn ' with line numbers and classify each by the symbol it exercises, not by the banner above it; (2) walk BACKWARD from each fn over contiguous ///, //, and #[..] lines to find the true block start; (3) after cutting, grep each new file's head/tail for a trailing doc comment or a leading orphaned fixture. Shared test fixtures (e.g. push_active_at) do not survive the split -- either move them with their only consumer or inline the one-off call; a #[cfg(test)] mod tests is private, so cross-module fixture sharing is not available without making the tests mod pub(crate).

Do NOT add a from_stash==to_stash no-op guard to _move_state (exploration/state_lifecycle.rs). Unlike _move_states (which guards to dodge a bulk double-insert/drop bug, angr-ph300.17), _move_state's same-stash remove-then-push_back reorder-to-back is LOAD-BEARING: _StashDict.setitem (rust_state_proxy.py) rebuilds a stash in caller-specified order by calling move_state(sid, cur, key) with cur==key per state (angr-wxuo). Adding the guard breaks test_stash_assignment_reorders. The two methods intentionally differ on same-stash semantics. Pinned by Rust test move_state_same_stash_reorders_to_back (angr-04tw3.4).

_move_states (exploration/state_lifecycle.rs) no-filter branch pattern remove(from)+ensure_stash(to)+insert(from,empty) is destructive when from==to: ensure_stash recreates the same key, append refills it, then insert overwrites with an empty VecDeque, dropping all states and dangling index entries. Fixed by guarding from_stash==to_stash -> return Ok(0) at fn top so all paths (no-filter, filter, single _move_state) agree. Rust regression tests in state_lifecycle_tests.rs. Note StashManager.insert is a raw HashMap::insert (stash.rs) — it clobbers, does not merge.

Phase 2 lazy STORE introduced install_multi_for_candidates_safe (memory/store.rs) — the production-safe entry that respects lazy regions. Three behaviors codified: (1) candidate page in declared lazy_region but unmapped → return UnmappedPageInRegion so interpreter fetches from Python; (2) candidate page unmapped AND non-lazy → silently filter (matches prepare_addresses_for_ite skip behavior; addr was concretized to it so it's nominally unreachable); (3) candidate page mapped → install Multi byte alternatives. install_multi_for_candidates (without _safe suffix) keeps its auto-map-as-RW behavior for test rigs and SimProcedure-direct calls via state_memory_store_symbolic_multi (Phase 1.4 PyO3 path). DO NOT route the production interpreter Store callback through the bare install_multi_for_candidates — it would auto-map zero pages over Python backer data.

Phase 4.1 introduced multi_versions: FxHashMap<u64, u64> on SymbolicMemory — a per-byte monotonic counter that MUST be bumped by any code path that mutates a Multi cell at byte_addr. Currently bumped on: set_multi_alternatives, clear_multi_at (only when payload existed), and per-byte inside flush_multi_cells. Versions persist across removal/reinstall so post-flush fingerprints differ from cached pre-flush ones even with identical alt counts. Any future write path that mutates multi_objects without going through these three entry points MUST also call self.bump_multi_version(addr) — otherwise the wider_load_cache (memory/mod.rs) will serve stale BVs. The cache key is (addr, size); fingerprint is Vec<ByteFingerprint::Multi{version, default_byte} | Concrete{byte}>.

After Phase 1.1, an address byte in Rust SymbolicMemory can be in one of four states: (1) pure Concrete (no bitmap bits, no sidecar entries); (2) plain Symbolic (page.is_symbolic bit set, entry in symbolic_objects and/or symbolic_spans, NOT in multi_objects); (3) Multi (page.is_multi bit set, entry in multi_objects, NOT in symbolic_objects — set_multi_alternatives clears the symbolic entries); (4) inconsistent/transitional (any other combination, treated as a bug). The 'Multi supersedes Symbolic' rule is enforced by the set_multi_alternatives setter — see test_multi_supersedes_existing_symbolic in native/angr/src/memory/tests/multi.rs. Future load.rs integration (angr-n082) and store helpers (angr-aija) MUST preserve this invariant: when transitioning a byte's state, clear the old sidecar entries before installing the new one.

Multi-xor-Symbolic invariant enforcement (angr-9ke6b.95, .96, .101 family): every code path that transitions a byte between the Multi and Symbolic states must clean the OTHER sidecar, because multi_bitmap and symbolic_bitmap are disjoint and load dispatch checks multi_objects FIRST. Use SymbolicMemory::clear_multi_at (memory/multi.rs) rather than hand-rolling the multi_objects.remove + page.clear_multi + bump_multi_version triple. In store_concrete the cleanup must run BEFORE the symbolic branch's page-cloning loop, which clones each MemoryPage, mutates the clone, and re-inserts it -- a clear_multi_at issued mid-loop would be flushed away by the stale clone. set_multi_alternatives already does the mirror direction (removes symbolic_objects/symbolic_spans on install).

invariant: an address-based find/avoid target that is ALSO a hooked SimProcedure address must never run natively. Native dispatch (exploration/core_outcome_handlers.rs::handle_simprocedure_core) is INLINE — it runs the proc body and sets pc=return_addr — so the target address never surfaces at a step boundary and the run-loop find/avoid check never fires. Fixed angr-1i5h7 (iter85): handle_simprocedure_core now computes is_find_or_avoid from ctx.find_addrs/ctx.avoid_addrs and forces NativeProcDisposition::Fallback, so the Python bounce path's existing short-circuit (run_loop.rs::step_one NeedCallback CallbackReason::SimProcedure special case, and the parallel MatKind::Bounce 'Bug C1' route via bounce_target_addr) routes the state to FOUND/AVOIDED before any proc body runs. run_loop.rs::step_one's OWN inline native path needs no guard: its pre-step find/avoid check on pc runs before the hook block. Symptom without the fix: explore(find=) runs straight past the target whenever a native proc exists for that name (this was the root cause of the xmllint_getenv 'catastrophic regression' recorded on angr-a8epx). Any NEW inline native dispatch site must replicate this gate — see avoid-fixing-only-one-native-dispatch-path.

Native procedure dispatch fires only when hook addr is OUT of binary_regions (skipped extern objects + non-executable sections of real binaries) AND the addr is in a real binary so _run_python_init_if_needed short-circuits. Sweet spot for testing native dispatch with fauxware: addrs in non-executable sections like .ctors (0x600e30+). Use proj.factory.blank_state(addr=NON_EXEC_INBIN_ADDR) and set state.memory.store(rsp, RET_ADDR) for return address. After native proc returns, dispatch reads return_addr from rust_memory; for chained calls populate via mgr._rust_mgr.active_states_map_memory(rsp, ret_addr.to_bytes(8,little), 7). No public API to update registers between mgr.run calls, so RDI/RSI for the next native call must be the same as the previous.

INVARIANT: the native libVEX seam (try_native_lift in interpreter/execution.rs) bypasses the _cb_lift_block Python callback ENTIRELY — it reads block bytes from rust_memory via read_concrete_bytes_for_lift. Two consequences. (1) SMC still works, but by a different mechanism: rust_memory holds the STORED bytes, so no dirty_bytes plumbing is needed; the callback-path dirty-bytes contract test (test_smc_rust_passes_dirty_bytes_to_python_lift, tests/engines/rust/test_error_stash.py) must therefore construct its manager with use_native_lift=False or it records zero lifts on a feature-on build. Companion test_smc_native_lift_executes_stored_bytes proves the native path behaviorally. (2) Any test/tool that observes lifting by wrapping _cb_lift_block will silently see nothing on an AMD64 feature-on build now that use_native_lift defaults True. NOTE: interpreter lift counters (rust_native_lift_count / rust_native_lift_fallback_count) are only published in mgr.stats after mgr.enable_profiling().

libVEX native-lift byte source (fn native_lift_source_bytes, interpreter/execution.rs): sidecar (rust_memory.read_concrete_bytes_for_lift) FIRST, because it reflects stores — that is what makes SMC work on the native seam with no dirty-bytes plumbing. But a code page is only in the sidecar once something faults it in, so COLD blocks (first block of a page; every block of a load_shellcode blob) read empty there and used to fall back to pyvex. Fallback order is now: sidecar -> load-time binary-region store (VEXInterpreter::read_concrete_prefix over concrete_memory, populated from _load_binary_regions). INVARIANT: never serve the binary-region bytes for a page is_code_range_dirtied() reports dirty — the load-time image is stale there and would silently lift the pre-store program; those must keep routing to the callback's byte_string= path. Pinned by test_native_lift_serves_cold_page_from_binary_regions + the two SMC tests in tests/engines/rust/test_error_stash.py.

Native realloc's heap bookkeeping is DELIBERATELY stricter than the Python reference -- do not 'fix' it toward parity. angr's SimHeapBrk._realloc (angr/state_plugins/heap/heap_brk.py) never calls free at all: it allocates, copies, returns. NativeRealloc (native/angr/src/procedures/malloc.rs) does call state.heap_free(ptr) for every non-NULL ptr, including realloc(ptr, 0) (POSIX/glibc 'free and treat as malloc(0)'), so HeapMetadata.free_count / is_allocated stay truthful for downstream double-free and leak analysis. Both are metadata-only -- the bump allocator never reclaims -- so the divergence is invisible to the memory model and cannot change a path's satisfiability. The bug fixed in angr-9ke6b.117 (commit e4305cdd3) was that heap_free shared the copy loop's 'ptr != 0 && size > 0' guard; the two conditions are now split (free on ptr != 0, copy on size > 0). Covered by test_realloc_zero_size_frees_original in procedures/malloc_tests.rs.

Native ReturnUnconstrained stubs (procedures/stub.rs::NativeReturnUnconstrained) cannot live in the static NativeProcedureRegistry: a SimLibrary stub is keyed on the BINARY's symbol name (get_flag, some_unresolved_import), not a libc name, and its return width comes from that hook's prototype. They are built at setup time from Python: rust_callback_dispatch::_unconstrained_stub_spec filters project._sim_procedures (exact class ReturnUnconstrained, no return_val= kwarg, prototype returnty size known) and RustExplorationManager._register_simprocedures passes (name, ret_bits) to the PyO3 method register_unconstrained_stubs, which skips any name that already has a real native proc. Two traps: (1) at registration time the prototype's SimType is NOT arch-bound, so returnty.size raises ValueError('Cant tell my size without an arch!') — call with_arch(project.arch) first; (2) the symbol width must be the prototype width, not arch bits, because Python stores it via SimCC.return_val(ty) which refines the return register (a narrow return is a partial register write, eax within rax).

Harness-seeded stdin (posix.stdin.content -> fd 0 content_sym, angr-mb09c) is consumed by exactly ONE helper: procedures/stdin_common.rs::mint_stdin_bytes. It mints the plain 8-bit leaf symbols, eq-binds the seeded prefix by constraint (never stores the seed AST into the guest buffer -- see avoid-storing-extract-asts-in-guest-buffers), and record_stdin_symbol's ONLY the bytes past the seed (recording seeded ones makes inject_rust_stdin append a duplicate copy of the harness's chunk). Callers: read.rs::read_stdin_symbolic, fgets.rs (fgets/gets/fgetc/getchar), scanf.rs::do_scanf %s path when record_stdin, syscalls/cgc.rs::NativeReceiveSyscall. INVARIANT: any NEW native reader of fd 0 must call mint_stdin_bytes rather than RustBV::symbolic + record_stdin_symbol, or harness-seeded stdin silently regresses to zeros + a zero prefix in posix.dumps(0). Known gap (angr-ptf54): scanf numeric conversions (%d et al.) do NOT consume the seed -- no byte-for-byte mapping exists through a decimal parse, so a seeded harness whose target scanfs %d still gets a fresh symbol and leaves the seed unconsumed. COMPANION (angr-9ke6b.158, commit 24a118286): the NON-stdin side of the same shape lives in syscalls/mod.rs -- syscalls::mint_symbolic_bytes (mint N fresh bytes + store into a buffer; used by read_symbolic, scatter_symbolic, cgc random, NativeGetrandomSyscall) and syscalls::fresh_byte_names (the '_' naming half, one counter bump per batch). CGC receive uses fresh_byte_names + mint_stdin_bytes: it needs the names BEFORE the bytes exist, which is exactly why naming is split out of mint_symbolic_bytes. A new fd-0 reader therefore combines both helpers; a new non-fd-0 buffer-filler uses mint_symbolic_bytes alone and must NOT hand-roll the counter/format!/store loop.

Native string procs (strlen.rs, strcmp.rs, strchr.rs and the memchr/memcmp variants) enforce Python's symbolic-scan budget, not just its pruning constraint. Two SEPARATE Python-parity mechanisms, both now present, do not confuse them: (1) PRUNING — strings::null_exists_constraint asserts 'a null exists in the scanned window', the constraint Python gets free from memory.find (smart_find_mixin._find_process_cases adds Or(*cases)). Landed under angr-sgcye. Called by strlen.rs::scan_for_null (require_null) and strcmp.rs (only when stop_at_null && max_len >= MAX_STRCMP_LEN — a caller-bounded strncmp(a,b,4) may legitimately compare four non-null bytes, so it must NOT assert this). (2) WINDOW — strings::MAX_SYMBOLIC_SCAN_BYTES = 60, mirroring state.libc.buf_symbolic_bytes (angr/state_plugins/libc.py), which Python passes to memory.find as max_symbolic_bytes; smart_find_mixin._find_iter_items simply RETURNS once that many symbolic chars have been yielded. Enforced inside strings::scan_concrete_then_collect (angr-gorvf.5, commit c94941fff) so every scanner that shares the skeleton inherits it. ONLY symbolic positions draw down the budget — concrete filler is free, exactly as in Python. WHY THE WINDOW MATTERS: without it a fully-symbolic buffer collected up to MAX=4096 positions, so the ITE chain AND the null_exists_constraint disjunction ran thousands of terms wide, and each term kept a downstream branch feasible -> fork-storm where Python deadends. Pruning alone does NOT fix this; a 4096-wide Or is barely a constraint. IMPLEMENTATION NOTE: the budget needed no signature change to scan_concrete_then_collect's 6 call sites — the existing concrete closure already answers ConcreteStep::BeginCollect exactly for the loads a given scan treats as symbolic, so it doubles as the symbolic predicate during the collect phase. KNOWN REMAINING DIVERGENCES (both benign, neither a fork-storm driver): Python strlen.py swaps a depth>3 result for a fresh BVS + equality constraint (native returns the raw ITE chain — AST-size cost only); and Python's total search window is max_str_len=128 with doubling, while native still scans concretely to 4096 (strictly more permissive, so it cannot wrongly kill a state). NULL_EXISTS_CONSTRAINT DETAILS (absorbed in the R4 merge): the helper (procedures/strings.rs::null_exists_constraint, an Or over the symbolic bytes collected by scan_for_null_symbolic / the s1 side of compare_bytes) declines when the window holds a concrete null (trivially true) or holds NO symbolic byte (trivially false - would wrongly kill the state). ONLY sound for the procedure's own MAX window: strnlen legitimately saturates at maxlen and strncmp(a,b,4) may compare 4 non-null bytes, so bounded variants pass require_null=false. Landed commit e370c8331 (angr-sgcye); Python-parity source is procedures/libc/strlen.py's state.memory.find assertion.

Native strncpy now serves a symbolic source window (angr-gorvf.13, procedures/strcpy.rs::strncpy_symbolic). Semantics deliberately mirror angr's Python strncpy, NOT POSIX: cpy_size = ITE(ULT(n, strlen(src)+1), n, strlen(src)+1) and memcpy that many bytes, so dest bytes past the copy length keep their PRIOR contents — no zero padding. The pre-existing all-concrete path still zero-pads (POSIX), so the two paths differ on the tail; that asymmetry is intentional (each matches what it matched before / what Python does) and is covered by test_strncpy_symbolic_source_null_truncates_copy. Reuse notes: the symbolic length comes from strings::build_strlen_chain and the bounded conditional store from mem_common::symbolic_size_conditional_store (the same primitive memcpy/memset use for a symbolic size) — do not hand-roll either. The concrete fast path still makes a SINGLE scan: the symbolic re-scan only runs after scan_concrete_bounded reports a symbolic byte.

NativeSyscallRegistry (native/angr/src/syscalls/mod.rs) mirrors NativeProcedureRegistry: HashMap keyed by (arch_name, syscall_num). Wired into exploration/stepping.rs at the RunResult::Syscall arm — try native dispatch before creating PendingCallback. Three outcomes: SyscallOutcome::Continue{ret} writes ret to return_register; SyscallOutcome::ContinueSymbolic{ret} writes the BV directly with set_register_by_offset (no concrete wrap); SyscallOutcome::Exit pushes to STASH_DEADENDED. All honor deferred_forks via process_deferred_forks_into. Handler returning Err falls back to the Python callback path (see invariant-syscall-fallback-on-collision for the brk-style 'pre-empt before mutate' pattern). SyscallOutcome derives Debug (needed for #[test] expect_err). Registry covers AMD64/X86/ARM/ARM64/MIPS32/MIPS64/CGC tables — register_syscalls! macro at mod.rs:116. See mod.rs lines 288 (AMD64), 394 (X86), 483 (ARM), 578 (ARM64), 651 (MIPS32), 736 (MIPS64), 819 (CGC) for live lists; do NOT enumerate them in memory (drifts within weeks).

Native syscall handler PC contract: by the time RunResult::Syscall fires in stepping.rs, the interpreter has already advanced PC to the post-syscall instruction (set in exits.rs::handle_exit before returning BlockResult::Syscall). So a Continue-outcome handler does NOT need to advance PC — it only needs to set the return register. This matches what Python does after _handle_syscall_callback resolves.

INVARIANT + test gotcha for apply_native_techniques' removal arms (exploration/native_technique.rs). (1) Discard semantics are ASYMMETRIC and easy to get wrong: LengthLimiter honors its OWN per-technique 'drop' flag (drop=true discards, and register_length_limiter then never even creates the 'cut' stash), while LoopBound ignores any per-technique flag and honors the MANAGER-wide sm.drop_terminal_states() instead — its discard_stash is always pre-created by register_loop_bound, so under drop_terminal_states it exists but stays empty. Timeout has no drop path at all. Do not 'unify' these without checking Python-side parity. (2) Both removal arms collect indices ascending then remove with to_remove.iter().rev(); a count-only test passes under forward iteration, so assert surviving state_ids IN ORDER with >=2 non-adjacent removals. (3) Timeout arms start_time lazily inside apply_native_techniques (get_or_insert_with(Instant::now)), so a register_timeout(0.0) test races clock resolution — backdate the field via Instant::now().checked_sub(..) before asserting expiry (see expire_timeouts in helpers_tests.rs).

A native SimProcedure's Memory(Unmapped) decline is NOT always a fallback: under STRICT_PAGE_ACCESS (RustSimState::enforce_permissions) Python's PrivilegedPagingMixin._initialize_page raises SimSegfaultException on the first touch of an unmapped page, so re-running the proc in Python can only reproduce the fault. core_outcome_handlers.rs::segfault_message + NativeProcDisposition::Segfault turn it into CoreReturn::Errored(state, '{page_addr:#x} (unmapped)') — page-ALIGNED, matching Python's pageno*page_size message. Gate is mandatory: with STRICT_PAGE_ACCESS OFF Python lazily inits the page and keeps executing, so those declines must still bounce. Only Unmapped is mirrored (not Permission / UnmappedPageInRegion). Retired unmapped_analysis's 2 simproc bounces (strncmp+strncpy) with byte-identical errored states.

invariant-ctype-mirror-python-not-rust-std sibling risk is now RETIRED: strtod.rs (floating_prefix_len + the endptr rescan in run_strtod) and strtol.rs (parse_concrete_prefix) no longer use Rust is_ascii_whitespace. All whitespace classification in native/angr/src/procedures/ now goes through the single pub(crate) helper procedures::ctype::is_c_space (' ' plus 0x09..=0x0d), used by NativeIsSpace too — grep for is_ascii_whitespace to verify no new site regresses. SEMANTICS DECISION (angr-2j9sk, commit 2ce6e098c): native strtol/strtod match libc, NOT Python. angr/procedures/libc/strtol.py skips no leading whitespace at all and says so in a source comment ('note: this does not handle skipping white space'), i.e. an acknowledged gap rather than a modelled behaviour — so 'mirror Python' does not apply where Python has no behaviour to mirror. The mirror-Python rule governs ctype PREDICATES, where Python encodes a deliberate predicate.

NativeSimProcedure::name() returns &'static str. For Python-registered procedures whose name is dynamic, store the String once on the wrapper and use Box::leak to produce a 'static reference. The leak is bounded — one allocation per registered procedure, lifetime of process — and the registry holds an Arc for the manager's lifetime anyway. See native/angr/src/procedures/python_proc.rs leaked_name().

angr-3ag1l root cause: RustExplorationManager::resume_after_symbolic_branch (native/angr/src/exploration/resume.rs) used to call set_sat_cache(true) on true_state/false_state, citing a can_be_true/can_be_false proof from the interpreter. That proof does NOT exist on this path: statements.rs IRStmt::Exit under !use_deferred_forks returns StmtResult::SymbolicBranch WITHOUT calling check_branch_feasibility (it deliberately skips the Z3 checks and defers constraint-adding to Python resume). The primed cache then satisfied every downstream satisfiable() gate (route_successor's gate_found_on_sat, the is_find push in run_loop step_one), so an UNSAT state landed in the found stash. INVARIANT: never prime sat_cache from a feasibility claim you did not just verify -- only is_sat()/eval() may write Some(true).

Public Rust APIs that accept newtype-wrapped values (Address(u64), StateId(u64), etc.) should take 'impl Into'. Rust's literal-type inference picks u64 automatically as long as From is the only conversion in scope, so call sites with plain integer literals like 'mem.map(0x1000, ...)' compile unchanged. This sidesteps the deferred-borb concern about every caller needing '.into()' or 'Newtype(...)' wrapping. Verified for memory::Address (angr-borb.1, 2026-05-21).

PyO3 REJECTS macro_rules! invocations inside a #[pymethods] impl body: 'error: macros cannot be used as items in #[pymethods] impl blocks (note: this was previously accepted and ignored)'. pyo3 0.27.2. This blocks the obvious DRY fix for any family of near-identical pymethods wrappers (hit on angr-9ke6b.204, the ~25 op_* binary-op wrappers in native/angr/src/solver.rs).

Two escapes and why only one is viable here: (1) macro-generate a SECOND '#[pymethods] impl' block -- needs the pyo3 'multiple-pymethods' feature, which this crate does NOT enable (see CLAUDE.md Key Files note on exploration/manager_methods.rs, split out for exactly this reason). (2) keep the wrappers hand-written but move their shared BODY into a private helper on a plain (non-pymethods) impl block, dispatching by fn pointer. This is what RustSolverContext::binop does: takes 'op: SymbolTableBinOp = fn(&RustSymbolTable, u64, u64, &SymContext) -> Result<RustBVHandle, BinaryOpError>', so each wrapper is one line 'self.binop(a_id, b_id, RustSymbolTable::op_add)'. 26 wrappers x 8 lines -> 26 x 3.

Silver lining: pyo3 ERRORS rather than silently dropping the methods from the Python type, so the dangerous failure mode (compiles, but hasattr(ctx,'op_add') is False) cannot happen. Verified anyway via tests/engines/rust/test_solver_ops.py, which getattr-s the op names from Python.

Native SimProcedure dispatchers MUST honor no_return. If they advance PC to return_addr after a NO_RET proc like exit, the state re-executes past the call site. In fauxware, exit's return address (0x40071d) coincides with main's prologue, so the state re-enters main -> infinite loop. Fix: when no_return is true, skip the PC/SP fixup, run process_deferred_forks_into to keep unexplored branches, then push the main state to STASH_DEADENDED instead of returning it as a successor. LIVE DISPATCH SITES (citations repaired 2026-08-02; the old 'stepping.rs:handle_simprocedure' and 'mod.rs:run top-of-loop hook check' no longer exist): (1) the hook block in exploration/run_loop_single.rs and (2) exploration/core_outcome_handlers.rs::handle_simprocedure_core. The two take the flag from DIFFERENT sources -- see invariant-no-return-two-dispatch-paths.

no_return flows through TWO independent paths in the Rust engine and they deliberately disagree on the source of the flag. (1) Serial step_one path: run_loop_single's hook block reads the Python-registered flag out of StepContext::simprocedures (the 4-tuple from RustExplorationManager::register_simprocedure) and passes it to dispatch_native_proc. (2) Core/parallel path: core_outcome_handlers::handle_simprocedure_core ignores the registration and uses NativeSimProcedure::no_return() instead. dispatch_native_proc's doc comment enumerates this as one of the caller-owned differences. Consequence: for a hook where the Python SimProcedure's NO_RET disagrees with the native proc's no_return(), the two paths terminate the state differently. The VEX interpreter itself carries NO no_return (SimProcedureInfo has no such field since angr-9ke6b.218 item 2, and RunResult::SimProcedure has no member for it) -- so do NOT 'fix' this by threading the flag through the interpreter; that silently picks one of the two answers. Related: invariant-no-return-deadend (whose stepping.rs:handle_simprocedure / mod.rs:run citations are STALE; the live sites are run_loop_single's hook block and handle_simprocedure_core).

INVARIANT: a Python inspect endpoint fired from INSIDE a Rust step must not call back into self._rust_mgr — the pyclass is mutably borrowed for the duration of the step, so e.g. get_state_ids('active') raises RuntimeError('Already mutably borrowed'). Hit in angr-op0dn.14.4.2: _cb_inspect_vex_lift resolved its state_id=-1 sentinel ('lifts are state-independent') via get_state_ids, which worked only because the pre-existing Python-lift dispatch was exercised out-of-step in tests. Fix: resolve the representative state with the borrow-free thread-local angr.rustylib.vex_engine.get_stepping_state_id() (cached as self._get_stepping_state_id in _setup_callbacks), keeping the stash query as the out-of-step fallback.

INVARIANT: any state.memory.store() / state.memory.load() in code that runs during _create_state_for_callback (rust_callback_dispatch.py:~2150) must be guarded with _is_rust_memory_proxy(state.memory) early-return when the operation is a 'Rust->Python copy' (replay/sync from pending Rust state). Reason: on the 2nd+ callback for a cached state, state.memory IS RustMemoryProxy from the prior install (line 2231). A 'sync to Python' store then round-trips through set_state_memory_concrete and clobbers symbolic_objects in Rust. Two known sites guarded in commit 2480b2aca: _replay_rust_dirty_pages, _install_rust_memory_proxy (both in rust_state_sync.py). Audit any new sync helpers added to _create_state_for_callback's prologue for the same pattern. Pattern in code: from angr.exploration.rust_manager import _is_rust_memory_proxy; if _is_rust_memory_proxy(state.memory): return

Symbolic-store zero-fill is a hard error, not a fallback (angr-9ke6b.19, commit 69c0ef344). bv_to_bytes (both copies: interpreter/helpers.rs and callbacks/dispatch.rs) returns all-ZERO bytes for a symbolic RustBV, so any 'fall back to the byte-level memory_store callback' path is sound ONLY for concrete values. Four sites used to take it unconditionally when memory_store_symbolic_value was unwired, reporting success while overwriting memory with 0: call_memory_store_symbolic_value's own fallback, statements.rs::handle_storeg (concrete-addr AND concretized-Single arms of the symbolic-guard StoreG path), statements_cas.rs::cas_store_symbolic_data (concrete addr), statements_store.rs::handle_symbolic_store (Single arm). Now all four reject a symbolic value: interpreter/helpers.rs::reject_symbolic_byte_store(value, addr, site) -> CbExecutionError::Unsupported is the single rule for the three interpreter sites, and call_memory_store_symbolic_value raises PyRuntimeError on its own path. Concrete values still take the byte fallback unchanged. Rule for new store paths: never hand a possibly-symbolic RustBV to bv_to_bytes + call_memory_store — either route through call_memory_store_symbolic_value / _symbolic_full, or call reject_symbolic_byte_store first. Latent in production (rust_manager.py::_setup_callbacks always registers the callback), live for minimal embeddings and bare PythonCallbacks::new() test harnesses. Sibling invariant on the buffering side: invariant-symbolic-store-no-zero-bytes. Pinned by dispatch_tests.rs::store_symbolic_value_without_callback_errors_instead_of_zero_filling and statements_tests.rs::cas_symbolic_store_without_callback_errors_not_zero_fills.

NX (execute) permission is checked at VEXInterpreter::get_or_lift_block (interpreter/execution.rs (fn get_or_lift_block)) via SymbolicMemory::check_executable(addr). Check runs BEFORE the cache lookup so a page whose X bit is stripped after the IRSB was first cached is still rejected. The check is a no-op when enforce_permissions is off OR when the page is unmapped — only mapped-without-X errors. Unmapped pages must Ok() through here so libpyvex region lift / Python lift_block fallbacks can still resolve code from the loader (binary regions are not always materialized in SymbolicMemory pages).

ObjectMapper identity in native/angr/src/automaton/python_bindings.rs (angr-9ke6b.187, 2026-08-01; interner extracted in .186, 2026-08-02): identity is bucket-by-hash() + PyAny::eq disambiguation via fn find_in_bucket, NOT the old (hash, repr) tuple key. Invariant for future edits: never reintroduce repr() (or any stringification) as an equality proxy — it silently merges eq-distinct NFA/DFA states/symbols. Both sides now share one struct IdInterner (fields: buckets, interned, reserved, kind); ObjectMapper holds states and symbols IdInterners and its get_or_create_state_id / get_or_create_symbol_id / get_symbol_by_id are thin delegators. StateId and SymbolId are both u32, so one interner serves both; the symbol side's only difference is reserved=Some(EPSILON), which IdInterner::get_or_create turns into the 'Too many symbols' error and IdInterner::get turns into the None round-trip. find_in_bucket stays a free function (not a method) because get_or_create holds a mutable borrow of buckets across the scan; it deliberately propagates a raising eq rather than treating the error as 'not equal'. Test gotcha in python_bindings_tests.rs: py.run() snippets get a locals dict but globals=None, so a class method cannot see its own class name — use type(other) is type(self), not isinstance(other, ClassName).

offload_surplus (exploration/scheduler_worker.rs) is unit-testable in isolation: call it directly with a VecDeque, a fresh Injector, an AtomicUsize idle count and a SchedulerCounters::default() whose serde_ns/step_ns are preset via store(). SchedulerCounters' private fields (surplus_offloaded) ARE readable from scheduler_worker_tests.rs because the worker module is a DESCENDANT of the scheduler module that defines the struct — no visibility edits needed. Trigger A gate offload_is_affordable is serde*SERDE_BUDGET_DIVISOR(4) <= step, inclusive, monotone and never reset for session life, so it only reopens once accumulated step time catches up; Trigger B (LOCAL_HWM=64, sheds to HWM/2, strict >) is deliberately NOT budget-gated. Covered by scheduler_worker_tests.rs (angr-ph300.15).

Off-thread pyclass-dealloc leak class is CONFINED to types the parallel scheduler workers actually own/drop, and workers own ONLY native (non-pyclass) data: worker_thread (exploration/scheduler.rs) captures channels (job_rx/done_tx); jobs cross the thread::scope join as native RustSimState (TaskOutcome.continue_states/terminal_states, serialized/'materialized'), NEVER as Py<...> pyclass objects. So among #[pyclass(unsendable)] types (RustSolverContext, RustExplorationManager, PyRustSimState, fuzzer/icicle types) only RustSolverContext was reachable for the cross-thread dealloc leak (fixed angr-87e56/.1). RustExplorationManager+PyRustSimState are #[new]/fork() GIL-thread-constructed and main-thread-dropped (exploration only BORROWS &PyRustSimState via add_state/_add_state); fuzzer/icicle are feature='fuzzer' default-off, not in the parallel build. Investigated angr-1yge9.4 iter67.

on_state_removed hook (exploration/selection_policy.rs SelectionPolicy::on_state_removed) must be called at EVERY STASH_ACTIVE removal path outside policy.select, else a memoizing policy (LoopHeadRoundRobin key_cache) leaks a memo entry per removed state. Full inventory of notify sites after angr-myzjx.25: PARALLEL — scheduler_worker.rs offload_surplus + drain, run_loop.rs wave-mode drain + seed_steady_session_from_active. NON-PARALLEL — helpers.rs apply_uniqueness_filter, apply_native_techniques (Timeout/LengthLimiter/LoopBound arms); state_lifecycle.rs _move_states (no-filter + filter branch), _move_state, _reset_for_stage (dropped ids); manager_methods.rs drop_state_from_stash; stepping.rs _step_state. Stash-generic sites (_move_states/_move_state/drop_state_from_stash/_step_state) guard on STASH_ACTIVE (via from_stash param or sm.stash_of before take). Any NEW active-removal path must add a notify — grep for on_state_removed to find the pattern. Not a correctness bug (state_id never reused, key stable) — pure over-session memory leak.

Before adding or trusting an IROp arm in native/angr/src/vex/opcode_map.rs, grep native/angr/vendor/pyvex_ffi.h for the exact Iop_ string — it is the vendored libVEX opcode enum and therefore the ground truth for what a real lift can emit. Two whole families were dead code that read as implemented coverage until angr-9ke6b.161/.162 (commit bad76646f): scalar Iop_MulHi{32,64}{S,U} (only vector Iop_MulHi{U,S}x exist; x86 IMUL/MUL lift to Iop_MullS32/Iop_MullU32 + Iop_64HIto32) and scalar Iop_Neg{8,16,32,64} (only float Iop_Neg{F16,F32,F64,F128} -> IROp::FNeg and vector Iop_NegFx exist; integer negation lifts as 0-x via Iop_Sub). The tell for this class: an opcode_map arm whose IROp variant has zero references in any _tests.rs — parse_opcode falls through to IROp::Unmapped for a name nobody emits, so the arm never fires and no test ever notices. The QDMulHi/QRDMulHi high-half vector family is genuinely unmapped (see invariant-qdmull-vex-op), which is a different thing from unreachable.

Page bitmap is the AUTHORITATIVE source of truth for byte-level symbolic-vs-concrete state in SymbolicMemory, NOT symbolic_objects/symbolic_spans. The sidecar maps (symbolic_objects, symbolic_spans, multi_objects) are caches/indexes that can lag behind page-bitmap-driven state. store_concrete's page.store_concrete correctly clears the bitmap bits but does NOT clean wider-sym sidecar entries based at a different address. Any load fast path that returns a sym (or extract) without first verifying the bitmap is buggy. See bytes_all_marked_symbolic helper (memory/mod.rs angr-jvjf) for the bitmap consultation pattern.

Parallel worker bounce states carry pc=0 unless stamped. parallel_process_state (run_loop_worker.rs) runs the single-threaded state-update preamble state.set_pc(step.new_pc) BEFORE classifying the CoreReturn; for a Hook / SimProcedurePython bounce step.new_pc is 0. dispatch_bounce re-stamps the pc for exactly those two kinds, so the normal bounce path never noticed — but ANY other consumer of a bounce state (route_materialized_terminal's untagged-residual None arm, flush_parked_bounces_to_active at snapshot time) inherits pc=0 and the state dies at its next lift ('Lift error at 0x0: No bytes in memory'), silently taking its whole subtree with it. Fix (angr-op0dn.13.11): the NeedsPython arm of parallel_process_state stamps bounce_target_addr(&kind) onto the bounce state — AFTER materialize_bounce_forks (so forks are still derived from the unmodified base, bit-identical to single-threaded) and before it crosses the join. Invariant for new code: a bounce state that can reach a stash must carry a re-enterable pc; kinds with no entry address (SyscallPython, SymbolicBranch) still carry new_pc and must never be routed to STASH_ACTIVE.

run_loop_parallel + run_loop_parallel_steady found early-return (found_count()>=num_find at loop top) must call flush_parked_bounces_to_active BEFORE returning ExplorationEvent::found, else a bounce tail parked in pending_parallel_bounces by a prior wave (states in NO stash) is stranded — active_count() under-reports vs the serial loop which leaves the equivalent frontier in STASH_ACTIVE. Steady loop flushes AFTER finalize_steady_session so the resident-id guard in flush_parked_bounces_to_active sees the drained frontier and never double-inserts. Distinct trigger from angr-05kiw (single-threaded fallback stranding). Fixed angr-ph300.8, commit cd8165d1d.

angr-vplge de-flake: parallel post-cancel test assertions must not assume worker timing. Two patterns to reuse. (1) Rust: in exploration/scheduler_tests.rs, never sleep() a peer task and hope a finder's cancel lands inside the window — a worker never dispatches a NEW task once CancelToken trips (scheduler_worker.rs checks it at the task boundary), so post_cancel_steps can only be incremented by a peer that was ALREADY in-flight. Use the spin_until() helper: finder holds until run_order>=2, peer holds until cancel.is_cancelled(). (2) Python: in tests/engines/rust/test_parallel_wave.py, any assertion whose magnitude depends on the RESIDUAL FRONTIER WIDTH at a num_find cancel point is load-sensitive on the parallel arm — which worker wins the race to the target decides how much frontier the others still hold. test_snapshot_after_cancel_round_trips_and_resumes' >=4-of-8 resumed-leaf bound is now serial-arm only; the parallel arm keeps only the no-overshoot upper bound. The worker-count-invariance contract lives in test_resume_from_fixed_snapshot_is_worker_count_invariant, which holds snapshot BYTES fixed and so has no dump-width variance.

Parallel-loop shared-context construction is DRY as of angr-ph300.12 (commit 003ee59b6): ParallelShared::seeded(found_count, num_find) is the ONLY place a ParallelShared literal is built, and RustExplorationManager::build_parallel_process(callbacks, prof, shared) is the ONLY place the Box wrapping parallel_process_state is assembled — used by both run_parallel_loop (per-wave) and ensure_steady_session (per-session). finalize_steady_session no longer hand-inlines the stepped.swap + CoreCounters drain; it calls fold_parallel_shared_counters, the same helper the wave loop uses, so wave and steady counter semantics cannot drift. INVARIANT for future work: add a new ParallelShared field by seeding it in ::seeded (not at a call site), and clone PythonCallbacks on the GIL thread BEFORE calling build_parallel_process (Py::clone needs the GIL and must never run on a worker).

Parallel terminal accounting (angr-op0dn.13.15): a Rust parallel worker NEVER serializes a dead path back to the coordinator — run_post_step_core's dead outcomes become TerminalSummary records that are counted and dropped in the worker's own Z3 context (scheduler_worker.rs worker_wave_loop / worker_session_loop -> SchedulerCounters::record_summaries). Consequence, by design: mgr.stash_counts()['deadended'] is ALWAYS 0 under RUST_PARALLEL_WORKERS>1 — the terminal STATES are unrecoverable; only the COUNTS survive (folded into sm.deadended_count/errored_count/pruned_count by fold_scheduler_dispatch_stats in exploration/helpers.rs, which both parallel loops call exactly once per run). Any test comparing serial vs parallel terminal behavior must project on stats()['deadended_count'], never on the deadended stash. Callers needing the dead states must run single-threaded.

Parallel dispatch counters (angr-op0dn.13.9): parallel_width_hist / parallel_max_active_width are now sampled at worker::dispatch_next (scheduler_worker.rs) from WorkTransport.pending, so BOTH the wave and steady loops record width — previously only the serial migration model (record_migration_sample, helpers.rs) did, and every parallel run reported width 0. parallel_worker_dispatch is a real per-worker dispatch vector (SchedulerCounters.worker_dispatches, fixed-size MAX_TRACKED_WORKERS=32) folded by RustExplorationManager::fold_scheduler_dispatch_stats. PITFALL: trim that vector by parallel_real_workers (the actual pool size), NOT parallel_num_workers — the latter is the MIGRATION MODEL's modelled worker count (defaults to 4, independent of the real pool), and sizing by it pads phantom zero-dispatch slots that make the gate's max/min balance ratio a spurious inf.

stats()['parallel_worker_dispatch_folded'] (angr-9ke6b.67) is the degraded-data marker for stats()['parallel_worker_dispatch']: non-zero means RUST_PARALLEL_WORKERS exceeded scheduler::MAX_TRACKED_WORKERS=32, so SchedulerCounters::record_dispatch folded the tail worker ids into the last slot and the per-worker max/min load-balance ratio the find-all gate reports is NOT trustworthy. record_dispatch also emits a one-time log::warn! on the first fold. 0 on every realistic run (pools are <= num_cpus).

parity_census.py's _EXONERATED table is NOT auto-derived — it is a hand-maintained ledger, and it silently rots whenever rust_manager.py demotes an option out of _RAISE_OPTION_NAMES. collect() classifies any divergence-risk option that is in neither _RAISE_OPTION_NAMES, _REJECTED_OPTION_NAMES, _EXONERATED, nor the rst 'Honored options' physical table as tier='silent'. _docs_matrix() only subtracts names from that physical table — a divergence-table row whose prose verdict reads '(a) honored' does NOT clear the option. So a demotion that is documented only in a rust_manager.py comment block plus divergence prose lands the option in the flip-gate silent surface, contradicting rust_engine.rst's 'opt-in silent count is now zero'. That is exactly how CONSTRAINT_TRACKING_IN_SOLVER (angr-op0dn.14.2) and EFFICIENT_STATE_MERGING (angr-op0dn.11.6) sat misreported until angr-xz5uu. RULE: any commit that demotes a SimOption out of _RAISE_OPTION_NAMES must add it to parity_census.py _EXONERATED and regenerate parity_census.json in the SAME commit. Guarded since angr-xz5uu by the nightly-ci.yml 'parity_census' job, which runs the census (its SystemExit drift guards gate) and then re-emits --json under 'git diff --exit-code' so the checked-in artifact cannot lag the harness.

pending_parallel_bounces (RustExplorationManager, exploration/mod.rs) holds LIVE states that live in NO stash — a wave parks its bounce-queue tail there when it surfaces one need_callback. Any new consumer that reads only stashes (snapshot dump, stash_counts, a new export path) must call flush_parked_bounces_to_active() first, and any new run-loop route must drain the queue. As of angr-05kiw (commit 6a980325d) the three callers are dump_snapshot_bytes, finalize_parallel_session, and run_loop_single_threaded (drain sits ABOVE the callbacks-not-set check so even the error exit consumes it); the two parallel loops drain it themselves via process_parallel_bounce_queue. Flush is idempotent (empty-queue early return + resident-id skip), so double-calling is safe. Non-re-enterable kinds (worker zeroed the pc) stay parked and are logged, never dropped.

Fixed 2026-05-08 (angr-3zhl, commit 813dbcce3): load_concrete detects when any other symbolic_objects entry starts inside (addr, addr+size) and falls through to a per-byte merge via symbolic_objects + symbolic_spans (endianness-aware). store_concrete still does NOT split or invalidate wider entries on partial overwrite; correctness now lives entirely on the load side. If you ever need to invalidate eagerly on store, the invariant to maintain is: for every byte in [addr, addr+size), exactly one of {symbolic_objects[byte_addr], symbolic_spans[byte_addr]→sym at non-stale offset} contributes. Regression test: memory::tests::test_load_concrete_partial_overlap_later_store_wins.

Leaf/path identity on the pbounce synthetic must NOT be projected as the concrete stdin witness bytes. The find gate is ((acc & 0xff) == 0xee), which leaves the stdin prefix substantial model latitude, so two solvers walking the SAME path legitimately return different satisfying 3-byte prefixes — a test asserting witness-set equality across worker counts (or across a snapshot round-trip) is flaky by construction. Valid projections, in increasing strength: (a) found-state pc set == {target}; (b) leaf COUNT; (c) witness DISTINCTNESS (len({s.posix.dumps(0)[:3] for s in found}) == len(found)) — this catches a run that silently re-collects one leaf twice, which the count alone does not. Used by TestParallelCheckpointFrontier::test_resume_from_fixed_snapshot_is_worker_count_invariant and ::test_resumed_found_states_solve_to_distinct_stdin.

invariant: _get_pending_ancestry (exploration/pending_api.rs) is BEST-EFFORT, not a complete lineage. Rust keeps no state_id->parent map — only RustSimState.parent_id (ONE hop) and StashManager.state_roots (id->root). So the ancestry walk (angr-ph300.25, commit 563e8c772) follows parent links only through states the manager STILL HOLDS: _parent_of checks pending_callbacks (hash lookup) then sm.find_state (stash scan). A fork CONSUMES its parent, so the walk records the parent id it was told about and then stops as soon as that ancestor is gone. Guards: repeated-id break + Self::MAX_ANCESTRY_DEPTH=64 (find_state has a linear all-stash fallback, so an uncapped walk could rescan every stash per hop). The sm.roots() lineage root is always appended when absent, so the result is never SHORTER than the pre-fix [state, parent, root]. Consumers: rust_callback_dispatch.py::_get_pending_ancestry and rust_state_sync.py iterate it to find cached SimState data; they must keep tolerating gaps. If a future need requires a GUARANTEED full chain, the fix is a state_parents map alongside state_roots in stash.rs — but note ~15 sm.set_root call sites and that state_roots already has a leak bead (angr-ph300.26), so a second map inherits the same GC hazard. Regression: pending_api_tests.rs (3 tests).

In exploration/pending_api.rs the three 'load memory as concrete bytes for Python' helpers now agree on refusing to fabricate data for non-concretizable symbolic loads: _get_state_memory (state_api.rs) returns Ok(None); _pending_memory_load returns Err(PyValueError) on both memory-fault (Err arm) AND eval-no-witness (else branch, fixed angr-04tw3.2); _get_pending_memory raises PyValueError immediately (no eval fallback, by design). Never return vec![0u8; size] for a symbolic load — callbacks consuming by length mistake zeros for real data (angr-ph300.19, angr-04tw3.2).

PendingWrite path semantics (memory/mod.rs:29 and tests.rs::test_pending_write_visible_after_flush): add_pending_write defers a store; subsequent loads do NOT see it because apply_pending_writes_concrete/_symbolic in load.rs are intentionally stubbed to return base_value (per lazy-memory-load-overlay-fails — overlay was disabled because it didn't work for sym-write). Only flush_pending_writes() materializes the writes via concretize+ITE; only after flush will a re-load see them. fork() clones the pending list via Vec::clone (mod.rs:298), so writes registered pre-fork are visible in both halves once each flushes. Tests pinning these three invariants: test_pending_write_visible_after_flush, test_fork_pending_writes_visible_in_both_after_flush, test_fork_pending_writes_isolation.

PerformanceTracker (angr/exploration/rust_perf_tracker.py) warmup-split gate: first_* SimProcedure phase twins must be gated on the private _phase_crossing_count (bumped once per real crossing in add_simprocedure_phase when phase=='state_create'), NOT on callback_simprocedure_count. The fast paths in rust_callback_dispatch.py (internal passthrough L667, stale-hook skip L681, deadend fast path L697) and the VEX-fallback increment_simprocedure_count all bump the raw count without recording any phase; gating on it let a fast-path bounce close the warmup window early. Fixed in angr-zi35f.3; covered by tests/engines/rust/test_perf_tracker_warmup_split.py.

try_concretize_triop_rm (vex/transcendentals.rs) must concretize BOTH operands from ONE joint witness — ctx.eval_many(&[a,b]), never two ctx.eval calls. Root cause (angr-z8elx, fixed eb2e508ed): SymContext::eval (symbolic/solving_ops.rs) short-circuits in strict-deterministic mode to self.min(bv,false) and deliberately skips the model cache, so back-to-back evals of two operands return independently-minimized witnesses that need not be jointly consistent. When path constraints correlate the operands (a+b==K), each min is individually feasible but the pair is not; the two assume_true pins then make a SAT context UNSAT and the feasible path is silently dropped (missed state, not a crash). GENERAL RULE for any input-concretization site that pins >1 symbolic value: use eval_many (lex_min_witness under deterministic mode, eval_all_in_model otherwise), because pinning is only sound against a model-consistent tuple. The sibling try_concretize_binop_rm has one operand and is exempt. Regression: transcendentals_tests.rs::concretize_triop_rm_pins_a_joint_witness_under_deterministic_mode (a+b==5, Iop_Yl2xF64, asserts still SAT) — confirmed failing pre-fix.

Native pread64/pwrite64 (syscalls/fd_io.rs NativePread64Syscall/NativePwrite64Syscall) need offset-honoring FileSystem I/O, NOT the append-only FileSystem::write. Added FileSystem::read_at(fd,offset,count) and write_at(fd,offset,data) in state.rs: read_at reads content[offset..] without advancing position; write_at overwrites content[offset..offset+len] and zero-fills the gap when offset>=len. Both leave fd position untouched (POSIX positioned-I/O). pwrite64 gathers ALL concrete bytes before write_at (same no-partial-mutation discipline as writev); symbolic offset/data or non-native/stdin fds fall back to Python. Mirrors posix/pread64.py + pwrite64.py.

When emitting RustBV operators to Z3 (native/angr/src/symbolic/value_z3.rs::to_z3_ast_cached), prefer z3-rs native methods over hand-rolled concat/extract sequences. Rationale: Z3's bv_rewriter has dedicated rules for SignExt/ZeroExt/Repeat/RotL/RotR that fold and propagate efficiently; a hand-rolled equivalent emits more AST nodes that the rewriter must collapse at constraint-assertion time (and may fail to collapse if interleaved with extract/concat already in the input). Concrete examples: ZeroExt already uses inner.zero_ext(bits); SignExt should use inner.sign_ext(bits) (angr-rbnk fix). Pattern to audit next: any other BVOp that materializes via Concat/Extract loops. Search: 'concat|extract' inside the BVOp::* arms in value_z3.rs to_z3_ast_cached match.

Address arithmetic in native/angr/src/procedures/ must use wrapping_* -- [profile.release] sets no overflow-checks, so a plain src + size panics in debug and SILENTLY WRAPS in release (the shipped .so), turning a range test into a wrong answer rather than a crash. Concrete case fixed 2026-08-02 (angr-9ke6b.110): NativeMemmove's overlap check was dst > src && dst < src + size, the one non-wrapping site in memcpy.rs; near u64::MAX it misclassified an overlapping move as non-overlapping and copied forward, clobbering unread source bytes. Wrap-safe spelling of 'dst is strictly inside [src, src+size)' is let d = dst.wrapping_sub(src); d != 0 && d < size -- see fn memmove_copies_backward. Grep new procs for bare + / - on address or address+length operands.

Progress-callback deadended_count is only observable via the PREDICATE explore path (mgr.explore(find=lambda s: False)), which sets drop_terminal_states(False) and keeps terminal states. The plain mgr.run(n=...) and address-find paths call set_drop_terminal_states(True), so deadended states are dropped and deadended_count stays 0 — even with a progress callback. Tests asserting nonzero deadended/avoid/errored counts must use the predicate path. See test_progress_callback_deadended_count and rust_manager.py _explore_with_predicates.

flareon2015_5 gate-on root cause (angr-5rjbq): under the callback-memory-proxy gate, the memory_store / memory_store_symbolic_value Python callbacks are DELIBERATE NO-OPS (state.memory is Rust memory; re-entering run() through the proxy double-borrows). The VEX interpreter's handle_symbolic_store Single branch and handle_concrete_store's use_sym_store branch dispatched stores ONLY to those callbacks, so under the gate the value was dropped outright and read back as structurally concrete <BV8 0>. Gate-off worked only because Python's real memory absorbed it. Fix: buffer_store_for_rust_memory (interpreter/statements_store.rs) buffers such stores into pending_(symbolic_)stores so they flush into rust_memory. INVARIANT: any store the interpreter routes exclusively through a Python memory callback must also land in rust_memory when the proxy gate is on.

RustStateProxy sub-proxy ctors (RustMemoryProxy, RustRegisterProxy, RustSolverProxyPlugin in angr/exploration/rust_state_proxy.py) take an optional python_mgr=None kwarg used ONLY for counter bumps (stats_proxy*). The first positional arg ('_mgr') is the PyO3 builtin RustExplorationManager which has NO Python attributes — any new instrumentation that touches Python-side counters MUST go through python_mgr, not _mgr. Construction sites that pass it today: RustStateProxy.regs/memory properties (lines 2813/2827), the proxy gate installers in rust_callback_dispatch.py (lines 2265/2283/2297), and the .copy() methods (lines 352/1085/1162). Adding new construction sites? Pass python_mgr through if you want counter visibility; safe to omit for stand-alone low-level unit tests.

RustSimulationManagerProxy.step_state() (rust_state_proxy.py, E1.b/angr-op0dn.1.2) diverges from SimulationManager.step_state() in two ways that callers must respect. (1) It CONSUMES the stepped state: the Rust pymethod uses StashManager::take_state, so the source state leaves its stash during the step — unlike the Python engine, where step() drops it only after bucketing. (2) Successors are returned as exported SimStates but their Rust twins MUST stay in the _step_out quarantine stash: _snapshot_to_angr attaches a Rust-solver eval fallback keyed on the rust state_id, so draining _step_out would break eval on the returned states. The caller places them with move_state(sid, '_step_out', 'active'). successor_func is unsupported by design (raises NotImplementedError) — the engine never builds a SimSuccessors; techniques needing it must run use_rust_engine=False. successors() likewise still raises.

callback-memory-proxy UNMAPPED-ACCESS semantics, both halves (angr-s0x0v commit 2f807a8c7, supersedes the store-only invariant-proxy-unmapped-write-semantics from angr-ijwp0 commit 2815611e4). Under ANGR_RUST_USE_CALLBACK_MEMORY_PROXY the Rust state IS the memory a SimProcedure sees, so RustMemoryProxy must reproduce angr DefaultMemory semantics ITSELF — 'fall back to Python' is not available. Rule for BOTH load and store: a page neither Rust nor the pre-swap _fallback_memory has mapped => under STRICT_PAGE_ACCESS raise SimSegfaultException(page_base, 'unmapped') via RustMemoryProxy._segfault_unmapped (page base = addr - addr%0x1000, reason 'unmapped' — this is exactly what angr PrivilegedPagingMixin._initialize_page raises; do NOT invent reasons like 'write-miss'); otherwise map on demand (store: *_automap setters; load: RustMemoryProxy._unmapped_read returns a zero BVV). The old load behavior (silently return BVV(0)) is a SILENT divergence: a libc proc dereferencing a garbage pointer reads zeros and sails on where Python segfaults. Any new proxy memory path must route its miss through _segfault_unmapped.

INVARIANT: any new mutable field added to PythonCallbacks (struct defined in native/angr/src/callbacks/mod.rs — dir module since angr-zel8z.2) that needs to be updated AFTER mgr.set_callbacks(callbacks) runs must be wrapped in a shared container (Arc or Arc<Mutex>). The struct derives Clone and the Rust manager keeps a clone. Primitive fields silently desync across the two copies. See inspect-enabled-clone-pitfall for the discovery. Callback Py fields are safe because Clone bumps the refcount on the same Python object; primitives are bitwise-copied and independent.

Any #[pymethods] entry that takes a raw Z3/pointer usize from Python must validate it before deref: use std::ptr::NonNull::new(...).ok_or_else(|| PyValueError...) NOT NonNull::new_unchecked. set_register_symbolic (native/angr/src/state/pymethods.rs) was fixed in angr-ph300.49 — a Python-passed 0 (the guarded absent-AST value in rust_state_sync.py) was UB + Z3_inc_ref segfault. AUDIT SIBLING: engine.rs (~line 129) still does NonNull::new_unchecked(py_z3_ctx_ptr as *mut _) on a Python-provided ctx ptr — same class of bug if reachable with 0/garbage; not yet fixed.

clippy::needless_pass_by_value on a #[pymethods] fn arg (e.g. segmentlist.rs next_pos_with_sort_not_in's sorts: HashSet<Option>) is a FALSE POSITIVE: PyO3 extracts args by value via FromPyObject; &HashSet does not implement the needed extraction (only &str/&[u8]/&Bound/&PyClass do), so the clippy fix breaks compilation. Confirm a fn is internal-only (grep Rust callers) before applying needless_pass_by_value. The 167yo audit bead mis-cited this as actionable. needless_pass_by_value is pedantic, not in the default -D warnings gate, so it never reddens CI anyway.

PyO3 0.27.2 in this project does NOT enable the 'multiple-pymethods' feature (Cargo.toml: features=["py-clone","abi3-py310"]). Consequence: each pyclass may have exactly ONE #[pymethods] impl block. Two valid decomposition moves given that constraint: (A) SPLIT the wrappers across files -> would need >1 block -> feature unavailable -> instead keep thin #[pyo3(signature=...)] wrapper in mod.rs and move the BODY to a pub(crate) fn in a sibling plain-impl module (pattern: exploration/run_loop.rs, pending_api.rs, stepping.rs, resume.rs, helpers.rs). (B) MOVE the entire single block verbatim to one sibling file -> still exactly one block -> works with NO feature. The #[pymethods] block does NOT have to live in the same file as its #[pyclass]; it only must be the sole block and compiled in-crate. Demonstrated angr-0mqkc.5 inc9 (7ac9c0fe2): state/pymethods.rs holds the whole #[pymethods] impl PyRustSimState (~749 lines of thin wrappers), #[pyclass] struct + inner()/inner_mut() plain impl stay in state/mod.rs. Sibling pymethods.rs uses 'use super::*;' (which DOES surface mod.rs's private 'use' imports like RegisterFile/HashMap/AddressConcretizer via glob) plus a few explicit imports (Permission, RustBV, PyValueError, PyAny/PyDict, Arc). Use (B) when moving ALL pymethods of a type; use (A) when splitting them into groups. Adding multiple-pymethods would pull in the 'inventory' crate + change class-registration semantics -- out of scope.

register_python_procedure (native/angr/src/procedures/python_proc.rs): num_args mismatch is silent — the dispatcher's extract_procedure_args extracts EXACTLY the registered count from arg regs/stack; caller's actual ABI count is never checked. So a callable registered with num_args=2 just won't see a third argument that's sitting in RDX. There is no crash, no warning, no truncation error. If you want to validate caller-vs-callee count, add a separate mechanism.

register_python_procedure return-value handling: callable returning -1, a value > u64::MAX, a non-int, or a float all fall back to Python via ProcedureError::Other (extract::() fails). dispatcher counts these as native_proc_stats.python_fallbacks (NOT native_calls), then emits need_simprocedure. So 'callable raised an error' and 'callable returned an invalid value' are indistinguishable from the dispatcher's perspective — both look like a Python fallback to the observer. RAX is left untouched on failure, which is the safe behavior.

rust_irsb_serializer.py serialize_const must special-case any pyvex const whose Rust PyVexConst variant uses named fields other than 'value'. U128 and V128 both deserialize into {low, high} structs (native/angr/src/vex/pyvex_bridge.rs PyVexConst::U128/V128); V256 uses {value: [u64;4]}. The generic '{tag: Ico, value}' fallback silently mismatches these serde shapes. Fixed U128 in angr-1yge9.6.

Iop_QDMull16Sx4/32Sx2 (signed doubling saturating widening multiply, NEON VQDMULL, (I64,I64)->V128) map to IROp::VQDMull{elem,count} in vex/opcode_map.rs. Implemented by vec_qdmull in ops_vec_permute_mul.rs: same full-lane widening layout as vec_mull (even=false, always signed), plus 2 and signed saturation to 2N bits. Saturation only fires on MINMIN (both -2^(N-1)): doubled product 2^(2N-1) clamps to 2^(2N-1)-1. Symbolic path widens inputs to out_width+2 bits before doubling to avoid overflow, then reuses saturate_lane_symbolic (widened to pub(super) in ops_vec_saturate.rs). Only 16Sx4/32Sx2 exist in libVEX; the QDMulHi/QRDMulHi high-half family is still unmapped.

rangemap + panic=abort makes an inverted Range a PROCESS ABORT, not a Rust panic Python can catch. native/angr/Cargo.toml sets [profile.release] panic="abort", and rangemap::RangeMap::{insert,remove} both assert!(range.start < range.end). So any 'address..address + size' built from Python-supplied values without a checked_add guard is a DoS vector, not a wrong-answer bug. Fixed in SegmentList::release (native/angr/src/segmentlist.rs) for angr-9ke6b.199; SegmentList::occupy already had the guard. Convention adopted at both sites: 'let Some(end) = address.checked_add(size) else { return; }' tagged // SILENT(cat-a) -- a wrapping range describes no real region, so a no-op is the correct answer, not a degraded one. If a new SegmentList-like RangeMap wrapper is added, grep for unchecked '+ size' in range construction first.

RDTSC determinism (angr-9ke6b.173): the simulated timestamp counter is per-RustSimState (field tsc_counter, accessors tsc_counter()/set_tsc_counter() in state/process.rs), NOT a process-wide static. It is carried into the interpreter as VEXInterpreter::dirty_helper_state (DirtyHelperState{tsc} in vex/dirty.rs) by run_interpreter_step_core and written back by apply_interpreter_step_result. INVARIANT: any future stateful dirty helper must put its mutable scratch in DirtyHelperState and add the same seed/write-back pair, or it re-introduces the cross-state/cross-run nondeterminism. Simulated time merges as a MAX watermark in RustSimState::merge (same class as heap_brk/mmap_base) so it never runs backwards, and the per-RDTSC bump saturates rather than wrapping.

readv (NativeReadvSyscall, syscalls/fd_io.rs) has an is_symbolic fast path (angr-myzjx.12): when a fd is open with no concrete content (content_len==0) AND FileSystem::is_symbolic(fd) is true (the stdin model via open_symbolic), it scatters fresh symbolic bytes natively per segment via the shared scatter_symbolic helper — mirroring read.rs's read_symbolic path — instead of falling back to Python. The stdin path (fd==0) uses the same helper. pread64 DELIBERATELY lacks this fast path: a positioned read on a stream model has no clear position semantics, so it keeps deferring to Python. Any new native read-family syscall serving symbolic-stream fds should reuse scatter_symbolic for name/counter consistency.

Iop_RecipEst/Step and Iop_RSqrtEst/Step (FP variants) are emulated as fresh-symbolic per lane — angr Python has _op_fgeneric_RSqrtEst returning BVS and no handler for the others, so matching that policy avoids divergence. Newton-Raphson refinement loops in binaries converge to the exact 1/x or 1/sqrt(x) regardless of seed, so the precision loss is recoverable. Computing 2.0-xy / (3.0-xy*y)/2 symbolically would be MORE faithful than angr Python and could cause cross-engine divergence.

RegisterFile::copy_to_bytes (native/angr/src/arch/mod.rs) zeroes the byte span of every entry in self.symbolic after copying self.data, because RegisterFile::put's symbolic branches never clear the concrete buffer: a register written concretely then overwritten symbolically leaves stale concrete bytes in data. INVARIANT for future edits: the flat register buffer is a CONCRETE-ONLY view — a byte that belongs to a symbolic register reads 0, and the symbolic value travels separately via ExplorationStateSnapshot::get_symbolic_register_names. Corollary for the wider audit family: self.data and self.symbolic are NOT kept mutually exclusive (put's sub-register compose branches deliberately write both), so any new reader of self.data must consult self.symbolic itself — RegisterFile::get and get_offset_u64 do; get_sp_value deliberately does not (documented fast concrete path). Also audited: get_registers_raw has NO Python caller — rust_state_export.py rebuilds registers from get_registers_named + get_symbolic_register_names.

Subregister symbol identity (angr-21vi5/4ju9e Layer 2): when importing a symbolic register from Python into Rust, route the FULL claripy AST through claripy_to_rustbv, NOT the raw-Z3-ptr path (PyRustSimState::set_register_symbolic). set_register_symbolic wraps the whole register value as an opaque RustBV::Symbolic{id:0}, so rustbv_to_claripy_memo (CLARIPY_AST_CACHE miss on id 0) mints a fresh BVS on export — losing any embedded leaf symbol (e.g. state.regs.ecx=BVS('ecx') -> rcx becomes opaque, exports as rcx_N not ecx). FIX: PyRustSimState::set_register_symbolic_ast(name, ast) calls claripy_to_rustbv which interns every leaf BVS into the shared cache (store_claripy_ast_with_info), so it round-trips. rust_state_sync.py register import prefers it (hasattr guard for old .so). Mirrors the memory-import path (_import_symbolic_to_state). Identity preservation depends on a NON-zero RustBV::Symbolic.id keyed into CLARIPY_AST_CACHE.

INVARIANT: Arch::register_names() (the per-arch REGISTER_NAMES const in arch/amd64.rs, x86.rs, arm.rs, ...) is the set of registers that cross the Python boundary — it drives register_names_for_arch (Python _supported_register_names in rust_state_sync.py) and RustSimState::export_full's named_registers. It is a strict SUBSET of that arch's CANONICAL table, and every entry MUST be <= 16 bytes: ExplorationStateSnapshot::get_registers_named carries each value as a u128, and RegisterFile::get's concrete read composes bytes with 'value |= (byte as u128) << (i8)', so a wider register silently yields garbage (release-mode shift masking) instead of failing. This is why x86/AMD64 'fpreg' (64 B, 8 x87 slots) is deliberately absent while fptag/fpround/fc3210/ftop were added in angr-9ke6b.6 (commit d24970d34). Gated by arch::tests::register_names_all_resolve_and_fit_in_u128 in arch/mod_tests.rs. Corollary for future audits: a CANONICAL entry missing from REGISTER_NAMES is a silent state.regs. omission bug UNLESS it is >16 bytes.

RustRegisterProxy._cache (per-name read cache, rust_state_proxy.py ~line 808) is NEVER invalidated when the underlying Rust state steps. Any code that holds a long-lived RustRegisterProxy across Rust steps (e.g. a state cached in _state_cache with a proxy as its registers plugin) will read STALE register values. The X_proxies() stash accessors mint FRESH proxies (empty cache) so they read live. INVARIANT: when re-using/materializing a state whose registers plugin is a RustRegisterProxy after Rust has stepped, clear proxy._cache (and rebind _state_id) or reads silently return pre-step values. RustRegisterProxy.copy() returns a fresh proxy (empty cache, but preserves the SOURCE _state_id). See register-proxy-stale-cache-root-cause and invariant-set-register-ip-syncs-pc.

RegisterFile (native/angr/src/arch/mod.rs) stores registers as data: Arc<Vec> (NOT Vec) since angr-6t8z3.1. fork()/derived Clone share the buffer O(1) via Arc::clone; the deep copy happens lazily on first write. EVERY &mut self register write MUST route through Arc::make_mut(&mut self.data) or it will silently leak across the fork boundary (CoW broken). Current write sites: put()'s three concrete-write loops + copy_from_bytes(). set_ip/set_sp delegate to put; merge mutates only self.symbolic. Reads index self.data[..] directly (Deref). Serde shadow RegisterFileData.data stays Vec: From uses Arc::unwrap_or_clone, From wraps Arc::new. Faithfulness gate: test_register_file_fork_cow_isolation in mod_tests.rs. Measured state_fork bench -9.6%. Extends invariant-symbolic-memory-fork-fields CoW discipline to registers.

remove_technique native teardown (angr-w9zce): the Rust manager has NO per-technique unregister. rust_techniques.py::_disarm_native_technique resets whole native categories to default then re-arms the surviving _active_techniques via _arm_native_technique. Categories + their reset entry points: selection -> set_state_selection_fifo; Explorer -> set_find_addrs([])/set_avoid_addrs([])/set_num_find(1); CheckUniqueness -> disable_uniqueness_filter; LoopSeer/LengthLimiter/Timeout/ManualMergepoint all share the native_techniques vec whose only entry point is clear_native_techniques (clear-all), hence clear-then-re-arm. Category membership lives in the frozensets _SELECTION_TECH_NAMES / _FIND_AVOID_TECH_NAMES / _UNIQUENESS_TECH_NAMES / _NATIVE_QUEUE_TECH_NAMES — INVARIANT: any new branch added to the _arm_native_technique if/elif chain must be added to the matching frozenset or its effect survives removal silently. Scoping per category is deliberate: a blanket reset would clobber a manual set_state_selection_random/set_find_addrs made outside the technique API.

M2 repeat-run result equality (angr-op0dn.10.4) is measured by tests/benchmarks/repeat_run_equality.py, and the ONLY two projections it compares are (a) stats['found_pcs'] — the found-state pc multiset, opted in per-child via env ANGR_BENCH_FOUND_FINGERPRINT=1 (spawn inherits it) — and (b) the bench's stdout (evaluated model bytes / flag). Do NOT swap in content_fingerprint.fingerprint_terminals: it is vacuous on Rust found states (see avoid-content-fingerprint-on-found-states). The reduction MUST stay hashlib-backed (content_fingerprint::_stable_digest), never builtin hash(), because each repeat is a separate PYTHONHASHSEED-randomized process. equality_verdict([]) returns equal=False on purpose: a bench whose repeats all crashed must fail the gate, not pass it vacuously. The harness carries ZERO wall-clock assertions by design — timing variance is out of M2 scope. Measured 2026-07-13: 20 runs x {fauxware, ais3_crackme, defcamp_r100} with deterministic=True are result-identical on both projections (tests/benchmarks/repeat_equality_numbers.json).

EXTENDED_IROP_SUPPORT is an INVERSE-POLARITY option gate for the Rust engine: the divergent configuration is the one where it is UNSET, not set. It only ever widens Python's IR-op table (angr/engines/vex/claripy/irop.py::vexop_to_simop auto-generates a SimIROp from the op name when extended=True, raises UnsupportedIROpError when False). Set — and it ships in EVERY mode bundle, so it always is — Rust honors it transparently: it runs the op natively, or defers the block to Python where the widening applies. Unset, the user is asking for the NARROW table and the Rust interpreter has no narrow mode, so it would execute an op Python would have refused. Hence it lives in _REQUIRED_OPTION_NAMES (refused by absence), not _RAISE_OPTION_NAMES (refused by presence), in angr/exploration/rust_manager.py. rust_unsupported_options() folds both polarities and reports a miss as 'unset EXTENDED_IROP_SUPPORT'. Same trap shape as CGC_NON_BLOCKING_FDS (see invariant-cgc-fdwait-option-polarity). When adding a SimOption gate, ALWAYS ask which polarity diverges — a default-bundle option can only ever diverge in the unset direction. TEST-PROBE COROLLARY (absorbed in the R4 merge): any test probing angr.exploration.rust_unsupported_options() with a synthetic option set MUST include EXTENDED_IROP_SUPPORT -- since angr-op0dn.14.7 its ABSENCE is itself an unsupported condition, so a bare probe like rust_unsupported_options({o.SOME_OPTION}) never returns []: it returns ['unset EXTENDED_IROP_SUPPORT'] and the assertion fails for a reason unrelated to the option under test (every real state carries it -- it ships in every mode bundle). Pattern: define a _BASE = {'EXTENDED_IROP_SUPPORT'} constant and probe with _BASE | {option}. See tests/engines/rust/test_mode_bundle_options.py.

invariant-reset-for-stage-clears-all-stashes: RustExplorationManager::reset_for_stage (exploration/state_lifecycle.rs) must (a) sweep EVERY stash name except STASH_ACTIVE — never a hardcoded name list; the old list omitted STASH_PRUNED and all technique stashes (cut/spinning/timeout/not_unique/copies/merge_waiting*), keeping stage-1 states and their Z3 solver clones alive for the whole session — and (b) unindex()+remove_root() each dropped active state; a bare VecDeque::retain() bypasses state_index/state_roots so state_stash(dropped_id) keeps answering 'active' and both maps grow unboundedly across multi-stage explores. Any code that removes a state from a stash by hand must mirror drop_state_from_stash (manager_methods.rs): take_state_from + remove_root. Covered by reset_for_stage* tests in exploration/state_lifecycle_tests.rs (angr-ph300.26).

Constraints imported from Python via the Z3-ptr fast path (exploration::constraints::import_python_constraints, the shared body behind BOTH _add_constraints_to_state and _add_constraints_to_pending since angr-9ke6b.71) used to be recorded TWICE: add_constraint_raw logged them in the residual sink (SymContext::local_constraints.non_bv_assertions) AND the call site pushed an assumed IR pair. Invariant: the residual sink is ONLY for constraints with no RustBV form. Anything reconstructible from the assumed IR must go in via add_constraint_raw_assumed (constraint_ops.rs), which skips the residual push. Violating this silently breaks SymContext::unsat_core_assumed, which asserts residuals UNGUARDED (they have no claripy AST to blame) — a double-listed constraint is then pinned outside its assumption literal and the unsat core comes back EMPTY. Symptom looked context-dependent (only after a real RustExplorationManager swapped the Rust thread-local Z3 ctx for claripy's) because AST-identity dedup happens to catch the dup in a Rust-owned context but not in claripy's. See [[unsat-core-on-demand-not-tracked]].

Rust init-to-main for thin-entry binaries: _resolve_main_address (rust_manager.py) resolves main via (1) 'main' symbol, (2) _start's rdi/edi PUT const (x86-64 __libc_start_main), (3) NEW fallback — entry block's direct Ijk_Call constant target when in main_obj && != entry && not a SimProcedure. The simproc guard is what keeps dynamically/statically-linked __libc_start_main binaries safe: their entry calls __libc_start_main which angr hooks as a SimProcedure, so fallback 3 skips it and fallback 2 (rdi parse) handles them. Only symbol-less direct-'call main' entries (CGC/DECREE) hit fallback 3. Inert for the benchmark corpus (all have main symbols or rdi parse). If you add a binary whose entry directly calls a non-main helper before main, this could mis-resolve — verify with mgr._resolve_main_address().

invariant-restore-plugins-template-walk: _restore_plugins_to_state's template selection must walk ancestors in proximity order, never picking an arbitrary cached state. Acceptable templates: (1) state_id itself, (2) snapshot.parent_id, (3) tracked root via _state_roots/get_state_root, (4) ANY cached root (not descendant). Falling back to a forked descendant is a correctness bug — descendants carry per-fork plugin mutations (posix.fd, heap allocations, fs entries) that must not leak across paths. Why: angr's plugin model says forks have independent plugin state; collapsing them to a wrong template silently cross-pollinates branches. How to apply: when adding new plugin-restore call sites, always go through _find_plugin_template_state (or pass snapshot_parent_id if you have a snapshot).

IROp::result_type() (vex/ir/ops_def.rs) must derive packed-vector widths from elemcount via the Self::width_total_to_type helper, never hardcode IRType::V128. The hardcoded arm was wrong in BOTH directions, not just the AVX2 one the audit bead flagged: opcode_map maps VAdd/VSub/VMul/VShlN/VShrN/VSarN/VCmpEQ/VCmpGT at D-reg NEON 64-bit totals (Iop_Add8x8 -> I64) as well as Q-reg/SSE 128 and, for VAdd/VSub only, AVX2 256 (Iop_Add8x32/16x16/32x8/64x4). Whenever an arm of result_type hardcodes a width, cross-check the corresponding parse_opcode arm in vex/opcode_map.rs for the full set of mapped shapes -- the two files are independent sources of truth and drift silently, because result_type is only consulted on the Err() fallback path of interpreter/expressions.rs (sizing a fresh-symbolic value) plus IRExpr::result_type in vex/ir/ast.rs, so a wrong width produces no test failure. The regression test test_packed_lane_result_type_tracks_mapped_width in vex/ir_tests.rs pins this by driving expectations through parse_opcode; extend it rather than writing a fresh literal-IROp test. Widening arms need their own rule: VMull{even=false}/VQDMull double lane width (2elemcount) while VMull{even=true} (Iop_MullEven) halves the lane count as the width doubles (elem*count). Remaining known hardcoded-V128 arms with an explicit 'for now' caveat: VMin/VMax/VAbs/VFAdd/VFSub/VFMul/VFDiv/VFSqrt/VFAbs/VFMin/VFMax.

invariant-resume-fork-base-must-precede-guard (FIXED angr-khpsh, commit on rust-symex 2026-07-22): in exploration/resume.rs, ALL THREE resume entry points now derive the deferred-fork base from a state carrying NEITHER the branch guard NOR the deferred forks' taken-path constraints. Concretely _resume_after_simprocedure and _resume_after_symbolic_branch build fork_base = pending.pre_callback_snapshot.unwrap_or_else(|| state.fork()) BEFORE calling apply_deferred_fork_constraints(&state, ..); _deadend_pending_callback never calls it up front at all and passes the parking state as MaterializeForkCtx::guard_sink. Any future edit that hoists a constraint-application above the fork_base binding silently prunes every snapshot-less deferred fork's unexplored side to STASH_PRUNED (it becomes trivially UNSAT). Regression: resume_tests.rs::snapshotless_resume_keeps_deferred_fork_live_in_every_entry_point (parity across all three entry points, no snapshot). Same bug class as angr-ph300.9 but for taken-path constraints rather than the branch guard.

Retiring a native-proc Python bounce can MOVE the bounce rather than remove it — the ZeroPy gate is per-BENCH (zero crossings), but the census is per-SITE. Concrete case (angr-gorvf.13, iter145): widening native open to concretize symbolic pathnames (like Python's open, which solver.evals the path and does not constrain it) retired the open crossing on fauxware, but the fd it then creates has no backing content, so NativeRead immediately declined with Other('read from fd=N has no concrete content') — bounce count still 1, gate still fails. LESSON: before claiming a bench flips, re-run it and re-read the fallback counters; a proc that ALLOCATES a resource (fd, FILE*, heap chunk) can hand the next proc an unmodelable one. Cheapest way to get the exact decline: RUST_LOG='rustylib::exploration=debug,off' prints 'Native procedure returned error, falling back to Python: ' (the *_fallbacks_by_name counters only bucket by variant). Follow-up: angr-gorvf.15.

Retiring a dead PythonCallbacks entry is a FIVE-place edit, not two (angr-9ke6b.218 item 1, commit 2a6643a07). Deleting PythonCallbacks::call_ alone leaves the field alive because callbacks/mod.rs drives fields through the with_callback_fields! macro list — the field must be dropped from that list AND from the struct AND its set_ pymethod AND the Python registration in rust_manager.py::setup_callbacks AND the matching gil_profile::CallbackSite variant (which requires bumping CallbackSite::COUNT and the all() array — COUNT is a hand-maintained const, so a stale one is a compile error in all(), which is the good failure mode). Deleting a CallbackSite variant is safe for the ZeroPy gate: run_zeropy_gate.py spells GIL_CLASSES out explicitly and the per-site gil_work_ns_callback keys are generated from CallbackSite::all(), so a removed always-zero site just stops emitting a key nobody reads. Check for a dispatch_tests.rs 'callback not set' table entry too — it names the method by hand.

Invariant for Reverse/Concat Z3 emission in native/angr/src/symbolic/value_z3.rs: any Reverse-related code change MUST include a Z3 round-trip test that pins the inner BV to a concrete value and asserts ctx.eval returns the byte-reversed value. Cargo-only structural checks (e.g. 'parts assemble in this order') won't catch the bug class because Z3 silently folds mis-shaped concats back to x via its bv_rewriter. Pattern: test_reverse_z3_emission_{16,32,64}bit_leaf and test_reverse_z3_emission_concat_of_bytes added 2026-05-19 in value_tests.rs.

tests/benchmarks/run_single.py::_run_in_child surfaces partial Rust diagnostics on failure. The _collect_rust_diagnostics() helper is called from MemoryError handler, generic Exception handler, and the success path; ok=False returns now include 'stats', 'perf_report', 'peak_memory_mb'. Main run_example() also calls _dump_counters_json / _dump_counters_table on the FAIL path when --counters-json/--dump-counters is set and stats are populated. Backwards-compatible: downstream (run_regression.py, bench_diff.py) gates on result.get('ok') first, so adding 'stats' to error dicts is a strict superset. Concrete near-term use: lets you attribute work done by mid-flight-crashing benches (e.g. CADET_00001 IndexError after buffer-overflow phase fired 3 native CGC syscalls). Pattern to apply when adding more crash-prone benches or characterization tooling: don't gate stats collection on ok=True; the rust_mgr_instance counters survive an exception in solve.py since the Python exception unwinds the bench frame, not the engine state. Lands angr-qcsg, commit edde63e2b.

run_single.py's Rust engine-swap monkeypatch (patched_simulation_manager) must exclude ONLY /angr/simos/ frames, not /angr/callable.py. The simos frame is where angr executes the load-time IFUNC/IRELATIVE resolver through a Callable (angr/simos/simos.py irelative_resolver + angr/simos/linux.py eager ifunc path) — those resolver states carry SYMBOL_FILL_UNCONSTRAINED_REGISTERS, which RustExplorationManager._check_raise_options rejects, so busybox_static would fail to load. Excluding all of callable.py (the pre-angr-zbpw0 state) also caught the Callables the BENCHES build, silently running mma_howtouse/flareon2015_10 entirely on the Python engine under --engine rust. Also: Callable.perform_call passes techniques=[]; RustExplorationManager does not accept it, so the patch must pop it (non-empty list => fall back to Python).

RustExplorationManager auto-skips _start->main during construction via _run_python_init_if_needed (rust_manager.py:1449). It runs Python init from entry through __libc_start_main to main, caches the result on disk, then hands the post-main state to Rust. Saves ~180ms per run. Side effect: Rust manager's first exported active state is at main (e.g. 0x40071d for fauxware) while Python's entry_state is at _start (0x400580). Diff-state harnesses must align by address. Disabling the auto-init breaks Rust because it can't run __libc_start_main natively.

Concrete integer arithmetic in the Rust VEX ops MUST use wrapping_/checked_ helpers, never bare / % + << *. Rust checks division overflow even in --release, and the workspace [profile.release] sets panic="abort", so any overflow panic (classic: i128::MIN / -1 in a signed DivMod) SIGABRTs the whole Python process — no catchable PanicException, no errored stash, all exploration lost (no catch_unwind in the step path). Z3 bvsdiv/bvsrem wrap, so wrapping_div/wrapping_rem match the symbolic path exactly. Fixed in divmod_double_to_single (native/angr/src/vex/ops_int_arith.rs) for DivModS128to64, angr-n0xru. Audit-driven bugs of this shape should grep other concrete arithmetic arms for bare operators.

engine="rust" project default (angr-op0dn.14.6, commit d7ed74cc6): the flip swaps the MANAGER, not the SimEngine. AngrObjectFactory.init accepts engine="rust" as a STRING sentinel (any other string raises AngrError); it sets self._rust_default and then resolves default_engine_factory to UberEngine exactly as engine=None does, so block()/CFG/lifting paths are untouched. Env equivalent: ANGR_DEFAULT_ENGINE=rust, read at PROJECT-CONSTRUCTION time by rust_manager.rust_default_engine_env() (NOT at import, unlike _AUTO_DISPATCH_ENABLED/ANGR_RUST_AUTO which is import-time + setter) so monkeypatch.setenv works. simulation_manager()s use_rust_engine default is now the _ENGINE_DEFAULT sentinel (class _EngineDefault in factory.py), NOT False — needed to tell "caller said nothing" from explicit False. When _rust_default, _auto_engine_choice(project_default=True) BYPASSES the global rust_auto_dispatch_enabled() gate: opting a project in IS the switch. Factory getstate/setstate tuple grew to 5 fields (added _rust_default) — any new factory field must be added there too.

INVARIANT: SymbolicMemory.dirty_pages (FxHashSet field in native/angr/src/memory/mod.rs) tracks per-state which pages were mutated since the last clear. Re-initialized empty on fork via the dirty_pages: FxHashSet::default() lines in SymbolicMemory's fork/clone constructors (mod.rs). Updated on every store via self.dirty_pages.insert(page_num) in the symbolic and concrete paths of memory/store.rs. get_dirty_pages() in mod.rs is the in-crate reader. Exposed for the PENDING state via _get_pending_dirty_pages and _clear_pending_dirty_tracking (exploration/pending_api.rs). The concrete-page reader is _pending_memory_load_page; the symbolic-page reader is _pending_memory_load_symbolic_page (pending_api.rs, added 2026-05-10 by angr-3tek.2). All three are USED by _replay_rust_dirty_pages (rust_state_sync.py) to invalidate-and-replay the cached Python SimState on every callback. Do not add yet another sync layer — this one is sufficient for NativeRead/NativeWrite. (Symbol-anchored per refactor-memory-sweep-rule; the original raw lines memory/mod.rs:88, :345, store.rs:92/103/132, pending_api.rs:227/231/431/438 all drifted ~40-60 by iter52.)

Engine dispatcher (angr-op0dn.14.5.2): factory.simulation_manager takes tri-state use_rust_engine (True=loud Rust, False=Python, None=auto). Auto routing predicate is rust_engine_eligible(project, states, kwargs) in angr/exploration/rust_manager.py — it reuses rust_unsupported_options + unsupported_rust_manager_kwargs + rust_supports_arch (native arch_supported pyfunction, engine.rs, backed by arch_from_name) + _unsupported_inspect_events. Auto mode is OFF by default; flip it with set_rust_auto_dispatch(True) or ANGR_RUST_AUTO=1 (angr-op0dn.14.6 will flip the default). Route is recorded on the returned manager as mgr.dispatch_reason. INVARIANT: add any new 'Rust refuses this' signal to rust_engine_eligible too, or the flip re-introduces a raise.

RustExplorationManager.explore() and .run() do NOT call self.step() per VEX block — they batch through Rust internally (_explore_with_addresses / _explore_with_predicates / _run_predicate_batch). Consequences for the tests/benchmarks/diff_state.py harness:

(1) A manager.step monkey-patch fires only once for the whole exploration, not once per step. To get per-step granularity, replace explore/run with a step(1) loop (set find/avoid via _rust_mgr.set_find_addrs etc., loop while has_active_states and _found_count < num_find). Pattern: _patch_rust_explore_to_single_step in diff_state.py.

(2) The step(1) loop must mirror live exploration's predicate handling. Production _explore_with_predicates / _explore_with_addresses re-evaluate callable find/avoid predicates after every step batch via _evaluate_predicates_on_active() (rust_state_cache.py:191). After manager.step(1), if getattr(manager, '_find_predicate', None) or getattr(manager, '_avoid_predicate', None), call manager._evaluate_predicates_on_active(). Otherwise stdout/state-based predicates (csgames2018, sym-write) silently never fire because Rust can't evaluate Python callables. Termination via manager._found_count() already counts both Rust-native and predicate-matched finds.