https://github.com/EasyCrypt/easycrypt
Tip revision: 88a87da162d7847426b5ab24d2f8ecfea89a332e authored by Cécile BARITEL-RUET on 17 December 2018, 14:33:18 UTC
Merge branch '1.0' of https://github.com/EasyCrypt/easycrypt into 1.0
Merge branch '1.0' of https://github.com/EasyCrypt/easycrypt into 1.0
Tip revision: 88a87da
PrimeField.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 Int IntDiv.
(* prime fields GF(q) for q prime *)
theory F.
(* the order of field is a prime q *)
op q: int.
axiom q_pos: Int.(<) 0 q.
(* TODO: Add an axiom asserting primality of q. *)
(* Type of elements of the field *)
type t.
op zero : t. (* zero *)
op one : t. (* one *)
op ( * ): t -> t -> t. (* multiplication modulo q *)
op ( + ): t -> t -> t. (* addition modulo q *)
op [ - ]: t -> t. (* the additive inverse *)
op inv: t -> t. (* the multiplicative inverse *)
op (-) : t -> t -> t. (* subtraction modulo q *)
op (/) : t -> t -> t. (* division modulo q for y <> 0 *)
op (^) : t -> int -> t. (* exponentiation *)
axiom non_trivial: zero <> one.
(* Addition/Subtraction *)
axiom addC (x y:t): x + y = y + x.
axiom addA (x y z:t) : x + (y + z) = (x + y) + z.
axiom addf0 (x:t): x + zero = x.
axiom addfN (x:t): x + -x = zero.
axiom sub_def (x y:t) : x - y = x + -y.
(* Multiplication *)
axiom mulC (x y:t): x * y = y * x.
axiom mulA (x y z:t): x * (y * z) = (x * y) * z.
axiom mulf1 (x:t): x * one = x.
axiom mulfV (x:t): x <> zero => (x * (inv x)) = one.
axiom mulfDl (x y z:t): x * y + x * z = x * (y + z).
axiom div_def (x y:t): x / y = x * (inv y).
axiom mulf_eq0:
forall (x y : t), x * y = zero <=> x = zero \/ y = zero.
(* Exponentiation *)
axiom pow0 (x:t): x ^ 0 = one.
axiom powS (x:t) (n:int): Int.(<=) 0 n => x ^ (Int.(+) n 1) = x * x ^ n.
axiom powN (x:t) (n:int): Int.(<=) 0 n => x ^ (Int.([-]) n) = inv (x ^ n).
(** conversion between int and gf_q *)
op ofint : int -> t.
op toint : t -> int.
axiom ofint0: ofint 0 = zero.
axiom ofintS (n:int): Int.(<=) 0 n => ofint (Int.(+) n 1) = (ofint n) + one.
axiom ofintN (n:int): ofint (Int.([-]) n) = -(ofint n).
import Int.
axiom toint_bounded (x:t): 0 <= toint x < q.
axiom oftoint (x:t): ofint (toint x) = x.
axiom toofint_mod (x:int): toint (ofint x) = IntDiv.(%%) x q.
end F.
export F.
(* Declaring the ring and field structure *)
require AlgTactic.
require Ring.
instance ring with t
op rzero = F.zero
op rone = F.one
op add = F.( + )
op opp = F.([-])
op mul = F.( * )
op expr = F.( ^ )
op sub = F.(-)
op ofint = ofint
proof oner_neq0 by smt
proof addr0 by smt
proof addrA by smt
proof addrC by smt
proof addrN by smt
proof mulr1 by smt
proof mulrA by smt
proof mulrC by smt
proof mulrDl by smt
proof expr0 by smt
proof exprS by smt
proof subrE by smt
proof ofint0 by smt
proof ofint1 by smt
proof ofintS by smt
proof ofintN by smt.
instance field with t
op rzero = F.zero
op rone = F.one
op add = F.( + )
op opp = F.([-])
op mul = F.( * )
op expr = F.( ^ )
op sub = F.(-)
op ofint = ofint
op inv = inv
op div = F.(/)
proof oner_neq0 by smt
proof addr0 by smt
proof addrA by smt
proof addrC by smt
proof addrN by smt
proof mulr1 by smt
proof mulrA by smt
proof mulrC by smt
proof mulrDl by smt
proof mulrV by smt
proof expr0 by smt
proof exprS by smt
proof exprN by smt
proof subrE by smt
proof divrE by smt
proof ofint0 by smt
proof ofint1 by smt
proof ofintS by smt
proof ofintN by smt.
(** Lemmas *)
lemma nosmt subff (x:t): (x - x) = zero
by ringeq.
lemma nosmt add0f (x:t): zero + x = x
by ringeq.
lemma nosmt mulf0 (x:t): x * zero = zero
by ringeq.
lemma nosmt mulNf (x y:t): (-x) * y = - (x * y)
by ringeq.
lemma nosmt mulfN (x y:t): y * (-x)= - (y * x)
by ringeq.
lemma nosmt oppK (x:t): -(-x) = x
by ringeq.
lemma nosmt mulfNl (x y z:t): x * y - x * z = x * (y - z)
by ringeq.
lemma nosmt mulN1f (x:t): (-one) * x = -x
by ringeq.
lemma nosmt oppfD (x y:t): (-x) + (-y) = -(x + y)
by ringeq.
import Int.
lemma nosmt toint_pos (x:t): 0 <= toint x
by [].
lemma nosmt toint_lt (x:t): toint x < q
by [].
lemma nosmt toint_le (x:t): toint x <= q - 1
by [].
lemma nosmt toofint (x:int): 0 <= x => x < q => toint (ofint x) = x.
proof.
move=> Hp Hlt;rewrite toofint_mod IntDiv.modz_small /#.
qed.
lemma nosmt ofint1_: ofint 1 = F.one
by [].
theory FDistr.
require import Distr.
require import Real.
(* distrinution *)
op dt: t distr.
axiom dt_fu: is_full dt.
axiom dt1E: forall (s:t), mu1 dt s = (1%r/q%r)%Real.
axiom dt_ll: is_lossless dt.
lemma dt_funi: is_funiform dt.
proof. by move=> ??;rewrite !dt1E. qed.
end FDistr.