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

add_constraints (native/angr/src/solver.rs) partial-batch contract: the raw Z3-AST fast path converts entries until one AST fails the is_bool() / claripy_to_rustbv gate, then flushes the converted PREFIX via SymContext::add_constraints_raw_batch and resumes from the failing index with per-constraint add_constraint_ast. Two invariants any future edit must keep: (1) resume_from == entries.len(), so a failure at index 0 means an EMPTY batch (add_constraints_raw_batch early-returns on empty) and resume_from=0 -- off-by-one here silently DROPS a constraint; (2) prefix-then-remainder preserves the original constraint order, which the unbatched loop guaranteed. Measured on N=300 Bool + 1 non-Bool last entry: pre-fix 4.406ms, post-fix 3.595ms (-18%), identical to a batch with no failure at all. Regression-covered by test_add_constraints_mixed_batch_applies_every_entry and test_add_constraints_leading_failure_still_applies_rest in tests/engines/rust/test_solver_ops.py. (angr-9ke6b.206)

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.

When carving a newtype out of u64 for a subsystem, distinguish byte ADDRESSES from PAGE NUMBERS (addr >> 12). Address newtype wraps byte addresses; page-keyed structures (pages: OrdMap<u64, MemoryPage>, dirty_pages: FxHashSet, lazy_regions: Vec<(u64, u64)>) MUST stay raw u64 because they're a different conceptual layer. Mixing them would defeat the type-safety win. 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. See native/angr/src/memory/address.rs for the documented migration pattern.

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). Otherwise every call to the mutator forces a deep clone even when no real change happens. See FileSystem::close/read/seek and RustSimState::clear_hooks for the pattern. Avoid Arc-wrap for fields mutated on every fork (e.g. RegisterFile.symbolic) — make_mut churn would offset the savings.

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 (scheduler::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_from_name (native/angr/src/arch/mod.rs) accepted names must all resolve to a CallingConvention. Since angr-9ke6b.216 both sides read ONE table: ALL_ARCHES (arch/mod.rs), a const slice of ArchDesc { name, aliases, vex, make_arch, make_cc }; arch_from_name/arch_from_vex/cc_for_arch/default_cc_for_arch all iterate it via arch_desc_from_name, so the completeness invariant is structural rather than a coincidence between two hand-written lists. Before that, arch_from_name had match arms and each CC carried its own ARCH_ALIASES const, which drifted. RustExplorationManager::new (manager_methods.rs) calls arch_from_name THEN default_cc_for_arch on the same string; a name accepted by the former but missing a CC passes the lookup then PANICS in default_cc_for_arch (PanicException) — a recognized alias failing more violently than an unrecognized one (clean PyValueError). test_arch_from_name_names_all_have_a_cc pins completeness; test_arch_aliases_disjoint pins no-overlap. To add an alias, add it to the ALL_ARCHES row.

ALL_ARCHES (native/angr/src/arch/mod.rs) name+aliases spellings must stay disjoint across rows. arch_desc_from_name walks the table in declaration order, so a spelling in two rows makes both arch_from_name and default_cc_for_arch silently order-dependent. test_arch_aliases_disjoint (arch/calling_conventions_tests.rs) pins this; do not weaken it. Superseded the per-CC ARCH_ALIASES consts deleted in angr-9ke6b.216. Decision recorded there: 'mips64be' is deliberately NOT a registered name — MIPS64 big-endian states are built as 'mips64' + Iend_BE; it used to sit in MipsN64::ARCH_ALIASES while arch_from_name rejected it, and the merge resolved that by rejecting it everywhere (test_mips64be_is_not_a_registered_arch_name).

The architecture-independent register spellings in native/angr/src/arch/*.rs ALIASES tables are "sp", "bp" (angr-6qzik) and "pc" (angr-9ke6b.217) — all six arches now resolve all three. There is deliberately NO "ip" alias on ANY arch: on ARM the ABI calls r12 "ip", so exposing the ABI reading made a Python write through "ip" land in r12 instead of the PC (angr-itm3u). RustStateProxy._canonical_name rewrites "pc"/"ip" to the arch canonical name via archinfo before the name reaches Rust, so the Python path never depended on these; they exist for direct Rust-level / RustSimState.set_register callers. Gate: arch/mod_tests.rs::test_all_arches_report_expected_special_register_offsets asserts register_offset("pc") == ip_offset on every ALL_ARCHES row. NOTE tests/engines/rust/test_arch_offset_parity.py CANNOT catch a missing alias — its harness skips any archinfo name Rust does not know, so absent names are invisible there; only the Rust sweep sees them.

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). The (name, offset, size) triplet is now 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_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. 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 now enforced on BOTH bridge directions. IMPORT: claripy_bridge/import.rs::claripy_to_rustbv compares cached_bv.width() to ast.length on AST_CACHE hit. 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. Unit test: cache_tests.rs::test_evict_claripy_ast_clears_both_stores. 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 cross-cache invariants C2/C6 (which existed solely for that cache) are gone; see claripy-bridge-thread-local-caches.

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

Invariant for any future consumer of SymContext::bare_z3_push_depth (angr-3ms1 step 1a): the counter ONLY reflects pushes on the 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 inherit the parent value at fork; this matters if future code threads bare pushes across fork, though today fork resets push_level so the inherited value is moot. (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.

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 (absorbed from invariant-catalog-tier-vs-medium-suite, 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 (bench, timeout) 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.rs) are TWO separate lowerings of Clz/Ctz/Popcount that must stay in sync. 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.

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.

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

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.

calc_flags_sub/add in native/angr/src/vex/ccall/x86_concrete.rs compute CF as 'arg_l < arg_r' on the RAW u64 values (NOT masked to nbits). This relies on VEX's invariant that ccall args are pre-masked to the operand width (the cc_dep IRExpr is typed at nbits). If you ever diff-fuzz the concrete vs symbolic path with random u64 inputs, pre-mask both sides to get_mask(nbits) — otherwise CF disagrees when the high bits differ between dep1/dep2. The symbolic path (sym_flags_sub) is the precise version since it extract_to_nbits's its inputs first.

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.

PythonCallbacks (native/angr/src/callbacks/mod.rs) has ONE source of truth for its 34 Option<Py> slots: the with_callback_fields! macro, which expands to $m!{field, field, ...}. new(), traverse_fields and clear_fields are all generated from it via local macro_rules! consumers (empty_holder / visit_fields / clear_all). To add a callback you edit exactly TWO places: the struct definition (doc comment + type) and that list — plus the set_* pymethod if Python needs to install it. WHY it matters: traverse_fields and clear_fields back traverse/clear on BOTH PythonCallbacks and RustExplorationManager (which holds a clone). A slot present in one list but not the other, or missing from both, silently keeps the mgr -> _callbacks -> bound method -> mgr reference cycle alive and leaks the manager plus its _state_cache (~4030 angr pages/call on mma_howtouse — the 9maq leak). ENFORCEMENT is compile-time, not a test: clear_fields destructures 'let Self { ... } = self' EXHAUSTIVELY, deliberately without a '..' rest pattern, so a field added to the struct but not the list has no binding and fails to build. Do NOT 'fix' that by adding '..' — that silently disarms the guard. Self-tested (angr-9ke6b.27) by adding a probe field to the struct alone: E0063 from the new() expansion + 'pattern requires .. due to inaccessible fields' from the clear destructure. The non-Py Arc fields (inspect_enabled, memory_is_rust_proxy, python_servable_pages, python_page_universe) are named explicitly in the destructure (three as ': _') for the same reason. Runtime half pinned by callbacks_tests.rs::clear_fields_drops_every_callback_slot.

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

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

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.

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

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

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.

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. Three fns + MAX_CONCRETE_CHUNK=16: store_concrete_bytes_chunked, load_concrete_bytes_chunked, u128_to_le_bytes; 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. The five call sites: state_api::_get_state_memory + _set_state_memory_concrete, pending_api::_get_pending_memory + _pending_memory_load + _pending_memory_store/_set_pending_memory, state/pymethods.rs::{memory_load,memory_store}. 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. HISTORY (absorbed from invariant-concrete-load-16b-chunking, which explicitly marked itself superseded by this key): 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).

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.

Phase 4.2 flush_multi_cells (multi.rs::flush_multi_cells) coalesces runs of adjacent Multi bytes ONLY when payload_cond_fingerprint() matches across consecutive addresses. Fingerprint uses Arc::as_ptr identity of RustBV::Expression operands — relies on install_multi_for_candidates building one cond RustBV per candidate then cloning into each byte (so neighbours from the same store-call share the same Arc). Any new store path that emits Multi bytes MUST follow this 'build cond once, clone into each byte' pattern, or it will silently fall back to the per-byte flush path (correctness preserved, perf loss). Run length is capped at COALESCE_MAX_RUN=16 because RustBV::concat_into's u128 concrete fast-path silently truncates widths >120+8. Lift the cap only after auditing concat_into for wider-than-128 safety.

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. Two 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. 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. Regression test: memory/tests/basic.rs::test_wide_concrete_load_exact. (2) BIT-SLICING (was invariant-concrete-extract-width128): 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).

RustBV concrete fast-paths that shift/mask a u128 by a bit position (not an operand-supplied amount) must guard for width>128: a Concrete stores its value in a u128, so any bit >=128 is logically zero, and shifting a u128 by >=128 is a debug abort / release mod-128 wrap. Canonical guards live in extract_into (value_ops.rs): shift=0 when low>=128, mask=u128::MAX when result_width>=128; concat_into keeps result_width>128 as a Concat expr instead of folding. extract_no_ctx had the same window logic but WITHOUT the guards until angr-ph300.31 -> aborted/mis-extracted on 256-bit ymm sub-register overlays (arch/mod.rs extract_no_ctx callers). Any new concrete BV op that shifts by a bit position must copy extract_into's guards. Complements [[invariant-concrete-shift-clamp-before-narrow]] which covers operand-amount narrowing.

Concrete shift/rotate arms in RustBV (value_ops.rs shl_into/lshr_into/ashr_into/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's semantics for out-of-range amounts.

invariant-concrete-width-gt-128-fast-paths: 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. Guards added (angr-qwyti.12): shl_into/lshr_into cut off at a>=width.min(128); ashr_into at width>128 collapses to lshr (sign bit at pos width-1>=128 is zero) and guards amt>=128; sign_extend_to returns value early when from_width>=128 (source non-negative, and avoids 1u128<<(from_width-1) overflow). Same class as invariant-concrete-bv-u128-16-byte-limit / invariant-concrete-shift-clamp-before-narrow / sign_extend_to-128 (qwyti.16) / sar_fill_mask (qwyti.17). Any NEW concrete fast-path op that shifts/masks a u128 by a width or bit-position must guard width>=128. Deterministic tests: WIDE_WIDTHS block in value_ops_property_tests.rs.

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

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. Concrete case: 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. [UPDATE angr-2j9sk] The sibling divergence in strtod.rs/strtol.rs is now FIXED and all whitespace classification shares procedures::ctype::is_c_space — see invariant-native-whitespace-single-source, which also records why strtol/strtod match libc rather than Python (Python skips no whitespace at all).

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.

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), push_assertion/extend_assertions 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 or extend_assertions -- direct .push()/.extend() on the Vec leaves the set stale and breaks the invariant. 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, was invariant-dedup-seeding-quadratic-cost): 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. Applies to future dedup-extension work (e.g., add_bv_constraint, add_constraints_raw_batch).

The 'fuzzer' cargo feature (native/angr/Cargo.toml: icicle-fuzzing/icicle-vm/libafl/libafl_bolts/pcode, git deps on icicle-emu) builds and its 9 unit tests (fuzzer::corpus::tests, fuzzer::executor::tests) pass: 'make test-fuzzer' == 'cargo test --release --features fuzzer --lib fuzzer'. 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.

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.

Every deferred-fork materialization in exploration/resume.rs MUST include the P11 (reconstruct condition from fork.condition_ast) and P15 (fork_base.fork() to unexplored_target, unconstrained) fallback arms. 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. P11 arm 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 P11 — off-GIL worker threads cannot Python::attach; only stored_conditions.get + P15 there.

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.

Native VEX dirty-helper handlers in native/angr/src/vex/dirty.rs are ONLY reachable if ALL their args are concrete u64. statements.rs (dirty stmt branch, ~L815) eval_expr_with_callbacks each arg first; IRExpr::GSPTR/VECRET return NeedPythonFallback (expressions.rs ~L98), propagating via ? before DirtyHelperDispatch::try_call runs. So any helper VEX invokes with a GSPTR arg (CPUID, RDTSCP) is DEAD CODE natively and must be handled by the Python engine — do NOT add native handlers for them. Reachable today: RDTSC (no args), IN/OUT (concrete port). angr-2iow measured zero GSPTR hits corpus-wide; angr-t1ok removed the dead CPUID/RDTSCP handlers.

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

Generic divmod_double_to_single (now in native/angr/src/vex/ops_int_arith.rs after the ops.rs split; symbol-anchored) handles all VEX DivMod{U,S}{64to32,128to64} via dividend_w = 2*divisor_w. CONCRETE PATH -- CRITICAL: the concrete signed branch must sign-extend the dividend from its declared width to i128, NOT just 'value as i128' -- for divmod_64_to_32 the dividend's bit 63 IS its sign bit, but treating a u128 with high bits=0 as i128 always gives a positive number. Use sign_extend_low_to_i128(value, width). Same applies to the divisor (sign-extended from divisor_w). Result packing is (quotient | (remainder << divisor_w)) at dividend_w bits. SYMBOLIC PATH (was invariant-divmod-symbolic; both signed+unsigned IROp variants): extend divisor to dividend width using zero_extend for unsigned ops or sign_extend for signed, then udiv/sdiv + urem/srem on the extended pair, finally extract low N/2 bits of each and concat(remainder, quotient). Result format is low = quotient, high = remainder -- concat puts self in high, other in low, so concat(remainder, quotient). Z3's div/mod by zero is total and matches claripy, so no explicit zero guard is needed for the symbolic path.

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. Used at: PutI (statements.rs, symbolic index branch) and eval_geti (expressions.rs) — both pinned by angr-eg6j; exit-target concretization (exits.rs); dirty-call args (statements.rs). 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 (angr/engines/vex/heavy/heavy.py:115-124): 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 (was invariant-check-executable-test-needs-both-flags): 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.

angr-9ke6b.99: memory page-range checks must go through memory::end_page_inclusive(addr, size) (native/angr/src/memory/mod.rs), never inline (addr + size - 1) >> 12. size==0 underflows; the workspace [profile.release] has overflow-checks OFF so release wraps to u64::MAX instead of panicking, and SymbolicMemory::check_perms_range then iterates start_page..=~4.5e15 — a hang, not an error. Two distinct underflows exist per load: the end_page one AND the wider-symbolic-object extract's size * 8 - 1 (u32) inside load_concrete, which fires BEFORE end_page is computed — hence the explicit size==0 early-return at the top of load_concrete and load_concrete_lazy_inner in addition to the helper. size==0 is reachable: _pending_memory_load (exploration/pending_api.rs) forwards a Python-supplied size unchecked, and on the store side size = value.width() / 8 is 0 for any sub-byte-width BV. Exclusive-end (addr + size + PAGE_SIZE - 1) >> 12 sites are safe and keep their zero-size no-op semantics.

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.

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

eval_upto/eval_upto_wide (native/angr/src/symbolic/solving_ops.rs) return witnesses in CANONICAL ASCENDING ORDER as of angr-op0dn.10.1 (commit 3f5e2a782). As of angr-9ke6b.142 (commit 0277e87a6) the enumeration machinery — warm-model seed, exclude-loop, trailing sort_unstable — lives in ONE shared helper, SymContext::enumerate_distinct<T: Ord>(ast, n, extract, exclusion_of); the two public fns keep only their concrete fast paths, the deterministic-mode branch (eval_upto only), the query_class scope, and the closures. So the sort is now in enumerate_distinct, not at the callsites. Presentation-only: the enumerated SET is decided by the exclude-loop and the ovqja.4 warm-model seed, so the sort cannot change WHICH values come back, only their order. For eval_upto_wide every witness is exactly width bits, so all byte vectors are the same length and big-endian lexicographic sort == numeric sort (see u128_to_be_bytes_width). INVARIANT for future work: any short-circuit or early-return added inside eval_upto (e.g. an M1 trivial-decide tier) must land ABOVE the helper call / sort, or it reintroduces order nondeterminism. Truncated case (n < #feasible) still returns an arbitrary Z3-chosen SUBSET — canonical subset choice is M2.2 (angr-op0dn.10.2). Tests: context_tests/solver.rs::test_eval_upto_canonical_order / test_eval_upto_wide_canonical_order.

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. Two of its #[pyo3(get,set)] knobs were dead and were deleted in 32b9901b1 (angr-9ke6b.16/.17): (1) max_concretization_range (default 65536) had no reader anywhere; the real symbolic-address bounds are ConcretizerConfig::{read_range_limit,write_range_limit} in concretize.rs (1024/128, SimOption-driven) -- extend THAT struct, never re-add a knob here; (2) 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 (it existed solely for BranchPolicy::Alternate and was already write-only under #[allow(dead_code)]). LESSON for the rest of the .16-.17-class audit beads: 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. Both 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.

op_zero_extend/op_sign_extend (solver.rs #[pymethods]) now call reject_extend_narrowing() to raise PyValueError when to_width < source width, instead of zero_extend_into silently returning a wider BV (which surfaced far away as a Z3 sort error / silent eq-False). zero_extend_into + sign_extend_into are now symmetric: both debug_assert!(to_width>=width) with == early-return. No internal caller narrows via extend (VEX widening ops, procedures all widen; strtol guards with 'if w<bits'). Width lookup uses table.with_value(a_id,|bv|bv.width()) — no clone. angr-ph300.38.

ExtractionError type lives in native/angr/src/arch/calling_conventions.rs and is re-exported from arch::mod. Variants: MemoryUnavailable (caller asked for stack args but passed None memory), SpSymbolic (regs.get(sp).as_u64() failed), StackUnmapped{arg_index,addr} (mem.load_concrete_lazy failed for that specific slot), RegisterOverflow{requested,available}. The trait method extract_args returns Result<Vec, ExtractionError> as of c858f7e5b; if a caller can entirely satisfy the request from registers (num_args <= arg_registers().len()) it never touches memory and always succeeds. UPDATE (angr-9ke6b.214, 2026-07-31): the VEXInterpreter::extract_simprocedure_args wrapper was DELETED as dead code — production argument extraction now runs entirely through exploration::core_outcome_cc and exploration::helpers, which reimplement the register-then-stack walk over RustSimState and construct SpSymbolic/StackUnmapped/RegisterOverflow themselves. CallingConvention::extract_args (and the MemoryUnavailable variant only it produces) survives solely for arch/calling_conventions_tests and carries #[cfg_attr(not(test), allow(dead_code))]. Don't reintroduce silent placeholders in EITHER implementation.

extract_z3_ast_ptr in solver.rs returns Err on null pointer. Callers using NonNull::new_unchecked on the Ok value can rely on this — no need for '!= 0' guard at call site. If you ever change extract_z3_ast_ptr to return raw usize again, all 3 unsafe call sites in solver.rs need null guards reinstated (add_constraint_ast, eval, eval_upto).

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.

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.

Pending-callback states are reachable through the ordinary state API: RustExplorationManager::find_state_mut (exploration/helpers.rs) checks self.pending_callbacks BEFORE self.sm, so with_state_mut/with_state cover pending states too. Consequence: 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.

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.

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.

FP-return calling convention: CallingConvention::fp_return_register() (native/angr/src/arch/calling_conventions.rs) is the single source of truth for where a scalar double return lands. Some(224)=xmm0 on SystemVAMD64, Some(320)=q0/v0 on AArch64CC, None everywhere else (x86 returns in the x87 st0 stack, ARM EABI soft-float in the r0:r1 integer pair, MIPS in $f0 — none are modelled in our register files). A native proc returning a double writes the 64-bit IEEE-754 bit pattern to the LOW 64 bits of that offset and must return Ok(None) to suppress the dispatcher's default integer-return store (see procedures/strtod.rs::NativeStrtod). To add a new FP-return arch: implement the trait method, do NOT hard-code an offset in the proc. Companion: cc_for_arch() is the non-panicking registry lookup — use it in procs that can defer to Python; default_cc_for_arch() keeps the loud panic for argument extraction, where a wrong CC would silently yield wrong-but-plausible args.

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.

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.

icicle.rs is behind the default-OFF fuzzer cargo feature (native/angr/src/lib.rs gates pub mod icicle on #[cfg(feature = "fuzzer")]). Consequence: a plain cargo test --release compiles and runs ZERO icicle tests — icicle_tests.rs is invisible to the default build AND to the ralph gate / CI cargo-test step. Any change to icicle.rs (Hitmap, VmExit/ExceptionCode bridges, invalidate_code_range predicates) must be verified with an explicit cargo test --manifest-path native/angr/Cargo.toml --release --features fuzzer --lib -- icicle::tests. That build pulls cranelift + icicle-jit + icicle-vm + icicle-fuzzing from a git rev: ~2m47s cold, ~28s for a --lib --tests check once the deps are cached. Same trap shape as the libvex-ffi feature (see zeropy-gate-libvex-build-recipe): a default-feature gate silently excludes a whole test module.

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.

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.

callbacks/inspect.rs: all 17 call_inspect_* methods share one prologue helper, PythonCallbacks::with_inspect_cb (attach + GilWorkGuard::enter_site(CallbackSite::Inspect) + callback-slot unwrap), plus the free fn opt_ast_or_none for the Option<&Py> -> py.None() attr wrap. INVARIANT: with_inspect_cb attaches and opens the GIL-profiling span BEFORE checking whether the slot is Some. That ordering is deliberate and preserved from the pre-refactor open-coded bodies -- hoisting the slot check out of Python::attach looks like a free optimization but silently changes CallbackSite::Inspect GIL accounting (unregistered slots stop being counted), which no test catches. The 'absent' parameter is the value returned when no callback is registered: None for mem_read/mem_write (which return PyResult<Option<Py>> for the value-injection path), () for the other 15. Landed angr-9ke6b.26, 506->398 lines, zero behavior change.

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

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

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