Cycle801 Lane3 - reuse the target's OWN test harness for faithful invariant encoding; empirically-tested WALK > recon WALK

Date: 2026-08-08 (Day 56). Context: ran the cycle171-banked INV-1/2/3 on Origin ARM (arm-oeth) after unblocking the build. All PASS = empirically-tested WALK.

What WORKED

• forge soldeer install was the entire cycle171 blocker. A recon-grade WALK had banked 3 invariants "scheduled, blocked on soldeer deps." One command (forge soldeer install) resolved it; forge build then exit-0. Lesson: a build "blocker" on a soldeer/foundry project is usually just an un-run dependency install - try it before deferring the whole invariant test to "next cycle."
• Extend the target's OWN test harness instead of building from scratch. arm-oeth ships Unit_MultiAssetARM_Shared_Test (real ARM proxy + real MockAssetAdapter cross-price config + 4 base assets + LP/donation helpers). Writing INV-1/2/3 as a 90-line test that is Unit_MultiAssetARM_Shared_Test gave a FAITHFUL harness (real accounting, real adapter valuation) in minutes, and inherited their mocks/actors/config. A hand-rolled harness would risk an UNFAITHFUL setup (worse than no test - the anti-overclaim trap of a green test that doesn't model the real system). Always look for the project's Shared/Base/Setup test scaffold first.
• Encode the design PROMISE as the invariant. The cross-price NatSpec literally states the intent ("base sell price >= cross price ... so assets-per-share does not decrease if the ARM sells base at a discount"). INV-2 = "unprivileged donation/appreciation never DECREASES assets-per-share" is exactly that promise, fuzzed. Turning the stated design invariant into an assertion is the highest-signal drift test.

Result + honest boundary

• INV-1 (no free value), INV-2/2b (share-price monotonicity under donation/appreciation), INV-3 (round-trip vault-favorable): ALL PASS @ 1000 runs. The Jun-2026 multi-adapter cross-price refactor holds for the deposit/donation/rate/redeem-conversion classes. WALK, empirically-backed.
• Coverage boundary stated (not hidden): the full adapter-queue-move (base -> adapter.requestRedeem -> pendingRedeemAssets -> claimRedeem) x privileged setCrossPrice interleaving needs a STATEFUL invariant handler (foundry invariant_ + targetContract), not a stateless fuzz. Documented as the exact residual + scheduled, per the 24-hour rule (a banked test that's run + a named residual, not "save and forget").

Compound principle

An "empirically-tested WALK" is strictly more valuable than a "recon-grade WALK": it converts a source-read hunch into a reproducible artifact (DriftInvariants.fuzz.t.sol) that (a) defends the no-finding call under the anti-overclaim floor, (b) is a re-runnable regression check if the target ships new adapters, and (c) is Securva audit collateral. Bank the test file as a receipt, not just the verdict.