https://github.com/EasyCrypt/easycrypt
Tip revision: 180d323ca283478521f58c6bff6e0842d21f0d7d authored by Pierre-Yves Strub on 27 January 2020, 13:48:30 UTC
Merge branch 'deploy-extended-tests' into deploy-simpler-xpaths
Merge branch 'deploy-extended-tests' into deploy-simpler-xpaths
Tip revision: 180d323
Hybrid.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
require import AllCore FSet Finite Distr DInterval.
require import OldMonoid.
require Means.
type input.
type output.
type inleaks.
type outleaks.
type outputA.
(* -------------------------------------------------------------------- *)
(* Wrappers for counting *)
module Count = {
var c : int
proc init () : unit = {
c <- 0;
}
proc incr () : unit = {
c <- c + 1;
}
}.
module type Adv = {
proc main() : outputA
}.
module AdvCount (A : Adv) = {
proc main() : outputA = {
var r : outputA;
Count.init();
r <@ A.main();
return r;
}
}.
module type Orcl = {
proc orcl(m : input) : output
}.
module OrclCount (O : Orcl) = {
proc orcl(m : input) : output = {
var r : output;
r <@ O.orcl(m);
Count.incr();
return r;
}
}.
(* -------------------------------------------------------------------- *)
(* Hybrid oracles and games *)
op q : { int | 0 < q } as q_pos.
module type AdvOrcl (O : Orcl) = {
proc main () : outputA
}.
module type Orclb = {
proc leaks (il : inleaks) : outleaks
proc orclL (m : input) : output
proc orclR (m : input) : output
}.
module L (Ob : Orclb) : Orcl = {
proc orcl = Ob.orclL
}.
module R (Ob : Orclb) : Orcl = {
proc orcl = Ob.orclR
}.
module type AdvOrclb (Ob : Orclb, O : Orcl) = {
proc main () : outputA
}.
module Orcln (A : AdvOrcl, O : Orcl) = AdvCount(A(OrclCount(O))).
module Ln(Ob : Orclb, A : AdvOrclb) = Orcln(A(Ob), L(Ob)).
module Rn(Ob : Orclb, A : AdvOrclb) = Orcln(A(Ob), R(Ob)).
(* Hybrid oracle:
Use left oracle for queries < l0,
oracle O for queries = l0, and
right oracle for queries > l0. *)
module HybOrcl (Ob : Orclb, O : Orcl) = {
var l, l0 : int
proc orcl(m:input):output = {
var r : output;
if (l0 < l) r <@ Ob.orclL(m);
elif (l0 = l) r <@ O.orcl(m);
else r <@ Ob.orclR(m);
l <- l + 1;
return r;
}
}.
(* Hybrid game: Adversary has access to
leaks, left, right, and hybrid oracle *)
module HybGame(A:AdvOrclb, Ob:Orclb, O:Orcl) = {
module LR = HybOrcl(Ob,O)
module A = A(Ob,LR)
proc main() : outputA = {
var r : outputA;
HybOrcl.l0 <$ [0..q-1];
HybOrcl.l <- 0;
r <@ A.main();
return r;
}
}.
clone import Means as M with
type input <- int,
type output <- outputA,
op d <- [0..q-1].
(* -------------------------------------------------------------------- *)
(* Prove that it is equivalent to consider n or 1 calls to the oracle *)
section.
declare module Ob : Orclb {Count,HybOrcl}.
declare module A : AdvOrclb {Count,HybOrcl,Ob}.
(* Hybrid game where index is fixed, not sampled *)
local module HybGameFixed (O : Orcl) = {
module LR = HybOrcl(Ob,O)
module A = A(Ob,LR)
proc work(x : int) : outputA = {
var r : outputA;
HybOrcl.l <- 0; HybOrcl.l0 <- x;
r <@ A.main();
return r;
}
}.
local equiv Obleaks : Ob.leaks ~ Ob.leaks : ={il,glob Ob} ==> ={res,glob Ob}.
proof. by proc true. qed.
local equiv Oborcl1 : Ob.orclL ~ Ob.orclL : ={m,glob Ob} ==> ={res,glob Ob}.
proof. by proc true. qed.
local equiv Oborcl2 : Ob.orclR ~ Ob.orclR : ={m,glob Ob} ==> ={res,glob Ob}.
proof. by proc true. qed.
local lemma GLB_WL &m (p:glob A -> glob Ob -> int -> outputA -> bool):
Pr[Ln(Ob,HybGame(A)).main() @ &m : p (glob A) (glob Ob) HybOrcl.l res /\ Count.c <= 1] =
Pr[Rand(HybGameFixed(L(Ob))).main() @ &m : p (glob A) (glob Ob) HybOrcl.l (snd res)].
proof.
byequiv (_ : ={glob A, glob Ob} ==>
={glob A, glob Ob,glob HybOrcl} /\ res{1} = snd res{2} /\
Count.c{1} <= 1) => //;proc.
inline{1} HybGame(A, Ob, OrclCount(L(Ob))).main; inline{2} HybGameFixed(L(Ob)).work;wp.
call (_: ={glob Ob, glob HybOrcl} /\ Count.c{1} = (HybOrcl.l0{1} < HybOrcl.l{1}) ? 1 : 0).
proc;wp.
if => //;first by call Oborcl1;skip;progress => //; smt.
if => //.
inline{1} OrclCount(L(Ob)).orcl Count.incr.
by wp;call Oborcl1;wp;skip;progress => //;smt.
by call Oborcl2;skip;progress => //; smt.
by conseq Obleaks.
by conseq Oborcl1.
by conseq Oborcl2.
swap{1} 1 2;inline{1} Count.init.
by wp;rnd;wp;skip;progress => //;smt.
qed.
local lemma GRB_WR &m (p:glob A -> glob Ob -> int -> outputA -> bool):
Pr[Rn(Ob,HybGame(A)).main() @ &m : p (glob A) (glob Ob) HybOrcl.l res /\ Count.c <= 1] =
Pr[Rand(HybGameFixed(R(Ob))).main() @ &m : p (glob A) (glob Ob) HybOrcl.l (snd res)].
proof.
byequiv (_ : ={glob A, glob Ob} ==>
={glob A, glob Ob, glob HybOrcl} /\ res{1} = snd res{2} /\
Count.c{1} <= 1) => //;proc.
inline{1} HybGame(A, Ob, OrclCount(R(Ob))).main; inline{2} HybGameFixed(R(Ob)).work;wp.
call (_: ={glob Ob, glob HybGame} /\ Count.c{1} = (HybOrcl.l0{1} < HybOrcl.l{1}) ? 1 : 0).
proc;wp.
if => //;first by call Oborcl1;skip;progress => //; smt.
if => //.
inline{1} OrclCount(R(Ob)).orcl Count.incr.
by wp;call Oborcl2;wp;skip;progress => //;smt.
by call Oborcl2;skip;progress => //; smt.
by conseq Obleaks.
by conseq Oborcl1.
by conseq Oborcl2.
swap{1} 1 2;inline{1} Count.init.
by wp;rnd;wp;skip;progress => //;smt.
qed.
axiom losslessL: islossless Ob.leaks.
axiom losslessOb1: islossless Ob.orclL.
axiom losslessOb2: islossless Ob.orclR.
axiom losslessA (Ob0 <: Orclb{A}) (LR <: Orcl{A}):
islossless LR.orcl =>
islossless Ob0.leaks => islossless Ob0.orclL => islossless Ob0.orclR =>
islossless A(Ob0, LR).main.
local lemma WL0_GLA &m (p:glob A -> glob Ob -> int -> outputA -> bool):
Pr[HybGameFixed(L(Ob)).work(0) @ &m : p (glob A) (glob Ob) HybOrcl.l res /\ HybOrcl.l <= q] =
Pr[Ln(Ob,A).main() @ &m : p (glob A) (glob Ob) Count.c res /\ Count.c <= q ].
proof.
byequiv (_ : ={glob A, glob Ob} /\ x{1}=0 ==>
(HybOrcl.l{1} <= q) = (Count.c{2} <= q) /\
(Count.c{2} <= q =>
={glob A, glob Ob,res} /\ HybOrcl.l{1} = Count.c{2})) => //;
[proc | smt].
call (_: q < Count.c,
={glob Ob} /\ HybOrcl.l0{1} = 0 /\ HybOrcl.l{1} = Count.c{2} /\ 0 <= HybOrcl.l{1},
HybOrcl.l0{1} = 0 /\ q < HybOrcl.l{1}).
by apply losslessA.
proc;inline{2} Count.incr;wp.
if{1};first by call Oborcl1;wp;skip;progress => //;smt.
rcondt{1} 1; first by move=> &m0;skip;smt.
by wp;call Oborcl1;wp;skip;progress => //;smt.
move=> &m2 _;proc.
rcondt 1; first by skip;smt.
by wp;call losslessOb1;skip;smt.
by move=> &m1;proc;inline Count.incr;wp;call losslessOb1;wp;skip;smt.
by conseq Obleaks.
move=> &m2 _;conseq losslessL.
move=> &m1; conseq losslessL.
by conseq Oborcl1.
move=> &m2 _;conseq losslessOb1.
move=> &m1; conseq losslessOb1.
by conseq Oborcl2.
move=> &m2 _;conseq losslessOb2.
move=> &m1; conseq losslessOb2.
by inline{2} Count.init;wp;skip;smt.
qed.
local lemma WRq_GRA &m (p:glob A -> glob Ob -> int -> outputA -> bool):
Pr[HybGameFixed(R(Ob)).work((q-1)) @ &m : p (glob A) (glob Ob) HybOrcl.l res /\ HybOrcl.l <= q] =
Pr[Rn(Ob,A).main() @ &m : p (glob A) (glob Ob) Count.c res /\ Count.c <= q ].
proof.
byequiv (_ : ={glob A, glob Ob} /\ x{1}=q-1 ==>
(HybOrcl.l{1} <= q) = (Count.c{2} <= q) /\
(Count.c{2} <= q =>
={glob A, glob Ob, res} /\ HybOrcl.l{1} = Count.c{2})) => //;
[proc | smt].
call (_: q < Count.c,
={glob Ob} /\ HybOrcl.l0{1} = q-1 /\ HybOrcl.l{1} = Count.c{2} /\ 0 <= HybOrcl.l{1},
HybOrcl.l0{1} = q-1 /\ q < HybOrcl.l{1}).
by apply losslessA.
proc;inline{2} Count.incr;wp.
if{1};first by call{1} losslessOb1;call{2} losslessOb2;wp;skip; smt.
if{1};
first by wp;call Oborcl2;wp;skip;progress => //;smt.
by call Oborcl2;wp;skip;progress => //;smt.
move=> &m2 _;proc.
rcondt 1; first by skip;smt.
by wp;call losslessOb1;skip; smt.
move=> &m1;proc;inline Count.incr;wp;call losslessOb2;wp;skip;smt.
by conseq Obleaks.
move=> &m2 _;conseq losslessL.
move=> &m1; conseq losslessL.
by conseq Oborcl1.
move=> &m2 _;conseq losslessOb1.
move=> &m1; conseq losslessOb1.
by conseq Oborcl2.
move=> &m2 _;conseq losslessOb2.
move=> &m1; conseq losslessOb2.
by inline{2} Count.init;wp;skip;smt.
qed.
local lemma WLR_shift &m v (p:glob A -> glob Ob -> int -> outputA -> bool):
1 <= v <= q-1 =>
Pr[HybGameFixed(L(Ob)).work(v) @ &m: p (glob A) (glob Ob) HybOrcl.l res] =
Pr[HybGameFixed(R(Ob)).work((v-1)) @ &m : p (glob A) (glob Ob) HybOrcl.l res].
proof.
move=> Hv;byequiv (_: ={glob A,glob Ob} /\ x{1} = v /\ x{2} = v-1 ==>
={glob A,glob Ob, HybOrcl.l, res}) => //.
proc.
call (_: ={glob Ob, HybOrcl.l} /\ HybOrcl.l0{1} = v /\ HybOrcl.l0{2} = v-1).
proc.
if{1}; first by rcondt{2} 1;[move=> &m0;skip;smt | wp;call Oborcl1].
if{1};first by rcondt{2} 1;
[move=> &m0;skip;smt | wp;call Oborcl1;wp].
rcondf{2} 1;first by move=> &m0;skip;smt.
by if{2};wp;call Oborcl2;wp.
by conseq Obleaks.
by conseq Oborcl1.
by conseq Oborcl2.
by wp.
qed.
(* TODO : move this *)
lemma Mrplus_inter_shift (i j k:int) f:
Mrplus.sum f (oflist (List.Iota.iota_ i (j - i + 1))) =
Mrplus.sum (fun l, f (l + k)) (oflist (List.Iota.iota_ (i-k) (j - i + 1))).
proof strict.
rewrite (Mrplus.sum_chind f (fun l, l - k) (fun l, l + k)) /=;first smt.
congr => //.
apply FSet.fsetP => x.
rewrite imageP !mem_oflist !List.Iota.mem_iota; split.
move=> [y];rewrite !mem_oflist !List.Iota.mem_iota;smt.
move=> Hx;exists (x+k);rewrite !mem_oflist !List.Iota.mem_iota;smt.
qed.
lemma Hybrid &m (p:glob A -> glob Ob -> int -> outputA -> bool):
let p' = fun ga ge l r, p ga ge l r /\ l <= q in
Pr[Ln(Ob,HybGame(A)).main() @ &m : p' (glob A) (glob Ob) HybOrcl.l res /\ Count.c <= 1] -
Pr[Rn(Ob,HybGame(A)).main() @ &m : p' (glob A) (glob Ob) HybOrcl.l res /\ Count.c <= 1] =
1%r/q%r * (
Pr[Ln(Ob,A).main() @ &m : p' (glob A) (glob Ob) Count.c res] -
Pr[Rn(Ob,A).main() @ &m : p' (glob A) (glob Ob) Count.c res]).
proof.
move=> p';rewrite (GLB_WL &m p') (GRB_WR &m p').
simplify p'; rewrite -(WL0_GLA &m p) -(WRq_GRA &m p).
cut Hint : forall x, support [0..q - 1] x <=> mem (oflist (List.Iota.iota_ 0 q)) x.
by move=> x; rewrite !mem_oflist !List.Iota.mem_iota supp_dinter; smt.
cut Hfin: is_finite (support [0..q - 1]).
exists (List.Iota.iota_ 0 q).
by rewrite List.Iota.iota_uniq=> /= x; rewrite List.Iota.mem_iota supp_dinter=> /#.
cut Huni : forall (x : int), x \in [0..q - 1] => mu1 [0..q - 1] x = 1%r / q%r.
by move=> x Hx; rewrite dinter1E /=; smt(supp_dinter).
pose ev :=
fun (_j:int) (g:glob HybGameFixed(L(Ob))) (r:outputA),
let (l,l0,ga,ge) = g in p ga ge l r /\ l <= q.
cut := M.Mean_uni (HybGameFixed(L(Ob))) &m ev (1%r/q%r) _ _ => //; simplify ev => ->.
cut := M.Mean_uni (HybGameFixed(R(Ob))) &m ev (1%r/q%r) _ _ => //; simplify ev => ->.
cut -> : oflist (to_seq (support [0..q - 1])) = oflist (List.Iota.iota_ 0 q).
by apply FSet.fsetP => x; rewrite !mem_oflist mem_to_seq// smt.
cut {1}->: oflist (List.Iota.iota_ 0 q) = oflist (List.Iota.iota_ 1 (q - 1)) `|` fset1 0.
by apply/fsetP=> x; rewrite !inE !mem_oflist !List.Iota.mem_iota; smt.
cut ->: oflist (List.Iota.iota_ 0 q) = oflist (List.Iota.iota_ 0 (q - 1)) `|` fset1 (q - 1).
by apply/fsetP=> x; rewrite !inE !mem_oflist !List.Iota.mem_iota; smt.
rewrite Mrplus.sum_add /=.
by rewrite mem_oflist List.Iota.mem_iota.
rewrite Mrplus.sum_add /=.
by rewrite mem_oflist List.Iota.mem_iota.
cut Hq : q%r <> 0%r by smt.
fieldeq => //.
cut ->: q - 1 = q - 1 - 1 - 0 + 1 by smt.
rewrite (Mrplus_inter_shift 0 (q - 1 - 1) (-1)) /=.
have ->: q - 1 - 1 + 1 = q - 1 by smt.
rewrite -(Mrplus.sum_comp (( * ) (-q%r))) 1..2:smt.
rewrite -(Mrplus.sum_comp (( * ) (q%r))) 1..2:smt.
rewrite Mrplus.sum_add2 /=.
rewrite (Mrplus.NatMul.sum_const 0%r) /Mrplus.NatMul.( * ) //=.
move=> x; rewrite mem_oflist List.Iota.mem_iota=> Hx.
cut:= WLR_shift &m x p' _; 1:smt. simplify p'=> ->.
by smt.
qed.
end section.
(* -------------------------------------------------------------------- *)
(* Simplified variant: Assume that A calls the oracle at most q times. *)
section.
declare module Ob : Orclb {Count,HybOrcl}.
declare module A : AdvOrclb {Count,HybOrcl,Ob}.
axiom A_call : forall (O<:Orcl{Count,A}), hoare [ Orcln(A(Ob), O).main : true ==> Count.c <= q ].
local module Al = Orcln(A(Ob),HybOrcl(Ob,L(Ob))).
local module Bl = {
proc main() : outputA = {
var r : outputA;
HybOrcl.l0 <$ [0..q-1];
HybOrcl.l <- 0;
r <@ Al.main();
return r;
}
}.
local module Ar = Orcln(A(Ob),HybOrcl(Ob,R(Ob))).
local module Br = {
proc main() : outputA = {
var r : outputA;
HybOrcl.l0 <$ [0..q-1];
HybOrcl.l <- 0;
r <@ Ar.main();
return r;
}
}.
local equiv B_Bl : HybGame(A,Ob,L(Ob)).main ~ Bl.main :
={glob A, glob Ob} ==>
={glob A, glob Ob, glob HybOrcl, res} /\ Count.c{2} = HybOrcl.l{2} /\ Count.c{2} <= q.
proof.
conseq [-frame] (_: ={glob A, glob Ob} ==> ={glob A, glob Ob, glob HybOrcl, res}) _
(_:true ==> Count.c = HybOrcl.l /\ Count.c <= q).
conseq [-frame] (_:true ==> Count.c = HybOrcl.l) (_: true ==> Count.c <= q).
proc; call (A_call (<:HybOrcl(Ob,L(Ob)))) => //.
proc;inline *;wp;call (_ : Count.c = HybOrcl.l).
proc;inline *;wp; by conseq (_: _ ==> true) => //.
conseq (_: _ ==> true) => //. conseq (_: _ ==> true) => //. conseq (_: _ ==> true) => //.
by wp.
proc;inline Al.main;wp. call (_: ={glob Ob, glob HybOrcl}).
proc;inline *;wp. sp;if => //. call (_:true) => //.
if => //. wp;call (_:true) => //. wp=> //. call (_:true) => //.
proc (={glob HybOrcl}) => //. proc (={glob HybOrcl}) => //. proc (={glob HybOrcl}) => //.
inline *;wp;rnd => //.
qed.
local equiv B_Br : HybGame(A,Ob,R(Ob)).main ~ Br.main :
={glob A, glob Ob} ==>
={glob A, glob Ob, glob HybOrcl, res} /\ Count.c{2} = HybOrcl.l{2} /\ Count.c{2} <= q.
proof.
conseq [-frame] (_: ={glob A, glob Ob} ==> ={glob A, glob Ob, glob HybOrcl, res}) _
(_:true ==> Count.c = HybOrcl.l /\ Count.c <= q).
conseq [-frame] (_:true ==> Count.c = HybOrcl.l) (_: true ==> Count.c <= q).
proc; call (A_call (<:HybOrcl(Ob,R(Ob)))) => //.
proc;inline *;wp;call (_ : Count.c = HybOrcl.l).
proc;inline *;wp; by conseq (_: _ ==> true) => //.
conseq (_: _ ==> true) => //. conseq (_: _ ==> true) => //. conseq (_: _ ==> true) => //.
by wp.
proc;inline Ar.main;wp. call (_: ={glob Ob, glob HybOrcl}).
proc;inline *;wp. sp;if => //. call (_:true) => //.
if => //. wp;call (_:true) => //. wp=> //. call (_:true) => //.
proc (={glob HybOrcl}) => //. proc (={glob HybOrcl}) => //. proc (={glob HybOrcl}) => //.
inline *;wp;rnd => //.
qed.
local lemma Pr_Bl &m (p:glob A -> glob Ob -> int -> outputA -> bool):
Pr[HybGame(A,Ob,L(Ob)).main() @ &m : p (glob A) (glob Ob) HybOrcl.l res] =
Pr[HybGame(A,Ob,L(Ob)).main() @ &m : p (glob A) (glob Ob) HybOrcl.l res /\ HybOrcl.l <= q].
proof.
cut -> :
Pr[HybGame(A,Ob,L(Ob)).main() @ &m : p (glob A) (glob Ob) HybOrcl.l res] =
Pr[Bl.main() @ &m : p (glob A) (glob Ob) HybOrcl.l res /\ HybOrcl.l <= q].
byequiv B_Bl => //.
apply eq_sym. byequiv B_Bl => //.
qed.
local lemma Pr_Br &m (p:glob A -> glob Ob -> int -> outputA -> bool):
Pr[HybGame(A,Ob,R(Ob)).main() @ &m : p (glob A) (glob Ob) HybOrcl.l res] =
Pr[HybGame(A,Ob,R(Ob)).main() @ &m : p (glob A) (glob Ob) HybOrcl.l res /\ HybOrcl.l <= q].
proof.
cut -> :
Pr[HybGame(A,Ob,R(Ob)).main() @ &m : p (glob A) (glob Ob) HybOrcl.l res] =
Pr[Br.main() @ &m : p (glob A) (glob Ob) HybOrcl.l res /\ HybOrcl.l <= q].
byequiv B_Br => //.
apply eq_sym. byequiv B_Br => //.
qed.
axiom losslessL: islossless Ob.leaks.
axiom losslessOb1: islossless Ob.orclL.
axiom losslessOb2: islossless Ob.orclR.
axiom losslessA (Ob0 <: Orclb{A}) (LR <: Orcl{A}):
islossless LR.orcl =>
islossless Ob0.leaks => islossless Ob0.orclL => islossless Ob0.orclR =>
islossless A(Ob0, LR).main.
lemma Hybrid_restr &m (p:glob A -> glob Ob -> int -> outputA -> bool):
Pr[HybGame(A,Ob,L(Ob)).main() @ &m : p (glob A) (glob Ob) HybOrcl.l res] -
Pr[HybGame(A,Ob,R(Ob)).main() @ &m : p (glob A) (glob Ob) HybOrcl.l res] =
1%r/q%r * (
Pr[Ln(Ob,A).main() @ &m : p (glob A) (glob Ob) Count.c res] -
Pr[Rn(Ob,A).main() @ &m : p (glob A) (glob Ob) Count.c res]).
proof.
pose p' := fun ga ge l r, p ga ge l r /\ l <= q.
cut -> : Pr[Ln(Ob,A).main() @ &m : p (glob A) (glob Ob) Count.c res] =
Pr[Ln(Ob,A).main() @ &m : p' (glob A) (glob Ob) Count.c res].
byequiv (_ : ={glob A, glob Ob} ==> ={glob A, glob Ob, Count.c, res} /\ Count.c{1} <= q) => //;
last by rewrite /p'.
conseq [-frame] (_: ={glob A, glob Ob} ==> ={glob A, glob Ob, Count.c, res}) (_ : true ==> Count.c <= q);
last by sim; proc (={Count.c}).
apply (A_call (<:L(Ob))).
cut -> : Pr[Rn(Ob,A).main() @ &m : p (glob A) (glob Ob) Count.c res] =
Pr[Rn(Ob,A).main() @ &m : p' (glob A) (glob Ob) Count.c res].
byequiv (_ : ={glob A, glob Ob} ==> ={glob A, glob Ob, Count.c, res} /\ Count.c{1} <= q) => //;
last by rewrite /p'.
conseq [-frame] (_: ={glob A, glob Ob} ==> ={glob A, glob Ob, Count.c, res}) (_ : true ==> Count.c <= q);
last by sim; proc (={Count.c}).
apply (A_call (<:R(Ob))).
rewrite (Pr_Bl &m p) (Pr_Br &m p).
cut := Hybrid Ob A _ _ _ _ &m p.
apply losslessL. apply losslessOb1. apply losslessOb2. apply losslessA.
move=> /= H. rewrite /p' -H.
congr; last congr.
byequiv (_ : ={glob A, glob Ob} ==> ={glob A, glob Ob, glob HybOrcl, res} /\ Count.c{2} <= 1) => //.
proc;inline *;wp.
call (_ : ={glob Ob, glob HybOrcl} /\ (if HybOrcl.l <= HybOrcl.l0 then Count.c = 0 else Count.c =1){2}).
proc. inline *;wp.
if => //. call (_: ={glob HybOrcl});auto; smt.
if => //. wp;call (_: ={glob HybOrcl});auto; smt. call (_: ={glob HybOrcl});auto; smt.
conseq (_: _ ==> ={res,glob Ob}) => //. sim.
conseq (_: _ ==> ={res,glob Ob}) => //. sim.
conseq (_: _ ==> ={res,glob Ob}) => //. sim.
auto;progress;smt.
byequiv (_ : ={glob A, glob Ob} ==> ={glob A, glob Ob, glob HybOrcl, res} /\ Count.c{2} <= 1) => //.
proc;inline *;wp.
call (_ : ={glob Ob, glob HybOrcl} /\ (if HybOrcl.l <= HybOrcl.l0 then Count.c = 0 else Count.c =1){2}).
proc. inline *;wp.
if => //. call (_: ={glob HybOrcl});auto; smt.
if => //. wp;call (_: ={glob HybOrcl});auto; smt. call (_: ={glob HybOrcl});auto; smt.
conseq (_: _ ==> ={res,glob Ob}) => //. sim.
conseq (_: _ ==> ={res,glob Ob}) => //. sim.
conseq (_: _ ==> ={res,glob Ob}) => //. sim.
auto;progress;smt.
qed.
end section.