https://github.com/EasyCrypt/easycrypt
Tip revision: 6561b69dcc30a72b8a78c97019cfc46e4df655f0 authored by Pierre-Yves Strub on 19 November 2021, 22:43:31 UTC
prune virtual tc
prune virtual tc
Tip revision: 6561b69
Prime_field.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2021 - Inria
* Copyright (c) - 2012--2021 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
(* prime fields GF(q) for q prime *)
require Int.
(* 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 gf_q.
op ( * ): gf_q -> gf_q -> gf_q. (* multiplication modulo q *)
op ( + ): gf_q -> gf_q -> gf_q. (* addition modulo q *)
op [ - ]: gf_q -> gf_q. (* the additive inverse *)
op inv: gf_q -> gf_q. (* the multiplicative inverse *)
op (-) (x y:gf_q): gf_q = x + -y. (* subtraction modulo q *)
op (/) (x y:gf_q): gf_q = x * (inv y). (* division modulo q for y <> 0 *)
const gf_q0: gf_q. (* zero *)
const gf_q1: gf_q. (* one *)
(** Field axioms, compare "Harrison: Theorem proving with the Real Numbers, p. 10" *)
axiom one_zero: gf_q0 <> gf_q1.
(* Addition/Subtraction *)
axiom gf_q_add_comm: forall (x y:gf_q),
x + y = y + x.
axiom gf_q_add_assoc: forall (x y z:gf_q),
x + (y + z) = (x + y) + z.
axiom gf_q_add_unit: forall (x:gf_q),
gf_q0 + x = x.
axiom gf_q_add_minus: forall (x:gf_q),
x + -x = gf_q0.
(* Multiplication *)
axiom gf_q_mult_comm: forall (x y:gf_q),
x * y = y * x.
axiom gf_q_mult_assoc: forall (x y z:gf_q),
x * (y * z) = (x * y) * z.
axiom gf_q_mult_unit: forall (x:gf_q),
x * gf_q1 = x.
axiom gf_q_mult_inv: forall (x:gf_q),
x <> gf_q0 => (x * (inv x)) = gf_q1.
axiom gf_q_distr: forall (x y z:gf_q),
x * (y + z) = x * y + x * z.
(** Lemmas *)
lemma gf_q_minus (x:gf_q):
(x - x) = gf_q0.
proof strict.
by (rewrite /(-) gf_q_add_minus).
qed.
lemma gf_q_add_unit_right (x:gf_q):
x + gf_q0 = x.
proof strict.
by rewrite gf_q_add_comm gf_q_add_unit.
qed.
lemma gf_q_mult_zero (x:gf_q):
x * gf_q0 = gf_q0.
proof strict.
have H: x * gf_q0 + x * gf_q0 = x * gf_q0.
by rewrite -gf_q_distr gf_q_add_unit.
have ->: x * gf_q0 = x * gf_q0 + (x * gf_q0 - x * gf_q0).
by rewrite gf_q_minus gf_q_add_unit_right.
by rewrite /(-) gf_q_add_assoc H gf_q_add_minus.
qed.
lemma gf_q_mult_minus (x y:gf_q):
(-x) * y = - (x * y).
proof strict.
have ->: (-x) * y = (-x) * y + x * y + (-( x * y)).
by rewrite -(gf_q_add_assoc _ (x * y)) gf_q_add_minus gf_q_add_unit_right.
rewrite (gf_q_mult_comm (-x)) (gf_q_mult_comm x) -gf_q_distr.
by rewrite (gf_q_add_comm (-x)) gf_q_add_minus gf_q_mult_zero gf_q_add_unit.
qed.
lemma gf_q_mult_minus_right (x y:gf_q):
y * (-x)= - (y * x).
proof strict.
by rewrite (gf_q_mult_comm y) (gf_q_mult_comm y) gf_q_mult_minus.
qed.
lemma nosmt gf_q_minus_minus (x:gf_q):
-(-x) = x
by [].
lemma gf_q_minus_distr (x y z:gf_q):
x * (y - z) = x * y - x * z.
proof strict.
by rewrite /(-) gf_q_distr gf_q_mult_minus_right.
qed.
lemma gf_q_opp_mult (x:gf_q):
-x = (-gf_q1) * x.
proof strict.
by rewrite gf_q_mult_minus gf_q_mult_comm gf_q_mult_unit.
qed.
lemma gf_q_opp_distr (x y:gf_q):
-(x + y) = (-x) + (-y).
proof strict.
by rewrite gf_q_opp_mult gf_q_distr -2!gf_q_opp_mult.
qed.
theory Dgf_q.
require import OldDistr.
require import Real.
op dgf_q: gf_q distr.
axiom supp_def: forall (s:gf_q),
in_supp s dgf_q.
axiom mu1_def_in: forall (s:gf_q),
mu1 dgf_q s = 1%r/q%r.
axiom lossless: weight dgf_q = 1%r.
end Dgf_q.
(** conversion between int and gf_q *)
import Int.
op i_to_gf_q : int -> gf_q.
op gf_q_to_i : gf_q -> int.
axiom gf_q_to_i_pos: forall (x:gf_q),
0 <= gf_q_to_i x.
axiom gf_q_to_i_smaller: forall (x:gf_q),
gf_q_to_i x <= q - 1.
axiom gf_q_to_i_inverse: forall (x:int),
0 <= x => x < q =>
gf_q_to_i (i_to_gf_q x) = x.
axiom i_to_gf_inverse: forall (x:gf_q),
i_to_gf_q (gf_q_to_i x) = x.