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

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
     let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_carry in
     let carry ≝ carry_of b c last_carry 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 ≝ exclusive_disjunction (exclusive_disjunction 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 ≝ exclusive_disjunction 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 ≝ exclusive_disjunction 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.

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).
    
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).
    
definition multiplication ≝
  λn: nat.
  λb, c: BitVector n.
    let b_nat ≝ nat_of_bitvector ? b in
    let c_nat ≝ nat_of_bitvector ? c in
    let result ≝ b_nat * c_nat in
      bitvector_of_nat (n + n) result.
      
definition division_u ≝
  λn: nat.
  λb, c: BitVector n.
    let b_nat ≝ nat_of_bitvector ? b in
    let c_nat ≝ nat_of_bitvector ? c in
    match c_nat with
    [ O ⇒ None ?
    | _ ⇒
      let result ≝ b_nat ÷ c_nat in
        Some ? (bitvector_of_nat n result)
    ].
      
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
        let b_as_nat ≝ nat_of_bitvector ? b in
        let c_as_nat ≝ nat_of_bitvector ? c in
        match c_as_nat with
        [ O ⇒ None ?
        | S o ⇒
          match b_sign_bit with
          [ true ⇒
            let temp_b ≝ b_as_nat - (2^p) in
            match c_sign_bit with
            [ true ⇒
              let temp_c ≝ c_as_nat - (2^p) in
                Some ? (bitvector_of_nat ? (temp_b ÷ temp_c)) 
            | false ⇒
              let result ≝ (temp_b ÷ c_as_nat) + (2^p) in
                Some ? (bitvector_of_nat ? result)
            ] 
          | false ⇒
            match c_sign_bit with
            [ true ⇒
              let temp_c ≝ c_as_nat - (2^p) in
              let result ≝ (b_as_nat ÷ temp_c) + (2^p) in
                Some ? (bitvector_of_nat ? result)
            | false ⇒ Some ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat))
            ]
          ]
        ]
    ].
    //
qed.

definition modulus_u ≝
  λn.
  λb, c: BitVector n.
    let b_nat ≝ nat_of_bitvector ? b in
    let c_nat ≝ nat_of_bitvector ? c in
    match c_nat with
    [ O ⇒ None ?
    | _ ⇒ 
      let result ≝ modulus b_nat c_nat in
      Some ? (bitvector_of_nat n result)
    ].
            
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 exclusive_disjunction 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 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)),
           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
     〈d, [[ ]]〉 ? b c.
    
definition half_add ≝
  λn: nat.
  λb, c: BitVector n.
    full_add n b c false.