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
|
theory eggman imports Main begin
type_synonym bit = "bool"
abbreviation B0 where "B0 == False"
abbreviation B1 where "B1 == True"
(* Note that all bitvectors are stored in LSB-first order *)
fun binary_to_nat :: "bit list \<Rightarrow> nat"
where
"binary_to_nat [] = 0"
| "binary_to_nat (b # l) = (if b then 1 else 0) + 2 * binary_to_nat l"
fun nat_to_binary :: "nat \<Rightarrow> bit list"
where
"nat_to_binary n =
(if n = 0 then [] else (if even n then B0 else B1) # nat_to_binary (n div 2))"
(* Remove any leading zeroes. Note that the bitvector for 0 is the empty list. *)
fun trim :: "bit list \<Rightarrow> bit list"
where
"trim [] = []"
| "trim (B0 # l) = (if trim l = [] then [] else B0 # trim l)"
| "trim (B1 # l) = B1 # trim l"
value "trim [B0,B1,B0,B0]"
value "trim [B1,B0,B1,B0,B1]"
value "trim [B1,B0,B1,B0,B0,B0]"
lemma binary_to_nat_trim:
"binary_to_nat (trim l) = binary_to_nat l"
by (induct l, auto)
lemma nat_to_binary_inv: "nat_to_binary (binary_to_nat l) = trim l"
proof (induct l)
case Nil
thus ?case by auto
next
case (Cons b l)
hence *: "nat_to_binary (binary_to_nat l) = trim l" by auto
thus ?case
proof (cases b)
case True
have "nat_to_binary (1 + 2 * binary_to_nat l) = trim (B1 # l)" using * by auto
with True show ?thesis by auto
next
case False
have "nat_to_binary (2 * binary_to_nat l) = trim (B0 # l)" using *
by (smt (z3) binary_to_nat.simps(1) binary_to_nat_trim dvd_triv_left
mult_0_right nat_to_binary.simps nonzero_mult_div_cancel_left
trim.simps(2) zero_neq_numeral)
with False show ?thesis by auto
qed
qed
lemma binary_to_nat_inv: "binary_to_nat (nat_to_binary n) = n"
proof - (* using complete induction *)
have "\<forall>m. m < n \<longrightarrow> binary_to_nat (nat_to_binary m) = m" by (induct n, auto)
thus ?thesis by simp
qed
(* Addition on two bitvectors is just defined "semantically" *)
definition bv_add :: "bit list \<Rightarrow> bit list \<Rightarrow> bit list" (infixr "+B" 51)
where
"l1 +B l2 = nat_to_binary (binary_to_nat l1 + binary_to_nat l2)"
fun zeroes :: "nat \<Rightarrow> bit list"
where
"zeroes 0 = []"
| "zeroes (Suc n) = B0 # zeroes n"
fun prefix :: "nat \<Rightarrow> bit list \<Rightarrow> bit list"
where
"prefix n [] = []"
| "prefix n (x # xs) = (if n = 0 then [] else x # prefix (n - 1) xs)"
value "prefix 3 [B0,B0,B1,B0,B1]"
value "prefix 4 [B0,B0,B1,B1]"
value "prefix 5 [B0,B0,B1]"
(* Forces a bitvector to have a given width, either by
trimming MSBs or by adding leading zeroes *)
definition setwidth :: "nat \<Rightarrow> bit list \<Rightarrow> bit list" ("\<^sub>_ _" [51, 52] 52)
where
"\<^sub>n l = prefix n (l @ zeroes (n - length l))"
value "\<^sub>4 [B0,B1,B0]"
value "\<^sub>3 [B0,B1,B0]"
value "\<^sub>2 [B0,B1,B0]"
(* A simple "add associativity" lemma (without bitwidths) *)
lemma bv_add_assoc_simple:
"(a +B b) +B c = a +B (b +B c)"
by (metis add.assoc binary_to_nat_inv bv_add_def)
(* Now incorporating bitwidths. Trying to see if Sam's sideconditions
are necessary. The counterexample indicates that they're not. *)
lemma bv_add_assoc_necessary:
assumes "\<^sub>t (\<^sub>u (\<^sub>p a +B \<^sub>r b) +B \<^sub>s c) = \<^sub>t (\<^sub>p a +B \<^sub>q (\<^sub>r b +B \<^sub>s c))"
and "a \<noteq> []" and "b \<noteq> []" and "c \<noteq> []"
and "p > 0" and "q > 0" and "r > 0" and "s > 0" and "t > 0"
shows "(q \<ge> t \<or> r + s \<le> q) \<and> (u \<ge> t \<or> p + r \<le> u)"
try
(*
Nitpick found a counterexample:
a = [B0, B0]
b = [B0, B0]
c = [B0]
p = 1
q = 2
r = 1
s = 2
t = 2
u = 1
*)
oops
end
|
