Research proof index

Running the monadic version of buildMerkleTree with an oracle function f is equivalent to running the functional version of buildMerkleTreeWithHash with the same oracle function.

Running the monadic getPutativeBatchRoot with an oracle function f is the same as running the functional getPutativeBatchRootWithHash with the corresponding hash function.

Under the empty env alphabet (EnvAction.empty Unit) and the trivial env scheduler (always processTick), runStepsAsync reduces to ProcessOver.runSteps with the env state pinned to () and a constant processTick trace. This is the operational core of the sync-recovery story: it factors the async engine into the synchronous ProcessOver.runSteps...

If main makes at most qb i queries to each oracle i, then its total query count (under the unit cost model) is at most ∑ i, qb i on every execution path.

The one-stage IND-CPA game is exactly the IND-CCA game instantiated with the trivial CPA-to-CCA embedding (toIND_CCA) that never uses the decryption oracle.

Proof-ladders A1 reduction statement: the one-time IND-CPA advantage of textbook KEM+DEM is bounded by two KEM IND-CPA advantages plus one DEM IND-CPA advantage, using the canonical left/right and DEM reductions defined above. The runtime coherence hypotheses require runtime.evalDist to be a monad morphism (preserves pure and distributes >>=) and to...