October 2026 main drop: mirror from GitHub

0ba037b verified 16 days ago

4.27 kB

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

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