Currently, the use of sections forces an unfortunate proof pattern, which involves defining the reductions (part of the statement) before opening a section that quantifies over the adversary. This is because defining reductions (as non-local modules) after the adversary is quantified does not allow us to then restrict the sharing of state between the reduction and adversary.
I propose that we allow annotating non-local module definitions inside a section with declared modules we expect them to be disjoint from. This disjointness assumption can be used in proofs inside the section, but must then be exposed outside. This can simply be done by reflecting it as an additional restriction on the relevant declared modules when the section is closed.
For example:
section S.
declare module A <: Adv { -Exp }.
global { -A } module R (A : Adv) = {
...
}.
lemma toto: P(Exp(R(A)).
admitted.
end section.
print toto.
(* forall A <: Adv { -Exp, -R }, P(Exp(R(A)). *)
In practice, this would allow defining the reduction where it is needed in the proof instead of having to front-load it before the proof starts.
Currently, the use of sections forces an unfortunate proof pattern, which involves defining the reductions (part of the statement) before opening a section that quantifies over the adversary. This is because defining reductions (as non-local modules) after the adversary is quantified does not allow us to then restrict the sharing of state between the reduction and adversary.
I propose that we allow annotating non-local module definitions inside a section with declared modules we expect them to be disjoint from. This disjointness assumption can be used in proofs inside the section, but must then be exposed outside. This can simply be done by reflecting it as an additional restriction on the relevant declared modules when the section is closed.
For example:
In practice, this would allow defining the reduction where it is needed in the proof instead of having to front-load it before the proof starts.