nx_bck_iv_gate.nx

nx_bck_iv_gate.nx -- THE ELISION PROOF GATE for LN7b (bck_elide_induction) and for the compiler's data-driven MODES (--mode=<name>, knowledge/lang_modes.conf). Sibling of nx_bck_elide_gate and built from the same parts (nx_ccbuild_lib, gv_*): sources assembled at RUNTIME under /tmp, compiled two ways by the compiler named in argv[1] (there is NO default compiler -- a gate that forks whatever is installed reports on a binary nobody chose), the emitted ASSEMBLY as the oracle for "fired" / "did not fire", and out-of-bounds witnesses whose only remaining protection is the check the pass was asked to keep. WHAT MUST FIRE: the receipt loop's own shape -- a counter initialised to a constant, incremented by a constant inside a `while k < N` whose N is the array's length, indexing that array. WHAT MUST NOT: F2 the guard is WIDER than the array (`while k < 2048` over [1024]i64) -- and it traps 71 under both builds, so the refusal is measured on a program that really does go out of range; F3 the counter is incremented by a value that is not a constant -- its range is unknowable here; F4 a constant reset (`k = 4000`) sits on the path between the guard and the access -- the guard's fact is dead by the time the access runs, and the program traps 71 under both builds; F5 the counter's address ESCAPES (`let p: *i64 = &k`) -- a store through p is invisible to the pass, and the program traps 71 under both builds. gv_bite ties the two halves: the detector must change F1 and leave F2 byte-identical. MODES: `--mode=f1` must produce assembly byte-identical to `--bckelide` (the bundle is exactly its flags, no more), and `--mode=nonesuch` must REFUSE the build (a silent default is a mode wearing the wrong name). Products land in _build/ because NAS /tmp is mounted noexec (the sibling gate's measured lesson). license_tier: ORIGINAL No hw writes (Rule 26).