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.
The HAdd notation for query implementations is their explicit QueryImpl.add
operation. This named bridge lets downstream proofs cross the module boundary without
requesting stronger reducibility for the instance.
Version of QueryImpl.add that also lifts the two implementations to a shared lift monad.
Instances For
Simulating a query-level lift from the left summand routes it to the left implementation.
Simulating a query-level lift from the right summand routes it to the right implementation.
A query formed directly against the sum specification routes to its left handler.
A query formed directly against the sum specification routes to its right handler.
A query to the left component of a sum handler routes to that component before its continuation is simulated.
A query to the right component of a sum handler routes to that component before its continuation is simulated.
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 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
reduce through simulateQ_spec_query after the component lift is re-expressed as the
canonical embedded query at its 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.
Routing through a two-way addLift whose components live in different monads #
addLift lifts each component handler into a shared target, so a computation lifted from one
summand resolves to that component's simulation, re-lifted into the target. Stated with the two
sources in distinct monads source₁ / source₂: that is the shape oracle-reduction verifiers
produce, where a base-spec handler and a message-oracle handler are combined into one target.
A computation lifted from the left summand routes to the left component of an addLift,
leaving its simulation lifted into the target.
A computation lifted from the right summand routes to the right component of an addLift,
leaving its simulation lifted into the target.
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 the OptionT.run_lift law, which collapses the OptionT lift chain to a
plain OracleComp lift; the chain-agnostic QueryImpl.simulateQ_liftM_eq_of_query then
resolves it.