Require Import ZArith.
Require Import listT.
Require Import Mod_GA.
(*-----------------------------------------------------------------------------                   Definition of a generic algorithm 
-----------------------------------------------------------------------------*)

Module  G_A (op:Op_Expr).

Import op.
Import E.


Inductive Run:Type:=
 erun:Run |
 step:Run->(listT Zq)->Run.

(* returns the number of steps of the run *)
Fixpoint steps (r : Run) : nat :=
  match r with
  | erun => 0
  | step r' _ => S (steps r')
  end.


Fixpoint Output (r:Run){struct r}:(listT (Expr Sec)):=
  match r with erun => nilT _
           | (step r' e) => (consT (mex input e) (Output r' ))
  end.



Definition list_min(a:(Expr Sec))(l:listT (Expr Sec)):listT (Expr Sec):=
mapT (min_Expr a) l.

(* returns the listT of all fi-fj  1<=i<j<=lengthT l*)
Fixpoint gen_coll_test(l:(listT (Expr Sec))):(listT (Expr Sec)):=
match l with 
  |nilT=>nilT _
  |consT x xs=>appT (list_min x xs) (gen_coll_test xs) 
    end.


Require Import POLY_ax.
(*returns True if for p:Expr Sec and x:Sec->Zq, p x=0
  where p is seen like a polynomial in Zq[Sec] *)
 Definition Evalstozero: (Sec ->  Zq) -> Expr Sec ->  Prop.
intros x e.
apply (eqZq (eval_poly (transl  e) (Fins2list x)) OZ).
Defined.
 
Axiom dec_Evalstozero:
 forall (e : Expr Sec) (x : Sec ->  Zq),
  ({ Evalstozero x e }) + ({ ~ Evalstozero x e }).

Require Import prob.
(* the event p=0 *)
 Definition Ev_Evalstozero(p:Expr Sec) :=
Build_Event (Sec ->  Zq) (fun (f : Sec ->  Zq) => Evalstozero f p) (dec_Evalstozero p). 

(* the event exists p in l s.t p=0 *)
 Definition Eq0 (l : listT (Expr Sec)) :=
   EvUnList (Sec ->  Zq) (mapT Ev_Evalstozero l).

(*returns True if we find a null element in l*)
 Fixpoint eq0 (x : Sec ->  Zq) (l : listT (Expr Sec)) {struct l} : Prop :=
 match l with
   nilT => False
  | consT p ps => Evalstozero x p \/ eq0 x ps
 end.

Definition Exprnon0(e:Expr Sec):=~(forall f:Sec->Zq,Evalstozero f e).



(* the outputs are "good" if 
    for all outputs a b, a-b<>0 *)
Definition GoodOutput(r:Run)(input:(listT (Expr Sec))):= ListPred  Exprnon0 (gen_coll_test (Output  r )).

Lemma length_step : forall (r :Run)(input:(listT (Expr Sec))), lengthT (Output r ) = steps r.
simple induction r.
simpl in |- *.
auto.
intros.
simpl in |- *.
auto.
Qed.


(* we have a non-trivial collision if we find an element w in the listT of all fi-fj  1<=i<j<=steps r, s.t, w=0 *)
Definition Coll (f:Sec ->Zq)(r:Run):=
exists e:(Expr Sec) , InT e (gen_coll_test (Output r )) /\ Evalstozero f e.

Axiom dec_col:
   forall (r : Run)  (f : Sec ->  Zq),
    ({ Coll  f r  }) + ({ ~ Coll  f r  }).
 
Definition Collisions (r : Run)  : Event (Sec ->  Zq) :=
   Build_Event
    (Sec ->  Zq) (fun (f : Sec ->  Zq) => Coll  f r ) (dec_col r  ).

(* we find a secret if we find a collision or if we find it arbitrarily *)
Inductive SecF :
    (Sec ->Zq)-> (Sec ->Zq)-> Run  -> Sec -> Prop :=
  | secret_found_wc :
      forall (f g: Sec -> Zq)(r : Run)(x : Sec),
      Coll f r  -> SecF f g r  x
  | secret_found_woc :
     forall (f g: Sec -> Zq)(r : Run)(x : Sec),
    ~ Coll f r -> (eqZq (f x) (g x)) -> SecF f g r  x.


Axiom SecF_dec :
    forall (r : Run) (x : Sec),
    dec_pred (prodT (Sec -> Zq) (Sec -> Zq))
      (fun fg => SecF (fstT fg) (sndT fg) r  x).


Definition EvSecF (r : Run) 
  (x : Sec) : Event (prodT (Sec -> Zq) (Sec -> Zq)) :=
  Build_Event (prodT (Sec -> Zq) (Sec -> Zq))
    (fun fg => (SecF (fstT fg) (sndT fg) r  x))
    (SecF_dec r x).



End G_A.