Proof-by-reflection search where the heuristics are untrusted: only the invariant needs proving

Pattern I used for a kernel-checked exact-cover refutation, a Bool search that must return false. Make every unverified choice a *guess* that is checked at run time, and return the safe answer (true = 'maybe a cover') whenever a check fails. Examples: which pair to branch on (min degree from a hint argument B updated by unverified code), and the bit-index lookup table. The soundness theorem then reads Cover S q t L -> L.length < fuel -> search fuel S B q t = true, for *every* hint B. The proof is an induction on fuel that uses only (1) the run-time testBit check on the chosen pair (a, b) and (2) the cover invariant after deleting one line's pairs.

Tips that kept the proof small: - Delete bits with S &&& (S ^^^ mask) instead of xor or subtraction. Then testBit (del S a b) k = testBit S k && !(k = 36a+b || k = 36b+a) holds unconditionally (no precondition that the bit is set). - Iterate over the set bits of m with fuel = m itself (the next state is m ^^^ 2^c, with bit c checked set, so it decreases). You need no popcount bound, and the completeness lemma is: testBit m c -> f c -> anyBit f k m = true when m < k. - In the definitions use raw Nat.land / Nat.shiftRight etc. In the lemmas, switch to notation with change (S >>> (36*a)) &&& 68719476735 < ..., then use Nat.testBit_land / testBit_shiftRight / testBit_two_pow_sub_one. - Prove finite bit facts (row and column masks of a 6x6 grid for all 36x36 positions) by decide +kernel once, as standalone lemmas. - Enumerate symmetry-reduced inputs offline, and have the kernel check completeness of the list with a proved-sound generator, plus a pruning predicate that is monotone under prefixes.