Theory DS_Reversible_Assignment
section ‹Reversible Assignment›
theory DS_Reversible_Assignment
imports DS_Unsigned_Literal Relaxed_Assignment
begin
definition [llvm_inline]: "snat_even_impl w ≡ doM {
b ← ll_and w (signed_nat 0x1);
ll_icmp_eq b (signed_nat 0)
}"
lemma snat_even_rule[vcg_rules]: "htriple (↿snat.assn n ni) (snat_even_impl ni) (λri. EXS r. ↿bool.assn r ri ** ↑(r = even n))"
unfolding snat_even_impl_def
apply vcg_monadify
by vcg
text ‹Assignment with rollback›
subsection ‹Array of Boolean as Map›
definition "bla_α xs i ≡ if i<length xs then xs!i else False"
definition "bla_get_checked xs i ≡ if i<length xs then xs!i else False"
definition "bla_get_unchecked xs i ≡ mop_list_get xs i"
definition "bla_set_unchecked xs i v ≡ mop_list_set xs i v"
definition "bla_new_size csz i ≡ do {
ASSERT(csz ≤ i);
SPEC (λns. i<ns ∧ even ns)
}"
definition "bla_set_checked_aux xs i v ≡ do {
len ← mop_list_length xs;
ns ← bla_new_size len i;
ASSERT(len<ns);
let xs = op_list_grow_init False ns len xs;
mop_list_set xs i v
}"
definition "bla_set_checked xs i v ≡ do {
len ← mop_list_length xs;
if i<len then mop_list_set xs i v
else bla_set_checked_aux xs i v
}"
lemma bla_α_empty[simp]: "bla_α [] = (λ_. False)"
unfolding bla_α_def by auto
lemma bla_init_correct[simp]: "bla_α (replicate n False) = (λ_. False)"
unfolding bla_α_def by auto
lemma bla_get_checked_correct[simp]: "bla_get_checked xs i = bla_α xs i"
unfolding bla_α_def bla_get_checked_def by auto
lemma bla_get_unchecked_correct[refine_vcg]: "i<length xs ⟹ bla_get_unchecked xs i ≤ SPEC (λr. r=bla_α xs i)"
unfolding bla_α_def bla_get_unchecked_def by auto
lemma bla_set_unchecked_correct[refine_vcg]:
"i<length xs ⟹ bla_set_unchecked xs i v ≤ SPEC (λxs'. length xs'=length xs ∧ bla_α xs' = (bla_α xs)(i:=v))"
unfolding bla_α_def bla_set_unchecked_def
by (auto simp: fun_eq_iff)
lemma bla_set_checked_aux_correct[refine_vcg]:
"⟦even (length xs); length xs ≤ i⟧ ⟹ bla_set_checked_aux xs i v ≤ SPEC (λxs'.
length xs ≤ length xs'
∧ i<length xs'
∧ even (length xs')
∧ bla_α xs' = (bla_α xs)(i:=v))"
unfolding bla_set_checked_aux_def bla_new_size_def
apply refine_vcg
unfolding bla_α_def
by (auto simp: fun_eq_iff nth_append)
lemma bla_set_checked_correct[refine_vcg]:
"even (length xs) ⟹ bla_set_checked xs i v ≤ SPEC (λxs'.
length xs ≤ length xs'
∧ i<length xs'
∧ even (length xs')
∧ bla_α xs' = (bla_α xs)(i:=v))"
unfolding bla_set_checked_def
apply refine_vcg
unfolding bla_α_def
by (auto simp: fun_eq_iff)
subsection ‹Assignment›
text ‹The assignment contains the array, the trail, and a capacity bound that the trail is guaranteed to not exceed›
type_synonym rpan = "bool list × nat list × nat"
definition rpan_α :: "rpan ⇒ dimacs_var rp_ass" where "rpan_α ≡ λ(A,_,_). bla_α A o ulit_of"
definition rpan_cap :: "rpan ⇒ nat" where "rpan_cap ≡ λ(_,tr,bnd). bnd - length tr"
definition rpan_dom :: "rpan ⇒ dimacs_var set" where "rpan_dom ≡ λ(A,_,_). { var_of_lit (ulit_α l) | l. l<length A ∧ ulit_invar l }"
definition rpan_invar :: "rpan ⇒ bool" where
"rpan_invar ≡ λ(A,tr,bnd).
even (length A)
∧ {x. bla_α A x} ⊆ set tr
∧ length tr≤bnd
∧ set tr ⊆ {0..<length A}
"
definition rpan_make :: "bool list ⇒ nat list ⇒ nat ⇒ rpan" where [simp]: "rpan_make A tr bnd ≡ (A,tr,bnd)"
definition rpan_dest :: "rpan ⇒ _" where [simp]: "rpan_dest x ≡ x"
definition rpan_empty :: "nat ⇒ nat ⇒ rpan" where
"rpan_empty maxlit cap ≡ rpan_make (replicate ((ulit_maxlit_adjust maxlit) + 1) False) [] cap"
lemma rpan_empty_correct[simp]:
"rpan_invar (rpan_empty ml cap)"
"rpan_α (rpan_empty ml cap) = rpa_empty"
"rpan_cap (rpan_empty ml cap) = cap"
"rpan_dom (rpan_empty ml cap) = maxlit_vdom ml"
unfolding rpan_empty_def rpan_α_def rpan_cap_def rpan_dom_def rpan_invar_def
apply (clarsimp_all simp: comp_def simp del: replicate.simps)
apply (rule)
subgoal by (auto simp: in_maxlit_vdom_iff)
subgoal
unfolding maxlit_vdom_def
by (auto simp: ulit_maxlit_adjust_def)
done
definition rpan_is_true_checked :: "rpan ⇒ dimacs_var literal ⇒ bool" where "rpan_is_true_checked rp x ≡ let (A,_,_) = rpan_dest rp in bla_get_checked A (ulit_of x)"
definition rpan_is_true_unchecked :: "rpan ⇒ dimacs_var literal ⇒ bool nres" where "rpan_is_true_unchecked rp x ≡ let (A,_,_) = rpan_dest rp in bla_get_unchecked A (ulit_of x)"
abbreviation "rpan_is_false_checked A x ≡ rpan_is_true_checked A (neg_lit x)"
abbreviation "rpan_is_false_unchecked A x ≡ rpan_is_true_unchecked A (neg_lit x)"
lemma rpan_is_true_checked_refine[simp]: "rpan_is_true_checked A x = is_true (rpan_α A) x"
unfolding rpan_is_true_checked_def is_true_def rpan_α_def
by auto
lemma var_of_lit_eq_cases[consumes 1]:
assumes "var_of_lit l = var_of_lit l'"
obtains (eq) "l=l'" | (neg) "l = neg_lit l'"
using assms apply (cases l; cases l') by auto
lemma even_lit_bound_conv: "⟦even n; ulit_invar l; ulit_invar l'; ulit_α l = neg_lit (ulit_α l')⟧ ⟹ l'<n ⟷ l<n"
unfolding ulit_α_def ulit_invar_def
by (fastforce split: if_splits)
lemma rpan_is_true_unchecked_refine[refine_vcg]:
"⟦rpan_invar A; var_of_lit x∈rpan_dom A ⟧ ⟹ rpan_is_true_unchecked A x ≤ SPEC (λr. r= is_true (rpan_α A) x)"
unfolding rpan_is_true_unchecked_def
apply refine_vcg
unfolding rpan_invar_def rpan_α_def is_true_def rpan_dom_def
by (auto elim!: var_of_lit_eq_cases simp: even_lit_bound_conv)
definition rpan_set_checked :: "rpan ⇒ dimacs_var literal ⇒ rpan nres" where
"rpan_set_checked ≡ λrp l. do {
let (A,tr,bnd) = rpan_dest rp;
let l = ulit_of l;
A ← bla_set_checked A l True;
ASSERT (length tr < bnd);
tr ← mop_list_append tr l;
RETURN (rpan_make A tr bnd)}"
definition rpan_set_unchecked :: "rpan ⇒ dimacs_var literal ⇒ rpan nres" where
"rpan_set_unchecked ≡ λrp l. do {
let l = ulit_of l;
let (A,tr,bnd) = rpan_dest rp;
A ← bla_set_unchecked A l True;
ASSERT (length tr < bnd);
tr ← mop_list_append tr l;
RETURN (rpan_make A tr bnd)}"
lemma rpan_set_checked_correct[refine_vcg]:
assumes "rpan_invar A" "rpan_cap A ≠ 0"
shows
"rpan_set_checked A l ≤ SPEC (λr.
rpan_invar r
∧ rpan_α r = (rpan_α A)(l:=True)
∧ rpan_cap r = rpan_cap A - 1
∧ insert (var_of_lit (l)) (rpan_dom A) ⊆ rpan_dom r
)"
unfolding rpan_set_checked_def
apply refine_vcg
using assms unfolding rpan_invar_def rpan_α_def rpan_cap_def rpan_dom_def
by (auto simp: fun_eq_iff intro: exI[where x="ulit_of l"])
lemma rpan_set_unchecked_correct[refine_vcg]:
assumes "rpan_invar A" "rpan_cap A ≠ 0" "var_of_lit l ∈ rpan_dom A"
shows
"rpan_set_unchecked A l ≤ SPEC (λr.
rpan_invar r
∧ rpan_α r = (rpan_α A)(l:=True)
∧ rpan_cap r = rpan_cap A - 1
∧ rpan_dom r = rpan_dom A
)"
unfolding rpan_set_unchecked_def
apply refine_vcg
using assms unfolding rpan_invar_def rpan_α_def rpan_cap_def rpan_dom_def
by (auto simp: fun_eq_iff even_lit_bound_conv elim: var_of_lit_eq_cases)
definition rpan_clear :: "nat ⇒ rpan ⇒ rpan nres" where "rpan_clear cap rp ≡ do {
let (A,tr,_) = rpan_dest rp;
A ← nfoldli tr (λ_. True) (λl A. bla_set_unchecked A l False) A;
tr ← mop_emptied_list tr;
RETURN (rpan_make A tr cap)
}"
lemma rpan_clear_correct[refine_vcg]:
assumes "rpan_invar A⇩0"
shows "rpan_clear cap A⇩0 ≤ SPEC (λA.
rpan_invar A
∧ rpan_α A = rpa_empty
∧ rpan_cap A = cap
∧ rpan_dom A = rpan_dom A⇩0
)"
apply (cases A⇩0)
subgoal for bla⇩0 tr⇩0 bnd⇩0
using assms unfolding rpan_clear_def
apply (refine_vcg nfoldli_rule[where I="λ_ it A. {x. bla_α A x} ⊆ set it ∧ set it ⊆ {0..<length A} ∧ length A = length bla⇩0"])
by (auto simp: rpan_invar_def rpan_α_def rpan_cap_def rpan_dom_def)
done
definition bla_new_size_aux_impl :: "size_t word ⇒ lit_size_t word ⇒ size_t word llM"
where [llvm_inline]:
"bla_new_size_aux_impl n i ≡ doM {
max::lit_size_t word ← ll_max_unat;
max ← unat_snat_upcast size_T max;
max ← ll_add max (signed_nat 1);
ns ← ll_mul n (signed_nat 3);
ns ← ll_udiv n (signed_nat 2);
do_max ← ll_icmp_sle max ns;
llc_if do_max (doM {
Mreturn max
}) (doM {
ns'::size_t word ← unat_snat_upcast size_T i;
ns' ← ll_add ns' (signed_nat 1);
take_ns ← ll_icmp_sle ns' ns;
llc_if take_ns (Mreturn ns) (Mreturn ns')
})
}"
lemma bla_new_size_aux_impl_rule[vcg_rules]:
"llvm_htriple
(↿snat.assn n ni ** ↿unat.assn i ii ** ↑(n ≤ i))
(bla_new_size_aux_impl ni ii)
(λri. EXS r. ↿snat.assn r ri ** ↑(i<r ∧ r≤max_lit))"
unfolding bla_new_size_aux_impl_def
apply (vcg_monadify)
apply vcg'
apply clarsimp_all
unfolding max_snat_def max_unat_def
apply (simp_all add: is_up')
done
definition [llvm_inline]: "bla_new_size_impl n i ≡ doM {
ns ← bla_new_size_aux_impl n i;
b ← snat_even_impl ns;
llc_if b (Mreturn ns) (ll_add ns (signed_nat 1))
}"
sepref_register bla_new_size
lemma bla_new_size_impl_refine[sepref_fr_rules]:
"(uncurry bla_new_size_impl, uncurry bla_new_size)
∈ size_assn⇧k *⇩a lit_assn⇧k →⇩a size_assn"
proof -
show ?thesis
unfolding bla_new_size_def bla_new_size_impl_def
apply sepref_to_hoare
unfolding in_snat_rel_conv_assn in_unat_rel_conv_assn
supply [simp] = refine_pw_simps
apply vcg_monadify
apply vcg'
by (auto simp: max_unat_def max_snat_def)
qed
type_synonym blai = "(1 word, size_t)larray"
abbreviation bla_assn :: "bool list ⇒ blai ⇒ assn" where "bla_assn ≡ larray_assn' size_T bool1_assn"
sepref_register bla_get_checked bla_get_unchecked bla_set_unchecked bla_set_checked
sepref_def bla_get_checked_impl is "uncurry (RETURN oo bla_get_checked)" :: "bla_assn⇧k *⇩a lit_assn⇧k →⇩a bool1_assn"
unfolding bla_get_checked_def
apply (rewrite at "if ⌑ < _ then _ else _" annot_unat_snat_upcast[where 'l=size_t])
apply (rewrite at "_!⌑" annot_unat_snat_upcast[where 'l=size_t])
supply [simp] = is_up'
by sepref
lemma bla_get_unchecked_alt: "bla_get_unchecked xs i = mop_list_get xs (op_unat_snat_upcast TYPE(size_t) i)"
unfolding bla_get_unchecked_def by simp
lemma bla_set_unchecked_alt: "bla_set_unchecked xs i v = mop_list_set xs (op_unat_snat_upcast TYPE(size_t) i) v"
unfolding bla_set_unchecked_def by simp
sepref_def bla_get_unchecked_impl [llvm_inline] is "uncurry (bla_get_unchecked)" :: "bla_assn⇧k *⇩a lit_assn⇧k →⇩a bool1_assn"
unfolding bla_get_unchecked_alt
supply [simp] = is_up'
by sepref
sepref_def bla_set_unchecked_impl [llvm_inline] is "uncurry2 (bla_set_unchecked)" :: "bla_assn⇧d *⇩a lit_assn⇧k *⇩a bool1_assn⇧k →⇩a bla_assn"
unfolding bla_set_unchecked_alt
supply [simp] = is_up'
by sepref
sepref_def bla_set_checked_aux_impl is "uncurry2 (bla_set_checked_aux)" :: "bla_assn⇧d *⇩a lit_assn⇧k *⇩a bool1_assn⇧k →⇩a bla_assn"
unfolding bla_set_checked_aux_def
apply (rewrite at "mop_list_set _ ⌑" annot_unat_snat_upcast[where 'l=size_t])
supply [simp] = is_up'
by sepref
sepref_def bla_set_checked_impl [llvm_inline] is "uncurry2 (bla_set_checked)" :: "bla_assn⇧d *⇩a lit_assn⇧k *⇩a bool1_assn⇧k →⇩a bla_assn"
unfolding bla_set_checked_def
apply (rewrite at "if ⌑ < _ then _ else _" annot_unat_snat_upcast[where 'l=size_t])
apply (rewrite at "mop_list_set _ ⌑" annot_unat_snat_upcast[where 'l=size_t])
supply [simp] = is_up'
by sepref
term rpan_empty
term arl_assn
lemma rpan_empty_alt: "rpan_empty ml cap = do {
let ml = ulit_maxlit_adjust ml;
let n = op_unat_snat_upcast TYPE(size_t) ml;
let n=n+1;
rpan_make (replicate n False) [] cap
}"
unfolding rpan_empty_def
by (auto)
sepref_register rpan_make rpan_dest rpan_empty rpan_is_true_unchecked rpan_set_checked rpan_set_unchecked rpan_clear
type_synonym rpani = "blai × (lit_size_t word, size_t) array_list"
definition rpan_assn :: "rpan ⇒ rpani ⇒ assn"
where "rpan_assn ≡ λ(A,tr,bnd) (Ai,tri). bla_assn A Ai ** al_assn' size_T lit_assn tr tri ** dropi_assn (rdomp size_assn) bnd ghost_var"
definition rpan_make_impl :: "_ ⇒ _ ⇒ 'a ⇒ rpani llM"
where [llvm_inline]: "rpan_make_impl Ai tri _ ≡ Mreturn (Ai,tri)"
lemma rpan_make_impl_refine[sepref_fr_rules]:
"(uncurry2 rpan_make_impl,uncurry2 (RETURN ooo rpan_make))
∈ [λ_. True]⇩c bla_assn⇧d *⇩a (al_assn lit_assn)⇧d *⇩a size_assn⇧k → rpan_assn [λ((Ai,tri),_) r. r = (Ai,tri) ]⇩c"
unfolding rpan_make_def rpan_make_impl_def rpan_assn_def any_rel_def
apply sepref_to_hoare
apply vcg_normalize
apply (simp named_ss HOL_basic_ss_nomatch: move_resolve_ex_eq)
supply [simp] = rdomp_pure_rel_eq
apply vcg
done
lemma rpan_make_impl_refine2[sepref_fr_rules]:
"(uncurry2 rpan_make_impl,uncurry2 (RETURN ooo rpan_make))
∈ [λ_. True]⇩c bla_assn⇧d *⇩a (al_assn lit_assn)⇧d *⇩a (dropi_assn (rdomp size_assn))⇧k → rpan_assn [λ((Ai,tri),_) r. r = (Ai,tri) ]⇩c"
unfolding rpan_make_def rpan_make_impl_def rpan_assn_def any_rel_def
apply sepref_to_hoare
apply vcg_normalize
apply (simp named_ss HOL_basic_ss_nomatch: move_resolve_ex_eq)
by vcg
lemma rpan_dest_impl_refine[sepref_fr_rules]:
"(λ(a,b). Mreturn (a,b,ghost_var::1 word), RETURN o rpan_dest)
∈ [λ_. True]⇩c rpan_assn⇧d → bla_assn ×⇩a al_assn lit_assn ×⇩a dropi_assn (rdomp size_assn) [λ(Ai,tri) (Ai',tri',_). Ai'=Ai ∧ tri'=tri]⇩c"
unfolding rpan_dest_def rpan_assn_def any_rel_def
apply sepref_to_hoare
apply vcg_normalize
apply (simp named_ss HOL_basic_ss_nomatch: move_resolve_ex_eq)
by vcg
sepref_definition rpan_free [llvm_code] is "λA. doN {let _ = rpan_dest A; RETURN ()}" :: "rpan_assn⇧d →⇩a unit_assn"
by sepref
lemma rpan_free[sepref_frame_free_rules]: "MK_FREE rpan_assn rpan_free"
apply (rule MK_FREE_hfrefI[OF rpan_free.refine])
by auto
sepref_def rpan_empty_impl is "uncurry (RETURN oo rpan_empty)" :: "lit_assn⇧k *⇩a size_assn⇧k →⇩a rpan_assn"
unfolding rpan_empty_alt
apply (annot_snat_const size_T)
apply (subst al_fold_custom_empty[where 'l=size_t])
apply (subst larray.fold_replicate_init)
supply [simp] = is_up'
by sepref
lemma rpan_is_true_unchecked_alt: "rpan_is_true_unchecked rp x = do {
let (A,tr,bnd) = rpan_dest rp;
r ← bla_get_unchecked A (ulit_of x);
let rp' = rpan_make A tr bnd;
unborrow rp' rp;
RETURN r
}"
unfolding rpan_is_true_unchecked_def
by (auto simp: unborrow_def split: prod.split)
lemma rpan_is_true_checked_alt: "RETURN oo rpan_is_true_checked = (λrp x. do {
let (A,tr,bnd) = rpan_dest rp;
let r = bla_get_checked A (ulit_of x);
let rp' = rpan_make A tr bnd;
unborrow rp' rp;
RETURN r
})"
unfolding rpan_is_true_checked_def
by (auto simp: fun_eq_iff unborrow_def)
lemmas [sepref_opt_simps] = rpan_make_impl_def
sepref_def rpan_is_true_unchecked_impl [llvm_code,llvm_inline] is "uncurry rpan_is_true_unchecked" :: "rpan_assn⇧k *⇩a ulit_assn⇧k →⇩a bool1_assn"
unfolding rpan_is_true_unchecked_alt
by sepref
sepref_def rpan_is_true_checked_impl [llvm_code,llvm_inline] is "uncurry (RETURN oo rpan_is_true_checked)" :: "rpan_assn⇧k *⇩a ulit_assn⇧k →⇩a bool1_assn"
unfolding rpan_is_true_checked_alt
by sepref
sepref_def rpan_set_checked_impl [llvm_code,llvm_inline] is "uncurry rpan_set_checked" :: "rpan_assn⇧d *⇩a ulit_assn⇧k →⇩a rpan_assn"
unfolding rpan_set_checked_def
by sepref
sepref_def rpan_set_unchecked_impl [llvm_code,llvm_inline] is "uncurry rpan_set_unchecked" :: "rpan_assn⇧d *⇩a ulit_assn⇧k →⇩a rpan_assn"
unfolding rpan_set_unchecked_def
by sepref
sepref_def rpan_clear_impl is "uncurry rpan_clear" :: "size_assn⇧k *⇩a rpan_assn⇧d →⇩a rpan_assn"
unfolding rpan_clear_def
apply (subst nfoldli_by_idx)
apply (subst nfoldli_upt_by_while)
apply (annot_snat_const size_T)
by sepref
export_llvm
rpan_empty_impl
rpan_is_true_unchecked_impl
rpan_is_true_checked_impl
rpan_set_checked_impl
rpan_set_unchecked_impl
rpan_clear_impl
end