(* Bit addressing and single-bit operation specification for bit_accelerator_v2. Memory is a map from word index to an integer word value. Addresses: absolute bit address = base_byte_address * 8 + bit_offset word index = bit address / 64 bit index = bit address mod 64 (Euclidean division) Corrections relative to the earlier draft (each disproved by Z3): - bit_63_same_word and bit_index_wraps_at_64 only hold for a word-aligned base (base mod 8 = 0); base = 7 and base = 1 are counterexamples. - within_word_uniqueness claimed two different offsets never share a bit index; offsets 0 and 64 do. It now states that (word, bit) determines the bit address. - disjoint_words_independent used a function where a bit result was meant. *) module BitAddressing use int.Int use int.EuclideanDivision use int.Power constant word_bits : int = 64 constant max_address : int = 281474976710656 (* 2^48 words *) predicate is_valid_bit_address (addr : int) = 0 <= addr < max_address * word_bits predicate word_aligned (addr : int) = mod addr word_bits = 0 function absolute_bit_address (base_byte_addr bit_offset : int) : int = base_byte_addr * 8 + bit_offset function word_index (bit_addr : int) : int = div bit_addr word_bits function bit_index_in_word (bit_addr : int) : int = mod bit_addr word_bits (* ---------------------------------------------------- address calculation *) lemma absolute_bit_address_valid : forall base offset : int. 0 <= base -> 0 <= offset -> absolute_bit_address base offset >= 0 lemma word_index_positive : forall bit_addr : int. is_valid_bit_address bit_addr -> 0 <= word_index bit_addr < max_address lemma bit_index_in_range : forall bit_addr : int. 0 <= bit_index_in_word bit_addr < word_bits lemma euclidean_division : forall bit_addr : int. bit_addr = word_index bit_addr * word_bits + bit_index_in_word bit_addr lemma word_and_bit_determine_address : forall a1 a2 : int. word_index a1 = word_index a2 -> bit_index_in_word a1 = bit_index_in_word a2 -> a1 = a2 (* --------------------------------------------------------------- boundaries *) lemma bit_0_maps_to_word_0 : forall base : int. word_index (absolute_bit_address base 0) = div base 8 lemma bit_63_same_word : forall base : int. mod base 8 = 0 -> word_index (absolute_bit_address base 0) = word_index (absolute_bit_address base 63) lemma bit_64_next_word : forall base : int. word_index (absolute_bit_address base 64) = word_index (absolute_bit_address base 0) + 1 lemma bit_index_wraps_at_64 : forall base : int. mod base 8 = 0 -> bit_index_in_word (absolute_bit_address base 63) = 63 /\ bit_index_in_word (absolute_bit_address base 64) = 0 lemma within_word_uniqueness : forall base offset1 offset2 : int. word_index (absolute_bit_address base offset1) = word_index (absolute_bit_address base offset2) -> bit_index_in_word (absolute_bit_address base offset1) = bit_index_in_word (absolute_bit_address base offset2) -> offset1 = offset2 (* -------------------------------------------------------- bit operations *) function bit_of (w b : int) : int = mod (div w (power 2 b)) 2 lemma bit_of_binary : forall w b : int. 0 <= b -> bit_of w b = 0 \/ bit_of w b = 1 predicate bit_get_correct (memory : int -> int) (base offset result : int) = let a = absolute_bit_address base offset in is_valid_bit_address a /\ result = bit_of (memory (word_index a)) (bit_index_in_word a) predicate frame (old_mem new_mem : int -> int) (w : int) = forall i : int. i <> w -> new_mem i = old_mem i predicate bit_set_correct (old_mem new_mem : int -> int) (base offset : int) = let a = absolute_bit_address base offset in is_valid_bit_address a /\ bit_of (new_mem (word_index a)) (bit_index_in_word a) = 1 /\ frame old_mem new_mem (word_index a) predicate bit_clear_correct (old_mem new_mem : int -> int) (base offset : int) = let a = absolute_bit_address base offset in is_valid_bit_address a /\ bit_of (new_mem (word_index a)) (bit_index_in_word a) = 0 /\ frame old_mem new_mem (word_index a) predicate bit_toggle_correct (old_mem new_mem : int -> int) (base offset : int) = let a = absolute_bit_address base offset in is_valid_bit_address a /\ bit_of (new_mem (word_index a)) (bit_index_in_word a) = 1 - bit_of (old_mem (word_index a)) (bit_index_in_word a) /\ frame old_mem new_mem (word_index a) lemma bit_get_binary : forall memory : int -> int, base offset result : int. bit_get_correct memory base offset result -> result = 0 \/ result = 1 let lemma bit_get_deterministic (memory : int -> int) (base offset r1 r2 : int) requires { bit_get_correct memory base offset r1 } requires { bit_get_correct memory base offset r2 } ensures { r1 = r2 } = let a = absolute_bit_address base offset in assert { r1 = bit_of (memory (word_index a)) (bit_index_in_word a) = r2 } (* A SET to one word does not change a GET from a different word. *) let lemma disjoint_words_independent (old_mem new_mem : int -> int) (base1 offset1 base2 offset2 r : int) requires { word_index (absolute_bit_address base1 offset1) <> word_index (absolute_bit_address base2 offset2) } requires { bit_set_correct old_mem new_mem base1 offset1 } requires { bit_get_correct new_mem base2 offset2 r } ensures { bit_get_correct old_mem base2 offset2 r } = let a2 = absolute_bit_address base2 offset2 in assert { new_mem (word_index a2) = old_mem (word_index a2) } (* After SET / CLEAR, GET of the same bit returns 1 / 0. *) lemma get_after_set : forall old_mem new_mem : int -> int, base offset : int. bit_set_correct old_mem new_mem base offset -> bit_get_correct new_mem base offset 1 lemma get_after_clear : forall old_mem new_mem : int -> int, base offset : int. bit_clear_correct old_mem new_mem base offset -> bit_get_correct new_mem base offset 0 end