Module Type Op_Expr.

Parameter Sec:Set.
  (*n=card Sec *)
Parameter n:nat.


Parameter Val:Set.
(* cardinal(Val)=card *)
Parameter card:nat.

(*Hash is the type for c1,...,cl*)
Parameter Hash:Set.
(* l is the number of interaction with the signer *)
Parameter l:nat.

(*il faudrait mettre l ds IGA_PA avec 
definition l:=lengthT (SignOutput) 
ms on a besoin de l pr transl_Hash*)

Parameter Expr:Set->Type.

Parameter min_Expr:(Expr Sec)->(Expr Sec)->(Expr Sec).
Parameter add_Expr:(Expr Sec)->(Expr Sec)->(Expr Sec).
Parameter mult_Expr:(Expr Sec)->(Expr Sec)->(Expr Sec).
Parameter OE:Expr Sec.
Parameter OH:Expr Hash.
Parameter min_Expr_V:(Expr Val)->(Expr Val)->(Expr Val).
Parameter min_H:(Expr Hash)->(Expr Hash)->(Expr Hash).
Parameter mult_H:(Expr Hash)->(Expr Hash)->(Expr Hash).
Parameter plus_H:(Expr Hash)->(Expr Hash)->(Expr Hash).

Require Import listT.
(*this is the list c1,...,cl*)
Parameter list_c:listT (Expr Hash).

Require Import Reals.
Require Import Ring_cat.

Parameter Zq_ring:RING.
Definition Zq:Type:=Carrier Zq_ring.
Definition null_Zq:Zq:=Monoid_cat.monoid_unit Zq_ring.
Definition unit_Zq:Zq:=ring_unit Zq_ring.
Definition mult_Zq:Zq->Zq->Zq:=ring_mult (R:=Zq_ring).
Definition add_Zq:Zq->Zq->Zq:=sgroup_law Zq_ring.
Definition opp_Zq:Zq->Zq:=group_inverse Zq_ring.
Definition min_Zq(a b:Zq):Zq:=add_Zq a (opp_Zq b).
Definition eqZq:Zq->Zq->Prop:=Equal (s:=Zq_ring).
Parameter dec_Zq:forall a b : Zq , {eqZq a b} + {~ eqZq a b}.


  (* card Zq=q *)
Parameter q : nat.
Parameter lt_0_q : (0 < INR q)%R.

Parameter inj_Sec:Zq->Expr Sec.
Parameter inj_Val:Zq->Expr Val.
Parameter Val2Expr:Val->Expr Val. (*apply secret *)	
Parameter Sec2Expr:Sec->Expr Sec. (*apply secret *)	  
Parameter inj_Hash:Zq->Expr Hash.
Parameter Eval:forall X:Set,(X->Zq)->(Expr X)->Zq.

Require Import listT.

(*input is the list 1,x *)
Parameter input:listT (Expr Sec).

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




(* normally Sec:=Finset n 
  for eval_poly we take an elt x:=(x1,. ,xn) of type list Zq instead of Sec->Zq
  so to simplify we use a function Fins2list that return an elt of type Sec->Zq like a list of Zq*)
Parameter Fins2list :(Sec ->  Zq) ->  listT Zq.

Parameter Fins2list_V :(Val ->  Zq) ->  listT Zq.

Require Import POLY_ax.
Require Import Pol_is_ring.
Parameter Call:CALL Zq.

Parameter transl : Expr Sec -> Poly n Call.
(*
Fixpoint transl [ e : (Expr Sec) ] : poly :=
 Cases e of
   (secret e') => (consT (!pairT (Zq_cring q) Mon (POS xH) (mon1e e')) (nilT ?))
  | (const e1) => (consT (!pairT (Zq_cring q) Mon e1 mon0) (nilT ?))
  | (mult e1 e2) => (mult_pol_pol (transl e1) (transl e2))
  | (add e1 e2) => (add_pol (transl e1) (transl e2))
 end.
*)

Parameter transl_V:Expr Val->Poly card Call.


Parameter transl_Hash:Expr Hash->Poly l Call.

Definition deg_Expr(e:Expr Sec):nat:=degre Zq Call n (transl e).
Definition list_deg(l:listT (Expr Sec)):listT nat:=mapT (deg_Expr) l.

Require Import max.
Definition deg_ (l : listT (Expr Sec)) : nat := max_elt 0 (list_deg l). 

	
End Op_Expr.