Theory LLVM_Examples
section ‹Examples›
theory LLVM_Examples
imports
"../ds/LLVM_DS_All"
"../ds/LLVM_DS_Array_List"
begin
text ‹Examples on top of Isabelle-LLVM basic layer.
For the verification of more complex algorithms, consider using
Isabelle-LLVM with the Refinement Framework, and the Sepref tool.
See, e.g., @{file Bin_Search.thy}.
›
subsection ‹Numeric Algorithms›
subsubsection ‹Exponentiation›
definition exp :: "'a::len word ⇒ 'b::len word llM" where [llvm_code]: "exp r ≡ doM {
a ← ll_const (unsigned 1);
(a,r) ← llc_while
(λ(a,r). doM { ll_icmp_ult (unsigned 0) r})
(λ(a,r). doM {
Mreturn (a*unsigned 2,r-unsigned 1)
})
(a,r);
Mreturn a
}"
abbreviation exp32::"32 word ⇒ 32 word llM" where "exp32 ≡ exp"
abbreviation exp64::"64 word ⇒ 64 word llM" where "exp64 ≡ exp"
export_llvm
exp32 is "uint32_t exp32 (uint32_t)"
exp64 is "uint64_t exp64 (uint64_t)"
file "code/exp.ll"
lemma exp_aux1:
assumes "2 ^ nat k < (N::int)" "t ≤ k" "0 < t"
shows "2 * 2 ^ nat (k - t) < N"
proof -
from assms have "nat (k - t) + 1 ≤ nat k" by auto
with assms have "(2::int) ^ (nat (k - t) + 1) ≤ 2 ^ nat k"
using one_le_numeral power_increasing by blast
thus ?thesis using assms by simp
qed
lemma exp_aux2: "⟦t ≤ k; 0 < t⟧ ⟹ nat (1+k-t) = Suc (nat (k-t))" by simp
lemma exp_correct:
assumes "LENGTH('b::len) ≥ 2"
shows "llvm_htriple
(↿uint.assn k (ki::'a::len word) ** ↑(2^nat k ∈ uints LENGTH('b)))
(exp ki)
(λr::'b word. ↿uint.assn (2^nat k) r ** ↿uint.assn k ki)"
unfolding exp_def
apply (rewrite annotate_llc_while[where
I="λ(ai,ri) t. EXS a r. ↿uint.assn a ai ** ↿uint.assn r ri ** ↑⇩d( 0≤r ∧ r≤k ∧ a = 2^nat (k-r) ) ** ↑⇩!(t = r)"
and R="measure nat"
])
apply vcg_monadify
apply (vcg'; (clarsimp simp: algebra_simps)?)
using assms
apply (simp_all add: exp_aux1 exp_aux2)
done
subsubsection ‹Euclid's Algorithm›
definition [llvm_code]: "euclid (a::'a::len word) b ≡ doM {
(a,b) ← llc_while
(λ(a,b) ⇒ ll_cmp (a ≠ b))
(λ(a,b) ⇒ if (a≤b) then Mreturn (a,b-a) else Mreturn (a-b,b))
(a,b);
Mreturn a
}"
export_llvm (debug)
"euclid :: 64 word ⇒ 64 word ⇒ 64 word llM" is "uint64_t euclid (uint64_t, uint64_t)"
file "code/euclid.ll"
lemma gcd_diff1': "gcd (a::int) (b-a) = gcd a b"
by (metis gcd.commute gcd_diff1)
lemma "llvm_htriple
(↿uint.assn a⇩0 ai ** ↿uint.assn b⇩0 bi ** ↑⇩d(0<a⇩0 ∧ 0<b⇩0))
(euclid ai bi)
(λri. ↿uint.assn (gcd a⇩0 b⇩0) ri)"
unfolding euclid_def
apply (rewrite annotate_llc_while[where
I="λ(ai,bi) t. EXS a b. ↿uint.assn a ai ** ↿uint.assn b bi
** ↑⇩a(t=a+b) ** ↑⇩d(0<a ∧ 0<b ∧ gcd a b = gcd a⇩0 b⇩0)"
and R="measure nat"
])
apply vcg_monadify
apply (vcg'; clarsimp?)
apply (simp_all add: gcd_diff1 gcd_diff1')
done
subsubsection ‹Fibonacci Numbers›
definition fib :: "'n::len word ⇒ 'n word llM" where [llvm_code]: "fib n ≡ REC (λfib' n.
if n≤unsigned 1 then Mreturn n
else doM {
n⇩1 ← fib' (n-unsigned 1);
n⇩2 ← fib' (n-unsigned 2);
Mreturn (n⇩1+n⇩2)
}) n"
abbreviation fib64 :: "64 word ⇒ 64 word llM" where "fib64 ≡ fib"
export_llvm thms: fib64
prepare_code_thms (LLVM) [code] fib_def
definition test :: "64 word ⇒ 64 word ⇒ _ llM"
where [llvm_code]: "test a b ≡ doM {
Mreturn (a,b)
}"
ML_val ‹
local open LLC_Preprocessor
val ctxt = @{context}
in
val thm = @{thm test_def}
|> cthm_inline ctxt
|> cthm_monadify ctxt
end
›
find_theorems llc_while
lemma "foo (test)"
unfolding test_def
apply (simp named_ss llvm_pre_simp:)
oops
export_llvm test
subsubsection ‹Distance between two Points (double)›
context begin
lemma plus_nan_double1[simp]:
"is_nan_double a ⟹ is_nan_double (a+b)"
apply transfer
unfolding plus_float_def fadd_def
by simp
lemma plus_nan_double2[simp]:
"is_nan_double b ⟹ is_nan_double (a+b)"
apply transfer
unfolding plus_float_def fadd_def
by simp
lemma [simp]: "is_nan_double ≠ bot"
using is_nan_double.abs_eq by force
lemma [simp]: "is_nan_single ≠ bot"
using is_nan_single.abs_eq by force
lemma pw_nan_double[pw_simp]:
"run ndet_nan_double s ≠ fail⇩n⇩e"
"is_res (run ndet_nan_double s) (x,i,s') ⟷ is_nan_double x ∧ i=0 ∧ s'=s"
unfolding ndet_nan_double_def
by pw+
lemma "doM {
a ← nanize_double a;
b ← nanize_double b;
nanize_double (a + b)
} = nanize_double (a + b)"
unfolding nanize_double_def
apply pw'
apply fastforce
done
definition ddist :: "double × double ⇒ double × double ⇒ double llM"
where [llvm_code]: "ddist p⇩1 p⇩2 ≡ doM {
let (x⇩1,y⇩1) = p⇩1;
let (x⇩2,y⇩2) = p⇩2;
dx ← nanize_double (x⇩1 - x⇩2);
dy ← nanize_double (y⇩1 - y⇩2);
dx2 ← nanize_double (dx*dx);
dy2 ← nanize_double (dy*dy);
dxy2 ← nanize_double (dx2+dy2);
nanize_double (dsqrt dxy2)
}"
export_llvm ddist
interpretation llvm_prim_arith_setup .
lemma "llvm_htriple □ (ddist p⇩1 p⇩2) (λ_. □)"
unfolding ddist_def
apply (simp split: prod.split add: Let_def)
unfolding nanize_double_def ndet_nan_double_def
apply vcg
done
definition fdist :: "single × single ⇒ single × single ⇒ single llM"
where [llvm_code]: "fdist p⇩1 p⇩2 ≡ doM {
let (x⇩1,y⇩1) = p⇩1;
let (x⇩2,y⇩2) = p⇩2;
dx ← nanize_single (x⇩1 - x⇩2);
dy ← nanize_single (y⇩1 - y⇩2);
dx2 ← nanize_single (dx*dx);
dy2 ← nanize_single (dy*dy);
dxy2 ← nanize_single (dx2+dy2);
nanize_single (ssqrt dxy2)
}"
export_llvm fdist
interpretation llvm_prim_arith_setup .
lemma "llvm_htriple □ (fdist p⇩1 p⇩2) (λ_. □)"
unfolding fdist_def
apply (simp split: prod.split add: Let_def)
unfolding nanize_single_def ndet_nan_single_def
apply vcg
done
end
subsection ‹Unions›
declare [[llc_compile_union=true]]