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