https://github.com/EasyCrypt/easycrypt
Tip revision: 863066bded664a5e2aba7f89c4fb7bc2afd0e28d authored by Pierre-Yves Strub on 23 September 2015, 08:28:02 UTC
Ring axioms of the `ring`/`field` tactics agree with the ones of `Ring.ec`
Ring axioms of the `ring`/`field` tactics agree with the ones of `Ring.ec`
Tip revision: 863066b
Word.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2015 - IMDEA Software Institute
* Copyright (c) - 2012--2015 - Inria
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
require Bool.
require import Int.
op length: int.
axiom length_pos: 0 <= length.
(* A word only has the get operator: its size is fixed. *)
(* Ideally, we would have cloned bitstrings, but they are equipped with an empty operator. *)
type word.
op "_.[_]": word -> int -> bool.
pred (==)(w0, w1:word) = forall i,
0 <= i => i < length =>
w0.[i] = w1.[i].
axiom word_ext w0 w1:
w0 == w1 => w0 = w1.
(* set *)
op "_.[_<-_]": word -> int -> bool -> word.
axiom get_set w i j b:
0 <= i => i < length =>
w.[i <- b].[j] = (i = j) ? b : w.[j].
(* zeros *)
op zeros: word.
axiom get_zeros i:
0 <= i < length =>
zeros.[i] = false.
(* xor *)
op (^^): word -> word -> word.
axiom get_xor w0 w1 i:
0 <= i < length =>
(w0 ^^ w1).[i] = Bool.(^^) w0.[i] w1.[i].
lemma xorK w:
w ^^ w = zeros.
proof strict.
by apply word_ext; smt.
qed.
lemma xorC w0 w1:
w0 ^^ w1 = w1 ^^ w0.
proof strict.
by apply word_ext; smt.
qed.
lemma xorA x y z:
x ^^ (y ^^ z) = (x ^^ y) ^^ z.
proof strict.
apply word_ext=> i le0i ltilen.
by rewrite !get_xor // Bool.xorA.
qed.
lemma xor0 w: w ^^ zeros = w.
proof strict.
by apply word_ext; smt.
qed.
lemma xor_opt x y: x ^^ y ^^ y = x.
proof strict.
by rewrite -xorA xorK xor0.
qed.
(* TODO: Finish writing the conversions *)
(** Array conversions *)
require Array.
op to_bits: word -> bool Array.array.
axiom length_to_array w:
Array.length (to_bits w) = length.
axiom get_to_array w i:
0 <= i < length =>
Array."_.[_]" (to_bits w) i = w.[i].
op from_bits: bool Array.array -> word.
axiom get_from_bits a i:
Array.length a = length =>
0 <= i < length =>
(from_bits a).[i] = Array."_.[_]" a i.
lemma to_from_array a:
Array.length a = length =>
to_bits (from_bits a) = a.
proof strict.
by intros Hlen; apply Array.array_ext; smt.
qed.
lemma from_to_bits w:
from_bits (to_bits w) = w.
proof strict.
by apply word_ext; smt.
qed.
(** Integer conversion *)
op to_int: word -> int.
op from_int: int -> word.
axiom to_from_int i:
0 <= i < 2^length =>
to_int (from_int i) = i.
axiom from_to_int w:
from_int (to_int w) = w.
require import Real.
require import Distr.
require import FSet.
(* Uniform distribution on fixed-length words *)
theory Dword.
op dword : word distr.
axiom mu_x_def (w:word): mu_x dword w = 1%r / (2 ^ length)%r.
axiom dwordL: weight dword = 1%r.
lemma supp_def (w:word): in_supp w dword.
proof strict.
rewrite /in_supp mu_x_def; smt.
qed.
lemma mu_cpMemw (s : word set):
mu dword (cpMem s) = (card s)%r *( 1%r / (2^length)%r).
proof strict.
rewrite (mu_cpMem _ _ (1%r / (2^length)%r))=> //.
intros x; rewrite mu_x_def; smt.
qed.
import FSet.Dexcepted.
lemma restrwL (X : word set):
FSet.card X < 2^length =>
weight (dword \ X) = 1%r.
proof strict.
intros=> Hcard; rewrite lossless_restr ?dwordL ?mu_cpMemw //.
apply (real_lt_trans _ ((2^length)%r * (1%r / (2 ^ length)%r)) _);
last smt.
apply mulrM; last by rewrite from_intM.
smt.
qed.
end Dword.