Hugging Face's logo

Snapkitty
/
bit-string-accelerator

snapkitty
october-2026-drop
systemverilog
rtl
fpga
asic
formal-verification
hardware
Model card Files
xet
 Community
bit-string-accelerator
File size: 6,234 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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
(* 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