bit_accelerator/formal/bit_addressing.mlw

(* 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