There is an issue that arises from query counting as we currently do it in generic results (with a broad restriction that the adversary must not make more than q queries regardless of the oracles they interact with). An example of where this fails is below. One way of avoiding the failure is to pollute the top-level statement with restrictions relevant only to the proof.
require import AllCore.
theory T.
type in_t, out_t.
module type O = {
proc o(_: in_t): out_t
}.
module type D (O : O) = {
proc d(): bool
}.
module Count (O : O) : O = {
var c : int
proc o(x) = {
var r;
r <@ O.o(x);
c <- c + 1;
return r;
}
}.
section.
declare module O <: O { -Count }.
declare module D <: D { -Count, -O }.
declare op q : { int | 0 <= q } as ge0_q.
declare axiom D_count (O <: O { -Count, -D }) c:
hoare [D(Count(O)).d: Count.c = c ==> Count.c <= c + q].
hoare toto P:
D(O).d: true ==> P q (glob O) res.
admitted.
end section.
end T.
theory T'.
type in'_t, out'_t.
module type O' = {
proc o(_: in'_t): out'_t
}.
module type D' (O : O') = {
proc d(): bool
}.
module Count' (O : O') : O' = {
var c : int
proc o(x) = {
var r;
r <@ O.o(x);
c <- c + 1;
return r;
}
}.
end T'.
type in_t, out_t.
clone import T' as Goal with
type in'_t <= in_t,
type out'_t <= out_t
proof *.
section.
declare module O <: O' { -Count' }.
declare module D <: D' { -Count', -O }.
declare op q : { int | 0 <= q } as ge0_q.
declare axiom D_count (O <: O' { -Count', -D }) c:
hoare [D(Count'(O)).d: Count'.c = c ==> Count'.c <= c + q].
local clone T as Hyp with
type in_t <- in_t,
type out_t <- out_t
proof *.
hoare toto P:
D(O).d: true ==> P q (glob O) res.
proof.
move: (Hyp.toto O D q ge0_q _ P).
+ move=> O0 c.
apply: (D_count O c). (* righteous failure! *)
It is possible that this could be worked through without much change to the libraries with support for nested sections, but the problem is also a strong indicator that our libraries should assume less and give stronger results. I propose that the general counting restrictions in the standard library be replaced with only those counting restrictions actually required for the proof to go through (counting with a specific implementation of the oracles), and to make an effort to minimize the assumptions on counting we need to make in the library by properly treating query count as a distinguishing behaviour. This will make our results more precise, and our libraries more general.
There is an issue that arises from query counting as we currently do it in generic results (with a broad restriction that the adversary must not make more than q queries regardless of the oracles they interact with). An example of where this fails is below. One way of avoiding the failure is to pollute the top-level statement with restrictions relevant only to the proof.
It is possible that this could be worked through without much change to the libraries with support for nested sections, but the problem is also a strong indicator that our libraries should assume less and give stronger results. I propose that the general counting restrictions in the standard library be replaced with only those counting restrictions actually required for the proof to go through (counting with a specific implementation of the oracles), and to make an effort to minimize the assumptions on counting we need to make in the library by properly treating query count as a distinguishing behaviour. This will make our results more precise, and our libraries more general.