aboutsummaryrefslogtreecommitdiffstats
path: root/src/bva/BVList.v
diff options
context:
space:
mode:
authorckeller <ckeller@users.noreply.github.com>2019-01-28 23:19:12 +0100
committerGitHub <noreply@github.com>2019-01-28 23:19:12 +0100
commit7021c53d4ecf97c82ccebb6bb45f5305d8b482ea (patch)
treeba7537e1e813cabf9ee0d910f845c71fa5f446e7 /src/bva/BVList.v
parent36548d6634864a131cc83ce21491c797163de305 (diff)
downloadsmtcoq-7021c53d4ecf97c82ccebb6bb45f5305d8b482ea.tar.gz
smtcoq-7021c53d4ecf97c82ccebb6bb45f5305d8b482ea.zip
Merge from LFSC (#26)
* Showing models as coq counter examples in tactic without constructing coq terms * also read models when calling cvc4 with a file (deactivated because cvc4 crashes) * Show counter examples with variables in the order they are quantified in the Coq goal * Circumvent issue with ocamldep * fix issue with dependencies * fix issue with dependencies * Translation and OCaml support for extract, zero_extend, sign_extend * Show run times of components * print time on stdout instead * Tests now work with new version (master) of CVC4 * fix small printing issue * look for date on mac os x * proof of valid_check_bbShl: some cases to prove. * full proof of "left shift checker". * full proof of "rigth shift checker". * Support translation of terms bvlshr, bvshl but LFSC rules do not exists at the moment Bug fix for bitvector extract (inverted arguments) * Typo * More modularity on the format of traces depending on the version of coq * More straightforward definitions in Int63Native_standard * Use the Int31 library with coq-8.5 * Use the most efficient operations of Int31 * Improved performance with coq-8.5 * Uniform treatment of sat and smt tactics * Hopefully solved the problem with universes for the tactic * Updated the installation instructions * Holes for unsupported bit blasting rules * Cherry-picking from smtcoq/smtcoq * bug fix hole for bitblast * Predefined arrays are not required anymore * fix issue with coq bbT and bitof construction from ocaml * bug fix in smtAtom for uninterpreted functions fix verit test file * fix issue with smtlib2 extract parsing * It looks like we still need the PArray function instances for some examples (see vmcai_bytes.smt2) * Solver specific reification: Each solver has a list of supported theories which is passed to Atom.of_coq, this function creates uninterpreted functions / sorts for unsupported features. * show counter-examples with const_farray instead of const for constant array definitions * Vernacular commands to debug checkers. Verit/Lfsc_Checker_Debug will always fail, reporting the first proof step of the certificate that failed be checked * Update INSTALL.md * show smtcoq proof when converting * (Hopefully) repared the universes problems * Corrected a bug with holes in proofs * scripts for tests: create a folder "work" under "lfsc/tests/", locate the benchmarks there. create a folder "results" under "lfsc/tests/work/" in which you'll find the results of ./cvc4tocoq. * make sure to give correct path for your benchs... * Checker for array extensionality modulo symmetry of equality * fix oversight with bitvectors larger than 63 bits * some printing functions for smt2 ast * handle smtlib2 files with more complicated equivalence with (= ... ) * revert: ./cvc4tocoq does not output lfsc proofs... * bug fix one input was ignored * Don't show verit translation of LFSC proof if environment variable DONTSHOWVERIT is set (e.g. put export DONTSHOWVERIT="" in your .bashrc or .bashprofile) * Also sort names of introduced variables when showing counter-example * input files for which SMTCoq retuns false. * input files for which SMTCoq retuns false. * use debug checker for debug file * More efficient debug checker * better approximate number of failing step of certificate in debug checker * fix mistake in ml4 * very first attempt to support goals in Prop * bvs: comparison predicates in Prop and their <-> proofs with the ones in bool farrays: equality predicate in Prop and its <-> proof with the one in bool. * unit, Bool, Z, Pos: comparison and equality predicates in Prop. * a typo fixed. * an example of array equality in Prop (converted into Bool by hand)... TODO: enhance the search space of cvc4 tactic. * first version of cvc4' tactic: "solves" the goals in Prop. WARNING: supports only bv and array goals and might not be complete TODO: add support for lia goals * cvc4' support for lia WARNING: might not be complete! * small fix in cvc4' and some variations of examples * small fix + support for goals in Bool and Bool = true + use of solve tactical WARNING: does not support UF and INT63 goals in Prop * cvc4': better arrangement * cvc4': Prop2Bool by context search... * cvc4': solve tactial added -> do not modify unsolved goals. * developer documentation for the smtcoq repo * cvc4': rudimentary support for uninterpreted function goals in Prop. * cvc4': support for goals with Leibniz equality... WARNING: necessary use of "Grab Existential Variables." to instantiate variable types for farrays! * cvc4': Z.lt adapted + better support from verit... * cvc4': support for Z.le, Z.ge, Z.gt. * Try arrays with default value (with a constructor for constant arrays), but extensionality is not provable * cvc4': support for equality over uninterpreted types * lfsc demo: goals in Coq's Prop. * lfsc demo: goals in Bool. * Fix issue with existential variables generated by prop2bool. - prop2bool tactic exported by SMTCoq - remove useless stuff * update usage and installation instructions * Update INSTALL.md * highlighting * the tactic: bool2prop. * clean up * the tactic smt: very first version. * smt: return unsolved goals in Prop. * Show when a certificate cannot be checked when running the tactic instead of at Qed * Tactic improvements - Handle negation/True/False in prop/bool conversions tactic. - Remove alias for farray (this caused problem for matching on this type in tactics). - Tactic `smt` that combines cvc4 and veriT. - return subgoals in prop * test change header * smt: support for negated goals + some reorganization. * conflicts resolved + some reorganization. * a way to solve the issue with ambiguous coercions. * reorganization. * small change. * another small change. * developer documentation of the tactics. * developer guide: some improvements. * developer guide: some more improvements. * developer guide: some more improvements. * developer guide: some more improvements. * pass correct environment for conversion + better error messages * cleaning * ReflectFacts added. * re-organizing developers' guide. * re-organizing developers' guide. * re-organizing developers' guide. * removing unused maps. * headers. * artifact readme getting started... * first attempt * second... * third... * 4th... * 5th... * 6th... * 7th... * 8th... * 9th... * 10th... * 11th... * 12th... * 13th... * 14th... * 15th... * 16th... * 17th... * Update artifact.md Use links to lfsc repository like in the paper * 18th... * 19th... * 20th... * 21st... * 22nd... * 23rd... * 24th... * 25th... * 26th... * 27th... * 28th... * Update artifact.md Small reorganization * minor edits * More minor edits * revised description of tactics * Final pass * typo * name changed: artifact-readme.md * file added... * passwd chaged... * links... * removal * performance statement... * typos... * the link to the artifact image updated... * suggestions by Guy... * aux files removed... * clean-up... * clean-up... * some small changes... * small fix... * additional information on newly created files after running cvc4tocoq script... * some small fix... * another small fix... * typo... * small fix... * another small fix... * fix... * link to the artifact image... * We do not want to force vm_cast for the Theorem commands * no_check variants of the tactics * TODO: a veriT test does not work anymore * Compiles with both versions of Coq * Test of the tactics in real conditions * Comment on this case study * an example for the FroCoS paper. * Fix smt tactic that doesn't return cvc4's subgoals * readme modifications * readme modifications 2 * small typo in readme. * small changes in readme. * small changes in readme. * typo in readme. * Sync with https://github.com/LFSC/smtcoq * Port to Coq 8.6 * README * README * INSTALL * Missing file * Yves' proposition for installation instructions * Updated link to CVC4 * Compiles again with native-coq * Compiles with both versions of Coq * Command to bypass typechecking when generating a zchaff theorem * Solved bug on cuts from Hole * Counter-models for uninterpreted sorts (improves issue #13) * OCaml version note (#15) * update .gitignore * needs OCaml 4.04.0 * Solving merge issues (under progress) * Make SmtBtype compile * Compilation of SmtForm under progress * Make SmtForm compile * Make SmtCertif compile * Make SmtTrace compile * Make SatAtom compile * Make smtAtom compile * Make CnfParser compile * Make Zchaff compile * Make VeritSyntax compile * Make VeritParser compile * Make lfsc/tosmtcoq compile * Make smtlib2_genconstr compile * smtCommand under progress * smtCommands and verit compile again * lfsc compiles * ml4 compiles * Everything compiles * All ZChaff unit tests and most verit unit tests (but taut5 and un_menteur) go through * Most LFSC tests ok; some fail due to the problem of verit; a few fail due to an error "Not_found" to investigate * Authors and headings * Compiles with native-coq * Typo
Diffstat (limited to 'src/bva/BVList.v')
-rw-r--r--src/bva/BVList.v2704
1 files changed, 2704 insertions, 0 deletions
diff --git a/src/bva/BVList.v b/src/bva/BVList.v
new file mode 100644
index 0000000..48befd6
--- /dev/null
+++ b/src/bva/BVList.v
@@ -0,0 +1,2704 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
+Require Import List Bool NArith Psatz Int63 Nnat.
+Require Import Misc.
+Import ListNotations.
+Local Open Scope list_scope.
+Local Open Scope N_scope.
+Local Open Scope bool_scope.
+
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(* We temporarily assume proof irrelevance to handle dependently typed
+ bit vectors *)
+Axiom proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2.
+
+Lemma inj a a' : N.to_nat a = N.to_nat a' -> a = a'.
+Proof. intros. lia. Qed.
+
+ Fixpoint leb (n m: nat) : bool :=
+ match n with
+ | O =>
+ match m with
+ | O => true
+ | S m' => true
+ end
+ | S n' =>
+ match m with
+ | O => false
+ | S m' => leb n' m'
+ end
+ end.
+
+Module Type BITVECTOR.
+
+ Parameter bitvector : N -> Type.
+ Parameter bits : forall n, bitvector n -> list bool.
+ Parameter of_bits : forall (l:list bool), bitvector (N.of_nat (List.length l)).
+ Parameter bitOf : forall n, nat -> bitvector n -> bool.
+
+ (* Constants *)
+ Parameter zeros : forall n, bitvector n.
+
+ (*equality*)
+ Parameter bv_eq : forall n, bitvector n -> bitvector n -> bool.
+
+ (*binary operations*)
+ Parameter bv_concat : forall n m, bitvector n -> bitvector m -> bitvector (n + m).
+ Parameter bv_and : forall n, bitvector n -> bitvector n -> bitvector n.
+ Parameter bv_or : forall n, bitvector n -> bitvector n -> bitvector n.
+ Parameter bv_xor : forall n, bitvector n -> bitvector n -> bitvector n.
+ Parameter bv_add : forall n, bitvector n -> bitvector n -> bitvector n.
+ Parameter bv_subt : forall n, bitvector n -> bitvector n -> bitvector n.
+ Parameter bv_mult : forall n, bitvector n -> bitvector n -> bitvector n.
+ Parameter bv_ult : forall n, bitvector n -> bitvector n -> bool.
+ Parameter bv_slt : forall n, bitvector n -> bitvector n -> bool.
+
+ Parameter bv_ultP : forall n, bitvector n -> bitvector n -> Prop.
+ Parameter bv_sltP : forall n, bitvector n -> bitvector n -> Prop.
+
+ Parameter bv_shl : forall n, bitvector n -> bitvector n -> bitvector n.
+ Parameter bv_shr : forall n, bitvector n -> bitvector n -> bitvector n.
+
+ (*unary operations*)
+ Parameter bv_not : forall n, bitvector n -> bitvector n.
+ Parameter bv_neg : forall n, bitvector n -> bitvector n.
+ Parameter bv_extr : forall (i n0 n1 : N), bitvector n1 -> bitvector n0.
+
+ (* Parameter bv_extr : forall (n i j : N) {H0: n >= j} {H1: j >= i}, bitvector n -> bitvector (j - i). *)
+
+ Parameter bv_zextn : forall (n i: N), bitvector n -> bitvector (i + n).
+ Parameter bv_sextn : forall (n i: N), bitvector n -> bitvector (i + n).
+ (* Parameter bv_extr : forall n i j : N, bitvector n -> n >= j -> j >= i -> bitvector (j - i). *)
+
+ (* Specification *)
+ Axiom bits_size : forall n (bv:bitvector n), List.length (bits bv) = N.to_nat n.
+ Axiom bv_eq_reflect : forall n (a b:bitvector n), bv_eq a b = true <-> a = b.
+ Axiom bv_eq_refl : forall n (a:bitvector n), bv_eq a a = true.
+
+ Axiom bv_ult_B2P : forall n (a b:bitvector n), bv_ult a b = true <-> bv_ultP a b.
+ Axiom bv_slt_B2P : forall n (a b:bitvector n), bv_slt a b = true <-> bv_sltP a b.
+ Axiom bv_ult_not_eq : forall n (a b:bitvector n), bv_ult a b = true -> a <> b.
+ Axiom bv_slt_not_eq : forall n (a b:bitvector n), bv_slt a b = true -> a <> b.
+ Axiom bv_ult_not_eqP: forall n (a b:bitvector n), bv_ultP a b -> a <> b.
+ Axiom bv_slt_not_eqP: forall n (a b:bitvector n), bv_sltP a b -> a <> b.
+
+ Axiom bv_and_comm : forall n (a b:bitvector n), bv_eq (bv_and a b) (bv_and b a) = true.
+ Axiom bv_or_comm : forall n (a b:bitvector n), bv_eq (bv_or a b) (bv_or b a) = true.
+ Axiom bv_add_comm : forall n (a b:bitvector n), bv_eq (bv_add a b) (bv_add b a) = true.
+
+ Axiom bv_and_assoc : forall n (a b c: bitvector n), bv_eq (bv_and a (bv_and b c)) (bv_and (bv_and a b) c) = true.
+ Axiom bv_or_assoc : forall n (a b c: bitvector n), bv_eq (bv_or a (bv_or b c)) (bv_or (bv_or a b) c) = true.
+ Axiom bv_xor_assoc : forall n (a b c: bitvector n), bv_eq (bv_xor a (bv_xor b c)) (bv_xor (bv_xor a b) c) = true.
+ Axiom bv_add_assoc : forall n (a b c: bitvector n), bv_eq (bv_add a (bv_add b c)) (bv_add (bv_add a b) c) = true.
+ Axiom bv_not_involutive: forall n (a: bitvector n), bv_eq (bv_not (bv_not a)) a = true.
+
+ Parameter _of_bits : forall (l: list bool) (s : N), bitvector s.
+
+End BITVECTOR.
+
+Module Type RAWBITVECTOR.
+
+Parameter bitvector : Type.
+Parameter size : bitvector -> N.
+Parameter bits : bitvector -> list bool.
+Parameter of_bits : list bool -> bitvector.
+Parameter _of_bits : list bool -> N -> bitvector.
+Parameter bitOf : nat -> bitvector -> bool.
+
+(* Constants *)
+Parameter zeros : N -> bitvector.
+
+(*equality*)
+Parameter bv_eq : bitvector -> bitvector -> bool.
+
+(*binary operations*)
+Parameter bv_concat : bitvector -> bitvector -> bitvector.
+Parameter bv_and : bitvector -> bitvector -> bitvector.
+Parameter bv_or : bitvector -> bitvector -> bitvector.
+Parameter bv_xor : bitvector -> bitvector -> bitvector.
+Parameter bv_add : bitvector -> bitvector -> bitvector.
+Parameter bv_mult : bitvector -> bitvector -> bitvector.
+Parameter bv_subt : bitvector -> bitvector -> bitvector.
+Parameter bv_ult : bitvector -> bitvector -> bool.
+Parameter bv_slt : bitvector -> bitvector -> bool.
+
+Parameter bv_ultP : bitvector -> bitvector -> Prop.
+Parameter bv_sltP : bitvector -> bitvector -> Prop.
+
+Parameter bv_shl : bitvector -> bitvector -> bitvector.
+Parameter bv_shr : bitvector -> bitvector -> bitvector.
+
+(*unary operations*)
+Parameter bv_not : bitvector -> bitvector.
+Parameter bv_neg : bitvector -> bitvector.
+Parameter bv_extr : forall (i n0 n1: N), bitvector -> bitvector.
+
+(*Parameter bv_extr : forall (n i j: N) {H0: n >= j} {H1: j >= i}, bitvector -> bitvector.*)
+
+Parameter bv_zextn : forall (n i: N), bitvector -> bitvector.
+Parameter bv_sextn : forall (n i: N), bitvector -> bitvector.
+
+(* All the operations are size-preserving *)
+
+Axiom bits_size : forall bv, List.length (bits bv) = N.to_nat (size bv).
+Axiom of_bits_size : forall l, N.to_nat (size (of_bits l)) = List.length l.
+Axiom _of_bits_size : forall l s,(size (_of_bits l s)) = s.
+Axiom zeros_size : forall n, size (zeros n) = n.
+Axiom bv_concat_size : forall n m a b, size a = n -> size b = m -> size (bv_concat a b) = n + m.
+Axiom bv_and_size : forall n a b, size a = n -> size b = n -> size (bv_and a b) = n.
+Axiom bv_or_size : forall n a b, size a = n -> size b = n -> size (bv_or a b) = n.
+Axiom bv_xor_size : forall n a b, size a = n -> size b = n -> size (bv_xor a b) = n.
+Axiom bv_add_size : forall n a b, size a = n -> size b = n -> size (bv_add a b) = n.
+Axiom bv_subt_size : forall n a b, size a = n -> size b = n -> size (bv_subt a b) = n.
+Axiom bv_mult_size : forall n a b, size a = n -> size b = n -> size (bv_mult a b) = n.
+Axiom bv_not_size : forall n a, size a = n -> size (bv_not a) = n.
+Axiom bv_neg_size : forall n a, size a = n -> size (bv_neg a) = n.
+Axiom bv_shl_size : forall n a b, size a = n -> size b = n -> size (bv_shl a b) = n.
+Axiom bv_shr_size : forall n a b, size a = n -> size b = n -> size (bv_shr a b) = n.
+
+Axiom bv_extr_size : forall i n0 n1 a, size a = n1 -> size (@bv_extr i n0 n1 a) = n0.
+
+(*
+Axiom bv_extr_size : forall n (i j: N) a (H0: n >= j) (H1: j >= i),
+ size a = n -> size (@bv_extr n i j H0 H1 a) = (j - i).
+*)
+
+Axiom bv_zextn_size : forall (n i: N) a,
+ size a = n -> size (@bv_zextn n i a) = (i + n).
+Axiom bv_sextn_size : forall (n i: N) a,
+ size a = n -> size (@bv_sextn n i a) = (i + n).
+
+(* Specification *)
+Axiom bv_eq_reflect : forall a b, bv_eq a b = true <-> a = b.
+Axiom bv_eq_refl : forall a, bv_eq a a = true.
+
+
+Axiom bv_ult_not_eq : forall a b, bv_ult a b = true -> a <> b.
+Axiom bv_slt_not_eq : forall a b, bv_slt a b = true -> a <> b.
+Axiom bv_ult_not_eqP : forall a b, bv_ultP a b -> a <> b.
+Axiom bv_slt_not_eqP : forall a b, bv_sltP a b -> a <> b.
+Axiom bv_ult_B2P : forall a b, bv_ult a b = true <-> bv_ultP a b.
+Axiom bv_slt_B2P : forall a b, bv_slt a b = true <-> bv_sltP a b.
+
+
+Axiom bv_and_comm : forall n a b, size a = n -> size b = n -> bv_and a b = bv_and b a.
+Axiom bv_or_comm : forall n a b, size a = n -> size b = n -> bv_or a b = bv_or b a.
+Axiom bv_add_comm : forall n a b, size a = n -> size b = n -> bv_add a b = bv_add b a.
+
+Axiom bv_and_assoc : forall n a b c, size a = n -> size b = n -> size c = n ->
+ (bv_and a (bv_and b c)) = (bv_and (bv_and a b) c).
+Axiom bv_or_assoc : forall n a b c, size a = n -> size b = n -> size c = n ->
+ (bv_or a (bv_or b c)) = (bv_or (bv_or a b) c).
+Axiom bv_xor_assoc : forall n a b c, size a = n -> size b = n -> size c = n ->
+ (bv_xor a (bv_xor b c)) = (bv_xor (bv_xor a b) c).
+Axiom bv_add_assoc : forall n a b c, size a = n -> size b = n -> size c = n ->
+ (bv_add a (bv_add b c)) = (bv_add (bv_add a b) c).
+Axiom bv_not_involutive: forall a, bv_not (bv_not a) = a.
+
+End RAWBITVECTOR.
+
+Module RAW2BITVECTOR (M:RAWBITVECTOR) <: BITVECTOR.
+
+ Record bitvector_ (n:N) : Type :=
+ MkBitvector
+ { bv :> M.bitvector;
+ wf : M.size bv = n
+ }.
+ Definition bitvector := bitvector_.
+
+ Definition bits n (bv:bitvector n) := M.bits bv.
+
+ Lemma of_bits_size l : M.size (M.of_bits l) = N.of_nat (List.length l).
+ Proof. now rewrite <- M.of_bits_size, N2Nat.id. Qed.
+
+ Lemma _of_bits_size l s: M.size (M._of_bits l s) = s.
+ Proof. apply (M._of_bits_size l s). Qed.
+
+ Definition of_bits (l:list bool) : bitvector (N.of_nat (List.length l)) :=
+ @MkBitvector _ (M.of_bits l) (of_bits_size l).
+
+ Definition _of_bits (l: list bool) (s : N): bitvector s :=
+ @MkBitvector _ (M._of_bits l s) (_of_bits_size l s).
+
+ Definition bitOf n p (bv:bitvector n) : bool := M.bitOf p bv.
+
+ Definition zeros (n:N) : bitvector n :=
+ @MkBitvector _ (M.zeros n) (M.zeros_size n).
+
+ Definition bv_eq n (bv1 bv2:bitvector n) := M.bv_eq bv1 bv2.
+
+ Definition bv_ultP n (bv1 bv2:bitvector n) := M.bv_ultP bv1 bv2.
+
+ Definition bv_sltP n (bv1 bv2:bitvector n) := M.bv_sltP bv1 bv2.
+
+ Definition bv_and n (bv1 bv2:bitvector n) : bitvector n :=
+ @MkBitvector n (M.bv_and bv1 bv2) (M.bv_and_size (wf bv1) (wf bv2)).
+
+ Definition bv_or n (bv1 bv2:bitvector n) : bitvector n :=
+ @MkBitvector n (M.bv_or bv1 bv2) (M.bv_or_size (wf bv1) (wf bv2)).
+
+ Definition bv_add n (bv1 bv2:bitvector n) : bitvector n :=
+ @MkBitvector n (M.bv_add bv1 bv2) (M.bv_add_size (wf bv1) (wf bv2)).
+
+ Definition bv_subt n (bv1 bv2:bitvector n) : bitvector n :=
+ @MkBitvector n (M.bv_subt bv1 bv2) (M.bv_subt_size (wf bv1) (wf bv2)).
+
+ Definition bv_mult n (bv1 bv2:bitvector n) : bitvector n :=
+ @MkBitvector n (M.bv_mult bv1 bv2) (M.bv_mult_size (wf bv1) (wf bv2)).
+
+ Definition bv_xor n (bv1 bv2:bitvector n) : bitvector n :=
+ @MkBitvector n (M.bv_xor bv1 bv2) (M.bv_xor_size (wf bv1) (wf bv2)).
+
+ Definition bv_ult n (bv1 bv2:bitvector n) : bool := M.bv_ult bv1 bv2.
+
+ Definition bv_slt n (bv1 bv2:bitvector n) : bool := M.bv_slt bv1 bv2.
+
+ Definition bv_not n (bv1: bitvector n) : bitvector n :=
+ @MkBitvector n (M.bv_not bv1) (M.bv_not_size (wf bv1)).
+
+ Definition bv_neg n (bv1: bitvector n) : bitvector n :=
+ @MkBitvector n (M.bv_neg bv1) (M.bv_neg_size (wf bv1)).
+
+ Definition bv_concat n m (bv1:bitvector n) (bv2: bitvector m) : bitvector (n + m) :=
+ @MkBitvector (n + m) (M.bv_concat bv1 bv2) (M.bv_concat_size (wf bv1) (wf bv2)).
+
+ Definition bv_extr (i n0 n1: N) (bv1: bitvector n1) : bitvector n0 :=
+ @MkBitvector n0 (@M.bv_extr i n0 n1 bv1) (@M.bv_extr_size i n0 n1 bv1 (wf bv1)).
+
+(*
+ Definition bv_extr n (i j: N) (H0: n >= j) (H1: j >= i) (bv1: bitvector n) : bitvector (j - i) :=
+ @MkBitvector (j - i) (@M.bv_extr n i j H0 H1 bv1) (@M.bv_extr_size n i j bv1 H0 H1 (wf bv1)).
+*)
+
+ Definition bv_zextn n (i: N) (bv1: bitvector n) : bitvector (i + n) :=
+ @MkBitvector (i + n) (@M.bv_zextn n i bv1) (@M.bv_zextn_size n i bv1 (wf bv1)).
+
+ Definition bv_sextn n (i: N) (bv1: bitvector n) : bitvector (i + n) :=
+ @MkBitvector (i + n) (@M.bv_sextn n i bv1) (@M.bv_sextn_size n i bv1 (wf bv1)).
+
+ Definition bv_shl n (bv1 bv2:bitvector n) : bitvector n :=
+ @MkBitvector n (M.bv_shl bv1 bv2) (M.bv_shl_size (wf bv1) (wf bv2)).
+
+ Definition bv_shr n (bv1 bv2:bitvector n) : bitvector n :=
+ @MkBitvector n (M.bv_shr bv1 bv2) (M.bv_shr_size (wf bv1) (wf bv2)).
+
+ Lemma bits_size n (bv:bitvector n) : List.length (bits bv) = N.to_nat n.
+ Proof. unfold bits. now rewrite M.bits_size, wf. Qed.
+
+ (* The next lemma is provable only if we assume proof irrelevance *)
+ Lemma bv_eq_reflect n (a b: bitvector n) : bv_eq a b = true <-> a = b.
+ Proof.
+ unfold bv_eq. rewrite M.bv_eq_reflect. split.
+ - revert a b. intros [a Ha] [b Hb]. simpl. intros ->.
+ rewrite (proof_irrelevance Ha Hb). reflexivity.
+ - intros. case a in *. case b in *. simpl in *.
+ now inversion H. (* now intros ->. *)
+ Qed.
+
+ Lemma bv_eq_refl n (a : bitvector n) : bv_eq a a = true.
+ Proof.
+ unfold bv_eq. now rewrite M.bv_eq_reflect.
+ Qed.
+
+ Lemma bv_ult_not_eqP: forall n (a b: bitvector n), bv_ultP a b -> a <> b.
+ Proof.
+ unfold bv_ultP, bv_ult. intros n a b H.
+ apply M.bv_ult_not_eqP in H. unfold not in *; intros. apply H.
+ apply M.bv_eq_reflect. rewrite H0. apply M.bv_eq_refl.
+ Qed.
+
+ Lemma bv_slt_not_eqP: forall n (a b: bitvector n), bv_sltP a b -> a <> b.
+ Proof.
+ unfold bv_sltP, bv_slt. intros n a b H.
+ apply M.bv_slt_not_eqP in H. unfold not in *; intros. apply H.
+ apply M.bv_eq_reflect. rewrite H0. apply M.bv_eq_refl.
+ Qed.
+
+ Lemma bv_ult_not_eq: forall n (a b: bitvector n), bv_ult a b = true -> a <> b.
+ Proof.
+ unfold bv_ult. intros n a b H.
+ apply M.bv_ult_not_eq in H. unfold not in *; intros. apply H.
+ apply M.bv_eq_reflect. rewrite H0. apply M.bv_eq_refl.
+ Qed.
+
+ Lemma bv_slt_not_eq: forall n (a b: bitvector n), bv_slt a b = true -> a <> b.
+ Proof.
+ unfold bv_slt. intros n a b H.
+ apply M.bv_slt_not_eq in H. unfold not in *; intros. apply H.
+ apply M.bv_eq_reflect. rewrite H0. apply M.bv_eq_refl.
+ Qed.
+
+ Lemma bv_ult_B2P: forall n (a b: bitvector n), bv_ult a b = true <-> bv_ultP a b.
+ Proof.
+ unfold bv_ultP, bv_ult; intros; split; intros;
+ now apply M.bv_ult_B2P.
+ Qed.
+
+ Lemma bv_slt_B2P: forall n (a b: bitvector n), bv_slt a b = true <-> bv_sltP a b.
+ Proof.
+ unfold bv_ultP, bv_slt; intros; split; intros;
+ now apply M.bv_slt_B2P.
+ Qed.
+
+ Lemma bv_and_comm n (a b:bitvector n) : bv_eq (bv_and a b) (bv_and b a) = true.
+ Proof.
+ unfold bv_eq. rewrite M.bv_eq_reflect. apply (@M.bv_and_comm n); now rewrite wf.
+ Qed.
+
+ Lemma bv_or_comm n (a b:bitvector n) : bv_eq (bv_or a b) (bv_or b a) = true.
+ Proof.
+ unfold bv_eq. rewrite M.bv_eq_reflect. apply (@M.bv_or_comm n); now rewrite wf.
+ Qed.
+
+ Lemma bv_add_comm n (a b:bitvector n) : bv_eq (bv_add a b) (bv_add b a) = true.
+ Proof.
+ unfold bv_eq. rewrite M.bv_eq_reflect. apply (@M.bv_add_comm n); now rewrite wf.
+ Qed.
+
+ Lemma bv_and_assoc : forall n (a b c :bitvector n), bv_eq (bv_and a (bv_and b c)) (bv_and (bv_and a b) c) = true.
+ Proof.
+ intros n a b c.
+ unfold bv_eq. rewrite M.bv_eq_reflect. simpl.
+ apply (@M.bv_and_assoc n a b c); now rewrite wf.
+ Qed.
+
+ Lemma bv_or_assoc : forall n (a b c :bitvector n), bv_eq (bv_or a (bv_or b c)) (bv_or (bv_or a b) c) = true.
+ Proof.
+ intros n a b c.
+ unfold bv_eq. rewrite M.bv_eq_reflect. simpl.
+ apply (@M.bv_or_assoc n a b c); now rewrite wf.
+ Qed.
+
+ Lemma bv_xor_assoc : forall n (a b c :bitvector n), bv_eq (bv_xor a (bv_xor b c)) (bv_xor (bv_xor a b) c) = true.
+ Proof.
+ intros n a b c.
+ unfold bv_eq. rewrite M.bv_eq_reflect. simpl.
+ apply (@M.bv_xor_assoc n a b c); now rewrite wf.
+ Qed.
+
+ Lemma bv_add_assoc : forall n (a b c :bitvector n), bv_eq (bv_add a (bv_add b c)) (bv_add (bv_add a b) c) = true.
+ Proof.
+ intros n a b c.
+ unfold bv_eq. rewrite M.bv_eq_reflect. simpl.
+ apply (@M.bv_add_assoc n a b c); now rewrite wf.
+ Qed.
+
+ Lemma bv_not_involutive: forall n (a: bitvector n), bv_eq (bv_not (bv_not a)) a = true.
+ Proof.
+ intros n a.
+ unfold bv_eq. rewrite M.bv_eq_reflect. simpl.
+ apply (@M.bv_not_involutive a); now rewrite wf.
+ Qed.
+
+
+End RAW2BITVECTOR.
+
+Module RAWBITVECTOR_LIST <: RAWBITVECTOR.
+
+Definition bitvector := list bool.
+Definition bits (a:bitvector) : list bool := a.
+Definition size (a:bitvector) := N.of_nat (List.length a).
+Definition of_bits (a:list bool) : bitvector := a.
+
+Lemma bits_size bv : List.length (bits bv) = N.to_nat (size bv).
+Proof. unfold bits, size. now rewrite Nat2N.id. Qed.
+
+Lemma of_bits_size l : N.to_nat (size (of_bits l)) = List.length l.
+Proof. unfold of_bits, size. now rewrite Nat2N.id. Qed.
+
+Fixpoint beq_list (l m : list bool) {struct l} :=
+ match l, m with
+ | nil, nil => true
+ | x :: l', y :: m' => (Bool.eqb x y) && (beq_list l' m')
+ | _, _ => false
+ end.
+
+Definition bv_eq (a b: bitvector): bool:=
+ if ((size a) =? (size b)) then beq_list (bits a) (bits b) else false.
+
+Fixpoint beq_listP (l m : list bool) {struct l} :=
+ match l, m with
+ | nil, nil => True
+ | x :: l', y :: m' => (x = y) /\ (beq_listP l' m')
+ | _, _ => False
+ end.
+
+Lemma bv_mk_eq l1 l2 : bv_eq l1 l2 = beq_list l1 l2.
+Proof.
+ unfold bv_eq, size, bits.
+ case_eq (Nat_eqb (length l1) (length l2)); intro Heq.
+ - now rewrite (EqNat.beq_nat_true _ _ Heq), N.eqb_refl.
+ - replace (N.of_nat (length l1) =? N.of_nat (length l2)) with false.
+ * revert l2 Heq. induction l1 as [ |b1 l1 IHl1]; intros [ |b2 l2]; simpl in *; auto.
+ intro Heq. now rewrite <- (IHl1 _ Heq), andb_false_r.
+ * symmetry. rewrite N.eqb_neq. intro H. apply Nat2N.inj in H. rewrite H in Heq.
+ rewrite <- EqNat.beq_nat_refl in Heq. discriminate.
+Qed.
+
+Definition bv_concat (a b: bitvector) : bitvector := b ++ a.
+
+Section Map2.
+
+ Variables A B C: Type.
+ Variable f : A -> B -> C.
+
+ Fixpoint map2 (l1 : list A) (l2 : list B) {struct l1} : list C :=
+ match l1, l2 with
+ | b1::tl1, b2::tl2 => (f b1 b2)::(map2 tl1 tl2)
+ | _, _ => nil
+ end.
+
+End Map2.
+
+Section Fold_left2.
+
+ Variables A B: Type.
+ Variable f : A -> B -> B -> A.
+
+ Fixpoint fold_left2 (xs ys: list B) (acc:A) {struct xs} : A :=
+ match xs, ys with
+ | nil, _ | _, nil => acc
+ | x::xs, y::ys => fold_left2 xs ys (f acc x y)
+ end.
+
+ Lemma foo : forall (I: A -> Prop) acc, I acc ->
+ (forall a b1 b2, I a -> I (f a b1 b2)) ->
+ forall xs ys, I (fold_left2 xs ys acc).
+ Proof. intros I acc H0 H1 xs. revert acc H0.
+ induction xs as [ | a xs IHxs]; intros acc H.
+ simpl. auto.
+ intros [ | b ys].
+ + simpl. exact H.
+ + simpl. apply IHxs, H1. exact H.
+ Qed.
+
+Fixpoint mk_list_true_acc (t: nat) (acc: list bool) : list bool :=
+ match t with
+ | O => acc
+ | S t' => mk_list_true_acc t' (true::acc)
+ end.
+
+Fixpoint mk_list_true (t: nat) : list bool :=
+ match t with
+ | O => []
+ | S t' => true::(mk_list_true t')
+ end.
+
+Fixpoint mk_list_false_acc (t: nat) (acc: list bool) : list bool :=
+ match t with
+ | O => acc
+ | S t' => mk_list_false_acc t' (false::acc)
+ end.
+
+Fixpoint mk_list_false (t: nat) : list bool :=
+ match t with
+ | O => []
+ | S t' => false::(mk_list_false t')
+ end.
+
+Definition zeros (n : N) : bitvector := mk_list_false (N.to_nat n).
+
+End Fold_left2.
+
+Definition bitOf (n: nat) (a: bitvector): bool := nth n a false.
+
+Definition bv_and (a b : bitvector) : bitvector :=
+ match (@size a) =? (@size b) with
+ | true => map2 andb (@bits a) (@bits b)
+ | _ => nil
+ end.
+
+Definition bv_or (a b : bitvector) : bitvector :=
+ match (@size a) =? (@size b) with
+ | true => map2 orb (@bits a) (@bits b)
+ | _ => nil
+ end.
+
+Definition bv_xor (a b : bitvector) : bitvector :=
+ match (@size a) =? (@size b) with
+ | true => map2 xorb (@bits a) (@bits b)
+ | _ => nil
+ end.
+
+Definition bv_not (a: bitvector) : bitvector := map negb (@bits a).
+
+
+(*arithmetic operations*)
+
+ (*addition*)
+
+Definition add_carry b1 b2 c :=
+ match b1, b2, c with
+ | true, true, true => (true, true)
+ | true, true, false
+ | true, false, true
+ | false, true, true => (false, true)
+ | false, false, true
+ | false, true, false
+ | true, false, false => (true, false)
+ | false, false, false => (false, false)
+ end.
+
+(* Truncating addition in little-endian, direct style *)
+
+Fixpoint add_list_ingr bs1 bs2 c {struct bs1} :=
+ match bs1, bs2 with
+ | nil, _ => nil
+ | _ , nil => nil
+ | b1 :: bs1, b2 :: bs2 =>
+ let (r, c) := add_carry b1 b2 c in r :: (add_list_ingr bs1 bs2 c)
+ end.
+
+Definition add_list (a b: list bool) := add_list_ingr a b false.
+
+Definition bv_add (a b : bitvector) : bitvector :=
+ match (@size a) =? (@size b) with
+ | true => add_list a b
+ | _ => nil
+ end.
+
+ (*substraction*)
+
+Definition twos_complement b :=
+ add_list_ingr (map negb b) (mk_list_false (length b)) true.
+
+Definition bv_neg (a: bitvector) : bitvector := (twos_complement a).
+
+Definition subst_list' a b := add_list a (twos_complement b).
+
+Definition bv_subt' (a b : bitvector) : bitvector :=
+ match (@size a) =? (@size b) with
+ | true => (subst_list' (@bits a) (@bits b))
+ | _ => nil
+ end.
+
+Definition subst_borrow b1 b2 b :=
+ match b1, b2, b with
+ | true, true, true => (true, true)
+ | true, true, false => (false, false)
+ | true, false, true => (false, false)
+ | false, true, true => (false, true)
+ | false, false, true => (true, true)
+ | false, true, false => (true, true)
+ | true, false, false => (true, false)
+ | false, false, false => (false, false)
+ end.
+
+Fixpoint subst_list_borrow bs1 bs2 b {struct bs1} :=
+ match bs1, bs2 with
+ | nil, _ => nil
+ | _ , nil => nil
+ | b1 :: bs1, b2 :: bs2 =>
+ let (r, b) := subst_borrow b1 b2 b in r :: (subst_list_borrow bs1 bs2 b)
+ end.
+
+Definition subst_list (a b: list bool) := subst_list_borrow a b false.
+
+Definition bv_subt (a b : bitvector) : bitvector :=
+ match (@size a) =? (@size b) with
+ | true => subst_list (@bits a) (@bits b)
+ | _ => nil
+ end.
+
+(*less than*)
+
+Fixpoint ult_list_big_endian (x y: list bool) :=
+ match x, y with
+ | nil, _ => false
+ | _ , nil => false
+ | xi :: nil, yi :: nil => andb (negb xi) yi
+ | xi :: x', yi :: y' =>
+ orb (andb (Bool.eqb xi yi) (ult_list_big_endian x' y'))
+ (andb (negb xi) yi)
+ end.
+
+Definition ult_list (x y: list bool) :=
+ (ult_list_big_endian (List.rev x) (List.rev y)).
+
+
+Fixpoint slt_list_big_endian (x y: list bool) :=
+ match x, y with
+ | nil, _ => false
+ | _ , nil => false
+ | xi :: nil, yi :: nil => andb xi (negb yi)
+ | xi :: x', yi :: y' =>
+ orb (andb (Bool.eqb xi yi) (ult_list_big_endian x' y'))
+ (andb xi (negb yi))
+ end.
+
+Definition slt_list (x y: list bool) :=
+ slt_list_big_endian (List.rev x) (List.rev y).
+
+
+Definition bv_ult (a b : bitvector) : bool :=
+ if @size a =? @size b then ult_list a b else false.
+
+
+Definition bv_slt (a b : bitvector) : bool :=
+ if @size a =? @size b then slt_list a b else false.
+
+Definition ult_listP (x y: list bool) :=
+ if ult_list x y then True else False.
+
+Definition slt_listP (x y: list bool) :=
+ if slt_list x y then True else False.
+
+Definition bv_ultP (a b : bitvector) : Prop :=
+ if @size a =? @size b then ult_listP a b else False.
+
+Definition bv_sltP (a b : bitvector) : Prop :=
+ if @size a =? @size b then slt_listP a b else False.
+
+
+ (*multiplication*)
+
+Fixpoint mult_list_carry (a b :list bool) n {struct a}: list bool :=
+ match a with
+ | nil => mk_list_false n
+ | a' :: xs =>
+ if a' then
+ add_list b (mult_list_carry xs (false :: b) n)
+ else
+ mult_list_carry xs (false :: b) n
+ end.
+
+Fixpoint mult_list_carry2 (a b :list bool) n {struct a}: list bool :=
+ match a with
+ | nil => mk_list_false n
+ | a' :: xs =>
+ if a' then
+ add_list b (mult_list_carry2 xs (false :: (removelast b)) n)
+ else
+ mult_list_carry2 xs (false :: (removelast b)) n
+ end.
+
+Fixpoint and_with_bool (a: list bool) (bt: bool) : list bool :=
+ match a with
+ | nil => nil
+ | ai :: a' => (bt && ai) :: and_with_bool a' bt
+ end.
+
+
+Fixpoint mult_bool_step_k_h (a b: list bool) (c: bool) (k: Z) : list bool :=
+ match a, b with
+ | nil , _ => nil
+ | ai :: a', bi :: b' =>
+ if (k - 1 <? 0)%Z then
+ let carry_out := (ai && bi) || ((xorb ai bi) && c) in
+ let curr := xorb (xorb ai bi) c in
+ curr :: mult_bool_step_k_h a' b' carry_out (k - 1)
+ else
+ ai :: mult_bool_step_k_h a' b c (k - 1)
+ | ai :: a' , nil => ai :: mult_bool_step_k_h a' b c k
+ end.
+
+Local Open Scope int63_scope.
+
+Fixpoint top_k_bools (a: list bool) (k: int) : list bool :=
+ if (k == 0) then nil
+ else match a with
+ | nil => nil
+ | ai :: a' => ai :: top_k_bools a' (k - 1)
+ end.
+
+
+Fixpoint mult_bool_step (a b: list bool) (res: list bool) (k k': nat) : list bool :=
+ let ak := List.firstn (S k') a in
+ let b' := and_with_bool ak (nth k b false) in
+ let res' := mult_bool_step_k_h res b' false (Z.of_nat k) in
+ match k' with
+ | O => res'
+ (* | S O => res' *)
+ | S pk' => mult_bool_step a b res' (S k) pk'
+ end.
+
+Definition bvmult_bool (a b: list bool) (n: nat) : list bool :=
+ let res := and_with_bool a (nth 0 b false) in
+ match n with
+ | O => res
+ | S O => res
+ | S (S k) => mult_bool_step a b res 1 k
+ end.
+
+Definition mult_list a b := bvmult_bool a b (length a).
+
+Definition bv_mult (a b : bitvector) : bitvector :=
+ if ((@size a) =? (@size b))
+ then mult_list a b
+ else zeros (@size a).
+
+(* Theorems *)
+
+Lemma length_mk_list_false: forall n, length (mk_list_false n) = n.
+Proof. intro n.
+ induction n as [ | n' IHn].
+ - simpl. auto.
+ - simpl. apply f_equal. exact IHn.
+Qed.
+
+Definition _of_bits (a:list bool) (s: N) :=
+if (N.of_nat (length a) =? s) then a else zeros s.
+
+Lemma _of_bits_size l s: (size (_of_bits l s)) = s.
+Proof. unfold of_bits, size. unfold _of_bits.
+ case_eq ( N.of_nat (length l) =? s).
+ intros. now rewrite N.eqb_eq in H.
+ intros. unfold zeros. rewrite length_mk_list_false.
+ now rewrite N2Nat.id.
+Qed.
+
+Lemma length_mk_list_true: forall n, length (mk_list_true n) = n.
+Proof. intro n.
+ induction n as [ | n' IHn].
+ - simpl. auto.
+ - simpl. apply f_equal. exact IHn.
+Qed.
+
+Lemma zeros_size (n : N) : size (zeros n) = n.
+Proof. unfold size, zeros. now rewrite length_mk_list_false, N2Nat.id. Qed.
+
+Lemma List_eq : forall (l m: list bool), beq_list l m = true <-> l = m.
+Proof.
+ induction l; destruct m; simpl; split; intro; try (reflexivity || discriminate).
+ - rewrite andb_true_iff in H. destruct H. rewrite eqb_true_iff in H. rewrite H.
+ apply f_equal. apply IHl. exact H0.
+ - inversion H. subst b. subst m. rewrite andb_true_iff. split.
+ + apply eqb_reflx.
+ + apply IHl; reflexivity.
+Qed.
+
+Lemma List_eqP : forall (l m: list bool), beq_listP l m <-> l = m.
+Proof.
+ induction l; destruct m; simpl; split; intro; try (reflexivity || discriminate); try now contradict H.
+ - destruct H. rewrite H.
+ apply f_equal. apply IHl. exact H0.
+ - inversion H. subst b. subst m. split.
+ + reflexivity.
+ + apply IHl; reflexivity.
+Qed.
+
+Lemma List_eq_refl : forall (l: list bool), beq_list l l = true.
+Proof.
+ induction l; simpl; try (reflexivity || discriminate).
+ - rewrite andb_true_iff. split. apply eqb_reflx. apply IHl.
+Qed.
+
+Lemma List_eqP_refl : forall (l: list bool), beq_listP l l <-> l = l.
+Proof. intro l.
+ induction l as [ | xl xsl IHl ]; intros.
+ - easy.
+ - simpl. repeat split. now apply IHl.
+Qed.
+
+Lemma List_neq : forall (l m: list bool), beq_list l m = false -> l <> m.
+Proof.
+ intro l.
+ induction l.
+ - intros. case m in *; simpl. now contradict H. easy.
+ - intros. simpl in H.
+ case_eq m; intros; rewrite H0 in H.
+ easy. simpl.
+ case_eq (Bool.eqb a b); intros.
+ rewrite H1 in H. rewrite andb_true_l in H.
+ apply Bool.eqb_prop in H1.
+ specialize (IHl l0 H).
+ rewrite H1.
+ unfold not in *.
+ intros. apply IHl.
+ now inversion H2.
+ apply Bool.eqb_false_iff in H1.
+ unfold not in *.
+ intros. apply H1.
+ now inversion H2.
+Qed.
+
+Lemma List_neqP : forall (l m: list bool), ~beq_listP l m -> l <> m.
+Proof.
+ intro l.
+ induction l.
+ - intros. case m in *; simpl. now contradict H. easy.
+ - intros. unfold not in H. simpl in H.
+ case_eq m; intros. easy.
+ rewrite H0 in H.
+ unfold not. intros. apply H. inversion H1.
+ split; try easy.
+ now apply List_eqP_refl.
+Qed.
+
+Lemma bv_eq_reflect a b : bv_eq a b = true <-> a = b.
+Proof.
+ unfold bv_eq. case_eq (size a =? size b); intro Heq; simpl.
+ - apply List_eq.
+ - split; try discriminate.
+ intro H. rewrite H, N.eqb_refl in Heq. discriminate.
+Qed.
+
+Lemma bv_eq_refl a: bv_eq a a = true.
+Proof.
+ unfold bv_eq. rewrite N.eqb_refl. now apply List_eq.
+Qed.
+
+Lemma bv_concat_size n m a b : size a = n -> size b = m -> size (bv_concat a b) = (n + m)%N.
+Proof.
+ unfold bv_concat, size. intros H0 H1.
+ rewrite app_length, Nat2N.inj_add, H0, H1; now rewrite N.add_comm.
+Qed.
+
+(*list bitwise AND properties*)
+
+Lemma map2_and_comm: forall (a b: list bool), (map2 andb a b) = (map2 andb b a).
+Proof. intros a. induction a as [ | a' xs IHxs].
+ intros [ | b' ys].
+ - simpl. auto.
+ - simpl. auto.
+ - intros [ | b' ys].
+ + simpl. auto.
+ + intros. simpl.
+ cut (a' && b' = b' && a'). intro H. rewrite <- H. apply f_equal.
+ apply IHxs. apply andb_comm.
+Qed.
+
+Lemma map2_and_assoc: forall (a b c: list bool), (map2 andb a (map2 andb b c)) = (map2 andb (map2 andb a b) c).
+Proof. intro a. induction a as [ | a' xs IHxs].
+ simpl. auto.
+ intros [ | b' ys].
+ - simpl. auto.
+ - intros [ | c' zs].
+ + simpl. auto.
+ + simpl. cut (a' && (b' && c') = a' && b' && c'). intro H. rewrite <- H. apply f_equal.
+ apply IHxs. apply andb_assoc.
+Qed.
+
+Lemma map2_and_idem1: forall (a b: list bool), (map2 andb (map2 andb a b) a) = (map2 andb a b).
+Proof. intros a. induction a as [ | a' xs IHxs].
+ intros [ | b' ys].
+ - simpl. auto.
+ - simpl. auto.
+ - intros [ | b' ys].
+ + simpl. auto.
+ + intros. simpl.
+ cut (a' && b' && a' = a' && b'). intro H. rewrite H. apply f_equal.
+ apply IHxs. rewrite andb_comm, andb_assoc, andb_diag. reflexivity.
+Qed.
+
+Lemma map2_and_idem_comm: forall (a b: list bool), (map2 andb (map2 andb a b) a) = (map2 andb b a).
+Proof. intros a b. symmetry. rewrite <- map2_and_comm. symmetry; apply map2_and_idem1. Qed.
+
+Lemma map2_and_idem2: forall (a b: list bool), (map2 andb (map2 andb a b) b) = (map2 andb a b).
+Proof. intros a. induction a as [ | a' xs IHxs].
+ intros [ | b' ys].
+ - simpl. auto.
+ - simpl. auto.
+ - intros [ | b' ys].
+ + simpl. auto.
+ + intros. simpl.
+ cut (a' && b' && b' = a' && b'). intro H. rewrite H. apply f_equal.
+ apply IHxs. rewrite <- andb_assoc. rewrite andb_diag. reflexivity.
+Qed.
+
+Lemma map2_and_idem_comm2: forall (a b: list bool), (map2 andb (map2 andb a b) b) = (map2 andb b a).
+Proof. intros a b. symmetry. rewrite <- map2_and_comm. symmetry; apply map2_and_idem2. Qed.
+
+Lemma map2_and_empty_empty1: forall (a: list bool), (map2 andb a []) = [].
+Proof. intros a. induction a as [ | a' xs IHxs]; simpl; auto. Qed.
+
+Lemma map2_and_empty_empty2: forall (a: list bool), (map2 andb [] a) = [].
+Proof. intros a. rewrite map2_and_comm. apply map2_and_empty_empty1. Qed.
+
+Lemma map2_nth_empty_false: forall (i: nat), nth i [] false = false.
+Proof. intros i. induction i as [ | IHi]; simpl; reflexivity. Qed.
+
+Lemma mk_list_true_equiv: forall t acc, mk_list_true_acc t acc = (List.rev (mk_list_true t)) ++ acc.
+Proof. induction t as [ |t IHt]; auto; intro acc; simpl; rewrite IHt.
+ rewrite app_assoc_reverse.
+ apply f_equal. simpl. reflexivity.
+Qed.
+
+Lemma mk_list_false_equiv: forall t acc, mk_list_false_acc t acc = (List.rev (mk_list_false t)) ++ acc.
+Proof. induction t as [ |t IHt]; auto; intro acc; simpl; rewrite IHt.
+ rewrite app_assoc_reverse.
+ apply f_equal. simpl. reflexivity.
+Qed.
+
+Lemma len_mk_list_true_empty: length (mk_list_true_acc 0 []) = 0%nat.
+Proof. simpl. reflexivity. Qed.
+
+Lemma add_mk_list_true: forall n acc, length (mk_list_true_acc n acc) = (n + length acc)%nat.
+Proof. intros n.
+ induction n as [ | n' IHn].
+ + auto.
+ + intro acc. simpl. rewrite IHn. simpl. lia.
+Qed.
+
+Lemma map2_and_nth_bitOf: forall (a b: list bool) (i: nat),
+ (length a) = (length b) ->
+ (i <= (length a))%nat ->
+ nth i (map2 andb a b) false = (nth i a false) && (nth i b false).
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ - intros [ | b ys].
+ + intros i H0 H1. do 2 rewrite map2_nth_empty_false. reflexivity.
+ + intros i H0 H1. rewrite map2_and_empty_empty2.
+ rewrite map2_nth_empty_false. reflexivity.
+ - intros [ | b ys].
+ + intros i H0 H1. rewrite map2_and_empty_empty1.
+ rewrite map2_nth_empty_false. rewrite andb_false_r. reflexivity.
+ + intros i H0 H1. simpl.
+ revert i H1. intros [ | i]; [ |intros IHi].
+ * simpl. auto.
+ * apply IHxs.
+ inversion H0; reflexivity.
+ inversion IHi; lia.
+Qed.
+
+Lemma length_mk_list_true_full: forall n, length (mk_list_true_acc n []) = n.
+Proof. intro n. rewrite (@add_mk_list_true n []). auto. Qed.
+
+Lemma mk_list_app: forall n acc, mk_list_true_acc n acc = mk_list_true_acc n [] ++ acc.
+Proof. intro n.
+ induction n as [ | n IHn].
+ + auto.
+ + intro acc. simpl in *. rewrite IHn.
+ cut (mk_list_true_acc n [] ++ [true] = mk_list_true_acc n [true]). intro H.
+ rewrite <- H. rewrite <- app_assoc. unfold app. reflexivity.
+ rewrite <- IHn. reflexivity.
+Qed.
+
+Lemma mk_list_ltrue: forall n, mk_list_true_acc n [true] = mk_list_true_acc (S n) [].
+Proof. intro n. induction n as [ | n IHn]; auto. Qed.
+
+Lemma map2_and_1_neutral: forall (a: list bool), (map2 andb a (mk_list_true (length a))) = a.
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ + auto.
+ + simpl. rewrite IHxs.
+ rewrite andb_true_r. reflexivity.
+Qed.
+
+Lemma map2_and_0_absorb: forall (a: list bool), (map2 andb a (mk_list_false (length a))) = (mk_list_false (length a)).
+Proof. intro a. induction a as [ | a' xs IHxs].
+ - simpl. reflexivity.
+ - simpl. rewrite IHxs.
+ rewrite andb_false_r; reflexivity.
+Qed.
+
+Lemma map2_and_length: forall (a b: list bool), length a = length b -> length a = length (map2 andb a b).
+Proof. induction a as [ | a' xs IHxs].
+ simpl. auto.
+ intros [ | b ys].
+ - simpl. intros. exact H.
+ - intros. simpl in *. apply f_equal. apply IHxs.
+ inversion H; auto.
+Qed.
+
+(*bitvector AND properties*)
+
+Lemma bv_and_size n a b : size a = n -> size b = n -> size (bv_and a b) = n.
+Proof.
+ unfold bv_and. intros H1 H2. rewrite H1, H2.
+ rewrite N.eqb_compare. rewrite N.compare_refl.
+ unfold size in *. rewrite <- map2_and_length.
+ - exact H1.
+ - unfold bits. now rewrite <- Nat2N.inj_iff, H1.
+Qed.
+
+Lemma bv_and_comm n a b : size a = n -> size b = n -> bv_and a b = bv_and b a.
+Proof.
+ intros H1 H2. unfold bv_and. rewrite H1, H2.
+ rewrite N.eqb_compare, N.compare_refl.
+ rewrite map2_and_comm. reflexivity.
+Qed.
+
+Lemma bv_and_assoc: forall n a b c, size a = n -> size b = n -> size c = n ->
+ (bv_and a (bv_and b c)) = (bv_and (bv_and a b) c).
+Proof. intros n a b c H0 H1 H2.
+ unfold bv_and, size, bits in *. rewrite H1, H2.
+ rewrite N.eqb_compare. rewrite N.eqb_compare. rewrite N.compare_refl.
+ rewrite N.eqb_compare. rewrite N.eqb_compare. rewrite H0. rewrite N.compare_refl.
+ rewrite <- (@map2_and_length a b). rewrite <- map2_and_length. rewrite H0, H1.
+ rewrite N.compare_refl.
+ rewrite map2_and_assoc; reflexivity.
+ now rewrite <- Nat2N.inj_iff, H1.
+ now rewrite <- Nat2N.inj_iff, H0.
+Qed.
+
+Lemma bv_and_idem1: forall a b n, size a = n -> size b = n -> (bv_and (bv_and a b) a) = (bv_and a b).
+Proof. intros a b n H0 H1.
+ unfold bv_and. rewrite H0. do 2 rewrite N.eqb_compare.
+ unfold size in *.
+ rewrite H1. rewrite N.compare_refl.
+ rewrite <- H0. unfold bits.
+ rewrite <- map2_and_length. rewrite N.compare_refl.
+ rewrite map2_and_idem1; reflexivity.
+ now rewrite <- Nat2N.inj_iff, H1.
+Qed.
+
+Lemma bv_and_idem2: forall a b n, size a = n -> size b = n -> (bv_and (bv_and a b) b) = (bv_and a b).
+Proof. intros a b n H0 H1.
+ unfold bv_and. rewrite H0. do 2 rewrite N.eqb_compare.
+ unfold size in *.
+ rewrite H1. rewrite N.compare_refl.
+ rewrite <- H0. unfold bits.
+ rewrite <- map2_and_length. rewrite N.compare_refl.
+ rewrite map2_and_idem2; reflexivity.
+ now rewrite <- Nat2N.inj_iff, H1.
+Qed.
+
+Definition bv_empty: bitvector := nil.
+
+Lemma bv_and_empty_empty1: forall a, (bv_and a bv_empty) = bv_empty.
+Proof. intros a. unfold bv_empty, bv_and, size, bits. simpl.
+ rewrite map2_and_empty_empty1.
+ case_eq (N.compare (N.of_nat (length a)) 0); intro H; simpl.
+ - apply (N.compare_eq (N.of_nat (length a))) in H.
+ rewrite H. simpl. reflexivity.
+ - rewrite N.eqb_compare. rewrite H; reflexivity.
+ - rewrite N.eqb_compare. rewrite H; reflexivity.
+Qed.
+
+Lemma bv_and_nth_bitOf: forall a b n (i: nat),
+ (size a) = n -> (size b) = n ->
+ (i <= (nat_of_N (size a)))%nat ->
+ nth i (bits (bv_and a b)) false = (nth i (bits a) false) && (nth i (bits b) false).
+Proof. intros a b n i H0 H1 H2.
+ unfold bv_and. rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl.
+ apply map2_and_nth_bitOf; unfold size in *; unfold bits.
+ now rewrite <- Nat2N.inj_iff, H1. rewrite Nat2N.id in H2; exact H2.
+Qed.
+
+Lemma bv_and_empty_empty2: forall a, (bv_and bv_empty a) = bv_empty.
+Proof. intro a. unfold bv_and, bv_empty, size.
+ case (length a); simpl; auto.
+Qed.
+
+Lemma bv_and_1_neutral: forall a, (bv_and a (mk_list_true (length (bits a)))) = a.
+Proof. intro a. unfold bv_and.
+ rewrite N.eqb_compare. unfold size, bits. rewrite length_mk_list_true.
+ rewrite N.compare_refl.
+ rewrite map2_and_1_neutral. reflexivity.
+Qed.
+
+Lemma bv_and_0_absorb: forall a, (bv_and a (mk_list_false (length (bits a)))) = (mk_list_false (length (bits a))).
+Proof. intro a. unfold bv_and.
+ rewrite N.eqb_compare. unfold size, bits. rewrite length_mk_list_false.
+ rewrite N.compare_refl.
+ rewrite map2_and_0_absorb. reflexivity.
+Qed.
+
+(* lists bitwise OR properties *)
+
+Lemma map2_or_comm: forall (a b: list bool), (map2 orb a b) = (map2 orb b a).
+Proof. intros a. induction a as [ | a' xs IHxs].
+ intros [ | b' ys].
+ - simpl. auto.
+ - simpl. auto.
+ - intros [ | b' ys].
+ + simpl. auto.
+ + intros. simpl.
+ cut (a' || b' = b' || a'). intro H. rewrite <- H. apply f_equal.
+ apply IHxs. apply orb_comm.
+Qed.
+
+Lemma map2_or_assoc: forall (a b c: list bool), (map2 orb a (map2 orb b c)) = (map2 orb (map2 orb a b) c).
+Proof. intro a. induction a as [ | a' xs IHxs].
+ simpl. auto.
+ intros [ | b' ys].
+ - simpl. auto.
+ - intros [ | c' zs].
+ + simpl. auto.
+ + simpl. cut (a' || (b' || c') = a' || b' || c'). intro H. rewrite <- H. apply f_equal.
+ apply IHxs. apply orb_assoc.
+Qed.
+
+Lemma map2_or_length: forall (a b: list bool), length a = length b -> length a = length (map2 orb a b).
+Proof. induction a as [ | a' xs IHxs].
+ simpl. auto.
+ intros [ | b ys].
+ - simpl. intros. exact H.
+ - intros. simpl in *. apply f_equal. apply IHxs.
+ inversion H; auto.
+Qed.
+
+Lemma map2_or_empty_empty1: forall (a: list bool), (map2 orb a []) = [].
+Proof. intros a. induction a as [ | a' xs IHxs]; simpl; auto. Qed.
+
+Lemma map2_or_empty_empty2: forall (a: list bool), (map2 orb [] a) = [].
+Proof. intros a. rewrite map2_or_comm. apply map2_or_empty_empty1. Qed.
+
+Lemma map2_or_nth_bitOf: forall (a b: list bool) (i: nat),
+ (length a) = (length b) ->
+ (i <= (length a))%nat ->
+ nth i (map2 orb a b) false = (nth i a false) || (nth i b false).
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ - intros [ | b ys].
+ + intros i H0 H1. do 2 rewrite map2_nth_empty_false. reflexivity.
+ + intros i H0 H1. rewrite map2_or_empty_empty2.
+ rewrite map2_nth_empty_false. contradict H1. simpl. unfold not. intros. easy.
+ - intros [ | b ys].
+ + intros i H0 H1. rewrite map2_or_empty_empty1.
+ rewrite map2_nth_empty_false. rewrite orb_false_r. rewrite H0 in H1.
+ contradict H1. simpl. unfold not. intros. easy.
+ + intros i H0 H1. simpl.
+ revert i H1. intros [ | i]; [ |intros IHi].
+ * simpl. auto.
+ * apply IHxs.
+ inversion H0; reflexivity.
+ inversion IHi; lia.
+Qed.
+
+Lemma map2_or_0_neutral: forall (a: list bool), (map2 orb a (mk_list_false (length a))) = a.
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ + auto.
+ + simpl. rewrite IHxs.
+ rewrite orb_false_r. reflexivity.
+Qed.
+
+Lemma map2_or_1_true: forall (a: list bool), (map2 orb a (mk_list_true (length a))) = (mk_list_true (length a)).
+Proof. intro a. induction a as [ | a' xs IHxs].
+ - simpl. reflexivity.
+ - simpl. rewrite IHxs.
+ rewrite orb_true_r; reflexivity.
+Qed.
+
+(*bitvector OR properties*)
+
+Lemma bv_or_size n a b : size a = n -> size b = n -> size (bv_or a b) = n.
+Proof.
+ unfold bv_or. intros H1 H2. rewrite H1, H2.
+ rewrite N.eqb_compare. rewrite N.compare_refl.
+ unfold size in *. rewrite <- map2_or_length.
+ - exact H1.
+ - unfold bits. now rewrite <- Nat2N.inj_iff, H1.
+Qed.
+
+Lemma bv_or_comm: forall n a b, (size a) = n -> (size b) = n -> bv_or a b = bv_or b a.
+Proof. intros a b n H0 H1. unfold bv_or.
+ rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl.
+ rewrite map2_or_comm. reflexivity.
+Qed.
+
+Lemma bv_or_assoc: forall n a b c, (size a) = n -> (size b) = n -> (size c) = n ->
+ (bv_or a (bv_or b c)) = (bv_or (bv_or a b) c).
+Proof. intros n a b c H0 H1 H2.
+ unfold bv_or. rewrite H1, H2.
+ rewrite N.eqb_compare. rewrite N.eqb_compare. rewrite N.compare_refl.
+ unfold size, bits in *. rewrite <- (@map2_or_length b c).
+ rewrite H0, H1.
+ rewrite N.compare_refl.
+ rewrite N.eqb_compare. rewrite N.eqb_compare.
+ rewrite N.compare_refl. rewrite <- (@map2_or_length a b).
+ rewrite H0. rewrite N.compare_refl.
+ rewrite map2_or_assoc; reflexivity.
+ now rewrite <- Nat2N.inj_iff, H0.
+ now rewrite <- Nat2N.inj_iff, H1.
+Qed.
+
+Lemma bv_or_empty_empty1: forall a, (bv_or a bv_empty) = bv_empty.
+Proof. intros a. unfold bv_empty.
+ unfold bv_or, bits, size. simpl.
+ case_eq (N.compare (N.of_nat (length a)) 0); intro H; simpl.
+ - apply (N.compare_eq (N.of_nat (length a)) 0) in H.
+ rewrite H. simpl. rewrite map2_or_empty_empty1; reflexivity.
+ - rewrite N.eqb_compare. rewrite H; reflexivity.
+ - rewrite N.eqb_compare. rewrite H; reflexivity.
+Qed.
+
+Lemma bv_or_nth_bitOf: forall a b n (i: nat),
+ (size a) = n -> (size b) = n ->
+ (i <= (nat_of_N (size a)))%nat ->
+ nth i (bits (bv_or a b)) false = (nth i (bits a) false) || (nth i (bits b) false).
+Proof. intros a b n i H0 H1 H2.
+ unfold bv_or. rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl.
+ apply map2_or_nth_bitOf; unfold size in *; unfold bits.
+ now rewrite <- Nat2N.inj_iff, H1. rewrite Nat2N.id in H2; exact H2.
+Qed.
+
+Lemma bv_or_0_neutral: forall a, (bv_or a (mk_list_false (length (bits a)))) = a.
+Proof. intro a. unfold bv_or.
+ rewrite N.eqb_compare. unfold size, bits. rewrite length_mk_list_false.
+ rewrite N.compare_refl.
+ rewrite map2_or_0_neutral. reflexivity.
+Qed.
+
+Lemma bv_or_1_true: forall a, (bv_or a (mk_list_true (length (bits a)))) = (mk_list_true (length (bits a))).
+Proof. intro a. unfold bv_or.
+ rewrite N.eqb_compare. unfold size, bits. rewrite length_mk_list_true.
+ rewrite N.compare_refl.
+ rewrite map2_or_1_true. reflexivity.
+Qed.
+
+(* lists bitwise XOR properties *)
+
+Lemma map2_xor_comm: forall (a b: list bool), (map2 xorb a b) = (map2 xorb b a).
+Proof. intros a. induction a as [ | a' xs IHxs].
+ intros [ | b' ys].
+ - simpl. auto.
+ - simpl. auto.
+ - intros [ | b' ys].
+ + simpl. auto.
+ + intros. simpl.
+ cut (xorb a' b' = xorb b' a'). intro H. rewrite <- H. apply f_equal.
+ apply IHxs. apply xorb_comm.
+Qed.
+
+Lemma map2_xor_assoc: forall (a b c: list bool), (map2 xorb a (map2 xorb b c)) = (map2 xorb (map2 xorb a b) c).
+Proof. intro a. induction a as [ | a' xs IHxs].
+ simpl. auto.
+ intros [ | b' ys].
+ - simpl. auto.
+ - intros [ | c' zs].
+ + simpl. auto.
+ + simpl. cut (xorb a' (xorb b' c') = (xorb (xorb a' b') c')). intro H. rewrite <- H. apply f_equal.
+ apply IHxs. rewrite xorb_assoc_reverse. reflexivity.
+Qed.
+
+Lemma map2_xor_length: forall (a b: list bool), length a = length b -> length a = length (map2 xorb a b).
+Proof. induction a as [ | a' xs IHxs].
+ simpl. auto.
+ intros [ | b ys].
+ - simpl. intros. exact H.
+ - intros. simpl in *. apply f_equal. apply IHxs.
+ inversion H; auto.
+Qed.
+
+Lemma map2_xor_empty_empty1: forall (a: list bool), (map2 xorb a []) = [].
+Proof. intros a. induction a as [ | a' xs IHxs]; simpl; auto. Qed.
+
+Lemma map2_xor_empty_empty2: forall (a: list bool), (map2 xorb [] a) = [].
+Proof. intros a. rewrite map2_xor_comm. apply map2_xor_empty_empty1. Qed.
+
+Lemma map2_xor_nth_bitOf: forall (a b: list bool) (i: nat),
+ (length a) = (length b) ->
+ (i <= (length a))%nat ->
+ nth i (map2 xorb a b) false = xorb (nth i a false) (nth i b false).
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ - intros [ | b ys].
+ + intros i H0 H1. do 2 rewrite map2_nth_empty_false. reflexivity.
+ + intros i H0 H1. rewrite map2_xor_empty_empty2.
+ rewrite map2_nth_empty_false. contradict H1. simpl. unfold not. intros. easy.
+ - intros [ | b ys].
+ + intros i H0 H1. rewrite map2_xor_empty_empty1.
+ rewrite map2_nth_empty_false. rewrite xorb_false_r. rewrite H0 in H1.
+ contradict H1. simpl. unfold not. intros. easy.
+ + intros i H0 H1. simpl.
+ revert i H1. intros [ | i]; [ |intros IHi].
+ * simpl. auto.
+ * apply IHxs.
+ inversion H0; reflexivity.
+ inversion IHi; lia.
+Qed.
+
+Lemma map2_xor_0_neutral: forall (a: list bool), (map2 xorb a (mk_list_false (length a))) = a.
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ + auto.
+ + simpl. rewrite IHxs.
+ rewrite xorb_false_r. reflexivity.
+Qed.
+
+Lemma map2_xor_1_true: forall (a: list bool), (map2 xorb a (mk_list_true (length a))) = map negb a.
+Proof. intro a. induction a as [ | a' xs IHxs].
+ - simpl. reflexivity.
+ - simpl. rewrite IHxs. rewrite <- IHxs.
+ rewrite xorb_true_r; reflexivity.
+Qed.
+
+(*bitvector OR properties*)
+
+Lemma bv_xor_size n a b : size a = n -> size b = n -> size (bv_xor a b) = n.
+Proof.
+ unfold bv_xor. intros H1 H2. rewrite H1, H2.
+ rewrite N.eqb_compare. rewrite N.compare_refl.
+ unfold size in *. rewrite <- map2_xor_length.
+ - exact H1.
+ - unfold bits. now rewrite <- Nat2N.inj_iff, H1.
+Qed.
+
+Lemma bv_xor_comm: forall n a b, (size a) = n -> (size b) = n -> bv_xor a b = bv_xor b a.
+Proof. intros n a b H0 H1. unfold bv_xor.
+ rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl.
+ rewrite map2_xor_comm. reflexivity.
+Qed.
+
+Lemma bv_xor_assoc: forall n a b c, (size a) = n -> (size b) = n -> (size c) = n ->
+ (bv_xor a (bv_xor b c)) = (bv_xor (bv_xor a b) c).
+Proof. intros n a b c H0 H1 H2.
+ unfold bv_xor. rewrite H1, H2.
+ rewrite N.eqb_compare. rewrite N.eqb_compare. rewrite N.compare_refl.
+ unfold size, bits in *. rewrite <- (@map2_xor_length b c).
+ rewrite H0, H1.
+ rewrite N.compare_refl.
+ rewrite N.eqb_compare. rewrite N.eqb_compare.
+ rewrite N.compare_refl. rewrite <- (@map2_xor_length a b).
+ rewrite H0. rewrite N.compare_refl.
+ rewrite map2_xor_assoc; reflexivity.
+ now rewrite <- Nat2N.inj_iff, H0.
+ now rewrite <- Nat2N.inj_iff, H1.
+Qed.
+
+Lemma bv_xor_empty_empty1: forall a, (bv_xor a bv_empty) = bv_empty.
+Proof. intros a. unfold bv_empty.
+ unfold bv_xor, bits, size. simpl.
+ case_eq (N.compare (N.of_nat (length a)) 0); intro H; simpl.
+ - apply (N.compare_eq (N.of_nat (length a)) 0) in H.
+ rewrite H. simpl. rewrite map2_xor_empty_empty1; reflexivity.
+ - rewrite N.eqb_compare. rewrite H; reflexivity.
+ - rewrite N.eqb_compare. rewrite H; reflexivity.
+Qed.
+
+Lemma bv_xor_nth_bitOf: forall a b n (i: nat),
+ (size a) = n -> (size b) = n ->
+ (i <= (nat_of_N (size a)))%nat ->
+ nth i (bits (bv_xor a b)) false = xorb (nth i (bits a) false) (nth i (bits b) false).
+Proof. intros a b n i H0 H1 H2.
+ unfold bv_xor. rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl.
+ apply map2_xor_nth_bitOf; unfold size in *; unfold bits.
+ now rewrite <- Nat2N.inj_iff, H1. rewrite Nat2N.id in H2; exact H2.
+Qed.
+
+Lemma bv_xor_0_neutral: forall a, (bv_xor a (mk_list_false (length (bits a)))) = a.
+Proof. intro a. unfold bv_xor.
+ rewrite N.eqb_compare. unfold size, bits. rewrite length_mk_list_false.
+ rewrite N.compare_refl.
+ rewrite map2_xor_0_neutral. reflexivity.
+Qed.
+
+Lemma bv_xor_1_true: forall a, (bv_xor a (mk_list_true (length (bits a)))) = map negb a.
+Proof. intro a. unfold bv_xor.
+ rewrite N.eqb_compare. unfold size, bits. rewrite length_mk_list_true.
+ rewrite N.compare_refl.
+ rewrite map2_xor_1_true. reflexivity.
+Qed.
+
+(*bitwise NOT properties*)
+
+Lemma not_list_length: forall a, length a = length (map negb a).
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ - auto.
+ - simpl. apply f_equal. exact IHxs.
+Qed.
+
+Lemma not_list_involutative: forall a, map negb (map negb a) = a.
+Proof. intro a.
+ induction a as [ | a xs IHxs]; auto.
+ simpl. rewrite negb_involutive. apply f_equal. exact IHxs.
+Qed.
+
+Lemma not_list_false_true: forall n, map negb (mk_list_false n) = mk_list_true n.
+Proof. intro n.
+ induction n as [ | n IHn].
+ - auto.
+ - simpl. apply f_equal. exact IHn.
+Qed.
+
+Lemma not_list_true_false: forall n, map negb (mk_list_true n) = mk_list_false n.
+Proof. intro n.
+ induction n as [ | n IHn].
+ - auto.
+ - simpl. apply f_equal. exact IHn.
+Qed.
+
+Lemma not_list_and_or: forall a b, map negb (map2 andb a b) = map2 orb (map negb a) (map negb b).
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ - auto.
+ - intros [ | b ys].
+ + auto.
+ + simpl. rewrite negb_andb. apply f_equal. apply IHxs.
+Qed.
+
+Lemma not_list_or_and: forall a b, map negb (map2 orb a b) = map2 andb (map negb a) (map negb b).
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ - auto.
+ - intros [ | b ys].
+ + auto.
+ + simpl. rewrite negb_orb. apply f_equal. apply IHxs.
+Qed.
+
+(*bitvector NOT properties*)
+
+Lemma bv_not_size: forall n a, (size a) = n -> size (bv_not a) = n.
+Proof. intros n a H. unfold bv_not.
+ unfold size, bits in *. rewrite <- not_list_length. exact H.
+Qed.
+
+Lemma bv_not_involutive: forall a, bv_not (bv_not a) = a.
+Proof. intro a. unfold bv_not.
+ unfold size, bits. rewrite not_list_involutative. reflexivity.
+Qed.
+
+Lemma bv_not_false_true: forall n, bv_not (mk_list_false n) = (mk_list_true n).
+Proof. intros n. unfold bv_not.
+ unfold size, bits. rewrite not_list_false_true. reflexivity.
+Qed.
+
+Lemma bv_not_true_false: forall n, bv_not (mk_list_true n) = (mk_list_false n).
+Proof. intros n. unfold bv_not.
+ unfold size, bits. rewrite not_list_true_false. reflexivity.
+Qed.
+
+Lemma bv_not_and_or: forall n a b, (size a) = n -> (size b) = n -> bv_not (bv_and a b) = bv_or (bv_not a) (bv_not b).
+Proof. intros n a b H0 H1. unfold bv_and in *.
+ rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl.
+ unfold bv_or, size, bits in *.
+ do 2 rewrite <- not_list_length. rewrite H0, H1.
+ rewrite N.eqb_compare. rewrite N.compare_refl.
+ unfold bv_not, size, bits in *.
+ rewrite not_list_and_or. reflexivity.
+Qed.
+
+Lemma bv_not_or_and: forall n a b, (size a) = n -> (size b) = n -> bv_not (bv_or a b) = bv_and (bv_not a) (bv_not b).
+Proof. intros n a b H0 H1. unfold bv_and, size, bits in *.
+ do 2 rewrite <- not_list_length.
+ rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl.
+ unfold bv_or, size, bits in *.
+ rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl.
+ unfold bv_not, size, bits in *.
+ rewrite not_list_or_and. reflexivity.
+Qed.
+
+(* list bitwise ADD properties*)
+
+Lemma add_carry_ff: forall a, add_carry a false false = (a, false).
+Proof. intros a.
+ case a; simpl; auto.
+Qed.
+
+Lemma add_carry_neg_f: forall a, add_carry a (negb a) false = (true, false).
+Proof. intros a.
+ case a; simpl; auto.
+Qed.
+
+Lemma add_carry_neg_f_r: forall a, add_carry (negb a) a false = (true, false).
+Proof. intros a.
+ case a; simpl; auto.
+Qed.
+
+Lemma add_carry_neg_t: forall a, add_carry a (negb a) true = (false, true).
+Proof. intros a.
+ case a; simpl; auto.
+Qed.
+
+Lemma add_carry_tt: forall a, add_carry a true true = (a, true).
+Proof. intro a. case a; auto. Qed.
+
+Lemma add_list_empty_l: forall (a: list bool), (add_list [] a) = [].
+Proof. intro a. induction a as [ | a xs IHxs].
+ - unfold add_list. simpl. reflexivity.
+ - apply IHxs.
+Qed.
+
+Lemma add_list_empty_r: forall (a: list bool), (add_list a []) = [].
+Proof. intro a. induction a as [ | a xs IHxs]; unfold add_list; simpl; reflexivity. Qed.
+
+Lemma add_list_ingr_l: forall (a: list bool) (c: bool), (add_list_ingr [] a c) = [].
+Proof. intro a. induction a as [ | a xs IHxs]; unfold add_list; simpl; reflexivity. Qed.
+
+Lemma add_list_ingr_r: forall (a: list bool) (c: bool), (add_list_ingr a [] c) = [].
+Proof. intro a. induction a as [ | a xs IHxs]; unfold add_list; simpl; reflexivity. Qed.
+
+Lemma add_list_carry_comm: forall (a b: list bool) (c: bool), add_list_ingr a b c = add_list_ingr b a c.
+Proof. intros a. induction a as [ | a' xs IHxs]; intros b c.
+ - simpl. rewrite add_list_ingr_r. reflexivity.
+ - case b as [ | b' ys].
+ + simpl. auto.
+ + simpl in *. cut (add_carry a' b' c = add_carry b' a' c).
+ * intro H. rewrite H. destruct (add_carry b' a' c) as (r, c0).
+ rewrite IHxs. reflexivity.
+ * case a', b', c; auto.
+Qed.
+
+Lemma add_list_comm: forall (a b: list bool), (add_list a b) = (add_list b a).
+Proof. intros a b. unfold add_list. apply (add_list_carry_comm a b false). Qed.
+
+Lemma add_list_carry_assoc: forall (a b c: list bool) (d1 d2 d3 d4: bool),
+ add_carry d1 d2 false = add_carry d3 d4 false ->
+ (add_list_ingr (add_list_ingr a b d1) c d2) = (add_list_ingr a (add_list_ingr b c d3) d4).
+Proof. intros a. induction a as [ | a' xs IHxs]; intros b c d1 d2 d3 d4.
+ - simpl. reflexivity.
+ - case b as [ | b' ys].
+ + simpl. auto.
+ + case c as [ | c' zs].
+ * simpl. rewrite add_list_ingr_r. auto.
+ * simpl.
+ case_eq (add_carry a' b' d1); intros r0 c0 Heq0. simpl.
+ case_eq (add_carry r0 c' d2); intros r1 c1 Heq1.
+ case_eq (add_carry b' c' d3); intros r3 c3 Heq3.
+ case_eq (add_carry a' r3 d4); intros r2 c2 Heq2.
+ intro H. rewrite (IHxs _ _ c0 c1 c3 c2);
+ revert Heq0 Heq1 Heq3 Heq2;
+ case a', b', c', d1, d2, d3, d4; simpl; do 4 (intros H'; inversion_clear H');
+ try reflexivity; simpl in H; discriminate.
+Qed.
+
+Lemma add_list_carry_length_eq: forall (a b: list bool) c, length a = length b -> length a = length (add_list_ingr a b c).
+Proof. induction a as [ | a' xs IHxs].
+ simpl. auto.
+ intros [ | b ys].
+ - simpl. intros. exact H.
+ - intros. simpl in *.
+ case_eq (add_carry a' b c); intros r c0 Heq. simpl. apply f_equal.
+ specialize (@IHxs ys). apply IHxs. inversion H; reflexivity.
+Qed.
+
+Lemma add_list_carry_length_ge: forall (a b: list bool) c, (length a >= length b)%nat -> length b = length (add_list_ingr a b c).
+Proof. induction a as [ | a' xs IHxs].
+ simpl. intros b H0 H1. lia.
+ intros [ | b ys].
+ - simpl. intros. auto.
+ - intros. simpl in *.
+ case_eq (add_carry a' b c); intros r c0 Heq. simpl. apply f_equal.
+ specialize (@IHxs ys). apply IHxs. lia.
+Qed.
+
+Lemma add_list_carry_length_le: forall (a b: list bool) c, (length b >= length a)%nat -> length a = length (add_list_ingr a b c).
+Proof. induction a as [ | a' xs IHxs].
+ simpl. intros b H0 H1. reflexivity.
+ intros [ | b ys].
+ - simpl. intros. contradict H. lia.
+ - intros. simpl in *.
+ case_eq (add_carry a' b c); intros r c0 Heq. simpl. apply f_equal.
+ specialize (@IHxs ys). apply IHxs. lia.
+Qed.
+
+Lemma bv_neg_size: forall n a, (size a) = n -> size (bv_neg a) = n.
+Proof. intros n a H. unfold bv_neg.
+ unfold size, bits in *. unfold twos_complement.
+ specialize (@add_list_carry_length_eq (map negb a) (mk_list_false (length a)) true).
+ intros. rewrite <- H0. now rewrite map_length.
+ rewrite map_length.
+ now rewrite length_mk_list_false.
+Qed.
+
+Lemma length_add_list_eq: forall (a b: list bool), length a = length b -> length a = length (add_list a b).
+Proof. intros a b H. unfold add_list. apply (@add_list_carry_length_eq a b false). exact H. Qed.
+
+Lemma length_add_list_ge: forall (a b: list bool), (length a >= length b)%nat -> length b = length (add_list a b).
+Proof. intros a b H. unfold add_list. apply (@add_list_carry_length_ge a b false). exact H. Qed.
+
+Lemma length_add_list_le: forall (a b: list bool), (length b >= length a)%nat -> length a = length (add_list a b).
+Proof. intros a b H. unfold add_list. apply (@add_list_carry_length_le a b false). exact H. Qed.
+
+Lemma add_list_assoc: forall (a b c: list bool), (add_list (add_list a b) c) = (add_list a (add_list b c)).
+Proof. intros a b c. unfold add_list.
+ apply (@add_list_carry_assoc a b c false false false false).
+ simpl; reflexivity.
+Qed.
+
+Lemma add_list_carry_empty_neutral_n_l: forall (a: list bool) n, (n >= (length a))%nat -> (add_list_ingr (mk_list_false n) a false) = a.
+Proof. intro a. induction a as [ | a' xs IHxs].
+ - intro n. rewrite add_list_ingr_r. reflexivity.
+ - intros [ | n].
+ + simpl. intro H. contradict H. easy.
+ + simpl. intro H.
+ case a'; apply f_equal; apply IHxs; lia.
+Qed.
+
+Lemma add_list_carry_empty_neutral_n_r: forall (a: list bool) n, (n >= (length a))%nat -> (add_list_ingr a (mk_list_false n) false) = a.
+Proof. intro a. induction a as [ | a' xs IHxs].
+ - intro n. rewrite add_list_ingr_l. reflexivity.
+ - intros [ | n].
+ + simpl. intro H. contradict H. easy.
+ + simpl. intro H.
+ case a'; apply f_equal; apply IHxs; lia.
+Qed.
+
+Lemma add_list_carry_empty_neutral_l: forall (a: list bool), (add_list_ingr (mk_list_false (length a)) a false) = a.
+Proof. intro a.
+ rewrite add_list_carry_empty_neutral_n_l; auto.
+Qed.
+
+Lemma add_list_carry_empty_neutral_r: forall (a: list bool), (add_list_ingr a (mk_list_false (length a)) false) = a.
+Proof. intro a.
+ rewrite add_list_carry_empty_neutral_n_r; auto.
+Qed.
+
+Lemma add_list_empty_neutral_n_l: forall (a: list bool) n, (n >= (length a))%nat -> (add_list (mk_list_false n) a) = a.
+Proof. intros a. unfold add_list.
+ apply (@add_list_carry_empty_neutral_n_l a).
+Qed.
+
+Lemma add_list_empty_neutral_n_r: forall (a: list bool) n, (n >= (length a))%nat -> (add_list a (mk_list_false n)) = a.
+Proof. intros a. unfold add_list.
+ apply (@add_list_carry_empty_neutral_n_r a).
+Qed.
+
+Lemma add_list_empty_neutral_r: forall (a: list bool), (add_list a (mk_list_false (length a))) = a.
+Proof. intros a. unfold add_list.
+ apply (@add_list_carry_empty_neutral_r a).
+Qed.
+
+Lemma add_list_empty_neutral_l: forall (a: list bool), (add_list (mk_list_false (length a)) a) = a.
+Proof. intros a. unfold add_list.
+ apply (@add_list_carry_empty_neutral_l a).
+Qed.
+
+Lemma add_list_carry_unit_t : forall a, add_list_ingr a (mk_list_true (length a)) true = a.
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ - simpl. reflexivity.
+ - simpl. case_eq (add_carry a true true). intros r0 c0 Heq0.
+ rewrite add_carry_tt in Heq0. inversion Heq0.
+ apply f_equal. exact IHxs.
+Qed.
+
+Lemma add_list_carry_twice: forall a c, add_list_ingr a a c = removelast (c :: a).
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ - intros c. simpl. reflexivity.
+ - intros [ | ].
+ + simpl. case a.
+ * simpl. rewrite IHxs.
+ case_eq xs. intro Heq0. simpl. reflexivity.
+ reflexivity.
+ * simpl. rewrite IHxs.
+ case_eq xs. intro Heq0. simpl. reflexivity.
+ reflexivity.
+ + simpl. case a.
+ * simpl. rewrite IHxs.
+ case_eq xs. intro Heq0. simpl. reflexivity.
+ reflexivity.
+ * simpl. rewrite IHxs.
+ case_eq xs. intro Heq0. simpl. reflexivity.
+ reflexivity.
+Qed.
+
+Lemma add_list_twice: forall a, add_list a a = removelast (false :: a).
+Proof. intro a.
+ unfold add_list. rewrite add_list_carry_twice. reflexivity.
+Qed.
+
+(*bitvector ADD properties*)
+
+Lemma bv_add_size: forall n a b, (size a) = n -> (@size b) = n -> size (bv_add a b) = n.
+Proof. intros n a b H0 H1.
+ unfold bv_add. rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl.
+ unfold size, bits in *. rewrite <- (@length_add_list_eq a b). auto.
+ now rewrite <- Nat2N.inj_iff, H0.
+Qed.
+
+Lemma bv_add_comm: forall n a b, (size a) = n -> (size b) = n -> bv_add a b = bv_add b a.
+Proof. intros n a b H0 H1.
+ unfold bv_add, size, bits in *. rewrite H0, H1.
+ rewrite N.eqb_compare. rewrite N.compare_refl.
+ rewrite add_list_comm. reflexivity.
+Qed.
+
+Lemma bv_add_assoc: forall n a b c, (size a) = n -> (size b) = n -> (size c) = n ->
+ (bv_add a (bv_add b c)) = (bv_add (bv_add a b) c).
+Proof. intros n a b c H0 H1 H2.
+ unfold bv_add, size, bits in *. rewrite H1, H2.
+ rewrite N.eqb_compare. rewrite N.eqb_compare. rewrite N.compare_refl.
+ rewrite <- (@length_add_list_eq b c). rewrite H0, H1.
+ rewrite N.compare_refl. rewrite N.eqb_compare.
+ rewrite N.eqb_compare. rewrite N.compare_refl.
+ rewrite <- (@length_add_list_eq a b). rewrite H0.
+ rewrite N.compare_refl.
+ rewrite add_list_assoc. reflexivity.
+ now rewrite <- Nat2N.inj_iff, H0.
+ now rewrite <- Nat2N.inj_iff, H1.
+Qed.
+
+Lemma bv_add_empty_neutral_l: forall a, (bv_add (mk_list_false (length (bits a))) a) = a.
+Proof. intro a. unfold bv_add, size, bits.
+ rewrite N.eqb_compare. rewrite length_mk_list_false. rewrite N.compare_refl.
+ rewrite add_list_empty_neutral_l. reflexivity.
+Qed.
+
+Lemma bv_add_empty_neutral_r: forall a, (bv_add a (mk_list_false (length (bits a)))) = a.
+Proof. intro a. unfold bv_add, size, bits.
+ rewrite N.eqb_compare. rewrite length_mk_list_false. rewrite N.compare_refl.
+ rewrite add_list_empty_neutral_r. reflexivity.
+Qed.
+
+Lemma bv_add_twice: forall a, bv_add a a = removelast (false :: a).
+Proof. intro a. unfold bv_add, size, bits.
+ rewrite N.eqb_compare. rewrite N.compare_refl.
+ rewrite add_list_twice. reflexivity.
+Qed.
+
+(* bitwise SUBST properties *)
+
+Lemma subst_list_empty_empty_l: forall a, (subst_list [] a) = [].
+Proof. intro a. unfold subst_list; auto. Qed.
+
+Lemma subst_list_empty_empty_r: forall a, (subst_list a []) = [].
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ - auto.
+ - unfold subst_list; auto.
+Qed.
+
+Lemma subst_list'_empty_empty_r: forall a, (subst_list' a []) = [].
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ - auto.
+ - unfold subst_list' in *. unfold twos_complement. simpl. reflexivity.
+Qed.
+
+Lemma subst_list_borrow_length: forall (a b: list bool) c, length a = length b -> length a = length (subst_list_borrow a b c).
+Proof. induction a as [ | a' xs IHxs].
+ simpl. auto.
+ intros [ | b ys].
+ - simpl. intros. exact H.
+ - intros. simpl in *.
+ case_eq (subst_borrow a' b c); intros r c0 Heq. simpl. apply f_equal.
+ specialize (@IHxs ys). apply IHxs. inversion H; reflexivity.
+Qed.
+
+Lemma length_twos_complement: forall (a: list bool), length a = length (twos_complement a).
+Proof. intro a.
+ induction a as [ | a' xs IHxs].
+ - auto.
+ - unfold twos_complement. specialize (@add_list_carry_length_eq (map negb (a' :: xs)) (mk_list_false (length (a' :: xs))) true).
+ intro H. rewrite <- H. simpl. apply f_equal. rewrite <- not_list_length. reflexivity.
+ rewrite length_mk_list_false. rewrite <- not_list_length. reflexivity.
+Qed.
+
+Lemma subst_list_length: forall (a b: list bool), length a = length b -> length a = length (subst_list a b).
+Proof. intros a b H. unfold subst_list. apply (@subst_list_borrow_length a b false). exact H. Qed.
+
+Lemma subst_list'_length: forall (a b: list bool), length a = length b -> length a = length (subst_list' a b).
+Proof. intros a b H. unfold subst_list'.
+ rewrite <- (@length_add_list_eq a (twos_complement b)).
+ - reflexivity.
+ - rewrite <- (@length_twos_complement b). exact H.
+Qed.
+
+Lemma subst_list_borrow_empty_neutral: forall (a: list bool), (subst_list_borrow a (mk_list_false (length a)) false) = a.
+Proof. intro a. induction a as [ | a' xs IHxs].
+ - simpl. reflexivity.
+ - simpl.
+ cut(subst_borrow a' false false = (a', false)).
+ + intro H. rewrite H. rewrite IHxs. reflexivity.
+ + unfold subst_borrow. case a'; auto.
+Qed.
+
+Lemma subst_list_empty_neutral: forall (a: list bool), (subst_list a (mk_list_false (length a))) = a.
+Proof. intros a. unfold subst_list.
+ apply (@subst_list_borrow_empty_neutral a).
+Qed.
+
+Lemma twos_complement_cons_false: forall a, false :: twos_complement a = twos_complement (false :: a).
+Proof. intro a.
+ induction a as [ | a xs IHxs]; unfold twos_complement; simpl; reflexivity.
+Qed.
+
+Lemma twos_complement_false_false: forall n, twos_complement (mk_list_false n) = mk_list_false n.
+Proof. intro n.
+ induction n as [ | n IHn].
+ - auto.
+ - simpl. rewrite <- twos_complement_cons_false.
+ apply f_equal. exact IHn.
+Qed.
+
+Lemma subst_list'_empty_neutral: forall (a: list bool), (subst_list' a (mk_list_false (length a))) = a.
+Proof. intros a. unfold subst_list'.
+ rewrite (@twos_complement_false_false (length a)).
+ rewrite add_list_empty_neutral_r. reflexivity.
+Qed.
+
+(* some list ult and slt properties *)
+
+Lemma ult_list_big_endian_trans : forall x y z,
+ ult_list_big_endian x y = true ->
+ ult_list_big_endian y z = true ->
+ ult_list_big_endian x z = true.
+Proof.
+ intros x. induction x.
+ simpl. easy.
+ intros y z.
+ case y.
+ simpl. case x; easy.
+ intros b l.
+ intros.
+ simpl in *. case x in *.
+ case z in *. simpl in H0. case l in *; easy.
+ case l in *.
+ rewrite andb_true_iff in H.
+ destruct H.
+ apply negb_true_iff in H. subst.
+ simpl. case z in *. easy.
+ rewrite !orb_true_iff, !andb_true_iff in H0.
+ destruct H0.
+ destruct H.
+ apply Bool.eqb_prop in H.
+ subst.
+ rewrite orb_true_iff. now right.
+ destruct H. easy.
+ rewrite !orb_true_iff, !andb_true_iff in H, H0.
+ destruct H.
+ simpl in H. easy.
+ destruct H.
+ apply negb_true_iff in H. subst.
+ simpl.
+ destruct H0.
+ destruct H.
+ apply Bool.eqb_prop in H.
+ subst.
+ case z; easy.
+ destruct H. easy.
+ case l in *.
+ rewrite !orb_true_iff, !andb_true_iff in H.
+ simpl in H. destruct H. destruct H. case x in H1; easy.
+ destruct H.
+ apply negb_true_iff in H. subst.
+ simpl in H0.
+ case z in *; try easy.
+ case z in *; simpl in H0; try easy.
+ case b in H0; simpl in H0; try easy.
+ case z in *; try easy.
+ rewrite !orb_true_iff, !andb_true_iff in *.
+ destruct H.
+ destruct H.
+ destruct H0.
+ destruct H0.
+ apply Bool.eqb_prop in H.
+ apply Bool.eqb_prop in H0.
+ subst.
+ left.
+ split.
+ apply Bool.eqb_reflx.
+ now apply (IHx (b1 :: l) z H1 H2).
+ right. apply Bool.eqb_prop in H. now subst.
+ right. destruct H0, H0.
+ apply Bool.eqb_prop in H0. now subst.
+ split; easy.
+Qed.
+
+
+Lemma ult_list_trans : forall x y z,
+ ult_list x y = true -> ult_list y z = true -> ult_list x z = true.
+Proof. unfold ult_list. intros x y z. apply ult_list_big_endian_trans.
+Qed.
+
+Lemma ult_list_big_endian_not_eq : forall x y,
+ ult_list_big_endian x y = true -> x <> y.
+Proof.
+ intros x. induction x.
+ simpl. easy.
+ intros y.
+ case y.
+ simpl. case x; easy.
+ intros b l.
+ simpl.
+ specialize (IHx l).
+ case x in *.
+ simpl.
+ case l in *. case a; case b; simpl; easy.
+ easy.
+ rewrite !orb_true_iff, !andb_true_iff.
+ intro.
+ destruct H.
+ destruct H.
+ apply IHx in H0.
+ apply Bool.eqb_prop in H.
+ rewrite H in *.
+ unfold not in *; intro.
+ inversion H1; subst. now apply H0.
+ destruct H.
+ apply negb_true_iff in H. subst. easy.
+Qed.
+
+Lemma ult_list_not_eq : forall x y, ult_list x y = true -> x <> y.
+Proof. unfold ult_list.
+ unfold not. intros.
+ apply ult_list_big_endian_not_eq in H.
+ subst. auto.
+Qed.
+
+Lemma slt_list_big_endian_not_eq : forall x y,
+ slt_list_big_endian x y = true -> x <> y.
+Proof.
+ intros x. induction x.
+ simpl. easy.
+ intros y.
+ case y.
+ simpl. case x; easy.
+ intros b l.
+ simpl.
+ specialize (IHx l).
+ case x in *.
+ simpl.
+ case l in *. case a; case b; simpl; easy.
+ easy.
+ rewrite !orb_true_iff, !andb_true_iff.
+ intro.
+ destruct H.
+ destruct H.
+ apply ult_list_big_endian_not_eq in H0.
+ apply Bool.eqb_prop in H. rewrite H in *.
+ unfold not in *. intros. apply H0. now inversion H1.
+ destruct H.
+ apply negb_true_iff in H0. subst. easy.
+Qed.
+
+Lemma slt_list_not_eq : forall x y, slt_list x y = true -> x <> y.
+Proof. unfold slt_list.
+ unfold not. intros.
+ apply slt_list_big_endian_not_eq in H.
+ subst. auto.
+Qed.
+
+
+Lemma ult_list_not_eqP : forall x y, ult_listP x y -> x <> y.
+Proof. unfold ult_listP.
+ unfold not. intros. unfold ult_list in H.
+ case_eq (ult_list_big_endian (List.rev x) (List.rev y)); intros.
+ apply ult_list_big_endian_not_eq in H1. subst. now contradict H1.
+ now rewrite H1 in H.
+Qed.
+
+Lemma slt_list_not_eqP : forall x y, slt_listP x y -> x <> y.
+Proof. unfold slt_listP.
+ unfold not. intros. unfold slt_list in H.
+ case_eq (slt_list_big_endian (List.rev x) (List.rev y)); intros.
+ apply slt_list_big_endian_not_eq in H1. subst. now contradict H1.
+ now rewrite H1 in H.
+Qed.
+
+Lemma bv_ult_B2P: forall x y, bv_ult x y = true <-> bv_ultP x y.
+Proof. intros. split; intros; unfold bv_ult, bv_ultP in *.
+ case_eq (size x =? size y); intros;
+ rewrite H0 in H; unfold ult_listP. now rewrite H.
+ now contradict H.
+ unfold ult_listP in *.
+ case_eq (size x =? size y); intros.
+ rewrite H0 in H.
+ case_eq (ult_list x y); intros. easy.
+ rewrite H1 in H. now contradict H.
+ rewrite H0 in H. now contradict H.
+Qed.
+
+Lemma bv_slt_B2P: forall x y, bv_slt x y = true <-> bv_sltP x y.
+Proof. intros. split; intros; unfold bv_slt, bv_sltP in *.
+ case_eq (size x =? size y); intros;
+ rewrite H0 in H; unfold slt_listP. now rewrite H.
+ now contradict H.
+ unfold slt_listP in *.
+ case_eq (size x =? size y); intros.
+ rewrite H0 in H.
+ case_eq (slt_list x y); intros. easy.
+ rewrite H1 in H. now contradict H.
+ rewrite H0 in H. now contradict H.
+Qed.
+
+Lemma nlt_be_neq_gt: forall x y,
+ length x = length y -> ult_list_big_endian x y = false ->
+ beq_list x y = false -> ult_list_big_endian y x = true.
+Proof. intro x.
+ induction x as [ | x xs IHxs ].
+ - intros. simpl in *. case y in *; now contradict H.
+ - intros.
+ simpl in H1.
+
+ case_eq y; intros.
+ rewrite H2 in H. now contradict H.
+ simpl.
+ case_eq l. intros. case_eq xs. intros.
+ rewrite H2 in H1.
+ rewrite H4 in H0, H. simpl in H0, H.
+ rewrite H2, H3 in H0, H.
+ rewrite H4, H3 in H1. simpl in H1. rewrite andb_true_r in H1.
+ case b in *; case x in *; easy.
+ intros.
+ rewrite H4, H2, H3 in H. now contradict H.
+ intros.
+ rewrite H2, H3 in H0, H1.
+
+ simpl in H0.
+ case_eq xs. intros. rewrite H4, H2, H3 in H. now contradict H.
+ intros. rewrite H4 in H0.
+ rewrite <- H3, <- H4.
+ rewrite <- H3, <- H4 in H0.
+ rewrite <- H3 in H1.
+ rewrite orb_false_iff in H0.
+ destruct H0.
+
+ case_eq (Bool.eqb x b); intros.
+ rewrite H6 in H0, H1.
+ rewrite andb_true_l in H0, H1.
+ assert (Bool.eqb b x = true).
+ { case b in *; case x in *; easy. }
+ rewrite H7. rewrite andb_true_l.
+ rewrite orb_true_iff.
+ left.
+ apply IHxs. rewrite H2 in H.
+ now inversion H.
+ easy. easy.
+ assert (Bool.eqb b x = false).
+ { case b in *; case x in *; easy. }
+ rewrite H7. rewrite orb_false_l.
+ case x in *. case b in *.
+ now contradict H6.
+ now easy.
+ case b in *.
+ now contradict H5.
+ now contradict H6.
+Qed.
+
+(** bitvector ult/slt *)
+
+Lemma bv_ult_not_eqP : forall x y, bv_ultP x y -> x <> y.
+Proof. intros x y. unfold bv_ultP.
+ case_eq (size x =? size y); intros.
+ - now apply ult_list_not_eqP in H0.
+ - now contradict H0.
+Qed.
+
+Lemma bv_slt_not_eqP : forall x y, bv_sltP x y -> x <> y.
+Proof. intros x y. unfold bv_sltP.
+ case_eq (size x =? size y); intros.
+ - now apply slt_list_not_eqP in H0.
+ - now contradict H0.
+Qed.
+
+Lemma bv_ult_not_eq : forall x y, bv_ult x y = true -> x <> y.
+Proof. intros x y. unfold bv_ult.
+ case_eq (size x =? size y); intros.
+ - now apply ult_list_not_eq in H0.
+ - now contradict H0.
+Qed.
+
+Lemma bv_slt_not_eq : forall x y, bv_slt x y = true -> x <> y.
+Proof. intros x y. unfold bv_slt.
+ case_eq (size x =? size y); intros.
+ - now apply slt_list_not_eq in H0.
+ - now contradict H0.
+Qed.
+
+Lemma rev_eq: forall x y, beq_list x y = true ->
+ beq_list (List.rev x) (List.rev y) = true.
+Proof. intros.
+ apply List_eq in H.
+ rewrite H.
+ now apply List_eq_refl.
+Qed.
+
+Lemma rev_neq: forall x y, beq_list x y = false ->
+ beq_list (List.rev x) (List.rev y) = false.
+Proof. intros.
+ specialize (@List_neq x y H).
+ intros.
+ apply not_true_is_false.
+ unfold not in *.
+ intros. apply H0.
+ apply List_eq in H1.
+
+ specialize (f_equal (@List.rev bool) H1 ).
+ intros.
+ now rewrite !rev_involutive in H2.
+Qed.
+
+Lemma nlt_neq_gt: forall x y,
+ length x = length y -> ult_list x y = false ->
+ beq_list x y = false -> ult_list y x = true.
+Proof. intros.
+ unfold ult_list in *.
+ apply nlt_be_neq_gt.
+ now rewrite !rev_length.
+ easy.
+ now apply rev_neq in H1.
+Qed.
+
+(* bitvector SUBT properties *)
+
+Lemma bv_subt_size: forall n a b, size a = n -> size b = n -> size (bv_subt a b) = n.
+Proof. intros n a b H0 H1.
+ unfold bv_subt, size, bits in *. rewrite H0, H1. rewrite N.eqb_compare.
+ rewrite N.compare_refl. rewrite <- subst_list_length. exact H0.
+ now rewrite <- Nat2N.inj_iff, H0.
+Qed.
+
+Lemma bv_subt_empty_neutral_r: forall a, (bv_subt a (mk_list_false (length (bits a)))) = a.
+Proof. intro a. unfold bv_subt, size, bits.
+ rewrite N.eqb_compare. rewrite length_mk_list_false.
+ rewrite N.compare_refl.
+ rewrite subst_list_empty_neutral. reflexivity.
+Qed.
+
+Lemma bv_subt'_size: forall n a b, (size a) = n -> (size b) = n -> size (bv_subt' a b) = n.
+Proof. intros n a b H0 H1. unfold bv_subt', size, bits in *.
+ rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl.
+ rewrite <- subst_list'_length. exact H0.
+ now rewrite <- Nat2N.inj_iff, H0.
+Qed.
+
+Lemma bv_subt'_empty_neutral_r: forall a, (bv_subt' a (mk_list_false (length (bits a)))) = a.
+Proof. intro a. unfold bv_subt', size, bits.
+ rewrite N.eqb_compare. rewrite length_mk_list_false.
+ rewrite N.compare_refl.
+ rewrite subst_list'_empty_neutral. reflexivity.
+Qed.
+
+(* bitwise ADD-NEG properties *)
+
+Lemma add_neg_list_carry_false: forall a b c, add_list_ingr a (add_list_ingr b c true) false = add_list_ingr a (add_list_ingr b c false) true.
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ - simpl. auto.
+ - case b as [ | b ys].
+ + simpl. auto.
+ + case c as [ | c zs].
+ * simpl. auto.
+ * simpl.
+ case_eq (add_carry b c false); intros r0 c0 Heq0.
+ case_eq (add_carry b c true); intros r1 c1 Heq1.
+ case_eq (add_carry a r1 false); intros r2 c2 Heq2.
+ case_eq (add_carry a r0 true); intros r3 c3 Heq3.
+ case a, b, c; inversion Heq0; inversion Heq1;
+ inversion Heq2; inversion Heq3; rewrite <- H2 in H4;
+ rewrite <- H0 in H5; inversion H4; inversion H5; apply f_equal;
+ try reflexivity; rewrite IHxs; reflexivity.
+Qed.
+
+
+Lemma add_neg_list_carry_neg_f: forall a, (add_list_ingr a (map negb a) false) = mk_list_true (length a).
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ - simpl. reflexivity.
+ - simpl.
+ case_eq (add_carry a (negb a) false); intros r0 c0 Heq0.
+ rewrite add_carry_neg_f in Heq0.
+ inversion Heq0. rewrite IHxs. reflexivity.
+Qed.
+
+Lemma add_neg_list_carry_neg_f_r: forall a, (add_list_ingr (map negb a) a false) = mk_list_true (length a).
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ - simpl. reflexivity.
+ - simpl.
+ case_eq (add_carry (negb a) a false); intros r0 c0 Heq0.
+ rewrite add_carry_neg_f_r in Heq0.
+ inversion Heq0. rewrite IHxs. reflexivity.
+Qed.
+
+Lemma add_neg_list_carry_neg_t: forall a, (add_list_ingr a (map negb a) true) = mk_list_false (length a).
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ - simpl. reflexivity.
+ - simpl.
+ case_eq (add_carry a (negb a) true); intros r0 c0 Heq0.
+ rewrite add_carry_neg_t in Heq0.
+ inversion Heq0. rewrite IHxs. reflexivity.
+Qed.
+
+Lemma add_neg_list_carry: forall a, add_list_ingr a (twos_complement a) false = mk_list_false (length a).
+Proof. intro a.
+ induction a as [ | a xs IHxs].
+ - simpl. reflexivity.
+ - unfold twos_complement. rewrite add_neg_list_carry_false. rewrite not_list_length at 1.
+ rewrite add_list_carry_empty_neutral_r.
+ rewrite add_neg_list_carry_neg_t. reflexivity.
+Qed.
+
+Lemma add_neg_list_absorb: forall a, add_list a (twos_complement a) = mk_list_false (length a).
+Proof. intro a. unfold add_list. rewrite add_neg_list_carry. reflexivity. Qed.
+
+(* bitvector ADD-NEG properties *)
+
+Lemma bv_add_neg_unit: forall a, bv_add a (bv_not a) = mk_list_true (nat_of_N (size a)).
+Proof. intro a. unfold bv_add, bv_not, size, bits. rewrite not_list_length.
+ rewrite N.eqb_compare. rewrite N.compare_refl.
+ unfold add_list. rewrite add_neg_list_carry_neg_f.
+ rewrite Nat2N.id, not_list_length. reflexivity.
+Qed.
+
+
+(* bitwise ADD-SUBST properties *)
+
+Lemma add_subst_list_carry_opp: forall n a b, (length a) = n -> (length b) = n -> (add_list_ingr (subst_list' a b) b false) = a.
+Proof. intros n a b H0 H1.
+ unfold subst_list', twos_complement, add_list.
+ rewrite add_neg_list_carry_false. rewrite not_list_length at 1.
+ rewrite add_list_carry_empty_neutral_r.
+ specialize (@add_list_carry_assoc a (map negb b) b true false false true).
+ intro H2. rewrite H2; try auto. rewrite add_neg_list_carry_neg_f_r.
+ rewrite H1. rewrite <- H0. rewrite add_list_carry_unit_t; reflexivity.
+Qed.
+
+Lemma add_subst_opp: forall n a b, (length a) = n -> (length b) = n -> (add_list (subst_list' a b) b) = a.
+Proof. intros n a b H0 H1. unfold add_list, size, bits.
+ apply (@add_subst_list_carry_opp n a b); easy.
+Qed.
+
+(* bitvector ADD-SUBT properties *)
+
+Lemma bv_add_subst_opp: forall n a b, (size a) = n -> (size b) = n -> (bv_add (bv_subt' a b) b) = a.
+Proof. intros n a b H0 H1. unfold bv_add, bv_subt', add_list, size, bits in *.
+ rewrite H0, H1.
+ rewrite N.eqb_compare. rewrite N.eqb_compare. rewrite N.compare_refl.
+ rewrite <- (@subst_list'_length a b). rewrite H0.
+ rewrite N.compare_refl. rewrite (@add_subst_list_carry_opp (nat_of_N n) a b); auto;
+ inversion H0; rewrite Nat2N.id; auto.
+ symmetry. now rewrite <- Nat2N.inj_iff, H0.
+ now rewrite <- Nat2N.inj_iff, H0.
+Qed.
+
+ (* bitvector MULT properties *)
+
+Lemma prop_mult_bool_step_k_h_len: forall a b c k,
+length (mult_bool_step_k_h a b c k) = length a.
+Proof. intro a.
+ induction a as [ | xa xsa IHa ].
+ - intros. simpl. easy.
+ - intros.
+ case b in *. simpl. rewrite IHa. simpl. omega.
+ simpl. case (k - 1 <? 0)%Z; simpl; now rewrite IHa.
+Qed.
+
+
+Lemma empty_list_length: forall {A: Type} (a: list A), (length a = 0)%nat <-> a = [].
+Proof. intros A a.
+ induction a; split; intros; auto; contradict H; easy.
+Qed.
+
+Lemma prop_mult_bool_step: forall k' a b res k,
+ length (mult_bool_step a b res k k') = (length res)%nat.
+Proof. intro k'.
+ induction k'.
+ - intros. simpl. rewrite prop_mult_bool_step_k_h_len. simpl. omega.
+ - intros. simpl. rewrite IHk'. rewrite prop_mult_bool_step_k_h_len. simpl; omega.
+Qed.
+
+Lemma and_with_bool_len: forall a b, length (and_with_bool a (nth 0 b false)) = length a.
+Proof. intro a.
+ - induction a.
+ intros. now simpl.
+ intros. simpl. now rewrite IHa.
+Qed.
+
+Lemma bv_mult_size: forall n a b, (size a) = n -> (@size b) = n -> size (bv_mult a b) = n.
+Proof. intros n a b H0 H1.
+ unfold bv_mult, size, bits in *.
+ rewrite H0, H1.
+ rewrite N.eqb_compare. rewrite N.compare_refl.
+ unfold mult_list, bvmult_bool.
+ case_eq (length a).
+ intros.
+ + rewrite empty_list_length in H. rewrite H in *. now simpl in *.
+ + intros.
+ case n0 in *. now rewrite and_with_bool_len.
+ rewrite prop_mult_bool_step. now rewrite and_with_bool_len.
+Qed.
+
+ (** list extraction *)
+ Fixpoint extract (x: list bool) (i j: nat) : list bool :=
+ match x with
+ | [] => []
+ | bx :: x' =>
+ match i with
+ | O =>
+ match j with
+ | O => []
+ | S j' => bx :: extract x' i j'
+ end
+ | S i' =>
+ match j with
+ | O => []
+ | S j' => extract x' i' j'
+ end
+ end
+ end.
+
+ Lemma zero_false: forall p, ~ 0 >= Npos p.
+ Proof. intro p. induction p; lia. Qed.
+
+ Lemma min_distr: forall i j: N, N.to_nat (j - i) = ((N.to_nat j) - (N.to_nat i))%nat.
+ Proof. intros i j; case i; case j in *; try intros; lia. Qed.
+
+ Lemma posSn: forall n, (Pos.to_nat (Pos.of_succ_nat n)) = S n.
+ Proof. intros; case n; [easy | intros; lia ]. Qed.
+
+ Lemma _length_extract: forall a (i j: N) (H0: (N.of_nat (length a)) >= j) (H1: j >= i),
+ length (extract a 0 (N.to_nat j)) = (N.to_nat j).
+ Proof. intro a.
+ induction a as [ | xa xsa IHa ].
+ - simpl. case i in *. case j in *.
+ easy. lia.
+ case j in *; lia.
+ - intros. simpl.
+ case_eq j. intros.
+ now simpl.
+ intros. rewrite <- H.
+ case_eq (N.to_nat j).
+ easy. intros. simpl.
+ apply f_equal.
+ specialize (@IHa 0%N (N.of_nat n)).
+ rewrite Nat2N.id in IHa.
+ apply IHa.
+ apply (f_equal (N.of_nat)) in H2.
+ rewrite N2Nat.id in H2.
+ rewrite H2 in H0. simpl in *. lia.
+ lia.
+ Qed.
+
+ Lemma length_extract: forall a (i j: N) (H0: (N.of_nat (length a)) >= j) (H1: j >= i),
+ length (extract a (N.to_nat i) (N.to_nat j)) = (N.to_nat (j - i)).
+ Proof. intro a.
+ induction a as [ | xa xsa IHa].
+ - intros. simpl.
+ case i in *. case j in *.
+ easy. simpl in *.
+ contradict H0. apply zero_false.
+ case j in *. now simpl.
+ apply zero_false in H0; now contradict H0.
+ - intros. simpl.
+ case_eq (N.to_nat i). intros.
+ case_eq (N.to_nat j). intros.
+ rewrite min_distr. now rewrite H, H2.
+ intros. simpl.
+ rewrite min_distr. rewrite H, H2.
+ simpl. apply f_equal.
+
+ specialize (@IHa 0%N (N.of_nat n)).
+ rewrite Nat2N.id in IHa.
+ simpl in *.
+ rewrite IHa. lia.
+ lia. lia.
+ intros.
+ case_eq (N.to_nat j).
+ simpl. intros.
+ rewrite min_distr. rewrite H, H2. now simpl.
+ intros.
+ rewrite min_distr. rewrite H, H2.
+ simpl.
+ specialize (@IHa (N.of_nat n) (N.of_nat n0)).
+ rewrite !Nat2N.id in IHa.
+ rewrite IHa. lia.
+ apply (f_equal (N.of_nat)) in H2.
+ rewrite N2Nat.id in H2.
+ rewrite H2 in H0. simpl in H0. lia.
+ lia.
+Qed.
+
+ (** bit-vector extraction *)
+ Definition bv_extr (i n0 n1: N) a : bitvector :=
+ if (N.ltb n1 (n0 + i)) then mk_list_false (nat_of_N n0)
+ else extract a (nat_of_N i) (nat_of_N (n0 + i)).
+
+ Lemma not_ltb: forall (n0 n1 i: N), (n1 <? n0 + i)%N = false -> n1 >= n0 + i.
+ Proof. intro n0.
+ induction n0.
+ intros. simpl in *.
+ apply N.ltb_nlt in H.
+ apply N.nlt_ge in H. lia.
+ intros. simpl.
+ case_eq i.
+ intros. subst. simpl in H.
+ apply N.ltb_nlt in H.
+ apply N.nlt_ge in H. intros. simpl in H. lia.
+ intros. subst.
+ apply N.ltb_nlt in H.
+ apply N.nlt_ge in H. lia.
+ Qed.
+
+
+ Lemma bv_extr_size: forall (i n0 n1 : N) a,
+ size a = n1 -> size (@bv_extr i n0 n1 a) = n0%N.
+ Proof.
+ intros. unfold bv_extr, size in *.
+ case_eq (n1 <? n0 + i).
+ intros. now rewrite length_mk_list_false, N2Nat.id.
+ intros.
+ specialize (@length_extract a i (n0 + i)). intros.
+ assert ((n0 + i - i) = n0)%N.
+ { lia. } rewrite H2 in H1.
+ rewrite H1.
+ now rewrite N2Nat.id.
+ rewrite H.
+ now apply not_ltb.
+ lia.
+ Qed.
+
+ (*
+ Definition bv_extr (n i j: N) {H0: n >= j} {H1: j >= i} {a: bitvector} : bitvector :=
+ extract a (nat_of_N i) (nat_of_N j).
+
+
+ Lemma bv_extr_size: forall n (i j: N) a (H0: n >= j) (H1: j >= i),
+ size a = n -> size (@bv_extr n i j H0 H1 a) = (j - i)%N.
+ Proof.
+ intros. unfold bv_extr, size in *.
+ rewrite <- N2Nat.id. apply f_equal.
+ rewrite <- H in H0.
+ specialize (@length_extract a i j H0 H1); intros; apply H2.
+ Qed.
+ *)
+
+ (** list extension *)
+ Fixpoint extend (x: list bool) (i: nat) (b: bool) {struct i}: list bool :=
+ match i with
+ | O => x
+ | S i' => b :: extend x i' b
+ end.
+
+ Definition zextend (x: list bool) (i: nat): list bool :=
+ extend x i false.
+
+ Definition sextend (x: list bool) (i: nat): list bool :=
+ match x with
+ | [] => mk_list_false i
+ | xb :: x' => extend x i xb
+ end.
+
+ Lemma extend_size_zero: forall i b, (length (extend [] i b)) = i.
+ Proof.
+ intros.
+ induction i as [ | xi IHi].
+ - now simpl.
+ - simpl. now rewrite IHi.
+ Qed.
+
+ Lemma extend_size_one: forall i a b, length (extend [a] i b) = S i.
+ Proof. intros.
+ induction i.
+ - now simpl.
+ - simpl. now rewrite IHi.
+ Qed.
+
+ Lemma length_extend: forall a i b, length (extend a i b) = ((length a) + i)%nat.
+ Proof. intro a.
+ induction a.
+ - intros. simpl. now rewrite extend_size_zero.
+ - intros.
+ induction i.
+ + intros. simpl. lia.
+ + intros. simpl. apply f_equal.
+ rewrite IHi. simpl. lia.
+ Qed.
+
+ Lemma zextend_size_zero: forall i, (length (zextend [] i)) = i.
+ Proof.
+ intros. unfold zextend. apply extend_size_zero.
+ Qed.
+
+ Lemma zextend_size_one: forall i a, length (zextend [a] i) = S i.
+ Proof.
+ intros. unfold zextend. apply extend_size_one.
+ Qed.
+
+ Lemma length_zextend: forall a i, length (zextend a i) = ((length a) + i)%nat.
+ Proof.
+ intros. unfold zextend. apply length_extend.
+ Qed.
+
+ Lemma sextend_size_zero: forall i, (length (sextend [] i)) = i.
+ Proof.
+ intros. unfold sextend. now rewrite length_mk_list_false.
+ Qed.
+
+ Lemma sextend_size_one: forall i a, length (sextend [a] i) = S i.
+ Proof.
+ intros. unfold sextend. apply extend_size_one.
+ Qed.
+
+ Lemma length_sextend: forall a i, length (sextend a i) = ((length a) + i)%nat.
+ Proof.
+ intros. unfold sextend.
+ case_eq a. intros. rewrite length_mk_list_false. easy.
+ intros. apply length_extend.
+ Qed.
+
+ (** bit-vector extension *)
+ Definition bv_zextn (n i: N) (a: bitvector): bitvector :=
+ zextend a (nat_of_N i).
+
+ Definition bv_sextn (n i: N) (a: bitvector): bitvector :=
+ sextend a (nat_of_N i).
+
+ Lemma plus_distr: forall i j: N, N.to_nat (j + i) = ((N.to_nat j) + (N.to_nat i))%nat.
+ Proof. intros i j; case i; case j in *; try intros; lia. Qed.
+
+ Lemma bv_zextn_size: forall n (i: N) a,
+ size a = n -> size (@bv_zextn n i a) = (i + n)%N.
+ Proof.
+ intros. unfold bv_zextn, zextend, size in *.
+ rewrite <- N2Nat.id. apply f_equal.
+ specialize (@length_extend a (nat_of_N i) false). intros.
+ rewrite H0. rewrite plus_distr. rewrite plus_comm.
+ apply f_equal.
+ apply (f_equal (N.to_nat)) in H.
+ now rewrite Nat2N.id in H.
+ Qed.
+
+ Lemma bv_sextn_size: forall n (i: N) a,
+ size a = n -> size (@bv_sextn n i a) = (i + n)%N.
+ Proof.
+ intros. unfold bv_sextn, sextend, size in *.
+ rewrite <- N2Nat.id. apply f_equal.
+ case_eq a.
+ intros. rewrite length_mk_list_false.
+ rewrite H0 in H. simpl in H. rewrite <- H.
+ lia.
+ intros.
+ specialize (@length_extend a (nat_of_N i) b). intros.
+ subst. rewrite plus_distr. rewrite plus_comm.
+ rewrite Nat2N.id.
+ now rewrite <- H1.
+ Qed.
+
+ (** shift left *)
+
+Fixpoint pow2 (n: nat): nat :=
+ match n with
+ | O => 1%nat
+ | S n' => (2 * pow2 n')%nat
+ end.
+
+Fixpoint _list2nat_be (a: list bool) (n i: nat) : nat :=
+ match a with
+ | [] => n
+ | xa :: xsa =>
+ if xa then _list2nat_be xsa (n + (pow2 i)) (i + 1)
+ else _list2nat_be xsa n (i + 1)
+ end.
+
+Definition list2nat_be (a: list bool) := _list2nat_be a 0 0.
+
+Definition _shl_be (a: list bool) : list bool :=
+ match a with
+ | [] => []
+ | _ => false :: removelast a
+ end.
+
+Fixpoint nshl_be (a: list bool) (n: nat): list bool :=
+ match n with
+ | O => a
+ | S n' => nshl_be (_shl_be a) n'
+ end.
+
+Definition shl_be (a b: list bool): list bool :=
+nshl_be a (list2nat_be b).
+
+Lemma length__shl_be: forall a, length (_shl_be a) = length a.
+Proof. intro a.
+ induction a; intros.
+ - now simpl.
+ - simpl. rewrite <- IHa.
+ case_eq a0; easy.
+Qed.
+
+Lemma length_nshl_be: forall n a, length (nshl_be a n) = length a.
+Proof. intro n.
+ induction n; intros; simpl.
+ - reflexivity.
+ - now rewrite (IHn (_shl_be a)), length__shl_be.
+Qed.
+
+Lemma length_shl_be: forall a b n, n = (length a) -> n = (length b)%nat ->
+ n = (length (shl_be a b)).
+Proof.
+ intros.
+ unfold shl_be. now rewrite length_nshl_be.
+Qed.
+
+ (** bit-vector extension *)
+Definition bv_shl (a b : bitvector) : bitvector :=
+ if ((@size a) =? (@size b))
+ then shl_be a b
+ else zeros (@size a).
+
+Lemma bv_shl_size n a b : size a = n -> size b = n -> size (bv_shl a b) = n.
+Proof.
+ unfold bv_shl. intros H1 H2. rewrite H1, H2.
+ rewrite N.eqb_compare. rewrite N.compare_refl.
+ unfold size in *. rewrite <- (@length_shl_be a b (nat_of_N n)).
+ now rewrite N2Nat.id.
+ now apply (f_equal (N.to_nat)) in H1; rewrite Nat2N.id in H1.
+ now apply (f_equal (N.to_nat)) in H2; rewrite Nat2N.id in H2.
+Qed.
+
+ (** shift right *)
+
+Definition _shr_be (a: list bool) : list bool :=
+ match a with
+ | [] => []
+ | xa :: xsa => xsa ++ [false]
+ end.
+
+Fixpoint nshr_be (a: list bool) (n: nat): list bool :=
+ match n with
+ | O => a
+ | S n' => nshr_be (_shr_be a) n'
+ end.
+
+Definition shr_be (a b: list bool): list bool :=
+nshr_be a (list2nat_be b).
+
+Lemma length__shr_be: forall a, length (_shr_be a) = length a.
+Proof. intro a.
+ induction a; intros.
+ - now simpl.
+ - simpl. rewrite <- IHa.
+ case_eq a0; easy.
+Qed.
+
+Lemma length_nshr_be: forall n a, length (nshr_be a n) = length a.
+Proof. intro n.
+ induction n; intros; simpl.
+ - reflexivity.
+ - now rewrite (IHn (_shr_be a)), length__shr_be.
+Qed.
+
+Lemma length_shr_be: forall a b n, n = (length a) -> n = (length b)%nat ->
+ n = (length (shr_be a b)).
+Proof.
+ intros.
+ unfold shr_be. now rewrite length_nshr_be.
+Qed.
+
+ (** bit-vector extension *)
+Definition bv_shr (a b : bitvector) : bitvector :=
+ if ((@size a) =? (@size b))
+ then shr_be a b
+ else zeros (@size a).
+
+Lemma bv_shr_size n a b : size a = n -> size b = n -> size (bv_shr a b) = n.
+Proof.
+ unfold bv_shr. intros H1 H2. rewrite H1, H2.
+ rewrite N.eqb_compare. rewrite N.compare_refl.
+ unfold size in *. rewrite <- (@length_shr_be a b (nat_of_N n)).
+ now rewrite N2Nat.id.
+ now apply (f_equal (N.to_nat)) in H1; rewrite Nat2N.id in H1.
+ now apply (f_equal (N.to_nat)) in H2; rewrite Nat2N.id in H2.
+Qed.
+
+End RAWBITVECTOR_LIST.
+
+Module BITVECTOR_LIST <: BITVECTOR.
+
+ Include RAW2BITVECTOR(RAWBITVECTOR_LIST).
+
+ Notation "x |0" := (cons false x) (left associativity, at level 73, format "x |0"): bv_scope.
+ Notation "x |1" := (cons true x) (left associativity, at level 73, format "x |1"): bv_scope.
+ Notation "'b|0'" := [false] (at level 70): bv_scope.
+ Notation "'b|1'" := [true] (at level 70): bv_scope.
+ Notation "# x |" := (@of_bits x) (no associativity, at level 1, format "# x |"): bv_scope.
+ Notation "v @ p" := (bitOf p v) (at level 1, format "v @ p ") : bv_scope.
+
+End BITVECTOR_LIST.
+
+(*
+ Local Variables:
+ coq-load-path: ((rec ".." "SMTCoq"))
+ End:
+*)
generated by cgit (git 2.34.1) at 2024-06-29 16:10:08 +0000