Append/Add Operation for Simulation Oracles #
Simplest version of adding queries when all implementations are in the same monad.
The actual add notation for QueryImpl uses QueryImpl.addLift which adds monad lifting
to this definition for greater flexibility.
Instances For
Add two QueryImpl to get an implementation on the sum of the two OracleSpec.
Version of QueryImpl.add that also lifts the two implementations to a shared lift monad.
Instances For
liftM-normal-form companion of simulateQ_add_liftComp_left. Because liftComp_eq_liftM
normalizes liftComp → liftM under simp, the liftComp-keyed lemma never fires inside simp;
this liftM-keyed form is what simp actually needs.
Deliberately not @[simp]: as a global rule it shifts the normal form of simulateQ over an
added handler applied to a lifted-in computation, which pre-empts and breaks existing proofs that
manage that reduction themselves. Pass it explicitly, e.g.
simp [myHandler, simulateQ_add_liftM_left, simulateQ_toQueryImpl].
liftM-normal-form companion of simulateQ_add_liftComp_right; opt-in, see
simulateQ_add_liftM_left.
Simulating the trivial HasQuery.toQueryImpl handler back into OracleComp spec is the
identity (the composite of HasQuery.toQueryImpl_eq_id' and simulateQ_id').
Like toQueryImpl_eq_id', this is deliberately not @[simp]: globally it lets simulateQ
of a unifFwdImpl-style toQueryImpl.liftTarget handler fully reduce, which can re-enable a
backward induction-hypothesis rewrite and diverge. Pass it explicitly to simp (alongside the
opaque handler definition) to discharge a lifted-in computation, e.g.
simp [myHandler, simulateQ_toQueryImpl]; the simulateQ_add_liftM_left/_right and
simulateQ_liftTarget rungs are @[simp] and fire on their own.
Query routing through a right-nested sum implementation #
Routing lemmas for the spec + (spec₁ + spec₂) layout used by stateless protocol
simulation oracles (e.g. a base spec plus a pair of message/statement oracle families,
the simOracle2 layout): a single query lifted from one component — either at the
query level (OracleQuery) or pre-embedded in its own computation monad
(OracleComp, the shape produced by reusable query helpers) — resolves under
simulateQ to the implementation at the routed index.
Each left-hand side spells the canonical MonadLiftT chain that typeclass resolution
synthesizes for that lift (through the intermediate spec + spec₂ etc.), which is what
lets these fire by simp on goals produced by elaborated protocol definitions. All six
are definitional modulo simulateQ_spec_query: the show … from rfl bridges re-express
the chained lift as the canonical embedded query at the routed index.
Unit tests: a query lifted from a component of a sum spec routes through a sum
implementation by simp alone, via the simulateQ_add_add_liftM_* routing lemmas.
The shape spec + (spec₁ + spec₂) with an addLifted pair is the simOracle2
layout used by oracle-reduction verifiers downstream.
Resolve a simulateQ over a three-way addLift impl (impl₁ + impl₂) applied to a
computation x : OracleComp spec₁ α that has been double-liftM'd — first into the inner
sum spec₁ + spec₂, then into the outer sum spec + (spec₁ + spec₂). The query routes to
the left inner implementation impl₁, leaving liftM (simulateQ impl₁ x).
This is the computation-level sibling of QueryImpl.simulateQ_add_add_liftM_comp_left: it
peels the outer addLift (simulateQ_add_liftComp_right), commutes the inner simulateQ
past the target lift (simulateQ_liftTarget), then peels the inner sum
(simulateQ_add_liftComp_left). Stated for the inner pair living in a possibly-different
monad n lifted into the target m.
Resolve a simulateQ over a three-way addLift impl (impl₁ + impl₂) applied to a
computation x : OracleComp spec₂ α that has been double-liftM'd — first into the inner
sum spec₁ + spec₂, then into the outer sum spec + (spec₁ + spec₂). The query routes to
the right inner implementation impl₂, leaving liftM (simulateQ impl₂ x).
The right companion of simulateQ_addLift_add_liftM_left.
OptionT companion to QueryImpl.simulateQ_liftM_eq_of_query: simulating an
OracleComp-computation oa lifted into OptionT (OracleComp spec₂') (the shape produced by
an OptionT-monadic verifier's let _ ← liftM (queryHelper) binds) agrees, at the run
(Option) level, with some-mapping the simulation of oa through a per-query-bridged
handler impl₁.
The key step is that the OptionT.run of a lifted OracleComp is some <$> (the OracleComp lift) definitionally (hrun below is rfl), which collapses the OptionT lift chain to a
plain OracleComp lift; the chain-agnostic QueryImpl.simulateQ_liftM_eq_of_query then
resolves it.