include "ASM/BitVector.ma".
include "ASM/Util.ma".

definition addr16_of_addr11: Word → Word11 → Word ≝
  λpc: Word.
  λa: Word11.
  let 〈pc_upper, ignore〉 ≝ vsplit … 8 8 pc in
  let 〈n1, n2〉 ≝ vsplit … 4 4 pc_upper in
  let 〈b123, b〉 ≝ vsplit … 3 8 a in
  let b1 ≝ get_index_v … b123 0 ? in
  let b2 ≝ get_index_v … b123 1 ? in
  let b3 ≝ get_index_v … b123 2 ? in
  let p5 ≝ get_index_v … n2 0 ? in
    (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
  //
qed.

definition nat_of_bool ≝
  λb: bool.
    match b with
      [ false ⇒ O
      | true ⇒ S O
      ].

definition carry_of : bool → bool → bool → bool ≝
λa,b,c. match a with [ false ⇒ b ∧ c | true ⇒ b ∨ c ].

definition add_with_carries : ∀n:nat. BitVector n → BitVector n → bool →
                                      BitVector n × (BitVector n) ≝
  λn,x,y,init_carry.
  fold_right2_i ???
   (λn,b,c,r.
     let 〈lower_bits, carries〉 ≝ r in
     let last_carry ≝ match carries with [ VEmpty ⇒ init_carry | VCons _ cy _ ⇒ cy ] in
      (* Next if-then-else just to avoid a quadratic blow-up of the whd of an application
         of add_with_carries *)
     if last_carry then
      let bit ≝ xorb (xorb b c) true in
      let carry ≝ carry_of b c true in
       〈bit:::lower_bits, carry:::carries〉
     else
      let bit ≝ xorb (xorb b c) false in
      let carry ≝ carry_of b c false in
       〈bit:::lower_bits, carry:::carries〉     
   )
   〈[[ ]], [[ ]]〉 n x y.

(* Essentially the only difference for subtraction. *)
definition borrow_of : bool → bool → bool → bool ≝
λa,b,c. match a with [ false ⇒ b ∨ c | true ⇒ b ∧ c ].

definition sub_with_borrows : ∀n:nat. BitVector n → BitVector n → bool →
                                      BitVector n × (BitVector n) ≝
  λn,x,y,init_borrow.
  fold_right2_i ???
   (λn,b,c,r.
     let 〈lower_bits, borrows〉 ≝ r in
     let last_borrow ≝ match borrows with [ VEmpty ⇒ init_borrow | VCons _ bw _ ⇒ bw ] in
     let bit ≝ xorb (xorb b c) last_borrow in
     let borrow ≝ borrow_of b c last_borrow in
       〈bit:::lower_bits, borrow:::borrows〉
   )
   〈[[ ]], [[ ]]〉 n x y.
    
definition add_n_with_carry:
      ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. n ≥ 5 →
      (BitVector n) × (BitVector 3) ≝
  λn: nat.
  λb: BitVector n.
  λc: BitVector n.
  λcarry: bool.
  λpf:n ≥ 5.
  
    let 〈result, carries〉 ≝ add_with_carries n b c carry in
    let cy_flag ≝ get_index_v ?? carries 0 ? in
    let ov_flag ≝ xorb cy_flag (get_index_v ?? carries 1 ?) in
    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
// @(transitive_le  … pf) /2/
qed.

definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. n ≥ 5 →
                                            (BitVector n) × (BitVector 3) ≝
  λn: nat.
  λb: BitVector n.
  λc: BitVector n.
  λcarry: bool.
  λpf:n ≥ 5.
  
    let 〈result, carries〉 ≝ sub_with_borrows n b c carry in
    let cy_flag ≝ get_index_v ?? carries 0 ? in
    let ov_flag ≝ xorb cy_flag (get_index_v ?? carries 1 ?) in
    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
// @(transitive_le  … pf) /2/
qed.

definition add_8_with_carry ≝
  λb, c: BitVector 8.
  λcarry: bool.
  add_n_with_carry 8 b c carry ?.
  @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *)
qed.

definition add_16_with_carry ≝
  λb, c: BitVector 16.
  λcarry: bool.
  add_n_with_carry 16 b c carry ?.
  @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S
  @le_S @le_S @le_n (* ugly: fix using tacticals *)
qed.

(* dpm: needed for assembly proof *)
definition sub_7_with_carry ≝
  λb, c: BitVector 7.
  λcarry: bool.
  sub_n_with_carry 7 b c carry ?.
  @le_S @le_S @le_n
qed.

definition sub_8_with_carry ≝
  λb, c: BitVector 8.
  λcarry: bool.
  sub_n_with_carry 8 b c carry ?.
  @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *)
qed.

definition sub_16_with_carry ≝
  λb, c: BitVector 16.
  λcarry: bool.
  sub_n_with_carry 16 b c carry ?.
  @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S
  @le_S @le_S @le_n (* ugly: fix using tacticals *)
qed.

definition increment ≝
  λn: nat.
  λb: BitVector n.
    \fst (add_with_carries n b (zero n) true).
        
definition decrement ≝
  λn: nat.
  λb: BitVector n.
    \fst (sub_with_borrows n b (zero n) true).

let rec bitvector_of_nat_aux (n,m:nat) (v:BitVector n) on m : BitVector n ≝
  match m with
  [ O ⇒ v
  | S m' ⇒ bitvector_of_nat_aux n m' (increment n v)
  ].

definition bitvector_of_nat : ∀n:nat. nat → BitVector n ≝
  λn,m. bitvector_of_nat_aux n m (zero n).

let rec nat_of_bitvector_aux (n,m:nat) (v:BitVector n) on v : nat ≝
match v with
[ VEmpty ⇒ m
| VCons n' hd tl ⇒ nat_of_bitvector_aux n' (if hd then 2*m +1 else 2*m) tl
].

definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝
  λn,v. nat_of_bitvector_aux n O v.

lemma bitvector_of_nat_ok:
  ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
 #n elim n -n
 [ #x #y #Hx #Hy #Heq <(le_n_O_to_eq ? (le_S_S_to_le ?? Hx)) <(le_n_O_to_eq ? (le_S_S_to_le ?? Hy)) @refl
 | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *) 
 ]
qed.

lemma bitvector_of_nat_abs:
  ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
 #n #x #y #Hx #Hy #Heq @notb_elim
 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/
 | #H / by I/
 ]
qed.

axiom bitvector_of_nat_exp_zero: ∀n.bitvector_of_nat n (2^n) = zero n.

axiom nat_of_bitvector_bitvector_of_nat_inverse:
  ∀n: nat.
  ∀b: nat.
    b < 2^n → nat_of_bitvector n (bitvector_of_nat n b) = b.

axiom bitvector_of_nat_inverse_nat_of_bitvector:
  ∀n: nat.
  ∀b: BitVector n.
    bitvector_of_nat n (nat_of_bitvector n b) = b.

axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n.

axiom eq_bitvector_of_nat_to_eq:
 ∀n,n1,n2.
  n1 < 2^n → n2 < 2^n →
   bitvector_of_nat n n1 = bitvector_of_nat n n2 → n1=n2.

lemma nat_of_bitvector_aux_injective:
  ∀n: nat.
  ∀l, r: BitVector n.
  ∀acc_l, acc_r: nat.
    nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r →
      acc_l = acc_r ∧ l ≃ r.
  #n #l
  elim l #r
  [1:
    #acc_l #acc_r normalize
    >(BitVector_O r) normalize /2/
  |2:
    #hd #tl #inductive_hypothesis #r #acc_l #acc_r
    normalize normalize in inductive_hypothesis;
    cases (BitVector_Sn … r)
    #r_hd * #r_tl #r_refl destruct normalize
    cases hd cases r_hd normalize
    [1:
      #relevant
      cases (inductive_hypothesis … relevant)
      #acc_assm #tl_assm destruct % //
      lapply (injective_plus_l ? ? ? acc_assm)
      -acc_assm #acc_assm
      change with (2 * acc_l = 2 * acc_r) in acc_assm;
      lapply (injective_times_r ? ? ? ? acc_assm) /2/
    |4:
      #relevant
      cases (inductive_hypothesis … relevant)
      #acc_assm #tl_assm destruct % //
      change with (2 * acc_l = 2 * acc_r) in acc_assm;
      lapply(injective_times_r ? ? ? ? acc_assm) /2/
    |2:
      #relevant  
      change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) =
        (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant;
      cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r))
      [1:
        #eqb_true_assm
        lapply (eqb_true_to_refl … eqb_true_assm)
        #refl_assm
        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
      |2:
        #eqb_false_assm
        lapply (eqb_false_to_not_refl … eqb_false_assm)
        #not_refl_assm cases not_refl_assm #absurd_assm
        cases (inductive_hypothesis … relevant) #absurd
        cases (absurd_assm absurd)
      ]
    |3:
      #relevant  
      change with ((nat_of_bitvector_aux r (2 * acc_l) tl) =
        (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant;
      cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1))
      [1:
        #eqb_true_assm
        lapply (eqb_true_to_refl … eqb_true_assm)
        #refl_assm
        lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm)
        -refl_assm #refl_assm
        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
      |2:
        #eqb_false_assm
        lapply (eqb_false_to_not_refl … eqb_false_assm)
        #not_refl_assm cases not_refl_assm #absurd_assm
        cases (inductive_hypothesis … relevant) #absurd
        cases (absurd_assm absurd)
      ]
    ]
  ]
qed.

lemma nat_of_bitvector_destruct:
  ∀n: nat.
  ∀l_hd, r_hd: bool.
  ∀l_tl, r_tl: BitVector n.
    nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) →
      l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl.
  #n #l_hd #r_hd #l_tl #r_tl
  normalize
  cases l_hd cases r_hd
  normalize
  [4:
    /2/
  |1:
    #relevant
    cases (nat_of_bitvector_aux_injective … relevant)
    #_ #l_r_tl_refl destruct /2/
  |2,3:
    #relevant
    cases (nat_of_bitvector_aux_injective … relevant)
    #absurd destruct(absurd)
  ]
qed.

lemma BitVector_cons_injective:
  ∀n: nat.
  ∀l_hd, r_hd: bool.
  ∀l_tl, r_tl: BitVector n.
    l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl.
  #l #l_hd #r_hd #l_tl #r_tl
  #l_refl #r_refl destruct %
qed.

lemma refl_nat_of_bitvector_to_refl:
  ∀n: nat.
  ∀l, r: BitVector n.
    nat_of_bitvector n l = nat_of_bitvector n r → l = r.
  #n
  elim n
  [1:
    #l #r
    >(BitVector_O l)
    >(BitVector_O r)
    #_ %
  |2:
    #n' #inductive_hypothesis #l #r
    lapply (BitVector_Sn ? l) #l_hypothesis
    lapply (BitVector_Sn ? r) #r_hypothesis
    cases l_hypothesis #l_hd #l_tail_hypothesis
    cases r_hypothesis #r_hd #r_tail_hypothesis
    cases l_tail_hypothesis #l_tl #l_hd_tl_refl
    cases r_tail_hypothesis #r_tl #r_hd_tl_refl
    destruct #cons_refl
    cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl)
    #hd_refl #tl_refl
    @BitVector_cons_injective try assumption
    @inductive_hypothesis assumption
  ]
qed.

definition two_complement_negation ≝
  λn: nat.
  λb: BitVector n.
    let new_b ≝ negation_bv n b in
      increment n new_b.
    
definition addition_n ≝
  λn: nat.
  λb, c: BitVector n.
    let 〈res,flags〉 ≝ add_with_carries n b c false in
      res.
    
definition subtraction ≝
  λn: nat.
  λb, c: BitVector n.
    addition_n n b (two_complement_negation n c).

let rec mult_aux (m,n:nat) (b:BitVector m) (c:BitVector (S n)) (acc:BitVector (S n)) on b : BitVector (S n) ≝
match b with
[ VEmpty ⇒ acc
| VCons m' hd tl ⇒
    let acc' ≝ if hd then addition_n ? c acc else acc in
    mult_aux m' n tl (shift_right_1 ?? c false) acc'
].

definition multiplication : ∀n:nat. BitVector n → BitVector n → BitVector (n + n) ≝
  λn: nat.
  match n return λn.BitVector n → BitVector n → BitVector (n + n) with
  [ O ⇒ λ_.λ_.[[ ]]
  | S m ⇒
    λb, c : BitVector (S m).
    let c' ≝ pad (S m) (S m) c in
      mult_aux ?? b (shift_left ?? m c' false) (zero ?)
  ].

definition short_multiplication : ∀n:nat. BitVector n → BitVector n → BitVector n ≝
λn,x,y. (\snd (vsplit ??? (multiplication ? x y))).

(* Division:  001...000 divided by 000...010
     Shift the divisor as far left as possible,
                                  100...000
      then try subtracting it at each
      bit position, shifting left as we go.
              001...000 - 100...000 X ⇒ 0
              001...000 - 010...000 X ⇒ 0
              001...000 - 001...000 Y ⇒ 1 (use subtracted value as new quotient)
              ...
      Then pad out the remaining bits at the front
         00..001...
*)
inductive fbs_diff : nat → Type[0] ≝
| fbs_diff' : ∀n,m. fbs_diff (S (n+m)).

let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝
match b return λn.λ_. option (fbs_diff n) with
[ VEmpty ⇒ None ?
| VCons m h t ⇒
    if h then Some ? (fbs_diff' O m)
    else match first_bit_set m t with 
         [ None ⇒ None ?
         | Some o ⇒ match o return λx.λ_. option (fbs_diff (S x)) with [ fbs_diff' x y ⇒ Some ? (fbs_diff' (S x) y) ]
         ]
].

let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝
match m with
[ O ⇒ 〈[[ ]], q〉
| S m' ⇒
    let 〈q',flags〉 ≝ add_with_carries ? q (two_complement_negation ? d) false in
    let bit ≝ head' … flags in
    let q'' ≝ if bit then q' else q in
    let 〈tl, md〉 ≝ divmod_u_aux n m' q'' (shift_right_1 ?? d false) in
    〈bit:::tl, md〉
].

definition divmod_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n) × (BitVector (S n))) ≝
  λn: nat.
  λb, c: BitVector (S n).

    match first_bit_set ? c with
    [ None ⇒ None ?
    | Some fbs' ⇒
        match fbs' return λx.λ_.option (BitVector x × (BitVector (S n))) with [ fbs_diff' fbs m ⇒
          let 〈d,m〉 ≝ (divmod_u_aux ? (S fbs) b (shift_left ?? fbs c false)) in
          Some ? 〈switch_bv_plus ??? (pad ?? d), m〉
        ]
    ].

definition division_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\fst p) ].
      
definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
  λn.
    match n with
    [ O ⇒ λb, c. None ?
    | S p ⇒ λb, c: BitVector (S p).
        let b_sign_bit ≝ get_index_v ? ? b O ? in
        let c_sign_bit ≝ get_index_v ? ? c O ? in
        match b_sign_bit with
        [ true ⇒
          let neg_b ≝ two_complement_negation ? b in
          match c_sign_bit with
          [ true ⇒
              (* I was worrying slightly about -2^(n-1), whose negation can't
                 be represented in an n bit signed number.  However, it's
                 negation comes out as 2^(n-1) as an n bit *unsigned* number,
                 so it's fine. *)
              division_u ? neg_b (two_complement_negation ? c)
          | false ⇒
              match division_u ? neg_b c with
              [ None ⇒ None ?
              | Some r ⇒ Some ? (two_complement_negation ? r)
              ]
          ]
        | false ⇒
          match c_sign_bit with
          [ true ⇒
              match division_u ? b (two_complement_negation ? c) with
              [ None ⇒ None ?
              | Some r ⇒ Some ? (two_complement_negation ? r)
              ]
          | false ⇒ division_u ? b c
          ]
        ]
   ].
    //
qed.

definition modulus_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\snd p) ].
            
definition modulus_s ≝
  λn.
  λb, c: BitVector n.
    match division_s n b c with
      [ None ⇒ None ?
      | Some result ⇒
          let 〈high_bits, low_bits〉 ≝ vsplit bool ? n (multiplication n result c) in
            Some ? (subtraction n b low_bits)
      ].
      
definition lt_u ≝
  fold_right2_i ??? 
    (λ_.λa,b,r.
      match a with
      [ true ⇒ b ∧ r
      | false ⇒ b ∨ r
      ])
    false.
      
definition gt_u ≝ λn, b, c. lt_u n c b.

definition lte_u ≝ λn, b, c. ¬(gt_u n b c).

definition gte_u ≝ λn, b, c. ¬(lt_u n b c).

definition lt_s ≝
  λn.
  λb, c: BitVector n.
    let 〈result, borrows〉 ≝ sub_with_borrows n b c false in
    match borrows with
    [ VEmpty ⇒ false
    | VCons _ bwn tl ⇒
      match tl with
      [ VEmpty ⇒ false
      | VCons _ bwpn _ ⇒
        if xorb bwn bwpn then 
          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
        else
          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
      ]
    ].
    
definition gt_s ≝ λn,b,c. lt_s n c b.

definition lte_s ≝ λn,b,c. ¬(gt_s n b c).

definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
      
alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".

definition max_u ≝ λn,a,b. if lt_u n a b then b else a.
definition min_u ≝ λn,a,b. if lt_u n a b then a else b.
definition max_s ≝ λn,a,b. if lt_s n a b then b else a.
definition min_s ≝ λn,a,b. if lt_s n a b then a else b.

definition bitvector_of_bool:
      ∀n: nat. ∀b: bool. BitVector (S n) ≝
  λn: nat.
  λb: bool.
   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
  //
qed.

definition full_add ≝
  λn: nat.
  λb, c: BitVector n.
  λd: Bit.
    fold_right2_i ? ? ? (
      λn.
       λb1, b2: bool.
        λd: Bit × (BitVector n).
        let 〈c1,r〉 ≝ d in
          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
           (xorb (xorb b1 b2) c1) ::: r〉)
     〈d, [[ ]]〉 ? b c.
    
definition half_add ≝
  λn: nat.
  λb, c: BitVector n.
    full_add n b c false.

definition add ≝
  λn: nat.
  λl, r: BitVector n.
    \snd (half_add n l r).

lemma half_add_carry_Sn:
  ∀n: nat.
  ∀l: BitVector n.
  ∀hd: bool.
    \fst (half_add (S n) (hd:::l) (false:::(zero n))) =
      andb hd (\fst (half_add n l (zero n))).
  #n #l elim l
  [1:
    #hd normalize cases hd %
  |2:
    #n' #hd #tl #inductive_hypothesis #hd'
    whd in match half_add; normalize nodelta
    whd in match full_add; normalize nodelta
    normalize in ⊢ (??%%); cases hd' normalize
    @pair_elim #c1 #r #c1_r_refl cases c1 %
  ]
qed.

lemma half_add_zero_carry_false:
  ∀m: nat.
  ∀b: BitVector m.
    \fst (half_add m b (zero m)) = false.
  #m #b elim b try %
  #n #hd #tl #inductive_hypothesis
  change with (false:::(zero ?)) in match (zero ?);
  >half_add_carry_Sn >inductive_hypothesis cases hd %
qed.

axiom half_add_true_true_carry_true:
  ∀n: nat.
  ∀hd, hd': bool.
  ∀l, r: BitVector n.
    \fst (half_add (S n) (true:::l) (true:::r)) = true.

lemma add_Sn_carry_add:
  ∀n: nat.
  ∀hd, hd': bool.
  ∀l, r: BitVector n.
    add (S n) (hd:::l) (hd':::r) =
      xorb (xorb hd hd') (\fst (half_add n l r)):::add n l r.
  #n #hd #hd' #l elim l
  [1:
    #r cases hd cases hd'
    >(BitVector_O … r) normalize %
  |2:
    #n' #hd'' #tl #inductive_hypothesis #r
    cases (BitVector_Sn … r) #hd''' * #tl' #r_refl destruct
    cases hd cases hd' cases hd'' cases hd'''
    whd in match (xorb ??);
    cases daemon
  ]
qed.
  
lemma add_zero:
  ∀n: nat.
  ∀l: BitVector n.
    l = add n l (zero …).
  #n #l elim l try %
  #n' #hd #tl #inductive_hypothesis
  change with (false:::zero ?) in match (zero ?);
  >add_Sn_carry_add >half_add_zero_carry_false
  cases hd <inductive_hypothesis %
qed.

axiom most_significant_bit_zero:
  ∀size, m: nat.
  ∀size_proof: 0 < size.
    m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false.
  normalize in size_proof; normalize @le_S_S assumption
qed.
    
axiom zero_add_head:
  ∀m: nat.
  ∀tl, hd.
    (hd:::add m (zero m) tl) = add (S m) (zero (S m)) (hd:::tl).

lemma zero_add:
  ∀m: nat.
  ∀b: BitVector m.
    add m (zero m) b = b.
  #m #b elim b try %
  #m' #hd #tl #inductive_hypothesis
  <inductive_hypothesis in ⊢ (???%);
  >zero_add_head %
qed.

axiom bitvector_of_nat_one_Sm:
  ∀m: nat.
    ∃b: BitVector m.
      bitvector_of_nat (S m) 1 ≃ b @@ [[true]].

axiom increment_zero_bitvector_of_nat_1:
  ∀m: nat.
  ∀b: BitVector m.
    increment m b = add m (bitvector_of_nat m 1) b.

axiom add_associative:
  ∀m: nat.
  ∀l, c, r: BitVector m.
    add m l (add m c r) = add m (add m l c) r.

lemma bitvector_of_nat_aux_buffer:
  ∀m, n: nat.
  ∀b: BitVector m.
    bitvector_of_nat_aux m n b = add m (bitvector_of_nat m n) b.
  #m #n elim n
  [1:
    #b change with (? = add ? (zero …) b)
    >zero_add %
  |2:
    #n' #inductive_hypothesis #b
    whd in match (bitvector_of_nat_aux ???);
    >inductive_hypothesis whd in match (bitvector_of_nat ??) in ⊢ (???%);
    >inductive_hypothesis >increment_zero_bitvector_of_nat_1
    >increment_zero_bitvector_of_nat_1 <(add_zero m (bitvector_of_nat m 1))
    <add_associative %
  ]
qed.

definition sign_extension: Byte → Word ≝
  λc.
    let b ≝ get_index_v ? 8 c 1 ? in
      [[ b; b; b; b; b; b; b; b ]] @@ c.
  normalize
  repeat (@le_S_S)
  @le_O_n
qed.

lemma bitvector_of_nat_sign_extension_equivalence:
  ∀m: nat.
  ∀size_proof: m < 128.
    sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m.
  #m #size_proof whd in ⊢ (??%?);
  >most_significant_bit_zero
  [1:
    elim m
    [1:
      %
    |2:
      #n' #inductive_hypothesis whd in match bitvector_of_nat; normalize nodelta
      whd in match (bitvector_of_nat_aux ???);
      whd in match (bitvector_of_nat_aux ???) in ⊢ (???%);
      >(bitvector_of_nat_aux_buffer 16 n')
      cases daemon
    ]
  |2:
    assumption
  ]
qed.

axiom add_commutative:
  ∀n: nat.
  ∀l, r: BitVector n.
    add … l r = add … r l.

axiom nat_of_bitvector_add:
 ∀n,v1,v2.
  nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n →
   nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.

axiom add_bitvector_of_nat:
 ∀n,m1,m2.
  bitvector_of_nat n (m1 + m2) =
   add n (bitvector_of_nat n m1) (bitvector_of_nat n m2).

(* CSC: corollary of add_bitvector_of_nat *)
axiom add_overflow:
 ∀n,m,r. m + r = 2^n →
  add n (bitvector_of_nat n m) (bitvector_of_nat n r) = zero n.

example add_SO:
  ∀n: nat.
  ∀m: nat.
    add n (bitvector_of_nat … m) (bitvector_of_nat … 1) = bitvector_of_nat … (S m).
 cases daemon.
qed.

axiom add_bitvector_of_nat_plus:
  ∀n,p,q:nat.
    add n (bitvector_of_nat ? p) (bitvector_of_nat ? q) = bitvector_of_nat ? (p+q).
    
lemma add_bitvector_of_nat_Sm:
  ∀n, m: nat.
    add … (bitvector_of_nat … 1) (bitvector_of_nat … m) =
      bitvector_of_nat n (S m).
 #n #m @add_bitvector_of_nat_plus
qed.

axiom le_to_le_nat_of_bitvector_add:
  ∀n,v,m1,m2.
    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 ≤ m2 → 
      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) ≤
      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).

lemma lt_to_lt_nat_of_bitvector_add:
  ∀n,v,m1,m2.
    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 → 
      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <
      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
#n #v #m1 #m2 #m2_ok #bounded #H
lapply (le_to_le_nat_of_bitvector_add n v (S m1) m2 ??) try assumption
#K @(transitive_le … (K H))
cases daemon (*CSC: TRUE, complete*)
qed.

definition sign_bit : ∀n. BitVector n → bool ≝
λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].

definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝
λm,n,v. pad_vector ? (sign_bit ? v) ?? v.

definition zero_ext : ∀m,n. BitVector m → BitVector n ≝
λm,n.
  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
  | nat_eq n' ⇒ λv. v
  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
  ].

definition sign_ext : ∀m,n. BitVector m → BitVector n ≝
λm,n.
  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v)
  | nat_eq n' ⇒ λv. v
  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
  ].

example sub_minus_one_seven_eight:
  ∀v: BitVector 7.
  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
 cases daemon.
qed.

axiom sub16_with_carry_overflow:
  ∀left, right, result: BitVector 16.
  ∀flags: BitVector 3.
  ∀upper: BitVector 9.
  ∀lower: BitVector 7.
    sub_16_with_carry left right false = 〈result, flags〉 →
      vsplit bool 9 7 result = 〈upper, lower〉 →
        get_index_v bool 3 flags 2 ? = true →
          upper = [[true; true; true; true; true; true; true; true; true]].
  //
qed.

axiom sub_16_to_add_16_8_0:
 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
  get_index' ? 2 0 flags = false →
  sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 →
   v1 = add ? v2 (sign_extension (false:::v3)).

axiom sub_16_to_add_16_8_1:
 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
  get_index' ? 2 0 flags = true →
  sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 →
   v1 = add ? v2 (sign_extension (true:::v3)).