theory IsaSAT_Arena_LLVM
imports IsaSAT_Arena IsaSAT_Literals_LLVM
WB_More_Word
begin
section ‹Code Generation›
no_notation WB_More_Refinement.fref ("[_]⇩f _ → _" [0,60,60] 60)
no_notation WB_More_Refinement.freft ("_ →⇩f _" [60,60] 60)
lemma protected_bind_assoc: "Refine_Basic.bind$(Refine_Basic.bind$m$(λ⇩2x. f x))$(λ⇩2y. g y) = Refine_Basic.bind$m$(λ⇩2x. Refine_Basic.bind$(f x)$(λ⇩2y. g y))" by simp
lemma convert_swap: "WB_More_Refinement_List.swap = More_List.swap"
unfolding WB_More_Refinement_List.swap_def More_List.swap_def ..
subsubsection ‹Code Generation›
definition "arena_el_impl_rel ≡ unat_rel' TYPE(32) O arena_el_rel"
lemmas [fcomp_norm_unfold] = arena_el_impl_rel_def[symmetric]
abbreviation "arena_el_impl_assn ≡ pure arena_el_impl_rel"
paragraph ‹Arena Element Operations›
context
notes [simp] = arena_el_rel_def
notes [split] = arena_el.splits
notes [intro!] = frefI
begin
text ‹Literal›
lemma xarena_lit_refine1: "(λeli. eli, xarena_lit) ∈ [is_Lit]⇩f arena_el_rel → nat_lit_rel" by auto
sepref_def xarena_lit_impl [llvm_inline] is [] "RETURN o (λeli. eli)" :: "uint32_nat_assn⇧k →⇩a uint32_nat_assn" by sepref
lemmas [sepref_fr_rules] = xarena_lit_impl.refine[FCOMP xarena_lit_refine1]
lemma ALit_refine1: "(λx. x,ALit) ∈ nat_lit_rel → arena_el_rel" by auto
sepref_def ALit_impl [llvm_inline] is [] "RETURN o (λx. x)" :: "uint32_nat_assn⇧k →⇩a uint32_nat_assn" by sepref
lemmas [sepref_fr_rules] = ALit_impl.refine[FCOMP ALit_refine1]
text ‹LBD›
lemma xarena_lbd_refine1: "(λeli. eli, xarena_lbd) ∈ [is_LBD]⇩f arena_el_rel → nat_rel" by auto
sepref_def xarena_lbd_impl [llvm_inline] is [] "RETURN o (λeli. eli)" :: "uint32_nat_assn⇧k →⇩a uint32_nat_assn" by sepref
lemmas [sepref_fr_rules] = xarena_lbd_impl.refine[FCOMP xarena_lbd_refine1]
lemma ALBD_refine1: "(λeli. eli, ALBD) ∈ nat_rel → arena_el_rel" by auto
sepref_def xarena_ALBD_impl [llvm_inline] is [] "RETURN o (λeli. eli)" :: "uint32_nat_assn⇧k →⇩a uint32_nat_assn" by sepref
lemmas [sepref_fr_rules] = xarena_ALBD_impl.refine[FCOMP ALBD_refine1]
text ‹Activity›
lemma xarena_act_refine1: "(λeli. eli, xarena_act) ∈ [is_Act]⇩f arena_el_rel → nat_rel" by auto
sepref_def xarena_act_impl [llvm_inline] is [] "RETURN o (λeli. eli)" :: "uint32_nat_assn⇧k →⇩a uint32_nat_assn" by sepref
lemmas [sepref_fr_rules] = xarena_act_impl.refine[FCOMP xarena_act_refine1]
lemma AAct_refine1: "(λx. x,AActivity) ∈ nat_rel → arena_el_rel" by auto
sepref_def AAct_impl [llvm_inline] is [] "RETURN o (λx. x)" :: "uint32_nat_assn⇧k →⇩a uint32_nat_assn" by sepref
lemmas [sepref_fr_rules] = AAct_impl.refine[FCOMP AAct_refine1]
text ‹Size›
lemma xarena_length_refine1: "(λeli. eli, xarena_length) ∈ [is_Size]⇩f arena_el_rel → nat_rel" by auto
sepref_def xarena_len_impl [llvm_inline] is [] "RETURN o (λeli. eli)" :: "uint32_nat_assn⇧k →⇩a uint32_nat_assn" by sepref
lemmas [sepref_fr_rules] = xarena_len_impl.refine[FCOMP xarena_length_refine1]
lemma ASize_refine1: "(λx. x,ASize) ∈ nat_rel → arena_el_rel" by auto
sepref_def ASize_impl [llvm_inline] is [] "RETURN o (λx. x)" :: "uint32_nat_assn⇧k →⇩a uint32_nat_assn" by sepref
lemmas [sepref_fr_rules] = ASize_impl.refine[FCOMP ASize_refine1]
text ‹Position›
lemma xarena_pos_refine1: "(λeli. eli, xarena_pos) ∈ [is_Pos]⇩f arena_el_rel → nat_rel" by auto
sepref_def xarena_pos_impl [llvm_inline] is [] "RETURN o (λeli. eli)" :: "uint32_nat_assn⇧k →⇩a uint32_nat_assn" by sepref
lemmas [sepref_fr_rules] = xarena_pos_impl.refine[FCOMP xarena_pos_refine1]
lemma APos_refine1: "(λx. x,APos) ∈ nat_rel → arena_el_rel" by auto
sepref_def APos_impl [llvm_inline] is [] "RETURN o (λx. x)" :: "uint32_nat_assn⇧k →⇩a uint32_nat_assn" by sepref
lemmas [sepref_fr_rules] = APos_impl.refine[FCOMP APos_refine1]
text ‹Status›
definition "status_impl_rel ≡ unat_rel' TYPE(32) O status_rel"
lemmas [fcomp_norm_unfold] = status_impl_rel_def[symmetric]
abbreviation "status_impl_assn ≡ pure status_impl_rel"
lemma xarena_status_refine1: "(λeli. eli AND 0b11, xarena_status) ∈ [is_Status]⇩f arena_el_rel → status_rel" by (auto simp: is_Status_def)
sepref_def xarena_status_impl [llvm_inline] is [] "RETURN o (λeli. eli AND 0b11)" :: "uint32_nat_assn⇧k →⇩a uint32_nat_assn"
apply (annot_unat_const "TYPE(32)")
by sepref
lemmas [sepref_fr_rules] = xarena_status_impl.refine[FCOMP xarena_status_refine1]
lemma xarena_used_refine1: "(λeli. eli AND 0b100 ≠ 0, xarena_used) ∈ [is_Status]⇩f arena_el_rel → bool_rel"
by (auto simp: is_Status_def status_rel_def bitfield_rel_def)
sepref_def xarena_used_impl [llvm_inline] is [] "RETURN o (λeli. eli AND 0b100 ≠ 0)" :: "uint32_nat_assn⇧k →⇩a bool1_assn"
apply (annot_unat_const "TYPE(32)")
by sepref
lemmas [sepref_fr_rules] = xarena_used_impl.refine[FCOMP xarena_used_refine1]
lemma status_eq_refine1: "((=),(=)) ∈ status_rel → status_rel → bool_rel"
by (auto simp: status_rel_def)
sepref_def status_eq_impl [llvm_inline] is [] "uncurry (RETURN oo (=))"
:: "(unat_assn' TYPE(32))⇧k *⇩a (unat_assn' TYPE(32))⇧k →⇩a bool1_assn"
by sepref
lemmas [sepref_fr_rules] = status_eq_impl.refine[FCOMP status_eq_refine1]
definition "AStatus_impl1 cs used ≡ (cs AND unat_const TYPE(32) 0b11) + (if used then unat_const TYPE(32) 0b100 else unat_const TYPE(32) 0b0)"
lemma AStatus_refine1: "(AStatus_impl1, AStatus) ∈ status_rel → bool_rel → arena_el_rel"
by (auto simp: status_rel_def bitfield_rel_def AStatus_impl1_def split: if_splits)
sepref_def AStatus_impl [llvm_inline] is [] "uncurry (RETURN oo AStatus_impl1)" :: "uint32_nat_assn⇧k *⇩a bool1_assn⇧k →⇩a uint32_nat_assn"
unfolding AStatus_impl1_def
supply [split] = if_splits
by sepref
lemmas [sepref_fr_rules] = AStatus_impl.refine[FCOMP AStatus_refine1]
subsubsection ‹Arena Operations›
paragraph ‹Length›
abbreviation "arena_fast_assn ≡ al_assn' TYPE(64) arena_el_impl_assn"
lemma arena_lengthI:
assumes "arena_is_valid_clause_idx a b"
shows "Suc 0 ≤ b"
and "b < length a"
and "is_Size (a ! (b - Suc 0))"
using SIZE_SHIFT_def assms
by (auto simp: arena_is_valid_clause_idx_def arena_lifting)
lemma arena_length_alt:
‹arena_length arena i = (
let l = xarena_length (arena!(i - snat_const TYPE(64) 1))
in snat_const TYPE(64) 2 + op_unat_snat_upcast TYPE(64) l)›
by (simp add: arena_length_def SIZE_SHIFT_def)
sepref_register arena_length
sepref_def arena_length_impl
is "uncurry (RETURN oo arena_length)"
:: "[uncurry arena_is_valid_clause_idx]⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k → snat_assn' TYPE(64)"
unfolding arena_length_alt
supply [dest] = arena_lengthI
by sepref
paragraph ‹Literal at given position›
lemma arena_lit_implI:
assumes "arena_lit_pre a b"
shows "b < length a" "is_Lit (a ! b)"
using assms unfolding arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
by (fastforce dest: arena_lifting)+
sepref_register arena_lit xarena_lit
sepref_def arena_lit_impl
is "uncurry (RETURN oo arena_lit)"
:: "[uncurry arena_lit_pre]⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k → unat_lit_assn"
supply [intro] = arena_lit_implI
unfolding arena_lit_def
by sepref
sepref_register mop_arena_lit mop_arena_lit2
sepref_def mop_arena_lit_impl
is "uncurry (mop_arena_lit)"
:: "arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a unat_lit_assn"
supply [intro] = arena_lit_implI
unfolding mop_arena_lit_def
by sepref
sepref_def mop_arena_lit2_impl
is "uncurry2 (mop_arena_lit2)"
:: "[λ((N, _), _). length N ≤ sint64_max]⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k → unat_lit_assn"
supply [intro] = arena_lit_implI
supply [dest] = arena_lit_pre_le_lengthD
unfolding mop_arena_lit2_def
by sepref
paragraph ‹Status of the clause›
lemma arena_status_implI:
assumes "arena_is_valid_clause_vdom a b"
shows "4 ≤ b" "b - 4 < length a" "is_Status (a ! (b-4))"
using assms STATUS_SHIFT_def arena_dom_status_iff
unfolding arena_is_valid_clause_vdom_def
by (auto dest: valid_arena_in_vdom_le_arena)
sepref_register arena_status xarena_status
sepref_def arena_status_impl
is "uncurry (RETURN oo arena_status)"
:: "[uncurry arena_is_valid_clause_vdom]⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k → status_impl_assn"
supply [intro] = arena_status_implI
unfolding arena_status_def STATUS_SHIFT_def
apply (annot_snat_const "TYPE(64)")
by sepref
paragraph ‹Swap literals›
sepref_register swap_lits
sepref_def swap_lits_impl is "uncurry3 (RETURN oooo swap_lits)"
:: "[λ(((C,i),j),arena). C + i < length arena ∧ C + j < length arena]⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a arena_fast_assn⇧d → arena_fast_assn"
unfolding swap_lits_def convert_swap
unfolding gen_swap
by sepref
paragraph ‹Get LBD›
lemma get_clause_LBD_preI:
assumes "get_clause_LBD_pre a b"
shows "2 ≤ b"
and "b < length a"
and "is_LBD (a ! (b - 2))"
using LBD_SHIFT_def assms
by (auto simp: get_clause_LBD_pre_def arena_is_valid_clause_idx_def arena_lifting)
sepref_register arena_lbd
sepref_def arena_lbd_impl
is "uncurry (RETURN oo arena_lbd)"
:: "[uncurry get_clause_LBD_pre]⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k →uint32_nat_assn"
unfolding arena_lbd_def LBD_SHIFT_def
supply [dest] = get_clause_LBD_preI
apply (annot_snat_const "TYPE(64)")
by sepref
paragraph ‹Get Saved Position›
lemma arena_posI:
assumes "get_saved_pos_pre a b"
shows "5 ≤ b"
and "b < length a"
and "is_Pos (a ! (b - 5))"
using POS_SHIFT_def assms is_short_clause_def[of ‹_ ∝ b›]
apply (auto simp: get_saved_pos_pre_def arena_is_valid_clause_idx_def arena_lifting
MAX_LENGTH_SHORT_CLAUSE_def[symmetric] simp del: MAX_LENGTH_SHORT_CLAUSE_def)
using arena_lifting(1) arena_lifting(4) header_size_def apply fastforce
done
lemma arena_pos_alt:
‹arena_pos arena i = (
let l = xarena_pos (arena!(i - snat_const TYPE(64) 5))
in snat_const TYPE(64) 2 + op_unat_snat_upcast TYPE(64) l)›
by (simp add: arena_pos_def POS_SHIFT_def)
sepref_register arena_pos
sepref_def arena_pos_impl
is "uncurry (RETURN oo arena_pos)"
:: "[uncurry get_saved_pos_pre]⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k → snat_assn' TYPE(64)"
unfolding arena_pos_alt
supply [dest] = arena_posI
by sepref
paragraph ‹Update LBD›
lemma update_lbdI:
assumes "update_lbd_pre ((b, lbd), a)"
shows "2 ≤ b"
and "b -2 < length a"
using LBD_SHIFT_def assms
apply (auto simp: arena_is_valid_clause_idx_def arena_lifting update_lbd_pre_def
dest: arena_lifting(10))
by (simp add: less_imp_diff_less valid_arena_def)
sepref_register update_lbd
sepref_def update_lbd_impl
is "uncurry2 (RETURN ooo update_lbd)"
:: "[update_lbd_pre]⇩a sint64_nat_assn⇧k *⇩a uint32_nat_assn⇧k *⇩a arena_fast_assn⇧d → arena_fast_assn"
unfolding update_lbd_def LBD_SHIFT_def
supply [simp] = update_lbdI
and [dest] = arena_posI
apply (annot_snat_const "TYPE(64)")
by sepref
paragraph ‹Update Saved Position›
lemma update_posI:
assumes "isa_update_pos_pre ((b, pos), a)"
shows "5 ≤ b" "2 ≤ pos" "b-5 < length a"
using assms POS_SHIFT_def
unfolding isa_update_pos_pre_def
apply (auto simp: arena_is_valid_clause_idx_def arena_lifting)
apply (metis (full_types) MAX_LENGTH_SHORT_CLAUSE_def arena_is_valid_clause_idx_def arena_posI(1) get_saved_pos_pre_def)
by (simp add: less_imp_diff_less valid_arena_def)
lemma update_posI2:
assumes "isa_update_pos_pre ((b, pos), a)"
assumes "rdomp (al_assn arena_el_impl_assn :: _ ⇒ (32 word, 64) array_list ⇒ assn) a"
shows "pos - 2 < max_unat 32"
proof -
obtain N vdom where
‹valid_arena a N vdom› and
‹b ∈# dom_m N›
using assms(1) unfolding isa_update_pos_pre_def arena_is_valid_clause_idx_def
by auto
then have eq: ‹length (N ∝ b) = arena_length a b› and
le: ‹b < length a› and
size: ‹is_Size (a ! (b - SIZE_SHIFT))›
by (auto simp: arena_lifting)
have ‹i<length a ⟹ rdomp arena_el_impl_assn (a ! i)› for i
using rdomp_al_dest'[OF assms(2)]
by auto
from this[of ‹b - SIZE_SHIFT›] have ‹rdomp arena_el_impl_assn (a ! (b - SIZE_SHIFT))›
using le by auto
then have ‹length (N ∝ b) ≤ uint32_max + 2›
using size eq unfolding rdomp_pure
apply (auto simp: rdomp_def arena_el_impl_rel_def is_Size_def
comp_def pure_def unat_rel_def unat.rel_def br_def
arena_length_def uint32_max_def)
subgoal for x
using unat_lt_max_unat[of x]
apply (auto simp: max_unat_def)
done
done
then show ?thesis
using assms POS_SHIFT_def
unfolding isa_update_pos_pre_def
by (auto simp: arena_is_valid_clause_idx_def arena_lifting eq
uint32_max_def max_unat_def)
qed
sepref_register arena_update_pos
sepref_def update_pos_impl
is "uncurry2 (RETURN ooo arena_update_pos)"
:: "[isa_update_pos_pre]⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a arena_fast_assn⇧d → arena_fast_assn"
unfolding arena_update_pos_def POS_SHIFT_def
apply (annot_snat_const "TYPE(64)")
apply (rewrite at "APos ⌑" annot_snat_unat_downcast[where 'l=32])
supply [simp] = update_posI and [dest] = update_posI2
by sepref
sepref_register IRRED LEARNED DELETED
lemma IRRED_impl[sepref_import_param]: "(0,IRRED) ∈ status_impl_rel"
unfolding status_impl_rel_def status_rel_def unat_rel_def unat.rel_def
by (auto simp: in_br_conv)
lemma LEARNED_impl[sepref_import_param]: "(1,LEARNED) ∈ status_impl_rel"
unfolding status_impl_rel_def status_rel_def unat_rel_def unat.rel_def
by (auto simp: in_br_conv)
lemma DELETED_impl[sepref_import_param]: "(3,DELETED) ∈ status_impl_rel"
unfolding status_impl_rel_def status_rel_def unat_rel_def unat.rel_def
by (auto simp: in_br_conv)
lemma mark_garbageI:
assumes "mark_garbage_pre (a, b)"
shows "4 ≤ b" "b-4 < length a"
using assms STATUS_SHIFT_def
unfolding mark_garbage_pre_def
apply (auto simp: arena_is_valid_clause_idx_def arena_lifting)
apply (metis (full_types) arena_dom_status_iff(5) insertCI valid_arena_extra_information_mark_to_delete)
by (simp add: less_imp_diff_less valid_arena_def)
sepref_register extra_information_mark_to_delete
sepref_def mark_garbage_impl is "uncurry (RETURN oo extra_information_mark_to_delete)"
:: "[mark_garbage_pre]⇩a arena_fast_assn⇧d *⇩a sint64_nat_assn⇧k → arena_fast_assn"
unfolding extra_information_mark_to_delete_def STATUS_SHIFT_def
apply (annot_snat_const "TYPE(64)")
supply [simp] = mark_garbageI
by sepref
paragraph ‹Activity›
lemma arena_act_implI:
assumes "arena_act_pre a b"
shows "3 ≤ b" "b - 3 < length a" "is_Act (a ! (b-3))"
using assms ACTIVITY_SHIFT_def
apply (auto simp: arena_act_pre_def arena_is_valid_clause_idx_def arena_lifting)
by (simp add: less_imp_diff_less valid_arena_def)
sepref_register arena_act
sepref_def arena_act_impl
is "uncurry (RETURN oo arena_act)"
:: "[uncurry arena_act_pre]⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k → uint32_nat_assn"
supply [intro] = arena_act_implI
unfolding arena_act_def ACTIVITY_SHIFT_def
apply (annot_snat_const "TYPE(64)")
by sepref
paragraph ‹Increment Activity›
context begin
interpretation llvm_prim_arith_setup .
sepref_register op_incr_mod32
lemma op_incr_mod32_hnr[sepref_fr_rules]:
"(λx. ll_add x 1, RETURN o op_incr_mod32) ∈ uint32_nat_assn⇧k →⇩a uint32_nat_assn"
unfolding unat_rel_def unat.rel_def
apply sepref_to_hoare
apply (simp add: in_br_conv)
apply vcg'
unfolding op_incr_mod32_def
by (simp add: unat_word_ariths)
end
sepref_register arena_incr_act
sepref_def arena_incr_act_impl is "uncurry (RETURN oo arena_incr_act)"
:: "[uncurry arena_act_pre]⇩a arena_fast_assn⇧d *⇩a sint64_nat_assn⇧k → arena_fast_assn"
unfolding arena_incr_act_def ACTIVITY_SHIFT_def
supply [intro] = arena_act_implI
apply (annot_snat_const "TYPE(64)")
by sepref
sepref_register arena_decr_act
sepref_def arena_decr_act_impl is "uncurry (RETURN oo arena_decr_act)"
:: "[uncurry arena_act_pre]⇩a arena_fast_assn⇧d *⇩a sint64_nat_assn⇧k → arena_fast_assn"
unfolding arena_decr_act_def ACTIVITY_SHIFT_def
supply [intro] = arena_act_implI
apply (rewrite at "_ div ⌑" unat_const_fold[where 'a=32])
apply (annot_snat_const "TYPE(64)")
by sepref
paragraph ‹Mark used›
term mark_used
lemma arena_mark_used_implI:
assumes "arena_act_pre a b"
shows "4 ≤ b" "b - 4 < length a" "is_Status (a ! (b-4))"
using assms STATUS_SHIFT_def
apply (auto simp: arena_act_pre_def arena_is_valid_clause_idx_def arena_lifting)
subgoal by (metis (full_types) arena_is_valid_clause_vdom_def arena_status_implI(1) insertCI valid_arena_extra_information_mark_to_delete)
subgoal by (simp add: less_imp_diff_less valid_arena_def)
done
sepref_register mark_used
sepref_def mark_used_impl is "uncurry (RETURN oo mark_used)"
:: "[uncurry arena_act_pre]⇩a arena_fast_assn⇧d *⇩a sint64_nat_assn⇧k → arena_fast_assn"
unfolding mark_used_def STATUS_SHIFT_def
supply [intro] = arena_mark_used_implI
apply (annot_snat_const "TYPE(64)")
by sepref
sepref_register mark_unused
sepref_def mark_unused_impl is "uncurry (RETURN oo mark_unused)"
:: "[uncurry arena_act_pre]⇩a arena_fast_assn⇧d *⇩a sint64_nat_assn⇧k → arena_fast_assn"
unfolding mark_unused_def STATUS_SHIFT_def
supply [intro] = arena_mark_used_implI
apply (annot_snat_const "TYPE(64)")
by sepref
paragraph ‹Marked as used?›
lemma arena_marked_as_used_implI:
assumes "marked_as_used_pre a b"
shows "4 ≤ b" "b - 4 < length a" "is_Status (a ! (b-4))"
using assms STATUS_SHIFT_def
apply (auto simp: marked_as_used_pre_def arena_is_valid_clause_idx_def arena_lifting)
subgoal by (metis (full_types) arena_is_valid_clause_vdom_def arena_status_implI(1) insertCI valid_arena_extra_information_mark_to_delete)
subgoal by (simp add: less_imp_diff_less valid_arena_def)
done
sepref_register marked_as_used
sepref_def marked_as_used_impl
is "uncurry (RETURN oo marked_as_used)"
:: "[uncurry marked_as_used_pre]⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k → bool1_assn"
supply [intro] = arena_marked_as_used_implI
unfolding marked_as_used_def STATUS_SHIFT_def
apply (annot_snat_const "TYPE(64)")
by sepref
sepref_register MAX_LENGTH_SHORT_CLAUSE
sepref_def MAX_LENGTH_SHORT_CLAUSE_impl is "uncurry0 (RETURN MAX_LENGTH_SHORT_CLAUSE)" :: "unit_assn⇧k →⇩a sint64_nat_assn"
unfolding MAX_LENGTH_SHORT_CLAUSE_def
apply (annot_snat_const "TYPE(64)")
by sepref
definition arena_other_watched_as_swap :: ‹nat list ⇒ nat ⇒ nat ⇒ nat ⇒ nat nres› where
‹arena_other_watched_as_swap S L C i = do {
ASSERT(i < 2 ∧
C + i < length S ∧
C < length S ∧
(C + 1) < length S);
K ← RETURN (S ! C);
K' ← RETURN (S ! (1 + C));
RETURN (L XOR K XOR K')
}›
lemma arena_other_watched_as_swap_arena_other_watched:
assumes
N: ‹(N, N') ∈ ⟨arena_el_rel⟩list_rel› and
L: ‹(L, L') ∈ nat_lit_rel› and
C: ‹(C, C') ∈ nat_rel› and
i: ‹(i, i') ∈ nat_rel›
shows
‹arena_other_watched_as_swap N L C i ≤ ⇓nat_lit_rel
(arena_other_watched N' L' C' i')›
proof -
have eq: ‹i =i'› ‹C=C'›
using assms by auto
have A: ‹Pos (L div 2) = A ⟹ even L ⟹ L = 2 * atm_of A› for A :: ‹nat literal›
by (cases A)
auto
have Ci: ‹(C' + i', C' + i') ∈ nat_rel›
unfolding eq by auto
have [simp]: ‹L = N ! (C+i)› if ‹L' = arena_lit N' (C' + i')› ‹C' + i' < length N'›
‹arena_lit_pre2 N' C i›
using that param_nth[OF that(2) Ci N] C i L
unfolding arena_lit_pre2_def
apply - apply normalize_goal+
subgoal for N'' vdom
using arena_lifting(6)[of N' N'' vdom C i] A[of ‹arena_lit N' (C' + i')›]
apply (simp only: list_rel_imp_same_length[of N] eq)
apply (cases ‹N' ! (C' + i')›; cases ‹arena_lit N' (C' + i')›)
apply (simp_all add: eq nat_lit_rel_def br_def)
apply (auto split: if_splits simp: eq_commute[of _ ‹Pos (L div 2)›]
eq_commute[of _ ‹ALit (Pos (_ div 2))›] arena_lit_def)
using div2_even_ext_nat by blast
done
have [simp]: ‹N ! (C' + i') XOR N ! C' XOR N ! Suc C' = N ! (C' + (Suc 0 - i))› if ‹i < 2›
using that i
by (cases i; cases ‹i-1›)
(auto simp: bin_pos_same_XOR3_nat)
have Ci': ‹(C' + (1 - i'), C' + (1 - i')) ∈ nat_rel›
unfolding eq by auto
have [intro!]: ‹(N ! (Suc C' - i'), arena_lit N' (Suc C' - i')) ∈ nat_lit_rel›
if ‹arena_lit_pre2 N' C i› ‹i < 2›
using that param_nth[OF _ Ci' N]
unfolding arena_lit_pre2_def
apply - apply normalize_goal+
apply (subgoal_tac ‹C' + (Suc 0 - i') < length N'›)
defer
subgoal for N'' vdom
using
arena_lifting(7)[of N' N'' vdom C i]
apply (auto simp: arena_lit_pre2_def list_rel_imp_same_length[of N]
simp del: arena_el_rel_def)
by (metis add.right_neutral add_Suc add_diff_cancel_left' arena_lifting(22) arena_lifting(4) arena_lifting(7) eq(1) eq(2) less_2_cases less_Suc_eq not_less_eq plus_1_eq_Suc)
apply (subgoal_tac ‹(Suc 0 - i') < length (x ∝ C)›)
defer
subgoal for N'' vdom
using
arena_lifting(7)[of N' N'' vdom C i]
by (auto simp: arena_lit_pre2_def list_rel_imp_same_length[of N]
arena_lifting(22) arena_lifting(4) less_imp_diff_less
simp del: arena_el_rel_def)
subgoal for N'' vdom
using
arena_lifting(6)[of N' N'' vdom C ‹Suc 0 - i›]
by (cases ‹N' ! (C' + (Suc 0 - i'))›)
(auto simp: arena_lit_pre2_def list_rel_imp_same_length[of N] eq
arena_lit_def arena_lifting)
done
show ?thesis
using assms
unfolding arena_other_watched_as_swap_def arena_other_watched_def
le_ASSERT_iff mop_arena_lit2_def
apply (refine_vcg)
apply (auto simp: le_ASSERT_iff list_rel_imp_same_length arena_lit_pre2_def
arena_lifting
bin_pos_same_XOR3_nat)
using arena_lifting(22) arena_lifting(4) arena_lifting(7) apply fastforce
using arena_lifting(22) arena_lifting(4) arena_lifting(7) arena_lit_pre2_def apply fastforce
done
qed
sepref_def arena_other_watched_as_swap_impl
is ‹uncurry3 arena_other_watched_as_swap›
:: ‹(al_assn' (TYPE(64)) uint32_nat_assn)⇧k *⇩a uint32_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a
sint64_nat_assn⇧k →⇩a uint32_nat_assn›
supply[[goals_limit=1]]
unfolding arena_other_watched_as_swap_def
apply (annot_snat_const "TYPE(64)")
by sepref
lemma arena_other_watched_as_swap_arena_other_watched':
‹(arena_other_watched_as_swap, arena_other_watched) ∈
⟨arena_el_rel⟩list_rel → nat_lit_rel → nat_rel → nat_rel →
⟨nat_lit_rel⟩nres_rel›
apply (intro fun_relI nres_relI)
using arena_other_watched_as_swap_arena_other_watched
by blast
lemma arena_fast_al_unat_assn:
‹hr_comp (al_assn unat_assn) (⟨arena_el_rel⟩list_rel) = arena_fast_assn›
unfolding al_assn_def hr_comp_assoc
by (auto simp: arena_el_impl_rel_def list_rel_compp)
lemmas [sepref_fr_rules] =
arena_other_watched_as_swap_impl.refine[FCOMP arena_other_watched_as_swap_arena_other_watched',
unfolded arena_fast_al_unat_assn]
end
sepref_def mop_arena_length_impl
is ‹uncurry mop_arena_length›
:: ‹arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a sint64_nat_assn›
unfolding mop_arena_length_def
by sepref
experiment begin
export_llvm
arena_length_impl
arena_lit_impl
arena_status_impl
swap_lits_impl
arena_lbd_impl
arena_pos_impl
update_lbd_impl
update_pos_impl
mark_garbage_impl
arena_act_impl
arena_incr_act_impl
arena_decr_act_impl
mark_used_impl
mark_unused_impl
marked_as_used_impl
MAX_LENGTH_SHORT_CLAUSE_impl
end
end