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

definition addr16_of_addr11: Word → Word11 → Word ≝
  λpc: Word.
  λa: Word11.
  let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in
  let 〈n1, n2〉 ≝ split … 4 4 pc_upper in
  let 〈b123, b〉 ≝ split … 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.

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

(* 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〉 ≝ split 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 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 (split … (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 (split … (switch_bv_plus … v))
  ].