invariant / 2

ite_builder.rs has a private loads_match helper (fn loads_match in memory/ite_builder.rs) used by build_strided_ite_tree / build_balanced_ite_load_inner / build_ite_tree_inner to skip ite(c,v,v)->v construction. Conservative by design: Concrete by value+width, Symbolic by id, Constrained by id+value, Expression by Arc::ptr_eq(operands)+op==op. NEVER walks deeper into expression trees — adding deep structural eq here would silently change semantics elsewhere if it's mistaken for a full RustBV PartialEq impl. RustBV's PartialEq (impl PartialEq for RustBV in symbolic/value.rs) intentionally only handles concrete pairs. If extending dedup later (e.g., Or-condition grouping for symmetric N-way fan-outs as the bead originally suggested), add a NEW helper rather than widening loads_match — call sites here rely on the conservative semantics. (Symbol-anchored per refactor-memory-sweep-rule; raw ite_builder.rs:8 and value.rs:3215 both drifted.)

Invariant in native/angr/src/memory: when a Python state's page is in Rust's lazy_regions but NOT yet in the pages map, the first store via SymbolicMemory::store_concrete_automap_internal (memory/store.rs) auto-maps a zero page on demand. This means angr/exploration/rust_state_sync.py CAN skip eager map_memory_data for all-zero pages PROVIDED add_lazy_region is still called. Skipping add_lazy_region as well would cause MemoryError::Unmapped on the first store. Used in fix for angr-9maq (commit fced54a07).

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).

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.

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). COROLLARY (angr-sqfj8.32, angr-03vl4.10): RustExplorationManager holds live states in THREE places -- the stashes, pending_callbacks, and pending_parallel_bounces -- so a manager-level mutator that updates states in place MUST walk all three, via RustExplorationManager::all_live_states/all_live_states_mut (exploration/run_loop.rs) rather than stashes_mut() alone. A parked callback owns three solver contexts that each become a stash state's solver on resume: pending.state and pre_callback_snapshot (both RustSimStates, so all_live_states yields them) plus every fork_snapshots entry, which is a raw BranchSnapshot outside that iterator's reach -- see constraints::apply_fork_snapshots_deterministic, the seam that covers exactly that third carrier (build_unexplored_fork materializes it via fork_from_snapshot, so it never inherits from fork_base). See invariant-config-broadcast-covers-pending for the general rule.

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).

Rust tests cannot observe a log::warn! emission in this test binary, and must not try to count its arguments either. Two independent reasons: (1) log::set_logger is a process-global one-shot already claimed by engine_tests.rs::set_rust_log_level_accepts_levels_and_specs, so a capture logger installed elsewhere races it non-deterministically (the convention state/tests/merge_scalars.rs, symbolic/constraint_ops_tests.rs and symbolic/constraint_ops.rs::dedup_backing_of_ptr already document: assert on the predicate, not the line). (2) Less obvious, and the reason a first attempt at callbacks/dispatch_tests.rs::warn_page_set_poisoned_speaks_once_per_latch failed: with no subscriber installed, log::max_level() is Off, so the log::warn! macro never evaluates its arguments -- a closure/expression passed as a log argument (e.g. warn_page_set_poisoned's 'detail: impl FnOnce() -> String') is invoked ZERO times in a correct build, not once. So 'assert_eq!(calls, 1)' on a lazily-built log argument is wrong by construction; only the upper bound ('<= 1', i.e. never twice) is assertable, and that is the half a dedup-latch regression would break anyway. Applies to every SILENT(cat-b)/(cat-c) site whose tag mandates a log::warn!: test the latch/atomic or the predicate the warning reports on, never the emission.

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.

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. Since angr-5mnx3.18 the admission is RESERVED with a compare_exchange loop (worker::reserve_admission), not decided from a plain load and fetch_add-ed afterwards: the old check-then-act let W workers each spend the same stale pending snapshot, so the bound was soft by a MULTIPLE of the worker count, not the documented workers-1. It is now soft by exactly ONE (the reserving worker's own parent discount) regardless of W -- the seed count stored into pending at wave start is still uncapped. 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.

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.

Orphaned bd-memory citations in source comments are a live rot class that RECURS AFTER EVERY PRUNE ROUND (~/angr-memories rounds delete keys comments still cite) -- re-run this sweep as part of each prune. DETECT (final form, angr-9ke6b.240): grep -rhoE '[a-z][a-z0-9]*(-[a-z0-9.]+){2,}' over native/angr/src + angr (the DOT inside the char class matters -- keys like v5a5-slice-4c.3-retry-... are invisible without it; the older 6-prefix regex (invariant|avoid|disk|benchmark|core|rust) missed 22 live keys), then 'bd recall ' EACH token. Do NOT diff against a 'bd memories' dump -- its listing format gives false negatives and keyword search has recall gaps. History: angr-9ke6b.36 found 5/8 dead in claripy_bridge/mod.rs; the repo-wide sweep (angr-9ke6b.239) found 13 more. REPAIR ARMS (per bd-memory-citation-repair-pattern; of the 13, only ONE could be repointed at a live memory): (1) the comment ALREADY states the rule in full -> just delete the dead backticked key, do not invent a replacement memory (9 of 13); (2) the rule lives elsewhere in-repo -> re-anchor at that SYMBOL, not a key (interpreter NEON sites now cite the OpError::UnsupportedNeon rustdoc; perror.rs/write.rs cite the 'Fd-table sync invariant' section of the procedures::read module doc); (3) repoint at the live memory covering the same rule, or inline the one-line rule. Corollary: when a module-doc numbered invariant is itself the anchor other files cite BY KEY (callbacks/mod.rs invariant 4, cited from rust_callback_dispatch.py and rust_state_export.py), retitle the heading to be self-describing and have citers name the heading; and soften any section header promising 'each invariant cites the bd memory key' once bullets lose their key (symbolic/context.rs, symbolic/lineage.rs). EXPECTED NON-KEY TOKENS -- do not 'repair' them: the in-file anchor labels in state/mod.rs (state-id-never-reused, state-metadata-dataclass, arc-make-mut-cow, arc-collection-iter, arc-make-mut-fresh-context) and exploration/state_lifecycle.rs (state-cache-pinning, state-lifecycle-stats-api), whose module headers say they are anchors not bd keys; Sphinx :ref: labels such as rust-engine-api-stability (docs/advanced-topics/rust_engine.rst); and the vex-engine-z3 cargo feature name.

INVARIANT: adding a MemoryError variant (native/angr/src/memory/mod.rs) requires triaging its disposition at the interpreter's two dispatch matches — VEXInterpreter::try_rust_memory_load (expressions_loads.rs) and try_rust_memory_store (statements_store.rs). Both end in a catch-all 'Err(e) => Err(CbExecutionError::Memory(e))', and CbExecutionError::Memory maps to FallbackStrategy::Panic (execution_error.rs::strategy), so a new variant is TERMINAL by default — it errors the whole state instead of degrading to Ok(None)/Ok(false) like Unmapped/UnmappedPageInRegion/SymbolicAddress. MemoryError is #[non_exhaustive], so the wildcard is required and the compiler cannot force the decision (unlike CbExecutionError::strategy, which is wildcard-free). SizeTooLarge shipped mistriaged this way for two review rounds while check_access_size's own doc promised a Python bounce (angr-0jh0j.83).

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. EXTENSION (angr-fs8kb.71): class 3 is not only for scalars — it is where any per-path STACK belongs too. native_resume_stack (angr-sqfj8.86) and call_stack both carry warn_on_diverge + #[merge_manual] with a hand-written *_diverges fn in fork.rs, because a silently dropped branch's frames corrupt that path's return flow with no diagnostic, and because the mechanical !=-based body does not fit. Two reasons it does not fit, and they generalize to any future class-3 aggregate: (a) an element type may have no usable PartialEq (NativeResumeFrame holds RustBVs whose PartialEq is documented non-reflexive for symbolic values), and (b) an element may carry per-path NOISE that must be excluded or the warning fires on every merge and says nothing (CallStackEntry::stack_ptr — two branches reconverging at one pc legitimately recorded different SPs at the same call site; call_stack_diverges compares only depth + the call_site/callee/return triple, which is what interpreter::exits' is_ret/is_empty arm actually reads). The same noise argument is why merge's inspection check is scoped to 'enabled_mask only'. Reachability note worth keeping: the default Python-facing RustExplorationManager.merge() groups candidates by PROGRAM COUNTER alone (_merge_native in angr/exploration/rust_manager.py), not by call stack, so a cross-call-history merge is the ordinary case, not a misuse.

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.

Copying a RustSimState for a merge input must use RustSimState::clone_for_merge, never fork(). fork() intentionally resets the three removal-tombstone sets (removed_hooks / removed_sim_options / removed_env_keys) because a child has removed nothing relative to itself yet — but RustSimState::merge subtracts exactly those sets to keep one branch's remove_hook/set_option(_,false)/unsetenv from being resurrected by a sibling. Forking before merging therefore silently defeats the angr-9ke6b.121 tombstone fix. That is exactly what _merge_states (exploration/state_lifecycle.rs) did until angr-sqfj8.33: RustSimState::merge was correct but nothing reached it with tombstones intact, so the whole manager-level / register_merge_point path resurrected removals. Generalization: when a unit test covers a low-level primitive directly, check that the production entry point does not pre-process its inputs in a way that neuters the invariant — add the test at the entry point too.

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.

MIRROR-PAIR SWEEP RULE (angr-5mnx3.67): when a fix hardens one member of a documented mirror pair, apply it to every sibling in the SAME commit and re-read the shared parent module's doc. Found instance: angr-j60q0.2 hardened VEXOps::vec_float_lane_op's over-arity debug_assert! into OpError::UnsupportedVectorOp; the sibling VEXOps::vec_int_lane_op (vex/ops/vec_int_lane.rs, whose own module doc says 'Mirrors ops/vec_float_lane.rs for the integer family') landed the same day and kept the debug_assert!, leaving a release-mode buf[idx] OOB process abort for any future IntLaneOp with arity() > INT_LANE_OP_MAX_ARITY. Worse, vex/ops/mod.rs's Panic Policy header then claimed angr-j60q0.2 hardened 'the packed-vector paths' (plural, unqualified) — the parent doc asserted a parity that only half existed, so a later reader auditing the int path would conclude it was already covered. Two checks when writing such a fix: (1) grep the fixed symbol's module doc for 'Mirrors'/'parallel to'/'sibling' and fix those files too; (2) grep the parent module doc for a PLURAL claim about the family and either fix the sibling or scope the claim to the one member actually covered. Applies beyond debug_assert! — any per-family hardening (typed-error conversion, overflow spelling, silent-fallback tagging) has this shape. Cf. debug-assert-triage-policy, angr-macros-call-site-invariants.

Mirror pattern for cross-mixin invariants in Rust rustdoc (angr-a2br.1.5, 2026-06-01; citations repaired angr-9ke6b.122, 2026-08-03): when the source-of-truth contract lives in a Python module docstring (the 'Cross-mixin invariants' section of angr/exploration/rust_manager.py's module docstring documents I1-I8), the Rust mirror at state/mod.rs, stash.rs and exploration/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 — cite the docstring SECTION/invariant HEADING ('I8. Exploration-loop termination conditions'), never a raw rust_manager.py:NNN, which drifts: all three mirrors had rotted by 2026-08-03 (state/mod.rs :10-100 for a 10-134 docstring, run_loop.rs :98 for I8, stash.rs :74 for I6); (3) cite the matching regression test name verbatim (TestMmapBaseSync.test_export_path_..., TestStateCacheSizeBound.test_cleanup_state_cache_...) so a future reader can locate it. Corollary: the Python header has SEVERAL Rust citers, so fixing one stale citation means grepping 'rust_manager.py:' across native/ + docs/ and fixing the siblings in the same commit. 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/pymethods.rs::set_registers_bulk). Acceptance: cargo doc --no-deps clean, all tests pass.

When a Rust VEX op/ccall disagrees with real hardware but AGREES with angr's Python engine, the correct outcome is to MIRROR PYTHON and document it — not to fix the Rust side. The two engines interleave within a single exploration (a block can fall back to Python mid-run), so a Rust-only correction makes the answer depend on which engine ran the block; a genuine fix is an upstream angr change that must land on both sides at once. Now seen in two unrelated subsystems: (1) arm64g ADC/SBC carry keyed off cc_dep2 instead of cc_dep3 — see invariant-arm64g-ccall-python-quirk; (2) vec_shift_vec (vex/ops/vec_shift.rs) reading the NEON shift-by-vector amount as UNSIGNED, where libVEX's own header FIXME says ARM32 means it signed (angr-0jh0j.64). VERIFICATION METHOD for this bug shape, both halves cheap: (a) what the front end really emits — .venv/bin/python -c 'import pyvex, archinfo; pyvex.lift(bytes, addr, archinfo.ArchARMEL(), opt_level=0).pp()' on a hand-encoded instruction; ARM32 vshl.s8 lifts to Sar8x8(v, Sub8x8(0, amt)), which is only coherent if a negative count means shift-left; (b) what Python computes — read angr/engines/vex/claripy/irop.py (_op_vector_mapped / _op_mapped / operation_map for the shift+arith+bitwise families). Close such a bead with the evidence plus a differential test pinning the agreement, and a REOPEN criterion naming the upstream change that would break it.

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).

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/payload.rs. When transitioning a byte's state, clear the old sidecar entries before installing the new one. BOTH directions have a setter that does this and both MUST be used: Symbolic->Multi is set_multi_alternatives, Multi->Symbolic is clear_multi_at (drops the multi_objects payload AND the page multi_bitmap bit; safe no-op on a non-Multi byte). Note MemoryPage::mark_symbolic alone is NOT enough — it only touches symbolic_bitmap, so a path that marks a byte symbolic without clear_multi_at leaves state (4). This exact omission has now been found and fixed at every known Multi->Symbolic transition site, so treat any NEW one as guilty until it calls clear_multi_at: SymbolicMemory::merge's collapse-a-Multi-side-into-an-ITE path (angr-0jh0j.31), store_concrete's symbolic branch (angr-9ke6b.95), and import_symbolic_value (angr-6cp06.62 — the live flush_stores / flush_stores_to_rust_memory path, so it silently dropped ordinary symbolic stores at concretized addresses). The failure mode is identical in all three: load_concrete_common's range_has_multi check dispatches Multi-marked bytes to the Multi path BEFORE consulting symbolic_objects, and flush_multi_cells then writes the stale payload back over the new value on export. See also [[invariant-symbolic-byte-lane-lookup]] and [[invariant-every-load-path-gates-multi]]. CORRECTION + DISPATCH ORDER: state (3)'s 'NOT symbolic' holds for the SIDECAR only. set_multi_alternatives (memory/multi.rs) retires the symbolic_objects entry via retire_symbolic_object_at but never calls MemoryPage::clear_symbolic, so a byte promoted Symbolic->Multi keeps BOTH page bitmap bits set -- the symbolic_bitmap and multi_bitmap are NOT mutually exclusive and no code may assume they are. Multi wins by DISPATCH ORDER: every reader must probe Multi before Symbolic (load_concrete_common's range_has_multi gate, assemble_load_with_multi, compute_wider_load_fingerprint, merge::merge_byte_value's is_multi arm all do); a new reader that checks is_symbolic first silently resolves a Multi byte to a retired/absent symbolic object. Readers that want only CONCRETE bytes must check both bits, because install_multi_for_candidates on a never-symbolic byte sets only the multi bit -- read_concrete_bytes_for_lift missing this let the lifter decode MultiPayload::collapse's don't-care concrete_byte as an instruction byte (angr-4r8mh). The reverse transition is deliberately asymmetric: a symbolic store over a Multi cell DOES clear the multi bit (store_concrete -> clear_multi_at), since there a stale bit would win dispatch and shadow the fresh value. Pinned by collapse.rs::test_symbolic_overwrite_clears_multi_cell and test_lift_read_stops_at_multi_byte.

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 for native procedures/syscalls (native/angr/src/procedures/, syscalls/): returning Err(ProcedureError|SyscallError) does NOT roll back state. Per procedures/mod.rs's dispatch doc (rule 5), Python takes over on the SAME mutated RustSimState, so every mutation the handler already applied is visible to — and re-applied on top of — the Python implementation. Consequence: order a handler so irreversible bookkeeping (heap_free/heap_alloc, fd-table updates, position advances) happens AFTER the fallible work, not before. NativeRealloc (procedures/malloc.rs) hit this in angr-sqfj8.82: it freed the old ptr, then copied; a copy failure would have handed Python a state where ptr was already marked freed. Fixed by moving heap_free below the copy_forward call. What cannot be avoided (the bump-heap allocation made to get a destination address) is leaked and documented in place. Sibling rule to invariant-syscall-fd-check-before-count: both are about statement ORDER inside a handler, and both need a test that drives the failure path and asserts the pre-failure state is still intact.

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.

A native SimProcedure's return value must be stored via exploration::helpers::write_proc_return_with_abi (or its two thin adapters, CcSnapshot::write_proc_return for the parallel post-step path and RustExplorationManager::write_proc_return for the single-threaded one) -- never via a raw state.set_register_by_offset(return_register, rv). RegisterFile::put writes exactly rv.width()/8 bytes at the offset and leaves the rest of the slot untouched, so a 32-bit int-return BV (printf/puts/open/strcmp/getopt/posix_memalign/fgetc) leaves the caller's stale RAX[63:32] / X0[63:32] alive -- which no real machine does (angr-fs8kb.40). The widening is an ABI fact, CallingConvention::return_extension() -> ReturnExtension::{Zero,Sign}: Zero (hardware sub-register-write semantics) for amd64/AArch64 and inert on the 32-bit ABIs whose return register is already int-wide; Sign for MipsN64, whose ABI requires a 32-bit value in a 64-bit register to be held sign-extended. Two corollaries: (1) adding a new CallingConvention impl means deciding return_extension, not inheriting the default by accident; (2) do NOT 'fix' an int-returning proc by switching it to arch_word() -- that sign-extends everywhere, and an amd64 int return of -1 is 0x00000000FFFFFFFF in RAX, not all-ones. A value already at or above the register width passes through verbatim, so pointer-returning procs and the invariant-wide-return-needs-python-fallback case are unaffected.

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/support.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. DISCARD RULE (angr-sqfj8.84): the consume half must run even when the value is thrown away -- scanf's suppressed conversions ('%*s'/'%*c') assign nothing but the real scanf(3) still reads those bytes off the stream, so do_scanf calls mint_stdin_bytes for them too and skips only the memory_store and the conversion-count increment. Any native reader with a 'skip/discard this field' path must consume rather than 'continue', or the fd-0 cursor desyncs and the NEXT conversion re-reads the seed from the wrong offset.

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::compare_bytes (only when stop_at_null && its explicit unbounded parameter — a caller-bounded strncmp/strncasecmp may legitimately compare n non-null bytes at ANY n, so it must NOT assert this). Deriving unbounded from the window length instead was angr-fs8kb.36: max_len >= MAX_STRCMP_LEN is also true for strncmp(a,b,4096), which pruned valid unterminated-but-equal buffers. Both flags are now explicit parameters; never re-derive one from max_len. (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,n) may compare n non-null bytes at any n, so the caller-bounded variants pass require_null=false / unbounded=false. Relatedly (angr-fs8kb.36), strncmp/strncasecmp no longer clamp n to MAX_STRCMP_LEN — a clamped window answers for 4096 bytes while claiming to answer for n — so n > MAX defers to Python via check_max, the same shape strnlen already used. 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; the SyscallOutcome/SyscallError/NativeSyscall vocabulary it dispatches through lives in the sibling syscalls/support.rs and is re-exported, so crate::syscalls::X paths are unchanged) 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 declared in mod.rs just above NativeSyscallRegistry::new. See the seven register_syscalls! invocations inside NativeSyscallRegistry::new (AMD64/X86/ARM/ARM64/MIPS32/MIPS64/CGC, each under its own banner comment) for live lists; do NOT enumerate them in memory (drifts within weeks).

Native-syscall vs Python-procedure divergence policy (rust-symex). Native handlers in native/angr/src/syscalls/ normally MIRROR the angr Python procedure, but there is a standing exception: when the Python procedure's behavior on a degenerate input is silently wrong (accepts a request it cannot honor and reports success), the native handler may instead implement real-Linux semantics and return the kernel's errno-style failure. Established by angr-ttr7 (MAP_FIXED collision: Python returns -1, native unmaps+remaps like Linux) and extended by angr-sqfj8.110 (misaligned MAP_FIXED addr: Python silently floors it to the containing page via page-granular map_region, native returns -1 = EINVAL as Linux do_mmap's offset_in_page(addr) check does). How to apply: justified only when (a) real Linux has an unambiguous answer, (b) Python's answer is silently-wrong rather than merely different, and (c) real toolchains never emit the input, so exploration parity is not actually at risk. Record the divergence in the handler's module doc next to the existing policy list — do NOT leave it implicit, since a future reader diffing against the Python proc will otherwise read it as a bug. Distinguish carefully from a hint-shaped arg (non-MAP_FIXED mmap addr), where round-down IS correct and must stay Python-identical.

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 byte-level whitespace classification in native/angr/src/procedures/ goes through the single pub(crate) helper procedures::ctype::is_c_space (' ' plus 0x09..=0x0d) — grep for is_ascii_whitespace to verify no new site regresses. Since angr-6cp06.1 the table itself is the pub(crate) const procedures::ctype::C_SPACE_RANGES: is_c_space delegates to it and NativeIsSpace consumes it directly (NativeIsSpace can no longer call is_c_space, which takes a u8, because the proc must compare the full arch-word argument), so the two still cannot drift. 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.

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 op_* binary-op wrappers in native/angr/src/solver.rs).

Two escapes: (1) macro-generate a SECOND '#[pymethods] impl' block -- needs the pyo3 'multiple-pymethods' feature. The crate now enables it (native/angr/Cargo.toml, angr-9ke6b.50), so this escape is open; it was not when binop was written. (2) (the one taken for RustSolverContext) 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)'. Each wrapper shrinks to about three lines.

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.

invariant: a test whose whole assertion is 'nothing happened' (a defensive/no-op branch, an ignored ping, a guard that returns early) must be proven non-vacuous before commit — temporarily invert the input so the branch is NOT taken and confirm the test fails, then restore. Same reasoning as the valgrind/rounding-mode gates' --self-test (AGENTS.md): an assertion that has never been seen to fail is indistinguishable from one that cannot. Worked example: exploration/scheduler_tests.rs::test_wake_worker_out_of_range_id_is_noop asserts PersistentPool::wake_worker with worker_id past job_txs' end emits no upstream WorkerUp within 250ms; swapping the out-of-range ids for 0 must (and does) fail the recv_timeout assert, because a woken worker re-parks and emits a second Quiesced. Without that step the timeout would also 'pass' if the pool were simply dead. SECOND SHAPE (operand choice, angr-0jh0j.40/.43): overflow-guard regression tests must pick operands whose WRAPPING product/sum is benign, not merely huge — otherwise the test passes under both spellings and pins nothing. For a saturating_mul sizecount guard, u64::MAX2 is wrong (wraps to u64::MAX-1, still over the cap, so the oversize branch fires either way); 2^63*2 is right (wraps to exactly 0, which takes the zero-total early-return and reports a successful no-op for a 2^64-byte request). Canonical pair: procedures/fwrite_tests.rs::test_fwrite_size_times_nmemb_saturates_instead_of_wrapping and procedures/fread_tests.rs::test_fread_size_times_nmemb_saturates_instead_of_wrapping. Always mutation-check: swap saturating_mul -> wrapping_mul, confirm the new test FAILS, revert. Release builds set no overflow-checks so the wrapping result is what ships; a checked-profile panic is a second, weaker net.

Registering a native syscall handler on an arch its own call arch-guard rejects is a NO-OP WITH A COST, not a harmless placeholder: the dispatcher runs the native lookup, the guard returns SyscallError::Other, and the state falls back to Python anyway — one extra hop per call, forever. The correct expression of 'this arch isn't supported yet' is to NOT register the number in NativeSyscallRegistry::new (native/angr/src/syscalls/mod.rs). Precedent: MIPS64 stat (5004) / fstat (5005) were correctly unregistered while lstat (5006) / newfstatat (5252) were registered-then-rejected until angr-9ke6b.154 removed them. The governing oracle for the stat family is the STAT_LAYOUT_WRITERS table in syscalls/file_path/stat_layouts.rs (see invariant-stat-family-arch-coverage) — an arch absent from that table must not appear in any stat-family registration. Since angr-6cp06.53 the handlers' guards derive from that table via require_stat_arch, so adding a new arch means adding the writer table entry AND the registration together (there is no longer a separate guard arm to forget). Cross-check tool: for each arch, awk -v a='"ARCH",' 'index($0,a){f=1} f&&/^ \);/{f=0} f' mod.rs | grep Native<X>Syscall vs the STAT_LAYOUT_WRITERS entries.

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/bv_utils.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/bv_utils.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. UPDATE (angr-sqfj8.61, commit 3456b308a): the same wrong answer has a SECOND shape — CONCRETIZE-then-store fallbacks. statements_store.rs::handle_concrete_store, when memory_store_symbolic_value errored, did ctx.eval(&data_val).unwrap_or(0) and wrote that; an unsat/unknown context or a >128-bit value therefore zero-filled while returning Ok(()). Rule extension: an eval-based concretization fallback must NEVER unwrap_or(0) — propagate the original error (Option -> loud Err + log::warn!). Also use symbolic::u128_to_le_bytes with a MAX_CONCRETE_CHUNK (16-byte) guard rather than a hand-rolled (v >> (i*8)) as u8 loop, which silently wraps mod 128 past 16 bytes. Pinned by statements_tests.rs::symbolic_store_fallback_errors_instead_of_zero_filling_when_eval_fails (+ the _writes_concretized_bytes_when_eval_succeeds converse).

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).

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 + angr-03vl4.20 + angr-0jh0j.13: 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; native_technique.rs apply_native_techniques (Timeout arm), evict_active_states (LengthLimiter/LoopBound), park_states_at_address (MergePoint parking, added angr-03vl4.20 — it was missed by the myzjx.25 'all 7 sites' audit because that audit enumerated only the match arms of apply_native_techniques, and MergePoint is handled out-of-band in a helper); 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; manager_methods_snapshot.rs load_snapshot_bytes (bulk self.sm replace, added angr-0jh0j.13). Stash-generic sites (_move_states/_move_state/drop_state_from_stash/_step_state/park_states_at_address) 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, and do NOT trust a per-match-arm audit to have covered helpers called out-of-band from the same loop, nor a per-state grep to have covered a wholesale-replace path. Not a correctness bug (state_id never reused, key stable) — pure over-session memory leak. BULK-REPLACE ADDENDUM (angr-0jh0j.13): the inventory must include wholesale-replace paths, not just per-state removals — load_snapshot_bytes overwrites self.sm and removes no state individually, so a per-state removal grep/audit (angr-myzjx.25's 'all 7 sites') could not see it; it now iterates self.sm.state_ids(STASH_ACTIVE) and notifies before the swap, AFTER steady_config_guard() so states that guard drains back into active are covered. The mirror ARRIVAL side is deliberately NOT routed through push_active/on_fork (unlike helpers.rs::push_to_stash for the Python move/insert APIs): a snapshot restore is a whole-world replacement whose active-deque order the dump preserved on purpose, and a lazily-memoizing policy populates its side table on the next select, so there is nothing to leak on arrival.

Before adding or trusting an IROp arm in native/angr/src/vex/opcode_map.rs or its opcode_map_float.rs / opcode_map_vector.rs siblings (angr-fs8kb.20 moved parse_float/parse_transcendental and parse_vector/parse_vreverse/parse_neon_unimplemented out of the parent), 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_NegF32/Iop_NegF64 -> IROp::FNeg, the unmappable Iop_NegF128 -- IRType has no F128 variant -- and vector Iop_Neg32Fx2/Iop_Neg32Fx4/Iop_Neg64Fx2 exist; there is NO Iop_NegF16, so do not re-copy the old Iop_Neg{F16,F32,F64,F128} brace-enumeration this memory used to carry, corrected in angr-fs8kb.19; 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 (libVEX does emit Iop_QDMulHi*/Iop_QRDMulHi*; see the comment in vex/opcode_map_vector.rs and the opcode_map_tests.rs pins), which is a different thing from unreachable. Its widening sibling IS mapped: Iop_QDMull16Sx4/32Sx2 (NEON VQDMULL, (I64,I64)->V128) -> IROp::VQDMull, implemented by VEXOps::vec_qdmull (vex/ops/vec_permute_mul.rs: vec_mull lane layout + 2 + signed saturation, which only fires on MINMIN; the symbolic path widens to out_width+2 bits before doubling). The mirror-image shape also exists and is INTENTIONAL: an IROp variant that is fully implemented and tested but has no opcode_map producer because libVEX has no such opcode. IROp::ModS/ModU (no Iop_Mod* exists; guests use the combined Iop_DivMod*, and VEXOps::divmod_double_to_single takes its remainder straight from RustBV::urem/srem) and the bare 1-bit IROp::FCmp{EQ,LT,LE} (every real float compare carries a width/lane suffix -> FCmpScalarLane/FCmpVecPacked; suffix-free Iop_CmpF32/64 is the three-way FComCC and suffix-free Iop_CmpEQ8/16/32/64 are integer) are both documented as such at their ops_def.rs definition sites since angr-fs8kb.17/.18 — do not re-file them as dispatch gaps, and document any new one the same way.

Testing an option-gated symbolic-address branch (AVOID_MULTIVALUED_READS/WRITES, and any future gate spelled option && addr.as_u64().is_none()): build the address as a BVS pinned by a solver constraint to ONE concrete location. as_u64() stays None so the gate fires, yet the concretizer resolves to exactly one address when it does not — so the ON and OFF runs differ ONLY by the short-circuit, with no multi-solution ITE noise to explain away. Canonical harness: memory/tests/avoid_multivalued.rs::pinned_symbolic_addr (mirrored as mv_write_addr in interpreter/statements_tests.rs and pinned_symbolic_addr in interpreter/expressions_tests.rs). Corollary from angr-6cp06.67: per-site sabotage is the only way to learn a gate is REDUNDANT — VEXInterpreter::try_rust_memory_load's copy of the read short-circuit is unobservable on its own because SymbolicMemory::load_symbolic_unified carries the same gate downstream. Say so in the test's doc comment instead of writing an assertion that pretends otherwise.

Overflow fix choice: saturating_add is right for SIZES/LENGTHS but WRONG for IDENTITIES (fd numbers, allocation slots, ids) — clamping hands the same identity out twice and aliases two live objects, which is a worse wrong answer than the plain + it replaced. For identity allocators, use checked_add and REFUSE (return None/Err so the caller bounces to Python), mirroring FileSystem::dup2's MAX_FD refusal. Applied in FileSystem::pipe (angr-03vl4.55): saturating would have returned u32::MAX for BOTH pipe ends. Contrast round_alloc_size (state/process.rs) where saturating IS correct — the value is a size, so clamping only over-reserves. Related: mixed-signedness position arithmetic wants neither — FileSystem::seek's offset_position widens u64 base + i64 offset to i128 and clamps, because 'base as i64 + offset' is wrong twice (i64 overflow AND a base above i64::MAX going negative before the offset applies). ESCAPE HATCH (angr-0jh0j.50, state/process.rs::advance_brk): an identity allocator whose -> u64 contract has no failure channel may saturate instead of refusing, but only when (a) wrapping would alias mapped memory while saturating aliases only the unreachable top of the address space, and (b) the saturation is logged (silent_default!(cat_c, ...)). Do not read that as license to saturate an identity that has a callable refusal path.

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.

COROLLARY for merge repair loops (angr-fs8kb.68). SymbolicMemory::merge's trailing adopt-from-other backfill iterates other.symbolic_objects keyed at each object's BASE address. Gating that repair on Entry::Vacant at the base key is wrong: OCCUPIED != RESOLVABLE. The both-present per-byte walk earlier in merge legitimately overwrites the base key with a fresh 8-BIT ITE, so for an object straddling a page boundary (base page both-present, tail page other-only) the Vacant test fails and the tail bytes' symbolic_spans inserts are skipped entirely — bitmap-symbolic with no sidecar resolving them, load errors out. Two generalizable rules: (1) the resolvability predicate is per byte, SymbolicMemory::symbolic_byte_lane(...).is_some(), never map.contains_key(base); (2) you cannot repair by re-pointing symbolic_spans at the base — symbolic_byte_lane rejects a span whose recorded width disagrees with the base object's actual width — so install an 8-bit self-referential entry per byte, the same shape the both-present walk uses. Gate the repair on the bitmap (this memory) AND on the byte not being Multi (see [[invariant-multi-vs-symbolic-cell-states]]), or you manufacture the inconsistent fourth cell state. Behavioural coverage lives in memory/tests/merge_sidecars.rs; this is the third recurrence of the adopt-the-bitmap-forget-the-sidecar shape after angr-c7xno.50 (multi_objects) and angr-91vj9.3 (interior symbolic_spans).

MOVE DIRECTION (inverse corollary, angr-c7xno.50): the bitmap is authoritative for READS but NOT self-sufficient for MOVES. MemoryPage carries only data + symbolic_bitmap + multi_bitmap; the per-address payloads (SymbolicMemory::symbolic_objects, symbolic_spans, multi_objects, multi_versions) are FLAT maps on SymbolicMemory, not nested in the page — so any path that inserts/clones/adopts a whole page from another SymbolicMemory (merge's (None,Some(op)) arm, snapshot restore, migration, prefetch) must copy the matching side-table entries explicitly or it installs bitmap bits pointing at nothing. Orphaned Multi bits are especially bad: range_has_multi (load.rs) gates on multi_objects, NOT the bitmap, so the load silently returns the stale concrete byte, and merge's 's_multi implies a payload' expect panics on the next merge. Fixed for merge by walking MemoryPage::multi_offsets (mirrors symbolic_offsets) and routing payloads through the existing multi_ops queue so set_multi_alternatives does the bitmap sync + bump_multi_version.

panic=abort is NOT in effect under cargo test. The workspace sets panic="abort" only in [profile.release] (root Cargo.toml), and cargo FORCES panic="unwind" on test/bench harness binaries regardless of the profile's panic setting (libtest needs to unwind to report a failing test); no [profile.test] override can opt back into abort. Consequence for panic-hardening audits in native/angr/src/: any 'this .expect is provably unreachable because panic=abort forecloses mutex poisoning / thread death' argument holds for the SHIPPED .so only, never for 'cargo test --release --lib' (the ralph gate's first check). Concretely in exploration/scheduler.rs (Panic policy module header) + scheduler_worker.rs: under cargo test a worker that panics while holding the job.results / job.summaries guard (worker::worker_loop's terminal+summary drains, worker::drain_local_into_results) poisons that lock, and the coordinator's next lock -- WaveJob::take_results, WaveJob::into_results, or the done_rx guard in PersistentPool::run_wave -- fires its .expect("... poisoned") as a SECOND, cascaded panic. That cascade is expected, not a violated invariant: when debugging, ignore the 'mutex poisoned' panic and look for the EARLIEST panic in the test output. Scoped into the module doc by angr-9ke6b.57 (commit c9d2f3e5d).

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.

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 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 the rst matrix, which presents every opt-in divergence as raised, rejected or honored. 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.

Parity-audit rule for native procs: a Python SimProcedure's kwarg/flag names an INTENT, not a branch that runs. Before filing a Rust-vs-Python divergence, check the flag's branch is reachable for the inputs the native proc actually accepts. Canonical miss (angr-j0dp3): fdopen.py passes create_file=True for w/w+/a/a+, but SimSystemPosix::_get_concrete_fd only materializes its /tmp/angr_implicit_N file on the solver.eval_one -> SimSolverError branch, i.e. a MULTI-SOLUTION SYMBOLIC fd. Concrete fds are returned unchanged whatever the mode, and native procs declared with 'concrete' args never see a symbolic one -- so a whole class of posix-plugin 'symbolic fallback' code (get_concrete_fd, get_fd concretization, close()'s eval_one) is dead for native and cannot be a divergence source. Same shape applies to any Python-side eval_one/concretize-on-demand path.

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.

vex/opcode_map.rs parse_type returning None is NOT a safe 'refuse to guess' signal: every caller in vex/pyvex_bridge.rs (Get/Load/CCall-retty/RegArray-elemTy/tyenv sites) and vex/libvex_lifter.rs::c_type_parse goes through opcode_map.rs::parse_type_or_log, which defaults to IRType::I64. So an unmapped Ity_* becomes 64 bits (loudly since angr-c7xno.90 — parse_type_or_log log::warn!s and carries the SILENT(cat-c) tag — but still wrongly). When a VEX type has no IRType variant, map it to the SAME-WIDTH variant rather than dropping to None. IRType is a width tag only -- nothing outside IRType::bits()/bytes() matches on which variant it is, and IRType::F80 is not constructible from any path except this table. Fixed at iter165: Ity_D32->I32, Ity_D64->I64, Ity_F128/Ity_D128->V128 (previously F80 = 80 bits for a 128-bit type). Latent-only; PPC/S390X are the sole emitters and are unsupported arches.

invariant: a partial hit in a memory-layer cache must never let the layer below answer for the bytes the cache already owns. The Rust interpreter's callback-path load ladder (interpreter/expressions_loads.rs::load_concrete_addr) shipped this bug twice: PendingStoreBuffer::try_load needs one store covering the whole load, try_load_assembled needs every byte buffered (angr-6cp06.69), and both refuse partial coverage — so a store-1-byte-then-load-2 fell through to the flushed-store / concrete-cache / Python-callback rungs, which answered for BOTH bytes and silently undid the buffered write (angr-6cp06.88). Correct shape: resolve the lower rungs FIRST (load_concrete_addr_below_pending), then splice the covered bytes over that result via bv_utils::splice_bytes_over_bv. The splice must NOT go through bv_to_bytes for a non-Concrete base: bv_to_bytes zeroes a symbolic value and drops a Constrained's constraints, so every non-Concrete variant is rebuilt as a Concat of per-byte lanes with Extract for the uncovered ones. Applies to any new rung added to this ladder, and to memory/ sidecar lookups with the same all-or-nothing shape. Still unhandled by design: a pending symbolic store partially covering a load (symbolic_store_load is full-coverage-only), and get_return_addr's probe in interpreter/simprocedures.rs, which deliberately does not mirror the overlay rung.

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.

Pointer-keyed identity in the Rust engine (address-as-key dedup) is only sound while every keyed value is SIMULTANEOUSLY ALIVE — a freed node's address is immediately reusable, so a later distinct node reads as an already-seen hit and inherits the dead one's id. Any address-keyed map must therefore PIN what it keys. Two instances: claripy_bridge/cache.rs's EXPRESSION_BY_OPERANDS_PTR pins the operands Arc for imports (documented in claripy_bridge/mod.rs's header); symbolic/sharing.rs's ConstraintSharingWalk did NOT, and since SymContext::fold_sharing_walk keys the Vec that get_assumed_constraints() clones and drops per state, consecutive states landed on the same freed addresses and analyze_constraint_sharing collapsed unique_pointers/unique_shapes toward 1 (angr-gkcxh). Fix shape: make the entry point take the batch BY VALUE and retain it until the accumulator is consumed, and make the by-borrow entry point private so the footgun is unreachable. Retention must be a Vec<Vec>, never one flat Vec — a flat Vec reallocates as batches accumulate and moves already-keyed nodes out from under their recorded addresses (growing the outer Vec only moves inner Vec headers; element buffers stay put).

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/ AND native/angr/src/syscalls/ must use wrapping_* -- [profile.release] sets no overflow-checks, so a plain src + size panics under CI's release-checked profile 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/syscalls for bare + / - on address or address+length operands; syscalls/ was swept 2026-08-11 (angr-03vl4.65/.66/.67: store_stat_u64/u32/zero96 in file_path/stat_layouts.rs, getrlimit in rlimit.rs, gettimeofday/clock_gettime in sim_time.rs).

TEST RECIPE for a non-vacuous near-u64::MAX regression test (the trap: pass a huge pointer and the FIRST memory_store errors Unmapped and ?-returns before the wrapping expression is ever evaluated, so the test passes with or without the fix). Do all three: (1) map BOTH the top page (0xFFFF_FFFF_FFFF_F000, 0x1000) and page 0, so the pre-wrap and post-wrap addresses are storable; (2) pick the base so every field store stays aligned within one page and none straddles the u64 boundary -- u64::MAX-7 works for 8-byte-aligned layouts (field 0 lands in the top page, every later offset wraps into page 0); (3) PROVE non-vacuity by temporarily restoring the bare + and confirming the test panics under cargo test --profile release-checked. Examples: gettimeofday_tv_near_u64_max_wraps_second_field (sim_time_tests.rs), fstat_statbuf_near_u64_max_wraps_field_offsets (file_path_fstat_tests.rs).

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. INVARIANT: any store the interpreter routes exclusively through a Python memory callback must also land in rust_memory when the proxy gate is on. angr-5mnx3.23 found four MORE sites that had repeated the raw dispatch (handle_storeg's two symbolic-guard branches, cas_store_symbolic_data, build_ite_store_from_callbacks) -- the pairing was a convention, not a structure. Enforcement now: VEXInterpreter::store_symbolic_value_buffered (interpreter/statements_store.rs) bundles buffer_store_for_rust_memory + call_memory_store_symbolic_value, and is the ONLY sanctioned way to reach that callback. A new store path calls it, never the callback directly. Callers needing the pending buffer drained first flush BEFORE the helper.

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.

A #[pymethods] fn's caller census cannot be established from the Rust side: its real callers live in angr/exploration/.py and are invisible to a native/ grep and to the compiler (nothing goes dead when the last Rust caller disappears). Two failure modes seen: (a) a doc comment asserting 'today the only caller passes X' (drop_state_from_stash claimed '_copies' while rust_manager.py::_route_preinit_seed_finds passed "active" and rust_state_proxy.py::_StashDict.setitem passed any key), which then labels a live branch as dead defensive code a maintainer may delete -- here that would have reintroduced the angr-myzjx.25 SelectionPolicy memo leak; (b) the mirror-image gap where only the Rust-exercised argument value has a test. RULE for any comment or audit on a #[pymethods] surface: grep angr/**/.py for the method name before writing a caller/argument claim, and prefer stating the invariant the branch upholds over enumerating who calls it today. Same spirit as AGENTS.md's no-cardinality rule, one language boundary further out. Found angr-6cp06.16, commit 91df6296b.

PyO3 gotcha for DRY passes over #[pymethods]: a macro_rules! invocation placed INSIDE a '#[pymethods] impl T { ... }' block is invisible to pyo3 — the proc-macro attribute parses the impl before declarative macros expand, so it sees an ImplItem::Macro and the generated fns are never registered on the Python type (they silently just don't exist at runtime; it does not fail to compile). To collapse repeated pymethods bodies, have the macro emit its OWN '#[pymethods] impl T { ... }' block at module level and invoke it after the main block — this works because Cargo.toml enables the 'multiple-pymethods' feature. Canonical example: postcard_pickle_methods! in native/angr/src/fuzzer/corpus.rs (angr-12jjk.27).

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.

A #[pyo3(get)] getter suppresses rustc's dead_code lint for the field it wraps — the derive counts as a read. So a pyclass whose Python surface is unreachable can hide arbitrarily much dead Rust state behind it, invisibly, forever. Removing DeferredFork's unreachable PyO3 surface (angr-03vl4.6) immediately exposed push_level, a third always-zero copy of the counter already killed twice in SymContext (angr-ph300.44, angr-c7xno.75); nothing had ever read it from Rust. Rule: when auditing a #[pyclass] for reachability, delete the getters FIRST and re-run clippy before concluding the change is cosmetic — the field-level cascade is where the real finding usually is. Same shape applies to #[pyo3(set)] and #[pymethods] accessors generally.

PyO3 'multiple-pymethods' IS now enabled in this project (native/angr/Cargo.toml pyo3 features = [py-clone, abi3-py310, multiple-pymethods], angr-9ke6b.50). A pyclass may have MANY #[pymethods] impl blocks, in any module in the crate. RustExplorationManager's ~228-method surface is split across manager_methods.rs (construction/config/callbacks) + manager_methods_{hooks,state,constraints,procedures,techniques,export,run,diagnostics,snapshot}.rs, one #[pymethods] block each, all opened with 'use super::*;'. The old (A)/(B) workarounds in pyo3-pymethods-child-module-split are no longer forced -- you may now peel a cohesive method group into its own file+block directly. Two costs the flip carries, both handled: (1) it pulls in the 'inventory' crate (linker-section class registration) and pyo3 documents a compile-time cost; (2) SURPRISE -- see below.

UNREACHABLE_PUB UNMASKING (angr-9ke6b.50): enabling the feature unmasked 391 unreachable_pub warnings crate-wide (lib.rs has #![warn(unreachable_pub)] from angr-9ke6b.214), instantly reddening CI clippy -D warnings. Mechanism: pyo3's NON-multiple-pymethods codegen was masking the lint on every #[pymethods] method AND on the #[pyclass] struct those blocks belong to — the flip does not create over-broad pubs, it reveals pre-existing ones. FIX CHOSEN: a scoped #[allow(unreachable_pub, reason = "pyo3 ...")] on each affected #[pymethods] impl block and #[pyclass] struct, restoring exactly the pre-feature coverage. Note the pyclass STRUCT needs its own allow separately from its #[pymethods] block. Rejected: rewriting ~391 'pub fn' -> 'pub(crate) fn' (mixes concerns, risks a dead_code wave). Do NOT blanket-allow unreachable_pub at crate level; that kills the guardrail for real Rust API surface.

CONVENTION for any NEW pyo3 item that trips the lint: use the scoped allow with the VERBATIM reason string used in segmentlist.rs/solver.rs — do NOT narrow it to pub(crate). Those items are reached from Python, not Rust, so their Rust visibility is decorative. Narrowing also makes clippy green, so the wrong fix is easy to land; check the existing allow sites before choosing. Non-pyo3 items keep the opposite rule (narrow to pub(crate), angr-9ke6b.214) so dead_code can see them.

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.

SUPERSEDED 2026-08-02 by invariant-pyo3-multiple-pymethods-enabled -- the feature IS now on (angr-9ke6b.50) and a pyclass may have MANY #[pymethods] blocks. Kept for the still-true sub-facts: (B) a #[pymethods] block does NOT have to live in the same file as its #[pyclass]; a sibling module opened with 'use super::*;' surfaces the parent's private 'use' imports, pub(crate) fields and type aliases so bodies compile unchanged (demonstrated by state/pymethods.rs holding the whole #[pymethods] impl PyRustSimState while the #[pyclass] struct + inner()/inner_mut() stay in state/mod.rs, 7ac9c0fe2). (A) the thin-wrapper-in-pymethods / pub(crate)-body-in-sibling-plain-impl pattern (exploration/run_loop.rs, pending_api.rs, stepping.rs, resume.rs, helpers.rs) is still the right split when the body is large -- it is now a style choice, not a constraint.

When Rust evaluates a caller-supplied Python predicate's return value, test it with Bound::is_truthy()? — never extract::(py).unwrap_or(false). Python filter/predicate functions conventionally return any truthy object (a non-empty list/str, a numpy bool, an object with bool), and strict bool extraction reads those as FALSE, i.e. 'doesn't match'. It also swallows an exception raised from bool into the same silent 'no match'. Found live in _move_states (exploration/state_lifecycle.rs) at angr-sqfj8.31. DISTINCTION: extract::() is still correct where the code is discriminating a type rather than testing truth — e.g. claripy_bridge/export.rs's compare_dunder, which asks 'did eq return a Python bool (concrete) or a claripy AST?' and must NOT coerce the AST branch to a bool. Rule of thumb: truth test -> is_truthy()?; 'is it a bool?' -> extract/downcast, and propagate rather than unwrap_or.

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.

panic=abort makes any Python-supplied size a PROCESS-ABORT vector, not a catchable error. native/angr/Cargo.toml sets [profile.release] panic="abort", so nothing below is recoverable at the PyO3 boundary. Two shapes seen so far: (1) rangemap::RangeMap::{insert,remove} assert!(range.start < range.end), so an 'address..address + size' built from Python values without a checked_add guard aborts -- fixed in SegmentList::release (native/angr/src/segmentlist.rs, angr-9ke6b.199); SegmentList::occupy already had it. Convention: 'let Some(end) = address.checked_add(size) else { return; }' tagged // SILENT(cat-a), since a wrapping range describes no real region. (2) allocating a buffer whose length came straight from Python -- Vec's 'capacity overflow' panic near usize::MAX and handle_alloc_error for a merely huge size both abort. Fixed in Icicle::mem_read (native/angr/src/fuzzer/icicle.rs) via the free fn checked_read_len: reject a wrapping addr+size and a size above Icicle::max_mem_read_bytes (the mmu's own capacity()*page_size()), THEN allocate. Rule for new code: validate the range/length before you build it, whether the consumer is a RangeMap or the allocator; a free fn taking (addr, size, max) keeps it unit-testable where the surrounding type needs a VM/GIL.

COUNT-BEFORE-RESERVE (third shape, generalized): any Vec::with_capacity / reserve whose count crosses the PyO3 boundary must be bounded BEFORE the reservation — no guest input needed, an ordinary documented Python call (RustExplorationManager::register_simprocedure with a bogus num_args) is enough. Two fix shapes, pick by whether the refusal should degrade or raise. (a) Degrade: a named MAX_* const next to the error enum + a new error variant returned before the reservation, so the caller falls back (native dispatcher -> Python SimProcedure) instead of crashing — arch::MAX_EXTRACT_ARGS / ExtractionError::TooManyArgs guarding exploration::helpers::extract_args_with_abi (angr-0jh0j.23). (b) Raise at the trust boundary: a MAX_* const + a check_*(op, n) -> Result<(), String> guard called by every Python-facing entry point, message-typed rather than error-typed so the layer defining it stays pyo3-free and callers reporting through different channels (PyValueError vs BridgeError) can share it — symbolic::width_guards::check_bv_width is the precedent, symbolic::bv_chunk::check_concrete_load_size / MAX_CONCRETE_LOAD_BYTES the second instance (angr-0jh0j.11). Shape (b) is what a generic helper wants when it cannot construct its own error type E: guard at the boundaries, and additionally cap the helper's own reservation (Vec::with_capacity(n.min(MAX)) — bounds the allocation without truncating the result) as defence in depth. A bound like this also retroactively makes downstream index arithmetic (i * ptr_size) provably non-overflowing.

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.

Recognizer/value-parser grammar parity is an invariant for any native proc that returns BOTH a value and a consumed-length (strtod/strtol/strtoul/sscanf-family). If the boundary-finder accepts a grammar the value-parser cannot handle, the result is the worst failure shape: a wrong value reported with *endptr advanced past the whole literal, so the caller believes a full correct parse happened. Concrete instance (angr-sqfj8.81, commit 98cc4c8fc): procedures/strtod.rs floating_prefix_len recognized C99 hex-floats but the value went through f64::from_str, which REJECTS hex-float syntax outright ('0x1.8p3'.parse::() is Err) -- .unwrap_or(0.0) made strtod("0x1.8p3") return 0.0 instead of 12.0. Rust std has NO hex-float parser; strtod.rs::parse_hex_float is the crate's only one (u128 significand + sticky bit past 124 bits for round-to-nearest-even, plus scale_by_pow2 = musl's three-step scalbn clamp so the exponent tails don't collapse through an intermediate inf/0). Reuse those two, do not hand-roll a second. Review rule: when auditing a proc with a prefix-scanner, diff the scanner's documented grammar against what the value parser actually accepts -- and prefer deferring to Python (ProcedureError::NotImplemented) over substituting a default on a prefix the value parser rejects.

BACKTRACK COROLLARY (angr-6cp06.2, commit 19528862f). The same scanners have a second failure mode on the OTHER side: when a longer alternative fails mid-scan, C's longest-valid-subject-sequence rule requires backtracking to the longest valid SHORTER prefix, not rejecting to the start. The natural Rust spelling -- capture 'prefix_start' at the top, 'return prefix_start' from every failure path -- is wrong wherever a shorter alternative already matched, and it silently drops the sign too because prefix_start is captured before the sign is consumed. floating_prefix_len's hex branch did exactly this: '0x' with no hex digit after it returned prefix_start, so strtod("0xg") reported end_offset 0 and strtod("-0xz") returned +0.0 at offset 0, where glibc gives 0.0/offset 1 and -0.0/offset 2 (the leading '0' is itself a complete decimal literal). Fix is to return the index of the byte that broke the longer alternative. Review rule: for each 'return ' in a prefix scanner, ask whether a shorter alternative had already succeeded at that point -- and check the sign is inside, not outside, the returned span. The strtol sibling (bd angr-bmfj0, commit afe68fd7e) shows the PREFERRED FIX SHAPE: rather than patching what the failure path returns, add a lookahead guard so the scanner never consumes the longer alternative it cannot complete -- strtol.rs::hex_prefix_has_digit gates both 0x-consuming sites in parse_concrete_prefix, leaving the '0' for the digit parser, which then reports value and endptr through the normal SUCCESS path (consumed > 0). That matters because the failure path in these procs is usually governed by a separate, often-divergent 'no conversion' rule (run_strtol points *endptr past the prefix, not at nptr as C says); routing a genuine conversion through it makes the fix depend on a quirk that a later correctness pass would break. Corollary for symbolic engines: a symbolic lookahead byte must count as USABLE (consume the prefix, let the accumulator decide), else constrained-to-digits buffers regress.

Refusal-guard placement invariant (angr-0jh0j.35): when you fix an overflow/validation bug by making a fallible entry point REFUSE the bad input, check what the new Err path reaches. A refusal can route the bad value straight INTO an infallible fallback that swallows errors and then performs the same unguarded arithmetic — in memory/, check_access_size in SymbolicMemory::load_concrete_common makes an oversize load fail, and SymbolicMemory::load_concrete_or_unconstrained's by-design 'every error becomes an unconstrained value' branch then computed the very size8 the guard existed to prevent. Two consequences: (1) an infallible fabricator needs its own clamped-width helper (memory::fabricate_width_bits) so the unreachable case degrades to a wrong-but-valid value rather than an invalid one (a 0-width BV Z3 cannot represent); (2) guards must ALSO sit on entry points that short-circuit before the shared body — load_symbolic/load_symbolic_unified reach unconstrained_read_value under AVOID_MULTIVALUED_READS without touching a page. Generalizes to any error-swallowing fallback (native-proc ProcedureError bounce, ITE-leaf fillers), not just memory. THIRD consequence (angr-0jh0j.84, found by audit one round later): fixing the sites a failing trace led you to is not the sweep — grep the whole file for the arithmetic SHAPE. .35 hardened two fabricate sites and left load_symbolic_unified's all-unmapped mem_all_unmapped_ arm on a bare size*8 for a full round, because no trace reached it (check_access_size refuses first, so it is unreachable defense-in-depth, not a live bug). When a helper like fabricate_width_bits is introduced, its doc should ENUMERATE its call sites — that list is what makes a missed site visible on the next read.

RegisterFile::copy_to_bytes (native/angr/src/arch/register_file.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.

Rust RegisterFile storage is little-endian on EVERY arch, unconditionally. Big-endian register semantics (angr stores its register file at arch.register_endness — Iend_BE for MIPS32/MIPS64/ARMEB) are implemented by mirroring the offset in RegisterFile::mirror_offset (native/angr/src/arch/register_file.rs), never by changing the byte<->value composition. Consequences future work must respect: (1) do NOT make le_bytes_to_u128 / u128_le_byte / compose_range / put's overlay bit arithmetic / RegisterFile::merge's concrete-diff chunk scan / get_sp_value endianness-aware — that would double-apply on top of the mirror; (2) endianness is a CALLER-supplied fact, never derivable from the arch: RegisterFile::new_with_endian(arch, is_le) and VEXInterpreter::with_config_endian(arch, ctx, config, is_le) are the two production constructors, and RegisterFile::new / VEXInterpreter::new are #[cfg(test)] LE-only conveniences precisely so a new production caller cannot silently pick LE (angr-21cz6). A new big-endian arch must also list every register in its CANONICAL table, since mirror_offset is the identity for an offset no canonical entry covers; (3) the mirror is an involution and the identity for a whole-register access, so name-keyed get_reg/put_reg and the Python<->Rust value-level sync are unaffected; (4) Arch::is_little_endian() is hardcoded true on every arch — the real answer is the state's little_endian override, seeded in rust_manager.py from project.arch.memory_endness (verified equal to register_endness on every archinfo arch as of 2026-08-16); the exploration path never has to re-derive it because exploration/step_core.rs does 'interp.registers = state.registers().fork()'; (5) TWO COORDINATE SPACES, never mix them (angr-6cp06.74): RegisterFile::get/put take a RAW VEX offset and mirror on entry, but every key of self.symbolic and every index into self.data is already a STORAGE offset. Code that iterates those keys and then wants to read must call RegisterFile::get_storage (the un-mirroring body of get), NOT get — RegisterFile::merge did the latter for its four read sites and double-mirrored, landing on the other half of the containing register. The involution property does NOT rescue a double application here, because the doubly-mirrored value is used as a real lookup key and bit-range reference against actual storage entries, not merely recomputed. Invisible on every LE arch and on every merge test that uses the LE-only RegisterFile::new — a BE regression test is mandatory for any new merge/overlay-scanning code (see arch/register_file_tests.rs::be_merge_reads_the_other_side_in_storage_coordinates). angr-fuhmm, angr-21cz6, angr-6cp06.74.

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.

REGISTER-TABLE PLACEMENT RULE (angr-9ke6b.9): any name listed in a per-arch REGISTER_NAMES export slice MUST also live in that arch's CANONICAL table, never ALIASES-only. register_name(offset) scans CANONICAL only, so an exported-but-aliased name resolves forward (name->offset) but not backward (offset->name). X86 shipped exactly that for xmm0..7 + the x87/SSE control words, making X86::register_name(XMM0) return None while AMD64::register_name resolved it. Fixed by moving the SSE/x87 block into x86.rs CANONICAL; forward lookups are unchanged because lookup_register_offset/size check CANONICAL then ALIASES. Gate: arch/registry_tests.rs::exported_register_names_reverse_resolve asserts, for every arch in ALL_ARCHES and every name in register_names(), that register_name(register_offset(name)) is Some and round-trips to the same offset (it compares offsets, not name identity, so 'pc' vs 'eip' canonicalization at a shared offset is allowed). Complements the opposite-direction rule in invariant-guest-state-size-vs-archinfo: the VEX bookkeeping fields (emnote/cmstart/cmlen/nraddr/ip_at_syscall) stay ALIASES-only precisely because they are NOT exported via REGISTER_NAMES.

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 EXACTLY that arch's CANONICAL table minus entries wider than 16 bytes, in BOTH directions: ExplorationStateSnapshot::get_registers_named carries each value as a u128 and RegisterFile::get's concrete read composes bytes with 'value |= (byte as u128) << (i*8)', so a wider register silently yields garbage (release-mode shift masking) instead of failing; and a narrow CANONICAL entry left OUT of REGISTER_NAMES is silently filtered by _supported_register_names, so set_registers_bulk drops every state.regs. write for that arch while the same write works on a sibling arch. Today x86/AMD64 'fpreg' (64 B, 8 x87 slots) is the only legitimate omission. Both directions are now machine-gated in arch/registry_tests.rs: register_names_all_resolve_and_fit_in_u128 (forward) and every_narrow_canonical_register_is_exported (converse, angr-sqfj8.6) — the latter reads the whole table via Arch::canonical_registers(), a test-only assertion primitive generated for all six arches by impl_arch_registers!. Width is the converse test's ONLY exemption, deliberately: no per-arch allowlist that can drift. History of this bug class: angr-9ke6b.6 added fptag/fpround/fc3210/ftop and left a HARDCODED field-list test (x87_control_registers_round_trip_through_register_names), which by construction only covers registers someone already thought of — it missed X86 sseround, fixed a sweep later in angr-sqfj8.1 (commit 6626d4df6). When adding a register to any CANONICAL table, add it to REGISTER_NAMES too unless it is >16 B.

RegisterFile.symbolic (native/angr/src/arch/mod.rs) is keyed by RAW VEX guest-state offset, and those keys are NOT register-aligned: x86/amd64 register the high-byte aliases ah/ch/dh/bh at GPR_offset+1 (see ALIASES in arch/amd64.rs and arch/x86.rs). Any code that scans the overlay map in arch-word-sized chunks and tests only the chunk's aligned start offset will miss an overlay living inside the chunk. That exact assumption produced angr-c7xno.1 (RegisterFile::merge's concrete-diff loop compared raw backing bytes for such a chunk and inserted a concrete-only ITE at the aligned offset, which get() then returned verbatim on a width match — silently shadowing the already-merged ah). The safe shapes: test the whole range [off, off+reg_bytes) for membership, and when an inner overlay exists compose both sides through RegisterFile::get (which walks the map for covering/contained overlays) rather than reading self.data directly. Whenever you insert a wide overlay that covers narrower ones, also drop the inner keys (the 'widened' subsumption pass in merge) — leaving both is hazardous because put() composes a sub-register write into the WIDER entry it finds and leaves the narrow duplicate stale, after which get()'s exact-offset hit returns the stale one.

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.

A 'Regression guard: ' citation in a Rust doc comment is unverified prose — nothing compiles or resolves it, so a fabricated or renamed name reads exactly like a real one and the invariant it claims coverage for may in fact have NONE. context.rs's three-gate SharedLineageSolver doc cited two test names (test_lineage_minted_only_when_opted_in / test_lineage_not_minted_under_bare_push) that never existed anywhere in the repo (angr-5mnx3.44). When repairing such a citation, do not just rename it to the nearest real test: first check per-clause whether a guard exists for EACH claim the sentence covers. Two of the three gates had guards under other names in another file; gate (c) (invariant-v5ht-dismantle-child-none) had none, and the doc had been asserting otherwise for months. Second, related trap: a negative-assertion guard whose setup makes the asserted value ALSO the default proves nothing. Both existing gate guards asserted child.lineage_arc().is_none() from a parent whose own lineage was already None, so they could not distinguish 'refused to mint' from 'cloned a None' — the new gate-(c) test has to stage a parent that actually HOLDS a lineage. Mutation-verify any guard you add (neuter the arm, confirm the test reddens); an assertion that passes against the broken code is the same defect one layer down.

A host-safety bound expressed relative to a current value (e.g. syscalls/brk.rs's MAX_BRK_GROWTH capping new_brk - current, or any 'growth cap') does NOT bound the absolute value: repeated in-bounds steps walk the quantity to the top of the address space. Any align-up (x + PAGE_MASK & !PAGE_MASK) or +len downstream of such a bound must therefore be treated as reachable at u64::MAX, not dismissed as 'the cap prevents it'. Two failure modes seen in brk (angr-fs8kb.51): (1) an aligned-up exclusive end wraps to 0, so a 'while addr < end' page walk runs ZERO iterations -- the bug is a silently skipped safety check, not a hang or a crash, which is why it survived review and the overflow audit gate; (2) the byte-stepped 'addr += PAGE_SIZE' wraps past the final page. Fix shape: iterate PageIndex::range_covering(start, len) over page numbers and derive len from the LAST BYTE (new_end - 1) rather than an aligned-up exclusive end. See also invariant-proc-address-arith-wrapping.

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).

INVARIANT (restore/reset paths must clear EVERY derived field, not just the primary container): four separate bugs of this exact shape landed in round 8's queue back-to-back -- RustExplorationManager::load_snapshot kept the pre-restore Python id-keyed shadow maps, load_snapshot_bytes kept the pre-restore ConstraintTracker sets, _reset_for_stage left the stage-1 uniqueness hashes live, and SegmentList::setstate (segmentlist.rs) cleared self.map but not self.bytes_occupied. The shape: a struct keeps a primary container PLUS one or more incrementally-maintained derived fields (byte totals, id-keyed shadow maps, dedup hash sets, tracker sets) whose only mutator is a monotonic add. A restore/reset/load method clears the container, replays the saved entries through the normal add path, and the derived field silently reports old-value + restored-value. Two rules: (1) when adding a derived/cached field to a struct, grep that struct's impl for every clear/reset/load/setstate method and extend each one; (2) when reviewing such a method, enumerate the struct's fields and check each is either reset or provably rebuilt by the replay -- a partial reset compiles and passes every fresh-instance test, because the in-tree caller is usually a pickle/new path that starts from Default. Reachability matters: a #[pymethods] fn is callable from arbitrary Python on a populated instance even when the in-tree protocol only ever hits it on a fresh one.

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. The dual failure is just as bad and hit twice (angr-sqfj8.121, angr-03vl4.74): recording in NEITHER log. Every reconstruction path — to_snapshot's dump_non_bv_smtlib2, unsat_core_assumed, _export_state_constraints — rebuilds from the assumed + residual logs and NEVER from local_constraints.z3_assertions, so a constraint that is only in z3_assertions is enforced in-process and then vanishes on snapshot/restore. So: any new route that asserts on the live solver owes an EXACTLY-ONE-log push. If it asserts via add_constraint_raw* that is automatic; if it asserts by some other route (add_constraint_tracked_indexed must use assert_and_track for unsat-core fidelity) it must call assumed_constraints_push or SymContext::push_residual_assertion itself, branching on whether claripy_to_rustbv succeeded. See [[unsat-core-on-demand-not-tracked]]. UPDATE (angr-6cp06.26): the per-constraint body moved down one level into exploration::constraints::import_one_constraint — the single seam now shared by import_python_constraints (initial/pending, ConstraintTier::Z3PtrFirst) AND RustExplorationManager::sync_constraints_from_python (callback-bounce sync, ConstraintTier::RustBvFirst), which used to be an independent reimplementation with inverted tier precedence. Any new tier or exactly-one-log fix belongs in import_one_constraint, not in either wrapper.

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 arms were 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 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 (integer/special families) or its opcode_map_float.rs / opcode_map_vector.rs siblings 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). STATUS (angr-sqfj8.115, iter50): the hardcoded-V128 class is now EXHAUSTED -- the last group (VMin/VMax/VAbs/VFAdd/VFSub/VFMul/VFDiv/VFSqrt/VFAbs/VFNeg/VFMin/VFMax) was moved onto width_total_to_type and pinned in that test. No hardcoded packed-width arm remains; if a new one appears, it is a regression. ADDENDUM (angr-9ke6b.169, iter161): the TAG matters too, not just the width. No consumer of result_type compares IRType tags for equality -- every caller goes through .bits() -- so an I128-vs-V128 mismatch is invisible to tests and must be caught by cross-referencing the libVEX header. DivMod{U,S}128to64 was tagged I128; libVEX types it ':: V128,I64 -> V128', and our own opcode_map already models the surrounding chain as vector-typed (Iop_64HLtoV128 -> Concat{ty: V128} builds the dividend, Iop_V128to64 / Iop_V128HIto64 split the result), so the retag to V128 is runtime-neutral and internally consistent. Pinned by test_divmod_128_to_64_result_is_vector_tagged in vex/ir_tests.rs. Rule of thumb: when an op's operands or consumers in opcode_map use V128, its result_type must not say I128.

invariant-resume-fork-base-must-precede-guard (FIXED angr-khpsh, commit on rust-symex 2026-07-22; EXTENDED angr-z3obp 2026-09-08): the deferred-fork base must NEVER carry the branch guard or the taken-path constraints at the moment build_unexplored_fork runs — on the snapshot-less arm it does base.fork_false/fork_true(condition), so a pre-guarded base makes the unexplored sibling UNSAT by construction and it silently lands in STASH_PRUNED instead of being explored. The snapshot arm is immune (it rebuilds from a pre-branch clone), which is why every instance of this bug has been latent-until-snapshotless.

RESUME HALF (angr-khpsh): in exploration/resume.rs, ALL THREE resume entry points derive the fork base from a state carrying NEITHER the branch guard NOR the deferred forks' taken-path constraints. _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 and passes the parking state as MaterializeForkCtx::guard_sink (distinct from fork_base, hence structurally immune). Any future edit that hoists a constraint-application above the fork_base binding reintroduces it. Regression: resume_tests.rs::snapshotless_resume_keeps_deferred_fork_live_in_every_entry_point.

MATERIALIZER HALF (angr-z3obp): the three materializers whose fork base IS the continuing state — stepping_forks.rs::process_deferred_forks_into and core_outcome_handlers.rs's materialize_deferred_forks_core / process_deferred_forks_into_core — all had the guard-first order. Closed structurally rather than per-site: fork_materialize::fork_unexplored_and_guard_base does build-then-guard and is the ONLY public entry; add_fork_guard_constraint and build_unexplored_fork are module-private so a fourth call site cannot re-derive the order. Regression: core_outcome_tests/simproc_forks.rs::simproc_success_fork_without_snapshot_survives_with_opposite_guard. Same bug class as angr-ph300.9 (branch guard) and angr-khpsh (taken-path constraints).

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 FOUR-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 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. (It was a FIVE-place edit until angr-0jh0j.6 generated the set_ pymethod from the with_callback_fields! list too — that one now disappears with the list entry.)

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_simplify_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).

Rust's as float cast (f64 as f32, float as int) is hard-wired to round-nearest-ties-to-even — it CANNOT express the VEX directed modes (rm&0x3: 1=-inf, 2=+inf, 3=zero). So in native/angr/src/vex/ops/conversions.rs any _rm-suffixed op whose concrete closure names its parameter _rm and reaches for a bare as cast is a silent-wrong-answer bug, not a style nit: it returns the RNE result under every mode with no error and no fallback (angr-c7xno.85 was exactly this for Iop_F64toF32; the open lint bead angr-91vj9.7 is meant to catch the class). Two correct patterns already in the file: float->INT uses ops::float_arith::apply_rounding (generic over IeeeNum since angr-6cp06.38; was Self::apply_rounding_f32/f64) -- round to an integer first, then cast; float->FLOAT narrowing uses VEXOps::narrow_f64_to_f32_rm — take the RNE result, and if widening it back is not bit-equal to the source, step ONE ULP toward the requested direction with next_up()/next_down(). That ULP step also buys IEEE-754 overflow saturation (+inf.next_down() == f32::MAX, so RZ/RD saturate instead of overflowing) and subnormal underflow (0.0.next_up() is the smallest subnormal, so RU on a tiny value does not flush to zero) with no special-casing. TRAP when testing: the RNE-implicit unop stub (VEXOps::unop(IROp::F64toF32, ..)) is NOT the path the interpreter takes — eval_binop routes the real 2-operand form into VEXOps::binop, so a test that only drives unop cannot see an rm bug at all.

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.