Require Import listT.
Require Import POLY_ax.
Require Import Ring_cat.
Require Import Mod_IGA_PA.

Set  Implicit Arguments.
Unset Strict Implicit.
 
Module interactive_Generic_algorithm(op:Op_Expr).
Import op.

(*the set of the encrypted messages *)
Parameter M:Type.

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.

(* we take 1 step's output f_i and an encrypted message m_i and we return H(f_i,m_i) belongs to Val 
  (IdealHashQuery f_i,m_i, c') =>c'=H(f_i,m_i)  *)
 Definition IdealHashQuery := PdT (listT Zq) M 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
 | signstep: Run ->IdealHashQuery -> Sec->  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 (PdT (listT Zq) M Val) :=
 match r with
   nil => nilT _
  | mexstep r' e => IdealOutput r'
  | hashstep r' (tripleT a m c) => consT (tripleT a m c) (IdealOutput r')
  | signstep r' _ _=> IdealOutput r'
 end.


(* ------------------------------- z=r+r*x ----------------------------------------*)
Definition mk_z(rom:Val->Zq)(r:Zq)(c:Expr Val)(x:Zq):Zq:=
(add_Zq (Eval Val rom c) (mult_Zq r x)).

(*input is the list 1,x *)

(* we return the list of all zj:=rj+cjx resulting from an interaction with the signer *)
(*peut etre ecrire avec z=log fi+ci*x avec input1 et make pol *)
Fixpoint IdealSign (R : Run) (rom : Val ->  Zq) (sec : Sec ->  Zq) {struct R}:
 listT Zq :=
 match R with
   nil => nilT _
  | mexstep r' e => IdealSign r' rom sec
  | hashstep r' _ => IdealSign r' rom sec
  | signstep r' (tripleT a m c) r => consT (mk_z rom (sec r) (Val2Expr c) (Eval Sec sec (headT OE (tailT  input)))) 
( IdealSign r' rom sec)
 end.

(* the list of all rj for an interaction with the signer *)
Fixpoint InpSign (R : Run) :
 listT (Expr Sec) :=
 match R with
   nil => nilT _
  | mexstep r' e =>InpSign  r' 
  | hashstep r' _ => InpSign r'
  | signstep r' _ r => consT (Sec2Expr r) (InpSign r' )
 end.

(* the list of all cj for an interaction with the signer *)
Fixpoint hashSign (R : Run) :
 listT  (PdT (listT Zq) M Val) :=
 match R with
   nil => nilT _
  | mexstep r' e =>hashSign   r' 
  | hashstep r' _ => hashSign r'
  | signstep r' (tripleT a m c) _ => consT (tripleT a m c) (hashSign r' )
 end.




Hypotheses L:forall r:Run,l<=lengthT (IdealOutput r).

(* this is the list c1,...,cl *)
Definition Hash_l(r:Run):listT (Expr Val):=mapT Val2Expr (mk_list_n_fst_elt l (list_td_PdT (hashSign r))).

(*Let us assume that we have l interactions with the signer
so we have a list inp_sign:=r1,...,rl *)
Definition inp_sign(r:Run):listT  (Expr Sec):=mk_list_n_fst_elt l (InpSign r).
 
Definition SignOutput(r:Run)(rom:Val->Zq)(sec:Sec->Zq):listT Zq:=mk_list_n_fst_elt l (IdealSign r rom sec).


(*input is the list of all input:1,x,r1,...,rl *)
Definition input(r:Run):=appT input (inp_sign r).


(*deg ai,1 +ai,2 x +ai,3 r1+...+ai,k rk = deg ai,1 +ai,2 x +ai,3 r1+...+ai,k rk+ ...+ai,t rt *)
Hypotheses deg_inp_sign:forall (r:Run)(e: Sec)(i:IdealHashQuery),
deg_ (input r)=deg_ (input (signstep r i e)).


(*deg ai,1 +ai,2 x +ai,3 r1+...+ai,k rk = deg ai,1 +ai,2 x +ai,3 r1+...+ai,k rk+ ...+ai,t rt *)
Hypotheses deg_inp_mex:forall (r:Run)(e:listT Zq),
deg_ (input r)=deg_ (input (mexstep r  e)).

(*deg ai,1 +ai,2 x +ai,3 r1+...+ai,k rk = deg ai,1 +ai,2 x +ai,3 r1+...+ai,k rk+ ...+ai,t rt *)
Hypotheses deg_inp_hash:forall (r:Run)(i:IdealHashQuery),
deg_ (input r)=deg_ (input (hashstep r i )).



(* 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_td_PdT (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'
  | signstep r' _ _=> StepList r'
 end.

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

Require Import ZArith.
Definition sum:=sum_mult_list  null_Zq  add_Zq mult_Zq.

Require Import Pol_is_ring.

Definition OZq:Zq:=null_Zq.

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


(*z'i=a..+sum ...+(a..-sum..+c'i)x :equation (4) in the paper *)
(* this is the poly: a..+sum ...+(a..-sum..+c'i)x - z'i *)
Definition EvSign(hash_out:(PdT (listT Zq) M Val))(r_i:Sec)(r:Run)(rom:Val->Zq):=
(add_pol  
(add_pol  (make_pol (FtT hash_out) (input r)) (mult_cte  (rom (TdT hash_out)) (transl (headT OE (tailT op.input)))))
(opp_pol (add_pol (transl (Sec2Expr r_i))
		       (mult_cte (rom (TdT hash_out)) (transl (headT OE (tailT op.input))))))).


Axiom dec_evSign:forall 
(hash_out:(PdT (listT Zq) M Val))(r_i:Sec)(r:Run)(rom:Val->Zq)(sec:Sec->Zq),
{eqZq (eval_poly   (EvSign hash_out r_i r  rom) (Fins2list sec))  OZq }+
{~ eqZq (eval_poly  (EvSign hash_out r_i r  rom) (Fins2list sec))  OZq }.

Require Import prob.  
Lemma dec_EvSign:forall 
(hash_out:(PdT (listT Zq) M Val))(r_i:Sec)(r:Run),
dec_pred (prodT (Sec->Zq) (Val->Zq)) (fun x :(prodT (Sec->Zq) (Val->Zq))=>
eqZq (eval_poly  (EvSign hash_out  r_i r  (sndT x)) (Fins2list (fstT x)))  OZq ).
unfold dec_pred;intros.
apply dec_evSign.
Qed.

Fixpoint Signer(R:Run)(sec:Sec->Zq)(rom:Val->Zq){struct R}:Prop:=
match R with 
            | nil  =>False
            |mexstep r' _=>(Signer r' sec rom)
            |hashstep r' _=>(Signer r' sec rom)
            |signstep r' hash_out r=>eqZq (eval_poly (EvSign hash_out r r'  rom) 
(Fins2list sec)) OZq
 \/(Signer r' sec rom)
 end.

Axiom dec_Sign_aux:forall (R:Run)(sec:Sec->Zq)(rom:Val->Zq),
{Signer R sec rom }+{~(Signer R sec rom )}.



Lemma dec_Sign:forall (R:Run),dec_pred (prodT (Sec->Zq) (Val->Zq) )
                                (fun x:prodT(Sec->Zq)  (Val->Zq) =>Signer R (fstT x) (sndT x) ).
unfold dec_pred;intros;apply dec_Sign_aux.
Qed.

Definition Sign(r:Run):=(Build_Event (prodT (Sec->Zq) (Val->Zq) )
                                (fun x:prodT (Sec->Zq) (Val->Zq) =>Signer r (fstT x) (sndT x)) (dec_Sign r)).

(*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)) OZq).
Defined.

Require Import prob.
(* the event p=0 *)

Axiom dec_Evalstozero:
 forall (e : Expr Sec) (x : Sec ->  Zq),
  ({ Evalstozero x e }) + ({ ~ Evalstozero x e }).

 Definition Ev_Evalstozero(p:Expr Sec) :=
Build_Event (Sec ->  Zq) (fun (f : Sec ->  Zq) => Evalstozero f p) (dec_Evalstozero p). 

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



(*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_V: (Val ->  Zq) -> Expr Val ->  Prop.
intros x e.
apply (eqZq (eval_poly (transl_V  e) (Fins2list_V x)) OZq).
Defined.


Axiom dec_Evalstozero_V:
 forall (e : Expr Val) (x : Val ->  Zq),
  ({ Evalstozero_V x e }) + ({ ~ Evalstozero_V x e }). 

 Definition Ev_Evalstozero_V(p:Expr Val) :=
Build_Event (Val ->  Zq) (fun (f : Val ->  Zq) => Evalstozero_V f p) (dec_Evalstozero_V p). 
 
Definition Exprnon0_V(e:Expr Val):=~(forall f:Val->Zq,Evalstozero_V f e).


(* the outputs are "good" if 
    for all group and hash outputs a b, a-b<>0 *)
 Definition GoodOutput (r : Run) :=
   ListPred Exprnon0  (gen_coll_test min_Expr (mex_Output r ))/\
   ListPred Exprnon0_V  (gen_coll_test min_Expr_V (mapT Val2Expr (list_td_PdT (IdealOutput 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 min_Expr  (mex_Output r)) /\
   Evalstozero f e .

(* we have a non-trivial collision if we find an element w in the listT of all Hi-Hj  1<=i<j<=steps r, s.t, w=0 *)
 Definition Coll_hash (r : Run) (rom : Val ->  Zq) :=
   exists e : Expr Val ,
   InT e (gen_coll_test min_Expr_V (mapT Val2Expr (list_td_PdT (IdealOutput r))))/\
   Evalstozero_V rom e .
 
Axiom dec_colh_aux:
   forall (r : Run) (rom : Val ->  Zq),
    ({ Coll_hash r rom }) + ({ ~ Coll_hash r rom }).
 
Axiom dec_col_aux:
   forall (r : Run) (f : Sec ->  Zq),
    ({ Collisions r f  }) + ({ ~ Collisions r f  }).

 
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.
 
Lemma dec_colh:
 forall (r : Run),
  dec_pred (Val ->  Zq) (fun (f : Val ->  Zq) => Coll_hash r f).
unfold dec_pred.
intros.
apply dec_colh_aux.
Qed.
 
Definition EvColl (r : Run)  :=
   Build_Event
    (Sec ->  Zq) (fun (f : Sec ->  Zq) => Collisions r f )
    (dec_col r ).
 
Definition EvCollh (r : Run) :=
   Build_Event
    (Val ->  Zq) (fun (f : Val ->  Zq) => Coll_hash r f) (dec_colh_aux r).
 
Definition Output (r : Run) (sec : Sec ->  Zq) (rom : Val ->  Zq)
                  : listT Zq :=
   appT (StepOutput r sec ) (HashRecord r rom).
 
Fixpoint nb_inter (r : Run) : nat :=
 match r with
   nil => O
  | mexstep r' _ => nb_inter r'
  | hashstep r' _ => S (nb_inter r')
  | signstep r' _ _=> nb_inter r'
 end.

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

 
Lemma lgt_hashstep:forall (r : Run) ,
  lengthT (list_td_PdT (IdealOutput  r))=nb_inter r.
simple induction r.
simpl.
auto.
intros.
simpl.
auto.
simpl; intros.
case i;simpl;intros.
auto.
simpl; intros.
auto.
Qed.

Fixpoint mex_step (r : Run) : nat :=
 match r with
   nil => O
  | mexstep r' _ => S (mex_step r')
  | hashstep r' _ => mex_step r'
  | signstep r' _ _=> mex_step r'
 end.
 
Lemma length_step:
 forall (r : Run) ,
  lengthT (mex_Output r ) = mex_step r.
simple induction r.
simpl.
auto.
intros.
simpl.
auto.
simpl; intros.
auto.
simpl; intros.
auto.
Qed.

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

(* the poly  sum ai,l cl -ai,0-H(fi,mi) : the eq (3) *)
(*this is a polynomial in Zq[c1,...,cl] *)
Definition listPolHash(rom:Val->Zq)(h:PdT (listT Zq) M Val):=
(transl_Hash (min_H
                                    (min_H  (sum_mult_list OH plus_H mult_H list_c
                                                                                  (mapT inj_Hash (tailT (tailT (FtT h)))))
                                                        (inj_Hash (headT null_Zq (FtT h))))
                         (inj_Hash (rom (TdT h))))).

Definition PolHashNul(rom:Val->Zq)(x:PdT (listT Zq) M Val):=
eq_pol (listPolHash rom x) (pol_null l Call).

Axiom dec_PolHashNul:forall(rom:Val->Zq)(x:PdT (listT Zq) M Val),
{PolHashNul  rom x}+
{~PolHashNul  rom x}.

(* H(fi,mi)=-ai,0+ sum ai,l cl *)
(* here, g is the list of  the elements compute by the algorithm:c1,...,cl: the hashoutput*)
Definition Pol_hashout_nul(g:listT Val)(rom:Val->Zq)(h:PdT (listT Zq) M Val):=
Pol1Eq  Zq (coef1 Zq Call) (Pc Zq (add_Zq 
            (min_Zq (headT null_Zq (FtT h)) (sum (tailT (tailT (FtT h))) (mapT rom g))) 
             (rom (TdT h)))) (PO Zq (coef1 Zq Call)).

Axiom dec_PolNulHash:forall (g:listT  Val)(rom:Val->Zq)(x:PdT (listT Zq) M Val),
{Pol_hashout_nul g rom x}+
{~Pol_hashout_nul g rom x}.

Definition HashOutput(r:Run):=(mapT (TdT (A:=listT Zq)(B:=M) (C:=Val)) (IdealOutput r)).

 
(* eq (3) holds at least l+1 times *)
Definition PolNul_hashout(r:Run)(rom:Val->Zq):=
nb_P_true (IdealOutput r) (dec_PolNulHash (HashOutput r) rom)>=l+1.

Definition Pol_HashNul(r:Run)(rom:Val->Zq):=
nb_P_true (IdealOutput r) (dec_PolHashNul rom)>=l+1.

(*normalement il faudrait un truc du genre solve la liste des l+1 equations *)

Axiom ROS_pb:Event (Val->Zq).
Definition Ros_pb(rom:Val->Zq):Prop:=
event_pred (Val -> Zq) ROS_pb rom.


Inductive mk_valid_sign :
 (Sec ->  Zq) ->(Val ->  Zq) -> Run ->  Prop :=
  mk_valid_sign_wc_gm:
    forall (f : Sec ->  Zq) (rom : Val ->  Zq) (r : Run),
    Collisions r f  ->mk_valid_sign f rom r  
 | mk_valid_sign_wc_rom:
     forall (f : Sec ->  Zq) (rom : Val ->  Zq) (r : Run),
     Coll_hash r rom  -> mk_valid_sign  f rom r  
| mk_valid_sign_woc_ROS:
     forall (f : Sec ->  Zq) (rom : Val ->  Zq) (r : Run),
    Pol_HashNul r rom->Ros_pb rom
    -> mk_valid_sign f rom r  
 | mk_valid_sign_woc:
     forall (f : Sec ->  Zq) (rom : Val ->  Zq) (r : Run),
    ~PolNul_hashout r rom
    ->
    Signer r f rom -> mk_valid_sign f rom r  .

Axiom dec_MkSign_aux: forall (r : Run)(f : (Sec->Zq)) (rom:  (Val ->  Zq)) ,
{mk_valid_sign  f rom r}+{~( mk_valid_sign f rom r)}.

Lemma dec_MkSign: forall (r : Run)(from: prodT (Sec->Zq) (Val ->  Zq)) ,
{mk_valid_sign (fstT from) (sndT from) r}+{~( mk_valid_sign (fstT from) (sndT from) r)}.
intros.
unfold dec_pred;simpl.
apply dec_MkSign_aux.
Qed.


Definition MkSign(r : Run):=
Build_Event
    (prodT (Sec->Zq) (Val ->  Zq)) (fun (w: prodT (Sec->Zq) (Val ->  Zq)) => 
mk_valid_sign (fstT w) (sndT w) r) (dec_MkSign r).
 
End interactive_Generic_algorithm.