rust-opencl-gpu / bit_accelerator /formal /bit_addressing_proofs.mlw

October 2026 main drop: mirror from GitHub

a8baeed verified 14 days ago

2.05 kB

(* Derived properties of BitAddressing, proved from the definitions in
   bit_addressing.mlw (run with `why3 prove -L formal ...`). *)

module BitAddressingProofs

  use int.Int
  use int.EuclideanDivision
  use bit_addressing.BitAddressing

  (* Every valid bit address has a valid word and an in-range bit index. *)
  lemma valid_address_decomposes :
    forall a : int. is_valid_bit_address a ->
      0 <= word_index a < max_address /\ 0 <= bit_index_in_word a < 64 /\
      a = word_index a * 64 + bit_index_in_word a

  (* The 64 offsets from a word-aligned base cover exactly one word, in order. *)
  lemma aligned_base_covers_one_word :
    forall base k : int. mod base 8 = 0 -> 0 <= k < 64 ->
      word_index (absolute_bit_address base k) = div base 8 /\
      bit_index_in_word (absolute_bit_address base k) = k

  (* Offset k + 64 reaches the same bit of the next word. *)
  lemma offset_plus_64 :
    forall base k : int.
      word_index (absolute_bit_address base (k + 64)) =
        word_index (absolute_bit_address base k) + 1 /\
      bit_index_in_word (absolute_bit_address base (k + 64)) =
        bit_index_in_word (absolute_bit_address base k)

  (* Offsets are interchangeable with base bytes: 8 bits per byte. *)
  lemma byte_offset_equivalence :
    forall base offset : int.
      absolute_bit_address (base + 1) offset = absolute_bit_address base (offset + 8)

  (* A CLEAR to one word does not change a GET from a different word. *)
  let lemma clear_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_clear_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) }
end

	(* Derived properties of BitAddressing, proved from the definitions in
	bit_addressing.mlw (run with `why3 prove -L formal ...`). *)

	module BitAddressingProofs

	use int.Int
	use int.EuclideanDivision
	use bit_addressing.BitAddressing

	(* Every valid bit address has a valid word and an in-range bit index. *)
	lemma valid_address_decomposes :
	forall a : int. is_valid_bit_address a ->
	0 <= word_index a < max_address /\ 0 <= bit_index_in_word a < 64 /\
	a = word_index a * 64 + bit_index_in_word a

	(* The 64 offsets from a word-aligned base cover exactly one word, in order. *)
	lemma aligned_base_covers_one_word :
	forall base k : int. mod base 8 = 0 -> 0 <= k < 64 ->
	word_index (absolute_bit_address base k) = div base 8 /\
	bit_index_in_word (absolute_bit_address base k) = k

	(* Offset k + 64 reaches the same bit of the next word. *)
	lemma offset_plus_64 :
	forall base k : int.
	word_index (absolute_bit_address base (k + 64)) =
	word_index (absolute_bit_address base k) + 1 /\
	bit_index_in_word (absolute_bit_address base (k + 64)) =
	bit_index_in_word (absolute_bit_address base k)

	(* Offsets are interchangeable with base bytes: 8 bits per byte. *)
	lemma byte_offset_equivalence :
	forall base offset : int.
	absolute_bit_address (base + 1) offset = absolute_bit_address base (offset + 8)

	(* A CLEAR to one word does not change a GET from a different word. *)
	let lemma clear_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_clear_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) }
	end