Perfectly Correct

theorem perfectlyCorrect [SampleableType Chal]    (hc : σ.PerfectlyComplete) :    SignatureAlg.PerfectlyComplete      (FiatShamir (m := OracleComp (unifSpec + (M × Commit →ₒ Chal))) σ hr M)      (runtime M) := by  intro msg  rw [perfectlyCorrect_evalDist_eq σ hr M msg]  change    Pr[= true | (do      let (pk, sk) ← hr.gen      let (c, e) ← σ.commit pk sk      let r ← $ᵗ Chal      let s ← σ.respond pk sk e r      pure (σ.verify pk c r s) : ProbComp Bool)] = 1  vcstep  vcstep using (fun x => OracleComp.ProgramLogic.propInd (x ∈ support hr.gen))  · simpa [OracleComp.ProgramLogic.propInd] using      OracleComp.ProgramLogic.triple_support (oa := hr.gen)  · intro x    rcases x with ⟨pk, sk⟩    by_cases hx : (pk, sk) ∈ support hr.gen    · have hrel : rel pk sk = true := hr.gen_sound pk sk hx      simpa [OracleComp.ProgramLogic.propInd, hx] using        (OracleComp.ProgramLogic.triple_probOutput_eq_one          (oa := do            let (c, e) ← σ.commit pk sk            let r ← $ᵗ Chal            let s ← σ.respond pk sk e r            pure (σ.verify pk c r s))          (x := true) (h := by simpa using hc pk sk hrel))    · simpa [OracleComp.ProgramLogic.propInd, hx] using        (OracleComp.ProgramLogic.triple_zero          (oa := do            let (c, e) ← σ.commit pk sk            let r ← $ᵗ Chal            let s ← σ.respond pk sk e r            pure (σ.verify pk c r s))          (post := fun y => if y = true then 1 else 0))