From 60502dc6f6246fbdeef676e8ecaae966492dcab7 Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Wed, 15 Jul 2026 22:53:39 -0500 Subject: [PATCH 1/6] refactor(OracleComp): make OracleComp and OracleQuery reducible over PolyFun Make `OracleComp`, `OracleQuery`, and `OracleSpec.toPFunctor` reducible aliases of their `PolyFun` counterparts and delete the bespoke `Monad`/`LawfulMonad`/`MonadLift`/`Functor` instances, so PolyFun's own instances and lemmas apply directly to oracle computations. Repair the resulting breakage: restate `Traversal` over `PFunctor.FreeM.Cursor`, re-key `toPFunctor_add` off the simp set, narrow ReplayFork's local transparency to `PFunctor.Idx`, route invariant-preservation proofs via `simulateQ_spec_query`, and align the `@[vcspec]`/`@[wpStep]` registry lookups with `Sym` pattern preprocessing via `symMatchKey`. Co-Authored-By: Claude Fable 5 --- Examples/PRGfromPRF.lean | 2 +- .../Sigma/Stateful/Compatibility.lean | 10 +- VCVio/CryptoFoundations/ReplayFork.lean | 13 +- VCVio/OracleComp/OracleComp.lean | 21 +- VCVio/OracleComp/OracleQuery.lean | 8 +- VCVio/OracleComp/OracleSpec.lean | 6 +- .../SimSemantics/StateT/PreservesInv.lean | 2 +- .../SimSemantics/WriterT/PreservesInv.lean | 3 +- VCVio/OracleComp/Traversal.lean | 185 ++++++++++++++---- VCVio/ProgramLogic/Tactics/Common/Core.lean | 11 ++ .../ProgramLogic/Tactics/Common/Registry.lean | 5 +- .../Tactics/Common/WpStepRegistry.lean | 3 +- VCVio/StateSeparating/CellRef.lean | 2 +- docs/agents/gotchas.md | 9 +- docs/agents/program-logic.md | 12 ++ 15 files changed, 208 insertions(+), 84 deletions(-) diff --git a/Examples/PRGfromPRF.lean b/Examples/PRGfromPRF.lean index 8d4c21c88..4ff53f183 100644 --- a/Examples/PRGfromPRF.lean +++ b/Examples/PRGfromPRF.lean @@ -109,7 +109,7 @@ private lemma simulateQ_prfReal_oracleOutputs (k : K) (n : ℕ) (s : S) : | succ n ih => simp only [oracleOutputs, streamOutputs, simulateQ_bind, simulateQ_query, OracleQuery.cont_query, id_map, OracleQuery.input_query] - show prfRealQueryImpl prf k (Sum.inr s) >>= _ = _ + change prfRealQueryImpl prf k (Sum.inr s) >>= _ = _ simp only [prfRealQueryImpl, QueryImpl.add_apply_inr] cases h : prf.eval k s with | mk s' out => diff --git a/VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean b/VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean index 7c58cc08d..14243af22 100644 --- a/VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean +++ b/VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean @@ -701,13 +701,11 @@ theorem statefulPostKeygenFreshAdvantage_eq_cmaRealRunProb_signedFreshAdv (oa := (SourceSigAlg (σ := σ) (hr := hr) (M := M)).verify ps.1 msg (c, resp))] cases hcache : cache (msg, c) with | some ch => - simpa [monad_norm] using - fiatShamirVerify_run_eq_cmaRealSourceFullSum_run_signedFresh_cache_some - σ hr M ps msg c resp bad signed cache keypair ch hcache + exact fiatShamirVerify_run_eq_cmaRealSourceFullSum_run_signedFresh_cache_some + σ hr M ps msg c resp bad signed cache keypair ch hcache | none => - simpa [monad_norm] using - fiatShamirVerify_run_eq_cmaRealSourceFullSum_run_signedFresh_cache_none - σ hr M ps msg c resp bad signed cache keypair hcache + exact fiatShamirVerify_run_eq_cmaRealSourceFullSum_run_signedFresh_cache_none + σ hr M ps msg c resp bad signed cache keypair hcache /-- Fixed-key public post-keygen experiment in the WriterT signing-log form. -/ @[reducible] private noncomputable def postKeygenFreshWriterComp diff --git a/VCVio/CryptoFoundations/ReplayFork.lean b/VCVio/CryptoFoundations/ReplayFork.lean index 159a08d3b..eb895cf27 100644 --- a/VCVio/CryptoFoundations/ReplayFork.lean +++ b/VCVio/CryptoFoundations/ReplayFork.lean @@ -25,12 +25,11 @@ open OracleSpec OracleComp OracleComp.ProgramLogic ENNReal Function Finset open scoped OracleSpec.PrimitiveQuery open scoped PFunctor --- Dependent path/zipper APIs must see that an oracle specification's --- polynomial positions and directions are its domain and ranges. Keep this --- transparency local: exporting it changes simplifier normal forms in --- unrelated OracleComp proofs. +-- Dependent path/zipper APIs identify `QueryLog` entries with erased polynomial +-- trace events, so `PFunctor.Idx` must unfold during `simp`/`rw` matching in +-- this file. Kept local: `Idx` is a Mathlib definition. set_option allowUnsafeReducibility true in -attribute [local reducible] OracleSpec.toPFunctor PFunctor.Idx +attribute [local reducible] PFunctor.Idx namespace QueryLog @@ -460,11 +459,11 @@ theorem contextFork_success rw [mem_support_freeM_bind_iff] at h obtain ⟨path, hpath, h⟩ := h rcases hcf : cf (PFunctor.FreeM.output main path) with _ | s - · simp [hcf, mem_support_freeM_pure_iff] at h + · simp [hcf] at h · simp only [hcf] at h rcases hlocated : PFunctor.FreeM.Cursor.locateAt? (P := spec.toPFunctor) i main path s with _ | located - · simp [hlocated, mem_support_freeM_pure_iff] at h + · simp [hlocated] at h · simp only [hlocated] at h rw [mem_support_freeM_map_iff] at h obtain ⟨second, hsecond, hresult⟩ := h diff --git a/VCVio/OracleComp/OracleComp.lean b/VCVio/OracleComp/OracleComp.lean index a78f0e203..fefacc327 100644 --- a/VCVio/OracleComp/OracleComp.lean +++ b/VCVio/OracleComp/OracleComp.lean @@ -18,6 +18,7 @@ open OracleSpec /-- `OracleComp spec α` represents computations with oracle access to oracles in `spec`, where the final return value has type `α`, represented as a free monad over the `PFunctor` corresponding to `spec.` -/ +@[reducible] def OracleComp {ι : Type u} (spec : OracleSpec.{u, v} ι) : Type w → Type (max u v w) := PFunctor.FreeM spec.toPFunctor @@ -34,21 +35,16 @@ This is the explicit abstraction boundary for generic PolyFun constructions; downstream semantics should use this function instead of unfolding `OracleComp`. -/ @[reducible] -def ofFreeM {α : Type w} (oa : PFunctor.FreeM spec.toPFunctor α) : - OracleComp spec α := - oa +def ofFreeM {α : Type w} (oa : PFunctor.FreeM spec.toPFunctor α) : OracleComp spec α := oa /-- Expose the polynomial free program underlying an oracle computation. -/ @[reducible] -def toFreeM {α : Type w} (oa : OracleComp spec α) : - PFunctor.FreeM spec.toPFunctor α := - oa +def toFreeM {α : Type w} (oa : OracleComp spec α) : PFunctor.FreeM spec.toPFunctor α := oa theorem ofFreeM_toFreeM {α : Type w} (oa : OracleComp spec α) : ofFreeM (toFreeM oa) = oa := rfl -theorem toFreeM_ofFreeM {α : Type w} - (oa : PFunctor.FreeM spec.toPFunctor α) : +theorem toFreeM_ofFreeM {α : Type w} (oa : PFunctor.FreeM spec.toPFunctor α) : toFreeM (ofFreeM oa) = oa := rfl /-- Make one oracle query at input `t`, then continue with `k` on the response. @@ -61,15 +57,6 @@ def queryBind {α} (t : spec.Domain) (k : spec.Range t → OracleComp spec α) : OracleComp spec α := PFunctor.FreeM.liftBind t k -instance (spec : OracleSpec ι) : Monad (OracleComp spec) := - inferInstanceAs (Monad (PFunctor.FreeM spec.toPFunctor)) - -instance (spec : OracleSpec ι) : LawfulMonad (OracleComp spec) := - inferInstanceAs (LawfulMonad (PFunctor.FreeM spec.toPFunctor)) - -instance : MonadLift (OracleQuery spec) (OracleComp spec) := - inferInstanceAs (MonadLift (PFunctor.Obj spec.toPFunctor) (PFunctor.FreeM spec.toPFunctor)) - theorem ofFreeM_pure {α : Type v} (x : α) : ofFreeM (PFunctor.FreeM.pure x : PFunctor.FreeM spec.toPFunctor α) = (pure x : OracleComp spec α) := rfl diff --git a/VCVio/OracleComp/OracleQuery.lean b/VCVio/OracleComp/OracleQuery.lean index ee2a83c8b..cfc0ba4e8 100644 --- a/VCVio/OracleComp/OracleQuery.lean +++ b/VCVio/OracleComp/OracleQuery.lean @@ -20,6 +20,7 @@ defined to be the object type of the corresponding `PFunctor`. In particular an element of `OracleQuery spec α` consists of an input value `t : spec.Domain`, and a continuation `f : spec.Range t → α` specifying what to do with the result. See `OracleSpec.query` for the case when the continuation `f` just returns the query result. -/ +@[reducible] def OracleQuery {ι : Type u} (spec : OracleSpec.{u, v} ι) : Type w → Type (max u v w) := PFunctor.Obj spec.toPFunctor @@ -73,13 +74,6 @@ namespace OracleQuery variable {ι : Type u} {spec : OracleSpec.{u, v} ι} -/-- `OracleQuery spec` inherits the functorial structure from `PFunctor.Obj`. -/ -instance {spec : OracleSpec ι} : Functor (OracleQuery spec) where - map := spec.toPFunctor.map - -instance {spec : OracleSpec ι} : LawfulFunctor (OracleQuery spec) := - inferInstanceAs (LawfulFunctor (PFunctor.Obj spec.toPFunctor)) - /-- The oracle input used in an oracle query. -/ @[inline, reducible] def input {α} (q : OracleQuery spec α) : spec.Domain := q.1 diff --git a/VCVio/OracleComp/OracleSpec.lean b/VCVio/OracleComp/OracleSpec.lean index 673b34d41..1806dc72d 100644 --- a/VCVio/OracleComp/OracleSpec.lean +++ b/VCVio/OracleComp/OracleSpec.lean @@ -29,6 +29,7 @@ namespace OracleSpec variable {ι : Type u} +@[reducible] def toPFunctor (spec : OracleSpec ι) : PFunctor := { A := ι, B := spec } @[reducible, inline] @@ -97,7 +98,10 @@ lemma add_def {ι ι'} (spec : OracleSpec ι) (spec' : OracleSpec ι') : @[simp] lemma add_apply_inr {ι ι'} (spec : OracleSpec ι) (spec' : OracleSpec ι') (t : ι') : (spec + spec') (.inr t) = spec' t := rfl -@[simp] lemma toPFunctor_add {ι : Type u} {ι' : Type u'} +/-- Deliberately not `@[simp]`: `toPFunctor` occurs inside the (instance-carrying) +type of an `OracleComp`, so rewriting with this under a `simulateQ`/`liftM` strands +the goal in a form the `simulateQ_query` family can no longer match. -/ +lemma toPFunctor_add {ι : Type u} {ι' : Type u'} (spec : OracleSpec ι) (spec' : OracleSpec ι') : (spec + spec').toPFunctor = spec.toPFunctor + spec'.toPFunctor := rfl diff --git a/VCVio/OracleComp/SimSemantics/StateT/PreservesInv.lean b/VCVio/OracleComp/SimSemantics/StateT/PreservesInv.lean index 1b009ebc5..7d4bd585c 100644 --- a/VCVio/OracleComp/SimSemantics/StateT/PreservesInv.lean +++ b/VCVio/OracleComp/SimSemantics/StateT/PreservesInv.lean @@ -98,7 +98,7 @@ theorem simulateQ_run_preservesInv simpa [simulateQ_bind, OracleComp.liftM_def] using hz rcases (mem_support_bind_iff _ _ _).1 hz' with ⟨us, hus, hzcont⟩ have hus' : us ∈ support ((impl t).run σ0) := by - simpa [OracleSpec.query_def, simulateQ_query] using hus + simpa [simulateQ_spec_query] using hus exact ih us.1 us.2 (himpl t σ0 hσ0 us hus') z hzcont end OracleComp diff --git a/VCVio/OracleComp/SimSemantics/WriterT/PreservesInv.lean b/VCVio/OracleComp/SimSemantics/WriterT/PreservesInv.lean index 33fb29657..d8ebca1d2 100644 --- a/VCVio/OracleComp/SimSemantics/WriterT/PreservesInv.lean +++ b/VCVio/OracleComp/SimSemantics/WriterT/PreservesInv.lean @@ -112,8 +112,7 @@ theorem simulateQ_run_writerPreservesInv simpa only [mul_one] using hs₀ | query_bind t oa ih => intro s₀ hs₀ z hz - simp only [OracleSpec.query_def, ofPFunctor_toPFunctor, simulateQ_bind, simulateQ_query, - OracleQuery.input_apply, OracleQuery.cont_apply, id_map, WriterT.run_bind, support_bind, + simp only [simulateQ_bind, simulateQ_spec_query, WriterT.run_bind, support_bind, support_map, Set.mem_iUnion, Set.mem_image, Prod.exists, exists_prop] at hz obtain ⟨u, w, hus, v, w', hvs, rfl⟩ := hz simpa only [mul_assoc] using ih u (s₀ * w) (himpl t s₀ hs₀ (u, w) hus) (v, w') hvs diff --git a/VCVio/OracleComp/Traversal.lean b/VCVio/OracleComp/Traversal.lean index be3adb781..59c3c3b31 100644 --- a/VCVio/OracleComp/Traversal.lean +++ b/VCVio/OracleComp/Traversal.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Devon Tuma, Quang Dao -/ import VCVio.OracleComp.EvalDist +import PolyFun.PFunctor.Free.Cursor /-! # Traversing Possible Paths of a Computation @@ -12,6 +13,13 @@ This file defines structural predicates for checking whether all or some reachab `OracleComp` satisfy predicates on query nodes and final outputs, relative to a chosen set of possible oracle outputs. +The predicates are phrased in terms of `PFunctor.FreeM.Cursor`: a cursor is a typed path prefix +into the underlying free-monad tree, so quantifying over cursors whose recorded answers stay +within the possible outputs simultaneously reaches every demanded query node (via non-terminal +cursors) and every reachable final output (via terminal cursors). Two generic helpers, +`PFunctor.TraceList.WithinOn` and `PFunctor.FreeM.Cursor.Sat`, express the answer-membership +filter and the per-cursor demand. + It also connects those structural predicates to the denotational set `supportWhen`, so proofs can move cleanly between the syntax-level traversal view and the reachable-output view. -/ @@ -22,76 +30,177 @@ universe u v w open scoped OracleSpec.PrimitiveQuery +namespace PFunctor + +variable {P : PFunctor.{u, v}} {α : Type w} + +namespace TraceList + +/-- Every event recorded on a trace answers within the allowed fibers. +Generic over the polynomial `P`; a candidate for upstreaming into `PolyFun`. -/ +def WithinOn (allowed : (a : P.A) → Set (P.B a)) (events : PFunctor.TraceList P) : Prop := + ∀ e ∈ events, e.2 ∈ allowed e.1 + +@[simp] lemma withinOn_nil (allowed : (a : P.A) → Set (P.B a)) : + WithinOn allowed ([] : PFunctor.TraceList P) := + fun _ he => absurd he (List.not_mem_nil) + +@[simp] lemma withinOn_cons (allowed : (a : P.A) → Set (P.B a)) + (e : P.Idx) (es : PFunctor.TraceList P) : + WithinOn allowed (e :: es) ↔ e.2 ∈ allowed e.1 ∧ WithinOn allowed es := + List.forall_mem_cons + +end TraceList + +namespace FreeM.Cursor + +/-- The demand a cursor places on a pair of predicates: a cursor selecting a leaf demands the +leaf predicate on its payload, while a cursor selecting an internal query node demands the node +predicate on its label. Generic over the polynomial `P`; a candidate for upstreaming into +`PolyFun`. -/ +def Sat (nodePred : P.A → Prop) (leafPred : α → Prop) + {program : PFunctor.FreeM P α} (c : PFunctor.FreeM.Cursor program) : Prop := + match c.residual with + | .pure x => leafPred x + | .liftBind a _ => nodePred a + +@[simp] lemma sat_root_pure (nodePred : P.A → Prop) (leafPred : α → Prop) (x : α) : + Sat nodePred leafPred (root (.pure x : PFunctor.FreeM P α)) = leafPred x := rfl + +@[simp] lemma sat_root_liftBind (nodePred : P.A → Prop) (leafPred : α → Prop) + (a : P.A) (next : P.B a → PFunctor.FreeM P α) : + Sat nodePred leafPred (root (.liftBind a next)) = nodePred a := rfl + +@[simp] lemma sat_down (nodePred : P.A → Prop) (leafPred : α → Prop) + {a : P.A} {next : P.B a → PFunctor.FreeM P α} + (answer : P.B a) (tail : PFunctor.FreeM.Cursor (next answer)) : + Sat nodePred leafPred (down answer tail) = Sat nodePred leafPred tail := rfl + +end FreeM.Cursor + +end PFunctor + namespace OracleComp -variable {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} +open PFunctor + +variable {ι : Type u} {spec : OracleSpec.{u, v} ι} {α β γ : Type v} /-- Given that oracle outputs are bounded by `possibleOutputs`, every reachable query input in the -computation satisfies `queryPred`, and every reachable pure output satisfies `outputPred`. -/ +computation satisfies `queryPred`, and every reachable pure output satisfies `outputPred`. + +Phrased as: every cursor into the computation whose recorded answers stay within +`possibleOutputs` satisfies its demand (`PFunctor.FreeM.Cursor.Sat`). Non-terminal cursors +reach every demanded query node — including nodes with no possible continuation below them — +while terminal cursors reach every possible final output. -/ def allPathsSatisfy (queryPred : spec.Domain → Prop) (outputPred : α → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) - (oa : OracleComp spec α) : Prop := by - induction oa using OracleComp.construct with - | pure x => exact outputPred x - | query_bind q _ ih => exact queryPred q ∧ ∀ x ∈ possibleOutputs q, ih x + (oa : OracleComp spec α) : Prop := + ∀ c : PFunctor.FreeM.Cursor oa, + TraceList.WithinOn possibleOutputs c.trace → FreeM.Cursor.Sat queryPred outputPred c /-- Given that oracle outputs are bounded by `possibleOutputs`, some reachable query input in the -computation satisfies `queryPred`, or some reachable pure output satisfies `outputPred`. -/ +computation satisfies `queryPred`, or some reachable pure output satisfies `outputPred`. + +Phrased as: some cursor into the computation whose recorded answers stay within +`possibleOutputs` satisfies its demand (`PFunctor.FreeM.Cursor.Sat`). -/ def somePathSatisfies (queryPred : spec.Domain → Prop) (outputPred : α → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) - (oa : OracleComp spec α) : Prop := by - induction oa using OracleComp.construct with - | pure x => exact outputPred x - | query_bind q _ ih => exact queryPred q ∨ ∃ x ∈ possibleOutputs q, ih x + (oa : OracleComp spec α) : Prop := + ∃ c : PFunctor.FreeM.Cursor oa, + TraceList.WithinOn possibleOutputs c.trace ∧ FreeM.Cursor.Sat queryPred outputPred c /-- Output-only view of [`OracleComp.allPathsSatisfy`]: every output reachable under `possibleOutputs` satisfies `outputPred`. -/ def allOutputsSatisfyWhen (outputPred : α → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) : Prop := - oa.allPathsSatisfy (fun _ => True) outputPred possibleOutputs + allPathsSatisfy (fun _ => True) outputPred possibleOutputs oa /-- Output-only view of [`OracleComp.somePathSatisfies`]: some output reachable under `possibleOutputs` satisfies `outputPred`. -/ def someOutputSatisfiesWhen (outputPred : α → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) : Prop := - oa.somePathSatisfies (fun _ => False) outputPred possibleOutputs + somePathSatisfies (fun _ => False) outputPred possibleOutputs oa variable {queryPred : spec.Domain → Prop} {outputPred : α → Prop} {possibleOutputs : (x : spec.Domain) → Set (spec.Range x)} @[simp] lemma allPathsSatisfy_pure (x : α) : - (pure x : OracleComp spec α).allPathsSatisfy queryPred outputPred possibleOutputs = - outputPred x := rfl + allPathsSatisfy queryPred outputPred possibleOutputs (pure x : OracleComp spec α) = + outputPred x := by + refine propext ⟨fun h => h (PFunctor.FreeM.Cursor.root _) (by simp), fun h c hw => ?_⟩ + obtain ⟨res, sp⟩ := c + cases sp + exact h @[simp] lemma somePathSatisfies_pure (x : α) : - (pure x : OracleComp spec α).somePathSatisfies queryPred outputPred possibleOutputs = - outputPred x := rfl + somePathSatisfies queryPred outputPred possibleOutputs (pure x : OracleComp spec α) = + outputPred x := by + refine propext ⟨fun ⟨c, _, hc⟩ => ?_, fun h => ⟨PFunctor.FreeM.Cursor.root _, by simp, h⟩⟩ + obtain ⟨res, sp⟩ := c + cases sp + exact hc @[simp] lemma allPathsSatisfy_query_bind (q : spec.Domain) (oa : spec.Range q → OracleComp spec α) : - ((query q : OracleComp spec _) >>= oa).allPathsSatisfy queryPred outputPred possibleOutputs ↔ + allPathsSatisfy queryPred outputPred possibleOutputs + ((query q : OracleComp spec _) >>= oa) ↔ queryPred q ∧ - ∀ x ∈ possibleOutputs q, (oa x).allPathsSatisfy queryPred outputPred possibleOutputs := - Iff.rfl + ∀ x ∈ possibleOutputs q, + allPathsSatisfy queryPred outputPred possibleOutputs (oa x) := by + change allPathsSatisfy queryPred outputPred possibleOutputs + (PFunctor.FreeM.liftBind q oa) ↔ _ + constructor + · intro h + refine ⟨h (PFunctor.FreeM.Cursor.root _) (by simp), fun u hu c hc => ?_⟩ + exact h (PFunctor.FreeM.Cursor.down u c) + (by simp only [PFunctor.FreeM.Cursor.trace_down, TraceList.withinOn_cons]; exact ⟨hu, hc⟩) + · rintro ⟨hq, h⟩ ⟨res, sp⟩ hw + cases sp with + | root => exact hq + | down answer tail => + simp only [show (⟨res, PFunctor.FreeM.Cursor.Spine.down answer tail⟩ : + PFunctor.FreeM.Cursor _) = PFunctor.FreeM.Cursor.down answer ⟨res, tail⟩ from rfl, + PFunctor.FreeM.Cursor.trace_down, TraceList.withinOn_cons, + FreeM.Cursor.sat_down] at hw ⊢ + exact h answer hw.1 ⟨res, tail⟩ hw.2 @[simp] lemma somePathSatisfies_query_bind (q : spec.Domain) (oa : spec.Range q → OracleComp spec α) : - ((query q : OracleComp spec _) >>= oa).somePathSatisfies queryPred outputPred possibleOutputs ↔ + somePathSatisfies queryPred outputPred possibleOutputs + ((query q : OracleComp spec _) >>= oa) ↔ queryPred q ∨ - ∃ x ∈ possibleOutputs q, (oa x).somePathSatisfies queryPred outputPred possibleOutputs := - Iff.rfl + ∃ x ∈ possibleOutputs q, + somePathSatisfies queryPred outputPred possibleOutputs (oa x) := by + change somePathSatisfies queryPred outputPred possibleOutputs + (PFunctor.FreeM.liftBind q oa) ↔ _ + constructor + · rintro ⟨⟨res, sp⟩, hw, hc⟩ + cases sp with + | root => exact Or.inl hc + | down answer tail => + simp only [show (⟨res, PFunctor.FreeM.Cursor.Spine.down answer tail⟩ : + PFunctor.FreeM.Cursor _) = PFunctor.FreeM.Cursor.down answer ⟨res, tail⟩ from rfl, + PFunctor.FreeM.Cursor.trace_down, TraceList.withinOn_cons, + FreeM.Cursor.sat_down] at hw hc + exact Or.inr ⟨answer, hw.1, ⟨res, tail⟩, hw.2, hc⟩ + · rintro (hq | ⟨u, hu, c, hw, hc⟩) + · exact ⟨PFunctor.FreeM.Cursor.root _, by simp, hq⟩ + · refine ⟨PFunctor.FreeM.Cursor.down u c, ?_, hc⟩ + simp only [PFunctor.FreeM.Cursor.trace_down, TraceList.withinOn_cons] + exact ⟨hu, hw⟩ /-- Every output of `oa` reachable under `possibleOutputs` satisfies `outputPred` exactly when `outputPred` holds throughout `oa.supportWhen possibleOutputs`. -/ lemma allOutputsSatisfyWhen_iff_supportWhen (outputPred : α → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) : - oa.allOutputsSatisfyWhen outputPred possibleOutputs ↔ + allOutputsSatisfyWhen outputPred possibleOutputs oa ↔ ∀ x ∈ oa.supportWhen possibleOutputs, outputPred x := by induction oa using OracleComp.inductionOn with | pure x => simp [OracleComp.allOutputsSatisfyWhen, OracleComp.supportWhen_pure] @@ -104,7 +213,7 @@ lemma allOutputsSatisfyWhen_iff_supportWhen (outputPred : α → Prop) `outputPred` holds at some point of `oa.supportWhen possibleOutputs`. -/ lemma someOutputSatisfiesWhen_iff_supportWhen (outputPred : α → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) : - oa.someOutputSatisfiesWhen outputPred possibleOutputs ↔ + someOutputSatisfiesWhen outputPred possibleOutputs oa ↔ ∃ x ∈ oa.supportWhen possibleOutputs, outputPred x := by induction oa using OracleComp.inductionOn with | pure x => simp [OracleComp.someOutputSatisfiesWhen, OracleComp.supportWhen_pure] @@ -120,12 +229,13 @@ lemma allPathsSatisfy_bind_iff (queryPred : spec.Domain → Prop) (outputPred : β → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) (ob : α → OracleComp spec β) : - (oa >>= ob).allPathsSatisfy queryPred outputPred possibleOutputs ↔ - oa.allPathsSatisfy queryPred - (fun x => (ob x).allPathsSatisfy queryPred outputPred possibleOutputs) - possibleOutputs := by - induction oa using OracleComp.inductionOn <;> - simp [monad_norm, OracleComp.allPathsSatisfy_query_bind, *] + allPathsSatisfy queryPred outputPred possibleOutputs (oa >>= ob) ↔ + allPathsSatisfy queryPred + (fun x => allPathsSatisfy queryPred outputPred possibleOutputs (ob x)) + possibleOutputs oa := by + induction oa using OracleComp.inductionOn with + | pure x => simp [pure_bind] + | query_bind q oa ih => simp [monad_norm, OracleComp.allPathsSatisfy_query_bind, ih] /-- A bind satisfies an existential path property exactly when either the first computation already satisfies it on some path, or one reachable continuation does. -/ @@ -134,12 +244,13 @@ lemma somePathSatisfies_bind_iff (queryPred : spec.Domain → Prop) (outputPred : β → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) (ob : α → OracleComp spec β) : - (oa >>= ob).somePathSatisfies queryPred outputPred possibleOutputs ↔ - oa.somePathSatisfies queryPred - (fun x => (ob x).somePathSatisfies queryPred outputPred possibleOutputs) - possibleOutputs := by - induction oa using OracleComp.inductionOn <;> - simp [monad_norm, OracleComp.somePathSatisfies_query_bind, *] + somePathSatisfies queryPred outputPred possibleOutputs (oa >>= ob) ↔ + somePathSatisfies queryPred + (fun x => somePathSatisfies queryPred outputPred possibleOutputs (ob x)) + possibleOutputs oa := by + induction oa using OracleComp.inductionOn with + | pure x => simp [pure_bind] + | query_bind q oa ih => simp [monad_norm, OracleComp.somePathSatisfies_query_bind, ih] /-- Output-only specialization of [`OracleComp.allPathsSatisfy_bind_iff`]. -/ @[simp] diff --git a/VCVio/ProgramLogic/Tactics/Common/Core.lean b/VCVio/ProgramLogic/Tactics/Common/Core.lean index 533456128..79804bf49 100644 --- a/VCVio/ProgramLogic/Tactics/Common/Core.lean +++ b/VCVio/ProgramLogic/Tactics/Common/Core.lean @@ -6,6 +6,7 @@ Authors: Quang Dao import Lean.Elab.Tactic.Basic import Lean.Meta.Match.MatcherApp +import Lean.Meta.Sym.Pattern import VCVio.OracleComp.Constructions.Replicate import VCVio.ProgramLogic.NotationCore @@ -257,6 +258,16 @@ def renderPassReplayLine (steps : Array PlannedStep) : Option String := def whnfReducible (e : Expr) : MetaM Expr := withReducible <| whnf e +/-- Normalize a goal-side computation the same way `Sym.mkPatternFromDeclWithKey` +normalizes rule statements (`Sym.preprocessType`: unfold reducible definitions, +then beta/zeta/eta reduce). `Sym.DiscrTree.getMatch` is purely structural, so +query keys must agree with the pattern keys computed at registration time. +`OracleComp` is reducible over `PFunctor.FreeM`, so an unnormalized query +diverges from the stored patterns at the monad argument of `Bind.bind` and +friends, and every registry lookup silently returns no candidates. -/ +def symMatchKey (e : Expr) : MetaM Expr := do + Lean.Meta.Sym.preprocessType (← instantiateMVars e) + def headConstName? (e : Expr) : Option Name := e.consumeMData.getAppFn.constName? diff --git a/VCVio/ProgramLogic/Tactics/Common/Registry.lean b/VCVio/ProgramLogic/Tactics/Common/Registry.lean index 898b2d001..dd9a25b7f 100644 --- a/VCVio/ProgramLogic/Tactics/Common/Registry.lean +++ b/VCVio/ProgramLogic/Tactics/Common/Registry.lean @@ -447,6 +447,7 @@ private def headOfWhnf (e : Expr) : MetaM (Option Name) := do `whnf`-free counterpart is `getRegisteredUnaryVCSpecEntriesNoWhnf`. -/ def getRegisteredUnaryVCSpecEntries (comp : Expr) : MetaM (Array VCSpecEntry) := do let comp ← whnfReducible (← instantiateMVars comp) + let comp ← symMatchKey comp let registry := vcSpecRegistry.getState (← getEnv) return Lean.Meta.Sym.getMatch registry.unary comp @@ -456,7 +457,7 @@ This is only for raw `wp` structural dispatch, where the syntactic head is alrea the surface we want to step and reducing zero/nil iterator terms can unfold into larger monadic expressions. -/ def getRegisteredUnaryVCSpecEntriesNoWhnf (comp : Expr) : MetaM (Array VCSpecEntry) := do - let comp ← instantiateMVars comp + let comp ← symMatchKey comp let registry := vcSpecRegistry.getState (← getEnv) return Lean.Meta.Sym.getMatch registry.unary comp @@ -464,7 +465,7 @@ def getRegisteredUnaryVCSpecEntriesNoWhnf (comp : Expr) : MetaM (Array VCSpecEnt and whose `rightHead?` equals the head constant of the right computation `ob`, queried from the `relational` discrimination tree after reducing `oa` with reducible `whnf`. -/ def getRegisteredRelationalVCSpecEntries (oa ob : Expr) : MetaM (Array VCSpecEntry) := do - let oa ← whnfReducible (← instantiateMVars oa) + let oa ← symMatchKey (← whnfReducible (← instantiateMVars oa)) let some rightHead ← headOfWhnf ob | return #[] let registry := vcSpecRegistry.getState (← getEnv) let candidates := Lean.Meta.Sym.getMatch registry.relational oa diff --git a/VCVio/ProgramLogic/Tactics/Common/WpStepRegistry.lean b/VCVio/ProgramLogic/Tactics/Common/WpStepRegistry.lean index 5c61577ab..f11e86103 100644 --- a/VCVio/ProgramLogic/Tactics/Common/WpStepRegistry.lean +++ b/VCVio/ProgramLogic/Tactics/Common/WpStepRegistry.lean @@ -177,6 +177,7 @@ tries each rewrite, so over-approximation here is harmless. -/ def getRegisteredWpStepEntries (oa : Expr) : MetaM (Array WpStepEntry) := do let oa ← instantiateMVars oa let oa ← withReducible <| whnf oa + let oa ← symMatchKey oa let registry := wpStepRegistry.getState (← getEnv) return Lean.Meta.Sym.getMatch registry.compTree oa @@ -186,7 +187,7 @@ Raw `wp` dispatch uses this as the first pass so syntactic zero/nil iterator redexes are offered to their exact rewrite rules before normalized fallback candidates such as successor/cons unfoldings. -/ def getRegisteredWpStepEntriesNoWhnf (oa : Expr) : MetaM (Array WpStepEntry) := do - let oa ← instantiateMVars oa + let oa ← symMatchKey oa let registry := wpStepRegistry.getState (← getEnv) return Lean.Meta.Sym.getMatch registry.compTree oa diff --git a/VCVio/StateSeparating/CellRef.lean b/VCVio/StateSeparating/CellRef.lean index 971751d84..ba8654fbb 100644 --- a/VCVio/StateSeparating/CellRef.lean +++ b/VCVio/StateSeparating/CellRef.lean @@ -787,7 +787,7 @@ theorem simulateQ_run_cellPreserved simpa [simulateQ_bind, OracleComp.liftM_def] using hz rcases (mem_support_bind_iff _ _ _).1 hz' with ⟨us, hus, hzcont⟩ refine (ih us.1 us.2 z hzcont).trans (himpl t h us ?_) - simpa [OracleSpec.query_def, simulateQ_spec_query] using hus + simpa [simulateQ_spec_query] using hus end OracleComp diff --git a/docs/agents/gotchas.md b/docs/agents/gotchas.md index bda4aa07a..36dd5ccbd 100644 --- a/docs/agents/gotchas.md +++ b/docs/agents/gotchas.md @@ -41,7 +41,14 @@ The bare `query` identifier is the `export`ed `HasQuery.query`, so writing `quer ### 7. Core types are `@[reducible]` thin wrappers -`OracleSpec`, `QueryImpl`, and `OracleComp` are all `def`/`abbrev`/`@[reducible]` over `PFunctor` machinery. Lean may unfold them aggressively. Use `OracleComp.inductionOn` / `OracleComp.construct` as canonical eliminators rather than pattern matching on `PFunctor.FreeM.pure`/`roll`. +`OracleSpec`, `QueryImpl`, `OracleComp`, `OracleQuery`, and `OracleSpec.toPFunctor` are all `def`/`abbrev`/`@[reducible]` over `PFunctor` machinery, and the `Monad`/`Functor` instances come directly from `PFunctor.FreeM`/`PFunctor.Obj`. Lean may unfold them aggressively. Use `OracleComp.inductionOn` / `OracleComp.construct` as canonical eliminators rather than pattern matching on `PFunctor.FreeM.pure`/`roll`. + +Two failure modes to recognize under this regime: + +- **Dot notation on monadic results fails.** The inferred type of `oa >>= ob` or `liftM (query t)` has head `PFunctor.FreeM`, not `OracleComp`, so `(query t >>= oa).myOracleCompLemma` reports `Invalid field … PFunctor.FreeM.myOracleCompLemma`. State such lemmas in prefix form (`myOracleCompLemma … (query t >>= oa)`); dot notation on plain variables of ascribed type `OracleComp spec α` still works. +- **Never `attribute [local reducible]` a definition that instance keys mention.** Instance discrimination-tree keys are computed at declaration site; changing transparency locally makes queries normalize differently and instances like `MonadLiftT (OracleComp spec) SetM` silently vanish (`support`, `evalDist`, `Pr[…]` all stop elaborating). `toPFunctor` is globally reducible for exactly this consistency reason. + +Relatedly, `OracleSpec.toPFunctor_add` is deliberately **not** `@[simp]`: `toPFunctor` occurs inside the instance-carrying type of an `OracleComp`, and rewriting `(spec + spec').toPFunctor` under a `simulateQ`/`liftM` strands goals in a form the `simulateQ_query` family can no longer match (typically visible as `simulateQ impl (liftM (query (Sum.inl t)))` refusing to simplify). ### 8. Universe polymorphism diff --git a/docs/agents/program-logic.md b/docs/agents/program-logic.md index 66ff699d7..0710967ae 100644 --- a/docs/agents/program-logic.md +++ b/docs/agents/program-logic.md @@ -563,6 +563,18 @@ same pattern preprocessing and lookup cost profile as future core tactics, and the migration to `Sym.Simp.*`-driven rewriting is a localised follow-up in two registry files rather than a framework rewrite. +**Key alignment invariant**: `Sym.DiscrTree.getMatch` is purely structural, so +goal-side query terms must be normalized with the *same* preprocessing the +pattern side gets at registration time. All registry query functions therefore +route the extracted computation through `symMatchKey` +(`Tactics/Common/Core.lean`), which applies `Sym.preprocessType` +(unfold-reducible + beta/zeta/eta). This matters because `OracleComp` is a +reducible alias of `PFunctor.FreeM`: the stored patterns carry unfolded +`FreeM`-form keys at the monad argument of `Bind.bind` and friends, and an +unnormalized query key diverges there, making every lookup silently return no +candidates (symptom: `vcstep` reports "no matching rule applied" on plain +`pure`/`>>=` goals while manual `rw [wp_pure]`/`rw [wp_bind]` works). + ### Registries and what they index | File | Attribute | Role | From 5d75264422f7f8e5aed0fd967ec5388ba3abc957 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Thu, 16 Jul 2026 18:34:59 +0530 Subject: [PATCH 2/6] Consume generic PolyFun traversal predicates (#491) * refactor(OracleComp): consume generic PolyFun traversal predicates * chore: pin merged PolyFun traversal API --- VCVio/OracleComp/OracleSpec.lean | 2 +- VCVio/OracleComp/Traversal.lean | 90 +++++---------------- VCVio/ProgramLogic/Tactics/Common/Core.lean | 28 +++++-- lake-manifest.json | 4 +- lakefile.lean | 2 +- 5 files changed, 45 insertions(+), 81 deletions(-) diff --git a/VCVio/OracleComp/OracleSpec.lean b/VCVio/OracleComp/OracleSpec.lean index 1806dc72d..a9b8f87f4 100644 --- a/VCVio/OracleComp/OracleSpec.lean +++ b/VCVio/OracleComp/OracleSpec.lean @@ -30,7 +30,7 @@ namespace OracleSpec variable {ι : Type u} @[reducible] -def toPFunctor (spec : OracleSpec ι) : PFunctor := { A := ι, B := spec } +def toPFunctor (spec : OracleSpec ι) : PFunctor := PFunctor.ofFamily spec @[reducible, inline] def ofPFunctor (P : PFunctor) : OracleSpec P.A := P.B diff --git a/VCVio/OracleComp/Traversal.lean b/VCVio/OracleComp/Traversal.lean index 59c3c3b31..eef0ed1f7 100644 --- a/VCVio/OracleComp/Traversal.lean +++ b/VCVio/OracleComp/Traversal.lean @@ -14,11 +14,11 @@ This file defines structural predicates for checking whether all or some reachab possible oracle outputs. The predicates are phrased in terms of `PFunctor.FreeM.Cursor`: a cursor is a typed path prefix -into the underlying free-monad tree, so quantifying over cursors whose recorded answers stay +into the underlying free-monad tree, so quantifying over cursors whose recorded directions stay within the possible outputs simultaneously reaches every demanded query node (via non-terminal -cursors) and every reachable final output (via terminal cursors). Two generic helpers, -`PFunctor.TraceList.WithinOn` and `PFunctor.FreeM.Cursor.Sat`, express the answer-membership -filter and the per-cursor demand. +cursors) and every reachable final output (via terminal cursors). The generic PolyFun predicates +`PFunctor.TraceList.DirectionsWithin` and `PFunctor.FreeM.RootSatisfies` express the trace filter +and the demand made by the selected residual root. It also connects those structural predicates to the denotational set `supportWhen`, so proofs can move cleanly between the syntax-level traversal view and the reachable-output view. @@ -26,60 +26,10 @@ move cleanly between the syntax-level traversal view and the reachable-output vi open OracleSpec -universe u v w +universe u v open scoped OracleSpec.PrimitiveQuery -namespace PFunctor - -variable {P : PFunctor.{u, v}} {α : Type w} - -namespace TraceList - -/-- Every event recorded on a trace answers within the allowed fibers. -Generic over the polynomial `P`; a candidate for upstreaming into `PolyFun`. -/ -def WithinOn (allowed : (a : P.A) → Set (P.B a)) (events : PFunctor.TraceList P) : Prop := - ∀ e ∈ events, e.2 ∈ allowed e.1 - -@[simp] lemma withinOn_nil (allowed : (a : P.A) → Set (P.B a)) : - WithinOn allowed ([] : PFunctor.TraceList P) := - fun _ he => absurd he (List.not_mem_nil) - -@[simp] lemma withinOn_cons (allowed : (a : P.A) → Set (P.B a)) - (e : P.Idx) (es : PFunctor.TraceList P) : - WithinOn allowed (e :: es) ↔ e.2 ∈ allowed e.1 ∧ WithinOn allowed es := - List.forall_mem_cons - -end TraceList - -namespace FreeM.Cursor - -/-- The demand a cursor places on a pair of predicates: a cursor selecting a leaf demands the -leaf predicate on its payload, while a cursor selecting an internal query node demands the node -predicate on its label. Generic over the polynomial `P`; a candidate for upstreaming into -`PolyFun`. -/ -def Sat (nodePred : P.A → Prop) (leafPred : α → Prop) - {program : PFunctor.FreeM P α} (c : PFunctor.FreeM.Cursor program) : Prop := - match c.residual with - | .pure x => leafPred x - | .liftBind a _ => nodePred a - -@[simp] lemma sat_root_pure (nodePred : P.A → Prop) (leafPred : α → Prop) (x : α) : - Sat nodePred leafPred (root (.pure x : PFunctor.FreeM P α)) = leafPred x := rfl - -@[simp] lemma sat_root_liftBind (nodePred : P.A → Prop) (leafPred : α → Prop) - (a : P.A) (next : P.B a → PFunctor.FreeM P α) : - Sat nodePred leafPred (root (.liftBind a next)) = nodePred a := rfl - -@[simp] lemma sat_down (nodePred : P.A → Prop) (leafPred : α → Prop) - {a : P.A} {next : P.B a → PFunctor.FreeM P α} - (answer : P.B a) (tail : PFunctor.FreeM.Cursor (next answer)) : - Sat nodePred leafPred (down answer tail) = Sat nodePred leafPred tail := rfl - -end FreeM.Cursor - -end PFunctor - namespace OracleComp open PFunctor @@ -89,26 +39,28 @@ variable {ι : Type u} {spec : OracleSpec.{u, v} ι} {α β γ : Type v} /-- Given that oracle outputs are bounded by `possibleOutputs`, every reachable query input in the computation satisfies `queryPred`, and every reachable pure output satisfies `outputPred`. -Phrased as: every cursor into the computation whose recorded answers stay within -`possibleOutputs` satisfies its demand (`PFunctor.FreeM.Cursor.Sat`). Non-terminal cursors +Phrased as: every cursor into the computation whose recorded directions stay within +`possibleOutputs` satisfies its root demand (`PFunctor.FreeM.RootSatisfies`). Non-terminal cursors reach every demanded query node — including nodes with no possible continuation below them — while terminal cursors reach every possible final output. -/ def allPathsSatisfy (queryPred : spec.Domain → Prop) (outputPred : α → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) : Prop := ∀ c : PFunctor.FreeM.Cursor oa, - TraceList.WithinOn possibleOutputs c.trace → FreeM.Cursor.Sat queryPred outputPred c + TraceList.DirectionsWithin possibleOutputs c.trace → + FreeM.RootSatisfies queryPred outputPred c.residual /-- Given that oracle outputs are bounded by `possibleOutputs`, some reachable query input in the computation satisfies `queryPred`, or some reachable pure output satisfies `outputPred`. -Phrased as: some cursor into the computation whose recorded answers stay within -`possibleOutputs` satisfies its demand (`PFunctor.FreeM.Cursor.Sat`). -/ +Phrased as: some cursor into the computation whose recorded directions stay within +`possibleOutputs` satisfies its root demand (`PFunctor.FreeM.RootSatisfies`). -/ def somePathSatisfies (queryPred : spec.Domain → Prop) (outputPred : α → Prop) (possibleOutputs : (x : spec.Domain) → Set (spec.Range x)) (oa : OracleComp spec α) : Prop := ∃ c : PFunctor.FreeM.Cursor oa, - TraceList.WithinOn possibleOutputs c.trace ∧ FreeM.Cursor.Sat queryPred outputPred c + TraceList.DirectionsWithin possibleOutputs c.trace ∧ + FreeM.RootSatisfies queryPred outputPred c.residual /-- Output-only view of [`OracleComp.allPathsSatisfy`]: every output reachable under `possibleOutputs` satisfies `outputPred`. -/ @@ -159,15 +111,16 @@ lemma allPathsSatisfy_query_bind (q : spec.Domain) · intro h refine ⟨h (PFunctor.FreeM.Cursor.root _) (by simp), fun u hu c hc => ?_⟩ exact h (PFunctor.FreeM.Cursor.down u c) - (by simp only [PFunctor.FreeM.Cursor.trace_down, TraceList.withinOn_cons]; exact ⟨hu, hc⟩) + (by + simp only [PFunctor.FreeM.Cursor.trace_down, TraceList.directionsWithin_cons] + exact ⟨hu, hc⟩) · rintro ⟨hq, h⟩ ⟨res, sp⟩ hw cases sp with | root => exact hq | down answer tail => simp only [show (⟨res, PFunctor.FreeM.Cursor.Spine.down answer tail⟩ : - PFunctor.FreeM.Cursor _) = PFunctor.FreeM.Cursor.down answer ⟨res, tail⟩ from rfl, - PFunctor.FreeM.Cursor.trace_down, TraceList.withinOn_cons, - FreeM.Cursor.sat_down] at hw ⊢ + PFunctor.FreeM.Cursor _) = PFunctor.FreeM.Cursor.down answer ⟨res, tail⟩ from rfl, + PFunctor.FreeM.Cursor.trace_down, TraceList.directionsWithin_cons] at hw ⊢ exact h answer hw.1 ⟨res, tail⟩ hw.2 @[simp] @@ -186,14 +139,13 @@ lemma somePathSatisfies_query_bind (q : spec.Domain) | root => exact Or.inl hc | down answer tail => simp only [show (⟨res, PFunctor.FreeM.Cursor.Spine.down answer tail⟩ : - PFunctor.FreeM.Cursor _) = PFunctor.FreeM.Cursor.down answer ⟨res, tail⟩ from rfl, - PFunctor.FreeM.Cursor.trace_down, TraceList.withinOn_cons, - FreeM.Cursor.sat_down] at hw hc + PFunctor.FreeM.Cursor _) = PFunctor.FreeM.Cursor.down answer ⟨res, tail⟩ from rfl, + PFunctor.FreeM.Cursor.trace_down, TraceList.directionsWithin_cons] at hw hc exact Or.inr ⟨answer, hw.1, ⟨res, tail⟩, hw.2, hc⟩ · rintro (hq | ⟨u, hu, c, hw, hc⟩) · exact ⟨PFunctor.FreeM.Cursor.root _, by simp, hq⟩ · refine ⟨PFunctor.FreeM.Cursor.down u c, ?_, hc⟩ - simp only [PFunctor.FreeM.Cursor.trace_down, TraceList.withinOn_cons] + simp only [PFunctor.FreeM.Cursor.trace_down, TraceList.directionsWithin_cons] exact ⟨hu, hw⟩ /-- Every output of `oa` reachable under `possibleOutputs` satisfies `outputPred` exactly when diff --git a/VCVio/ProgramLogic/Tactics/Common/Core.lean b/VCVio/ProgramLogic/Tactics/Common/Core.lean index 79804bf49..b8c958e76 100644 --- a/VCVio/ProgramLogic/Tactics/Common/Core.lean +++ b/VCVio/ProgramLogic/Tactics/Common/Core.lean @@ -258,15 +258,27 @@ def renderPassReplayLine (steps : Array PlannedStep) : Option String := def whnfReducible (e : Expr) : MetaM Expr := withReducible <| whnf e -/-- Normalize a goal-side computation the same way `Sym.mkPatternFromDeclWithKey` -normalizes rule statements (`Sym.preprocessType`: unfold reducible definitions, -then beta/zeta/eta reduce). `Sym.DiscrTree.getMatch` is purely structural, so -query keys must agree with the pattern keys computed at registration time. -`OracleComp` is reducible over `PFunctor.FreeM`, so an unnormalized query -diverges from the stored patterns at the monad argument of `Bind.bind` and -friends, and every registry lookup silently returns no candidates. -/ +/-- Normalize the reducible oracle wrappers in a goal-side computation so its +key agrees with the patterns produced by `Sym.mkPatternFromDeclWithKey`. +`Sym.DiscrTree.getMatch` is purely structural, and those stored patterns unfold +`OracleComp`, `OracleQuery`, `OracleSpec.toPFunctor`, and the generic +`PFunctor.ofFamily` constructor used by the latter. + +Do not use the more general `Sym.preprocessType` here. Besides being intended +for declaration types rather than terms, in Lean 4.32 it also unfolds reducible +user programs. A program containing a matcher can then make later +definitional equality reduce a matcher with loose de Bruijn variables and +panic in `whnfEasyCases`. The wrappers below are the only newly +reducible declarations whose shapes registry lookup needs to expose. -/ def symMatchKey (e : Expr) : MetaM Expr := do - Lean.Meta.Sym.preprocessType (← instantiateMVars e) + let e ← instantiateMVars e + Meta.transform e (pre := fun e => do + let some declName := e.getAppFn.constName? | return .continue + unless declName == ``OracleComp || declName == ``OracleQuery || + declName == ``OracleSpec.toPFunctor || declName == ``PFunctor.ofFamily do + return .continue + let some value ← unfoldDefinition? e | return .continue + return .visit value) def headConstName? (e : Expr) : Option Name := e.consumeMData.getAppFn.constName? diff --git a/lake-manifest.json b/lake-manifest.json index 599bf33b2..7f97f8bf4 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "97a262ce2ba7513448b76635e1f6a07f61f40de5", + "rev": "a65a9ab83ad42034229d379940bbeed2f44831df", "name": "PolyFun", "manifestFile": "lake-manifest.json", - "inputRev": "97a262ce2ba7513448b76635e1f6a07f61f40de5", + "inputRev": "a65a9ab83ad42034229d379940bbeed2f44831df", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", diff --git a/lakefile.lean b/lakefile.lean index 46e24fe21..144d09546 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -58,7 +58,7 @@ require "leanprover-community" / "mathlib" @ git "v4.32.0" require PolyFun from git "https://github.com/Verified-zkEVM/PolyFun.git" @ - "97a262ce2ba7513448b76635e1f6a07f61f40de5" + "a65a9ab83ad42034229d379940bbeed2f44831df" /-- Main library. -/ @[default_target] lean_lib VCVio From 874ef0006cfc3e6358eb898e48e6d02471886494 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Fri, 17 Jul 2026 16:23:37 +0530 Subject: [PATCH 3/6] refactor(OracleSpec): use PFunctor.mk directly (#493) --- VCVio/OracleComp/OracleSpec.lean | 2 +- VCVio/ProgramLogic/Tactics/Common/Core.lean | 6 +++--- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/VCVio/OracleComp/OracleSpec.lean b/VCVio/OracleComp/OracleSpec.lean index a9b8f87f4..45c5c822b 100644 --- a/VCVio/OracleComp/OracleSpec.lean +++ b/VCVio/OracleComp/OracleSpec.lean @@ -30,7 +30,7 @@ namespace OracleSpec variable {ι : Type u} @[reducible] -def toPFunctor (spec : OracleSpec ι) : PFunctor := PFunctor.ofFamily spec +def toPFunctor (spec : OracleSpec ι) : PFunctor := PFunctor.mk ι spec @[reducible, inline] def ofPFunctor (P : PFunctor) : OracleSpec P.A := P.B diff --git a/VCVio/ProgramLogic/Tactics/Common/Core.lean b/VCVio/ProgramLogic/Tactics/Common/Core.lean index b8c958e76..9add2b5f9 100644 --- a/VCVio/ProgramLogic/Tactics/Common/Core.lean +++ b/VCVio/ProgramLogic/Tactics/Common/Core.lean @@ -261,8 +261,8 @@ def whnfReducible (e : Expr) : MetaM Expr := /-- Normalize the reducible oracle wrappers in a goal-side computation so its key agrees with the patterns produced by `Sym.mkPatternFromDeclWithKey`. `Sym.DiscrTree.getMatch` is purely structural, and those stored patterns unfold -`OracleComp`, `OracleQuery`, `OracleSpec.toPFunctor`, and the generic -`PFunctor.ofFamily` constructor used by the latter. +`OracleComp`, `OracleQuery`, and `OracleSpec.toPFunctor` to the underlying +structure constructor. Do not use the more general `Sym.preprocessType` here. Besides being intended for declaration types rather than terms, in Lean 4.32 it also unfolds reducible @@ -275,7 +275,7 @@ def symMatchKey (e : Expr) : MetaM Expr := do Meta.transform e (pre := fun e => do let some declName := e.getAppFn.constName? | return .continue unless declName == ``OracleComp || declName == ``OracleQuery || - declName == ``OracleSpec.toPFunctor || declName == ``PFunctor.ofFamily do + declName == ``OracleSpec.toPFunctor do return .continue let some value ← unfoldDefinition? e | return .continue return .visit value) diff --git a/lake-manifest.json b/lake-manifest.json index 7f97f8bf4..3ddc7eb80 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "a65a9ab83ad42034229d379940bbeed2f44831df", + "rev": "1f7f477c9701f7606841bb1638dcffb9b2359d62", "name": "PolyFun", "manifestFile": "lake-manifest.json", - "inputRev": "a65a9ab83ad42034229d379940bbeed2f44831df", + "inputRev": "1f7f477c9701f7606841bb1638dcffb9b2359d62", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", diff --git a/lakefile.lean b/lakefile.lean index 144d09546..f1778920c 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -58,7 +58,7 @@ require "leanprover-community" / "mathlib" @ git "v4.32.0" require PolyFun from git "https://github.com/Verified-zkEVM/PolyFun.git" @ - "a65a9ab83ad42034229d379940bbeed2f44831df" + "1f7f477c9701f7606841bb1638dcffb9b2359d62" /-- Main library. -/ @[default_target] lean_lib VCVio From 8622511d228d53257981aa960fb572fbcaf85b4d Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Wed, 22 Jul 2026 18:10:30 +0530 Subject: [PATCH 4/6] refactor: align VCVio with merged PolyFun APIs --- Examples/OneTimePad/UC.lean | 52 +++++++++---------- VCVio/Interaction/UC/AsyncRuntime.lean | 24 ++++----- VCVio/Interaction/UC/AsyncSecurity.lean | 32 ++++++------ VCVio/Interaction/UC/Runtime.lean | 41 +++++++-------- VCVio/Interaction/UC/StdDoBridge.lean | 51 +++++++++--------- .../SimSemantics/QueryImpl/Basic.lean | 16 ++++-- .../SimSemantics/StateT/StateSeparating.lean | 17 +++++- docs/agents/oracle-comp.md | 9 +++- docs/agents/program-logic.md | 21 ++++---- lake-manifest.json | 4 +- lakefile.lean | 2 +- 11 files changed, 149 insertions(+), 120 deletions(-) diff --git a/Examples/OneTimePad/UC.lean b/Examples/OneTimePad/UC.lean index f5196f21e..2909cf9a4 100644 --- a/Examples/OneTimePad/UC.lean +++ b/Examples/OneTimePad/UC.lean @@ -266,7 +266,7 @@ noncomputable def msgClosed (sp : ℕ) (msg : BitVec sp) : T.Closed where Proc := BitVec sp step := fun _ => - { spec := .done + { tree := .done semantics := ⟨⟩ next := fun _ => msg } stepSampler := fun _ => ⟨⟩ @@ -451,19 +451,19 @@ def Δ_otp (sp : ℕ) : PortBoundary where In := Interface.sum (bvInInterface sp) (bvInInterface sp) Out := bvOutInterface sp -/-- The single-round interaction spec at the core of both real and +/-- The single-round interaction tree at the core of both real and ideal OTP processes: one node samples a `BitVec sp` (the key for the real world, the ciphertext for the ideal world), then terminates. -/ -abbrev otpSpec (sp : ℕ) : Interaction.Spec.{0} := - Spec.node (BitVec sp) (fun _ => Spec.done) +abbrev otpTree (sp : ℕ) : Interaction.TypeTree.{0} := + TypeTree.node (BitVec sp) (fun _ => TypeTree.done) -/-- The canonical uniform `ProbComp`-sampler for `otpSpec sp`, -synthesized from the `Spec.Fintype (otpSpec sp)` instance built by +/-- The canonical uniform `ProbComp`-sampler for `otpTree sp`, +synthesized from the `TypeTree.Fintype (otpTree sp)` instance built by typeclass synthesis from `Fintype (BitVec sp)` and `Nonempty (BitVec sp)`. -/ noncomputable def uniformOtpSampler (sp : ℕ) : - Spec.Sampler ProbComp (otpSpec sp) := - Spec.Sampler.uniformI _ + TypeTree.Sampler ProbComp (otpTree sp) := + TypeTree.Sampler.uniformI _ /-- Lift a `ProbComp`-valued sampler to an `OptionT ProbComp`-valued one by applying `liftM : ProbComp X → OptionT ProbComp X` at every @@ -472,10 +472,10 @@ node of the spec tree via `Decoration.map`. This is how we thread a real uniform sampler through an open process whose surface monad is `OptionT ProbComp` (the observation monad used by the bundled `UC.Semantics` above). -/ -noncomputable def liftSamplerToOptionT {spec : Interaction.Spec.{0}} - (s : Spec.Sampler ProbComp spec) : - Spec.Sampler (OptionT ProbComp) spec := - PFunctor.FreeM.Displayed.Decoration.map +noncomputable def liftSamplerToOptionT {spec : Interaction.TypeTree.{0}} + (s : TypeTree.Sampler ProbComp spec) : + TypeTree.Sampler (OptionT ProbComp) spec := + TypeTree.Decoration.map (Γ := fun X => ProbComp X) (Δ := fun X => OptionT ProbComp X) (fun _ (x : ProbComp _) => (liftM x : OptionT ProbComp _)) spec s @@ -484,13 +484,13 @@ by lifting `uniformOtpSampler`. Both `realOtp` and `idealOtp` thread this same sampler, so their distributional content lives in the boundary emission, not in the sampler. -/ noncomputable def otpStepSampler (sp : ℕ) : - Spec.Sampler (OptionT ProbComp) (otpSpec sp) := + TypeTree.Sampler (OptionT ProbComp) (otpTree sp) := liftSamplerToOptionT (uniformOtpSampler sp) /-! ### Boundary emissions: real vs ideal -/ /-- Real-world boundary emission. On the unique sample node of -`otpSpec sp`, when the sampler produces `k : BitVec sp`, emit one +`otpTree sp`, when the sampler produces `k : BitVec sp`, emit one packet on the single output port of `Δ_otp sp` carrying the ciphertext `k ⊕ msg`. -/ def realEmit (sp : ℕ) (msg : BitVec sp) : @@ -498,7 +498,7 @@ def realEmit (sp : ℕ) (msg : BitVec sp) : fun k => [⟨(), k ^^^ msg⟩] /-- Ideal-world boundary emission. On the unique sample node of -`otpSpec sp`, when the sampler produces `c : BitVec sp`, emit it +`otpTree sp`, when the sampler produces `c : BitVec sp`, emit it verbatim on the single output port of `Δ_otp sp`. Under the uniform sampler this is already the correct distribution @@ -509,7 +509,7 @@ def idealEmit (sp : ℕ) : PFunctor.Trace (Δ_otp sp).Out (BitVec sp) := fun c => [⟨(), c⟩] -/-- The open-node context at the unique sample node of `otpSpec sp`: +/-- The open-node context at the unique sample node of `otpTree sp`: trivial controllers and views, and the given boundary emission action. -/ def otpOpenNode (sp : ℕ) @@ -522,11 +522,11 @@ def otpOpenNode (sp : ℕ) { isActivated := false emit := emit } -/-- Decoration for `otpSpec sp` bundling a single `otpOpenNode` at the +/-- Decoration for `otpTree sp` bundling a single `otpOpenNode` at the root and the trivial `PUnit` decoration at the terminal leaf. -/ def otpDecoration (sp : ℕ) (emit : PFunctor.Trace (Δ_otp sp).Out (BitVec sp)) : - PFunctor.FreeM.Displayed.Decoration (UC.OpenNodeContext Party (Δ_otp sp)) (otpSpec sp) := + TypeTree.Decoration (UC.OpenNodeContext Party (Δ_otp sp)) (otpTree sp) := ⟨otpOpenNode sp emit, fun _ => ⟨⟩⟩ /-! ### Real and ideal open processes -/ @@ -534,14 +534,14 @@ def otpDecoration (sp : ℕ) /-- **Real-world OTP open process** at `Δ_otp sp`. State space `Unit` (single-round, one-shot). Every step runs the -single-sample `otpSpec sp`, emitting the ciphertext `k ⊕ msg` on the +single-sample `otpTree sp`, emitting the ciphertext `k ⊕ msg` on the output port via `realEmit`, with the uniform sampler threaded through `otpStepSampler`. -/ noncomputable def realOtp (sp : ℕ) (msg : BitVec sp) : T.Obj (Δ_otp sp) where Proc := Unit step := fun _ => - { spec := otpSpec sp + { tree := otpTree sp semantics := otpDecoration sp (realEmit sp msg) next := fun _ => () } stepSampler := fun _ => otpStepSampler sp @@ -559,7 +559,7 @@ collapses the two bundled `SPMF Unit` observations. -/ noncomputable def idealOtp (sp : ℕ) : T.Obj (Δ_otp sp) where Proc := Unit step := fun _ => - { spec := otpSpec sp + { tree := otpTree sp semantics := otpDecoration sp (idealEmit sp) next := fun _ => () } stepSampler := fun _ => otpStepSampler sp @@ -571,7 +571,7 @@ one-step transcript as the emitted ciphertext packet. -/ @[simp] theorem realOtp_boundaryTrace (sp : ℕ) (msg k : BitVec sp) : Interaction.UC.OpenStep.boundaryTrace ((realOtp sp msg).step ()) - (⟨k, ⟨⟩⟩ : Spec.Transcript (otpSpec sp)) = + (⟨k, ⟨⟩⟩ : TypeTree.Path (otpTree sp)) = [(⟨(), k ^^^ msg⟩ : Σ _ : Unit, BitVec sp)] := by rfl @@ -580,13 +580,13 @@ one-step transcript as the emitted uniform ciphertext packet. -/ @[simp] theorem idealOtp_boundaryTrace (sp : ℕ) (c : BitVec sp) : Interaction.UC.OpenStep.boundaryTrace ((idealOtp sp).step ()) - (⟨c, ⟨⟩⟩ : Spec.Transcript (otpSpec sp)) = + (⟨c, ⟨⟩⟩ : TypeTree.Path (otpTree sp)) = [(⟨(), c⟩ : Σ _ : Unit, BitVec sp)] := by rfl /-- For any nonzero plaintext `msg`, the real and ideal OTP open processes at `Δ_otp sp` are not equal: they agree on `Proc`, -`step.spec`, `step.next`, and `stepSampler`, but their +`step.tree`, `step.next`, and `stepSampler`, but their `step.semantics`'s boundary emissions disagree on the all-zero key (`0#sp ^^^ msg = msg ≠ 0#sp`). -/ theorem realOtp_ne_idealOtp (sp : ℕ) {msg : BitVec sp} @@ -599,11 +599,11 @@ theorem realOtp_ne_idealOtp (sp : ℕ) {msg : BitVec sp} eq_of_heq hstep have hstep0 := congrFun hstep' () change - ({ spec := otpSpec sp, + ({ tree := otpTree sp, semantics := otpDecoration sp (realEmit sp msg), next := fun _ => () } : Concurrent.StepOver (UC.OpenNodeContext Party (Δ_otp sp)) Unit) = - { spec := otpSpec sp, + { tree := otpTree sp, semantics := otpDecoration sp (idealEmit sp), next := fun _ => () } at hstep0 injection hstep0 with _ hsem _ diff --git a/VCVio/Interaction/UC/AsyncRuntime.lean b/VCVio/Interaction/UC/AsyncRuntime.lean index 0a24a56f0..4c31dc5a1 100644 --- a/VCVio/Interaction/UC/AsyncRuntime.lean +++ b/VCVio/Interaction/UC/AsyncRuntime.lean @@ -35,7 +35,7 @@ developments will reach for. bookkeeping state. * `ProcessScheduler` / `EnvScheduler` — the two sibling samplers driving the async runtime. The process scheduler reuses the existing - `Spec.Sampler m` from `Runtime.lean`; the env scheduler is a separate + `TypeTree.Sampler m` from `Runtime.lean`; the env scheduler is a separate monadic choice over `RuntimeEvent`. * `Concurrent.runStepsAsync` — the recursive engine. Mirrors `Concurrent.ProcessOver.runSteps` from `Runtime.lean`, with explicit @@ -71,12 +71,12 @@ namespace UC /-- One tick of the async runtime: either a process step (no payload, the -actual move is sampled inside the `Spec`-driven `procScheduler`) or an +actual move is sampled inside the `TypeTree`-driven `procScheduler`) or an environment event carrying its alphabet symbol. The sum is *non-symmetric* on purpose: `processTick` carries no payload because the move space at a process step is determined by the process's -`Spec`, not by the runtime trace; `envTick` carries the alphabet symbol +`TypeTree`, not by the runtime trace; `envTick` carries the alphabet symbol because the `EnvAction.react` reaction is keyed by the symbol. -/ inductive RuntimeEvent (Event : Type) where @@ -140,18 +140,18 @@ end AsyncRuntimeState /-! ## Schedulers -/ /-- -A process scheduler picks a process-side `Spec.Sampler` at each step, +A process scheduler picks a process-side `TypeTree.Sampler` at each step, parameterized by the joint async-runtime state. -The sampler-side type `Spec.Sampler m (specOf st)` is the existing one +The sampler-side type `TypeTree.Sampler m (specOf st)` is the existing one from `Runtime.lean`, unchanged. The extra `AsyncRuntimeState`-dependent argument lets a scheduler refuse to schedule, e.g., a corrupted machine's tick. -/ abbrev ProcessScheduler (m : Type → Type) (Proc : Type) (State : Type) - (specOf : AsyncRuntimeState Proc State → Spec.{0}) : Type := - ∀ st : AsyncRuntimeState Proc State, Spec.Sampler m (specOf st) + (specOf : AsyncRuntimeState Proc State → TypeTree.{0}) : Type := + ∀ st : AsyncRuntimeState Proc State, TypeTree.Sampler m (specOf st) /-- An env scheduler chooses the next runtime event in the monad `m`. @@ -203,18 +203,18 @@ Mirrors the recursion shape of `Concurrent.ProcessOver.runSteps` with explicit env-event interleaving. The env reaction lives in the same runtime monad `m` (`EnvAction.react : Event → State → m State`). The process sampler type is unchanged from the synchronous runtime: the -`ProcessScheduler` carries the existing `Spec.Sampler m` from +`ProcessScheduler` carries the existing `TypeTree.Sampler m` from `Runtime.lean`. -/ noncomputable def runStepsAsync {m : Type → Type} [Monad m] - {Γ : Spec.Node.Context} + {Γ : TypeTree.Node.Context} {State : Type} {Event : Type} {P : Type} (process : ProcessOver P Γ) (envAction : Interaction.UC.EnvAction m Event State) (procScheduler : Interaction.UC.ProcessScheduler m process.Proc State - (fun st => (process.step st.proc).spec)) + (fun st => (process.step st.proc).tree)) (envScheduler : Interaction.UC.EnvScheduler m process.Proc State Event) : ℕ → AsyncRuntimeState process.Proc State → @@ -249,9 +249,9 @@ trace bookkeeping pass, and is reused by -/ theorem runStepsAsync_empty_trivial_eq {m : Type → Type} [Monad m] [LawfulMonad m] - {Γ : Spec.Node.Context} {P : Type} + {Γ : TypeTree.Node.Context} {P : Type} (process : ProcessOver P Γ) - (sampler : (s : process.Proc) → Spec.Sampler m (process.step s).spec) + (sampler : (s : process.Proc) → TypeTree.Sampler m (process.step s).tree) (fuel : ℕ) (s : process.Proc) : runStepsAsync (m := m) process (Interaction.UC.EnvAction.empty Unit) (fun st => sampler st.proc) diff --git a/VCVio/Interaction/UC/AsyncSecurity.lean b/VCVio/Interaction/UC/AsyncSecurity.lean index 078492227..b7ee1f3d8 100644 --- a/VCVio/Interaction/UC/AsyncSecurity.lean +++ b/VCVio/Interaction/UC/AsyncSecurity.lean @@ -92,10 +92,10 @@ extensions that match `runStepsAsync`: * `state n` is the *joint* runtime state at step `n`, i.e. the residual process state plus the env-action bookkeeping state. * `event n` records which side fired at step `n`: a `processTick` - consumes the `procTranscript`, while an `envTick e` consumes the + consumes the `procPath`, while an `envTick e` consumes the `envSample`. * `next_state n` enforces the coherence law of one async step: at - process ticks the proc field advances by the chosen transcript; + process ticks the proc field advances by the chosen path; at env ticks the env state advances to the sampled new state. This is a freer object than the runtime's randomized executions @@ -106,33 +106,33 @@ runtime distribution, exactly as `ProcessOver.Run`. -/ structure AsyncRun - {Γ : Spec.Node.Context} {m : Type → Type} [Pure m] {State Event P : Type} + {Γ : TypeTree.Node.Context} {m : Type → Type} [Pure m] {State Event P : Type} (process : Concurrent.ProcessOver P Γ) (envAction : EnvAction m Event State) where /-- The joint runtime state at each step. -/ state : ℕ → AsyncRuntimeState process.Proc State /-- The runtime event chosen at each step. -/ event : ℕ → RuntimeEvent Event - /-- The process-side transcript chosen at each step. Only constrained + /-- The process-side path chosen at each step. Only constrained to be coherent when `event n = .processTick`; left unconstrained in the env-tick branch. -/ - procTranscript : (n : ℕ) → (process.step (state n).proc).spec.Transcript + procPath : (n : ℕ) → (process.step (state n).proc).tree.Path /-- The env-state result sampled at each step. Only constrained to be coherent when `event n = .envTick e`. -/ envSample : ℕ → State /-- One-step coherence: at process ticks the proc field advances by - the chosen transcript, at env ticks the env state advances to the + the chosen path, at env ticks the env state advances to the sampled new state. -/ next_state : ∀ n, state (n + 1) = match event n with | .processTick => { state n with - proc := (process.step (state n).proc).next (procTranscript n) } + proc := (process.step (state n).proc).next (procPath n) } | .envTick _ => { state n with envState := envSample n } namespace AsyncRun -variable {Γ : Spec.Node.Context} +variable {Γ : TypeTree.Node.Context} variable {m : Type → Type} [Pure m] variable {State Event P : Type} variable {process : Concurrent.ProcessOver P Γ} @@ -171,7 +171,7 @@ structure Ticketed toEnvProcess : EnvOpenProcess.{0, 0, 0, 0, 0} m Party Δ Event State /-- The stable obligation type. -/ Ticket : Type - /-- The stable ticket assigned to each complete process-step transcript. -/ + /-- The stable ticket assigned to each complete process-step path. -/ ticket : toEnvProcess.process.toProcess.Tickets Ticket namespace Ticketed @@ -193,7 +193,7 @@ def envAction (ticketed : Ticketed Party m Δ Event State) : /-- A process ticket is *enabled* at step `n` of an async run when -some transcript through the current process spec carries that +some path through the current process type tree carries that ticket. Equivalent to the synchronous @@ -205,18 +205,18 @@ def enabledAt (ticketed : Ticketed Party m Δ Event State) (run : AsyncRun ticketed.process.toProcess ticketed.envAction) (ticket : ticketed.Ticket) (n : ℕ) : Prop := - ∃ tr : (ticketed.process.step (run.state n).proc).spec.Transcript, + ∃ tr : (ticketed.process.step (run.state n).proc).tree.Path, ticketed.ticket (run.state n).proc tr = ticket /-- A process ticket *fires* at step `n` of an async run when: 1. the runtime fired a `processTick` at step `n`, and -2. the chosen transcript carries that ticket. +2. the chosen path carries that ticket. Note the asymmetry with the synchronous `firedAt`: an `envTick` at step `n` cannot fire a process ticket, even though the -recorded `procTranscript n` is still well-formed. This matches +recorded `procPath n` is still well-formed. This matches the operational reading that env ticks do not advance the process side. -/ @@ -225,7 +225,7 @@ def firedAt (run : AsyncRun ticketed.process.toProcess ticketed.envAction) (ticket : ticketed.Ticket) (n : ℕ) : Prop := run.event n = .processTick ∧ - ticketed.ticket (run.state n).proc (run.procTranscript n) = ticket + ticketed.ticket (run.state n).proc (run.procPath n) = ticket /-- *Weak fairness* for a single process ticket: continuously enabled @@ -279,7 +279,7 @@ theorem fired_implies_enabled (run : AsyncRun ticketed.process.toProcess ticketed.envAction) (ticket : ticketed.Ticket) (n : ℕ) : firedAt ticketed run ticket n → enabledAt ticketed run ticket n := - fun ⟨_, hticket⟩ => ⟨run.procTranscript n, hticket⟩ + fun ⟨_, hticket⟩ => ⟨run.procPath n, hticket⟩ /-- Strong fairness implies weak fairness on the same ticket. -/ theorem weakFairOn_of_strongFairOn @@ -314,7 +314,7 @@ structure SchedulerPair (State Event : Type) where /-- The process-side sampler, indexed by closed processes. -/ proc : ∀ p : (openTheory.{u, 0, 0, 0} Party m schedulerSampler).Closed, - ProcessScheduler m p.Proc State (fun st => (p.step st.proc).spec) + ProcessScheduler m p.Proc State (fun st => (p.step st.proc).tree) /-- The env-side sampler, indexed by closed processes. -/ env : ∀ p : (openTheory.{u, 0, 0, 0} Party m schedulerSampler).Closed, EnvScheduler m p.Proc State Event diff --git a/VCVio/Interaction/UC/Runtime.lean b/VCVio/Interaction/UC/Runtime.lean index d5d5d39b8..072cc3251 100644 --- a/VCVio/Interaction/UC/Runtime.lean +++ b/VCVio/Interaction/UC/Runtime.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Quang Dao -/ import PolyFun.Interaction.Basic.Sampler -import PolyFun.Interaction.Basic.SpecFintype +import PolyFun.Interaction.Basic.TypeTreeFintype import PolyFun.Interaction.UC.OpenProcessModel import VCVio.Interaction.UC.Computational import VCVio.OracleComp.Constructions.SampleableType @@ -16,7 +16,7 @@ This file bridges the structural `OpenProcess` layer to the bundled sub-probabilistic semantics (`UC.Semantics`) by defining how to execute a closed process. -The core runtime primitives (`Spec.Sampler`, `sampleTranscript`, +The core runtime primitives (`TypeTree.Sampler`, `samplePath`, `StepOver.sample`, `ProcessOver.runSteps`) are parameterized by an arbitrary monad `m : Type → Type`. This generality lets the execution intermediate monad carry additional capabilities, such as shared oracle @@ -44,11 +44,10 @@ Common instantiations: ## Main definitions -* `Spec.Sampler m spec` provides an `m X` computation at each node of - a `Spec` tree, resolving each move in the intermediate monad. +* `TypeTree.Sampler m spec` provides an `m X` computation at each node of + a `TypeTree`, resolving each move in the intermediate monad. -* `Spec.sampleTranscript` executes a sampler to produce a full - transcript in `m`. +* `TypeTree.samplePath` executes a sampler to produce a full path in `m`. * `StepOver.sample` runs one step by sampling a transcript and applying the continuation. @@ -80,7 +79,7 @@ open OracleComp namespace Interaction -namespace Spec +namespace TypeTree /-- Uniform selection from a nonempty finite type as a `ProbComp` primitive, @@ -95,43 +94,43 @@ noncomputable def probCompUniformOfFintype (X : Type) [Fintype X] [Nonempty X] : $ᵗ X /-- -Canonical uniform sampler on a `Spec.Fintype`-ornamented spec, built by +Canonical uniform sampler on a `TypeTree.Fintype`-ornamented tree, built by recursion on the ornament: each node samples uniformly from its move space using `probCompUniformOfFintype`, and the continuation samplers are produced recursively from the per-branch ornament. This is the interaction-spec analogue of `SampleableType` for `OracleSpec`: concrete `spec` trees whose move types all carry `Fintype` -and `Nonempty` synthesize an instance of `Spec.Fintype spec` +and `Nonempty` synthesize an instance of `TypeTree.Fintype spec` automatically, yielding `Sampler.uniform spec` as the canonical coin-flip-only sampler for downstream runtime semantics (`processSemanticsProbComp`, etc.). -/ noncomputable def Sampler.uniform : - (spec : Spec.{0}) → Spec.Fintype spec → Sampler ProbComp spec + (spec : TypeTree.{0}) → TypeTree.Fintype spec → Sampler ProbComp spec | .done, _ => ⟨⟩ | .node X rest, .node hFin hNon hRec => (@probCompUniformOfFintype X hFin hNon, fun x => Sampler.uniform (rest x) (hRec x)) /-- Instance-argument form of `Sampler.uniform`. -/ @[reducible] -noncomputable def Sampler.uniformI (spec : Spec.{0}) [h : Spec.Fintype spec] : +noncomputable def Sampler.uniformI (spec : TypeTree.{0}) [h : TypeTree.Fintype spec] : Sampler ProbComp spec := Sampler.uniform spec h -/-! Smoke test: typeclass synthesis builds a `Spec.Fintype` instance for a +/-! Smoke test: typeclass synthesis builds a `TypeTree.Fintype` instance for a concrete spec, and `Sampler.uniformI` elaborates against it. -/ -private example : Spec.Fintype - (Spec.node Bool (fun _ => Spec.node (Fin 4) (fun _ => Spec.done))) := +private example : TypeTree.Fintype + (TypeTree.node Bool (fun _ => TypeTree.node (Fin 4) (fun _ => TypeTree.done))) := inferInstance private noncomputable example : Sampler ProbComp - (Spec.node Bool (fun _ => Spec.node (Fin 4) (fun _ => Spec.done))) := + (TypeTree.node Bool (fun _ => TypeTree.node (Fin 4) (fun _ => TypeTree.done))) := Sampler.uniformI _ -end Spec +end TypeTree namespace Concurrent @@ -140,18 +139,18 @@ Run one step of a `ProcessOver` by sampling a transcript from the step's spec and applying the continuation to get the next state. -/ noncomputable def StepOver.sample {m : Type → Type} [Monad m] - {Γ : Spec.Node.Context} {P : Type} - (step : StepOver Γ P) (sampler : Spec.Sampler m step.spec) : m P := - step.next <$> Spec.sampleTranscript step.spec sampler + {Γ : TypeTree.Node.Context} {P : Type} + (step : StepOver Γ P) (sampler : TypeTree.Sampler m step.tree) : m P := + step.next <$> TypeTree.samplePath step.tree sampler /-- Run `fuel` steps of a process, starting from state `s`, using a state-dependent sampler at each step. -/ noncomputable def ProcessOver.runSteps {m : Type → Type} [Monad m] - {Γ : Spec.Node.Context} {P : Type} + {Γ : TypeTree.Node.Context} {P : Type} (process : ProcessOver P Γ) - (sampler : (p : process.Proc) → Spec.Sampler m (process.step p).spec) : + (sampler : (p : process.Proc) → TypeTree.Sampler m (process.step p).tree) : ℕ → process.Proc → m process.Proc | 0, s => pure s | n + 1, s => (process.step s).sample (sampler s) >>= runSteps process sampler n diff --git a/VCVio/Interaction/UC/StdDoBridge.lean b/VCVio/Interaction/UC/StdDoBridge.lean index 8812391a8..1036e63db 100644 --- a/VCVio/Interaction/UC/StdDoBridge.lean +++ b/VCVio/Interaction/UC/StdDoBridge.lean @@ -12,7 +12,7 @@ import VCVio.ProgramLogic.Unary.StdDoBridge # `Std.Do` / `mvcgen` bridge for the Interaction / UC runtime Equip the runtime primitives in `VCVio.Interaction.UC.Runtime` -(`Spec.sampleTranscript`, `Concurrent.StepOver.sample`, +(`TypeTree.samplePath`, `Concurrent.StepOver.sample`, `Concurrent.ProcessOver.runSteps`) with the equational and Hoare-triple machinery `mvcgen` needs, so users can prove triples about UC executions in the same style as `VCVio.ProgramLogic.Unary.HandlerSpecs`. @@ -20,7 +20,7 @@ in the same style as `VCVio.ProgramLogic.Unary.HandlerSpecs`. ## Architecture The runtime primitives are defined by structural recursion over the -`Interaction.Spec` tree (for transcript sampling) or over fuel `ℕ` (for +`Interaction.TypeTree` (for path sampling) or over fuel `ℕ` (for `runSteps`). Neither recursion is walked by `mvcgen`, so we expose the recursive equations as `@[simp]` lemmas and provide a closed-form `runSteps_triple_preserves_invariant` for the most common @@ -35,10 +35,10 @@ since both carry `Std.Do.WPMonad` instances via ## Main results -* `Spec.sampleTranscript_done`, `Spec.sampleTranscript_node` — rfl-level - unfolding of `Spec.sampleTranscript` for base and step cases. +* `TypeTree.samplePath_done`, `TypeTree.samplePath_node` — rfl-level + unfolding of `TypeTree.samplePath` for base and step cases. * `Concurrent.StepOver.sample_eq` — unfolds `StepOver.sample` in terms - of `sampleTranscript`. + of `samplePath`. * `Concurrent.ProcessOver.runSteps_zero`, `Concurrent.ProcessOver.runSteps_succ` — base and step unfolding of `runSteps` on fuel. @@ -47,7 +47,7 @@ since both carry `Std.Do.WPMonad` instances via induction on fuel. These equations are tagged `@[simp]` so that `mvcgen` can walk an -exposed `sampleTranscript` / `sample` / `runSteps` body in one simp pass +exposed `samplePath` / `sample` / `runSteps` body in one simp pass before the usual `do`-block traversal. The bind-shaped definitions hold by `rfl`; `Concurrent.StepOver.sample_eq` rephrases the map-shaped `StepOver.sample` and needs `[LawfulMonad m]`. @@ -57,39 +57,39 @@ open Std.Do OracleComp namespace Interaction -namespace Spec +namespace TypeTree section unfolding variable {m : Type → Type} [Monad m] @[simp] -theorem sampleTranscript_done (samp : Sampler m .done) : - sampleTranscript .done samp = pure ⟨⟩ := rfl +theorem samplePath_done (samp : Sampler m .done) : + samplePath .done samp = pure ⟨⟩ := rfl @[simp] -theorem sampleTranscript_node {X : Type} - (rest : X → Spec.{0}) (samp : m X) (sampRest : ∀ x, Sampler m (rest x)) : - sampleTranscript (.node X rest) ⟨samp, sampRest⟩ = +theorem samplePath_node {X : Type} + (rest : X → TypeTree.{0}) (samp : m X) (sampRest : ∀ x, Sampler m (rest x)) : + samplePath (.node X rest) ⟨samp, sampRest⟩ = (do let x ← samp - let tr ← sampleTranscript (rest x) (sampRest x) + let tr ← samplePath (rest x) (sampRest x) return ⟨x, tr⟩) := rfl end unfolding -end Spec +end TypeTree namespace Concurrent section StepOver variable {m : Type → Type} [Monad m] -variable {Γ : Interaction.Spec.Node.Context.{0, 0}} {P : Type} +variable {Γ : Interaction.TypeTree.Node.Context.{0, 0}} {P : Type} @[simp] theorem StepOver.sample_eq [LawfulMonad m] (step : StepOver Γ P) - (sampler : Spec.Sampler m step.spec) : step.sample sampler = - (do let tr ← Spec.sampleTranscript step.spec sampler + (sampler : TypeTree.Sampler m step.tree) : step.sample sampler = + (do let tr ← TypeTree.samplePath step.tree sampler return step.next tr) := by rw [StepOver.sample, map_eq_pure_bind] @@ -98,16 +98,17 @@ end StepOver section ProcessOver variable {m : Type → Type} [Monad m] -variable {Γ : Interaction.Spec.Node.Context.{0, 0}} +variable {Γ : Interaction.TypeTree.Node.Context.{0, 0}} @[simp] theorem ProcessOver.runSteps_zero {P : Type} (process : ProcessOver P Γ) - (sampler : ∀ p : process.Proc, Spec.Sampler m (process.step p).spec) (s : process.Proc) : + (sampler : ∀ p : process.Proc, TypeTree.Sampler m (process.step p).tree) + (s : process.Proc) : process.runSteps sampler 0 s = pure s := rfl @[simp] theorem ProcessOver.runSteps_succ {P : Type} (process : ProcessOver P Γ) - (sampler : ∀ p : process.Proc, Spec.Sampler m (process.step p).spec) (n : ℕ) + (sampler : ∀ p : process.Proc, TypeTree.Sampler m (process.step p).tree) (n : ℕ) (s : process.Proc) : process.runSteps sampler (n + 1) s = (do let s' ← (process.step s).sample (sampler s) @@ -124,7 +125,7 @@ namespace ProcessOver variable {m : Type → Type} [Monad m] variable {ps : PostShape} [WPMonad m ps] -variable {Γ : Interaction.Spec.Node.Context.{0, 0}} +variable {Γ : Interaction.TypeTree.Node.Context.{0, 0}} /-- If every one-step execution preserves an invariant `I` on the process state, then `runSteps n` preserves `I` for any fuel `n`. @@ -134,7 +135,7 @@ This is the process-runtime analogue of a generic invariant lemma that factors out the fuel induction so downstream proofs stay inside the `Std.Do` world. -/ theorem runSteps_triple_preserves_invariant {P : Type} (process : ProcessOver P Γ) - (sampler : ∀ p : process.Proc, Spec.Sampler m (process.step p).spec) + (sampler : ∀ p : process.Proc, TypeTree.Sampler m (process.step p).tree) (I : process.Proc → Prop) (hstep : ∀ p : process.Proc, Std.Do.Triple ((process.step p).sample (sampler p)) (spred(⌜I p⌝)) @@ -170,20 +171,20 @@ namespace Interaction.Concurrent.ProcessOver namespace Example /-- Trivial node context carrying no per-node metadata. -/ -private abbrev trivCtx : Interaction.Spec.Node.Context.{0, 0} := fun _ => PUnit +private abbrev trivCtx : Interaction.TypeTree.Node.Context.{0, 0} := fun _ => PUnit /-- Always-increment process: each step has no moves and bumps the counter by one. -/ private def incrementProcess : ProcessOver ℕ trivCtx := ProcessOver.ofStep ℕ fun p => - { spec := .done + { tree := .done semantics := PUnit.unit next := fun _ => p + 1 } /-- Trivial sampler for the always-`.done` step-spec family. -/ private def trivSampler : ∀ p : incrementProcess.Proc, - Interaction.Spec.Sampler ProbComp (incrementProcess.step p).spec := + Interaction.TypeTree.Sampler ProbComp (incrementProcess.step p).tree := fun _ => PUnit.unit private theorem incrementProcess_step_triple (p₀ p : ℕ) : diff --git a/VCVio/OracleComp/SimSemantics/QueryImpl/Basic.lean b/VCVio/OracleComp/SimSemantics/QueryImpl/Basic.lean index 87ad29440..c6f10e29e 100644 --- a/VCVio/OracleComp/SimSemantics/QueryImpl/Basic.lean +++ b/VCVio/OracleComp/SimSemantics/QueryImpl/Basic.lean @@ -6,6 +6,7 @@ Authors: Devon Tuma import Mathlib.Algebra.MvPolynomial.Eval import Mathlib.Algebra.Polynomial.Eval.Defs import VCVio.OracleComp.OracleComp +import PolyFun.PFunctor.Handler /-! # Implementing Oracle Queries in Other Monads @@ -22,11 +23,12 @@ universe u v w open scoped OracleSpec.PrimitiveQuery -/-- Specifies a way to implement queries to oracles in `spec` using the monad `m`. -This is defined in terms of a mapping of input elements to oracle outputs, -which extends to a mapping on `OracleQuery spec` by copying over the continuation, -and then further to `OracleComp spec` by preserving the pure and bind operations. -See `QueryImpl.mapQuery` and `simulateQ` for these two operations. -/ +/-- A monadic handler for the polynomial interface induced by `spec`. + +Concretely, this maps every oracle input `x` to a computation returning an +answer of type `spec.Range x`. It extends first to `OracleQuery spec` by +applying the continuation, then to `OracleComp spec` by preserving `pure` and +`bind`; see `QueryImpl.mapQuery` and `simulateQ`. -/ @[reducible] def QueryImpl {ι} (spec : OracleSpec ι) (m : Type u → Type v) := (x : spec.Domain) → m (spec.Range x) @@ -34,6 +36,10 @@ namespace QueryImpl variable {ι} {spec : OracleSpec ι} {m : Type u → Type v} {n : Type u → Type w} +/-- `QueryImpl` is definitionally PolyFun's generic monadic handler for the +polynomial interface induced by an oracle specification. -/ +theorem eq_handler : QueryImpl spec m = PFunctor.Handler m spec.toPFunctor := rfl + instance [spec.Inhabited] [Pure m] : Inhabited (QueryImpl spec m) where default _ := pure default diff --git a/VCVio/OracleComp/SimSemantics/StateT/StateSeparating.lean b/VCVio/OracleComp/SimSemantics/StateT/StateSeparating.lean index b85c4b004..cae1de715 100644 --- a/VCVio/OracleComp/SimSemantics/StateT/StateSeparating.lean +++ b/VCVio/OracleComp/SimSemantics/StateT/StateSeparating.lean @@ -5,6 +5,7 @@ Authors: Quang Dao -/ import VCVio.OracleComp.Coercions.Add import VCVio.OracleComp.SimSemantics.StateT.Basic +import PolyFun.PFunctor.Handler.Stateful import PolyFun.PFunctor.Lens.State /-! @@ -37,12 +38,20 @@ state, via `link` and `par`, or an explicit `Frame` that describes how two component states are embedded as separated lawful state lenses inside a larger state. -/ -def Stateful +@[reducible] def Stateful {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} (I : OracleSpec.{uᵢ, vᵢ} ιᵢ) (E : OracleSpec.{uₑ, v} ιₑ) (σ : Type v) : Type _ := QueryImpl E (StateT σ (OracleComp I)) +/-- `QueryImpl.Stateful` is definitionally PolyFun's generic effectful +stateful-handler interface specialized to oracle computations. -/ +theorem Stateful.eq_handler + {ιᵢ : Type uᵢ} {ιₑ : Type uₑ} + (I : OracleSpec.{uᵢ, vᵢ} ιᵢ) (E : OracleSpec.{uₑ, v} ιₑ) (σ : Type v) : + QueryImpl.Stateful I E σ = + PFunctor.Handler.Stateful (OracleComp I) σ E.toPFunctor := rfl + namespace Stateful variable {ιᵢ : Type uᵢ} {ιₘ : Type uₘ} {ιₑ : Type uₑ} @@ -139,6 +148,12 @@ def runState {α : Type v} (h : QueryImpl.Stateful I E σ) (s₀ : σ) (A : Orac OracleComp I (α × σ) := (simulateQ h A).run s₀ +/-- `QueryImpl.Stateful.runState` is the `OracleSpec` specialization of the +generic PolyFun effectful-stateful handler runner. -/ +theorem runState_eq_handler_run {α : Type v} (h : QueryImpl.Stateful I E σ) + (s₀ : σ) (A : OracleComp E α) : + h.runState s₀ A = PFunctor.Handler.Stateful.run h A s₀ := rfl + /-- Run a stateful handler from the default initial state, keeping the final state. -/ def runState₀ {α : Type v} [Inhabited σ] (h : QueryImpl.Stateful I E σ) diff --git a/docs/agents/oracle-comp.md b/docs/agents/oracle-comp.md index 59a16062d..7a1c76e72 100644 --- a/docs/agents/oracle-comp.md +++ b/docs/agents/oracle-comp.md @@ -136,13 +136,20 @@ When lifting `OracleComp spec α` to `OracleComp superSpec α` (e.g., a sub-comp ### QueryImpl -Maps each oracle input to a monadic response: +`QueryImpl` maps each oracle input to a monadic response: ```lean @[reducible] def QueryImpl (spec : OracleSpec ι) (m : Type u → Type v) := (x : spec.Domain) → m (spec.Range x) ``` +This is definitionally `PFunctor.Handler m spec.toPFunctor`, recorded by +`QueryImpl.eq_handler`. The source definition retains the oracle-shaped +dependent function because it gives Lean better expected-type information for +polymorphic query code; the PolyFun theorem makes clear that the same object +can interpret any free program over the interface, not only oracle-specific +syntax. + Constructors: | Constructor | Use | diff --git a/docs/agents/program-logic.md b/docs/agents/program-logic.md index 0710967ae..3ec898818 100644 --- a/docs/agents/program-logic.md +++ b/docs/agents/program-logic.md @@ -564,16 +564,17 @@ and the migration to `Sym.Simp.*`-driven rewriting is a localised follow-up in two registry files rather than a framework rewrite. **Key alignment invariant**: `Sym.DiscrTree.getMatch` is purely structural, so -goal-side query terms must be normalized with the *same* preprocessing the -pattern side gets at registration time. All registry query functions therefore -route the extracted computation through `symMatchKey` -(`Tactics/Common/Core.lean`), which applies `Sym.preprocessType` -(unfold-reducible + beta/zeta/eta). This matters because `OracleComp` is a -reducible alias of `PFunctor.FreeM`: the stored patterns carry unfolded -`FreeM`-form keys at the monad argument of `Bind.bind` and friends, and an -unnormalized query key diverges there, making every lookup silently return no -candidates (symptom: `vcstep` reports "no matching rule applied" on plain -`pure`/`>>=` goals while manual `rw [wp_pure]`/`rw [wp_bind]` works). +goal-side query terms must expose the same oracle-wrapper shapes as the pattern +side. All registry query functions therefore route the extracted computation +through `symMatchKey` (`Tactics/Common/Core.lean`), which recursively unfolds +only `OracleComp`, `OracleQuery`, and `OracleSpec.toPFunctor`. This targeted +normalization is necessary because `OracleComp` is a reducible alias of +`PFunctor.FreeM`, while deliberately avoiding `Sym.preprocessType`: applying +that declaration-oriented preprocessing to terms can unfold reducible user +programs and panic when a matcher contains loose de Bruijn variables. Without +the targeted unfolding, lookup can silently return no candidates (symptom: +`vcstep` reports "no matching rule applied" while the corresponding manual +rewrite works). ### Registries and what they index diff --git a/lake-manifest.json b/lake-manifest.json index 3ddc7eb80..59ce787ee 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "1f7f477c9701f7606841bb1638dcffb9b2359d62", + "rev": "59072c30eb4e01e21cb1cf540de4cbef15eff07d", "name": "PolyFun", "manifestFile": "lake-manifest.json", - "inputRev": "1f7f477c9701f7606841bb1638dcffb9b2359d62", + "inputRev": "59072c30eb4e01e21cb1cf540de4cbef15eff07d", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", diff --git a/lakefile.lean b/lakefile.lean index f1778920c..038dd5690 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -58,7 +58,7 @@ require "leanprover-community" / "mathlib" @ git "v4.32.0" require PolyFun from git "https://github.com/Verified-zkEVM/PolyFun.git" @ - "1f7f477c9701f7606841bb1638dcffb9b2359d62" + "59072c30eb4e01e21cb1cf540de4cbef15eff07d" /-- Main library. -/ @[default_target] lean_lib VCVio From 462fdfc44a7d9082e35850618b5b3c6f2319b361 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Wed, 22 Jul 2026 18:43:27 +0530 Subject: [PATCH 5/6] chore: update PolyFun and split sampler ornaments --- Examples/OneTimePad/UC.lean | 6 ++--- VCVio/Interaction/UC/Runtime.lean | 40 ++++++++++++++++++------------- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 4 files changed, 30 insertions(+), 22 deletions(-) diff --git a/Examples/OneTimePad/UC.lean b/Examples/OneTimePad/UC.lean index 2909cf9a4..247bc1230 100644 --- a/Examples/OneTimePad/UC.lean +++ b/Examples/OneTimePad/UC.lean @@ -458,9 +458,9 @@ abbrev otpTree (sp : ℕ) : Interaction.TypeTree.{0} := TypeTree.node (BitVec sp) (fun _ => TypeTree.done) /-- The canonical uniform `ProbComp`-sampler for `otpTree sp`, -synthesized from the `TypeTree.Fintype (otpTree sp)` instance built by -typeclass synthesis from `Fintype (BitVec sp)` and -`Nonempty (BitVec sp)`. -/ +synthesized from the separate `TypeTree.Fintype (otpTree sp)` and +`TypeTree.Nonempty (otpTree sp)` instances built by typeclass synthesis from +`Fintype (BitVec sp)` and `Nonempty (BitVec sp)`. -/ noncomputable def uniformOtpSampler (sp : ℕ) : TypeTree.Sampler ProbComp (otpTree sp) := TypeTree.Sampler.uniformI _ diff --git a/VCVio/Interaction/UC/Runtime.lean b/VCVio/Interaction/UC/Runtime.lean index 072cc3251..0ab4ab965 100644 --- a/VCVio/Interaction/UC/Runtime.lean +++ b/VCVio/Interaction/UC/Runtime.lean @@ -94,37 +94,45 @@ noncomputable def probCompUniformOfFintype (X : Type) [Fintype X] [Nonempty X] : $ᵗ X /-- -Canonical uniform sampler on a `TypeTree.Fintype`-ornamented tree, built by -recursion on the ornament: each node samples uniformly from its move -space using `probCompUniformOfFintype`, and the continuation samplers -are produced recursively from the per-branch ornament. +Canonical uniform sampler on a finite, nonempty-branching tree, built by +recursion on the two ornaments: each node samples uniformly from its move +space using `probCompUniformOfFintype`, and the continuation samplers are +produced recursively from the corresponding per-branch ornaments. This is the interaction-spec analogue of `SampleableType` for `OracleSpec`: concrete `spec` trees whose move types all carry `Fintype` -and `Nonempty` synthesize an instance of `TypeTree.Fintype spec` -automatically, yielding `Sampler.uniform spec` as the canonical -coin-flip-only sampler for downstream runtime semantics -(`processSemanticsProbComp`, etc.). +and `Nonempty` synthesize separate `TypeTree.Fintype spec` and +`TypeTree.Nonempty spec` instances automatically, yielding `Sampler.uniform +spec` as the canonical coin-flip-only sampler for downstream runtime +semantics (`processSemanticsProbComp`, etc.). -/ noncomputable def Sampler.uniform : - (spec : TypeTree.{0}) → TypeTree.Fintype spec → Sampler ProbComp spec - | .done, _ => ⟨⟩ - | .node X rest, .node hFin hNon hRec => - (@probCompUniformOfFintype X hFin hNon, fun x => Sampler.uniform (rest x) (hRec x)) + (spec : TypeTree.{0}) → TypeTree.Fintype spec → TypeTree.Nonempty spec → + Sampler ProbComp spec + | .done, _, _ => ⟨⟩ + | .node X rest, .node hFin hFinRec, hNon => + (@probCompUniformOfFintype X hFin (TypeTree.Nonempty.rootNonempty hNon), + fun x => Sampler.uniform (rest x) (hFinRec x) (TypeTree.Nonempty.rest hNon x)) /-- Instance-argument form of `Sampler.uniform`. -/ @[reducible] -noncomputable def Sampler.uniformI (spec : TypeTree.{0}) [h : TypeTree.Fintype spec] : +noncomputable def Sampler.uniformI (spec : TypeTree.{0}) + [hFin : TypeTree.Fintype spec] [hNon : TypeTree.Nonempty spec] : Sampler ProbComp spec := - Sampler.uniform spec h + Sampler.uniform spec hFin hNon -/-! Smoke test: typeclass synthesis builds a `TypeTree.Fintype` instance for a -concrete spec, and `Sampler.uniformI` elaborates against it. -/ +/-! Smoke test: typeclass synthesis builds separate `TypeTree.Fintype` and +`TypeTree.Nonempty` instances for a concrete spec, and `Sampler.uniformI` +elaborates against both. -/ private example : TypeTree.Fintype (TypeTree.node Bool (fun _ => TypeTree.node (Fin 4) (fun _ => TypeTree.done))) := inferInstance +private example : TypeTree.Nonempty + (TypeTree.node Bool (fun _ => TypeTree.node (Fin 4) (fun _ => TypeTree.done))) := + inferInstance + private noncomputable example : Sampler ProbComp (TypeTree.node Bool (fun _ => TypeTree.node (Fin 4) (fun _ => TypeTree.done))) := diff --git a/lake-manifest.json b/lake-manifest.json index 59ce787ee..aeddbb134 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "59072c30eb4e01e21cb1cf540de4cbef15eff07d", + "rev": "078493a7576d2d9115241fbfbeeca682ba09cb8f", "name": "PolyFun", "manifestFile": "lake-manifest.json", - "inputRev": "59072c30eb4e01e21cb1cf540de4cbef15eff07d", + "inputRev": "078493a7576d2d9115241fbfbeeca682ba09cb8f", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", diff --git a/lakefile.lean b/lakefile.lean index 038dd5690..f922dda7b 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -58,7 +58,7 @@ require "leanprover-community" / "mathlib" @ git "v4.32.0" require PolyFun from git "https://github.com/Verified-zkEVM/PolyFun.git" @ - "59072c30eb4e01e21cb1cf540de4cbef15eff07d" + "078493a7576d2d9115241fbfbeeca682ba09cb8f" /-- Main library. -/ @[default_target] lean_lib VCVio From a62b2feb7b8abea9c82288ce704630a89665f9b4 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Wed, 22 Jul 2026 19:56:54 +0530 Subject: [PATCH 6/6] refactor: consume PolyFun handler normalization --- Examples/ProgramLogic/ProofMode.lean | 15 ++++++++++++++- VCVio/OracleComp/QueryTracking/HandlerSimp.lean | 17 +++++------------ VCVio/Prelude.lean | 2 +- VCVio/ProgramLogic/Tactics/Handler.lean | 10 +++++----- docs/agents/program-logic.md | 9 ++++++++- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 7 files changed, 36 insertions(+), 23 deletions(-) diff --git a/Examples/ProgramLogic/ProofMode.lean b/Examples/ProgramLogic/ProofMode.lean index 7a7a31e2a..f125ddd6c 100644 --- a/Examples/ProgramLogic/ProofMode.lean +++ b/Examples/ProgramLogic/ProofMode.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Quang Dao -/ -import VCVio.ProgramLogic.Tactics.Relational +import VCVio.ProgramLogic.Tactics /-! # Proof-Mode Entry / Exit Tactic Examples @@ -25,6 +25,19 @@ variable {ι : Type u} {spec : OracleSpec ι} variable [IsUniformSpec spec] variable {α β γ : Type} +/-! ## Handler normalization -/ + +section HandlerNormalization + +/-- `handler_step` consumes PolyFun's generic handler normal form. -/ +example {m : Type → Type} [Monad m] [LawfulMonad m] + (h : PFunctor.Handler.Stateful m Nat (PFunctor.monomial Bool Nat)) + (query : Bool) (state : Nat) : + h.run (PFunctor.FreeM.lift query) state = (h query).run state := by + handler_step + +end HandlerNormalization + /-! ## `game_trans` -/ example {g₁ g₂ g₃ : OracleComp spec α} diff --git a/VCVio/OracleComp/QueryTracking/HandlerSimp.lean b/VCVio/OracleComp/QueryTracking/HandlerSimp.lean index 71fcf25b5..1fd067361 100644 --- a/VCVio/OracleComp/QueryTracking/HandlerSimp.lean +++ b/VCVio/OracleComp/QueryTracking/HandlerSimp.lean @@ -3,16 +3,18 @@ Copyright (c) 2026 Quang Dao. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Quang Dao -/ +import PolyFun.PFunctor.Handler.Normalization import VCVio.OracleComp.QueryTracking.CachingLoggingOracle import VCVio.OracleComp.QueryTracking.CountingOracle import VCVio.OracleComp.QueryTracking.SeededOracle import VCVio.OracleComp.SimSemantics.StateT.StateProjection /-! -# `handler_simp` for Query Handlers +# Handler Normalization for Query Handlers -Small normalization simp-set for the common handler transformers and their -`StateT` / `WriterT` run-shapes. +The `handler_simp` simp set extends PolyFun's generic `handler_nf` normal form +with VCVio query simulation, instrumentation, caching, and local WriterT +compatibility equations. The goal is not to create a second proof mode; it is just the shared "open the handler one step" surface that proof scripts can use before handing control @@ -45,16 +47,7 @@ attribute [handler_simp] cachingOracle.apply_eq seededOracle.apply_eq cachingLoggingOracle.apply_eq - StateT.run_bind - StateT.run_get - StateT.run_set - StateT.run_modifyGet - StateT.run_pure - StateT.run_monadLift - WriterT.run_bind WriterT.run_bind' WriterT.run_monadLift WriterT.run_monadLift' - WriterT.run_pure WriterT.run_pure' - WriterT.run_tell diff --git a/VCVio/Prelude.lean b/VCVio/Prelude.lean index 3de2c3b3b..b5a211a44 100644 --- a/VCVio/Prelude.lean +++ b/VCVio/Prelude.lean @@ -16,5 +16,5 @@ declare_aesop_rule_sets [UnfoldEvalDist] /-- Simp set for game-hopping proofs: evalDist, probOutput, simulateQ, wp, relTriple rules. -/ register_simp_attr game_rule -/-- Simp set for opening common query-handler definitions and run-shapes. -/ +/-- VCVio-specific extension of PolyFun's `handler_nf` normalization set. -/ register_simp_attr handler_simp diff --git a/VCVio/ProgramLogic/Tactics/Handler.lean b/VCVio/ProgramLogic/Tactics/Handler.lean index 27a6c5f99..d19d63c27 100644 --- a/VCVio/ProgramLogic/Tactics/Handler.lean +++ b/VCVio/ProgramLogic/Tactics/Handler.lean @@ -10,10 +10,10 @@ import VCVio.OracleComp.QueryTracking.HandlerSimp /-! # Handler Normalization Tactic -`handler_step` performs one small normalization pass using the `handler_simp` -set. It is intentionally thin: use it to expose the next handler body or -run-shape, then continue with `mvcgen`, `vcstep`, `rvcstep`, or direct proof -steps. +`handler_step` performs one small normalization pass using PolyFun's generic +`handler_nf` set followed by VCVio's `handler_simp` extension. It is +intentionally thin: use it to expose the next handler body or run-shape, then +continue with `mvcgen`, `vcstep`, `rvcstep`, or direct proof steps. -/ open Lean Elab Tactic @@ -24,6 +24,6 @@ syntax "handler_step" : tactic elab_rules : tactic | `(tactic| handler_step) => do - evalTactic (← `(tactic| simp only [handler_simp])) + evalTactic (← `(tactic| simp only [handler_nf, handler_simp])) end OracleComp.ProgramLogic diff --git a/docs/agents/program-logic.md b/docs/agents/program-logic.md index 3ec898818..fc4dab4d5 100644 --- a/docs/agents/program-logic.md +++ b/docs/agents/program-logic.md @@ -160,13 +160,20 @@ This keeps ordinary rule ordering stable when new `@[vcspec]` lemmas are added. | Tactic | Goal shape | What it does | |--------|-----------|--------------| -| `handler_step` | handler-heavy `QueryImpl` / `simulateQ` / `StateT` goals | Runs one `simp only [handler_simp]` normalization pass to expose the next handler body or run-shape | +| `handler_step` | handler-heavy `FreeM` / `QueryImpl` / `simulateQ` / transformer goals | Runs one `simp only [handler_nf, handler_simp]` normalization pass to expose the next handler body or run-shape | `handler_step` is deliberately thin. Use it when a proof is stuck behind handler combinators such as cache overlays, logging handlers, counting handlers, or state-transformer maps; then continue with `vcstep`, `rvcstep`, `rvcgen`, or direct proof steps. +PolyFun owns the generic `handler_nf` rules for `FreeM`, +`PFunctor.Handler.Stateful`, `StateT`, and standard `WriterT`. VCVio's +`handler_simp` set adds only oracle simulation, query instrumentation, +caching, and local WriterT compatibility equations. Downstream code can use +the two sets independently; `handler_step` composes them in generic-to-specific +order. + **Opt-in `wp`-rewrite lookup**: mark an equational rewrite of shape `wp comp post = …` with `@[wpStep]` to extend the inner `wp`-stepping driver (`runWpStepRules`). The driver indexes registered rules by the path of `comp` diff --git a/lake-manifest.json b/lake-manifest.json index aeddbb134..4bbd1d5b8 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "078493a7576d2d9115241fbfbeeca682ba09cb8f", + "rev": "29644990ebc2828ca09170bc9d398649cd9f5950", "name": "PolyFun", "manifestFile": "lake-manifest.json", - "inputRev": "078493a7576d2d9115241fbfbeeca682ba09cb8f", + "inputRev": "29644990ebc2828ca09170bc9d398649cd9f5950", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", diff --git a/lakefile.lean b/lakefile.lean index f922dda7b..06898e0a3 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -58,7 +58,7 @@ require "leanprover-community" / "mathlib" @ git "v4.32.0" require PolyFun from git "https://github.com/Verified-zkEVM/PolyFun.git" @ - "078493a7576d2d9115241fbfbeeca682ba09cb8f" + "29644990ebc2828ca09170bc9d398649cd9f5950" /-- Main library. -/ @[default_target] lean_lib VCVio