refactor(OracleComp): make OracleComp/OracleQuery reducible over PolyFun

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
-typeclass synthesis from `Fintype (BitVec sp)` and
-`Nonempty (BitVec sp)`. -/
+/-- The canonical uniform `ProbComp`-sampler for `otpTree 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 : ℕ) :
-    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,21 +484,21 @@ 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) :
     PFunctor.Trace (Δ_otp sp).Out (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,26 +522,26 @@ 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 -/
 
 /-- **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 _

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 =>

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 α}

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

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

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)