| Splitting bitvectors into component pieces |
Require Import Arith Bool Bvector Euclid.
Require Import Asm.Util.ArithUtil.
Require Import Asm.Util.Mod.
Require Import Asm.Util.Tactics.
Require Import Asm.Bitvector.BArith.
Require Import Asm.Bitvector.Bitwise.
Require Import Asm.Bitvector.Convert.
Require Import Asm.Bitvector.Defs.
The basic split operation |
| Split an even-length bitvector into its two halves |
Definition split_word n (v : Bvector (2 * n)) :=
eucl_dev (pow2 n) (pow2_pos n) (bvec_to_nat v).
Definition lower_half n (v : Bvector (2 * n)) :=
match split_word n v with
divex q r _ _ => nat_to_bvec n r
end.
Definition upper_half n (v : Bvector (2 * n)) :=
match split_word n v with
divex q r _ _ => nat_to_bvec n q
end.
Theorem split_sound : forall n (v : Bvector (2 * n)),
bvec_to_nat v = bvec_to_nat (lower_half n v) + pow2 n * bvec_to_nat (upper_half n v).
Specialized to 32 bits |
Definition byte1 (v : int32) : int8 := lower_half 8 (lower_half 16 v).
Definition byte2 (v : int32) : int8 := upper_half 8 (lower_half 16 v).
Definition byte3 (v : int32) : int8 := lower_half 8 (upper_half 16 v).
Definition byte4 (v : int32) : int8 := upper_half 8 (upper_half 16 v).
Theorem split32_sound : forall v,
bvec_to_nat v
= bvec_to_nat (byte1 v)
+ pow2 8 * bvec_to_nat (byte2 v)
+ pow2 16 * bvec_to_nat (byte3 v)
+ pow2 24 * bvec_to_nat (byte4 v).