File size: 4,274 Bytes
0ba037b | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 | (* Address mapping of rtl/bit_accelerator.sv.
Part 1 states the mapping over unbounded integers.
Part 2 states the RTL's 64-bit datapath over bit-vectors and proves it
implements Part 1 whenever (base << 3) + offset does not overflow. *)
module BitAddress
use int.Int
use int.EuclideanDivision
constant word_bits : int = 64
(* base is a byte address, offset a bit offset; result is a bit address. *)
function effective_bit (base offset : int) : int = base * 8 + offset
function word_index (b : int) : int = div b word_bits
function bit_index (b : int) : int = mod b word_bits
function word_byte_address (b : int) : int = word_index b * 8
lemma decomposition :
forall b : int. b = word_index b * word_bits + bit_index b
lemma bit_index_bounds :
forall b : int. 0 <= bit_index b < word_bits
lemma word_byte_address_aligned :
forall b : int. mod (word_byte_address b) 8 = 0
(* (word, bit) identifies a bit address uniquely. *)
lemma decomposition_injective :
forall b1 b2 : int.
word_index b1 = word_index b2 -> bit_index b1 = bit_index b2 -> b1 = b2
(* Offsets 0..63 from a word-aligned base stay in that word, in order. *)
lemma aligned_base_same_word :
forall base k : int. mod base 8 = 0 -> 0 <= k < word_bits ->
word_index (effective_bit base k) = div base 8 /\
bit_index (effective_bit base k) = k
(* Adding 64 to the bit address moves to the next word, same bit. *)
lemma next_word :
forall b : int.
word_index (b + word_bits) = word_index b + 1 /\
bit_index (b + word_bits) = bit_index b
(* Offsets 0 and 64 from any base land in adjacent words. *)
lemma offset_64_next_word :
forall base : int.
word_index (effective_bit base 64) = word_index (effective_bit base 0) + 1
end
module RtlDatapath
use int.Int
use int.EuclideanDivision
use bv.BV64
use BitAddress
(* The RTL expressions, verbatim in bit-vector form. *)
function eff_bit (base offset : t) : t = add (lsl_bv base (3 : t)) offset
function bit_idx (e : t) : t = bw_and e (63 : t)
function req_addr (e : t) : t = lsl_bv (lsr_bv e (6 : t)) (3 : t)
lemma bit_idx_lt_64 :
forall e : t. ult (bit_idx e) (64 : t)
lemma req_addr_aligned :
forall e : t. bw_and (req_addr e) (7 : t) = (0 : t)
(* The word address and bit index recompose the effective bit address. *)
lemma rtl_decomposition :
forall e : t. add (lsl_bv (lsr_bv e (6 : t)) (6 : t)) (bit_idx e) = e
(* The shift/mask forms equal division, remainder and multiplication. *)
lemma bit_idx_is_urem :
forall e : t. bit_idx e = urem e (64 : t)
lemma req_addr_is_udiv_mul :
forall e : t. req_addr e = mul (udiv e (64 : t)) (8 : t)
lemma shl3_is_mul8 :
forall b : t. lsl_bv b (3 : t) = mul b (8 : t)
(* Trusted base: four specialisations of facts in the Why3 standard library
module bv.BV64 (axioms to_uint_urem and to_uint_udiv at divisor 64, lemmas
to_uint_mul_bounded at factor 8 and to_uint_add_bounded). The SMT drivers
map urem/udiv/mul/add to native bit-vector operations and do not pass the
library's integer axioms on, so these instances are restated here. Each is
true in SMT-LIB bit-vector semantics. Everything else in this file is
proved, not assumed. *)
axiom urem_64 : forall e : t. t'int (urem e (64 : t)) = mod (t'int e) 64
axiom udiv_64 : forall e : t. t'int (udiv e (64 : t)) = div (t'int e) 64
axiom mul_8_bounded :
forall a : t. t'int a * 8 < two_power_size -> t'int (mul a (8 : t)) = t'int a * 8
axiom add_bounded :
forall a b : t. t'int a + t'int b < two_power_size ->
t'int (add a b) = t'int a + t'int b
lemma udiv_64_bound : forall e : t. 0 <= div (t'int e) 64 * 8 < two_power_size
(* Bridge to the integer specification. *)
lemma bit_idx_is_mod :
forall e : t. t'int (bit_idx e) = bit_index (t'int e)
lemma req_addr_is_word_byte_address :
forall e : t. t'int (req_addr e) = word_byte_address (t'int e)
(* Without overflow the 64-bit sum equals the integer effective address. *)
lemma eff_bit_no_overflow :
forall base offset : t.
t'int base * 8 + t'int offset < two_power_size ->
t'int (eff_bit base offset) = effective_bit (t'int base) (t'int offset)
end
|