Theory LRAT_Checker_Impl
section ‹Implementation of Checker›
theory LRAT_Checker_Impl
imports
SAT_Basic
Relaxed_Assignment
DS_Reversible_Assignment
DS_Clause_Database
Debugging_Tools
CNF_Parser_Impl
LRAT_Parsers
begin
subsection ‹Abstract Algorithms›
subsubsection ‹Checking for Unit or Tautology›
definition "check_uot_invar A ≡ λC⇩1 _ (ul,err). ¬err ⟶ (case ul of
None ⇒ rpa_is_conflict_clause A C⇩1
| Some l ⇒ rpa_is_uot_lit A C⇩1 l)"
lemma rpa_is_conflict_clause_empty[simp]: "rpa_is_conflict_clause A {}"
unfolding rpa_is_conflict_clause_def by auto
lemma rpa_is_conflict_clause_insert[simp]: "rpa_is_conflict_clause A (insert l C) ⟷ is_false A l ∧ rpa_is_conflict_clause A C"
unfolding rpa_is_conflict_clause_def by auto
lemma rpa_is_uot_lit_insert_false[simp]: "is_false A l' ⟹ rpa_is_uot_lit A (insert l' C) l ⟷ rpa_is_uot_lit A C l"
unfolding rpa_is_uot_lit_def by blast
lemma rpa_is_uot_lit_insert_nfalseI: "¬is_false A l ⟹ rpa_is_conflict_clause A C ⟹ rpa_is_uot_lit A (insert l C) l"
unfolding rpa_is_uot_lit_def rpa_is_conflict_clause_def by auto
text ‹First, we implement the loop. For technical reasons (we have to access an inner array),
we will use a locale, and here, only specify body and condition.
›
abbreviation (input) "err_code_mult_undecided ≡ 0x2"
abbreviation (input) "err_code_invalid_id ≡ 0x3"
definition "check_uot2_body A ≡ λl (ul,err). doN {
if⇩N rpan_is_false_unchecked A l then RETURN (ul,err)
else if is_None ul then RETURN (Some l,err)
else doN {
ERROR_lit err_code_mult_undecided l;
ERROR_lito err_code_mult_undecided ul;
RETURN (ul,True)
}
}"
definition [simp]: "check_uot2_cond _ _ = True"
text ‹Next, we use sepref to produce implementations of body and condition›
sepref_definition check_uot2_body_impl [llvm_inline] is "uncurry2 check_uot2_body" :: "rpan_assn⇧k *⇩a ulit_assn⇧k *⇩a (ulito_assn ×⇩a bool1_assn)⇧d →⇩a ulito_assn ×⇩a bool1_assn"
unfolding check_uot2_body_def
by sepref
sepref_definition check_uot2_cond_impl [llvm_inline] is "uncurry (RETURN oo check_uot2_cond)" :: "rpan_assn⇧k *⇩a (ulito_assn ×⇩a bool1_assn)⇧k →⇩a bool1_assn"
unfolding check_uot2_cond_def
by sepref
text ‹Finally, we instantiate the locale for the loop.›
interpretation uot: clause_iteration_setup check_uot2_cond_impl check_uot2_cond check_uot2_body_impl check_uot2_body rpan_assn "(ulito_assn ×⇩a bool1_assn)"
apply unfold_locales
apply (rule check_uot2_cond_impl.refine)
apply (rule check_uot2_body_impl.refine)
done
text ‹We prove the generated loop correct›
lemma uot_cdb_iterate_clause_correct[refine_vcg]:
assumes [simp]: "rpan_invar A"
assumes CIDV: "cdb cid = Some C"
assumes VB: "∀C∈ran cdb. var_of_lit`C ⊆ rpan_dom A"
shows "uot.cdb_iterate_clause cdb cid A (ulito_None,False) ≤ SPEC (λ(ul,err). ¬err ⟶
(case ul of
None ⇒ rpa_is_conflict_clause (rpan_α A) C
| Some l ⇒ rpa_is_uot_lit (rpan_α A) C l
)
)"
unfolding uot.cdb_iterate_clause_def check_uot2_cond_def check_uot2_body_def
apply (subst FOREACHcdi_def[where I="check_uot_invar (rpan_α A)", symmetric])
apply refine_vcg
unfolding check_uot_invar_def
using CIDV VB
by (auto split!: option.splits simp: rpa_is_uot_lit_insert_nfalseI ran_def)
text ‹And combine it with looking up the clause›
definition cdb_check_uot :: "rpan ⇒ cdb ⇒ nat ⇒ (dv_lit option × bool) nres"
where "cdb_check_uot A cdb cid ≡ do {
if⇩N cdb_contains cid cdb then do {
uot.cdb_iterate_clause cdb cid A (ulito_None,False)
} else doN {
ERROR_cid err_code_invalid_id cid;
RETURN (ulito_None,True)
}
}"
text ‹The following lemma shows a direct characterization of \<^const>‹cdb_check_uot› as presented in the paper›
lemma "cdb_check_uot A cdb cid = (
if cid ∈ dom cdb then doN {
let C = the (cdb cid);
ASSUME (finite C);
FOREACHcd C (λuv. True) (λl (ul, err). doN {
ASSERT (ulit_of (neg_lit l) < length (fst A));
if fst A ! ulit_of (neg_lit l) then RETURN (ul, err)
else if is_None ul then RETURN (Some l, err)
else RETURN (ul, True)
}) (None, False)
} else RETURN (None, True)
)"
proof -
have rpan_is_false_unchecked_alt: "rpan_is_false_unchecked A l = doN {
ASSERT (ulit_of (neg_lit l) < length (fst A));
RETURN (fst A ! ulit_of (neg_lit l))
}" for l
unfolding rpan_is_true_unchecked_def bla_get_unchecked_def
apply (cases A; simp)
done
show ?thesis
unfolding cdb_check_uot_def uot.cdb_iterate_clause_def check_uot2_cond_def check_uot2_body_def Let_def rpan_is_false_unchecked_alt
apply simp
apply (fo_rule cong | simp | intro ext impI conjI)+
done
qed
text ‹Correctness theorem for \<^const>‹cdb_check_uot›:›
lemma cdb_check_uot_correct:
assumes "rpan_invar A"
assumes "∀C∈ran cdb. var_of_lit`C ⊆ rpan_dom A"
shows "cdb_check_uot A cdb cid ≤ SPEC (λ(ul,err). ¬err ⟶
(∃C. cdb cid = Some C ∧ (case ul of
None ⇒ rpa_is_conflict_clause (rpan_α A) C
| Some l ⇒ rpa_is_uot_lit (rpan_α A) C l
))
)"
proof -
have aux: "cid∈dom cdb ⟹ cdb cid = Some (the (cdb cid))" by auto
show ?thesis
unfolding cdb_check_uot_def cdb_contains_def
apply refine_vcg
apply (rule assms)
apply (erule aux)
using assms
by (auto split: option.split)
qed
text ‹Actually, for our verification, we only need a weaker version that ignores
clause identifiers:›
lemma cdb_check_uot_correct_weak[refine_vcg]:
assumes "rpan_invar A"
assumes "∀C∈ran cdb. var_of_lit`C ⊆ rpan_dom A"
shows "cdb_check_uot A cdb cid ≤ SPEC (λ(ul,err). ¬err ⟶
(∃C∈ran cdb. (case ul of
None ⇒ rpa_is_conflict_clause (rpan_α A) C
| Some l ⇒ rpa_is_uot_lit (rpan_α A) C l
))
)"
apply (refine_vcg cdb_check_uot_correct)
using assms
by (auto 0 3 split: option.splits intro: ranI)
text ‹Finally, we use Sepref to generate an imperative implementation›
sepref_def cdb_check_uot_impl is "uncurry2 cdb_check_uot" :: "rpan_assn⇧k *⇩a cdb_assn⇧k *⇩a cid_assn⇧k →⇩a ulito_assn ×⇩a bool1_assn"
unfolding cdb_check_uot_def
by sepref
subsubsection ‹Checker States›
text ‹This is the first refinement of the abstract checker state \<^typ>‹'a checker_state›.
We split the state into three different types, depending on the represented abstract state.
Each checker state comes with an invariant, and an abstraction function
to map it the corresponding abstract checker state.
›
text ‹All checker state invariants share a common part, which we have factored out here:›
definition "cs_common_invar cap A cbld cdb ≡
rpan_invar A
∧ cbld_invar cbld ∧ cap ≤ cbld_α_cap cbld
∧ ulit_of`(⋃(ran cdb)) ⊆ {0..cbld_α_maxlit cbld}
∧ (∀C∈ran cdb. var_of_lit`C ⊆ rpan_dom A)
∧ (var_of_lit`cbld_α_clause cbld ⊆ rpan_dom A)
"
paragraph‹In Proof›
type_synonym checker_state_in_proof = "bool × bool × rpan × cbld × cdb"
definition cs_ip_invar :: "nat ⇒ checker_state_in_proof ⇒ bool" where
"cs_ip_invar cap ≡ λ(err,confl,A,cbld,cdb). cs_common_invar cap A cbld cdb ∧ (¬err ⟶ cap + 1 ≤ cbld_α_cap cbld) ∧ cap≤rpan_cap A"
definition cs_ip_α :: "checker_state_in_proof ⇒ dimacs_var checker_state" where
"cs_ip_α ≡ λ(err,confl,A,cbld,cdb).
if err then checker_state.FAIL
else if confl then PROOF_DONE (ran cdb) (cbld_α_clause cbld)
else PROOF (ran cdb) (cbld_α_clause cbld) (rpan_α A)"
lemma cs_ip_invar_antimono: "cs_ip_invar cap' csip ⟹ cap≤cap' ⟹ cs_ip_invar cap csip"
unfolding cs_ip_invar_def cs_common_invar_def
by auto
paragraph‹Outside Proof›
type_synonym checker_state_out_proof = "bool × bool × cdb × cbld × rpan"
definition cs_op_invar :: "nat ⇒ checker_state_out_proof ⇒ bool" where
"cs_op_invar cap ≡ λ(err,unsat,cdb,cbld,A).
cs_common_invar cap A cbld cdb
∧ cbld_α_clause cbld = {}
"
definition cs_op_α :: "checker_state_out_proof ⇒ dimacs_var checker_state" where
"cs_op_α ≡ λ(err,unsat,cdb,cbld,A).
if err then checker_state.FAIL
else if unsat then checker_state.UNSAT
else CNF (ran cdb)"
lemma cs_op_invar_antimono: "cs_op_invar cap' csop ⟹ cap≤cap' ⟹ cs_op_invar cap csop"
unfolding cs_op_invar_def cs_common_invar_def
by auto
lemma cs_op_invar_error_antimono: "cs_op_invar cap' (err,unsat,A,cdb) ⟹ cap≤cap' ⟹ cs_op_invar cap (True,unsat,A,cdb)"
unfolding cs_op_invar_def cs_common_invar_def
by auto
definition csop_is_unsat :: "checker_state_out_proof ⇒ bool" where
"csop_is_unsat ≡ λ(err,unsat,A,cdb). unsat"
definition csop_is_error :: "checker_state_out_proof ⇒ bool" where "csop_is_error ≡ λ(err,_). err"
definition csop_set_error :: "checker_state_out_proof ⇒ checker_state_out_proof" where
"csop_set_error ≡ λ(_,rest). (True,rest)"
lemma csop_set_error_error[simp]: "csop_is_error (csop_set_error cs)"
unfolding csop_is_error_def csop_set_error_def
by (auto split: prod.split)
lemma cs_op_invar_set_error[simp]: "cs_op_invar cap cs ⟹ cs_op_invar cap (csop_set_error cs)"
unfolding cs_op_invar_def csop_set_error_def
by auto
lemma csop_is_error_correct[simp]: "csop_is_error csop ⟷ cs_op_α csop = FAIL"
unfolding csop_is_error_def cs_op_α_def
apply (cases csop)
by simp
lemma csop_set_error_correct[simp]: "cs_op_α (csop_set_error csop) = FAIL"
unfolding csop_set_error_def cs_op_α_def by (cases csop) auto
paragraph‹Building Clause›
type_synonym checker_state_build_lemma = "bool × rpan × cbld × cdb"
definition cs_bl_invar :: "nat ⇒ checker_state_build_lemma ⇒ bool" where
"cs_bl_invar cap ≡ λ(err,A,cbld,cdb).
cs_common_invar cap A cbld cdb
∧ rpan_α A = rpa_and_not_C rpa_empty (cbld_α_clause cbld)
∧ cap≤rpan_cap A
"
lemma cs_bl_invar_antimono: "cs_bl_invar cap' csbl ⟹ cap≤cap' ⟹ cs_bl_invar cap csbl"
unfolding cs_bl_invar_def cs_common_invar_def
by auto
definition cs_bl_α :: "checker_state_build_lemma ⇒ dimacs_var checker_state" where
"cs_bl_α ≡ λ(err,A,cbld,cdb).
if err then checker_state.FAIL
else PREP_LEMMA (ran cdb) (cbld_α_clause cbld) (rpan_α A)
"
subsubsection ‹Transitions between Checker States›
text ‹We implement the transitions between the checker states.
For each transition, we prove that it preserves the invariant,
and implements the transition relation \<^const>‹checker_trans› on the abstract checker state.
›
paragraph ‹Proof Step›
definition proof_step :: "nat ⇒ checker_state_in_proof ⇒ checker_state_in_proof nres" where
"proof_step cid ≡ λ(err,confl,A,cbld,cdb). if err then
RETURN (err,confl,A,cbld,cdb)
else do {
(ul,err') ← cdb_check_uot A cdb cid;
if err' then
RETURN (err',confl,A,cbld,cdb)
else if is_None ul then
RETURN (err,True,A,cbld,cdb)
else do {
A ← rpan_set_unchecked A (the ul);
RETURN (err,confl,A,cbld,cdb)
}
}"
lemma proof_step_correct[refine_vcg]: "⟦cs_ip_invar cap csip; cap>0 ⟧
⟹ proof_step cid csip ≤ SPEC (λcsip'.
cs_ip_invar (cap-1) csip'
∧ checker_trans (cs_ip_α csip) (cs_ip_α csip')
)"
unfolding proof_step_def
apply refine_vcg
apply clarsimp_all
unfolding cs_ip_invar_def cs_common_invar_def
apply clarsimp_all
apply (all ‹(intro conjI)?›)
apply simp_all
subgoal
by (auto simp add: cs_ip_α_def split: option.splits simp: ct_fail)
subgoal
by (auto simp add: cs_ip_α_def split: option.splits simp: ct_refl ct_fail)
subgoal
by (auto simp add: cs_ip_α_def simp: ct_refl ct_fail)
subgoal
by (auto simp add: cs_ip_α_def split: option.splits simp: ct_refl ct_fail ct_add_conflict)
subgoal
unfolding rpa_is_uot_lit_def
by auto
subgoal
by (auto simp add: cs_ip_α_def simp: ct_refl ct_fail ct_add_unit)
done
paragraph ‹Finish proof›
abbreviation (input) "err_code_no_conflict ≡ 0x4"
definition finish_proof :: "nat ⇒ checker_state_in_proof ⇒ checker_state_out_proof nres" where
"finish_proof cid ≡ λ(err,confl,A,cbld,cdb).
if err then doN {
cbld ← cbld_abort_clause cbld;
RETURN (err,False,cdb,cbld,A)
} else if ¬confl then doN {
ERROR err_code_no_conflict;
cbld ← cbld_abort_clause cbld;
RETURN (True,False,cdb,cbld,A)
} else doN {
e ← cbld_is_empty cbld;
(cl,cbld) ← cbld_finish_clause cbld;
cdb ← cdb_insert cid cl cdb;
RETURN (False,e,cdb,cbld,A)
}"
lemma in_ran_updD: "⟦X ∈ ran (m(k ↦ v))⟧ ⟹ X∈ran m ∨ X=v"
by (auto simp: ran_def split: if_splits)
lemma finish_proof_correct[refine_vcg]: "⟦ cs_ip_invar cap csip ⟧
⟹ finish_proof cid csip ≤ SPEC (λcsop. cs_op_invar cap csop ∧ rtranclp checker_trans (cs_ip_α csip) (cs_op_α csop))"
unfolding finish_proof_def cdb_insert_def
apply refine_vcg
apply clarsimp_all
unfolding cs_ip_invar_def cs_op_invar_def cs_common_invar_def cs_ip_α_def cs_op_α_def
apply (clarsimp_all)
subgoal
by (auto intro: ct_fail)
subgoal
apply (auto dest!: in_ran_updD simp: cbld_α_maxlit_bound)
apply blast
done
apply (intro conjI impI)
subgoal
by (auto intro: ct_finish_proof_unsat)
subgoal
apply (auto
intro: r2_into_rtranclp[of checker_trans, OF ct_finish_proof ct_del_clauses]
dest: in_ran_updD)
done
done
paragraph ‹Start lemma›
definition start_lemma :: "nat ⇒ checker_state_out_proof ⇒ checker_state_build_lemma nres" where
"start_lemma cap ≡ λ(err,unsat,cdb,cbld,A). doN {
A ← rpan_clear cap A;
RETURN (err,A,cbld,cdb)
}"
lemma rpa_and_not_C_empty[simp]: "rpa_and_not_C A {} = A" unfolding rpa_and_not_C_def by auto
lemma start_lemma_correct[refine_vcg]: "⟦cs_op_invar cap csop; ¬csop_is_unsat csop⟧ ⟹
start_lemma cap csop ≤ SPEC (λcsbl. cs_bl_invar cap csbl ∧ checker_trans (cs_op_α csop) (cs_bl_α csbl))"
unfolding start_lemma_def
apply refine_vcg
unfolding cs_op_invar_def cs_bl_invar_def cs_common_invar_def
apply clarsimp_all
unfolding cs_op_α_def cs_bl_α_def csop_is_unsat_def
by (auto simp: ct_fail ct_start_lemma)
paragraph ‹Add literal›
definition add_literal:: "dv_lit ⇒ checker_state_build_lemma ⇒ checker_state_build_lemma nres" where
"add_literal l ≡ λ(err,A,cbld,cdb). do {
ASSERT (cbld_invar cbld);
cbld ← cbld_add_lit l cbld;
A ← rpan_set_checked A (neg_lit l);
RETURN (err,A,cbld,cdb)
}"
lemma rpa_and_not_C_insert[simp]: "rpa_and_not_C A (insert l C) = (rpa_and_not_C A C)(neg_lit l:=True)"
unfolding rpa_and_not_C_def by auto
lemma ss_range_maxI: "A ⊆ {l..h} ⟹ A ⊆ {l..max h h'}" for A :: "nat set"
by (auto simp: max_def)
lemma add_literal_correct[refine_vcg]: "⟦ cs_bl_invar cap csbl; cap≠0 ⟧ ⟹
add_literal l csbl ≤ SPEC (λcsbl'. cs_bl_invar (cap-1) csbl' ∧ checker_trans (cs_bl_α csbl) (cs_bl_α csbl'))"
unfolding add_literal_def
apply refine_vcg
unfolding cs_bl_invar_def cs_common_invar_def Let_def
apply (clarsimp_all)
apply (all ‹(intro conjI)?›)
apply simp_all
subgoal by (simp add: ss_range_maxI)
subgoal by blast
unfolding cs_bl_α_def
by (auto intro: ct_fail ct_add_lit)
paragraph ‹Start proof›
definition start_proof:: "checker_state_build_lemma ⇒ checker_state_in_proof nres" where
"start_proof ≡ λ(err,A,cbld,cdb).
RETURN (err,False,A,cbld,cdb)
"
lemma start_proof_correct[refine_vcg]: "⟦cs_bl_invar cap csbl; 0<cap⟧
⟹ start_proof csbl ≤ SPEC (λcsip. cs_ip_invar (cap-1) csip ∧ checker_trans (cs_bl_α csbl) (cs_ip_α csip))"
unfolding start_proof_def
apply refine_vcg
unfolding cs_bl_invar_def cs_ip_invar_def Let_def
apply clarsimp_all
subgoal
unfolding cs_common_invar_def
by linarith
subgoal
unfolding cs_bl_α_def cs_ip_α_def
by (auto intro: ct_fail ct_start_proof)
done
definition start_proof_error:: "checker_state_build_lemma ⇒ checker_state_in_proof nres" where
"start_proof_error ≡ λ(err,A,cbld,cdb). do {
RETURN (True,False,A,cbld,cdb)
}"
lemma start_proof_error_correct[refine_vcg]: "⟦cs_bl_invar cap csbl⟧
⟹ start_proof_error csbl ≤ SPEC (λcsip. cs_ip_invar cap csip ∧ checker_trans (cs_bl_α csbl) (cs_ip_α csip))"
unfolding start_proof_error_def
apply refine_vcg
unfolding cs_bl_invar_def cs_ip_invar_def Let_def
apply clarsimp_all
unfolding cs_bl_α_def cs_ip_α_def
by (auto intro: ct_fail)
paragraph ‹Delete Clause›
definition delete_clause:: "nat ⇒ checker_state_out_proof ⇒ checker_state_out_proof nres" where
"delete_clause cid ≡ λ(err,unsat,cdb,cbld,A). doN {
cdb ← cdb_delete cid cdb;
RETURN (err,unsat,cdb,cbld,A)
}"
lemma ran_del_ss: "ran (m(k:=None)) ⊆ ran m"
by (auto simp: ran_def)
lemma delete_clause_correct[refine_vcg]: "⟦ cs_op_invar cap csop ⟧
⟹ delete_clause cid csop ≤ SPEC (λcsop'. cs_op_invar cap csop' ∧ checker_trans (cs_op_α csop) (cs_op_α csop'))"
unfolding delete_clause_def cdb_delete_def
apply refine_vcg
apply clarsimp_all
subgoal
unfolding cs_op_invar_def cs_common_invar_def cs_op_α_def
by (auto dest!: ran_del_ss[THEN set_mp])
subgoal
unfolding cs_op_α_def
by (auto intro: ct_fail ct_refl ct_del_clauses dest: ran_del_ss[THEN set_mp])
done
subsection ‹Combining Checker with LRAT Parser›
text ‹Using the \<^typ>‹brd_rs› interface to read from binary encoded files,
we define functions to parse them as LRAT, and make the corresponding transitions
on the checker state.
The correctness lemmas show that the checker state invariants are preserved.
›
definition skip_to_zero_uids :: "brd_rs ⇒ brd_rs nres" where
"skip_to_zero_uids prf⇩0 ≡ do {
(prf,_) ← WHILEIT (λ(prf,_). brd_rs_invar prf ∧ brd_rs_remsize prf ≤ brd_rs_remsize prf⇩0)
(λ(prf,brk). ¬brd_rs_no_size_left prf ∧ ¬brk)
(λ(prf,_). do {
(cid,prf) ← brd_rs_read_signed_id prf;
RETURN (prf,dest_cid cid=0)
})
(prf⇩0,False);
RETURN prf
}"
lemma skip_to_zero_uids_correct[refine_vcg]: "brd_rs_invar prf ⟹
skip_to_zero_uids prf ≤ SPEC (λprf'. brd_rs_invar prf' ∧ brd_rs_remsize prf' ≤ brd_rs_remsize prf)"
unfolding skip_to_zero_uids_def
apply (refine_vcg WHILEIT_rule[where R="measure (brd_rs_remsize o fst)"])
by auto
definition delete_clauses :: "checker_state_out_proof ⇒ brd_rs ⇒ (checker_state_out_proof × brd_rs) nres" where
"delete_clauses cs prf⇩0 ≡ doN {
(cs,prf,_) ← monadic_WHILEIT (λ_. True)
(λ(cs,prf,brk). doN { ASSERT(brd_rs_invar prf); RETURN (¬brd_rs_no_size_left prf ∧ ¬brk)})
(λ(cs,prf,_). do {
(cid,prf) ← brd_rs_read_signed_id prf;
if dest_cid cid = 0 then
RETURN (cs,prf,True)
else doN {
cs ← delete_clause cid cs;
RETURN (cs,prf,False)
}
})
(cs,prf⇩0,False);
RETURN (cs,prf)
}"
lemma delete_clauses_correct[refine_vcg]: "⟦ cs_op_invar cap cs; brd_rs_invar prf ⟧ ⟹
delete_clauses cs prf ≤ SPEC (λ(cs',prf').
cs_op_invar cap cs' ∧ rtranclp checker_trans (cs_op_α cs) (cs_op_α cs')
∧ brd_rs_invar prf' ∧ brd_rs_remsize prf' ≤ brd_rs_remsize prf)"
unfolding delete_clauses_def
apply (refine_vcg monadic_WHILEIT_strengthen_invar_rule[where
Inew="λ(cs',prf',_).
brd_rs_invar prf' ∧ brd_rs_remsize prf' ≤ brd_rs_remsize prf
∧ cs_op_invar cap cs'
∧ rtranclp checker_trans (cs_op_α cs) (cs_op_α cs')"
and R="measure (λ(_,prf,_). brd_rs_remsize prf)"
]
)
by auto
abbreviation (input) "err_code_no_term_zero_lit ≡ 0x5"
definition add_literals_loop :: "checker_state_build_lemma ⇒ brd_rs ⇒ (checker_state_in_proof × brd_rs) nres" where
"add_literals_loop cs prf ≡ doN {
(cs,prf,ctd)←monadic_WHILEIT (λ_. True)
(λ(cs,prf,ctd). doN { ASSERT(brd_rs_invar prf); RETURN (¬brd_rs_no_size_left prf ∧ ctd) })
(λ(cs,prf,_). do {
(l,prf) ← brd_rs_read_ulito prf;
PARSED_LRAT_LIT l;
if is_None l then RETURN (cs,prf,False)
else doN {
cs ← add_literal (the l) cs;
RETURN (cs,prf,True)
}
})
(cs,prf,True);
if ctd then doN {
ERROR err_code_no_term_zero_lit;
cs←start_proof_error cs;
RETURN (cs,prf)
} else doN {
cs←start_proof cs;
RETURN (cs,prf)
}
}"
lemma add_literals_loop_correct[refine_vcg]: "⟦ cs_bl_invar (brd_rs_remsize prf) cs; brd_rs_invar prf ⟧
⟹ add_literals_loop cs prf ≤ SPEC (λ(cs',prf').
brd_rs_invar prf'
∧ brd_rs_remsize prf' ≤ brd_rs_remsize prf
∧ cs_ip_invar (brd_rs_remsize prf') cs'
∧ rtranclp checker_trans (cs_bl_α cs) (cs_ip_α cs'))"
unfolding add_literals_loop_def
apply (refine_vcg monadic_WHILEIT_strengthen_invar_rule[where
Inew="λ(cs',prf',ctd).
brd_rs_invar prf'
∧ brd_rs_remsize prf' ≤ brd_rs_remsize prf
∧ cs_bl_invar (if ctd then brd_rs_remsize prf' else Suc (brd_rs_remsize prf')) cs'
∧ rtranclp checker_trans (cs_bl_α cs) (cs_bl_α cs')"
and R="measure (λ(_,prf,_). brd_rs_remsize prf)"
]
)
apply clarsimp_all
apply (all ‹(erule asm_rl[of "cs_bl_invar _ _"] asm_rl[of "checker_invar _ _"])?›)
apply (auto elim: cs_bl_invar_antimono cs_ip_invar_antimono)
done
definition prove_units_loop :: "checker_state_in_proof ⇒ brd_rs ⇒ (checker_state_in_proof × brd_rs) nres" where
"prove_units_loop cs prf ≡ doN {
(cs,prf,_)←monadic_WHILEIT (λ_. True)
(λ(cs,prf,brk). doN { ASSERT(brd_rs_invar prf); RETURN (¬brd_rs_no_size_left prf ∧ ¬brk) })
(λ(cs,prf,_). do {
(cid,prf) ← brd_rs_read_signed_id prf;
PARSED_LRAT_ID cid;
if dest_cid cid=0 then RETURN (cs,prf,True)
else doN {
cs ← proof_step cid cs;
RETURN (cs,prf,False)
}
})
(cs,prf,False);
RETURN (cs,prf)
}"
lemma prove_units_loop_correct[refine_vcg]: "⟦ brd_rs_invar prf; cs_ip_invar (brd_rs_remsize prf) cs ⟧
⟹ prove_units_loop cs prf ≤ SPEC (λ(cs',prf').
brd_rs_invar prf'
∧ brd_rs_remsize prf' ≤ brd_rs_remsize prf
∧ cs_ip_invar (brd_rs_remsize prf') cs'
∧ rtranclp checker_trans (cs_ip_α cs) (cs_ip_α cs'))"
unfolding prove_units_loop_def
apply (refine_vcg monadic_WHILEIT_strengthen_invar_rule[where
Inew="λ(cs',prf',_).
brd_rs_invar prf'
∧ brd_rs_remsize prf'≤brd_rs_remsize prf
∧ cs_ip_invar (brd_rs_remsize prf') cs'
∧ rtranclp checker_trans (cs_ip_α cs) (cs_ip_α cs')"
and R="measure (λ(_,prf,_). brd_rs_remsize prf)"
]
)
apply clarsimp_all
apply (all ‹(erule asm_rl[of "cs_ip_invar _ _"] asm_rl[of "checker_invar _ _"])?›)
apply (auto elim: cs_ip_invar_antimono)
done
synth_definition rdmem_it_free [llvm_inline] is [sepref_frame_free_rules]: "MK_FREE rdmem_it_assn ⌑"
unfolding rdmem_it_assn_def rdmem_it_assn_raw_def
by sepref_dbg_side
definition main_checker_loop :: "checker_state_out_proof ⇒ brd_rs ⇒ (bool × brd_rs) nres" where
"main_checker_loop cs prf ≡ doN {
(cs,prf)←monadic_WHILEIT (λ_. True)
(λ(cs,prf). doN { ASSERT(brd_rs_invar prf); RETURN (¬csop_is_error cs ∧ ¬csop_is_unsat cs ∧ ¬brd_rs_no_size_left prf) })
(λ(cs,prf). doN {
(c,prf) ← brd_rs_read prf;
if c=char_a then do {
(cid,prf) ← brd_rs_read_signed_id_ndecr prf;
PARSED_LRAT_ADD cid;
ASSERT(brd_rs_invar prf);
cs←start_lemma (brd_rs_remsize prf) cs;
(cs,prf)←add_literals_loop cs prf;
(cs,prf)←prove_units_loop cs prf;
cs ← finish_proof cid cs;
RETURN (cs,prf)
} else if c=char_d then doN {
(cs,prf) ← delete_clauses cs prf;
RETURN (cs,prf)
} else doN {
ERROR err_code_syntax_error;
let cs = csop_set_error cs;
RETURN (cs,prf)
}
})
(cs,prf);
RETURN (¬csop_is_error cs ∧ csop_is_unsat cs,prf)
}"
lemma cs_op_invar_err: "cs_op_invar cap (err,unsat,A,cdb) ⟹ cs_op_invar cap (True,unsat,A,cdb)"
unfolding cs_op_invar_def by auto
lemma checker_invar_err: "checker_invar F⇩0 (cs_op_α (True, unsat,A,cdb))"
unfolding cs_op_α_def by (auto simp: checker_invar.simps)
lemma cs_op_α_err: "cs_op_α (True, unsat,A,cdb) = FAIL"
unfolding cs_op_α_def by auto
lemma csop_unsat_α: "⟦csop_is_unsat cs; ¬csop_is_error cs⟧ ⟹ cs_op_α cs = UNSAT"
unfolding cs_op_α_def csop_is_unsat_def csop_is_error_def
by (cases cs; auto)
lemma csop_unsat_imp_unsat:
"⟦cs_op_invar cap cs; csop_is_unsat cs; ¬csop_is_error cs; checker_invar F⇩0 (cs_op_α cs) ⟧ ⟹ ¬sat F⇩0"
unfolding cs_op_α_def csop_is_unsat_def csop_is_error_def
by (cases cs; auto simp: checker_invar.simps)
theorem main_checker_loop_correct[refine_vcg]: "⟦ brd_rs_invar prf; cs_op_invar (brd_rs_remsize prf) cs; rtranclp checker_trans (CNF F⇩0) (cs_op_α cs) ⟧
⟹ main_checker_loop cs prf ≤ SPEC (λ(r,prf). brd_rs_invar prf ∧ (r ⟶ ¬sat F⇩0))
"
unfolding main_checker_loop_def
unfolding csop_set_error_def
apply (refine_vcg monadic_WHILEIT_strengthen_invar_rule[where
Inew="λ(cs,prf). brd_rs_invar prf ∧ cs_op_invar (brd_rs_remsize prf) cs ∧ rtranclp checker_trans (CNF F⇩0) (cs_op_α cs)"
and R="measure (λ(cs,prf). brd_rs_remsize prf)"
])
apply (clarsimp_all simp: cs_op_α_err csop_unsat_α)
apply (all ‹(erule asm_rl[of "cs_ip_invar _ _"] asm_rl[of "cs_op_invar _ _"] asm_rl[of "checker_invar _ _"])?›)
apply (auto
simp: parsed1_remsize parsed_remsize
elim: cs_op_invar_antimono cs_op_invar_error_antimono
intro: ct_fail
dest: checker_trans_rtrancl_unsatI)
done
subsubsection ‹Combining CNF Parser with Checker›
text ‹In this section, we combine the CNF parser and the main checker loop›
paragraph ‹Convert builder state to checker state›
text ‹
Our DIMACS parser uses a \<^typ>‹builder_state› to construct the initial formula.
First, we have to convert it into an initial checker state.
›
abbreviation (input) "info_code_ncid ≡ 0x1"
abbreviation (input) "info_code_maxlit ≡ 0x2"
definition builder_finish_building :: "builder_state ⇒ checker_state_out_proof nres" where
"builder_finish_building ≡ λ(ncid,cbld,cdb). doN {
ml ← cbld_get_maxlit cbld;
INFO_cid info_code_ncid ncid;
INFO_ulit info_code_maxlit ml;
let A = rpan_empty ml 0;
RETURN (False, False, cdb, cbld, A)
}"
lemma builder_finish_building_correct[refine_vcg]: "⟦ bs_invar cap⇩1 cap⇩2 bs; bs_αC bs = {} ⟧ ⟹
builder_finish_building bs ≤ SPEC (λcsop. cs_op_invar cap⇩1 csop ∧ cs_op_α csop = CNF (bs_αF bs))"
unfolding builder_finish_building_def
apply refine_vcg
subgoal
unfolding bs_invar_def cbld_invar_def
by auto
subgoal
unfolding bs_invar_def cs_op_invar_def cs_common_invar_def bs_αC_def
apply (auto simp: maxlit_vdom_def)
by (metis atLeastAtMost_iff basic_trans_rules(31) image_eqI mem_simps(9) ulit_of_inv(1) ulit_of_inv(2))
subgoal
unfolding cs_op_invar_def cs_op_α_def bs_invar_def bs_αF_def
by auto
done
paragraph ‹Read DIMACS file to initial checker state›
definition read_dimacs_cs :: "input ⇒ (checker_state_out_proof × nat) nres"
where "read_dimacs_cs dimacs_input ≡ doN {
(bs,cap⇩1,err) ← read_dimacs_file dimacs_input;
cs ← builder_finish_building bs;
if err then RETURN (csop_set_error cs,cap⇩1)
else RETURN (cs,cap⇩1)
}"
lemma read_dimacs_cs_correct[refine_vcg]: "
read_dimacs_cs dimacs_input ≤ SPEC (λ(cs,cap⇩1).
cs_op_invar cap⇩1 cs
∧ (¬csop_is_error cs ⟶ (∃fml. (i_data dimacs_input, fml) ∈ gM_rel cnf_dimacs ∧ cs_op_α cs = CNF fml)))"
unfolding read_dimacs_cs_def
apply (refine_vcg)
apply simp_all
apply (clarsimp; assumption)
apply (hypsubst; simp; fail)
apply (hypsubst; simp; fail)
subgoal by simp
subgoal by blast
done
lemma "
read_dimacs_cs dimacs_input ≤ SPEC (λ(cs,cap⇩1).
cs_op_invar cap⇩1 cs
∧ (cs_op_α cs = FAIL ∨ (∃fml. (i_data dimacs_input, fml) ∈ gM_rel cnf_dimacs ∧ cs_op_α cs = CNF fml)))"
apply (refine_vcg)
apply simp_all
apply auto
done
definition [simp]: "ll_dbg_tag_parsed_cnf (err::8 word) ≡ RETURN ()"
lemma [refine_vcg]: "ll_dbg_tag_parsed_cnf x ≤ SPEC (λ_. True)" by simp
sepref_register ll_dbg_tag_parsed_cnf
sepref_def ll_dbg_tag_parsed_cnf_impl is "ll_dbg_tag_parsed_cnf" :: "word_assn⇧k →⇩a unit_assn"
unfolding ll_dbg_tag_parsed_cnf_def
by sepref
paragraph ‹Read DIMACS file and run checker›
definition read_check_lrat :: "input ⇒ bool nres" where
"read_check_lrat cnf ≡ doN {
(cs,cap) ← read_dimacs_cs cnf;
if csop_is_error cs then doN {
ll_dbg_tag_parsed_cnf 0;
RETURN False
} else VCG_STOP (doN {
let prf = brd_rs_new cap;
ll_dbg_tag_parsed_cnf 1;
(res,prf) ← main_checker_loop cs prf;
RETURN res
})
}"
text ‹This is the correctness theorem of the functional abstraction level checker:
If it returns true, the input was a valid representation of an unsatisfiable formula.
›
theorem read_check_lrat_correct[refine_vcg]: "read_check_lrat cnf ≤ SPEC (λr.
r ⟶ (∃F. (i_data cnf, F) ∈ gM_rel cnf_dimacs ∧ ¬sat F))"
unfolding read_check_lrat_def
apply refine_vcg
apply clarsimp_all
apply (rule VCG_STOP)
apply refine_vcg
by auto
subsection ‹Refinement to LLVM›
text ‹We refine from the functional level to the imperative level.
This is done by the Sepref tool, and mostly automatic.
›
subsubsection ‹Concrete Checker States and Transitions›
definition "cs_ip_assn = bool1_assn ×⇩a bool1_assn ×⇩a rpan_assn ×⇩a cbld_assn ×⇩a cdb_assn"
definition "cs_op_assn = bool1_assn ×⇩a bool1_assn ×⇩a cdb_assn ×⇩a cbld_assn ×⇩a rpan_assn"
definition "cs_bl_assn ≡ bool1_assn ×⇩a rpan_assn ×⇩a cbld_assn ×⇩a cdb_assn"
sepref_register proof_step csop_set_error csop_is_error csop_is_unsat finish_proof start_lemma
add_literal start_proof start_proof_error delete_clause
term proof_step
sepref_def proof_step_impl is "uncurry proof_step" :: "cid_assn⇧k *⇩a cs_ip_assn⇧d →⇩a cs_ip_assn"
unfolding proof_step_def cs_ip_assn_def
by sepref
sepref_def csop_set_error_impl [llvm_inline] is "RETURN o csop_set_error" :: "cs_op_assn⇧d →⇩a cs_op_assn"
unfolding csop_set_error_def cs_op_assn_def
by sepref
sepref_def csop_is_error_impl [llvm_inline] is "RETURN o csop_is_error" :: "cs_op_assn⇧k →⇩a bool1_assn"
unfolding csop_is_error_def cs_op_assn_def
by sepref
sepref_def csop_is_unsat_impl [llvm_inline] is "RETURN o csop_is_unsat" :: "cs_op_assn⇧k →⇩a bool1_assn"
unfolding csop_is_unsat_def cs_op_assn_def
by sepref
sepref_def finish_proof_impl is "uncurry finish_proof" :: "cid_assn⇧k *⇩a cs_ip_assn⇧d →⇩a cs_op_assn"
unfolding finish_proof_def cs_ip_assn_def cs_op_assn_def
by sepref
sepref_def start_lemma_impl is "uncurry start_lemma" :: "size_assn⇧k *⇩a cs_op_assn⇧d →⇩a cs_bl_assn"
unfolding start_lemma_def cs_op_assn_def cs_bl_assn_def
by sepref
sepref_def add_literal_impl is "uncurry add_literal" :: "ulit_assn⇧k *⇩a cs_bl_assn⇧d →⇩a cs_bl_assn"
unfolding add_literal_def cs_bl_assn_def
by sepref
sepref_def start_proof_impl is "start_proof" :: "cs_bl_assn⇧d →⇩a cs_ip_assn"
unfolding start_proof_def cs_bl_assn_def cs_ip_assn_def
by sepref
sepref_def start_proof_error_impl is "start_proof_error" :: "cs_bl_assn⇧d →⇩a cs_ip_assn"
unfolding start_proof_error_def cs_bl_assn_def cs_ip_assn_def
by sepref
sepref_def delete_clause_impl is "uncurry delete_clause" :: "cid_assn⇧k *⇩a cs_op_assn⇧d →⇩a cs_op_assn"
unfolding delete_clause_def cs_op_assn_def
by sepref
subsubsection ‹Checker with LRAT Parser, up to \<^const>‹main_checker_loop››
sepref_register skip_to_zero_uids delete_clauses add_literals_loop prove_units_loop main_checker_loop
sepref_def skip_to_zero_uids_impl is "skip_to_zero_uids" :: "brd_rs_assn⇧d →⇩a brd_rs_assn"
unfolding skip_to_zero_uids_def
apply (annot_snat_const size_T)
by sepref
sepref_def delete_clauses_impl is "uncurry delete_clauses" :: "cs_op_assn⇧d *⇩a brd_rs_assn⇧d →⇩a cs_op_assn ×⇩a brd_rs_assn"
unfolding delete_clauses_def
apply (annot_snat_const size_T)
by sepref
sepref_def add_literals_loop_impl is "uncurry add_literals_loop"
:: "cs_bl_assn⇧d *⇩a brd_rs_assn⇧d →⇩a cs_ip_assn ×⇩a brd_rs_assn"
unfolding add_literals_loop_def
by sepref
sepref_def prove_units_loop_impl is "uncurry prove_units_loop"
:: "cs_ip_assn⇧d *⇩a brd_rs_assn⇧d →⇩a cs_ip_assn ×⇩a brd_rs_assn"
unfolding prove_units_loop_def
apply (annot_snat_const size_T)
by sepref
synth_definition cs_op_free [llvm_code] is [sepref_frame_free_rules]: "MK_FREE (cs_op_assn) ⌑"
unfolding cs_op_assn_def
by sepref_dbg_side
sepref_def main_checker_loop_impl is "uncurry main_checker_loop" :: "cs_op_assn⇧d *⇩a brd_rs_assn⇧d →⇩a bool1_assn ×⇩a brd_rs_assn"
unfolding main_checker_loop_def
supply [[goals_limit = 1]]
by sepref
subsubsection ‹Combination with CNF Parser›
sepref_register
builder_finish_building
read_dimacs_cs
sepref_def builder_finish_building_impl is builder_finish_building :: "bs_assn⇧d →⇩a cs_op_assn"
unfolding builder_finish_building_def bs_assn_def cs_op_assn_def
apply (annot_snat_const size_T)
by sepref
sepref_def read_dimacs_cs_impl is "read_dimacs_cs"
:: "rdmem_inp_assn⇧k →⇩a cs_op_assn ×⇩a size_assn"
unfolding read_dimacs_cs_def
by sepref
sepref_register read_check_lrat
sepref_def read_check_lrat_impl is "read_check_lrat" :: "rdmem_inp_assn⇧k →⇩a bool1_assn"
unfolding read_check_lrat_def VCG_STOP_def
by sepref
subsubsection ‹Wrapping into Nicer Interface›
text ‹In order to interface with C, we unfold some definitions:
▪ we pass a pointer and a size, rather than the tuple defined by \<^const>‹rdmem_inp_assn›
▪ we return a byte (i8) instead of a bit (i1)
›
definition "make_input_from_array_and_size (xs::8 word list) n ≡ doN {
ASSERT (n = length xs);
RETURN (INPUT xs)
}"
lemma make_input_from_array_and_size_correct[refine_vcg]:
"n = length xs ⟹ make_input_from_array_and_size xs n ≤ SPEC (λr. i_data r = xs)"
unfolding make_input_from_array_and_size_def
apply refine_vcg
by auto
definition mk_rdmem_inp :: "8 word list ⇒ nat ⇒ rdmem_inp nres" where "mk_rdmem_inp xs n ≡ doN {
ASSERT (length xs = n);
RETURN (xs,n)
}"
definition rdmem_data :: "rdmem_inp ⇒ 8 word list" where "rdmem_data ≡ λ(xs,n). xs"
lemma mk_rdmem_inp_refine: "(mk_rdmem_inp,make_input_from_array_and_size) ∈ Id → Id → ⟨rdmem_inp_rel⟩nres_rel"
unfolding mk_rdmem_inp_def make_input_from_array_and_size_def
apply refine_vcg
unfolding rdmem_inp_rel_def in_br_conv
by auto
lemma rdmem_data_refine: "(rdmem_data, i_data) ∈ rdmem_inp_rel → Id"
unfolding rdmem_data_def rdmem_inp_rel_def
by (auto simp: in_br_conv)
sepref_def mk_rdmem_inp_impl is "uncurry mk_rdmem_inp"
:: "[λ_. True]⇩c (array_slice_assn id_assn)⇧d *⇩a size_assn⇧k → rdmem_inp_assn_raw [λ(p,_) (p',_). p'=p]⇩c"
unfolding mk_rdmem_inp_def rdmem_inp_assn_raw_def
by sepref
sepref_def rdmem_data_impl is "RETURN o rdmem_data" :: "[λ_. True]⇩c rdmem_inp_assn_raw⇧d → array_slice_assn id_assn [λ(p,_) p'. p'=p]⇩c"
unfolding rdmem_data_def rdmem_inp_assn_raw_def
by sepref
sepref_register make_input_from_array_and_size
context
notes [fcomp_norm_unfold] = rdmem_inp_assn_def[symmetric]
begin
lemmas [sepref_fr_rules] = mk_rdmem_inp_impl.refine[FCOMP mk_rdmem_inp_refine]
lemmas [sepref_fr_rules] = rdmem_data_impl.refine[FCOMP rdmem_data_refine]
end
definition "read_check_lrat_wrapper cnfp cnf_size ≡ doN {
cnf ← make_input_from_array_and_size cnfp cnf_size;
res ← read_check_lrat cnf;
let cnfp' = i_data cnf;
unborrow cnfp' cnfp;
if res then RETURN 1 else RETURN 0
}"
definition lrat_checker_spec :: "8 word list ⇒ nat ⇒ nat nres" where
"lrat_checker_spec cnf cnf_size ≡ doN {
ASSERT(cnf_size = length cnf);
SPEC (λr::nat. r≠0 ⟶ ( (∃F. (cnf,F)∈gM_rel cnf_dimacs ∧ ¬sat F)))
}"
lemma read_check_lrat_wrapper_refine: "(read_check_lrat_wrapper, lrat_checker_spec) ∈ Id → Id → ⟨Id⟩nres_rel"
unfolding read_check_lrat_wrapper_def lrat_checker_spec_def
apply refine_vcg
by auto
sepref_def lrat_checker is "uncurry read_check_lrat_wrapper"
:: "(array_slice_assn id_assn)⇧k *⇩a size_assn⇧k →⇩a (char_assn)"
unfolding read_check_lrat_wrapper_def
apply (annot_unat_const char_T)
by sepref
theorem lrat_checker_refines_spec: "(uncurry lrat_checker, uncurry lrat_checker_spec)
∈ (IICF_Array.array_slice_assn (word_assn' char_T))⇧k *⇩a size_assn⇧k →⇩a unat_assn' char_T"
using lrat_checker.refine[FCOMP read_check_lrat_wrapper_refine]
.
lemma "lrat_checker p n = do⇩M {
r ← read_check_lrat_impl (p,n);
llc_if r (return⇩M 1) (return⇩M 0)
}"
unfolding lrat_checker_def mk_rdmem_inp_impl_def rdmem_data_impl_def
by simp
subsection ‹Generation of LLVM and Correctness Theorem›
export_llvm lrat_checker is "uint8_t lrat_checker(uint8_t *, int64_t)"
file "../code/lrat_isa_export.ll"
theorem lrat_checker_correct: "llvm_htriple
(raw_array_slice_assn cnf cnf_ptr ∧* size_assn cnf_size cnf_sizei
∧* ↑(cnf_size=length cnf))
(lrat_checker cnf_ptr cnf_sizei)
(λr. raw_array_slice_assn cnf cnf_ptr ∧* size_assn cnf_size cnf_sizei
∧* ↑(r≠0 ⟶ (∃F. (cnf,F)∈gM_rel cnf_dimacs ∧ ¬sat F)))"
apply (rule htriple_pure_preI)
apply vcg_prepare_external
proof -
have AUX1: "array_slice_assn id_assn = raw_array_slice_assn"
unfolding array_slice_assn_def by simp
have [simp]: "nofail (lrat_checker_spec cnf (length cnf))"
unfolding lrat_checker_spec_def by simp
assume [simp]: "cnf_size = length cnf"
have AUX2: "Refine_Basic.RETURN x ≤ lrat_checker_spec cnf (length cnf)
⟷ ((x≠0 ⟶ (∃F. (cnf, F) ∈ gM_rel cnf_dimacs ∧ ¬ sat F)))" for x
unfolding lrat_checker_spec_def
by simp
note T1[vcg_rules] = lrat_checker_refines_spec[
THEN hfrefD, THEN hn_refineD,
of "(cnf,length cnf)" "(cnf_ptr,cnf_sizei)",
unfolded AUX1, simplified]
thm unat.rel_def
have AUX3: "unat_assn x r = ↑(x = unat r)" for x and r :: "8 word"
by (auto simp: unat_rel_def unat.rel_def in_br_conv pure_def)
have AUX4: "0<unat r ⟷ r≠0" for r :: "8 word"
by (simp add: unat_gt_0)
note [dest] = AUX2[THEN iffD1, rule_format]
note [simp] = AUX3 AUX4
show ?thesis by vcg
qed
lemma "size_assn n w = ↑(n = unat w ∧ unat w < 2^(size_t_len-1))"
unfolding snat_rel_def snat.rel_def pure_def in_br_conv snat_invar_alt
by (auto simp: snat_eq_unat_aux1)
lemma "size_assn n w = ↑(n = nat (sint w) ∧ sint w ≥ 0)"
unfolding snat_rel_def snat.rel_def pure_def in_br_conv snat_invar_def
by (auto simp: word_msb_sint snat_def)
end