Random oracle framework #
This file is a barrel re-exporting the framework. The actual definitions
and lemmas live in PlonkLean/RO/:
PlonkLean.RO.Basic— RO primitives only:random_oracle_stateaxiom,lazy_init/random_oracle_init,lazy_query/random_oracle_query, andlazy_query_inFootprint_ro. No bridging between lazy and eager.PlonkLean.RO.TransferConvert— the lazy/eager bridge:convertitself, convert algebra (convert_wp_eq,convert_mass,convert_commutes_set/get,convert_random_oracle_init,convert_bind_random_oracle_init_bind), the foundational lazy/eager equations (lazy_init_convert_eq_random_oracle_init,lazy_query_convert_eq_convert_random_oracle_query,if_factor_convert), theProgramDenotation.transferrelation (=transferBy convert, closure laws inherited fromGaudisCrypt.Logic.TransferBy), and the wp/marginal bridges (ProgramDenotation.transfer_value_marginaland the RO-invariant enrichments).PlonkLean.RO.OracleLoop— scratch state for adversary-driven loops (want_more,oracle_input,oracle_output,adversary_result,skip, disjointness instances), thelazy_query + set oracle_outputkey-reasoning lemmas (query_set_convert_eq,lazy_query_then_set_oracle_output_inFootprint_compl,lazy_query_set_oracle_output_preserves_RO_at_other_key,RO_setentry_neq_commutes_lazy_query_set_oracle_output), the three oracle loop variants (oracle_step,oracle_loop_n,oracle_loop), and their transfer/inRange/indicator-step lemmas.PlonkLean.RO.ROEquiv— the lazy = eager equivalence fororacle_loop:adv_conv_eq_conv_adv(convertcommutes with RO-disjoint adversaries),ProgramDenotation.transfer_oracle_loop(full transfer of the while-loop game, built via the framework'stransfer_while_loopclosure law),oracle_loop_lazy_convert_eq_random_oracle_loop(the foundational equation), and the corollary familyoracle_loop_wp_lazy_eq_random_oracle/oracle_loop_marginal_lazy_eq_random_oracle/..._compl.