swh:1:snp:a009335c9ad61a15b4ffe398f445dd601942b68c
Tip revision: 9e114126d5961fa73a21372b8a44f64723d79242 authored by François Dupressoir on 16 January 2020, 20:48:25 UTC
Generalize arguments about sampling in dexcepted
Generalize arguments about sampling in dexcepted
Tip revision: 9e11412
BitWord.eca
(* --------------------------------------------------------------------
* 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 import Bool Core Int List.
require (*--*) FinType Word Ring.
pragma +implicits.
(* -------------------------------------------------------------------- *)
op n : {int | 0 < n} as gt0_n.
clone include Word with
type Alphabet.t <- bool,
op Alphabet.enum <- [true; false],
op Alphabet.card <- 2,
op n <- n,
op dchar <- false
proof Alphabet.* by case, ge0_n by apply/ltzW/gt0_n
rename [op] "oflist" as "bits2w"
[op] "tolist" as "w2bits".
(* -------------------------------------------------------------------- *)
op zerow: word = offun (fun i => false).
op onew : word = offun (fun i => true ).
op (+^) (w1 w2 : word): word =
offun (fun i => w1.[i] ^^ w2.[i]).
op andw (w1 w2:word): word =
offun (fun i => w1.[i] /\ w2.[i]).
op oppw (w : word): word = w.
op invw (w : word): word =
offun (fun i => !w.[i]).
(* -------------------------------------------------------------------- *)
lemma zerowE i: zerow.[i] = false.
proof. by rewrite offunifE. qed.
lemma onewE i: onew.[i] = (0 <= i < n).
proof. by rewrite offunifE; case: (_ <= _ < _)%Int. qed.
lemma xorwE w1 w2 i: (w1 +^ w2).[i] = w1.[i] ^^ w2.[i].
proof.
rewrite offunifE /= andaE eq_iff; apply/andb_idl.
by case: (0 <= i < n)=> // h; rewrite !getE h.
qed.
lemma andwE (w1 w2:word) i: (andw w1 w2).[i] = (w1.[i] /\ w2.[i]).
proof.
rewrite offunifE /= andaE eq_iff; apply/andb_idl.
by case: (0 <= i < n) => // h; rewrite !getE h.
qed.
lemma invwE (w:word) i: 0 <= i < n =>
(invw w).[i] = !w.[i].
proof. by move=> lt_in; rewrite offunE. qed.
lemma oppwE (w:word) i: (oppw w).[i] = w.[i].
proof. by []. qed.
hint rewrite bwordE : zerowE onewE xorwE andwE invwE.
(* -------------------------------------------------------------------- *)
lemma onew_neq0: onew <> zerow.
proof. by apply/negP=> /wordP/(_ 0); rewrite !bwordE /= gt0_n. qed.
lemma xorw0: right_id zerow (+^).
proof. by move=> w; apply/wordP=> i _; rewrite !bwordE xor_false. qed.
lemma xorwA: associative (+^).
proof. by move=> w1 w2 w3; apply/wordP=> i _; rewrite !bwordE xorA. qed.
lemma xorwC: commutative (+^).
proof. by move=> w1 w2; apply/wordP=> i _; rewrite !bwordE xorC. qed.
lemma xorwK: forall x, x +^ x = zerow.
proof. by move=> w; apply/wordP=> i _; rewrite !bwordE xorK. qed.
lemma andw1: right_id onew andw.
proof. by move=> w; apply/wordP=> i h; rewrite !bwordE h. qed.
lemma andwA: associative andw.
proof. by move=> w1 w2 w3; apply/wordP=> i h; rewrite !bwordE andbA. qed.
lemma andwC: commutative andw.
proof. by move=> w1 w2; apply/wordP=> i h; rewrite !bwordE andbC. qed.
lemma andwDl: left_distributive andw (+^).
proof. move=> w1 w2 w3; apply/wordP=> i h; rewrite !bwordE smt. qed.
lemma andwK: idempotent andw.
proof. by move=> x; apply/wordP=> i h; rewrite !bwordE andbb. qed.
(* -------------------------------------------------------------------- *)
instance bring with word
op rzero = zerow
op rone = onew
op add = Self.(+^)
op mul = andw
op opp = oppw
proof oner_neq0 by apply/onew_neq0
proof addr0 by apply/xorw0
proof addrA by (move=> w1 w2 w3; rewrite xorwA)
proof addrC by apply/xorwC
proof addrK by apply/xorwK
proof mulr1 by apply andw1
proof mulrA by (move=> w1 w2 w3; rewrite andwA)
proof mulrC by apply/andwC
proof mulrDl by apply/andwDl
proof mulrK by apply/andwK
proof oppr_id by trivial.
pred unitw (w:word) = w = onew.
op iandw (w:word) = if w = onew then onew else w.
clone import Ring.ComRing as WRing with
type t = word,
op zeror <- zerow,
op ( + ) <- (+^),
op [ - ] <- oppw,
op oner <- onew,
op ( * ) <- andw,
op invr <- iandw,
pred unit <- unitw
proof *.
realize addrA. proof. apply xorwA. qed.
realize addrC. proof. apply xorwC. qed.
realize add0r. proof. move=> ?;ring. qed.
realize addNr. proof. move=> ?;ring. qed.
realize oner_neq0. proof. apply onew_neq0. qed.
realize mulrA. proof. apply andwA. qed.
realize mulrC. proof. apply andwC. qed.
realize mul1r. proof. move=> ?;ring. qed.
realize mulrDl. proof. apply andwDl. qed.
realize mulVr. proof. move=> ?;rewrite /unitw /iandw => -> /=;ring. qed.
realize unitout. proof. by move=> x;rewrite /unitw /iandw => ->. qed.
realize unitP.
proof.
move=> x y; rewrite /unitw !wordP => + i Hi -/(_ i Hi).
by rewrite andwE onewE Hi /#.
qed.