Validation client 1: schema_inner_equation, relationally

A relational re-proof of schema_inner_equation (PlonkLean/RO/OneWayness_GameHop/GuessExperiment.lean), the per-σ', t correspondence between the match-tracking game (set a target, flag matches on the fly) and the recording game (record all queries, compare at the end).

The unary original needs ≈950 lines (state-alignment via wp_shift_input, three EquivModuloLens chains, a bespoke invariant-agreement loop induction, maxHeartbeats 1600000). Relationally it is one synchronized loop invariant:

Inv σ₁ σ₂ := ∃ l, σ₂ = qs.set l (matched.set m₀ (target.set tv₀ σ₁))
               ∧ matched.get σ₁ = decide (t ∈ l)

("the recording state is the matching state with the three bookkeeping lenses overwritten, and the matched flag agrees with membership in the recorded list"), threaded through relE.loop_n and relE.bind. The shared query q relates to itself across the lens overwrite by self_lens_set (× 3, composed with relE.trans), framed by the matched-flag value.

Note the statement is more general than the original: generic in the state type, and no Fintype/Nonempty assumptions on T.

theorem PRHLSchema.schema_inner_equation_prhl {s T : Type} [DecidableEq T] (target_var : GaudisCrypt.Lens T s) (matched_var : GaudisCrypt.Lens Bool s) (queries_list_var : GaudisCrypt.Lens (List T) s) [GaudisCrypt.disjoint matched_var queries_list_var] [GaudisCrypt.disjoint matched_var target_var] (q_body q_final : GaudisCrypt.ProgramDenotation s T) (h_q_body_matched : q_body.inFootprint matched_var.footprintᶜ) (h_q_body_qs : q_body.inFootprint queries_list_var.footprintᶜ) (h_q_body_target : q_body.inFootprint target_var.footprintᶜ) (h_q_final_matched : q_final.inFootprint matched_var.footprintᶜ) (h_q_final_qs : q_final.inFootprint queries_list_var.footprintᶜ) (h_q_final_target : q_final.inFootprint target_var.footprintᶜ) (n : ℕ) (σ' : s) (t : T) : (do GaudisCrypt.ProgramDenotation.set target_var t GaudisCrypt.ProgramDenotation.set matched_var false GaudisCrypt.loop_n n do let a ← q_body if a = t then GaudisCrypt.ProgramDenotation.set matched_var true else pure () do let a ← q_final if a = t then GaudisCrypt.ProgramDenotation.set matched_var true else pure () GaudisCrypt.ProgramDenotation.get matched_var).wp (fun (bσ : Bool × s) => if bσ.1 = true then 1 else 0) σ' = (do GaudisCrypt.ProgramDenotation.set queries_list_var [] GaudisCrypt.loop_n n do let a ← q_body let qs ← GaudisCrypt.ProgramDenotation.get queries_list_var GaudisCrypt.ProgramDenotation.set queries_list_var (qs ++ [a]) do let a ← q_final let qs ← GaudisCrypt.ProgramDenotation.get queries_list_var GaudisCrypt.ProgramDenotation.set queries_list_var (qs ++ [a]) let qs ← GaudisCrypt.ProgramDenotation.get queries_list_var GaudisCrypt.ProgramDenotation.set matched_var (decide (t ∈ qs)) GaudisCrypt.ProgramDenotation.get matched_var).wp (fun (bσ : Bool × s) => if bσ.1 = true then 1 else 0) σ'

schema_inner_equation, relationally. Same statement as the unary original, but generic in the state type, without Fintype/Nonempty assumptions on T, and needing only two of the original's three disjointness assumptions.