invariant / 1

When implementing the angr-3tek.2 fix, ORDER MATTERS in _create_state_for_callback (rust_callback_dispatch.py): the new dirty-page replay must run AFTER install_rust_memory_proxy (which writes concrete pointer slots from the SP page) and BEFORE restore_symbolic_pages (which restores Python-pushed symbolic snapshots). Within the dirty-page loop, replay symbolic stores LAST per-page so they overwrite concrete defaults at the same addresses. Without that ordering, NativeRead's stdin symbolic bytes get clobbered by the eager SP-page concrete copy. Also: must call _clear_pending_dirty_tracking AFTER replay, otherwise the next callback re-syncs the same pages. (Symbol-anchored per refactor-memory-sweep-rule; raw rust_callback_dispatch.py:1733 drifted to ~513 by iter52 — file shrank substantially.)

The Rust run-loop 'active stash exhausted' termination path (run_loop_parallel_wave / run_loop_parallel_steady / run_loop_single_threaded in exploration/run_loop.rs) MUST return ExplorationEvent::active_empty, NOT found, even when found_count()>0. That path is only reachable with found_count()<num_find because the top-of-loop path (a) returns 'found' for >=num_find before draining active. The Python _explore_with_addresses loop breaks on a 'found' event only when found_count>=num_find; a partial-count 'found' with an empty active stash is neither a break nor active_empty, so run() is re-invoked forever (unbounded spin, looks like a hang at 100% single-core CPU inside the Python loop, not the scheduler). This was angr-q1mwl (test_parallel_wave.py hang). Latent in single-threaded too: explore(find=X, num_find > reachable-finds) would hang identically. Returning active_empty lets the angr-027h phase-2 eager retry fire.

max_active_states is now enforced via push_to_active_or_drop helper in exploration/helpers.rs. The helper uses sm.push() (which indexes) rather than raw push_back. Call this helper instead of stashes_mut().entry(STASH_ACTIVE.to_string()).push_back() at any new STASH_ACTIVE push site, otherwise the limit will silently break again.

invariant-active-stash-push (2026-08-01): still correct for the SERIAL path, but INCOMPLETE — see invariant-max-active-states-two-sites for the parallel half added in angr-9ke6b.48.

RustExplorationManager._add_rust_state (rust_manager.py) MUST operate on a private angr_state.copy(), never the caller's SimState: _concretize_stack_registers pins symbolic sp/bp and adds a permanent sp-equality constraint in place (angr-hv4lt.7, sibling of angr-3uye). The cached Python mirror (_state_cache[actual_state_id]) is therefore the COPY, not the passed-in object. Two consequences future work must respect: (1) SimStateScratch.copy() DROPS custom attrs — the cross-manager transfer path reads angr_state.scratch.rust_mgr / rust_found_state_id (set by RustSolverFallback.attach in rust_state_export.py), so _add_rust_state re-copies those onto the fork explicitly; any new scratch attr the transfer path needs must be added to that carry-over loop. (2) _get_default_state (rust_state_cache.py) returns next(iter(_state_cache.values())) = first-inserted entry = the init copy; tests that inject a state via _put_state_in_default_cache must .clear() the cache first or the copy wins.

Overflow triage: the single most common address-arith bug shape in this codebase is the two-comparison containment test addr >= base && addr < base + size (and its range variant min < base + size). base + size overflows for a region abutting the top of the guest address space, so the shipped .so wraps it to a small value and the test reports every in-region address as OUTSIDE — a silent wrong answer, not a crash. Rewrite as the single wrapping-distance comparison addr.wrapping_sub(base) < size: same result for a non-wrapping region, correct for a wrapping one, and it never forms base+size. Canonical implementation: ConcreteMemoryRegion::offset_of/contains (interpreter/concrete_memory.rs) and covering_range (interpreter/pending_store.rs), which does the same for a load range and hands back the slice Range<usize> so the off + size index sum is proven in-bounds by construction rather than re-checked at each call site. Where the test is a range-vs-range intersection and a conservative over-estimate is safe, saturating_add plus an overflow-ok: comment naming that fact is fine (statements_store.rs::invalidate_code_for_concretization's TooLarge arm). Found in angr-xloth.3; expect the same shape repeatedly in the remaining memory/ triage.

COROLLARY (angr-fs8kb.63, PendingStoreBuffer::push): the 'saturating_add is fine for a range-vs-range intersection' escape hatch above is only safe when you check WHICH DIRECTION the error goes. For a range that wraps past the top of the address space, saturating_add clamps the end to u64::MAX and therefore UNDER-estimates the covered set — it silently drops the wrapped tail (addresses 0..). So it is conservative only for a consumer where a missed overlap is the safe answer (invalidate_code_for_concretization over-invalidates, so it is). push's overlap-patch loop was the opposite: a missed overlap means an earlier store's buffer is never patched, and try_load's reverse-scan fallback later serves the stale pre-overwrite byte. Rule: compute a range intersection in OFFSET space, never in address space — derive both offsets with wrapping_sub from one of the two bases and take the min of the remaining lengths, the way overlap_offsets (interpreter/pending_store.rs) does beside covering_range. Neither end address is ever formed, so there is nothing to saturate or wrap.

COROLLARY 2 (angr-fs8kb.64): the same gap existed on the SYMBOLIC-store side — symbolic_overlap_load (interpreter/expressions.rs) and evict_overlapping_symbolic_stores (interpreter/statements_store.rs) each re-derived the interval arithmetic in address space. Both now call the pending_store.rs helpers, which are pub(super) precisely so the interpreter has exactly ONE wraparound-safe coverage test (covering_range) and ONE overlap test (overlap_offsets). If you find a fourth site asking either question, reuse them rather than writing a local wrapping_sub — three independent re-derivations is how this family kept recurring, and only the shared helper carries the doc explaining why no end address may be formed.

memory/ overflow triage: the Address newtype (native/angr/src/memory/address.rs) implements Add/Sub/Sub as wrapping_, so an addr + i/addr - base site whose operand is an Address is ALREADY in the sanctioned state (address arithmetic wraps — invariant-rust-concrete-arith-must-wrap) and needs no wrapping_ rewrite. tools/audit_overflow_wraparound.py is a textual scan and cannot see the type, so it reports every one of them; that is the dominant false-positive class in the memory/ baseline (roughly 30 of the 69 sites triaged under angr-xloth.4). Do NOT 'fix' them by adding .wrapping_add on the raw() value — that loses the newtype. Mark them with a short overflow-ok: Address ops are wrapping_* comment, and note the exception that matters: wrapping makes the op non-panicking, NOT semantically correct. A wrapped sum used in a COMPARISON is still a bug — containing_wider_sym's addr + size <= base_addr + sym_size was wrapping and still wrong (see invariant-address-containment-wrapping-distance; the memory/ canonical fix is now Address::offset_in / Address::range_in). INVERSE BLIND SPOT (angr-fs8kb.69): the audit's false-NEGATIVE class is the mirror image — a site that ESCAPES the newtype to hand-roll saturating/checked arith on .raw(), e.g. Address(current.raw().saturating_add(n)) in SymbolicMemory::read_concrete_bytes_for_lift. The scan matches bare +/- operators only, so a method call is invisible to it and silently opts that one site out of the file's wrapping convention. For an address cursor, saturating is not a safe conservative choice: it clamps to u64::MAX and the enclosing loop then re-visits the same last byte/page instead of wrapping to page 0 (that read returned a duplicated trailing byte to the lifter). When triaging a file for this class, grep .raw() for saturating_/checked_/wrapping_ alongside running the audit — and when writing a top-of-address-space regression, always assert the whole returned buffer, not just its length, since the corruption is in the contents.

When carving a newtype out of u64 for a subsystem, distinguish byte ADDRESSES from PAGE NUMBERS (addr >> 12). Two complementary newtypes now exist: memory::Address wraps byte addresses (see native/angr/src/memory/address.rs for the documented migration pattern), and memory::PageIndex (memory/page.rs, angr-91vj9.8) wraps page numbers for callers ABOVE the memory layer — VEXInterpreter::dirtied_code_pages, syscalls/mmap.rs::range_collides, syscalls/mprotect.rs::NativeMprotectSyscall::call. Its PageIndex::range_covering(addr, len) replaces the open-coded 'first..=last' page loops (it is empty for len==0 and saturates instead of wrapping). INVARIANT (angr-fs8kb.49): a page walk must iterate page NUMBERS via range_covering, never step a byte address by PAGE_SIZE ('while a < end { ...; a += PAGE_SIZE }'). That shape is structurally broken at the top of the address space — an end computed as '(last_byte & !PAGE_MASK).saturating_add(PAGE_SIZE)' saturates to the non-page-aligned u64::MAX, so a page-aligned start can never reach it and ALWAYS overflows on the step after the final page: silent wrap to 0 in [profile.release] (walk resumes from low memory → false -1 or ~2^52-iteration hang), panic under release-checked. tools/audit_overflow_wraparound.py cannot see it — BINOP_RE's (?![=>]) lookahead excludes compound assignment (tracked as angr-fs8kb.52). Page numbers are under 2^52, so range_covering has no per-iteration overflow to get wrong. Matching rule for the range guard: only the LAST BYTE must be representable (addr.checked_add(length - 1)), so a region ending exactly at 2^64 is legal — do_mmap's MAP_FIXED guard and mprotect now agree on this. The page-keyed structures INSIDE memory/ (pages: OrdMap<u64, MemoryPage>, dirty_pages: FxHashSet, lazy_regions: Vec<(u64,u64)>) and the raw page API they expose (page_permissions) deliberately stay raw u64 — callers cross that boundary explicitly with PageIndex::get()/from_raw(). MemoryError variants also keep u64 to preserve existing Display formatting. Address-keyed structures in memory/: symbolic_objects, symbolic_spans, multi_objects, multi_versions, imported_addrs, wider_load_cache.

angr-z21g0 root cause: the gate-on (prefer_native_library_hooks) fork storm on xmllint was NOT native malloc's fill policy nor native string procs — it was RustExplorationManager._apply_state_metadata (angr/exploration/rust_manager.py). That helper mirrors a WHITELIST of SimOptions from the user's seed state onto the init-cache state, which is built from project.factory.blank_state() and therefore starts with angr's DEFAULT options. ZERO_FILL_UNCONSTRAINED_MEMORY/REGISTERS were not on the list, so the cached Python state used for SimProcedure callbacks (_cb_memory_load -> state.memory.load) hit DefaultFillerMixin.default_value with no zero-fill option and minted fresh mem BVSes for every unmapped byte; those symbolic bytes flowed back into Rust and fork-stormed. INVARIANT: any SimOption that changes VALUES (not just diagnostics) must be added to the _apply_state_metadata allow-list, else it is silently dropped across the init cache. Debug recipe that found it: monkeypatch DefaultFillerMixin._default_value to print a stack trace when it returns a symbolic value (scratchpad/sgcye-evidence/trace_fill.py).

Pattern for read-mostly fields in RustSimState that need O(1) fork: wrap in Arc and use Arc::make_mut on mutation. For methods that mutate, peek the read path first to skip the CoW clone when the operation would be a no-op (e.g. fd not found, nothing to read, invalid arg, re-adding an element already present, setting a key to the value it already holds). Otherwise every call to the mutator forces a deep clone even when no real change happens. See FileSystem::close/read/seek, RustSimState::clear_hooks/add_hook/remove_hook/set_option/setenv/unsetenv for the pattern. PER-ARC, NOT PER-METHOD: a mutator that unconditionally mutates one Arc field still needs the peek on every OTHER Arc it touches — FileSystem::install_fd always inserts into fds, but known_paths is a separate Arc, so re-opening an already-known path was deep-cloning that set for nothing (angr-5mnx3.38, fixed by the shared FileSystem::note_known_path peek helper). Do not reason 'this call always mutates, so the peek is pointless'. Avoid Arc-wrap for fields mutated on every fork (e.g. RegisterFile.symbolic) — make_mut churn would offset the savings. SAME RULE for im::OrdMap fields (SymbolicMemory::pages): OrdMap::get_mut copies the tree path down to the target key even if the closure changes nothing, so probe with the read-only get() before taking &mut — see SymbolicMemory::clear_multi_at (angr-fgqco), whose no-op path runs once per byte of every symbolic store. TESTING THIS INVARIANT: asserting on the collection's CONTENTS after a no-op mutation passes whether or not the clone was skipped, so it proves nothing — that vacuity is how five mutators drifted off the invariant unnoticed (angr-0jh0j.47). The only observable that distinguishes 'skipped the clone' from 'cloned into an equal value' is Arc::ptr_eq against a fork taken before the mutation; see state/tests/cow_peek.rs::shares_after and state/filesystem/tests.rs's *_skips_cow_clone tests.

The clippy::arc_with_non_send_sync suppression in arc_shared (native/angr/src/lib.rs) is NOT justified by single-threadedness — the engine steps states on real OS worker threads (exploration::scheduler_pool::worker_thread, named angr-worker-N). It is sound because RustSimState/SymContext are !Send by design and the ONLY cross-thread transport is StateMigrationPayload (state/migration.rs), which is Send-by-construction and compile-time guarded by assert_send::(); no unsafe impl Send/Sync exists in production code. So an arc_shared Arc cannot escape its worker except via detach_for_migration/reattach, which rebuilds the shared state on the destination thread. A contributor adding a genuinely cross-thread Arc must route it through that payload — do not widen the suppression. Same rationale now documented at SymContext::with_timeout (symbolic/context.rs) and SymContext::fork (symbolic/snapshot_fork_ops.rs). angr-e6p38, commit cac6f6a10.

arch/.rs CANONICAL vs ALIASES is NOT a naming taxonomy — it is the gate on what crosses the Python boundary. Only CANONICAL entries feed REGISTER_NAMES, which drives BOTH directions: RustStateSyncMixin.supported_register_names on the way in and RustSimState::export_full's named_registers on the way out. A register parked in ALIASES is therefore silently unexported: a Python-set state.regs. is dropped and a guest-computed value never comes back, each side reading 0 with no error. ARM's whole VFP file (d0-d31, fpscr, tpidruro, itstate) and AArch64's q0-q31/cc/tpidr_el0/qcflag/fpcr shipped this way for the life of the branch (angr-l8kfw).

Rules when adding/auditing an arch table:

1. Distinct guest storage with no other canonical entry covering the same bytes => CANONICAL. Only an overlapping SPELLING of storage some canonical entry already covers stays in ALIASES (x86 sub-registers, ARM32 qN over its dN pair, AArch64 vN/dN under qN). Exactly one spelling per offset may be canonical or Arch::register_name(offset) picks arbitrarily between them.
2. Prefer the FULL-WIDTH spelling as the canonical one (AArch64 qN, not dN) — a narrower canonical name truncates the register on export.
3. An exported name must also exist in archinfo's registers dict for that arch, or _sync_registers_to_rust's getattr(state.regs, name) raises. ARM32 has no qN in archinfo at all — that, not the overlap, is why qN cannot be exported there.
4. The VEX bookkeeping tail (emnote/cmstart/cmlen/nraddr/ip_at_syscall) stays alias-only on every arch; AMD64 is the reference for where the line sits. arch::registry_tests::every_narrow_canonical_register_is_exported enforces rule 1's consequence but only over canonical_registers(), so it is blind to anything still in ALIASES — the gap has to be caught by reading the table.

TEST-DESIGN COROLLARY: a boundary round-trip test must assert on a register the GUEST computed, never on the one Python preset — the preset value is still in the Python state's own copy, so the assertion passes vacuously even with the channel fully broken. tests/engines/rust/test_multiarch.py::test_vector_registers_cross_the_python_boundary uses a guest vector move (vmov d0,d1 / mov v0.16b,v1.16b) so both halves must work.

Prove the corollary holds rather than trusting it: delete the new names from that arch's REGISTER_NAMES, rebuild the .so, and confirm the test fails on the guest-written assertion. A test that still passes with the export list reverted is asserting on a preset value. The x86 half (angr-2uw03: cs/ds/es/fs/gs/ss + ldt/gdt) was checked this way and failed at "ebx reads back 0x0" as required.

The sweep is now complete for ARM/AArch64 (angr-l8kfw), MIPS32/64 (angr-n2556) and x86 (angr-2uw03). x86 also settled where rule 4's line sits below the tail: guest_SC_CLASS records HOW a syscall was entered (int $0x80 / sysenter), not architectural state a guest instruction reads, so it stays alias-only alongside emnote/cmstart/cmlen/nraddr/ip_at_syscall.

Arch register offset tables (native/angr/src/arch/*.rs 'mod offsets') must match archinfo/VEX guest layout EXACTLY, including omitted-but-real VEX blocks. Recurring bug class: amd64 GS_CONST (angr-a68t), MIPS64 FPU +8 (angr-mpln0), ARM32 -16 (angr-ihfe5). ARM32 root cause: table skipped the 16-byte VEX block at 108-127 (emnote/cmstart/cmlen/nraddr/ip_at_syscall), shifting D0-D31/fpscr/tpidruro/itstate -16; IR PUTs to real offsets fell past GUEST_STATE_SIZE and were silently dropped by RegisterFile::put (no else on the bounds check), GETs returned zero. TRAP: get_register/set_register share the SAME table, so name round-trip tests pass VACUOUSLY against wrong offsets. GUARD (as of angr-j4f1l): the generalized gate is tests/engines/rust/test_arch_offset_parity.py, covering all 6 arches x every shared register name for BOTH offset and size — run it after any arch table edit. The older per-arch checks test_arm32_offsets_match_archinfo / test_mips64_fpu_offsets_match_archinfo in test_multiarch.py remain as named regression anchors. Re-derive from archinfo.ArchXXX().registers, never hand-count. See [[arch-offset-parity-gate]].

Per-arch register tables in native/angr/src/arch/{amd64,x86,arm,arm64,mips}.rs use CANONICAL: &[RegEntry] + ALIASES: &[RegEntry] const slices, where RegEntry = (name, offset, size_bytes). The lookup_register_{offset,size,name} helpers in arch/mod.rs and the impl_arch_registers!(canonical, aliases, names) macro drive the trait methods. CANONICAL drives register_name(offset) reverse lookups (one canonical name per offset); ALIASES holds sub-register names sharing an offset (e.g., 'eax' aliases 'rax' on amd64) and is consulted only by name->offset/size forward lookups. To add a new register: add ONE row in CANONICAL (if reverse-mappable) or ALIASES (if just a forward alias) -- but if the name is also in REGISTER_NAMES it MUST be CANONICAL, see invariant-register-names-subset-of-canonical (angr-9ke6b.9 moved X86's sseround/xmm0..7/fpreg/fptag/fpround/fc3210/ftop out of ALIASES for exactly this reason). The (name, offset, size) triplet is a single source of truth. ARM canonical uses sp/lr/pc (not r13/r14/r15t); ARM64 uses fp/lr/sp (not x29/x30/xsp); MIPS uses ABI mnemonics (zero/at/v0/...) not numeric rN. MIPS64 register_name is intentionally narrow (only zero/v0/a0/sp/fp/ra/pc reverse-mappable) -- preserved bug-for-bug. Arch trait methods (sp_offset, ip_offset, bp_offset, syscall_num_offset) live alongside the tables. NOTE (angr-9ke6b.216): Arch::argument_registers() and Arch::return_register() were DELETED -- they had zero callers and duplicated the CallingConvention tables. ABI arg/return registers now live only on CallingConvention impls, which reference the per-arch 'offsets' modules (now pub(crate)) by const name. NEVER hand-code 'match VexArch { ... => (offset, size) }' tables in callers -- they will silently drift. Always reach data through self.registers.arch() or arch_from_vex(arch).(). If a needed lookup isn't on the trait, add a trait method, don't duplicate the match.

Rust engine evaluates ARM (arm32) conditional-load/branch guards SYMBOLICALLY, not concretely: armg_calculate_condition exists in vex/ccall/arm32.rs but the ARM cc_* flag thunks (cc_op/cc_dep1/...) read as 0/unconstrained from RegisterFile, so a guard like NE on a blank_state comes back symbolic. Net effect: a conditional ldrneh becomes r0=ITE(sym_guard, loaded, alt=0), and solver.eval picks the alt=0 branch. Consequence for tests: integration tests of ARM guarded ops cannot assert a concrete post-load register value; instead assert solver.satisfiable([reg==expected]) which proves the loaded branch carries the right width regardless of guard concreteness. Likely same family as angr-37d4 (arm64 csel fresh guards).

arm64g ccalls (arm64g_calculate_condition / _flags_nzcv / flag{n,z,c,v}) are implemented in native/angr/src/vex/ccall/arm64.rs as of angr-37d4. Key gotcha: angr's Python arm64g_calculate_flag_c/v for ADC/SBC keys the carry-comparison off cc_dep2 (!= 0), NOT the carry-in dep cc_dep3 — this looks like a Python bug vs VEX hardware semantics but we deliberately mirror it so the diff-fuzz vs the Python engine matches. cc_op set has explicit 32/64-bit variants (ADD32=1..LOGIC64=10); condition encoding is identical to 32-bit ARM so arm_cond/arm_flag_shift constants are reused. AL(14) and NV(15) are both unconditional-true on AArch64.

RustBV::as_u128() returns Some for BOTH Concrete and Constrained (symbolic-with-known-value) leaves — see RustBV::as_u128 in symbolic/value.rs. Any op that folds via match self.as_u128() { Some(v) => Self::concrete(v, ..) } therefore DESTROYS RustBV::Constrained{id} and turns a still-symbolic value into a bare Concrete. Downstream that is a wrong answer, not an error: query_class, memory::ite_builder, memory::multi and interpreter::concretize_cache key off Constrained.id for symbol tracking / structural hashing / cache keys, and interpreter::exits + interpreter::statements special-case Constrained as 'concrete value but still symbolic'. RULE for any new conversion op: check the width/shape IDENTITY case and return self BEFORE calling as_u128(). zero_extend_into/sign_extend_into always did; truncate_into and drive_extract (value_ops.rs) did not until angr-9ke6b.128 (commit 2421919b7). Folding IS correct when the op actually changes the value (narrowing truncate, partial extract, real extension) — that is a new leaf, not the same symbol. Regression tests: identity_truncate_extract_preserve_constrained_id / narrowing_truncate_extract_fold_constrained_to_concrete in symbolic/value_serde_tests.rs; they build the Constrained via serde round-trip because snapshot deserialization (RustBVData::Constrained arm) is the ONLY live constructor.

Release-build invariant checks in native/angr/src/ must use assert!, not debug_assert!: the workspace [profile.release] does NOT set debug-assertions, so it defaults to false and every debug_assert! compiles out of the shipped .so. (angr-03vl4.84 armed debug-assertions in [profile.release-checked] — the CI rust_test / ralph-gate TEST profile — so a debug_assert! now at least gets test coverage; the shipped wheel still builds against plain release, so this rule is unchanged.) Found in angr-9ke6b.68 — scheduler.rs worker_thread's WorkerCtl::Run arm guarded the 'no !Send state parked across the coordinator boundary' invariant with debug_assert!, giving release builds zero protection (a violation would silently re-park stale states, no diagnostic trail). Rule of thumb: debug_assert! is fine only for hot-path checks whose violation is already caught elsewhere; any invariant whose violation causes silent corruption gets a real assert!. Cost is usually nil — this one is a VecDeque::is_empty per session-loop return and the fast-tier bench suite showed no delta. Pairs with panic-abort-no-poison-invariant: under panic='abort' an assert! is a loud SIGABRT at the violation site, which is the module's documented failure mode (scheduler.rs 'Panic policy' header). The follow-on sweep angr-9ke6b.220 applied this rule to the rest of the crate and recorded the per-site verdicts (which sites were promoted, and the five classes deliberately LEFT debug-only) in debug-assert-triage-policy — consult that before promoting anything new.

Cross-cache invariant C5 (width-mismatch cache eviction) is enforced on BOTH bridge directions. IMPORT: claripy_bridge/import.rs::claripy_to_rustbv_depth compares cached_bv.width() to ast.length on an AST_CACHE hit, evicts via cache.rs::evict_bv_by_ast_hash and reconverts. EXPORT (added angr-ph300.54): claripy_bridge/export.rs::rustbv_to_claripy_memo compares the cached claripy AST .length to the requested Symbolic width on a get_claripy_ast(id) hit; on mismatch it calls cache.rs::evict_claripy_ast(id) — which removes the entry from the process-global SymbolicIdentityRegistry (global_registry().remove) — then falls through to re-mint+re-register. Guards against id-level aliasing (id:0 collisions, angr-owr37). Bool ASTs have length=None → treat as width 1 in both directions; since angr-5mnx3.12 that probe is ONE shared helper, cache.rs::claripy_ast_guard_width, carrying the single SILENT(cat-b) rationale (a raising getattr degrades to eviction+reconversion/re-mint, never a wrong-width result — angr-sqfj8.23). The two guards stay separate CALL SITES because their recovery differs (reconvert vs re-mint). The C5 text in claripy_bridge/mod.rs was rescoped in angr-5mnx3.13: it is AST_CACHE-specific and now names EXPRESSION_BY_OPERANDS_PTR (needs no check — its Arc-pinning key cannot be recycled, C4) and the registry (needs the analogous guard) explicitly, instead of the old universal 'other caches do not need it'. Unit test: cache_tests.rs::test_evict_claripy_ast_clears_registry. NOTE: the thread-local CLARIPY_AST_CACHE that evict used to also clear was REMOVED in angr-4xaga.2 (commit ac05abd92) — the registry is now the sole rust_id→AST store, and C2/C6 are gone; see claripy-bridge-thread-local-caches.

Regex audit gates (tools/audit_overflow_wraparound.py, audit_sp_default_zero.py, audit_rounding_mode_threading.py, audit_silent_fallback.py, audit_page_shift.py, check_line_citations.py) report 'OK, 0 new' whenever nothing matched their GRAMMAR — which is not the same as 'no such site exists'. RULE: when a bug is found by review inside a directory some gate already scans, treat the gate's silence as a second defect and widen the detector in the SAME commit — patching only the flagged site leaves the class open. Two confirmed instances, and note they are different KINDS of blind spot. (a) Incomplete grammar, angr-5mnx3.53: do_mmap's addr=0 align-up '(new_base & !PAGE_MASK) + PAGE_SIZE' was a real u64 overflow the gate never reported, because BINOP_RE's OPERAND only matched identifier/dotted-field/numeric-literal and cannot begin an operand at ')'. (b) DELIBERATE exclusion, angr-fs8kb.52: BINOP_RE's '(?![=>])' lookahead was written to skip '+=' / '-=' / '->', so a stepped address 'page_addr += PAGE_SIZE' was invisible project-wide — which is how two page-walk wraparounds (angr-fs8kb.49, .51) landed in syscalls/ while it was fully scanned with an empty baseline. So also audit what a gate intentionally excludes, not only what its grammar happens to miss; a lookahead added for noise control is a silent scope cut. Four corollaries. (1) Every widening needs BOTH a must-fire and a must-NOT-fire control in the script's --self-test (the .52 widening added a stats-counter control and a '+=' whose address-shaped name is on the right). (2) A widening usually surfaces sites that were always there; expect to triage them in the same commit — .53's two hits already carried an 'overflow-ok:' rationale that fell just outside the three-line window, .52 surfaced 9 bounded loop counters needing fresh markers, and angr-fs8kb.91's new page-arithmetic gate surfaced 7 open-coded sites in state/export.rs + syscalls/cgc.rs + procedures/test_util.rs. (3) If naive widening is dominated by one benign shape, narrow by MEANING rather than abandoning it: the overflow gate's detector 2 keys on the compound assignment's DESTINATION name only (in 'a += b' the LHS is the accumulator) and on that name's LAST ''-separated component, minus 'count' — 77 raw hits down to 9 real ones. audit_page_shift.py's detector 2 does the same for magic page literals: requiring the literal be ADJACENT TO AN OPERATOR whose other side is an address-shaped name drops every legitimate 'const MAX_...: usize = 4096;' buffer bound, because those sit to the right of an '='. (4) A prose sentence in a doc comment saying a class 'keeps coming back every audit round' (PageIndex's doc in memory/page.rs said exactly that across angr-c7xno.49 / angr-sqfj8.140 / angr-fs8kb.70) IS a gate that has not been written yet — treat that phrasing as the trigger to write one, not as documentation.

Bare SymContext::pop() (transaction_ops.rs) must roll back the LOCAL constraint bookkeeping, not just the Z3 frame. scope_savepoint_push/pop (lineage_ops.rs) record/truncate (z3_assertions.len, assumed.len, non_bv_assertions.len) via the bare_local_savepoints stack and clear dedup_set on truncate — mirroring transaction_rollback, which is the ONLY other path that truncates these logs. Why it matters: the Z3 solver pop(1) forgets the assertions, but the local z3_assertions log feeds (a) add_constraint dedup (stale ptr -> re-add silently skipped, angr-ph300.41) and (b) fork() replay (stale entries frozen into child as permanent asserts, angr-ph300.42). transaction_commit deliberately does NOT pop (frame kept), so its savepoint entry leaks by design; transaction_rollback re-truncates idempotently to the same length. Guard the truncate on len-grew so hot interpreter fork-guard push/pop with no adds is free. Note: non_bv_assertions is truncated here but transaction_rollback still ignores it (latent gap).

Rust engine: bare SymContext::push()/pop() (transaction_ops.rs) restores the Z3 solver frame and scope_path but does NOT truncate local.assumed (the assumed export/re-assert log) — only transaction_rollback did. Any assume_true/assume_false made inside a bare push()/pop() scope leaks permanently into local.assumed. The deferred-fork block-feasibility loop in interpreter/statements.rs (prev-fork assert loop, popped at execution.rs block end) hit this: its feasibility-only assumes leaked and got re-asserted verbatim by restore_from_snapshot on wave migration (the spurious re-asserts angr-kenpr's constraint_count pin compensates for). FIX (commit 02ce2aae3, angr-ype54 iter34): SymContext::assumed_local_len + truncate_assumed_local bracket the loop. INVARIANT: if you add assume_* calls inside a bare push()/pop() (not a transaction), snapshot assumed_local_len first and truncate_assumed_local after, or they poison the export log. SIBLING FIX (angr-c7xno.75): the same loop also leaked into local.z3_assertions via fork()'s freeze — truncate_assumed_local only touches local.assumed. fork() now refuses to drain any local log while bare_local_savepoints is non-empty, so the z3_assertions half is closed at the fork gate rather than per-call-site. The assumed_local_len bracket is still required (it covers the export log independent of forking).

Invariant for any future consumer of SymContext::bare_z3_push_depth (angr-3ms1 step 1a, revised angr-c7xno.75): the counter ONLY reflects pushes on THIS context's per-context Z3 solver (None lineage branch). It is always 0 along the Some (shared-lineage) branch, which records on scope_savepoints instead. Consequences: (1) the slice-1c fork-time materialization gate reads the parent counter at fork time — a non-zero value means parent has unbalanced bare pushes on its per-context solver, which would corrupt the shared lineage Z3 stack if a lineage were minted. (2) Children do NOT inherit the parent's value — fork() resets it to 0 (angr-c7xno.75, was inherited before). A child owns no open Z3 scopes: its bare_local_savepoints starts empty and SymContext::solver()'s cold-start replay emits flat assert()s, never push(). Inheriting a non-zero value made try_pop() (gated solely on this counter) forward a pop(1) to a never-pushed solver and permanently disqualified the child from lineage minting via gate (b). (3) When mixing Some and None paths (a context starts None, gets bare pushes, then has a lineage installed), the counter would still reflect the bare pushes — the gate should consider this case if it ever arises. Note this counter is NOT the 'is a scope open?' indicator: bare_local_savepoints is (it records on BOTH dispatch branches), and that is what fork()'s freeze gate and debug_assert_no_open_scope read.

baseline_counters.json must contain a key for every NON-bimodal fast+medium SUITE bench in run_regression.py (key = name, or name__dfs for dfs-strategy entries; bimodal benches in BIMODAL_BENCHMARKS are excluded since their Z3-path nondeterminism makes per-counter diffs noise). Gated by run_regression.expected_counter_keys/missing_counter_keys + 'python run_regression.py --check-counter-coverage --full' (CI step) + tests/benchmarks/test_counter_coverage.py. As of 2026-06-19: 19 fast + 7 medium = 26 keys. Adding a bench without rerunning --update-counters now reddens CI instead of silently dropping its bench_diff report.

run_zeropy_gate.py corpus keys are baseline_timings.json keys, NOT run_single example names. Two traps, both fixed in iter129 (angr-gorvf.4.4): (1) the '__dfs' suffix is a baseline-key convention owned by run_regression._baseline_key_for so one example can carry bfs+dfs counter snapshots -- run_single knows nothing about it and needs (example, --strategy dfs). run_zeropy_gate.split_baseline_key() inverts it. Any NEW harness that iterates baseline_timings keys and shells out to run_single must do the same split or it will die with 'solve.py not found'. (2) A bench with rust_time=null (CADET_00001) has never completed under the Rust engine (divergent explore, angr-027h) and cannot produce counters -- run_zeropy_gate.no_rust_baseline() short-circuits it to UNMEASURED instead of burning the full timeout into ERROR. Also: run_single traps its own timeout and exits cleanly WITHOUT the trailing JSON, so a divergent bench never trips a caller's subprocess TimeoutExpired -- match its 'TIMEOUT rust ' stdout line to tell a timeout apart from a real failure.

Bench-harness engine swap lives in ONE place: tests/benchmarks/engine_patch.py::install_rust_engine_patch (shared by run_single.py::_run_in_child and run_leak_check.py::_run_iters_in_child). It patches AngrObjectFactory.simulation_manager/.simgr to build a Rust manager via a make_manager(project, states) callback, and falls back to the Python factory for callers under PYTHON_ENGINE_CALLERS (/angr/analyses/, /angr/exploration_techniques/, /angr/simos/) plus any call passing a non-empty techniques= list. NEVER widen the exclusion to /angr/callable.py: that silently routes Callable-heavy benches (mma_howtouse, flareon2015_10) entirely to the Python engine (angr-zbpw0). Any NEW bench harness that drives solve.py must import this helper -- run_leak_check went a full release measuring the Python engine because it didn't (angr-pm8ha). Assert managers_built > 0 as the fidelity guard.

run_regression.py's FAST_SUITE/MEDIUM_SUITE membership is a hand-maintained runtime-BUDGET split (fast <10s, medium 10-60s) and is deliberately NOT a mirror of the 'tier' field in run_single.EXAMPLE_CATALOG (fast <5s, medium 5-30s, gated by validate_tier.py + test_validate_tier.py). Six MEDIUM_SUITE members are catalog tier='fast' after the perf waves: sym-write, flareon2015_5, flareon2015_10, ekopartyctf2016_rev250, csaw_wyvern, codegate_2017-angrybird. Retiering a bench in the catalog must NOT move it between suites — 'syncing' the two would silently shrink what 'run_regression.py --full' gates. test_medium_suite_membership_is_independent_of_catalog_tier (tests/benchmarks/test_validate_tier.py) pins that set. Symptom that surfaces stale labels: test_audit_real_catalog_smoke goes red with 'Unexpected tier drift'; the fix is normally the catalog label, not the measured number — confirm with 'run_single.py --engine rust' first (angr-a1k7j, 2026-08-01). EARLIER STATEMENT (same invariant from an earlier pass): the catalog tier is a measured-runtime classification via validate_tier.classify with FOUR bands -- fast <5s, medium <30s, slow <120s, very_slow -- gated by test_validate_tier.py::test_audit_real_catalog_smoke against baseline_timings.json; MEDIUM_SUITE is a hand-maintained --full runtime-budget list of (name, timeout[, strategy[, rust_only]]) tuples, independent of the catalog tier by design and must not be reconciled with it. flareon2015_10 joining the fast-tier-but-MEDIUM_SUITE set was first noted per angr-zm7im, before the later angr-a1k7j pass recorded above.

tests/benchmarks/run_regression.py FAST_SUITE/MEDIUM_SUITE entries are tuples: (name, timeout, [strategy, [rust_only]]). Positional with len(e) defaults: strategy='bfs' if missing, rust_only=False if missing. Adding a new benchmark: append a tuple, run 'python run_regression.py --update --full --check-counts' to populate baseline_timings.json with full algorithmic stats (callback_count, state_creations, steps, peak_memory_mb, rust_time, python_time). Most entries are rust_only because of OOM/output-divergence on this hardware (entry counts drift; read the suite lists for the live set). rust_only rationale: several benchmarks (csaw_wyvern, securityfest_fairlight, ekopartyctf2016_rev250, csgames2018, whitehatvn2015_re400, sym-write) Python engine OOMs or timeouts under the 4GB run_single.py memory limit on 8GB no-swap machines — their original baselines were captured on beefier hardware. Mark such benches rust_only=True so the regression suite tracks only Rust timing + algorithmic metrics for them. The 4GB limit is intentional — it prevents OOM-killing the orchestrator.

op_binary! macro (native/angr/src/symbolic/table.rs) validates equal operand width before delegating to the RustBV method, returning Python-agnostic BinaryOpError (MissingHandle | WidthMismatch). solver.rs owns 'impl From for PyErr' (keeps table.rs pyo3-free) and the 25 op_* pymethods map errors via .map_err(PyErr::from). ALL 24+ binary ops require equal width incl shifts (shift amount is resized to value width before this layer) — eq_into/ne_into/arith/cmp all only debug_assert_eq! width, so a release build would hand mismatched sorts to Z3 and abort under panic=abort. op_concat is NOT op_binary!-generated and legitimately allows different widths (result width = sum) — never add an equal-width check to it.

The internal Z3 lowering (build_z3_ast_cached in native/angr/src/symbolic/value_z3.rs) and the claripy EXPORT path (build_sound_bitcount in native/angr/src/claripy_bridge/export/ast_helpers.rs, moved there by angr-5mnx3.11) are TWO separate lowerings of Clz/Ctz/Popcount that must stay in sync ON VALUE, not on structure. Both must build an operand-tied encoding: clz/ctz -> ITE ladder over per-bit tests, popcount -> sum of zero-extended bits. Never use z3 BV::new_const(name,width) for these: Z3 hash-conses named consts so every symbolic clz of a given width aliases to ONE shared unconstrained variable, making clz(x)==0 && clz(y)==5 UNSAT (prunes feasible branches) and letting eval(x) ignore the clz constraint. Fixed angr-ph300.29 (internal path); export path fixed earlier via test_lzcnt_symbolic_export_is_sound. Since angr-0jh0j.54 the two lowerings DIVERGE structurally: the Rust Z3 arm accumulates the ladder at bitcount_acc_width (ilog2(width)+1 bits) and zero_ext's once, because accumulating at the operand width is O(width^2) (width constants of width bits each, ~137 GiB at MAX_BV_WIDTH); build_sound_bitcount does not, and does not need to, because its caller already refuses width > 64. Keep the accumulator wide enough to hold the value 'width' itself -- clz/ctz of an all-zero operand IS width, and that is the only case a correctness test can distinguish, so any regression test for the sizing must pin an all-zero operand at a width above 64.

ZeroPy gate: the park-and-bounce excursion is NOT a GilWorkGuard region. When a Python SimProcedure/syscall/hook/symbolic-branch handler runs, the Rust run loop has RETURNED: RunLoopWallGuard is dropped and no GilWorkGuard is live, so BOTH gil_work_time_ns and run_wall_time_ns are stopped across it. Pre-angr-gorvf.8 this made gil==0 a FAKE PASS (fauxware executed a 59.6ms Python 'open' proc at gil==0). FIXED by GilClass::Bounce in gil_profile.rs: park_start(enabled) armed in the run() pymethod when it returns with pending_callbacks non-empty; park_end() at the top of the four resume bodies in exploration/resume.rs (_resume_after_simprocedure, _deadend_pending_callback, _resume_after_error, _resume_after_symbolic_branch) banks the elapsed into BOTH GIL_ACCUM_NS (class Bounce) and WALL_ACCUM_NS (so gil<=wall holds); park_cancel() at run() entry discards a park Python never resumed, so driver-loop overhead is not counted as exploration Python. INVARIANT for future callbacks: any NEW park-and-bounce reason must route its resume through one of those four bodies or it will be invisible to the gate again.

Bounce-target history contract (angr-9ke6b.51): the bounce entry address lands in RustSimState::history() EXACTLY ONCE per visit, appended by whichever site is LAST to touch the state — never by every restore site. The worker core's bounce() (core_outcome.rs / core_outcome_handlers.rs) appends NOTHING. TERMINAL restores must append: dispatch_bounce's BounceKind::Hook / SimProcedurePython arms (stepping.rs) and route_materialized_terminal's find/avoid short-circuit (run_loop.rs) all pair set_pc(addr)+add_to_history(addr) because the state is either handed to a Python callback or pushed to FOUND/AVOID and never stepped again. flush_parked_bounces_to_active (run_loop.rs) deliberately does set_pc WITHOUT add_to_history: it is the ONLY non-terminal restore — the state goes back to STASH_ACTIVE and its next step re-lifts the hook and re-enters dispatch_bounce, which appends there. add_to_history (state/history.rs) never dedups, so 'fixing' the flush to match its siblings double-counts one visit. Pinned by run_loop_tests.rs::terminal_bounce_restore_appends_the_target_to_history and ::flush_parked_bounce_leaves_history_for_the_replay_to_append. Rule for any future bounce-restore site: append iff the state will not be re-stepped.

angr-gorvf.15 root cause + fallout: retiring a Python SimProcedure bounce can BREAK the driver, because RustExplorationManager's explore loop only regains control between native batches. Three latent bugs surfaced the moment fauxware stopped bouncing (all fixed in 92c6de8b6, angr/exploration/rust_manager.py): (1) _explore_with_addresses/_explore_with_predicates batched 50 native steps between 'until' predicate checks — Python's SimulationManager.run(until=) checks after EVERY step, so fauxware's run(until=len(active)>1) ran the whole program and emptied the active stash (batch_size is now 1 whenever until is set); (2) the full-batch path called an unbounded rust_mgr.run() even with max_steps set, so run(max_steps=1) executed to completion (now run(max_steps - steps_taken)); (3) the progress callback fired only from _check_limits at the TOP of an iteration, so a run finishing inside one batch never fired it (now also fires post-batch via _fire_progress_if_due). LESSON: any future native-proc widening must re-run the whole tests/engines/rust suite — a bounce is an implicit per-step yield point that driver code silently depends on.

Overflow triage, bug shape the audit can't see: the BOUNDS CHECK itself is an overflow site when its index is wrapping-derived. SymbolicMemory::extract_byte_lane (memory/load.rs) guarded with '(byte_offset + 1) * 8 > total_bits'; both callers (assemble_load_with_multi, try_byte_merge_load) form byte_offset as '(byte_addr - base_addr) as u32', and Sub for Address is wrapping_sub — so a stale symbolic_spans entry whose base sits ABOVE the byte yields a near-u32::MAX offset, the product wraps to a small value with release overflow-checks off, the check PASSES, and the big-endian arm computes an underflowed 'total_bits - byte_offset8 - 1'. Fixed by 'byte_offset.checked_add(1)?.checked_mul(8)?' — refuse, per invariant-overflow-fix-refuse-not-saturate-identities (an offset with no representable bit position IS out of range). Generalization: whenever an index crosses a wrapping boundary (Address diff, guest register, Python-supplied size), the guard that validates it must use checked_ even though the guarded expression looks safe once guarded. tools/audit_overflow_wraparound.py flags the guarded expression, never the guard, so an 'overflow-ok: guarded above' comment can silently bless a broken guard — read the guard before writing that comment. Regression: test_extract_byte_lane_refuses_wrapping_byte_offset (memory/tests/symbolic_wide.rs). Related: invariant-address-containment-wrapping-distance.

Wave-parallel cancel has TWO flavors and conflating them livelocks small run(n) calls (angr-9ke6b.52). CancelToken::cancel() = find/num_find/session-finalize: parallel_process_state's pre-step guard (run_loop.rs, the 'preempts_in_flight' branch) hands the state back UNSTEPPED so post-find speculation is not wasted. CancelToken::cancel_for_budget() = the wave dispatch budget (WorkTransport::max_dispatches, set by WaveJob::set_max_dispatches from run_loop_parallel_wave's remaining max_steps): the in-flight step MUST complete, because the dispatch was already charged to the budget. First attempt used plain cancel() for the budget and deadended_count went 14 -> 0 on tests/engines/rust/test_parallel_wave.py::test_deadended_count_survives_the_worker_boundary[4]: RustExplorationManager.run(n=N) maps to N native run(1) calls, so the wave budget is 1 -- a peer worker observed the budget spent and cancelled while the ONE worker that had dispatched was mid-step, which then bailed unstepped, so 4096 python-side steps advanced the manager by 4 steps total. Rule for any future 'stop the wave' signal: decide whether it should preempt already-dispatched work, and if not, route it through preempts_in_flight()==false.

audit_overflow_wraparound.py scans bare +/- only, so a bare '*' on address/size operands is invisible to it. That blind spot matters because a wrapping multiply fails differently from a wrapping add: the add-side bug is a range check that wraps large, but a multiply can wrap to a value that is small (2^63 * 2 == 0), so a 'units * size > CAP' budget guard silently ACCEPTS an unbounded loop instead of refusing it. Rule: any product feeding a cap/budget comparison uses saturating_mul (saturating is correct here precisely because the saturated value is unambiguously over-cap and therefore refuses). Precedent: procedures/mem_common.rs::check_store_budget, shared by memset.rs::memset_symbolic_addr and memcpy.rs::copy_symbolic_addr. Companion to invariant-rust-concrete-arith-must-wrap (which covers +/- address arithmetic).

native/angr/src/interpreter/concretize_cache.rs::bv_cache_key is the per-block address-concretization cache key. It MUST hash the full RustBV op tree (helper fn hash_bv recurses over operands with a per-variant tag byte + operand count + leaf ids/values). Two prior collision bugs (angr-owr37): (1) nested Expression operands hashed only (discriminant(op),width), so Add(And(x,0xf),c)==Add(And(y,0xf),c) -> concretize_cached_write returned the wrong store target (silent wrong-address corruption in default rust-memory config); (2) BVOp carries inline payload (Extract(hi,lo), ZeroExt(n), Float{kind,prec}) so hashing only discriminant collided Extract(7,0,x) with Extract(15,8,x) -> hash the whole op. Expression id is always the EXPRESSION_ID sentinel (u64::MAX), so it gives NO identity — never rely on it for cache keys. Regression tests in concretize_cache_tests.rs.

Rust native syscalls/procs that write a buffer with a byte-at-a-time state.memory_store loop (canonical: syscalls/directory.rs::NativeGetcwdSyscall::call) are intentionally NOT all-or-nothing: on a mid-buffer fault the bytes already stored stay committed and the handler returns -EFAULT. Do NOT 'fix' this into a rollback/staging buffer — it would diverge from both models we mirror. Real Linux copy_to_user keeps whatever it copied before the fault, and the Python SimProcedure's single state.memory.store (e.g. procedures/linux_kernel/cwd.py::getcwd) commits page by page before SimSegfaultException unwinds. A future audit round flagging one of these loops as a 'partial write bug' should document + pin it instead; directory_tests.rs::getcwd_partial_write_is_not_rolled_back is the pattern to copy. Corollary for callers: a -EFAULT return means the buffer is CLOBBERED, not preserved.

Rust-engine memoization caches must key on EVERYTHING the cached value depends on, not just the input expression. interpreter/concretize_cache.rs::bv_cache_key has now been the site of three separate wrong-answer bugs of exactly this shape: angr-owr37 (nested leaf identity dropped -> two distinct addresses collided), angr-9ke6b.89 (leaf variant untagged -> Concrete{value:N} vs Symbolic{id:N} collided), angr-360gt (producer CONFIG untagged -> a Multiple computed under read_range_limit=1024 was served to a store bound by write_range_limit=128, bypassing its Max fallback). The third is the subtle class: the key covered the input perfectly, but the cached value also depended on WHICH strategy chain produced it. Fix pattern: a namespace discriminant hashed into the key (see enum ConcretizeNs), not a post-hoc re-validation on hit — re-validation only works for shapes that carry their limit (TooLarge does; Multiple/Strided produced by the <=16 fast-enum path do not, since that path never consults the limit). When adding a new consumer to a shared cache, ask what config the entry was computed under; if it can differ, give it its own namespace. SECOND RULE: a call-site precondition NEVER justifies dropping a field from a RECURSIVE hash/key function. bv_cache_key's 'all call sites early-return on as_u64(), so Concrete/Constrained never reach here' argument scopes only to the TOP-LEVEL value; hash_bv recurses into Expression operands where those variants are routine — angr-fs8kb.65 dropped Constrained's value field under exactly that justification, making Add(y,Constrained{id:5,value:10}) and Add(y,Constrained{id:5,value:20}) hash identically (a guaranteed collision). Every arm hashes its full payload, and do not reintroduce a 'cheap' untagged leaf shortcut for perf (the symbolic-leaf hash is ns against a Z3 concretize call; bench gate showed no movement). Details live on bv_cache_key / hash_bv in interpreter/concretize_cache.rs.

Callback fd-table sync (angr-op0dn.14.1.5): a bounced Python SimProcedure's open() picks the fd NUMBER from state.posix._pick_fd, so Rust must adopt it AT that number — FileSystem::register_fd_at (not ::open, which draws from next_fd) — and bump next_fd past it. register_fd_at refuses (returns false, changes nothing) when the fd already exists; that refusal is what makes _sync_state_posix_fds_to_rust idempotent across the repeated callbacks that share one cached state. Rust fds hold CONCRETE bytes: an fd whose SimFile content or seek pos is symbolic is deliberately left unregistered, because adopting it with an empty buffer would make a native read return wrong bytes (worse than the pre-existing fallback). Sits alongside _sync_state_heap_to_rust / _sync_state_posix_to_rust on the same 3 resume sites in rust_callback_dispatch.

Callback fd-table sync is now BIDIRECTIONAL (angr-op0dn.14.1.5 out + .14.1.6 in). Inbound: rust_callback_dispatch::_inject_rust_fds mirrors every Rust fd>2 into the callback state's state.posix.fd (SimFileDescriptor at the SAME number, _pos from Rust) + a concrete SimFile in state.fs, called from _create_state_for_callback next to _inject_rust_stdout. Two bugs it fixes: (1) a bounced proc reading/writing a natively-opened fd hit a closed fd; (2) posix._pick_fd only knows Python's fds, so a bounced open() could pick a number Rust already used — the sides then point at different files under one fd. Fast path: new FFI has_state_extra_fds (FileSystem::has_fds_above_stderr) so the common bounce never builds the get_state_open_fds tuple list. Deliberate loss: if state.fs already holds a SimFile for that path (pre-seeded harness file), it is reused as-is and Rust's appended bytes are NOT merged — clobbering possibly-symbolic pre-seeded content with a concrete snapshot would be worse. Tests: TestCallbackFdInboundSync in tests/engines/rust/test_state_sync.py.

Callback-state heap plugin: NEVER materialize state.heap eagerly on the SimProcedure-callback path. SimHeapBase.init_state calls state.memory.map_region(0xC0000000, 0x800000) — an 8MB region map that measures ~40-65ms per state (profiled 2026-07-13 via cProfile on a blank AMD64 state). Touching state.heap in _create_state_for_callback would add that to EVERY bounce (already ~2.8ms/call). Pattern used instead (angr-op0dn.14.1.3, rust_callback_dispatch::_install_lazy_heap_sync): if 'heap' in state.plugins -> sync now (cheap dict test); else patch the instance's get_plugin (SimState.getattr routes an unregistered plugin through self.get_plugin, so an instance-level override fires exactly once, only for callbacks that actually touch the heap). In practice the plugin IS already materialized on callback states, because rust_manager::_add_rust_state's init-time heap_location push does getattr(state,'heap') on the seed. The same instance-patch trick works for any other lazily-materialized expensive plugin.

SimProcedure-callback posix sync (angr-op0dn.14.1.4): the bounce now round-trips fd output buffers in BOTH directions, and both halves are PREFIX-DELTA based, not append-based. Inbound rust_callback_dispatch::_inject_rust_stdout / _inject_rust_fd_output writes only rust_buf[py_len:]; outbound rust_state_export::_sync_state_posix_to_rust pushes only py_bytes[rust_len:] via the new Rust append_state_fd_output. Idempotency is LOAD-BEARING, not a nicety: _create_state_for_callback commonly reuses the CACHED SimState in place (no copy when no predicates/proxies are on), so a blind append would duplicate stdout on every bounce; _sync_cached_state also re-injects on every export. The length-based outbound delta is only sound because the inbound injection keeps the Python stream a prefix of Rust's buffer — keep the two directions over the SAME fd set (POSIX_SYNC_FDS = (1,2)).

PythonCallbacks naming beads (e.g. angr-9ke6b.29) should be closed with DOCS, not renames: each call_<x> / has_<x> / set_<x> in native/angr/src/callbacks/{dispatch,mod}.rs is keyed to a Python callback SLOT of the same name, wired by rust_manager.py::_setup_callbacks and asserted by name in error strings (' callback not set') that tests match on. Renaming the Rust side alone desyncs the trio from the slot and breaks grep-by-slot-name; renaming both ends is a Python-surface change for a readability win. The canonical example: the three symbolic-store variants now carry a selector list in the dispatch.rs module doc — call_memory_store_symbolic_value = concrete address + AST data, call_memory_store_symbolic_full = symbolic address (data either), and bare call_memory_store_symbolic is NOT a third mode, it forwards to _full and hard-errors when _full is unwired (angr-ph300.64).

When a Rust->Python bounce hands a SimState to a Python engine, the callback state is NOT a VEX-executed state: it has no history.parent jumpkind and none of the VEX-set pseudo-registers (ip_at_syscall, and by extension anything else VEX writes on an exit). Any Python code path that depends on those — SimEngineSyscall's Ijk_Sys* dispatch check, SimCCSyscall.return_addr = SimRegArg('ip_at_syscall') — silently degrades. Resolve procedures explicitly and seed the pseudo-registers yourself rather than relying on the engine's own dispatch. Discovered in angr-89w70; see syscall-fallback-root-cause.

RustCallStackProxy (the lightweight view on RustStateProxy) reads call frames LIVE on every _frames access — no Python-side cache (angr-qwyti.10). It calls mgr.get_state_call_stack(state_id) then list(reversed(raw)) each time. iter/getitem/top snapshot once and pass _StaticFrameOwner so a single access stays consistent for frame.next walks. Why removed the old _frames_cache: a RustStateProxy memoizes its .callstack sub-proxy, so a permanently-cached frame list served pre-step frames if the view was held across a Rust step on the same state_id (same stale-cache shape as register-proxy _cache in angr-4rq7 and solver-fallback fork in angr-hv4lt.9). The sibling RustCallStackProxyPlugin (installed on materialized states) already read live every access; the view now matches. How to apply: never reintroduce a persistent _frames cache on either callstack proxy; keep both live-read. Pinned by test_callstack_proxy_reads_live_not_stale + test_callstack_proxy_independent_across_states (tests/engines/rust/test_proxy.py).

Rust unit tests (cargo test, default features) CANNOT lift a VEX block. The native lifter is behind the libvex-ffi feature, which is deliberately NOT in Cargo.toml's default set (setup.py appends it, so pip/CI builds have it but cargo test does not). Without it, VEXInterpreter block lifting routes through the unregistered Python lift_block callback and fails. CONSEQUENCE for test design: a #[cfg(test)] test that wants to drive run_interpreter_step_core / parallel_process_state to a post-step outcome (CoreReturn::Continue/Deadended/Errored/Unconstrained) would assert a DIFFERENT thing depending on the feature set — do not write one. What IS reachable without a lifter: a hooked/simproc'd initial pc, which short-circuits before any lift and yields CoreReturn::NeedsPython (BounceKind::Hook / SimProcedurePython). Post-step arm classification is instead unit-tested directly on run_post_step_core (core_outcome_tests/, split per RunResult arm); the worker's routing of them is covered by the Python tests/engines/rust/ parallel suite. Precedent + rationale live in the module headers of step_core_tests.rs and run_loop_worker_tests.rs.

INVARIANT: Single-word VEX CAS leaves oldHi=0xFFFFFFFF (libVEX IRTemp_INVALID sentinel) on the pyvex side, with expdHi=None and dataHi=None. The Rust execute_cas_stmt validates oldHi/expdHi/dataHi as all-Some (DCAS) or all-None (single) — any mixed shape errors with InvalidIR. The native lift path is native/angr/src/vex/pyvex_bridge.rs, which deserializes oldHi directly as Option (#[serde(rename = "oldHi")] old_hi: Option, consumed in execute_cas_stmt build). The actual 0xFFFFFFFF→None mapping is done Python-side in angr/exploration/rust_irsb_serializer.py (result["oldHi"] = None if old_hi == 0xFFFFFFFF else old_hi) before serialization, so the JSON fallback lift never sees the sentinel. Bug fixed 2026-05-21 (angr-4enc): previously the serializer passed the sentinel through verbatim, so LOCK CMPXCHG via the Python fallback lift errored (DCAS via cmpxchg16b passed because oldHi was a real temp index).

EXAMPLE_CATALOG['tier'] in tests/benchmarks/run_single.py does NOT drive the CI benchmark gates. run_regression.py's FAST_SUITE and MEDIUM_SUITE are hardcoded lists of (name, timeout, strategy, both) tuples and never read the tier field. tier is consumed ONLY by run_single.py --suite / --list selection and property_fuzzer.py::_eligible (which skips slow/very_slow to keep fuzz throughput up). So retiering a bench is safe metadata maintenance — it cannot change what the PR gate or nightly gate runs. Corollary: adding a bench to a CI gate requires editing FAST_SUITE/MEDIUM_SUITE directly; setting tier='fast' does nothing. validate_tier.py::audit() cross-checks tier against baseline_timings.json rust_time (+/-10pct boundary slack) and test_validate_tier.py::test_audit_real_catalog_smoke gates it, so a stale tier shows up as a red test, not a gate change. (angr-ko17e, 2026-07-13)

Each CallingConvention impl must use the right return-register offset for its target arch's VEX guest state. EAX in x86 = offset 8. RAX in amd64 = offset 16. Don't copy offsets across calling conventions. Since angr-9ke6b.216 the impls no longer spell the numbers at all: calling_conventions.rs imports each arch's 'offsets' module (amd64_off, x86_off, arm_off, arm64_off, mips32_off, mips64_off -- all pub(crate) since .216) and every ABI table is a slice of named consts, so a wrong-arch copy is now visible at the call site. Two tests lock it: test_return_register_offsets_per_arch (calling_conventions_tests.rs) keeps INDEPENDENT hardcoded literals as a foreign oracle -- do NOT convert it to reference the consts, that would make it tautological -- and test_cc_arg_registers_resolve_to_expected_register_names maps every CC arg/syscall-arg/return offset through Arch::register_name and asserts the expected mnemonic list per ALL_ARCHES row. Extend both whenever a new CC is added. Why: latent in code until any native SimProcedure returns a result for that arch (most fall back to Python via SymbolicArgument); when the wrong register gets the symbolic result, downstream cmp/jne against the right register sees stale concrete data and resolves without forking, silently breaking the binary's control flow.

CCall symbolic dispatch drifts BETWEEN ARCH SIBLINGS, not just between builder and consumer. Since the angr-5mnx3.60 helper split, native/angr/src/vex/ccall/mod.rs::handle_ccall_with_ctx is pure name dispatch and the near-identical arm pairs are sibling helper FUNCTIONS — handle_arm32_condition/flags_nzcv/flag_single vs handle_arm64_, handle_x86_calculate_condition/eflags_c/eflags_all covering both x86g_ and amd64g_. A symbolic branch added to one sibling is repeatedly never mirrored onto the other: angr-0jh0j.70 found armg_calculate_flag_n/z/c/v concrete-only while arm64g_calculate_flag_ had had its symbolic branch all along, even though arm_sym_flag_n/z/c/v already existed in ccall/arm32.rs and were already used by arm_sym_calculate_condition in the same file. INVARIANT: when touching any handle_* helper, grep the sibling-arch CCall name and confirm both have the same concrete+symbolic structure; a missing symbolic branch is a silent ~30x wall-clock Python fallback (angr-9ke6b.88), not a visible error. angr-zgd3r closed the last known ARM gap by adding arm_sym_flags_nzcv / arm64_sym_flags_nzcv — note it fixed BOTH siblings in one commit, which is the shape to aim for. Corollary from that fix: a packed-flags symbolic path must refuse a ret_bits too narrow to hold its top shift (sym_pack_nzcv returns None for ret_bits <= SHIFT_N) — RustBV shift amounts are built at the result width and would wrap silently. Anchor tests on the coverage pattern (iterate the whole cc_op range, assert nothing returns None) plus a z3-gated diff-fuzz that pins a symbolic dep with add_bv_constraint and compares ctx.eval against the concrete calculator — see arm32_flag_ccalls_symbolic_cover_every_cc_op / diff_fuzz_arm_flags_nzcv_symbolic_matches_concrete in vex/ccall_tests.rs. Related: invariant-symflags-category-coverage (the builder-vs-consumer half of the same family).

Symbolic ccall flag masks must reuse the same named G_CC_MASK_* constants as the concrete calculate_eflags_all path, never a hand-derived hex literal. In vex/ccall/mod.rs the symbolic CC_OP_COPY branch (handle_x86_eflags_all since the angr-5mnx3.60 helper split; inline in handle_ccall_with_ctx before it) had drifted to 0xD5 (C,P,A,Z,S) while the concrete Copy path used O|S|Z|P|C|A = 0x8D5, silently zeroing the Overflow bit (0x800) for symbolic-operand COPY cc_ops — a silent wrong-answer on OF branches. Fixed angr-36vvn.1 by masking with the constants. Rule: any flag-mask literal duplicated across the concrete+symbolic ccall paths is a drift hazard.

INVARIANT (ccall guest-width truncation): a sub-64-bit guest's ccall flag helper computes in u64, so it MUST mask both its dep inputs and the arithmetic result to the guest width before extracting a flag bit. The dispatch site's RustBV::concrete(result, ret_bits) does NOT rescue an unmasked helper — it truncates 0x1FFFFFFFF to 0xFFFFFFFF, i.e. turns garbage into different garbage instead of erroring. angr-03vl4.72: vex/ccall/arm32.rs::armg_calc_flag_n was the lone ARM32 per-flag helper without it, so ARMG_CC_OP_SUB with dep1=0,dep2=1 returned 0xFFFFFFFF for the N flag instead of 1, live on the standalone armg_calculate_flag_n CCall arm (taken whenever all four args are concrete). Its siblings armg_calc_flag_z/_c/v mask on entry and mask each wrapping* result; arm64 gets it for free via the shared arm64_res helper. When adding or reviewing a per-flag helper for a 32-bit guest, check BOTH masks — entry-only masking still lets a borrowing subtract sign-extend into the high half. Sibling rule: [invariant-ccall-flag-mask-named-constants].

X86/AMD64 HALF: all six raw-operand concrete flag builders in vex/ccall/x86_concrete.rs — calc_flags_add/sub/adc/sbb/umul/smul — mask their operands to get_mask(nbits) BEFORE use, matching the symbolic siblings in x86_symbolic.rs which extract_to_nbits unconditionally (add/sub angr-36vvn.3; umul/smul angr-0jh0j.69: umul's hi = (prod >> nbits) & mask picked up cross-term garbage from bits above the width, wrecking CF/OF, and sign_extend_to_i64's non-negative branch returned val verbatim so nbits=8 val=0x100 multiplied as 256 instead of 0). Gate: ccall_tests.rs::diff_fuzz_sym_flags_unmasked_inputs diffs concrete vs symbolic over Add/Sub/Adc/Sbb/Logic/Umul/Smul with UNMASKED random operands and pins that masking inputs changes nothing. When adding a new concrete flag builder that takes raw operands, mask first and extend that test's category list — every other diff_fuzz_sym_flags_* pre-masks and cannot see this bug class.

expressions_arith.rs eval_ccall fallback contract (UPDATED angr-9ke6b.88, commit 68d7ad34a — supersedes the pre-2026-08-01 'fabricate is sound' rule). handle_ccall_with_ctx==None now has TWO outcomes, not three: (1) calculate_condition/eflags/rflags → Err(NeedPythonFallback) BY DEFAULT; a fresh unconstrained symbolic is fabricated ONLY when ANGR_RUST_FABRICATE_UNSUPPORTED_IROP is set (same OnceLock gate as vex_op_fallback; bumps vex_bypass_fabricate_count). Rationale: the result of *_calculate_condition IS a branch guard, so an unconstrained stand-in explores both directions regardless of real flag semantics — strictly worse than the ordinary-IROp case angr-oyzvj already made opt-in. (2) any other CCall → Err(NeedPythonFallback), mapped by execution.rs to RunResult::NeedPythonVEX → _handle_python_vex_fallback. NEVER return concrete(0) on the fallthrough. Regression test: eval_ccall_unsupported_cond_routes_to_python_not_fabricate in interpreter/expressions_tests.rs (negation-verify by running it with ANGR_RUST_FABRICATE_UNSUPPORTED_IROP=1). GENERALIZED (angr-c7xno.44, 2026-08-09): this is now the crate-wide policy for EVERY site that would stand in an unconstrained symbolic for a value it cannot compute — there are three, all sharing the one OnceLock gate expressions_arith.rs::fabricate_unsupported_irop (pub(super) since c7xno.44) and the vex_bypass_fabricate_count counter: vex_op_fallback's any_sym arm, eval_ccall's condition-flag arm, and statements_dirty.rs::handle_dirty_call's !callbacks.has_dirty_call() arm. A NEW fabrication site must join them (gate + counter + a routes-to-python-not-fabricate test) rather than fabricating ungated. handle_dirty_call's test is statements_dirty_tests.rs::unmodelled_dirty_call_routes_to_python_not_fabricate.

The native CGC fdwait (syscalls/cgc.rs NativeFdwaitSyscall) unconditionally implemented the CGC_NON_BLOCKING_FDS behavior (concrete all-ready bits). The divergence was therefore INVERTED relative to how the parity census classified it: the option was honored when SET and silently wrong when UNSET (Python's fdwait proc fills the masks with unconstrained per-fd ready bits, so a binary branching on fd readiness explores both arms under Python, only the all-ready arm under Rust). Fix (angr-op0dn.14.8) was to gate the stub on state.has_option("CGC_NON_BLOCKING_FDS") and return SyscallError::Other otherwise, deferring to Python. Lesson: before promoting a 'silent divergence-risk' SimOption to _RAISE_OPTION_NAMES, check which POLARITY of the option Rust already implements — raising on the polarity Rust gets right is exactly backwards.

CGC fdwait total_ready counts fds unconditionally (angr-cslvl). procedures/cgc/fdwait.py accumulates total_ready across BOTH the read and write fd loops for every fd < nfds (0..32), and guards ONLY the mask stores with condition=readfds!=0 / writefds!=0. So *readyfds always gets min(nfds,32)*2 even when one or both mask pointers are NULL. syscalls/cgc.rs::NativeFdwaitSyscall originally added 'queried' per mask only when that pointer was non-null, under-reporting by half (or fully, with both null). Invariant for any future native fdwait/select-family work: the count is decoupled from the stores -- do not fold the count into the 'if ptr != 0' arm. The option half is separate: without CGC_NON_BLOCKING_FDS the native stub returns SyscallError and defers to Python (which mints unconstrained 1-bit ready flags per fd, so both readiness arms get explored); the native path implements exactly the option-is-set behavior. Tests: cgc_tests.rs::fdwait_counts_null_masks_like_python, fdwait_both_masks_null_still_counts, fdwait_clamps_to_32_fds (total=64, not 32).

RustSimState::merge (native/angr/src/state/fork.rs::merge) anti-alias combinators for the CGC allocator fields (angr-n0irt.2, sibling to angr-ph300.51's heap_brk/posix_brk/mmap_base max-fold). KEY: cgc_allocation_base grows DOWNWARD (allocate(2) uses checked_sub in syscalls/cgc.rs::NativeAllocateSyscall) so its merge combinator is MIN (furthest-advanced base), NOT the max used for the up-growing brk/mmap watermarks. cgc_sinkholes must INTERSECT (keep only regions freed in EVERY branch), NOT union: memory::merge (native/angr/src/memory/mod.rs::merge) unions live pages from all branches, so a region freed in one branch but live in another survives in merged memory — unioning its sinkhole would let a later allocate() reuse it and alias that live data. The n0irt.2 bead proposed union; that is UNSOUND, intersection is correct. General rule: any per-field merge combinator must respect that Rust's memory::merge page-unions all branches, so allocator watermarks must cover the furthest allocation in EITHER growth direction and freelists must intersect not union.

DECREE CGC syscall ABI dispatched through a separate 'CGC' registry key in NativeSyscallRegistry (native/angr/src/syscalls/mod.rs), NOT the per-arch tables. CGC numbers 1=_terminate, 2=transmit, 3=receive, 4=fdwait, 5=allocate, 6=deallocate, 7=random collide with Linux i386 syscalls, so the dispatcher in stepping.rs picks the table based on ExecutionEnvironment::os_name (set to 'cgc' from RustExplorationManager when project.simos.name == 'CGC'). ALL SEVEN syscalls now land natively in syscalls/cgc.rs: angr-krp1 (commit 0e3b480de) added _terminate/transmit/receive/fdwait/random; angr-rdgs (commit e16ca3bf3) added allocate/deallocate atop a new RustSimState::cgc_allocation_base (0xB800_0000 default) + cgc_sinkholes Vec<(addr,len)> mirror. Allocate still falls back to Python when the bump would straddle the CGC flag page (0x4347C000) since Rust syscalls lack project.loader access for the proper overlap split — minor edge case for first allocations in tiny address spaces.

SymContext::can_be_true(c) and can_be_false(c) are each literally check_branch_feasibility(c).0/.1 (native/angr/src/symbolic/solving_ops.rs, vex-engine-z3 arm), so calling BOTH on the same condition pays two full feasibility queries — two solver acquisitions, two Z3_BRANCH_* counter ticks, and the model-cache shortcut applied twice — where one call answers both directions under a single lock. Any site that needs the (can_be_true, can_be_false) pair must call check_branch_feasibility once, never the can_be_* pair. Fixed at the guarded-load/store handlers in angr-12jjk.22 (VEXInterpreter::classify_guard in interpreter/statements.rs is now the shared entry point for every guarded statement's tristate; GuardClass::from_feasibility folds the pair).

angr-9ke6b.230 (commit a0846d97f): the u128 chunk helpers now live in native/angr/src/symbolic/bv_chunk.rs (re-exported from symbolic::), NOT exploration/helpers.rs — they were sunk one layer so state/pymethods.rs (which must not import exploration/) can use them too. Four fns + MAX_CONCRETE_CHUNK=16: store_concrete_bytes_chunked, load_concrete_bytes_chunked, u128_to_le_bytes, u128_le_byte; all generic over the error type E so symbolic/ takes no pyo3 dep (pymethods sites use E=PyErr). INVARIANT: any concrete bulk memory read/write wider than 16 bytes MUST go through them — RustBV::Concrete is u128-backed, so as_u128()/u128_to_le_bytes only round-trip 16 bytes and a wider single op truncates, wraps mod 128 into a repeating pattern, or (read side) fails as 'symbolic' on a fully-concrete region. Call sites: state_api::{_get_state_memory, _set_state_memory_concrete, _set_state_memory_concrete_automap}, pending_api::{_get_pending_memory, _pending_memory_load}, state/pymethods.rs::{memory_load, memory_store}, and RustSimState::apply_changes (state/mod.rs) for both its register-write and memory-write loops. (The pending_api _pending_memory_store/_set_pending_memory pair was removed in angr-9ke6b.72 -- pending-state writes go through _set_state_memory_concrete, whose with_state_mut also finds pending states.) Callers do their with_state/with_pending lookup ONCE outside the helper and read inside that single borrow; do not resurrect the old per-chunk recursive self-call. Behavioral split to preserve: _get_pending_memory is deliberately eval-free (angr-04tw3.2), while _get_state_memory and _pending_memory_load concretize a symbolic load to a SAT witness. _get_state_memory keeps its Option contract with a closure-local sentinel PyErr so a missing state_id is still Err, not Ok(None). Tests live in symbolic/bv_chunk_tests.rs. GOTCHA (angr-0jh0j.1/.2, commit 11817904e): the ceiling is NOT memory-specific — it bit the REGISTER file too. arch/register_file.rs's RegisterFile::get/put composed a whole register into one u128, and x86/amd64 'fpreg' is 64 bytes; the name-keyed get_reg/put_reg reach it even though register_names() excludes it for exactly this width. When scanning for this bug class, the question is 'does any u128 shift index come from a caller-supplied byte count?', not 'is this the memory subsystem?'. The two fix shapes, both now canonical: a >16-byte READ has no Concrete representation at all — build it with concat (RegisterFile::compose_range), which declines to fold past 128 bits and stays exact as a Concat tree, and let as_u128()==None give the Python caller a clean error; a >16-byte WRITE of a wide Concrete extracts bytes via u128_le_byte, whose zeros above the payload ARE the value (a >128-bit Concrete is its low bits zero-extended), never a wrapped repeat. Second-order gotcha: tests that infer a register's size behaviorally by diffing get_registers_raw() after a set_register write (tests/engines/rust/test_arch_offset_parity.py::_rust_offset_size) can only observe 16 bytes once the wrap is fixed — cap the expectation at the probe's reach (_PROBE_MAX_BYTES), do not read the shrinking span as offset-table drift. HISTORY: originally fixed per-site rather than via one shared helper -- state_api::_get_state_memory (angr-ph300.x), pending_api::_pending_memory_load + _get_pending_memory (angr-ph300.19), and PyRustSimState::memory_load in state/pymethods.rs (angr-ph300.53, where pre-fix wide concrete loads errored as 'symbolic'). Those hand-copies were consolidated by angr-9ke6b.82 then relocated to symbolic::bv_chunk by angr-9ke6b.230 (this key). Still-live behavioral detail not repeated elsewhere in this key: _pending_memory_load used to swallow load errors as full-size zeros; it now propagates a PyValueError (callers in rust_state_sync.py catch Exception). When adding any new concrete bulk-load/store API, chunk to 16B and propagate errors, don't return zeros.

Rust↔Python FFI annotation preservation works in two layers (post angr-ykdq; code now under claripy_bridge/ submodules after the zel8z.5 split — import.rs + export.rs + cache.rs; was the single claripy_bridge.rs): (1) Symbolic leaves: SymbolicIdentityRegistry/CLARIPY_AST_CACHE (cache.rs) map symbol_id→claripy AST. Cache hit returns original AST (with annotations) verbatim. This was already in place pre-ykdq. (2) Expression nodes: thread-local LruCache<usize, (RustBV, Py)> EXPRESSION_BY_OPERANDS_PTR (cache.rs) keyed by Arc::as_ptr(&operands), populated in claripy_bridge/import.rs::claripy_to_rustbv after a non-BVV result, consulted at start of claripy_bridge/export.rs::rustbv_to_claripy_memo. The cached BV clone pins the operands Arc alive so the allocator cannot reuse the pointer while the entry is live — this is the safety mechanism, do not remove it. Cleared by clear_ast_cache. For both cases, if the cache misses (e.g. Rust constructed a new Expression internally without a Python source), the recursive rebuild fallback runs and annotations on intermediate nodes are dropped. That is the residual gap: only annotations on Rust-generated Expressions are unrecoverable, and those were never imported with annotations to begin with.

claripy BV.floordiv is UNSIGNED division and mod is UNSIGNED remainder (verified: BVV(0xFFFFFFFE,32)//3==0x55555554, %3==2). Only the explicit SDiv/SMod op-names are signed (claripy SMod==z3 bvsrem). In native/angr/src/claripy_bridge/import.rs::claripy_to_rustbv the floordiv dunder must map to udiv and mod to urem, NOT sdiv/srem. Was a bug (angr-p05r, fixed 2026-06-13): the dunders were aliased onto the signed arms, giving wrong models when the dividend sign bit was set.

clippy::restriction denies (unwrap_used/expect_used/indexing_slicing) added as module-level #![deny(...)] in a boundary file PROPAGATE into that file's #[cfg(test)] #[path=...] test submodule — so --all-targets clippy will flag every idiomatic .unwrap() in the tests. Fix: put #[allow(clippy::unwrap_used, clippy::expect_used, reason=...)] on the 'mod tests;' declaration line, not inside the test file. Verified in angr-qwyti.11 (solver.rs, exploration/resume.rs, state_lifecycle.rs).

Provenance of a cloned struct must be a flag stamped at its mint site, never inferred from a name/path string field. Closed angr-tqw60 (2026-09-08): FileSystem::fd0_is_dup2d asked 'is fd 0 still the pristine stdin placeholder?' by comparing FileDescriptor::name against "/dev/stdin", but FileSystem::open stores the caller's path verbatim and dup2 clones the whole descriptor, so a guest open("/dev/stdin")+dup2(fd,0) produced a clone the check read as pristine -- native stdin readers kept minting fresh unconstrained bytes over the guest's real content (silently wrong). Fix: FileDescriptor::is_std_placeholder, set ONLY by FileDescriptor::new_std_placeholder which only FileSystem::default's three std fds use; never by open/open_with_content/open_symbolic/register_fd_at/pipe. The same heuristic had been copy-pasted into Python (_inject_rust_fds in angr/exploration/rust_callback_dispatch.py); it now asks Rust via RustExplorationManager::state_fd0_is_dup2d, because the get_state_open_fds tuple carries no provenance signal and widening it would break every unpack site. Two lessons: (1) when a native check has a Python mirror, fix both in the same change or the bounce path re-introduces the bug; (2) for a new #[serde(default)] provenance field, pick the polarity whose legacy-snapshot default lands on the conservative side (here false => 'treat as dup2'd' => bounce to the reference Python impl, never a wrong answer).

RustBV unsigned comparisons (ult/ule/ugt/uge) and try_zext_const_cmp_fold direction: Ult uses (ZExtCmp::Ult, ZExtCmp::UltSwapped) forward+swap; Ule uses (Ule, UleSwapped); Ugt and Uge INVERT because Ugt(a,b)==Ult(b,a), so Ugt's forward is UltSwapped and its swap is plain Ult (Uge symmetric with Ule). Signed comparisons (slt/sle/sgt/sge) do NOT use try_zext_const_cmp_fold — the sign-bit handling is delicate and that shortcut is unsigned-only (callout in eq_into, value_ops.rs). The define_signed_cmp_pair! macro consequently has no zext-fold args. If you ever want to add a signed zext-fold variant, treat it as a new macro, not a hack on the existing one.

INVARIANT for future commutative-op work on RustBV (post angr-kkpr, commit 65b97cec9): the constructors add_into/mul_into/and_into/or_into/xor_into/eq_into/ne_into canonicalize operand order at the FALLBACK arm (after short-circuits) via RustBV::canonicalize_commutative. If you add a new commutative op or replace one of these constructors, preserve the canonicalize_commutative call OR re-derive equivalence. The canonical key uses Arc::as_ptr() for Expression sub-key — within-run determinism only, NOT cross-process. Any code that pattern-matches operands[0] of a commutative op expecting LHS-position semantics is broken — it should try both orders or use the per-position keys. Z3-level hash-cons handles cross-Arc structural-equality at to_z3_ast, so canonicalization's job is purely the commutative-permutation case.

RustBV::Concrete stores its value in a u128 (16 bytes / 128 bits max) regardless of declared width. Four hazard families follow. (1) ASSEMBLY: any code that ASSEMBLES a concrete value wider than 16 bytes by funneling bytes through a u128 is BUGGY: the shift wraps mod 128 in release (panics in debug), OR-ing high bytes back over low bytes. Fixed sites (commit df4bb4cd3, bd angr-tk7yv): memory/load.rs::load_concrete (two copies -- eager + lazy paths) now assemble size>16 loads as a Concat of per-byte concretes; symbolic/value_ops.rs::concat_into AND concat_no_ctx now guard the concrete-fold with 'if result_width <= 128' (else keep a Concat expression); exploration/state_api.rs::_get_state_memory reads in <=16-byte chunks. Also interpreter/bv_utils.rs::bytes_to_bv (angr-03vl4.31, commits 7608c8814 + 00b619214) -- the VEX-side twin of memory/load.rs::bytes_to_bv, reached from expressions.rs load fast paths, mod.rs read_memory and statements_dirty.rs::handle_dirty_call; it folds >16-byte inputs into a Concat via concat_no_ctx (high byte first: a.concat(b) puts a above b). Also interpreter/expressions.rs::eval_const's IRConst::V256 arm (angr-03vl4.29, commit 6ac725232) -- it packed v[0]|v[1]<<64 into ONE concrete tagged width 128, dropping v[2]/v[3]; now high.concat_no_ctx(&low) of the two 128-bit halves. Note the acceptance criteria said 'just retag the width as 256', which alone would have kept the truncation -- a wide width tag on a Concrete is a LIE, not a fix. Symptom seen: get_state_memory(24) on xmllint rodata returned chunk0|chunk2. Affects 32-byte AVX (ymm) concrete loads too. INVARIANT for future code: never pack >16 concrete bytes into a u128; build wide concretes via per-byte/per-chunk Concat, and do NOT 'fix' the overflow by clamping at 16 bytes -- that trades an abort for a silently truncated value. (2) BIT-SLICING: bits at position >= 128 of a wider-than-128 Concrete (e.g. a 192-bit Multi-cell value) are logically zero, and RustBV::as_u128() returns Some for ANY Concrete width. Any bit-slicing on a concrete fast path (e.g. extract_into in symbolic/value_ops.rs) MUST guard BOTH: shift-by-low (v >> low overflows when low >= 128 -> result is 0) AND mask (1u128 << result_width overflows at result_width >= 128 -> use u128::MAX). Fixed in angr-dondi; mirrors the same width>=128 mask guard already in RustBV::concrete() (value.rs). (3) VEC-OP WIDENING (angr-sqfj8.118): adding 256-bit lane shapes to a vex/opcode_map*.rs parse arm (vector shapes live in opcode_map_vector.rs) silently makes that op's evaluator concrete fast path reachable at total_width=256, where 'result |= lane << lo' shifts a u128 by up to 192. Before widening ANY vector op family to V256, check its evaluator carries the 'if total_width <= 128' guard that vec_int_lane_op (ops/vec_int_lane.rs) has -- vec_shift_n (ops/vec_shift.rs; the merged shift-by-immediate helper that replaced vec_shl_n/vec_shr_n/vec_sar_n in angr-5mnx3.68) did not until .118. Applied again in angr-sqfj8.112 (V256 CmpEQ/CmpGT): vec_int_lane_op's existing guard is why that widening needed no evaluator change. The float lane ops were the last V256 op-coverage gap and are now covered too (angr-fs8kb.15, ops/tests_vec_float_lane.rs::test_vec_float_binops_avx2_256_bit_f32x8 and ::test_vec_float_min_max_sqrt_avx2_256_bit_f64x4); vec_float_lane_op's 'if total_width <= 128' guard was already present and correct. (4) SERIALIZATION (angr-03vl4.4): the reverse direction, RustBV -> bytes, has the mirror overflow ('value >> (i*8)' for i up to 31). interpreter/bv_utils.rs::bv_to_bytes stops at 16 bytes and zero-fills above, which IS correct there because as_u128() only ever exposes the low 128 bits -- but it means bv_to_bytes CANNOT serialize a wide Concat (as_u128() is None -> it returns all zeros); the reject_symbolic_byte_store guard is what keeps that from silently zeroing memory. callbacks/dispatch.rs used to carry a byte-identical private copy of bv_to_bytes that inherited every bug; it now imports interpreter::bv_utils::bv_to_bytes (which is pub(crate) for exactly that reason). Test pattern for a >128-bit op: build operands with concat_into of two 128-bit concretes and assert one extracted lane at a time (ops/tests_vec_int_lane.rs::test_vec_cmp_avx2_256_bit_i32x8); for the byte conversions see interpreter/bv_utils_tests.rs::bytes_to_bv_of_256_bit_buffer_keeps_every_byte_via_concat. ADDENDUM: hazard (2)'s guards apply to EVERY concrete op that shifts/masks by a bit POSITION, not only extract_into — extract_no_ctx had the same window logic without the guards until angr-ph300.31 and aborted/mis-extracted on 256-bit ymm sub-register overlays (arch/register_file.rs callers). Any new concrete BV op that shifts by a bit position must copy extract_into's guards (shift=0 when low>=128, mask=u128::MAX when result_width>=128); operand-amount narrowing is the separate rule in invariant-concrete-shift-clamp-before-narrow.

Concrete shift/rotate arms in RustBV (value_ops.rs shl_into/lshr_into/ashr_into and define_rotate_pair! -> rotl_into/rotr_into) must reduce/clamp the shift amount BEFORE narrowing u128->u32. A pre-narrow "a as u32" truncates amounts>=2^32 to their low 32 bits (2^32 reads as 0), diverging from the Z3/symbolic arms which compare the full-width amount. Also: shl/lshr by width==128 wraps wrapping_shl(128) to a no-op (guard amt>=w -> 0); rotl/rotr with amt%w==0 must special-case (else v>>(w-amt) shifts a u128 by 128 = debug abort under panic=abort). ashr saturates to sign for amt>=w (clamp to w-1). Any new binop that narrows an amount to u32 must match its symbolic arm semantics for out-of-range amounts. WIDTH>128 RULE (angr-03vl4.59, commit 31df03cb7): a Concrete may declare width up to 256 while storing only the low 128 bits (see invariant-concrete-bv-u128-16-byte-limit), so every concrete fast path needs a width>128 story -- but "add the width.min(128) clamp the siblings have" is NOT always that story. Split by whether the true wide result is representable in the low 128 bits: lshr/ashr out-of-range results are all-zero, so they ARE representable and the clamp is right (a right shift can only shrink the represented magnitude); shl is the exception (angr-fs8kb.25) -- it GROWS the magnitude, so both halves of the old width.min(128) clamp were wrong at width>128: an amount in [128,width) is an in-range shift with a nonzero result, not a full shift-out, and even an in-range amount can push v's own high bits past bit 127. shl_into now cuts off at the true a>=width and otherwise folds only when the free fn exact_shl says the result fits the payload, declining to an Expression like rotate/reverse do; a non-trivial rotate moves set bits to positions >=128 that the u128 payload cannot hold, so there is NO correct concrete answer and the fold must be DECLINED (fall through to expr_node, keeping the op symbolic -- same choice concat_into/concat_no_ctx make for a wide concat). reverse_owned joined the declined-fold group in angr-03vl4.60 (commit ec6b2d264): a byte reverse moves byte 0 to bit position w-8 >= 128, likewise unstorable. Ask "is the wide answer storable?" before reaching for a clamp; clamping an unstorable result silently truncates (the same mistake the first angr-03vl4.31 commit made in bytes_to_bv). Wide coverage lives in value_ops_property_tests.rs WIDE_WIDTHS tests (wide_rotate_declines_the_concrete_fold, wide_reverse_declines_the_concrete_fold, wide_shl_declines_the_fold_when_bits_escape_the_payload).

A RustBV::Concrete stores its value in a u128 but may legitimately carry width>128 (bits>=128 are logically zero; zero_extend_into/truncate_into fast paths return concrete(v, to_width) for ANY to_width). So the concrete fast-path ops in value_ops.rs must stay correct for width>128, NOT just <=128. FOUR distinct hazards. (1) OVERFLOW/WRAP when shifting or masking a u128 by a width or bit-position (angr-qwyti.12): lshr_into cuts off at a>=width.min(128) (a right shift only SHRINKS the magnitude, so an out-of-range amount really does clear every readable bit); shl_into does NOT -- see hazard (3), it cuts off at the true a>=width and declines the fold whenever the shift would push a set bit to position >=128; ashr_into at width>128 collapses to lshr and guards amt>=128; sign_extend_to returns value early when from_width>=128 (avoids 1u128<<(from_width-1)). Same class as invariant-concrete-bv-u128-16-byte-limit / invariant-concrete-shift-clamp-before-narrow / sar_fill_mask (qwyti.17). (2) SIGN SEMANTICS (angr-03vl4.58): at width>128 the true sign bit (pos width-1>=128) is beyond the storage, so the value is logically NON-NEGATIVE and every SIGNED fast path must degenerate to its unsigned sibling -- signed compare to unsigned compare, bvsdiv/bvsrem to bvudiv/bvurem. Predicate sign_bit_beyond_storage(width) in value_ops.rs single-sources this; the fn sign_extend (u128->i128 helper feeding define_signed_cmp_pair!/sdiv/srem) must NOT be reached there and debug_asserts it, because past 128 bits the logical value can exceed i128::MAX and is not representable in i128 at all -- 'treat it as non-negative' is not expressible in the return type, the CALLER owes the unsigned branch. (3) UNREPRESENTABLE RESULT (angr-0jh0j.51/.52/.53, round 5; earlier angr-03vl4.59/.60 for rotate/reverse): the fold's true answer needs a bit in [128..width) that the payload cannot store, so folding emits a DIFFERENT number, not a truncated one -- e.g. (2^128-1)+1 at width 200 folded to 0, NOT of a wide zero folded to 2^128-1, sign-extending a 32-bit -1 to 200 bits folded to a NON-NEGATIVE 2^128-1. The only correct move is to DECLINE the fold and return an Expression node (Z3 then computes it exactly at the declared width). Predicate bits_beyond_storage(width) single-sources the ceiling test (sign_bit_beyond_storage delegates to it); concrete_arith_fits(width, checked_result) is the add/sub/mul form (and, via the free fn exact_shl, the shl form -- u128::checked_shl reports only an out-of-range AMOUNT, never a bit shifted off the top, so shl needs its own exact-result helper) -- below the ceiling a carry across bit 127 IS the mandated mod-2^width wrap, above it the carry is a real result bit. sign_extend_to returns Option so it can decline. (4) SATURATED CONSTANT (angr-nknv1): RustBV::all_ones_mask(width) and RustBV::ones(width) both SATURATE at width>=128 -- they yield 2^128-1, which above 128 bits is an ordinary number, not the width's all-ones value (unrepresentable in the payload). So (a) never test 'is this operand all-ones' with a bare v == Self::all_ones_mask(w) -- use the free fn is_all_ones(v, width), which ANDs in !bits_beyond_storage; the and_into x & all_ones -> x and or_into x | all_ones -> all_ones arms fired on 2^128-1 and, with a SYMBOLIC operand, respectively kept bits [128..w) the AND must clear and dropped bits the OR must keep. (b) never MATERIALISE Self::ones(w) on a path a wide width reaches -- udiv/sdiv's total x / 0 -> all-ones fold now declines via a b != 0 || !bits_beyond_storage(w) arm guard (Z3 bvudiv/bvsdiv are total the same way). Audit any new Self::ones caller (exploration/core_outcome_cc.rs::write_syscall_return is fine: register width <=64). Declining is ALWAYS safe (correctness over folding); the ops that legitimately still fold wide are and/or/xor of two CONCRETES (bitwise ops on two logically-high-zero payloads are exact), -0, mul-by-0, x%0, rotate-by-multiple-of-width, and any add/sub/mul whose checked_* is Some. Deterministic tests: WIDE_WIDTHS block in value_ops_property_tests.rs (wide_shl_/wide_lshr_/wide_ashr_/wide_sign_extend_/wide_signed_compare_degenerates_to_unsigned/wide_sdiv_srem_degenerate_to_unsigned/wide_rotate_declines_the_concrete_fold/wide_reverse_declines_the_concrete_fold/wide_arith_declines_the_fold_when_the_result_leaves_the_payload/wide_not_and_neg_decline_the_concrete_fold/wide_sign_extend_of_negative_source_declines_the_concrete_fold/wide_and_or_against_saturated_all_ones_decline_the_simplification/wide_div_by_zero_declines_the_concrete_fold).

concretize_and_pin (interpreter/expressions.rs) returns None ONLY when ctx.eval yields no model (UNSAT). It pins the choice with an equality constraint, which only tightens the constraint set. Consequence: re-running an arg-concretization loop over the same args after a first-pass failure is dead code — the failing arg fails identically, so the retry is equivalent to an immediate error (this was the angr-zi35f.15 dirty-call cleanup). Do not add a 'more aggressive' concretization retry expecting a different result without changing the actual strategy (e.g. Max vs eval).

Concurrency regression tests over scheduler helpers need an explicit std::sync::Barrier to have any signal. test_absorb_continues_cap_holds_under_concurrent_workers (exploration/scheduler_worker_tests.rs) first spawned W threads under std::thread::scope with no gate and PASSED against the known-buggy check-then-act absorb_continues -- thread spawn is slow enough that each worker finished its whole load-decide-add before the next started, so the race never occurred. Building the states BEFORE the barrier and releasing all workers together makes the pre-fix shape fail within the first couple of rounds (32 rounds x 4 workers x 8 forks, ~0.4s). Rule: a concurrency test must be shown to FAIL with the fix reverted (git checkout the production file, run, restore) -- otherwise it is a coin flip that only ever documents the fixed behavior.

A manager-level BROADCAST mutator (one that loops self.sm.stashes_mut(), or just STASH_ACTIVE, to push something onto every live state) must ALSO reach the TWO buckets of live RustSimStates that live in NO stash: (1) self.pending_callbacks — pending.state plus pending.pre_callback_snapshot (the fork_base deferred forks are materialized from), and (2) self.pending_parallel_bounces — the bounce queue a wave/session pass left undispatched. Since angr-0jh0j.82 there IS one helper that spans all three buckets: RustExplorationManager::all_live_states / all_live_states_mut (exploration/run_loop.rs), plus non_stash_live_states_mut for a broadcast that deliberately covers only some stashes (_active_states_map_memory maps into STASH_ACTIVE only). Reach for those, not a hand-rolled .chain().chain() — the three bucket lines differ only by method name, so a copy that drops one still compiles. A parked state is in no stash and nothing re-applies the change on resume, so it keeps the old value forever, as do its deferred forks. Bitten four times: set_deterministic (angr-sqfj8.32) and set_max_history (angr-c7xno.21) vs pending_callbacks, _active_states_map_memory (angr-03vl4.23) vs pending_callbacks, then all THREE of those vs pending_parallel_bounces (angr-03vl4.10) — so it is NOT only a config-knob rule: any broadcast over live states qualifies, including a memory mapping. Neither #[angr_macros::steady_guarded] nor its compile-time impl-block coverage check (#[angr_macros::steady_guard_checked], in native/angr-macros, which replaced a retired script gate) covers this: both only prove SOME call to steady_config_guard() happened, which drains the parallel session's resident frontier — they say nothing about the parked-state buckets, which remain a SEPARATE, unautomated obligation. The one carrier all_live_states does NOT reach is fork_snapshots (BranchSnapshot carries solver + registers + memory, nothing else), because it is not a RustSimState; a caller chains its own pending_callbacks loop for it. Which flavor needs it: a solver-flavored broadcast does (constraints::apply_fork_snapshots_deterministic — narrowed in angr-0jh0j.82 to exactly that carrier, since all_live_states now covers the two RustSimState halves it used to also touch), a memory-flavored one does (active_states_map_memory maps into snapshot.memory), a plain state-struct-field knob like max_history does not; pending_parallel_bounces entries are bare (RustSimState, BounceKind, u64) tuples, so they need no carrier walk at all. NOTE the broadcast/census asymmetry: all_live_states/parked_bounce_states yield EVERY parked entry, while RustExplorationManager::parked_bounces_flushable_count (angr-03vl4.15) deliberately excludes resident duplicates and unreplayable kinds — a census must equal the post-flush stash population, a broadcast must reach every state that can still execute. Regression pattern: manager_methods_tests.rs::set{deterministic,max_history}reaches_parked{pending_callback,parallel_bounce}states / pending_api_tests.rs::active_states_map_memory_reaches_parked{pending_callback,parallel_bounce}_states — assert over several values, or prove non-vacuity by mutating away each arm, so a one-way latch or the default cannot pass. Distinct from invariant-find-state-mut-covers-pending, which is about the single-state API already reaching pending. TEARDOWN DUAL (angr-6cp06.27): the same three-bucket rule applies in reverse to any "replace/discard the whole live-state world" operation, not just broadcasts — manager_methods_snapshot.rs::load_snapshot_bytes cleared both parked buckets, state_lifecycle.rs::_reset_for_stage did not, so a state parked mid-callback (or a wave's undispatched bounce) survived a multi-stage-explore stage transition and leaked stage-1 constraints/history into the next stage's frontier. Teardown differs from broadcast in one way: load_snapshot_bytes swaps in a fresh StashManager so the index goes with it, while _reset_for_stage keeps ours — a keeper must ALSO sm.unindex + sm.remove_root each discarded parked id or stash_of keeps answering for a dead id (angr-ph300.26 in a different bucket). Do NOT call policy.on_state_removed for a parked state: it already left STASH_ACTIVE through policy.select, which notifies. Skip the id being retained — a parked bounce may legitimately duplicate a stash-resident state. THIRD AXIS (angr-fs8kb.9): teardown must also sweep manager-level per-stage AGGREGATE bookkeeping that is keyed by nothing — not a stash, not a parked bucket, not even a StateId. constraints.rs::ConstraintTracker::uniqueness_set (a HashSet of register-tuple hashes, filled by helpers.rs::apply_uniqueness_filter) survived _reset_for_stage, so a legitimate stage-2 state whose hash collided with ANY stage-1 state went to not_unique (or was dropped outright under drop_terminal_states) and vanished from exploration. The three-bucket walk cannot catch this class — all_live_states enumerates states, and this field holds no states. Rule for a new manager field: ask whether its contents are scoped to one run/stage; if yes it belongs in _reset_for_stage (and load_snapshot_bytes) explicitly. The two sibling sets skip_find_predicate_states / skip_avoid_predicate_states are the counter-example that stays: they are keyed by the monotonic StateId, never reused, so a stale entry can only match a dead id. Regression: state_lifecycle_tests.rs::reset_for_stage_clears_uniqueness_seen_set, which asserts behaviourally (a stage-2 state reusing a stage-1 register tuple stays active) as well as by set size — both halves mutation-checked, since a size-only assert would pass on any code path that merely happened to leave the set empty.

steady_config_guard is NOT the whole config-invalidation story: it finalizes the live parallel_session, but leaves parallel_pool (the PersistentPool) untouched, and BOTH lazy creation sites (run_loop_wave.rs::run_loop_parallel_wave, run_loop_steady.rs::ensure_steady_session) are guarded on 'if self.parallel_pool.is_none()' with no resize path on PersistentPool. So any config a pool bakes in at creation time goes stale silently the moment a setter changes it — set_parallel_workers(N) was inert for the manager's whole life after the first parallel run (angr-5mnx3.14), which rust_manager.py::_engage_parallel_workers hits on every explore(). Rule for a future setter that feeds pool construction: after the #[steady_guarded] injection, call run_loop.rs::retire_parallel_pool_for_resize (or an analogue) to drop the mismatched pool so the is_none() path rebuilds it; release the GIL around the drop (Python::attach + py.detach, same reasoning as RustExplorationManager::drop) and refuse to drop while a session survived the guard, since joining live workers deadlocks. Keeping the pool is right when the new config means the pool is simply unused (workers<=1 routes to must_run_serial), so the downgrade/restore cycle does not pay a thread-spawn + Z3-context rebuild per explore.

sync_constraints_from_python (exploration/constraint_sync.rs) uses claripy_to_rustbv as primary (preserves assumed_constraints tracking for export_state_constraints) and claripy.backends.z3.convert(ast).as_ast().value -> add_constraint_raw as fallback when claripy_to_rustbv hits UnsupportedOp. claripy and Rust solver share Z3 context so the raw ptr is valid in place. add_constraint_raw does NOT push to assumed_constraints, so fallback-rescued constraints are invisible to export_state_constraints — this is fine for solver correctness (Python state already has them) but means re-export back to Python can lose info for FP/etc constraints.

When adding AST-emission counters (like bvop_extract_count/bvop_concat_count/bvop_reverse_count in angr-2j5v), bump at the actual RustBV::Expression { ... } construction site, NOT at the public entry of the *_into method. Reason: the public entry (e.g. extract_into) recurses through pattern-simplification rules that may collapse to a fully-folded result without ever emitting a node. Counting at entry inflates by simplification recursion depth (Extract(Extract) Rule 1 alone adds 1 per nesting). Counting at construction = exact Z3-visible node count, the number that actually matters for AST instrumentation. Verified by the test_bvop_counters_fire_on_symbolic_construction test which sees 1 extract emission per symbolic-input extract call.

Cross-engine bump-allocator/pointer drift fields (heap_brk, posix_brk, mmap_base) all sync the same 3-point way: (1) RustSimState getter+setter, (2) FFI get/set_state_ pair on RustExplorationManager + PyRustSimState property, (3) Python export-side sync_rust_to_state (Rust->Python, max(rust,py)) wired into BOTH materialize and _sync_cached_state paths, plus import-side push in _add_rust_state (Python->Rust). heap_brk mirrors state.heap.heap_location (SimHeapBrk, always plain int — no BV guard needed, unlike posix_brk). Regression class: native heap-allocating procs (malloc/calloc/realloc/strdup/fopen via heap_alloc) bump Rust heap_brk; without the export sync a Python fallback proc reads stale heap_location and overlaps Rust-allocated memory. Fixed angr-um39j (commit f9fb83f22).

Native ctype procs must mirror angr/procedures/libc/.py, NOT Rust's std char classifiers — the sets differ, AND must compare the argument at its FULL width, not its low byte. (1) Predicate sets: NativeIsSpace (native/angr/src/procedures/ctype.rs) used Rust's is_ascii_whitespace, which omits \v (0x0b), while Python's isspace and libc accept c==32 || 9<=c<=13 (angr-9ke6b.107). Rust's is_alphanumeric/is_whitespace family is Unicode/Rust-defined, not C-locale defined. When adding or auditing a ctype proc, read the Python SimProcedure's predicate and encode THAT via ranges_predicate/set_predicate; a std one-liner that looks equivalent is the trap. (2) Argument width (angr-6cp06.1): the arg arrives as an arch-word RustBV, and Python's default SimProcedure prototype is all-char, so its 'c' is arch-word too and 'And(c >= 48, c <= 57)' compares all 64 bits unsigned. Truncating to bits[7:0] made isdigit(304) true natively / false in Python, made case_shift return the truncated byte so tolower(EOF) yielded 255 instead of -1, and made the symbolic path outright UNSOUND (solver satisfies a byte-only predicate for c outside [0,255]). ranges_predicate/set_predicate/arg_in_range now compare at arg.width(), and case_shift returns the argument verbatim on the out-of-range arm. The concrete path derives its answer from the SAME ranges/members table (in_ranges/in_set) as the symbolic disjunction — there is deliberately no separate 'concrete_check' closure to drift. [UPDATE angr-2j9sk] The sibling divergence in strtod.rs/strtol.rs is FIXED and all whitespace classification shares procedures::ctype::is_c_space — see invariant-native-whitespace-single-source.

Python data-callback return protocol (Rust side): every callback that returns a value + symbolic flag uses the shape (bytes, is_symbolic, symbolic_ast?) where a 2-tuple AND a 3-tuple whose third element is Python None BOTH mean 'no AST'. As of angr-9ke6b.24 there is exactly ONE decoder: free fn extract_data_tuple in native/angr/src/callbacks/dispatch.rs, returning the BatchLoadEntry alias. call_memory_load, call_memory_load_batch's per-item loop, call_get_register and call_dirty_call all route through it (they used to open-code four near-identical copies). Any change to the optionality rule goes there, not at a call site; dispatch_tests.rs::extract_data_tuple_handles_all_three_tuple_shapes pins the 2-tuple / explicit-None / Some cases directly on the decoder.

Dead-code removal must sweep for same-named siblings in other structs, not just the one struct the bead names. angr-xvnz removed RustSimState.dirty_registers as a zero-consumer bitset but left VEXInterpreter.dirty_registers (interpreter/mod.rs) — an identical write-only bitset fed by mark_register_dirty from statements.rs's Put/PutI arms — alive for months until angr-0jh0j.27 found it again. Before closing a dead-field/dead-fn removal, grep the whole crate for the bare symbol name (not the qualified path) and remove every copy in the same commit; the second copy is usually in the layer above or below, sharing the concept but not the type. Same discipline as refactor-memory-sweep-rule, applied to code instead of memories.

LocalConstraints.dedup_set is a HashSet of Z3_ast ptrs that tracks every assertion currently asserted on the solver (shared + local z3_assertions). Invariant: 'ptr-in-set => already asserted on the current solver state, AND tracked in either z3_assertions_shared or local.z3_assertions.' Maintained by: lazy-seed on first add_constraint_raw call (one walk of shared+local, in SymContext::seed_and_check_z3_dedup), LocalConstraints::push_assertion on subsequent inserts, dedup_set.clear() + seeded=false on transaction_rollback. When adding new code paths that push to z3_assertions, use LocalConstraints::push_assertion (for a known-new Bool) or SymContext::seed_and_check_z3_dedup / contains_or_insert_ptr (which push on a miss) -- direct .push()/.extend() on the Vec leaves the set stale and breaks the invariant. There is deliberately NO bulk push helper: the one that existed, LocalConstraints::extend_assertions, recorded ptrs but never CONSULTED the set, which is exactly how add_constraints_raw_batch shipped for months re-pushing/re-asserting/double-counting already-asserted constraints and minting spurious ScopeFrames under shared lineage (angr-5mnx3.43, fixed 2026-08-28; the batch now filters through seed_and_check_z3_dedup and extend_assertions is deleted). Safety claim relies on Z3 hash-consing: live AST ptrs are unique among structurally distinct nodes (z3-rs holds refs via Bool::clone preventing GC reuse). PERF COROLLARY (angr-mwbp): the lazy-seed cost (O(N) walk over shared+local z3_assertions on first call) is paid PER-CONTEXT. Branch-heavy benches fork many contexts; if each fork pays the seed cost on its first dedup-checking call, the total work is quadratic in exploration depth -- flareon2015_2 went from 5s to 30s timeout when unconditional seeding was added from assume_*/false. Mitigation: piggy-back dedup checks on whatever seeded the table (typically add_constraint_raw); do NOT trigger seeding from hot paths in fresh contexts. add_constraints_raw_batch DOES seed (measured no regression: flareon2015_2 3.25s vs 3.81s baseline) because it is the same Python-originated SimSolver.add class of traffic as add_constraint_raw, not a per-branch hot path; add_bv_constraint remains un-deduped.

The 'fuzzer' cargo feature (native/angr/Cargo.toml: icicle-fuzzing/icicle-vm/libafl/libafl_bolts/pcode, git deps on icicle-emu) builds and its unit tests pass: 'make test-fuzzer' == 'cargo test --release --features fuzzer --lib fuzzer'. Since angr-fs8kb.85 moved icicle under fuzzer/, that filter covers fuzzer::corpus::tests, fuzzer::executor::tests AND fuzzer::icicle::tests (33 tests, was 9). Cold build ~2m22s. Executed nightly by .github/workflows/nightly-ci.yml::fuzzer_feature_tests (sibling of libvex_ffi_tests). Pattern for any default-off cargo feature: clippy --all-features only COMPILES its tests, it never RUNS them — a default-off feature needs its own cargo-test lane.

The default angr 'symbolic' mode bundle (used by factory.entry_state() with no add_options/remove_options) ships TRACK_CONSTRAINT_ACTIONS and TRACK_MEMORY_MAPPING. These are technically (b)-classified divergence-risk for the Rust engine but cannot be raised-on or warn-on without spamming every default-options test/script. Any future 'reject silent-ignore SimOptions' work must exclude options that ship in default symbolic mode unless the user explicitly opted in.

Every deferred-fork materialization in exploration/resume.rs MUST include BOTH condition-fallback arms: (a) reconstruct the condition from fork.condition_ast when it is absent from stored_conditions, and (b) the conservative arm — fork_base.fork() to unexplored_target, unconstrained — when neither source supplies one. Missing either silently drops forks whose condition is absent from stored_conditions -> unexplored branch never routed, find target behind it unreachable. STRUCTURE (angr-qwyti.4): the two TERMINAL-sink consumers _deadend_pending_callback and _resume_after_error share ONE helper materialize_terminal_deferred_forks(&mut self, pending: PendingCallback) -> RustSimState (guard_sink=Some(&state) since main state moves to a terminal stash; UNSAT forks lineage-registered only, SAT routed; returns main state for caller to push to DEADENDED vs ERRORED). _resume_after_error was an accidental omission for a long time (angr-4xaga.5) — pushed pending.state to STASH_ERRORED without reading deferred_forks. _resume_after_simprocedure/_resume_after_symbolic_branch keep their OWN blocks (guard_sink=None: continuing state already carries taken-path guard via apply_deferred_fork_constraints / branch-state routing differ). The two NON-materializing consumers _resume_find_predicate/_resume_avoid_predicate carry an always-on assert!(pending.deferred_forks.is_empty()) canary — safe because built via PendingCallback::lightweight (hardcoded empty); real assert! (CI runs cargo test --release, debug_assert compiled out); pinned by #[should_panic] tests {find,avoid}_predicate_pending_with_deferred_fork_trips_canary. Arm (a) is helpers::reconstruct_deferred_fork_condition (angr-ph300.76, single source of truth; call materialize_deferred_forks, do not re-inline). NOTE: parallel core_outcome_handlers.rs paths (process_deferred_forks_into/_core) intentionally have NO condition_ast reconstruction — off-GIL worker threads cannot Python::attach; only stored_conditions.get + the conservative arm there.

Deferred forks materialized during resume MUST be based on a guard-free fork base (pending.pre_callback_snapshot), never on the post-constraint state. In _resume_after_symbolic_branch (resume.rs) the base used to be true_state, which carries BOTH the fork's own taken constraint (added by apply_deferred_fork_constraints) AND the branch guard (assume_true) — a snapshot-less deferred fork's unexplored side then goes UNSAT and a reachable path is pruned. pre_callback_snapshot is captured before apply_deferred_fork_constraints runs, so it is the only clean base. build_unexplored_fork only escapes a polluted base when a per-condition BranchSnapshot exists in fork_snapshots; without one it forks the base directly, so base cleanliness is load-bearing. Same pattern already in _resume_after_simprocedure (fork_base = pre_callback_snapshot.unwrap_or_else(|| state.fork())). Ties into the .76 DRY refactor to share fork-materialization.

Deferred fork primary path is always snapshot-based: fork_from_snapshot REPLACES the solver/registers/memory entirely with the snapshot's state, so the parent state used for the call (e.g., successors[0] vs a separately-cloned fork_base) only matters for inherited fields like history/call_stack — these are equivalent across both call sites at the time of cloning since no mutations happen between the two captures. Every deferred fork creates a corresponding snapshot in interpreter/statements.rs (deferred-fork store path), so the no-snapshot fallback is unreachable in practice. Files: native/angr/src/exploration/stepping.rs, native/angr/src/state/fork.rs (fork_from_snapshot).

invariant-demoted-files-stay-python-owned: a write-demoted file (FileSystem::demote_symbolic_content, angr-0xyq2 Phase 2) is Python-owned FOREVER — the native write bounced, so Python's SimFile holds bytes the Rust FileSystem never saw. Any native I/O path that would serve such an fd from native state must bounce instead. NativeRead's contentless-fd mint (read_file_symbolic, angr-gorvf.15) violated this and silently invented bytes over the Python write; fixed in angr-8kk32 by gating on FileSystem::is_demoted_fd (fd name -> normalize_path -> demoted_paths lookup). Rule for future native-proc widening: before making a proc serve an fd it used to bounce on, check is_demoted_fd.

DFA (native/angr/src/automaton/dfa.rs) keeps a redundant reverse_transitions index alongside transitions; every mutation of one MUST maintain the other or find_predecessors (and minimize()'s Hopcroft refinement) sees edges that no longer exist and produces a non-language-preserving DFA. add_transition was fixed (angr-9ke6b.179, commit b3d5e21aa) to drop the source from the old destination's reverse set on overwrite. Generalized rule: any future DFA mutator (remove_transition, state renumbering, alphabet pruning) must update BOTH maps in the same fn; the class of bug is silent and only shows up as a wrong minimized automaton, never as a panic. Regression anchor: test_overwriting_transition_retires_stale_reverse_edge in automaton/dfa_tests.rs.

DFA (native/angr/src/automaton/dfa.rs) now matches EpsilonNFA: every entry point taking a raw StateId (add_transition, set_start_state, add_final_state) calls the private DFA::ensure_state to auto-grow num_states. Invariant: no transition/final/start id may exceed num_states(), because PyDFA::to_networkx (python_bindings.rs) enumerates nodes as 0..num_states and would emit edges to nodes it never added. add_state() still hands out the next unused id after auto-growth. NOTE: DFA has no to_graph method -- the graph export is PyDFA::to_networkx; angr-9ke6b.192's description cited a nonexistent DFA::to_graph.

DirectedCfgDistance::select (exploration/selection_policy.rs) picks its beam with select_nth_unstable_by_key, NOT a sort — safe only because the subsequent min_by_key key ends in the front index i, making it a total order whose winner is independent of the beam's internal order. Any future policy tiebreak that is NOT a total order (e.g. dropping the trailing i) would make the unstable partition order-visible and break the module's order-determinism contract. Guard the call with 'if beam_len < len' — select_nth_unstable_by_key panics on an out-of-range index, and beam_width can exceed the frontier size. Regression oracle: test_directed_wide_frontier_matches_full_sort keeps the pre-change full-sort implementation in the tests and asserts identical dispatch order over a wide tied frontier.

ype54 FIXED (iter48, commit 'fix(rust): carry dirty_pages through the memory snapshot'). REAL ROOT CAUSE (supersedes the iter47 'Python SimProc adds ' framing in ype54-root-cause — that false guard was a SYMPTOM): SymbolicMemory::to_snapshot/from_snapshot (native/angr/src/memory/mod.rs, struct SymbolicMemorySnapshot) treated dirty_pages as a rebuildable per-state runtime cache and restored it EMPTY. It is NOT rebuildable: the cached Python SimState used for SimProcedure callbacks is refreshed by REPLAYING Rust's dirty pages (rust_state_sync::replay_rust_dirty_pages -> mgr.get_pending_dirty_pages). Dropping the set on a migration round-trip stranded every Rust write made between the last callback and the migration, so the callback SimState kept stale ZERO bytes; a SimProc reading them (fauxware: 'open' loading its filename buffer at 0x7ffffffeff20 -> 0x0 instead of the stdin* symbols) computed a concretely-false guard -> solver UNSAT -> lost continuation. Fix: serialize dirty_pages (Vec, #[serde(default)]) and restore it. fauxware RUST_PARALLEL_WORKERS=2 found_count 1 -> 2, matching W=1.

METHOD THAT WORKED (reuse for angr-5rjbq-class 'Rust zeros where symbols should be' bugs): instrument the PYTHON callback boundary first, not Rust. Print, at the SimProc dispatch site in rust_callback_dispatch.py::_handle_simprocedure_callback, the proc name + its argument regs + state.memory.load(ptr) and diff W=1 vs W=2. That immediately localized 'the exported callback state's memory is stale', which ruled out the Rust snapshot (symbolic_objects WERE present in the snapshot) and the proxy (get_state_memory_ast was never called — callbacks read the CACHED Python SimState's own memory, not the proxy). Dead ends ruled out this iter: pending_writes/multi_objects snapshot drop (both empty at snapshot time); the _state_cache ancestry lookup (sid=1 hit the cache in both W=1 and W=2).

INVARIANT: any per-state field the Python side consumes as a DELTA (dirty_pages today) must survive migration serde. 'Runtime cache, rebuilds lazily' is only true for pure-read caches (wider_load_cache, multi_versions).

Rust init disk cache key MUST include the loader-object identity, not just the main binary: the pickled payload embeds pages (_extract_loader_pages) and post-relocation section patches (_extract_section_patches) for EVERY loader.all_objects entry, and _try_fast_memory_sync applies them unconditionally with no revalidation. RustDiskCacheManager._loader_identity_digest (rust_disk_cache.py) supplies that axis: per-object binary path + on-disk size/mtime_ns + mapped_base, sorted (loader order jitter must not change the digest), class-name fallback when os.stat fails (cle##externs/kernel have no backing file). It is mixed into _disk_cache_key's hash header AND the _disk_key_cache memo tuple -- all three of (version constant, hash header, memo tuple) move together (invariant I1 in rust_manager.py). Deliberately stat metadata, not content hashing: shared libs are large and a real libc upgrade changes size/mtime or the path. Note auto_load_libs/force_load_libs need no explicit axis -- they change the object SET, which the digest already covers. Covered by tests/engines/rust/test_disk_cache_loader_key.py (angr-uv7z5).

test_default_engine_env_parity.py's 4 assertions are coupled to reason strings produced elsewhere: 'rust engine supports this project...' and the 'state options not honored by the rust engine: ' list both come from rust_engine_eligible() in angr/exploration/rust_manager.py, while 'explicit use_rust_engine=False' is f-string-built in AngrObjectFactory.simulation_manager (angr/factory.py). If you reword any of those reasons, this test module and its nightly default_engine_parity job break — grep dispatch_reason before editing them.

Rust engine div-by-zero semantics are TOTAL and the concrete folds must match the symbolic (Z3) arms exactly — verified + regression-covered by angr-g2je6 (commit 12f946f5c). The contract: udiv(x,0)=all-ones, urem(x,0)=srem(x,0)=x, and sdiv(x,0) = -1 for x>=0 but +1 for x<0 (SMT-LIB bvsdiv is asymmetric — this is the trap; the old fold returned all-ones unconditionally). VEXOps::divmod_double_to_single (vex/ops/int_arith.rs) packs the LOW divisor_w bits of those same full-width totals on a zero divisor (quotient low half, remainder high half = the dividend), NOT zero. Concrete folds live in RustBV::{sdiv,udiv,srem,urem}_into (symbolic/value_ops.rs). Two secondary invariants: (1) any concrete signed div/rem fold must use wrapping_div/wrapping_rem — plain / and %% panic on i128::MIN / -1 even in release, and panic=abort SIGABRTs the process (same guard divmod_double_to_single already carried, angr-n0xru); (2) the test pattern that proves alignment is: build the value concretely, then build the SAME expression with a symbolic operand pinned via ctx.add_constraint(pinned.to_z3_ast().eq(z3::ast::BV::from_u64(1,1))) and compare ctx.eval — see test_sdiv_by_zero_concrete_matches_z3 (value_concrete_arm_tests.rs) and divmod_zero_divisor_matches_symbolic (ops/tests_int_arith.rs). Note angr's Python engine instead RAISES ClaripyZeroDivisionError on concrete SDiv-by-zero; PRODUCE_ZERODIV_SUCCESSORS is promoted-to-raise so those states route to Python (angr-op0dn.14.9).

A code example that appears in BOTH a docs/.rst worked example and a Rust module doc (//!) is one logical example with N copies, and a signature change reaches only the copy the author happened to be looking at. Concrete recurrence: angr-c7xno.64 fixed the stale 3-arg scan_for_null(state, addr, MAX_STRLEN) in simprocedures.rst -- and missed a SECOND copy 150 lines lower in the same file plus a third in procedures/macros.rs's module doc; both survived until angr-0jh0j.41/.39 two rounds later. RULE: when a shared helper's signature or dispatch changes, grep the helper/symbol name across docs/**/.rst AND native/angr/src/**/*.rs doc comments -- not just the one file you are editing, and not just once per file (grep -n, count the hits, fix all of them). The line-citation gate (tools/check_line_citations.py) does NOT catch this class: a wrong argument list carries no line number. Same reasoning as refactor-memory-sweep-rule, applied to doc copies instead of bd memories. GUARD-DRIFT COROLLARY: a fix that adds a guard to a function used as a worked example in docs/ must update that example in the same commit. Round-5 instances: simprocedures.rst 'Worked example 3: malloc' lost NativeMalloc's check_max(size, MAX_ALLOC_SIZE)? when angr-03vl4.53 added it (the section had been refreshed one commit earlier for an unrelated reason, so 'recently touched' is no evidence of currency), and rust_vex_ops.rst's BYPASS matrix kept a dead Iop_Perm8x32 after angr-sqfj8.117 remapped the family. Worse than ordinary doc rot because examples are COPIED — a missing guard propagates the hole into every new procedure written from it. No CI gate sees this class; applies to any declare_proc!/register_procs! sample, VEX opcode table or API snippet.

Doc line refs to native/angr/src/ and angr/exploration/ files drift fast; upstream angr Python files drift SLOWLY: confirmed across SIX consecutive audit sweeps now — angr-vfmm (iter 268, rust_manager.py SimOption matrix), angr-61ww (iter 269, rust_manager.py whole-file), angr-enhf (iter 270, engine.rs whole-file), angr-bi1a (iter 271, sweep-target multi-file), angr-ncd8 (iter 272, callbacks/errors/exploration/solver/state/stash/symbolic/fuzzer/icicle/memory/load + context/rust_manager stragglers), angr-4dkn (iter 273, UPSTREAM Python files: engines/successors, sim_options, cfg_emulated, identifier/{identify,runner}, state_plugins/posix, veritesting analyses + exploration_technique, jumptable, address_concretization_mixin, heavy.py + 2 rust_callback_dispatch.py stragglers). Iter 273 found 26 drifted refs across 3 .rst files, primarily +1 to +4 line shifts (modest upstream churn). EXCEPTION: rust_callback_dispatch.py (in angr/exploration/) had +70-line drift on regs._ip handling — file is actively edited. Stable utility modules across all 6 sweeps: claripy_bridge cache decls, syscalls/cgc, symbolic/registry, exploration/state_api, z3_ast_ptr, rust_state_sync utility fns. REVISED LESSON: drift correlates VERY strongly with sustained edit activity. Upstream angr Python is a quasi-stable target (~1-4 line shift per audit cycle); native/angr/src exploration/state/callbacks files have 60-100% drift per sweep. Pattern (now applied in 6 sweeps): every file:LINE ref in docs ALSO names the enclosing function/struct so future audits can re-locate after both renumbering AND renaming. AUDIT FULLY COMPLETE for first cycle: native + upstream + lazy_memory + proxy_writes all swept at least once. Future drift will require fresh audit ~1 month cadence.

FileSystem::dup (native/angr/src/state/filesystem/ops.rs) allocates the LOWEST FREE fd via the private lowest_free_fd() helper, not monotonic next_fd (fixed angr-9ke6b.119, iter103). A close()d fd counts as free even though close() leaves an is_open=false tombstone in the fds map — dup overwrites it, which is POSIX-correct. dup also bumps next_fd past its allocation so a later open()/open_symbolic()/pipe() (all still monotonic by design) cannot hand out the same number. Deliberate divergence kept: Python procedures/posix/dup.py's gap scan keeps the LAST mismatching index instead of breaking at the first, so with 2+ gaps it can return a still-open fd and clobber it; we return the true lowest and the two agree on the single-gap case. If a future bead makes open() reuse slots too, that is a separate decision — the FileSystem contract today is 'dup reuses, open does not'.

angr dup2/dup3 parity: angr's Python dup3 (procedures/posix/dup.py) does NOT return -EINVAL for oldfd==newfd — it returns newfd like dup2 (real dup3(2) returns EINVAL, angr does not). The Rust NativeDup2/Dup3Syscall must match Python, NOT POSIX: adding EINVAL would break parity. Shared dup2_body() in syscalls/file_descriptor.rs mirrors Python's exact check order (oldfd-open EBADF -> oldfd==newfd success BEFORE newfd-range EBADF -> alias).

Both children of an EAGER-mode symbolic branch need a real satisfiable() check before routing (angr-3ag1l, re-asserted by angr-gorvf.14). The non-deferred IRStmt::Exit path in interpreter/statements.rs returns StmtResult::SymbolicBranch WITHOUT calling check_branch_feasibility — only the guard's symbolic-ness is established, neither direction is known feasible. Deferred mode is different: it DOES run check_branch_feasibility, so its forks are pre-vetted. Any code that touches handle_symbolic_branch_core must keep the per-child sat check and route UNSAT children to CoreOutcome::pruned; priming the sat cache with true instead lets an UNSAT state sail through every downstream gate into the found stash.

Eager-concretize pattern in interpreter: when as_u64() fails for a value that must be concrete (PutI/GetI index, exit target, dirty-call args), use ctx.eval(&val) -> Option, build RustBV::concrete(eval_result, val.width()), construct val.eq(&conc_bv, ctx), then ctx.assume_true(&constraint). This pins the value while preserving constraint history for forks/Python sync. Wrapped as VEXInterpreter::concretize_and_pin (expressions.rs). Used at: GetI/PutI register-array index — since angr-sqfj8.65 both share VEXInterpreter::regarray_offset (expressions.rs), called from eval_geti and the IRStmt::PutI arm in statements.rs (originally pinned separately by angr-eg6j); exit-target concretization (exits.rs); dirty-call args (statements_dirty.rs VEXInterpreter::dirty_arg_values). Omitting the eq-pin is a soundness bug (solver can later pick a different value) — angr-eg6j fixed the GetI/PutI gap that angr-30fk left. Standard pattern — apply when adding new fallbacks.

The native crate is edition 2024, so unsafe_op_in_unsafe_fn is warn-by-default and becomes an error under CI -D warnings: an unsafe fn body still needs explicit unsafe{} blocks for each deref/union-access. For an all-FFI marshalling module (libvex_lifter.rs) scope #![allow(unsafe_op_in_unsafe_fn)] at module top with rationale instead of wrapping every op. bindgen-generated FFI (libvex_ffi.rs include!) also needs #![allow(clippy::missing_safety_doc, clippy::ptr_offset_with_cast, clippy::useless_transmute, clippy::too_many_arguments)] — those lints fire in the generated file, not our code.

Every Rust accessor Python treats as 'the state's address' must go through exploration::helpers::effective_pc, not RustSimState::pc. Under the register-proxy write-through gate a forked successor's self.pc stays stale at 0 while the IP register holds the real branch target (angr-4rq7), and _snapshot_to_angr derives state.addr from the IP register. Before angr-ph300.23 only get_state_pc_by_id had the fallback; get_state_pc and get_state_predicate_info read raw pc, so Python's find/avoid predicate cache (rust_state_cache.py, rust_techniques.py) keyed such a state under (sid, 0) and evaluated its predicate at address 0, missing the genuine find until a later step refreshed pc. Rule: nonzero pc is always authoritative; only pc==0 falls back; a genuinely-zero IP still reports 0. Test fixture for the stale shape: set_register_by_offset(RIP=184) directly — set_ip() syncs self.pc and hides the bug.

ENABLE_NX (X-bit non-executable check) is gated on BOTH enforce_permissions (STRICT_PAGE_ACCESS) AND enforce_nx (ENABLE_NX) in SymbolicMemory::check_executable (native/angr/src/memory/mod.rs). This matches Python's heavy VEX engine (HeavyVEXMixin.process_successors in angr/engines/vex/heavy/heavy.py): the permissions lookup happens inside an o.STRICT_PAGE_ACCESS in options block, and the raise is guarded by o.ENABLE_NX in options. Setting only one option must NOT fire the X check. Both flags propagate through SymbolicMemory::fork. Python->Rust wiring at rust_manager.py::_add_rust_state and _apply_state_metadata (allow-list includes LAZY_SOLVES, STRICT_PAGE_ACCESS, ENABLE_NX). TEST-WRITING COROLLARY: tests that exercise check_executable's X-rejection path must call BOTH set_enforce_permissions(true) AND set_enforce_nx(true) -- the gate short-circuits to Ok if either flag is missing. 'Allows X page' / 'skips unmapped' style tests pass even without enforce_nx because they expect Ok anyway, but they are effectively no-op assertions in that form.

memory page-range helpers (native/angr/src/memory/mod.rs) must be reached via end_page_inclusive(addr,size) / end_page_exclusive(addr,size), never an inlined formula. The workspace [profile.release] leaves overflow-checks OFF, so both directions wrap silently in production: (1) UNDERFLOW, size==0 (angr-9ke6b.99): addr+size-1 wraps to u64::MAX and check_perms_range iterates ~4.5e15 pages — a hang. Rejected as MemoryError::ZeroSize. Reachable: _pending_memory_load (exploration/pending_api.rs) forwards a Python-supplied size unchecked; on the store side size = value.width()/8 is 0 for any sub-byte BV. A second, earlier underflow exists per load — the wider-symbolic extract's size*8-1 (u32) inside load_concrete — hence the explicit size==0 early-returns in load_concrete / load_concrete_lazy_inner in addition to the helper. (2) OVERFLOW, addr near u64::MAX (angr-03vl4.34/.35): addr+size-1 wraps to an end_page BELOW start_page, so start_page..=end_page and check_perms_range are both EMPTY — every mapped-page and permission check silently skipped — and the byte loops' wrapping Address addition then walks down through 0 and reads/writes a real low page. Rejected as MemoryError::OutOfBounds. Reachable, not theoretical: write_fallback_max is the default (concretize.rs, matching Python's SimConcretizationStrategyMax), so an under-constrained store pointer concretizes to exactly u64::MAX. Both helpers are fallible; end_page_exclusive is NOT exempt (its old doc claimed 'only ever adds, so cannot underflow' — true, but it overflows). Three rules future work must keep: (a) addr+size == 2^64 (a region ending exactly at the top of the address space, e.g. mapping the last page) is LEGAL, not an overflow — end_page_exclusive special-cases it to (u64::MAX>>12)+1, and any caller-level guard must therefore check addr.checked_add(size - 1), not checked_add(size), or it over-rejects the last page; (b) the infallible-signature callers map/unmap/add_lazy_region skip-and-warn on overflow via silent_default!(cat_c) rather than CLAMPING to the last page — clamping would turn map(0, u64::MAX) from a fast no-op into 2^52 page insertions, i.e. a Python-reachable OOM; (c) BECAUSE (b) makes map/unmap skip silently, every caller that REPORTS SUCCESS after calling them needs its own overflow guard — otherwise it returns success for a mapping that was never made. syscalls/mmap.rs::do_mmap hit exactly this (angr-03vl4.68): its if !is_fixed && range_collides(..) gate meant the MAP_FIXED branch never reached range_collides's checked_add guard, so a page-aligned addr near u64::MAX under the MAX_MAP_SIZE cap returned Ok(candidate) having mapped nothing. When adding a new memory-mapping caller, ask whether its success path can outlive a skipped map().

INVARIANT: byte order in the Rust engine is a PER-STATE property, not an arch property. RustSimState::is_little_endian (seeded from the little_endian override in with_solver_endian) is the only authoritative source. Arch::is_little_endian hardcodes true in every impl -- including ARM and MIPS, where endianness is a per-binary build flag -- so it is a wrong-answer trap on exactly the big-endian targets you would consult it for; its doc comment now says so. CallingConvention::endness was a second copy of the same hardcoded answer and was DELETED in angr-9ke6b.218 item 7 rather than kept, precisely because a dead accessor returning Little unconditionally would mislead its first real caller. If you need byte order for memory access, note that SymbolicMemory already carries its own endness; for VEX-level work use vex::ir::arch::ArchInfo::endness.

Enum-discriminant-indexed parallel arrays are a panic-grade cardinality-rot shape in this crate: an enum with #[repr(usize)] plus a hand-written NUM_* const, hand-written [AtomicU64; NUM_] initializers, and a hand-written [&str; NUM_] name table, where a dispatcher does TABLE[variant as usize]. Adding a variant compiles clean, keeps any 'tables agree with NUM_*' test green (it never cross-checks the enum's arity), and panics out of bounds on first use. Both known instances are now macro-generated: symbolic/query_class.rs::QueryClass (query_classes!, angr-6cp06.49) and symbolic/stats.rs::CheckSite (check_sites!, angr-6cp06.89). Fix pattern: one 'Variant => "stats_key"' list drives the enum, the NUM_ const (as [$($key),+].len() on a fresh array literal -- NAMES.len() would be a const cycle), every counter array ([const { AtomicU64::new(0) }; NUM_]), the name table, and a const _ block asserting discriminant == declaration index; drop explicit = 0..N discriminants since an implicit fieldless #[repr(usize)] enum numbers from 0 by definition. The two macros were deliberately NOT hoisted into one shared macro -- CheckSite's family splits across the vex-engine-z3 cfg, has two counter arrays not one, and uses different visibilities, so parameterizing over all three costs more than the list it would share. Distinct from AGENTS.md's 'never describe a set by its cardinality' comment rule -- that one rots prose, this one crashes. When you meet a new NUM_ const, check whether it is hand-synced against an enum.

Assert-hardening rule of thumb for a broken internal precondition (established in the automaton/epsilon_nfa.rs hardening, angr-9ke6b.191/.193), three tiers: (1) return a Result when the function is PyO3-reachable AND has few callers -- a Rust panic surfaces in Python as an opaque PanicException instead of a ValueError (EpsilonNFA::move_on_symbol now returns Result<StateSet, EpsilonSymbolError>, rippled through subset_construction to PyEpsilonNFA::minimize's PyValueError); (2) debug_assert! for a pure-internal worklist invariant whose violation would only mis-step (dfa.rs, angr-9ke6b.182); (3) unconditional panic! when skipping the bad input would produce a SILENTLY WRONG result in release builds -- EpsilonNFA::epsilon_closure panics on a stale-cache/out-of-range state id, because a dropped state means a wrong closure means a wrong DFA, and debug_assert! alone leaves release silently wrong. Both functions' rustdoc carries the per-site rationale. Complements debug-assert-triage-policy (which adds the fourth shape: when the enclosing fn already has an error channel, log and return that error in every profile).

RustErrorRecord.error_class taxonomy (_ERROR_CLASS_PREFIXES in angr/exploration/rust_manager.py) is keyed off the Display impl prefixes of CbExecutionError variants in native/angr/src/interpreter/mod.rs. If you add or rename a CbExecutionError variant, update _ERROR_CLASS_PREFIXES (and the test_error_record_classifies_message dict) to keep the taxonomy stable. Why: error bisecting between Python and Rust runs depends on a stable string vocabulary — 'CAS unsupported', 'solver timeout', and 'memory unmapped' otherwise look identical. Substring fallbacks (timeout/unmapped/rust_panic) catch wrapped messages that don't start with a known prefix. Per-VEX-statement granularity in last_statements is NOT available today; that field is block-level history (state.history.recent_bbl_addrs[-5:]) and would require interpreter changes to upgrade. (Symbol-anchored per refactor-memory-sweep-rule; raw rust_manager.py:269 drifted to ~569 by iter52.)

load_concrete vs load_concrete_lazy_inner: BOTH must gate Multi cells before any symbolic fast path. install_multi_for_candidates sets the page multi_bitmap, NEVER symbolic_bitmap -- so page.is_symbolic() is false for a Multi byte and every symbolic_objects/symbolic_spans fast path misses, dropping the load through to bytes_to_bv over the STALE CONCRETE PLACEHOLDER byte with no error (silently wrong). angr-9ke6b.96 fixed load_concrete, which had no Multi handling at all despite being the production path behind RustSimState::memory_load (the memory_load pymethod every SimProcedure uses) and _pending_memory_load; only the _lazy variant had it. The shared predicate is SymbolicMemory::range_has_multi (memory/load.rs) -- any NEW load path must call it before its fast paths, and the is_empty() guard inside keeps all-concrete loads free. Test pattern: build the regression test, then temporarily delete the dispatch and confirm it FAILS -- a Multi test that only exercises load_concrete_lazy or loads after flush_multi_cells is vacuous.

ExecutionConfig (native/angr/src/callbacks/config.rs) is the deferred-fork/prefetch loop config ONLY -- it is NOT where concretization or branch selection is configured. THREE of its #[pyo3(get,set)] knobs have now been found dead and deleted: (1)+(2) in 32b9901b1 (angr-9ke6b.16/.17) -- max_concretization_range (default 65536) had no reader anywhere; the real symbolic-address bounds are AddressConcretizer::{read_range_limit,write_range_limit} in concretize.rs (1024/128, SimOption-driven; the struct is AddressConcretizer, there is no ConcretizerConfig type) -- extend THAT struct, never re-add a knob here; and branch_policy + the whole BranchPolicy pyclass enum (TakeTrue/TakeFalse/TakeFallthrough/Alternate, registered via m.add_class in engine.rs) was read only by repr and its own unit tests -- the fork path always continues down the true branch and defers the other side (see use_deferred_forks). VEXInterpreter::branch_counter went with it. (3) in 4756de8d3 (angr-c7xno.5) -- enable_stride_detection was a separate field from AddressConcretizer::enable_stride_detection (hardcoded true in its Default, read by the stride paths); AddressConcretizer is built without ever seeing an ExecutionConfig (VEXInterpreter::with_config, RustSimState::with_solver_endian) and VEXInterpreter::set_config only assigns self.config, so the Python setter was a silent no-op. LESSON for the rest of that audit-bead class: a #[pyo3(get,set)] field with no Rust reader is worse than dead code -- it is a silent no-op in the PUBLIC API, so removal beats wiring unless a second mechanism does not already own the behavior. GENERALIZED CHECK when auditing any config struct: a field name that also exists on a different struct is the tell -- grep the name and confirm the reader reads THIS struct's copy, not the twin's. All three scope decisions are recorded in the ExecutionConfig doc comment so the knobs do not get re-added.

_exit_continuation_addrs cache (rust_callback_dispatch.py) MUST only be populated when proc.NO_RET=True. Address-only caching is unsafe because a state-dependent SimProcedure can produce all-Ijk_Exit successors for one state but normal returns for others, which would be incorrectly fast-deadended. Continuations inherit NO_RET via make_continuation's copy.copy(self.canonical), so __libc_start_main's after_main correctly remains cached.

Rust->claripy export mints Rust-native leaves with claripy.BVS(name, width, explicit_name=True) (claripy_bridge/export.rs, the RustBV::Symbolic arm of rustbv_to_claripy_memo). WHY it must stay that way: without explicit_name claripy renames to name_; export registers the AST against the rust_id so the round trip works, but if that registration is ever lost (registry GC, a fresh process, an evicted cache) the importer sees the RENAMED ast and mints a leaf whose Z3 constant is name — a new unconstrained variable no existing constraint binds (angr-izov2 failure mode, silent). Because RustBV::from_parts derives the Z3 term from the NAME (see invariant-symbol-identity-is-by-name), the explicit name makes a registry miss cost only object identity + annotations, never soundness. This is what unblocked SymbolicIdentityRegistry::retain() — angr-9ke6b.40 had found collecting against an approximate active set unsound. The name passed is the RUST name tag-and-all: a Bool leaf's !bool! prefix (angr-9ke6b.223) must survive or the re-mint builds BV::new_const instead of Bool::new_const(..).ite(1,0). The two unconstrained-placeholder mints in the same function (result for width>64 bitcount, fp_result) deliberately KEEP the auto-rename — they mean a fresh variable each time. Test: claripy_bridge_tests.rs::test_rust_minted_leaf_exports_under_its_rust_name. Bead angr-9ke6b.222, commit c43565e29.

State export must ALWAYS flush: RustSimState::export_full walks MemoryPage::symbolic_offsets, which reads only symbolic_bitmap and never multi_bitmap. Bytes parked in Multi cells (SymbolicMemory::multi_objects, installed by install_multi_for_candidates_safe for any symbolic-address store resolving Multiple/Strided) are invisible to it and export as their stale concrete backing byte. flush_and_export_full -> flush_pending_writes -> flush_multi_cells is the only correct entry point; since angr-9ke6b.101 _export_state/_export_stash/_export_found_states all use it and the pymethods take &mut self. Second half of the bug: flushing alone is NOT enough on the Python side -- the flushed Multi cell becomes a Rust-minted ITE symbolic_object that was never routed through addr_to_ast, so rust_state_export._recover_symbolic_ast misses it and the orphan-BVS fallback replaces the value with an unconstrained symbol (byte correctly marked symbolic, but holding garbage). _restore_symbolic_regions now second-chances through _recover_rust_memory_ast -> mgr.get_state_memory_ast, storing with endness='Iend_LE' because that FFI returns the raw LSB-first layout regardless of arch.

EXPRESSION_BY_OPERANDS_PTR is the SOLE Rust->claripy cache for compound RustBV::Expression nodes (defined in claripy_bridge/cache.rs after the zel8z.5 split; was claripy_bridge.rs). The old hash-keyed EXPRESSION_CACHE was removed (angr-fawo, commit 895bd285d): the export path claripy_bridge/export.rs::rustbv_to_claripy_memo holds only a RustBV and cannot recompute claripy's import-time ast_hash, so any hash-keyed export cache is structurally unreadable and just pins Python ASTs. Lesson: a Rust->Python AST cache is only useful if its key is derivable from the RustBV on the export side (operands Arc::as_ptr is; claripy ast_hash is not). The C4 cross-cache invariant in the claripy_bridge module rustdoc (mod.rs) now reflects single-key (was 'two-key redundancy by design').

Export-identity pattern: to make a Rust-minted claripy export STABLE across repeated rustbv_to_claripy calls (object identity), store it via store_expression_ast_by_operands(operands_ptr, bv.clone(), ast) keyed by Arc::as_ptr(operands). The top of rustbv_to_claripy_memo checks get_expression_ast_by_operands for ALL Expression variants, so the next export of the same RustBV (same operands Arc) returns the identical object. The bv.clone() pins the operands Arc alive to prevent pointer reuse — this is the safety mechanism, do not remove it. Used by clz/ctz/popcount/Float arms (angr-acoq); originally only imported-expression annotation preservation (angr-ykdq) used this cache.

Any width / bit-range / offset chosen by a caller OUTSIDE the engine must be bound-checked at the trust boundary itself, via the shared helpers in native/angr/src/symbolic/width_guards.rs (MAX_BV_WIDTH = 1<<20, check_bv_width, check_extract_bounds). Two boundaries call them: solver/handle_api.rs (the claripy-bypass handle API: create_symbolic/create_concrete/op_zero_extend/op_sign_extend width cap, op_extract range, op_truncate via reject_truncate_widening — the mirror of the older reject_extend_narrowing — and op_concat via reject_concat_overflow) and claripy_bridge/import.rs (the Extract arm via check_extract_bounds; the BVV and BVS arms via check_bv_width; the ZeroExt/SignExt arms via the file-local extended_width helper — angr-0jh0j.8; the Concat arm via that same helper applied to its accumulator at EVERY step of the operand loop, not once at the end — angr-5mnx3.9). Add new external-input constructors to that list rather than re-deriving the conditions.

WHY the downstream debug_assert!s are not enough — this is a SCOPE LIMIT on debug-assert-triage-policy class (1) ('width/arity checks in value_ops.rs kept debug-only because a width mismatch is already rejected at the Python boundary by symbolic/table.rs's binary-op macro'). That rationale only covers binary-op width MISMATCH between two operands. It does NOT cover a unary width ARGUMENT: value_ops::truncate_into's debug_assert!(to_width <= width), value_ops::zero_extend_into's debug_assert!(to_width >= self.width()) and drive_extract's debug_assert!(high < width) guard values that arrive from Python with no macro in the path, and all compile out of the shipped release profile (see invariant-assert-not-debug-assert-in-release). Consequence when unchecked (angr-c7xno.92/.93/.94): low>high wraps the result width high-low+1 to near-u32::MAX under release's no-overflow-checks arithmetic; to_width>source or to_width==0 builds an Extract past the end; both reach Z3_mk_extract as invalid-argument calls, i.e. a SIGABRT under panic='abort' that Python cannot catch. An absurd width instead defers to a multi-gigabit Z3 sort allocation (hang/OOM).

GOTCHA 1: an op whose result width is DERIVED, not passed, is the easy one to miss — no width argument means no obvious place to call check_bv_width, so op_concat sat unguarded while every named-width sibling was covered (angr-0jh0j.73), and import.rs's ZeroExt/SignExt computed val.width() + extend_bits with a bare + (angr-0jh0j.8). The scan question is 'can this op make the width grow?', not 'does this op take a width?'. And the scan has to be run per-BOUNDARY as well as per-op: fixing op_concat at the handle-API boundary (angr-0jh0j.73) and ZeroExt/SignExt at the claripy boundary (angr-0jh0j.8) still left import.rs's Concat arm unguarded through two more review rounds, because each fix swept its own file. When you guard a derived-width op, grep the OTHER boundary for the same op name before closing. Derive with checked_add and REFUSE on overflow (never saturate — see invariant-overflow-fix-refuse-not-saturate-identities), then check_bv_width the sum: h = op_concat(h, h) doubles per call, reaching the cap in ~21 calls and wrapping u32 in ~32, which leaves an Expression whose recorded width is small and wrong while its Z3 AST is enormous — corrupting even the later check_extract_bounds that validates against it. A wrapped ZeroExt is worse still: new_width comes out SMALLER than the source, so the 'extension' silently narrows.

GOTCHA 2: width 0 is a SUPPORTED degenerate concrete RustBV (tests/engines/rust/test_plugins.py::test_create_concrete_zero_width_round_trip round-trips it), so check_bv_width deliberately allows 0 — do not add a nonzero-width check to the creation path. It is only rejected for op_truncate of a wider source, where to_width-1 wraps. See invariant-rustbv-zero-width for the obligation that places on each op's concrete arm.

GOTCHA 3: guarding the arm is not enough if a FAST PATH bypasses it. claripy_bridge::import::try_extract_bvv is a cheap shortcut for the same 'BVV' arm, consumed by five solver.rs call sites — one of which (RustSolverContext::eval_batch) builds RustBV::concrete(value, width) from it. Guarding only the arm would have let the shortcut accept exactly what the general path refuses. Any such shortcut must apply the same check (there: check_bv_width(...).ok()? so an over-cap width falls back to the general, error-reporting path). When adding a guard, grep for the op's fast path as well as its arm.

factory.simulation_manager(use_rust_engine=True) kwargs contract (angr-op0dn.14.5.1): the Rust branch used to pop save_unconstrained and DROP every other kwarg. Fixed in angr/factory.py — it now forwards **kwargs to RustExplorationManager and raises NotImplementedError for names RustExplorationManager.init does not declare. The trap: RustExplorationManager.init itself takes **kwargs (forward-compat) and ignores unknowns, so simply forwarding is NOT enough — the loud check via unsupported_rust_manager_kwargs() (rust_manager.py, signature-introspection) is what prevents a silent drop. Single source of truth for the raise-listed SimOptions is now rust_unsupported_options()/state_requires_python_engine() in rust_manager.py, consumed by _check_raise_options and (next) the .14.5.2 dispatcher — never re-derive _RAISE_OPTION_NAMES. Test gotcha: attribute access on a manager falls through to stash lookup, so mgr.save_unconstrained returns [] not the flag; assert on mgr._save_unconstrained.

Any Python stand-in object handed to claripy_to_rustbv (a 'Fake' AST fixture in Rust unit tests, or any duck-typed AST) MUST define hash content-addressed — (op, length, child hashes) — never 'return id(self)'. claripy_bridge/cache.rs's AST_CACHE is a thread-local LRU keyed on ast.hash(); its doc states the precondition explicitly (content hashes survive collection, ids are recycled). A fixture hashing by id lets a Fake built after an earlier one was dropped inherit the freed node's cached RustBV, producing a WRONG value with no error — angr-5o2v7 saw claripy_bridge::import::import_tests::test_bool_fold_refuses_mismatched_operand_widths read the empty-And identity (1) back for empty-Or (0), intermittently, depending on pymalloc address reuse. It presented as a 'flaky test' for six clean runs before reproducing in the ralph gate. The shared fixture now lives in one const, FAKE_AST_CLASS in claripy_bridge/import_tests.rs; reuse it rather than re-inlining a class body. The same hazard applies to any future cache keyed on a Python hash.

Fast-path/saved-work counters must be gated on COLLAPSE-TO-ZERO, not on drift. A solver fast path (branch/assume-concrete, zext-cmp trivial decide, the model-hit families) fails silently: a refactor stops reaching the branch, every query falls through to Z3, and only wall-clock notices — and timing will NOT catch it on a bench where the path saves a few hundred checks. run_regression.py::FASTPATH_COUNTERS + the --check-counts block encode the rule: fail iff baseline_counters.json recorded the counter nonzero for that bench AND the current run reports exactly 0. Partial drops must NOT gate — which fast paths a bench hits shifts with path choice, so a drift threshold here is a false-alarm machine. Contrast TRACKED_METRICS, which gate the opposite direction (counter goes UP). Coverage is real but sparse: 13/34 benches carry a nonzero z3_saved_check_total; on the fast tier it is almost entirely z3_branch_model_hit (11 benches) + z3_extrema_model_hit (3) — branch/assume-concrete and zext-cmp trivial-decide are 0 corpus-wide.

FileSystem fd-vs-path matching must use FileDescriptor::norm_name (the cwd-normalized path frozen at open by open/open_with_content/register_fd_at/open_symbolic) via FileSystem::fd_norm_name -- never re-normalize the raw d.name against the CURRENT cwd. d.name stays raw because fd_info exposes it to Python verbatim, so a guest chdir between open and query silently re-keys any scan that normalizes it late. This is the same freeze-cwd-at-open rule known_paths and registry_key already follow; three scans had drifted from it (content_size_for_path, register_file_content's stamp scan, is_demoted_fd) before angr-9ke6b.120. Any NEW path-keyed fd scan must go through fd_norm_name.

Rust feature-flag matrix in nightly-ci.yml runs (1) cargo check (2) cargo test (3) cargo test --test feature_flag_smoke for each combo. The smoke test (native/angr/tests/feature_flag_smoke.rs) is feature-gated: '' = 2 tests, 'automaton' = 3, 'vex-engine' = 3, 'vex-engine,vex-engine-z3' = 4, default = 5. Adding new feature combos requires extending feature_flag_smoke.rs with appropriate gates so the public surface for that combo gets exercised end-to-end, not just compile-checked.

Feature-gated Rust modules (fuzzer/, fuzzer/icicle.rs, automaton/, libvex-ffi code) ARE linted at PR time: ci.yml rust_check runs 'cargo clippy --all-targets --all-features -- -D warnings' from the workspace root, and AGENTS.md / rust_build.rst / the ralph _footer prescribe the same command locally. Dropping --all-features locally hides a feature-gated red (angr-9ke6b.50 / angr-fggug: an unreachable_pub sweep skipped src/fuzzer/). Mirror-image blind spot (angr-aygsg): --all-features compiles every feature-only caller, so it can never see dead_code that exists only in the DEFAULT-feature build, and no CI lane gates default-feature warnings. Rule: when adding a helper to a non-feature-gated module whose every caller is feature-gated, gate the declaration and impl too (#[cfg(feature = "x")]), and run both 'cargo check --release' and clippy --all-features before committing.

File-size split convention for native/angr/src (established angr-a2br.2 context.rs split, angr-7hwz value.rs split; test-file ambiguity resolved by angr-5mnx3.49 commit 5a84a60a0): every file — PROD AND TEST ALIKE — stays under ~2000 lines. Test files are NOT exempt; angr-p3bi's close text mused the owner 'may rule test files exempt' but the repo's actual shape had already settled the other way (vex/ops/tests_vec_.rs, symbolic/value_ops_property_tests.rs, symbolic/value_z3_fp_tests.rs are all one-topic-per-file siblings). The split recipe, in order: (1) cut along the section banners already in the file — they are the author's own topic boundaries and land on test boundaries; (2) give each new file a //! module doc naming its scope and cross-referencing its siblings; (3) register each with test_submod!(z3 "file.rs" => modname) from the PROD file (keeping the same z3 gate — see no-default-features-test-gating), NOT from mod.rs; (4) a helper used by MORE THAN ONE resulting module moves to a shared _tests_support.rs as pub(super) — sibling test modules are all children of the same prod module, so super::tests_support::helper resolves; a helper used by exactly one stays private there. VERIFY the split lost nothing: grep -c the fn decls before and after (must match) and confirm cargo test --release reports the SAME pass count, not merely green. Then rename-sweep: moving a test between modules breaks doc citations of the form module::test_name — the value_tests split had 2 in-repo (value_ops_property_tests.rs) plus 7 bd memories to repair. PROD-side addendum (angr-5mnx3.1, arch/mod.rs -> register_file.rs + registry.rs): moving an impl block out of a mod.rs into a sibling breaks two things the type-checker only reports one at a time. (1) A method that was PRIVATE in the impl was visible to the mod_tests.rs sibling (both descendants of the same module); once the impl lives one level deeper it is not — widen exactly those to pub(super), not the whole impl. (2) An item that was DEFINED in mod.rs and is read only by tests (ArchDesc/ALL_ARCHES) becomes an unused_imports warning the moment it is re-exported instead, because the plain lib build has no consumer — CI clippy is --all-targets -D warnings, so it reds. Fix by making the sibling pub(crate) mod and having the tests path through it, keeping the re-export for the members lib code actually uses. (3) A type the moved code references ONLY in an intra-doc link ([SymContext] in a doc comment) must still be imported for rustdoc to resolve it, but rustc's unused_imports pass does NOT count doc-link uses — so the import warns and CI clippy -D warnings reds. Spell it #[expect(unused_imports, reason = "referenced only by the intra-doc links below")] rather than allow: if a later edit gives the import a real code use, unfulfilled_lint_expectations tells you to drop the attribute, whereas an allow would sit there forever. Seen in angr-fs8kb.35 (context.rs -> context_snapshot.rs / local_constraints.rs, both of which only name SymContext in prose). (4) angr-fs8kb.44 (sprintf.rs -> sprintf_spec.rs/sprintf_conv.rs, scanf.rs -> scanf_spec.rs): the _tests.rs sibling reaches the prod file's private items through use super::*, so ANY const/helper you move out of the prod file into a new sibling module breaks the test file even when the move is pure code motion and nothing changed visibility. rustc reports it as E0425 'cannot find value X in this scope' in the TEST file, pointing at the moved definition -- which reads like a visibility bug and is not; the fix is an explicit use crate::<path>::<new_mod>::{X, y}; in the test file, plus pub(super) on the moved item. Corollary: do NOT keep the moved item imported in the prod file just to re-expose it to super::* -- with no lib-side consumer that is an unused_imports warning and CI clippy -D warnings reds, same trap as (2) above. (5) angr-fs8kb.20 (opcode_map.rs -> opcode_map_float.rs/opcode_map_vector.rs): when the prod file defines macro_rules! that the moved code invokes, textual macro scope does NOT follow the code to a SIBLING module (it covers only the defining module and its children), so each macro needs a pub(super) use <name>; line immediately after its definition and the new module imports it by path. Second half of the same trap: macro bodies name types unqualified (IROp/IRType/FCmpKind here) and macro_rules paths resolve at the CALL site, so the correct import list for each new module is whatever ITS OWN invocations expand to -- not a copy of the parent's use line. Expect the parent to shed an import as a result (FCmpKind became unused in opcode_map.rs once the fcmp invocations left), which CI clippy -D warnings will red. Verification for a macro-heavy split: grep -c the macro invocations (_arms!) as well as the fn decls before and after. (6) angr-fs8kb.66 (expressions.rs -> expressions_loads.rs/expressions_arith.rs): a baseline-gated audit script (tools/audit_silent_fallback.py and its four siblings) keys each known site by RELATIVE PATH, so moving a baselined line into a new file makes the gate report it as a NEW untagged site -- with the old entry now orphaned and silently unenforced. Fix by editing the one path in the baseline .txt (keeping its sorted position), NOT by --update-baseline, which would re-accept every other drift in the same run. Same reasoning as the pinned-baseline rule in run_regression.py: a refresh command hides the diff a hand edit makes reviewable. (7) angr-fs8kb.96 (statements_tests.rs -> statements_dirty_tests.rs/statements_cas_tests.rs): rule (4)'s super::<base>_tests_support::helper resolves claim holds ONLY while every test module is registered from the SAME prod file. When the split is PER PROD SIBLING -- each test module registered from the file it covers, which is the shape rule (3) pushes you toward once the prod side is already split -- the consumers are children of DIFFERENT prod modules and no super:: path reaches across them. Register the support module one level up, from the package's mod.rs, and have each test module import it by full crate path (use crate::interpreter::statements_tests_support::{..};). pub(super) on the helpers is still the right visibility: super is now the package module, so it scopes them to exactly the subtree that may use them, without widening to pub(crate). This is the one sanctioned exception to rule (3)'s register-from-the-prod-file-not-mod.rs -- and it applies to the SUPPORT module only; the test modules themselves still register from their own prod sibling. (8) The same path-keying bites tools/check_line_citations.py: its baseline rows are \t, so a file split/move re-reds the gate with the baselined line citation reappearing as NEW under the new path. Preferred fix is to SYMBOL-ANCHOR the moved citation (per AGENTS.md's symbol-anchor convention) and DELETE the old baseline row -- shrinking the debt rather than relocating it; repath the row only when the target has no resolvable symbol; never --update-baseline (seen angr-c7xno.45, expressions.rs -> expressions_inspect.rs). (9) When splitting a prod module, split its sibling _tests.rs along the SAME boundaries. Section-banner markers are a starting point, not a trustworthy cut line: in helpers_tests.rs (angr-9ke6b.76) one '// --- Timeout / LengthLimiter / LoopBound ---' banner covered ~460 lines that also held the effective_pc tests and the materialize_deferred_forks block, and slicing on banners left dangling doc comments ('error: expected item after doc comment') plus cross-file fixture refs. Reliable method: list every top-level fn with line numbers and classify by the symbol it exercises, not the banner above it; walk BACKWARD from each fn over contiguous ///, // and #[..] lines to find the true block start; after cutting, grep each new file's head/tail for a trailing doc comment or orphaned fixture. A shared fixture with a single remaining consumer (e.g. push_active_at) moves with that consumer or is inlined; multi-consumer ones go to the support module per (4)/(7). Never hand-write the old '#[cfg(test)] #[path=..] #[allow(clippy::unwrap_used..)] mod x;' block -- every site goes through lib.rs's crate-root test_submod! (arms: test_submod!("f.rs" => name), test_submod!(name), optional 'z3 ' prefix for the cfg(all(test, feature="vex-engine-z3")) gate; invoke unqualified, #[path] resolves relative to the invoking file). DOC DUPLICATION (angr-5mnx3.69): extraction leaves two copies of a submodule's op-set description -- the doc comment on 'mod X;' in the parent and the file's own //! header -- and later op moves update only the header (vex/ops/mod.rs had three stale decl comments). When moving an op between submodules, fix the parent's 'mod ;' decl comment in the SAME commit; prefer keeping decl comments to placement/visibility rationale and letting the //! header own the inventory.

invariant: find/avoid routing is FIND-FIRST at every site (angr-03vl4.14). A pc in both find_addrs and avoid_addrs goes to FOUND, never AVOID — angr's Python Explorer documents that as the default (avoid_priority=False, angr/exploration_techniques/explorer.py::_filter_inner) and the Rust engine exposes no avoid_priority knob at all. set_find_addrs/set_avoid_addrs never reject an overlap, so it IS a reachable config. Five routing sites must agree or the same state routes differently depending on which side of a step boundary it is observed on (and, for the worker, on RUST_PARALLEL_WORKERS): run_loop_single.rs::step_one (pre-step, both find arms — needs_python predicate then addrs — before both avoid arms), helpers.rs::route_successor (fresh successors), step_one's SimProcedure-bounce arm (is_find = find_addrs.contains(addr), else AVOID), run_loop_wave.rs's bounce_target_addr match, and run_loop_worker.rs::parallel_process_state. Any NEW routing site must be find-first too. Regression pinned by run_loop_single_tests.rs::pre_step_and_post_step_routing_agree_on_an_overlapping_address, which drives one config through step_one AND route_successor and asserts the same stash.

RustExplorationManager::find_state / find_state_mut (exploration/helpers.rs) search all THREE live-state buckets, in this precedence order: pending_callbacks (hash lookup) -> the stashes -> pending_parallel_bounces (linear scan, added angr-eukuf). Consequences: (1) with_state/with_state_mut and every Python-facing method built on them reach pending-callback and parked-bounce states too, so pending-only mirror methods (_set_pending_memory, _pending_memory_store, _pending_state_map_memory, _pending_memory_map_data) were pure duplication of _set_state_memory_concrete and were removed in angr-9ke6b.72 — before adding a new pending* mutator, check whether the state equivalent already reaches it. (2) The parked-bounce leg MUST stay last: an id can be resident in a stash AND parked at once, and flush_parked_bounces_to_active drops the parked copy as the redundant duplicate in exactly that case, so the stash copy is the one carrying the path forward and must win the lookup too. (3) find_state_mut cannot use a &mut self bucket method for that leg — the receiver conflicts with the pending_callbacks borrow the early return holds for the whole fn. That is why the bucket bodies are pub(super) FREE functions over the field (run_loop::parked_states_mut etc., angr-0jh0j.82): find_state_mut calls run_loop::parked_states_mut(&mut self.pending_parallel_bounces) and keeps the disjoint-field borrow. Coverage for the whole bucket x method grid lives in exploration/manager_methods_coverage_tests.rs (add a column, not a bespoke test).

run_findall_gate.py (tests/benchmarks/) is the parallel scheduler's STRUCTURAL correctness gate and now runs nightly as nightly-ci.yml::findall_worker_invariance (wired iter141, commit 5387d5ce2; make gate-findall). Contract: an exhaustive find-all must produce an IDENTICAL found-set fingerprint (multiset of found pcs, exported via ANGR_BENCH_FOUND_FINGERPRINT=1) at every RUST_PARALLEL_WORKERS count. It is NOT a wall-clock gate — and must not become one: measured 2026-07-22 on the default synthetic corpus, workers>1 is SLOWER than serial on both benches (pbounce 46.9s serial vs 52.6s at w=2/w=4; trap 19.6s serial vs 33.7s/31.4s), with steal fraction 75-90% and gil% climbing 3.3%->66% on trap. Those numbers are the expected shape for this corpus, not a regression. Cost: 2 benches x workers{1,2,4} x 3 reps = 18 run_single children, ~12.5min (measured 4m11s at --reps 1). Empty found-set FAILS rather than passing vacuously.

FloatOpKind::RoundToInt was the first FloatOpKind variant where one operand (the rm BV) is NOT a float. The generic build_fp_z3_ast_cached loop blindly Z3_mk_fpa_to_fp_bv every operand — feeding it a 32-bit rm BV would mis-encode it as an F32. Solution: early-branch on RoundToInt to a separate helper (build_fp_round_to_int_cached) that only converts operand[1] to Float. Future float ops with metadata operands (rm, signedness flags, source-precision discriminators) should follow the same split-helper pattern instead of trying to generalize the operand loop. See commit d0377abb9.

FloatOpKind::result_bits(prec) added in commit 37983a77b — replaces the hardcoded 'compare ? 1 : prec.bits()' width logic in build_float_expr and rustbv_to_claripy. CRITICAL for ConvertFtoI/FtoIRm where the result width is dst_bits (often != prec.bits()): src may be F64 but dst is i32. If you add a new FloatOpKind whose result width differs from prec.bits(), update result_bits() — both the expression-builder and the claripy bridge use it.

flush_stores in interpreter/mod.rs drains pending_stores by move into all_flushed_stores (no Vec clone). pending_symbolic_stores is drained in the same loop as the rust_mem.import_symbolic_value call so we use the original BV for all_flushed and a single clone for rust_mem. INVARIANT: drain conflicts with simultaneous &mut self.rust_memory borrow on concrete path; we iter() under rust_mem borrow then drain after the borrow ends.

Fork-metadata GIL attach eliminated (angr-gorvf.4.2, 2026-07-14, commit 27f44e7f4). ROOT CAUSE: RustSimState's three Python-AST overlays (symbolic_pages / hook_symbolic_memory / addr_to_ast) held bare Py. Py::clone_ref REQUIRES a Python token, so RustSimState::fork -> clone_py_metadata had to Python::attach on every fork of a state with ANY non-empty overlay. It cost only ~4ms corpus-wide yet was the SOLE GIL holder on 4 otherwise-Python-free benches. FIX: type SharedPyAst = Arc<Py> (defined in state/mod.rs); clone_py_metadata is now a plain HashMap clone = atomic refcount bumps, no GIL. Dropping the last Arc is safe without the GIL — pyo3 defers the decref. REJECTED ALTERNATIVE: Arc<HashMap<..>> + Arc::make_mut (the pattern used by RustSimState::hooks/environment) does NOT work here — make_mut needs Clone on the map, and Py: Clone only exists behind pyo3's py-clone feature (and panics without the GIL). Per-VALUE Arc, not per-map Arc, is the shape that works for Py values. MEASURED: run_zeropy_gate.py PASS 2->6 on a libvex-ffi build (google2016_unbreakable_0, ais3_crackme, securityfest_fairlight, strcpy_find). GilClass::ForkMetadata was KEPT so gil_work_ns_fork_metadata keeps proving the zero. MECHANISM/CALLERS (absorbed in the R4 merge): the three overlays are forked via RustSimState::clone_py_metadata (native/angr/src/state/fork.rs), called from fork/fork_true/fork_false/fork_from_snapshot/merge. Semantics: Python identity is preserved across the fork (an 'is' comparison works), while each state owns its own HashMap so key insert/remove does not alias. There is no Python-callable setter for these maps on PyRustSimState - set_addr_to_ast etc. are only reachable via RustExplorationManager.set_state_addr_to_ast(state_id, ...). To test fork+metadata, either go through the dispatcher (run an exploration that forks) or write a Rust unit test.

RustSimState::fork() (now in state/fork.rs; state.rs split into state/ dir module, angr-zel8z.1) requires the Python interpreter to be initialized (PyO3 0.27 panics otherwise). This means cargo test --lib for any test that calls fork() will fail with 'The Python interpreter is not initialized'. Pre-existing failing tests: test_state_fork, test_state_fork_memory_cow, test_filesystem_fork_isolation, test_inspection_fork_isolation. Workaround: write fork tests in tests/engines/rust/ (Python) instead — Python's pytest harness initializes the interpreter. The fork() codepath itself works fine in production where Python is always live.

angr-62ar5 root cause: a deferred fork built from a pre-branch BranchSnapshot inherits NO branch guards at all. interpreter/statements.rs deliberately never calls assume_true/false permanently during a block ('the solver stays clean so snapshots capture unconstrained state'), so BranchSnapshot::solver = ctx.fork() has zero guards regardless of how well-guarded the fork base is. build_unexplored_fork re-assumed only the OPPOSITE side of its own branch, so a fork for branch i lost the taken-path guards of branches 0..i-1 in the same step -> found states under-constrained, Z3 free to return a model contradicting a decision on the state's own path. INVARIANT for any new fork-materialization site: pass the (condition, path_taken) pairs of the already-materialized forks via helpers::PriorGuards. Snapshot arm replays them unconditionally; base-derived arms replay unless base_carries (stepping.rs::process_deferred_forks_into and core_outcome_handlers.rs apply each guard to the continuing state as they iterate, so they set base_carries=true but STILL must feed the vec for their snapshot arm). Presented as parallel-only (angr-lkim0 content gate) but serial was equally broken and merely got lucky in Z3's model choice — never conclude 'serial is correct' from a passing witness check. Regression: helpers_tests.rs materialize_deferred_forks_replays_earlier_guards_onto_later_forks + snapshot_built_fork_replays_earlier_guards.

Native format-string procs must THREAD every field they parse, not just the one the happy path needs. procedures/format_common.rs::parse_width_digits/parse_length_modifier are shared by scanf_spec.rs::parse_scanf_format and the printf family; a spec struct that parses a width/precision and then omits it from the struct compiles cleanly and silently diverges from angr/procedures/stubs/format_parser.py. Two instances found in round 7: scanf's numeric arm (%d/%u/%x/%o) dropped field_width, minting a free full-width BVS where Python's FormatString.interpret range-constrains to [-(base**(d-1)-1), base**d - 1] whenever dlog2(base) < bits — fixed by scanf_spec.rs::digit_range_bound + ScanfSpec.digit_bound (angr-6cp06.9); and sprintf's '.' precision consuming a vararg unconditionally (angr-6cp06.8). RULE when adding/editing a specifier arm: read the matching branch of format_parser.py::FormatString.interpret (packets path) and .replace/.interpret (addr path) and account for EVERY component field it reads (length_spec, pad_chr, size, spec_type) — an unused parsed field is the bug signature. Prefer computing the derived bound at parse time as a pure fn (testable without z3, so the four --no-default-features combos keep coverage) over inlining it in do_scanf.

How to gate found-state CONTENT for the Rust engine when the vh834 AST fingerprint is vacuous (Rust found states export an empty Python-side constraint log, so state.constraints fingerprinting collapses all paths to one class — see avoid-content-fingerprint-on-found-states): do NOT compare raw solver models across runs (Z3 model choice is not stable across worker counts or migration). Instead REPLAY the binary's own arithmetic in Python on the concretized witness (state.posix.dumps(0)) and assert the program's own reachability predicate holds. That projection is model-independent, hence worker-, migration- and re-solve-invariant. Implemented as _pbounce_witness / TestParallelFoundContentSynthetic in tests/engines/rust/test_parallel_wave.py (angr-lkim0, commit 7a742e54e); it found a real workers>=2 defect (angr-62ar5) on its first run that every addr/count gate had been green on for months. Reusable for any synthetic bench whose accept condition is closed-form.

Writing FP tests for the Rust engine: three traps that silently make a test vacuous or flaky. (1) 1/3 is NOT a valid RNE-vs-RZ rounding witness — its binary expansion rounds DOWN, so round-nearest and round-toward-zero produce identical bits, and an rm-threading test built on it passes even when the rounding mode is dropped entirely (the angr-c7xno.85 bug shape). Use 0.1 (rounds up into a double) or sqrt(2); scaling a witness by a power of two does NOT change its rounding direction, so 2/3 is just as useless as 1/3. Assert BOTH 'RZ != RNE' and 'RZ == RNE - 1' so the witness proves itself. (2) NEVER assert the exact bit pattern of a NaN result coming out of the symbolic path: symbolic/value_z3.rs::float_to_ieee_bv uses Z3_mk_fpa_to_ieee_bv, which Z3 leaves UNSPECIFIED for NaN, so the model may hand back any bits (including a finite value) and the assertion is nondeterministic. Ask the FP theory instead — FloatOpKind::IsNaN over the operand — and note that round-tripping a NaN through the ieee-bv encoding and back into a Float is equally unspecified, so IsNaN over an ieee-bv-encoded intermediate does not rescue it. Infinities are safe: they have unique IEEE encodings. (3) When you constrain a SYMBOLIC operand and assert the solved value, a unique encoding of the RESULT does not pin the OPERAND — rounding collapses a whole interval of operands onto one result, so 'assert_eq!(eval_f64(&ctx, &x), 2.5)' for 'x + 1.5 == 4.0' asserts a Z3 model preference, not a semantic fact (angr-63g3w: RNE's solution set is {2.5, 2.5 + 1 ULP}, since the latter's exact sum is a tie that rounds down because 4.0's significand is even). Compute the true solution set by hand FIRST; then assert (a) the returned model satisfies the constraint under Rust's own concrete add, and (b) the solution set itself, one pinned candidate per is_sat() call — that second form is strictly stronger AND doubles as a rounding-mode check, because a wrong mode admits/rejects different neighbours. See native/angr/src/symbolic/value_z3_fp_tests.rs::test_fp_add_symbolic_solution_set_is_exactly_rne and its sibling test_fp_add_with_symbolic_operand_solves, whose comments carry all three rationales at the assertions.

INVARIANT for native stdio/read procs (native/angr/src/procedures/): the FileSystem::is_open gate has TWO polarities and picking the wrong one is silently wrong. A proc that SERVES content natively (read.rs, fread.rs) bounces to Python on the UNTRACKED fd — Python's SimFile model owns bytes Rust cannot see. A proc that MINTS fresh unconstrained BVs instead of parsing content (do_fscanf in scanf.rs; the same shape as NativeSscanf's whole-call deferral) must bounce on the TRACKED/open fd — over real content a free BVS makes impossible paths feasible and never advances FileDescriptor::position, so a later native read/fread re-reads bytes the mint conceptually consumed. Key on is_open, not fd_info().is_some(): a closed fd has no live cursor to corrupt. The tracked-fd bounce is coherent because rust_callback_dispatch::_inject_rust_fds hydrates the callback state's posix.fd from the Rust descriptor (name, content, position). Ask which polarity a new proc needs before copying a sibling's gate.

invariant-fs-write-choke-point: FileSystem::write/write_at (native/angr/src/state/filesystem/ops.rs) have TWO refusal predicates, order matters. write_closed(fd) -- fd present but !is_open -- is checked FIRST and returns false WITHOUT demoting: a write to a closed fd is EBADF, never reaches file content, so demoting would needlessly strip native serving from sibling fds on the same file. write_refused(fd) -- content_sym/registry_key present -- is checked second and DOES demote_symbolic_content. A missing fd is deliberately NOT refused by either: write/write_at auto-vivify a write-only FileDescriptor, which is how state.write_fd(2, ..) works on a state whose stderr was never opened. Any new write-path predicate must preserve those three cases. Symmetry rule: read/read_at/read_sym/read_sym_at all guard is_open, so any write primitive must too or the fd silently accumulates unreadable bytes (angr-9ke6b.118).

PATTERN: std HashMap/HashSet keyed by internal u64/u32 IDs (page numbers, register offsets, addresses, condition_ids, BV ids) on hot paths should use rustc_hash::FxHash{Map,Set}. SipHasher's DoS resistance is dead weight when keys are not attacker-controlled, and FxHasher is ~2-3x faster on integer keys. Cumulative wins so far: state_fork 283 ns -> 199.66 ns (-29.4% across angr-75y3 + angr-z84i + angr-07rg). memory store_8bytes -38%. For local short-lived sets in cold paths (e.g. merge functions like RegisterFile::merge:445), keep std HashSet. Already migrated: SymbolicMemory.{symbolic_objects,symbolic_spans,dirty_pages,imported_addrs}, RegisterFile.symbolic, HeapMetadata.allocated, VEXInterpreter.{all_flushed_stores,all_flushed_symbolic_stores,pending_symbolic_stores,stored_conditions,fork_snapshots,concretize_cache}, PendingStoreBuffer.byte_index, PendingCallback.{stored_conditions,fork_snapshots}. Remaining candidates: RustExplorationManager id maps (state->id maps in exploration/mod.rs:340-450, NativeProcStats.call_counts), state.rs Arc-wrapped fds/hooks/environment maps (Arc-share is cheap; hashing matters only on contains/insert/CoW).

gil_profile timing tests must not assert against fixed ns ceilings -- under full-suite parallelism (2228 tests) scheduler preemption inflates a guard's wall span far past a nominal busy_ns() budget, causing flaky failures (e.g. outermost_only_times_once banked 415309 ns vs a 350000 ceiling at iter 31). Test the RATIO instead: measure the region's wall span with an Instant around it and assert banked <= 1.5x span (banked2 <= span3). Preemption inflates span and banked equally so the ratio is load-stable, while a naive per-guard double-count (~2x span) is still caught. Same pattern applies to any GilWorkGuard/RunLoopWallGuard test in gil_profile.rs.

Process-global-counter tests must assert on a DELTA across their own bump window, never on an absolute threshold over the whole emitted map. angr-c0wlh: test_simplify_sample_ticker_is_not_emitted (native/angr/src/symbolic/stats_tests.rs) scanned get_solver_stats() for any value >= MARK (1<<40), which conflates its own marker with any unrelated large counter, and needed a name-based contains('time')/ends_with('_ns') carve-out for wall-clock sums — a duration counter spelled any other way slips through. Fix: snapshot before + after the bump, flag only keys that grew by >= MARK, with saturating_sub so a concurrent reset_solver_stats() reads as no-growth (fails safe: a reset can hide a real leak, never invent one). Same rule applies to total_while_bumped's siblings. Also: MARK-bump helpers must call undo_bump BEFORE any assert/expect that can panic, or the marker leaks into the global counter for the rest of the process.

Guest-controlled size/offset feeding a HOST allocation must be capped natively in the Rust handler — do NOT 'fall back to Python' as the defense. The Python procedure (e.g. procedures/posix/mmap.py -> map_region, brk.py -> set_brk) allocates just as eagerly, so bouncing only relocates the OOM. Rust's SymbolicMemory::map walks the range page-by-page and MemoryPage::new does an eager vec![0u8; PAGE_SIZE] per page (NOT lazy/COW from a shared zero page), so an unbounded length also hangs the O(pages) scan long before it OOMs. Five shared caps: syscalls::mod's MAX_IO_SIZE (bytes serviced natively before a legitimate Python fallback) and MAX_MAP_SIZE (host-safety bound on address space MAPPED; used by syscalls::mmap::do_mmap as MAX_MMAP_SIZE and syscalls::brk::NativeBrkSyscall::call as MAX_BRK_GROWTH), state::filesystem::fd's MAX_FS_FILE_SIZE (host-safety bound on an fd's eager content Vec; enforced inside FileSystem::write / write_at, angr-c7xno.67) and MAX_FD (upper bound on a caller-chosen fd number; enforced inside FileSystem::dup2, angr-03vl4.52), plus procedures::malloc's MAX_ALLOC_SIZE (every allocator proc — malloc/calloc/realloc/memalign/posix_memalign — calls check_max with it before state.heap_alloc). Note the destination-vs-length distinction that hid .67: MAX_IO_SIZE bounds only the per-call LENGTH at every call site, never the write OFFSET, so an unbounded lseek/pwrite64 offset still reached resize(). Reject the way the real kernel signals failure — mmap returns -1/MAP_FAILED, brk returns the UNCHANGED break — rather than erroring out. ORDERING RULE (angr-c7xno.67): when a host-safety refusal lives at a choke point that also performs an ownership transfer (FileSystem::write's demote_symbolic_content, which hands a registered file to Python), the refusal must come AFTER the transfer — refusing first leaves Rust serving stale native content while the Python fallback performs the write. Place it before any Arc::make_mut so a refusal costs no CoW. LAYERING RULE (angr-03vl4.52): the cap belongs on the shared MODEL method, not on one entry point. Most libc calls have TWO native entry points into the same model — the raw syscall handler (syscalls/) and the libc SimProcedure (procedures/) — and a bound enforced in only one is simply absent from the other: syscalls::file_descriptor::dup2_body enforced NEWFD_LIMIT while procedures::fileops::NativeDup2 called the identical FileSystem::dup2 with no bound at all. When Python-parity ordering forces a duplicate check at the entry point (Python's dup2 returns success for oldfd==newfd BEFORE its range test), keep the entry-point check but derive its constant from the model's, never a second literal. Corollary: a guest fd/handle arrives as u64; narrowing it with as u32 at the entry point ALIASES an unrelated object (0x1_0000_0000 -> 0 == stdin), so use u32::try_from and treat overflow as the not-found error. NO-HOST-ALLOCATION COROLLARY (angr-03vl4.53): a cap is still required where the guest size drives NO host allocation at all. RustSimState::heap_alloc is pure address-space bookkeeping, yet an uncapped near-u64::MAX size wrapped its 16-byte rounding down to a tiny bump, so two logically-distinct mallocs ALIAS — a wrong symbolic-execution answer, not an OOM. So audit an allocator/IO family for SIBLING PARITY (four of five malloc procs capped; malloc alone did not) and make the shared model's size rounding saturating (state::process::round_alloc_size), not plain +. Keep Python-parity constants (syscalls::cgc::CGC_MAX_ALLOCATION mirrors state.cgc.max_allocation) separate from host-safety caps even when the value coincides, so lowering one for safety can't silently break parity.

MIPS32/MIPS64 GUEST_STATE_SIZE in arch/mips.rs (offsets32/offsets64) used to be 432/592 -- exactly where the late-VEX bookkeeping block (emnote/cmstart/cmlen/nraddr/...ip_at_syscall) BEGINS, so the guest state buffer truncated every register archinfo places after the FPU control block. angr-9ke6b.10 grew them to archinfo's real state end (496/624). Convention across arch/: GUEST_STATE_SIZE == max(offset+size) over archinfo's register map (X86 344, AMD64 1060, MIPS32 496, MIPS64 624; ARM 400 is 4 over archinfo's 396). RegisterFile::new allocates vec![0u8; arch.state_size()], and arch/registry_tests.rs::register_names_all_resolve_and_fit_in_u128 + vex_bookkeeping_fields_resolve_on_every_arch both assert offset+size <= state_size, so a new register past the old bound fails loudly rather than corrupting. PLACEMENT RULE: emnote/cmstart/cmlen/nraddr/ip_at_syscall live in each arch's ALIASES table, not CANONICAL (so register_name reverse lookup does not claim those offsets) and not REGISTER_NAMES (not exported to Python's named-register channel) -- X86/ARM/ARM64 set that precedent and AMD64/MIPS now match.

HeapMetadata.freed (native/angr/src/state/types.rs) is a SET, not a free-call log: record_free skips an address already in freed, same as union_from does on the merge path (angr-9ke6b.127, commit 003d31b4e). So free_count/get_heap_free_count/proxy heap.freed count DISTINCT freed pointers — never use them to detect a double free. The signal for a double free is record_free returning None (the allocated entry was already removed). Kept as a Vec with a linear contains() scan rather than a hash set so export order stays deterministic (first-free order); freed stays small per path so the O(n) scan is not a hot cost. Any future consumer wanting free-call multiplicity must add a separate counter, not un-dedup this field.

A SimProcedure installed via proj.hook(addr, proc) at a BINARY-INTERNAL address takes the hook path and NEVER consults the Rust native-procedure registry — so a natively-implemented proc still bounces to Python. Measured 2026-07-14 (iter144, angr-gorvf.12): cmu_binary_bomb_partial bounces strcmp at 0x401338 even though procedures/mod.rs registers Arc::new(strcmp::NativeStrcmp), and the whole bench reports native_proc_calls == 0. Extern/PLT procs (the 0x7000xx pseudo-addresses) DO go through native dispatch — that is why fauxware's open and unbreakable_0's strncpy tick native_proc_symbolic_fallbacks_by_name while cmu's strcmp ticks nothing. CONSEQUENCE for any bounce/fallback audit: the native_proc__fallbacks_by_name counters are BLIND to this class — they only tick when the registry is consulted. Cross-check the bounced name against the registry's own 'name = "..."' attrs in native/angr/src/procedures/.rs (zeropy_bounce_census.py::native_registry_names does exactly this) or you will misfile a dispatch gap as a missing proc.

Native syscall handlers must NOT run extract_concrete_arg() on an argument they never read: forcing concretization turns a symbolic value into SyscallError::SymbolicArgument and a needless Python syscall_stub round-trip for an outcome identical to the concrete case. Use let _ = args.get(N); instead — the convention already used by syscalls/file_descriptor.rs::fcntl_dispatch (F_SETFL arg), NativeIoctlSyscall (ioctl arg) and, since angr-9ke6b.155, NativeDup3Syscall (O_CLOEXEC flags). Only concretize args whose value actually steers dispatch or state. Test shape: file_descriptor_tests.rs::dup3_tolerates_symbolic_flags_without_python_fallback.

Init cache key must include concrete argv/env, not just binary hash (angr-gxaht). RustDiskCacheManager._concrete_input_digest (rust_disk_cache.py) md5s the SP stack page — SimLinux.state_entry writes argc/argv/envp + arg/env strings there via table.dump(state, sp-16), so distinct concrete inputs differ in that page. Threaded into _compute_mem_init_key (appends ':') and _compute_disk_init_key (appends '-') in rust_manager.py; caller _run_python_init_if_needed computes it once. GOTCHA: eval(page, cast_to=bytes) raises SimError/SimUnsatError on an unsat state (error-recovery tests seed unsat deliberately) — the digest helper catches broad Exception and returns '' (non-differentiating fallback), so DON'T narrow that except back to AttributeError/KeyError. _state_has_user_symbolic only catches SYMBOLIC divergence; concrete-input divergence needs this digest. Determinism: cast_to=bytes resolves default-fill symbolic bytes to minimum (0), stable cross-process.

INVARIANT: the Rust manager's init cache (rust_disk_cache.py + rust_manager._try_in_memory_init_cache/_try_disk_init_cache) is built from a plain blank_state and re-attached to a user state via _apply_state_metadata, which ONLY carries constraints, globals, and an option allow-list. The allow-list is ALSO a mirror (add when src has it, discard when it doesn't): options not listed get STRIPPED on init-cache hits, and listed options must be mirror-applied (not just additive) because the in-memory _init_cache is keyed by binary path — a cached state populated from a prior STRICT_PAGE_ACCESS run would otherwise leak that option to a subsequent caller that didn't request it. Mirror pattern introduced commit 1c3263198 (angr-zd4x); TRACK_ACTION_HISTORY added for preconstrainer compat in angr-fkvt (2026-06-06). Read the tuple in _apply_state_metadata for the live list (LAZY_SOLVES, STRICT_PAGE_ACCESS, ENABLE_NX, NO_IP_CONCRETIZATION, NO_SYMBOLIC_JUMP_RESOLUTION, KEEP_IP_SYMBOLIC, TRACK_ACTION_HISTORY, plus _NATIVE_SIMOPTIONS since angr-kzjv6) — when adding a new honored SimOption you MUST add it there or the option silently disappears after the first cache-warm run. The cache does NOT carry memory pages, the fs (SimFilesystem) plugin, or the posix fd table. Therefore any user state customization beyond constraints/globals/allow-listed options must be detected by _state_has_user_symbolic (the cache-disable gate) — otherwise a cache hit silently drops it. As of commit 00a1bb3dc the gate scans: SP stack page, non-stack symbolic memory pages, register file, AND state.fs._files (non-empty => disable). The gate is enforced in _compute_disk_init_key (and _compute_mem_init_key): returns '' when the state has user-created symbolic data (e.g. argv BVS — blank_state from cache cannot round-trip their identity), suppressing BOTH the load AND save paths. If you add a new user-customizable plugin that must survive init, EITHER extend _apply_state_metadata to copy it OR extend _state_has_user_symbolic to disable the cache when it is populated. Tests: tests/engines/rust/test_state_roundtrip.py::TestInitCacheUserSymbolicGate. || THIRD FAILURE MODE, added angr-6cp06.12 (2026-09-07): a CONCRETE plugin scalar is caught by NEITHER lever. _state_has_user_symbolic only gates on symbolic data, and _apply_state_metadata does not copy plugin attributes, so simos/linux.py's state.posix.{argv,argc,environ,auxv} pointers were all None after _deserialize_init_state even though the KEY=VALUE string table they point at IS in the cached stack_page. As of angr-7tmoz all four are persisted and restored: the three address-shaped ones through _extract_posix_pointer over the _POSIX_POINTER_FIELDS tuple, argc through _extract_posix_argc as a (value, width) pair because consumers call BV methods on it (argc.sign_extend), and all of them re-attached as claripy BVs by _restore_posix_entry_fields (_PYTHON_METADATA_VERSION now 3). GENERAL RULE: any Rust<->Python bridge that reads a plugin attribute at state-add time must ALSO persist it in the pickle, or it works cold and silently no-ops warm. TESTING GOTCHA: such a bug is invisible to a fresh-checkout test run — a cold cache takes the real Python-init path and passes. Force the disk path explicitly (construct one manager to populate, RustExplorationManager._init_cache.clear(), construct a second) as tests/engines/rust/test_environ_seed.py::test_warm_disk_cache_hit_keeps_environ does; a single-run green here proves nothing. SECOND TESTING GOTCHA (angr-7tmoz): a warm-disk test that uses the real ~/.cache/angr_rust_init is order-dependent — a pickle a prior run left behind means the cold run never calls _save_init_to_disk_cache, so a capture-the-save fixture skips instead of failing. Redirect _disk_cache_dir at a tmp_path, and do it with mock.patch.object, NOT a setattr/restore pair: the mixin defines it as an inherited staticmethod, so restoring by hand rebinds a plain function onto the class that then eats self and breaks disk caching for every later test in the session (464 failures, all green in isolation). See tests/engines/rust/test_disk_cache_posix.py.

The Rust init disk cache (~/.cache/angr_rust_init) is bounded by _prune_disk_cache in angr/exploration/rust_disk_cache.py, NOT by version-prefix GC. Why prefix GC is impossible: _disk_cache_key MD5s the version axes (_RUST_CACHE_VERSION/_PYTHON_METADATA_VERSION) together with the binary content and arch, so the filename carries no recoverable generation marker -- a stale generation is indistinguishable from a current one by inspection. The working mechanism is a usage-ordered budget: _prune_disk_cache ranks *.pkl newest-mtime-first and unlinks past _disk_cache_budgets() (ANGR_RUST_INIT_CACHE_MAX_BYTES / ANGR_RUST_INIT_CACHE_MAX_FILES, defaults 512MiB/128; 0 disables a dimension). Two non-obvious invariants: (1) _load_init_pickle calls os.utime on every hit, which is what makes mtime last-USE not last-write -- without it a hot binary rebuilt rarely gets evicted ahead of a one-shot binary, and stale generations never age out; (2) the just-written keep_key is charged against the budget BEFORE the eviction loop and never evicted, so a single oversized binary degrades to a one-entry cache instead of an empty one (a naive mid-scan skip overshoots the budget by its size). Covered by tests/engines/rust/test_disk_cache_gc.py.

Real-binary integration tests for arches without locally-available ELF binaries can construct a minimal ELF inline in the test using struct.pack: 64-byte ELF64 header + 56-byte PT_LOAD program header + raw code bytes. Pattern locked in commit 5b6f034ba (test_aarch64_explore_real_elf): e_machine=0xB7 (AARCH64) / 0x28 (ARM) etc., PT_LOAD with p_flags=5 (RX), p_vaddr=p_paddr, p_align=0x1000, p_offset=0 covers the headers + code in one segment. CLE's ELF backend parses this without sections. This is the workaround when no real binary is available AND no cross-compiler is installed AND lief is not installed — instead of skipping the test, construct the ELF inline. Used for AArch64 because angr-examples has no AArch64 binary and gcc is host-only. MIPS32 instantiation (ELF32 differs): EM_MIPS=0x08 in e_machine; ELF32 header=52 bytes, ELF32 phdr=32 bytes with different field order (p_type,p_offset,p_vaddr,p_paddr,p_filesz,p_memsz,p_flags,p_align); e_flags=0x50001000 = EF_MIPS_ARCH_32 | EF_MIPS_ABI_O32. MIPS32 instruction encodings verified for inline-ELF tests (endian-agnostic at decode; storage byte order set by EI_DATA): ADDIU rt,rs,imm=0x24080000|imm16 (rt=t0=8, rs=zero=0); BEQ rs,rt,off=0x10000000|(rs<<21)|(rt<<16)|off16 (off in PC-relative words, target = PC+4+(off<<2)); B off=0x10000000|off16 (BEQ zero,zero); NOP=0x00000000. Branch delay slot must always be filled (NOP works). For LE storage: struct.pack('<I', opcode). Equivalent pattern applies to MIPS64 if binaries are unavailable.

The inspect-event 'Supported events' grid table in docs/advanced-topics/rust_engine.rst is now guarded by TestRustInspectAllowlistConsistency.test_doc_supported_events_table_matches_code (tests/engines/rust/test_proxy.py): _parse_doc_supported_events() finds the 'Supported events' section, brackets the RST simple table by its 3 '====' delimiter lines, and extracts the first backtick token of every non-indented body line (event rows start at col 0; BP-attr continuation lines are indented). Asserts that set == _RUST_INSPECT_SUPPORTED_EVENTS exactly. Companion to TestRustSimOptionMatrixConsistency (test_misc.py) for the SimOption half. INVARIANT: when you add/remove an event in _INSPECT_EVENT_SPECS (rust_state_proxy.py), add/remove the matching table row in the SAME commit or this test reddens. angr-c4xcs.2.

writev/readv native syscall handlers (syscalls/fd_io.rs, NativeWritevSyscall/NativeReadvSyscall) walk a struct iovec[] where each element is two POINTER-WIDTH words (iov_base, iov_len) read via state.arch().bytes() — NOT fixed 8-byte. writev must gather ALL concrete bytes across every segment BEFORE calling write_fd: returning Err mid-loop falls back to Python which redoes the whole write, so any partial write_fd would double-write. The append-only FileSystem::write (state.rs) is why pread64/pwrite64 were deferred (angr-dbb1): positioned write needs an offset-honoring write_at. lseek/readv/writev/uname/set_tid_address/set_robust_list/getrandom are AMD64-only so far (nums 8/19/20/63/218/273/318).

angr register-name aliases: 'ip' is the architecture-independent INSTRUCTION POINTER in archinfo on every arch (ARMEL 'ip'==(68,4)==R15T, AMD64 'ip'==rip), NOT the ARM-ABI scratch register r12. native/angr/src/arch/*.rs deliberately define no 'ip' alias at all (angr-itm3u removed arm.rs's ('ip', R12, 4) entry) — RustStateProxy::_canonical_name in angr/exploration/rust_state_proxy.py resolves 'ip' via archinfo.register_size_names before the name reaches Rust, so direct RustSimState.set_register('ip', ..) raising ValueError is the intended loud failure. Do not re-add an ABI-flavored 'ip'.