(* --------------------------------------------------------------------
 * Copyright (c) - 2012--2016 - IMDEA Software Institute
 * Copyright (c) - 2012--2016 - Inria
 *
 * Distributed under the terms of the CeCILL-B-V1 license
 * -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
require import Fun Bool Int List.
require (*--*) FinType Word.

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: (_ <= _ < _). qed.

lemma xorwE w1 w2 i: (w1 +^ w2).[i] = w1.[i] ^^ w2.[i].
proof.
rewrite offunifE /= anda_and; 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 /= anda_and; 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 andA. qed.

lemma andwC: commutative andw.
proof. by move=> w1 w2; apply/wordP=> i h; rewrite !bwordE andC. 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 andK. 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.