| Fixed-size bit vectors with two's-complement arithmetic |
Require Import Arith ZArith.
Require Import Bool Bvector.
Require Import Asm.Util.ArithUtil.
Require Import Asm.Util.Mod.
Require Import Asm.Util.Specif.
Require Import Asm.Util.Tactics.
Require Import Asm.Util.Vector.
Set Implicit Arguments.
Abbreviations for specific sizes |
Definition int8 := Bvector 8.
Definition int16 := Bvector 16.
Definition int32 := Bvector 32.
Equality |
| Strongly-specified, decidable equality |
Definition bvec_eq_dec : forall n (v1 v2 : Bvector n), {v1 = v2} + {v1 <> v2}.
Definition int8_eq_dec := @bvec_eq_dec 8.
Definition int16_eq_dec := @bvec_eq_dec 16.
Definition int32_eq_dec := @bvec_eq_dec 32.
| Boolean decidable equality |
Definition bvec_eq n (v1 v2 : Bvector n) := sum_to_bool (bvec_eq_dec v1 v2).
Definition int8_eq := @bvec_eq 8.
Definition int16_eq := @bvec_eq 16.
Definition int32_eq := @bvec_eq 32.
Constants |
| Constant zero vectors |
Definition bzero := Bvect_false.
Definition bzero8 := bzero 8.
Definition bzero16 := bzero 16.
Definition bzero32 := bzero 32.
| Maximal vectors for particular sizes |
Definition bmax := Bvect_true.
Conversion |
Converting bitvectors into naturals |
Fixpoint bvec_to_nat n (v : Bvector n) {struct v} : nat :=
match v with
| Vnil => O
| Vcons false n v => 2 * bvec_to_nat v
| Vcons true n v => 1 + 2 * bvec_to_nat v
end.
Converting naturals into bitvectors |
Fixpoint nat_to_bvec (bound n : nat) {struct bound} : Bvector bound :=
match bound as x return Bvector x with
| O => Bnil
| S bound =>
Bcons (mod2_bool n) bound (nat_to_bvec bound (div2 n))
end.
Constant one vectors |
Definition bone (n : nat) := nat_to_bvec n 1.
Definition bone8 := bone 8.
Definition bone16 := bone 16.
Definition bone32 := bone 32.
Increment and decrement |
| Increment |
Fixpoint binc len (v : Bvector len) {struct v} : Bvector len :=
match v in vector _ len return Bvector len with
| Vnil => Bnil
| Vcons false n v => Bcons true n v
| Vcons true n v => Bcons false n (binc v)
end.
Definition binc2 n (v : Bvector n) := binc (binc v).
Definition binc3 n (v : Bvector n) := binc (binc (binc v)).
Definition binc4 n (v : Bvector n) := binc (binc (binc (binc v))).
| Decrement |
Fixpoint bdec len (v : Bvector len) {struct v} : Bvector len :=
match v in vector _ len return Bvector len with
| Vnil => Bnil
| Vcons false n v => Bcons true n (bdec v)
| Vcons true n v => Bcons false n v
end.
Definition bdec2 n (v : Bvector n) := bdec (bdec v).
Definition bdec3 n (v : Bvector n) := bdec (bdec (bdec v)).
Definition bdec4 n (v : Bvector n) := bdec (bdec (bdec (bdec v))).
Bitwise operations |
| NOT |
Definition bnot := Bneg.
Definition bnot8 := @bnot 8.
Definition bnot16 := @bnot 16.
Definition bnot32 := @bnot 32.
| AND |
Definition band := BVand.
Definition band8 := @band 8.
Definition band16 := @band 16.
Definition band32 := @band 32.
| OR |
Definition bor := BVor.
Definition bor8 := @bor 8.
Definition bor16 := @bor 16.
Definition bor32 := @bor 32.
| Left shift |
Definition bshl := BshiftL_iter.
Definition bshl8 := @bshl 7.
Definition bshl16 := @bshl 15.
Definition bshl32 := @bshl 31.
| Right shift |
Definition bshr := BshiftRl_iter.
Definition bshr8 := @bshr 7.
Definition bshr16 := @bshr 15.
Definition bshr32 := @bshr 31.
Two's complement arithmetic |
| Negation |
Definition bneg len (v : Bvector len) := binc (bnot v).
Definition bneg8 := @bneg 8.
Definition bneg16 := @bneg 16.
Definition bneg32 := @bneg 32.
| Generic arithmetic operation |
Definition barith f bound (v1 v2 : Bvector bound) :=
nat_to_bvec bound (f (bvec_to_nat v1) (bvec_to_nat v2)).
| Addition |
Definition badd := barith plus.
Definition badd8 := @badd 8.
Definition badd16 := @badd 16.
Definition badd32 := @badd 32.
| Subtraction |
Definition bsub bound v1 v2 := @barith plus bound v1 (bneg v2).
Definition bsub8 := @bsub 8.
Definition bsub16 := @bsub 16.
Definition bsub32 := @bsub 32.
Decidable comparisons |
| Less-than |
Definition blt_dec n (v1 v2 : Bvector n) :=
dec_lt (bvec_to_nat v1) (bvec_to_nat v2).
| Less-than-or-equal-to |
Definition ble_dec n (v1 v2 : Bvector n) :=
dec_le (bvec_to_nat v1) (bvec_to_nat v2).