source: src/ASM/Arithmetic.ma @ 2593

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".

(* Some properties of addition_n *)
lemma commutative_add_with_carries : ∀n,a,b,carry. add_with_carries n a b carry = add_with_carries n b a carry.
#n elim n
[ 1: #a #b #carry 
     lapply (BitVector_O … a) lapply (BitVector_O … b) #H1 #H2 destruct @refl
| 2: #n' #Hind #a #b #carry
     lapply (BitVector_Sn … a) lapply (BitVector_Sn … b)
     * #bhd * #btl #Heqb
     * #ahd * #atl #Heqa destruct
     lapply (Hind atl btl carry)
     whd in match (add_with_carries ????) in ⊢ ((??%%) →  (??%%));
     normalize in match (rewrite_l ??????);
     normalize nodelta
     #Heq >Heq
     generalize in match (fold_right2_i ????????); * #res #carries
     normalize nodelta
     cases ahd cases bhd @refl
] qed.

lemma commutative_addition_n : ∀n,a,b. addition_n n a b = addition_n n b a.
#n #a #b whd in match (addition_n ???) in ⊢ (??%%); >commutative_add_with_carries
@refl
qed.

(* -------------------------------------------------------------------------- *)
(* Associativity proof for addition_n. The proof relies on the observation 
 * that the two carries (inner and outer) in the associativity equation are not
 * independent. In fact, the global carry can be encoded in a three-valued bits
 * (versus 2 full bits, i.e. 4 possibilites, for two carries). I seriously hope
 * this proof can be simplified, but now it's proved at least. *)

inductive ternary : Type[0] ≝ 
| Zero_carry : ternary
| One_carry : ternary
| Two_carry : ternary.

definition carry_0 ≝ λcarry. 
    match carry with
    [ Zero_carry ⇒ 〈false, Zero_carry〉
    | One_carry ⇒ 〈true, Zero_carry〉
    | Two_carry ⇒ 〈false, One_carry〉 ].
    
definition carry_1 ≝ λcarry. 
    match carry with
    [ Zero_carry ⇒ 〈true, Zero_carry〉
    | One_carry ⇒ 〈false, One_carry〉
    | Two_carry ⇒ 〈true, One_carry〉 ].

definition carry_2 ≝ λcarry. 
    match carry with
    [ Zero_carry ⇒ 〈false, One_carry〉
    | One_carry ⇒ 〈true, One_carry〉
    | Two_carry ⇒ 〈false, Two_carry〉 ].

definition carry_3 ≝ λcarry. 
    match carry with
    [ Zero_carry ⇒ 〈true, One_carry〉
    | One_carry ⇒ 〈false, Two_carry〉
    | Two_carry ⇒ 〈true, Two_carry〉 ].

(* Count the number of true bits in {xa,xb,xc} and compute the new bit along the new carry,
   according to the last one. *)
definition ternary_carry_of ≝ λxa,xb,xc,carry.
if xa then
  if xb then
    if xc then
      carry_3 carry
    else
      carry_2 carry
  else
    if xc then
      carry_2 carry
    else
      carry_1 carry
else
  if xb then
    if xc then
      carry_2 carry
    else
      carry_1 carry
  else
    if xc then
      carry_1 carry
    else
      carry_0 carry.

let rec canonical_add (n : nat) (a,b,c : BitVector n) (init : ternary) on a : (BitVector n × ternary) ≝
match a in Vector return λsz.λ_. BitVector sz → BitVector sz → (BitVector sz × ternary) with
[ VEmpty ⇒ λ_,_. 〈VEmpty ?, init〉
| VCons sz' xa tla ⇒ λb',c'.
  let xb ≝ head' … b' in
  let xc ≝ head' … c' in
  let tlb ≝ tail … b' in
  let tlc ≝ tail … c' in
  let 〈bits, last〉 ≝ canonical_add ? tla tlb tlc init in
  let 〈bit, carry〉 ≝ ternary_carry_of xa xb xc last in
  〈bit ::: bits, carry〉
] b c.

(* convert the classical carries (inner and outer) to ternary) *)
definition carries_to_ternary ≝ λcarry1,carry2.
  if carry1
  then if carry2 
       then Two_carry
       else One_carry
  else if carry2 
       then One_carry
       else Zero_carry.

(* Copied back from Clight/casts.ma *)
lemma add_with_carries_unfold : ∀n,x,y,c.
  add_with_carries n x y c = fold_right2_i ????? n x y.
// qed.       
    
lemma add_with_carries_Sn : ∀n,a_hd,a_tl,b_hd,b_tl,carry. 
  add_with_carries (S n) (a_hd ::: a_tl) (b_hd ::: b_tl) carry =
   (let 〈lower_bits,carries〉 ≝ add_with_carries n a_tl b_tl carry in 
    let last_carry ≝
    match carries in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
    [VEmpty⇒carry
    |VCons (sz:ℕ) (cy:bool) (tl:(Vector bool sz))⇒cy] 
    in 
    if last_carry then 
      let bit   ≝ xorb (xorb a_hd b_hd) true in 
      let carry ≝ carry_of a_hd b_hd true in 
      〈bit:::lower_bits,carry:::carries〉 
    else 
      let bit ≝ xorb (xorb a_hd b_hd) false in 
      let carry ≝ carry_of a_hd b_hd false in 
      〈bit:::lower_bits,carry:::carries〉).
#n #a_hd #a_tl #b_hd #b_tl #carry
whd in match (add_with_carries ????);
normalize nodelta
<add_with_carries_unfold
cases (add_with_carries n a_tl b_tl carry)
#lower_bits #carries normalize nodelta
elim n in a_tl b_tl lower_bits carries;
[ 1: #a_tl #b_tl #lower_bits #carries
     >(BitVector_O … carries) normalize nodelta
     cases carry normalize nodelta
     cases a_hd cases b_hd //
| 2: #n' #Hind #a_tl #b_tl #lower_bits #carries
     lapply (BitVector_Sn … carries) * #carries_hd * #carries_tl
     #Heq >Heq normalize nodelta
     cases carries_hd cases a_hd cases b_hd normalize nodelta
     //
] qed.

(* Correction of [canonical_add], left side. Note the invariant on carries. *)
lemma canonical_add_left : ∀n,carry1,carry2,a,b,c.
  let 〈res_ab,flags_ab〉 ≝ add_with_carries n a b carry1 in
  let 〈res_ab_c,flags_ab_c〉 ≝ add_with_carries n res_ab c carry2 in
  let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c (carries_to_ternary carry1 carry2) in
  res_ab_c = res_canonical
  ∧ (match n return λx. BitVector x → BitVector x → Prop with
     [ O ⇒ λ_.λ_. True
     | S _ ⇒ λflags_ab',flags_ab_c'. carries_to_ternary (head' … flags_ab') (head' … flags_ab_c') = last_carry
     ] flags_ab flags_ab_c).
#n elim n
[ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try //
| 2: #n' #Hind #carry1 #carry2 #a #b #c
     elim (BitVector_Sn … a) #xa * #a' #Heq_a
     elim (BitVector_Sn … b) #xb * #b' #Heq_b
     elim (BitVector_Sn … c) #xc * #c' #Heq_c
     lapply (Hind … carry1 carry2 a' b' c') -Hind
     destruct >add_with_carries_Sn
     elim (add_with_carries … a' b' carry1) #Hres_ab #Hflags_ab normalize nodelta
     lapply Hflags_ab lapply Hres_ab lapply c' lapply b' lapply a'
     -Hflags_ab -Hres_ab -c' -b' -a'
     cases n'
     [ 1: #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta
          >(BitVector_O … a') >(BitVector_O … b') >(BitVector_O … c')
          >(BitVector_O … Hres_ab) >(BitVector_O … Hflags_ab)
          normalize nodelta #_
          cases carry1 cases carry2 cases xa cases xb cases xc normalize @conj try //
     | 2: #n' #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta
          elim (BitVector_Sn … Hflags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab
          normalize nodelta
          elim (BitVector_Sn … Hres_ab) #hd_res_ab * #tl_res_ab #Heq_res_ab >Heq_res_ab
          cases hd_flags_ab in Heq_flags_ab; #Heq_flags_ab normalize nodelta
          >add_with_carries_Sn
          elim (add_with_carries (S n') (hd_res_ab:::tl_res_ab) c' carry2) #res_ab_c #flags_ab_c 
          normalize nodelta
          elim (BitVector_Sn … flags_ab_c) #hd_flags_ab_c * #tl_flags_ab_c #Heq_flags_ab_c >Heq_flags_ab_c
          normalize nodelta
          cases hd_flags_ab_c in Heq_flags_ab_c; #Heq_flags_ab_c
          normalize nodelta 
          whd in match (canonical_add (S (S ?)) ? ? ? ?); 
          whd in match (tail ???); whd in match (tail ???);
          elim (canonical_add (S n') a' b' c' (carries_to_ternary carry1 carry2)) #res_canonical #last_carry normalize
          * #Hres_ab_is_canonical #Hlast_carry <Hlast_carry normalize
          >Hres_ab_is_canonical
          cases xa cases xb cases xc try @conj try @refl
     ]
] qed.

(* Symmetric. The two sides are most certainly doable in a single induction, but lazyness
   prevails over style.  *)
lemma canonical_add_right : ∀n,carry1,carry2,a,b,c.
  let 〈res_bc,flags_bc〉 ≝ add_with_carries n b c carry1 in
  let 〈res_a_bc,flags_a_bc〉 ≝ add_with_carries n a res_bc carry2 in
  let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c (carries_to_ternary carry1 carry2) in
  res_a_bc = res_canonical
  ∧ (match n return λx. BitVector x → BitVector x → Prop with
     [ O ⇒ λ_.λ_. True
     | S _ ⇒ λflags_bc',flags_a_bc'. carries_to_ternary (head' … flags_bc') (head' … flags_a_bc') = last_carry
     ] flags_bc flags_a_bc).
#n elim n
[ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try //
| 2: #n' #Hind #carry1 #carry2 #a #b #c
     elim (BitVector_Sn … a) #xa * #a' #Heq_a
     elim (BitVector_Sn … b) #xb * #b' #Heq_b
     elim (BitVector_Sn … c) #xc * #c' #Heq_c
     lapply (Hind … carry1 carry2 a' b' c') -Hind
     destruct >add_with_carries_Sn
     elim (add_with_carries … b' c' carry1) #Hres_bc #Hflags_bc normalize nodelta
     lapply Hflags_bc lapply Hres_bc lapply c' lapply b' lapply a'
     -Hflags_bc -Hres_bc -c' -b' -a'
     cases n'
     [ 1: #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta
          >(BitVector_O … a') >(BitVector_O … b') >(BitVector_O … c')
          >(BitVector_O … Hres_bc) >(BitVector_O … Hflags_bc)
          normalize nodelta #_
          cases carry1 cases carry2 cases xa cases xb cases xc normalize @conj try //
     | 2: #n' #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta
          elim (BitVector_Sn … Hflags_bc) #hd_flags_bc * #tl_flags_bc #Heq_flags_bc >Heq_flags_bc
          normalize nodelta
          elim (BitVector_Sn … Hres_bc) #hd_res_bc * #tl_res_bc #Heq_res_bc >Heq_res_bc
          cases hd_flags_bc in Heq_flags_bc; #Heq_flags_bc normalize nodelta
          >add_with_carries_Sn
          elim (add_with_carries (S n') a' (hd_res_bc:::tl_res_bc) carry2) #res_a_bc #flags_a_bc
          normalize nodelta
          elim (BitVector_Sn … flags_a_bc) #hd_flags_a_bc * #tl_flags_a_bc #Heq_flags_a_bc >Heq_flags_a_bc
          normalize nodelta
          cases (hd_flags_a_bc) in Heq_flags_a_bc; #Heq_flags_a_bc
          whd in match (canonical_add (S (S ?)) ????); 
          whd in match (tail ???); whd in match (tail ???);
          elim (canonical_add (S n') a' b' c' (carries_to_ternary carry1 carry2)) #res_canonical #last_carry normalize
          * #Hres_bc_is_canonical #Hlast_carry <Hlast_carry normalize 
          >Hres_bc_is_canonical
          cases xa cases xb cases xc try @conj try @refl
     ]
] qed.


(* Note that we prove a result more general that just associativity: we can vary the carries. *)
lemma associative_add_with_carries :
  ∀n,carry1,carry2,a,b,c.
  (\fst (add_with_carries n a (let 〈res,flags〉 ≝ add_with_carries n b c carry1 in res) carry2))
   =
  (\fst (add_with_carries n (let 〈res,flags〉 ≝ add_with_carries n a b carry1 in res) c carry2)).
#n cases n
[ 1: #carry1 #carry2 #a #b #c
      >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c)
      normalize try @refl
| 2: #n' #carry1 #carry2 #a #b #c
     lapply (canonical_add_left … carry1 carry2 a b c) 
     lapply (canonical_add_right … carry1 carry2 a b c)
     normalize nodelta
     elim (add_with_carries (S n') b c carry1) #res_bc #flags_bc
     elim (add_with_carries (S n') a b carry1) #res_ab #flags_ab
     normalize nodelta
     elim (add_with_carries (S n') a res_bc carry2) #res_a_bc #flags_a_bc
     normalize nodelta     
     elim (add_with_carries (S n') res_ab c carry2) #res_ab_c #flags_ab_c
     normalize nodelta
     cases (canonical_add ? a b c (carries_to_ternary carry1 carry2)) #canonical_bits #last_carry
     normalize nodelta
     * #HA #HB * #HC #HD destruct @refl
] qed.

(* This closes the proof of associativity for bitvector addition. *)     

lemma associative_addition_n : ∀n,a,b,c. addition_n n a (addition_n n b c) = addition_n n (addition_n n a b) c.
#n #a #b #c
whd in match (addition_n ???) in ⊢ (??%%);
whd in match (addition_n n b c);
whd in match (addition_n n a b);
lapply (associative_add_with_carries … false false a b c)
elim (add_with_carries n b c false) #bc_bits #bc_flags
elim (add_with_carries n a b false) #ab_bits #ab_flags
normalize nodelta
elim (add_with_carries n a bc_bits false) #a_bc_bits #a_bc_flags
elim (add_with_carries n ab_bits c false) #ab_c_bits #ab_c_flags
normalize
#H @H
qed.



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)).