Require Import listT.
Require Import POLY_ax.
Require Import Ring_cat.
Require Import Mod_IGA.

Set Implicit Arguments.
Unset Strict Implicit.

Module I_G_A(op:Op_Expr).
Import op.
Import E.


Definition null_Zq:Zq:=OZ.
Definition unit_Zq:Zq:=IZ.




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.

Fixpoint multIO_list (f : Sec -> Zq) (e : listT (Expr Sec)) (a : listT Zq) {struct a} : Zq:=
  match a with
  | nilT =>  null_Zq
  | consT b bs =>
      match e with
      | nilT =>  null_Zq
      | consT x xs => (add_Zq (mult_Zq (Eval Sec f x) b) (multIO_list f xs bs))
      end
  end.

(* in order for the hash function to be random, we factor it out *)

Variable IdealHash:Zq->Zq->Zq->Val.


(* Signed encrypted messages *)

(* a signed encrypted message has the form: (g^r,mg^(rx),c,z) 
					   where c=H(g^s,g^r,mg^(rx)) and z=s+cr
In Run we consider all ciphertext to have form: (f_i,f_j,c',f_k)
					   where f_i,f_j,f_k belong to step output 
						 and c' belongs to hash output *)
Definition IdealCipher:= (ProdT (listT Zq) (listT Zq)  Val (listT Zq)).

Definition Cipher:= ProdT Zq  Zq  Zq  Zq.

(* this function determines if a ciphertext is valid i.e, 
 (g^r,mg^(rx),c,z) is valid if c=H(g^z(g^r)^-c,g^r,mg^(rx))  *)
Parameter ValidCipher : Cipher -> Prop.

(* we take 3 step's output f_i,f_j,f_k and we return H(f_i,f_j,f_k) belongs to Val 
(IdealHashQuery f_i,f_j,f_k c') =>c'=H(f_i,f_j,f_k)  *)
Definition HashQuery := (ProdT Zq Zq Zq Val).



Definition IdealHashQuery:=(ProdT (listT Zq) (listT Zq) (listT Zq) Val).

(* we use the list of exponents 
Definition IdealHashQuery (f:Sec->Zq)(input:(listT (Expr Sec))): (ProdT (listT (Expr Val)) (listT (Expr Val)) (listT (Expr Val)) Val):=
(quadT (multIO_list f input (FstT HashQuery))  (multIO_list f input (SndT HashQuery)) (multIO_list f input (TrdT HashQuery)) (? (FthT HashQuery)) .
*)

Inductive Run : Type :=
  | nil : Run
  | mexstep :  Run -> (listT Zq) ->  Run
  | hashstep: Run -> IdealHashQuery -> Run
  | decstep: Run ->  IdealHashQuery->Zq -> Run.

(* normally hash's output should be a list of Val (all results H(f_i,f_j,f_k)) 
   but we need to keep a trace of the input's elements of H *)
Fixpoint IdealOutput(r:Run):(listT  (ProdT (listT Zq) (listT Zq) (listT Zq) Val)):=
  match r with 
  | nil =>nilT _
  | mexstep r' e => IdealOutput r'
  | hashstep r' (quadT a b d c) => consT (quadT a b d c) (IdealOutput r')
  | decstep r' _ _ =>IdealOutput r'
end.

(* this is the hash's output (all results H(f_i,f_j,f_k)) in Zq *)
Definition HashRecord(r: Run)(rom:Val->Zq):(listT Zq):=
mapT rom (list_fth_Prod (IdealOutput r)).


(* we just return the list of exponents *)
Fixpoint StepList(r:Run):listT (listT Zq):=
  match r with 
  | nil =>nilT _
  | mexstep r' e =>consT e  (StepList r')
  | hashstep r' _ =>StepList r' 
  | decstep r' _ _ => StepList r'
end.

Require Import eqZq.


Fixpoint StepOutput(r:Run)(f:Sec->Zq){struct r} :listT Zq:=
  match r with 
  | nil =>nilT _
  | mexstep r' e =>consT (multIO_list f input e) (StepOutput r' f )
  | hashstep r' _ =>StepOutput r' f 
  | decstep r' _ _ =>StepOutput r' f 
end.


(* for (g1,g2,g3,g4):listT (Expr Sec) and (a1,a2,a3,a4):listT Zq
computes  g1^a1.g2^a2.g3^a3.g4^a4 *)
Parameter mex:(listT (Expr Sec))->(listT Zq)->(Expr Sec).


Fixpoint mex_Output (r:Run){struct r}:(listT (Expr Sec)):=
  match r with nil => nilT _
           | (mexstep r' e) => (consT (mex input e) (mex_Output r' ))
	   | hashstep r' _ =>(mex_Output r')
           | decstep r' _ _ =>(mex_Output r' )
  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):= ListPred  Exprnon0 (gen_coll_test (mex_Output r )).


Definition ConstrRun (r : Run) :=
  GoodOutput r .




(* 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 Collisions(r:Run) (f:Sec ->Zq):=
exists e:(Expr Sec) , InT e (gen_coll_test (mex_Output r )) /\ Evalstozero f e.


Axiom dec_col_aux:forall (r:Run)(f:Sec->Zq),
   {Collisions r f }+{~Collisions r f }.

Require Import prob.

Lemma dec_col:forall (r:Run),dec_pred (Sec -> Zq) (fun f :  (Sec -> Zq) =>Collisions r f ).
unfold dec_pred.
intros.
apply dec_col_aux.
Qed.


Definition EvColl(r:Run):=Build_Event  (Sec -> Zq) (fun f :  (Sec -> Zq) =>Collisions r f ) (dec_col r ).

Definition Output(r: Run) (sec:Sec->Zq)(rom:Val->Zq): (listT Zq):=
appT  (StepOutput r sec) (HashRecord r rom).


Definition make_pol(l:listT Zq)(input:listT (Expr Sec)):Poly n Call:=
        transl (mult_IO add_Expr mult_Expr  inj_Sec OZ input l) .

Definition input1:listT (Expr Sec):=(consT (inj_Sec unit_Zq) (consT (inj_Sec null_Zq) (consT (inj_Sec null_Zq) (consT (inj_Sec null_Zq) (nilT _))))).


(* to eliminate interactions with the decryptor we define an extractor 
   if the polynomial construct by the input's elements of H i.e,
(log((FstT hash_out)*(SndT hash_out)^(FthT hash_out))), is constant we find the plaintext  *)

Require Import Pol_is_ring.

(* on ecrit z(x)-z(c)=0 au lieu de z(x)=z(c) *)
(* ceci represente le poly z(x)-z(c) *)
Definition Extract(hash_out:(ProdT (listT Zq) (listT Zq) (listT Zq) Val))(z:Zq)(rom:Val->Zq):=
(add_pol 
(add_pol  (make_pol (FstT hash_out) input) (mult_cte  (Call:=Call) (rom (FthT hash_out)) (make_pol (SndT hash_out) input)))
(opp_pol (mk_cte Zq n z))).

Axiom dec_extr:forall (hash_out:(ProdT (listT Zq) (listT Zq) (listT Zq) Val))(z:Zq)(rom:Val->Zq)(x:Sec->Zq),
{(eqZq (eval_poly (Call:=Call) (n:=n)   (Extract hash_out z rom )  (Fins2list x)) OZ)}+
{~(eqZq (eval_poly (Extract hash_out z rom )  (Fins2list x)) OZ)}.

Lemma dec_Extract:forall (hash_out:(ProdT (listT Zq) (listT Zq) (listT Zq) Val))(z:Zq),
dec_pred (prodT (Val->Zq) (Sec->Zq)) (fun x :(prodT (Val->Zq) (Sec->Zq))=>(eqZq (eval_poly  (Extract hash_out z (fstT x) )  (Fins2list (sndT x))) OZ)).
unfold dec_pred;intros.
apply dec_extr.
Qed.

Definition eq_Extr_0(rom:Val->Zq)(x:Sec->Zq)(hash_out:(ProdT (listT Zq) (listT Zq) (listT Zq) Val))(z:Zq):Prop:=
eqZq (eval_poly (Call:=Call) (n:=n)   (Extract hash_out z rom  )  (Fins2list x)) OZ.

Require Import listT.
Fixpoint DecOutput_h(r:Run):listT IdealHashQuery:=
match r with nil => nilT _
           | mexstep r' _ => DecOutput_h r'
	   | hashstep r' _ =>DecOutput_h r'
           | decstep r' h z=>consT h (DecOutput_h r')
  end.

Fixpoint DecOutput_z(r:Run):listT Zq:=
match r with nil => nilT _
           | mexstep r' _ => DecOutput_z r'
	   | hashstep r' _ =>DecOutput_z r'
           | decstep r' h z=>consT z (DecOutput_z r')
  end.


Definition Extractor(r:Run)(rom:Val->Zq)(x:Sec->Zq):Prop:=
ListPred_Or  (eq_Extr_0 rom x) (DecOutput_h r) (DecOutput_z r).


Fixpoint nb_inter(r:Run):nat:=
  match r with 
          | nil => O
          | mexstep r' _ => nb_inter r'
          | hashstep r' _  => nb_inter r'
          | decstep r' _ _ => S (nb_inter r')
  end.

Fixpoint mex_step(r:Run):nat:=
  match r with 
          | nil => O
          | mexstep r' _ =>S (mex_step  r')
          | hashstep r' _  =>  mex_step r'
          | decstep r' _ _ =>mex_step  r'
  end.

Definition step(r:Run):nat:=nb_inter r+mex_step r.


Lemma length_step : forall (r :Run), lengthT (mex_Output r ) = mex_step r.
simple induction r.
simpl in |- * .
auto.
intros.
simpl in |- * .
auto.
simpl;intros.
auto.
simpl;intros.
auto.
Qed.


Hypotheses Nb_Inter:forall r:Run,(le (nb_inter r) card).



Axiom dec_Extr_aux:forall (r:Run)(rom:Val->Zq)(x:Sec->Zq),
                          {(Extractor r rom  x)}+{~(Extractor r rom  x)}.

Lemma dec_Extr:forall (r:Run),
                                       dec_pred (prodT (Val->Zq) (Sec->Zq)) (fun x : (prodT (Val->Zq) (Sec->Zq)) =>(Extractor r (fstT x)  (sndT x))).
unfold dec_pred.
intros.
apply dec_Extr_aux.
Qed.


Definition Extr(r:Run):=(Build_Event (prodT (Val->Zq) (Sec->Zq)) (fun x :(prodT (Val->Zq) (Sec->Zq)) => (Extractor r (fstT x)  (sndT x))) (dec_Extr r )).


Inductive SecFound:(Sec -> Zq) -> (Sec -> Zq) ->(Val->Zq)-> Run -> Sec -> Prop :=
  | secret_found_wc :
      forall (f g : Sec -> Zq) (rom:Val->Zq)(r : Run) (x : Sec),
      Collisions r f   -> SecFound f g rom r  x
  |secret_found_wextr :  forall (f g : Sec -> Zq) (rom:Val->Zq)(r : Run)  (x : Sec),
      ~  Collisions r f ->Extractor r rom  f-> SecFound f g rom r  x
  | secret_found_woc :
      forall (f g : Sec -> Zq) (rom:Val->Zq)(r : Run)  (x : Sec),
      ~  Collisions r f  -> ~ Extractor r rom  f->eqZq (f x) (g x) -> SecFound f g rom r x.


Axiom SF_dec_aux:forall (fg : PdT (Sec -> Zq) (Sec -> Zq) (Val->Zq))(r : Run) (x : Sec), {SecFound  (FtT fg) (SdT fg) (TdT fg) r x}+{~(SecFound (FtT fg) (SdT fg) (TdT fg) r x)}.

Lemma SF_dec:forall (r : Run)  (x : Sec),dec_pred (PdT (Sec -> Zq) (Sec -> Zq) (Val->Zq)) (fun fg : PdT (Sec -> Zq) (Sec -> Zq) (Val->Zq)=>SecFound  (FtT fg) (SdT fg) (TdT fg) r  x).
unfold dec_pred.
intros.
apply SF_dec_aux.
Qed.


Axiom dec_Zq:forall a b:Zq,{eqZq a b}+{~(eqZq a b)}.

Definition Ev_guess (x : Sec) :
  Event (PdT (Sec -> Zq) (Sec -> Zq) (Val->Zq)) :=
  Build_Event (PdT (Sec -> Zq) (Sec -> Zq) (Val->Zq))
    (fun fg => eqZq (FtT fg x) (SdT fg x))
    (fun fg => dec_Zq (FtT fg x) (SdT fg x)).


End  I_G_A.