include "Exponential.ma". include "BitVector.ma". ndefinition nat_of_bool ≝ λb: Bool. match b with [ false ⇒ Z | true ⇒ S Z ]. ndefinition add_n_with_carry: ∀n: Nat. ∀b, c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝ λn: Nat. λb: BitVector n. λc: BitVector n. λcarry: Bool. let b_as_nat ≝ nat_of_bitvector n b in let c_as_nat ≝ nat_of_bitvector n c in let carry_as_nat ≝ nat_of_bool carry in let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) * n)) + (modulus c_as_nat ((S (S Z)) * n)) + c_as_nat) ≳ ((S (S Z)) * n) in let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n - (S Z)))) + (modulus c_as_nat ((S (S Z))^(n - (S Z)))) + c_as_nat) ≳ ((S (S Z))^(n - (S Z)))) in let result ≝ modulus result_old ((S (S Z))^n) in let cy_flag ≝ (result_old ≳ ((S (S Z))^n)) in let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in mk_Cartesian ? ? (bitvector_of_nat n result) ([[ cy_flag ; ac_flag ; ov_flag ]]). ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (BitVector three) ≝ λb: BitVector eight. λc: BitVector eight. λcarry: Bool. let b_as_nat ≝ nat_of_bitvector eight b in let c_as_nat ≝ nat_of_bitvector eight c in let carry_as_nat ≝ nat_of_bool carry in let temporary ≝ b_as_nat mod sixteen - c_as_nat mod sixteen in let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≲ (c_as_nat mod sixteen)) (temporary ≲ carry_as_nat)) in let bit_six ≝ negation (conjunction ((b_as_nat mod one_hundred_and_twenty_eight) ≲ (c_as_nat mod one_hundred_and_twenty_eight)) (temporary ≲ carry_as_nat)) in let old_result_1 ≝ b_as_nat - c_as_nat in let old_result_2 ≝ old_result_1 - carry_as_nat in let ov_flag ≝ exclusive_disjunction carry bit_six in match conjunction (b_as_nat ≲ c_as_nat) (old_result_1 ≲ carry_as_nat) with [ false ⇒ let cy_flag ≝ false in 〈 bitvector_of_nat eight old_result_2, [[ cy_flag ; ac_flag ; ov_flag ]]〉 | true ⇒ let cy_flag ≝ true in let new_result ≝ b_as_nat + two_hundred_and_fifty_six - c_as_nat - carry_as_nat in 〈 bitvector_of_nat eight new_result, [[ cy_flag ; ac_flag ; ov_flag ]]〉 ]. ndefinition add_8_with_carry ≝ add_n_with_carry eight. ndefinition add_16_with_carry ≝ add_n_with_carry sixteen. ndefinition increment ≝ λn: Nat. λb: BitVector n. let b_as_nat ≝ (nat_of_bitvector n b) + (S Z) in let overflow ≝ b_as_nat ≳ (S (S Z))^n in match overflow with [ false ⇒ bitvector_of_nat n b_as_nat | true ⇒ zero n ]. ndefinition decrement ≝ λn: Nat. λb: BitVector n. let b_as_nat ≝ nat_of_bitvector n b in match b_as_nat with [ Z ⇒ max n | S o ⇒ bitvector_of_nat n o ]. alias symbol "greater_than_or_equal" (instance 1) = "Nat greater than or equal prop". ndefinition bitvector_of_bool: ∀n: Nat. ∀b: Bool. BitVector (S n) ≝ λn: Nat. λb: Bool. (pad (S n - (S Z)) (S Z) [[b]])⌈(S n - (S Z)) + S Z ↦ S n⌉. /2/. nqed. ndefinition 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 〈inclusive_disjunction (conjunction b1 b2) (conjunction c1 (inclusive_disjunction b1 b2)), (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉) 〈d, [[ ]]〉 ? b c. ndefinition half_add ≝ λn: Nat. λb, c: BitVector n. full_add n b c false.