Theory Example_End_To_End_Certificate
theory Example_End_To_End_Certificate
imports "Voblint_VIMP.VIMP_Notation" "Voblint_CLI.Analysis_Certified"
begin
section ‹One configuration, one program, no premise left standing›
text ‹
‹run_voblint_source_sound› is stated for an arbitrary configuration
and an arbitrary program, so on its own it says nothing about any particular
run: a caller still owes the answer. This theory computes it, by evaluation,
for one program at one configuration --- the
product domain, a call-string context of length one, and always-join named
explicitly rather than defaulted --- and reads the theorem's conclusion off
the result.
Three dimensions at once is the point. A composite domain exercises the
product's transfer; a call-string policy keys the solved table by call history;
and naming a discipline the pairing does not default to shows the certificate
travels with the solver actually run, not with the one the registry prefers.
›
subsection ‹The program›
text ‹
‹bump› is called twice with different actuals, so a call string of length one
files two activations of it under two contexts. The check reads the second
result.
›
definition certificate_demo_prog :: imp_prog where
"certificate_demo_prog = program {
fun bump(n) { return n + 1; }
fun main() {
a = bump(1);
b = bump(41);
__voblint_check(0 < b);
}
}"
lemma certificate_demo_wf: "wf_program_compile_input_exec certificate_demo_prog"
by eval
text ‹
The configuration: Int at its most precise refinement, the joining
update rule, and call strings of length one.
›
abbreviation certificate_analyses :: "analysis_domain list" where
"certificate_analyses ≡ [Int_Analysis Refine_Fixpoint]"
abbreviation certificate_config :: analysis_config where
"certificate_config ≡ Analysis_Config certificate_analyses Globals_Join (Ctx_CallString 1)
Program_Globals_Flow_Sensitive"
subsection ‹What the configuration answers›
text ‹
Running ‹certificate_config› on ‹certificate_demo_prog› by evaluation: the
single check at ‹Statement 4› comes back ‹Check_Proved›.
›
lemma certificate_demo_report:
"(case run_voblint certificate_config
certificate_demo_prog of
Analysed res ⇒
map (λchk. (check_point chk, check_verdict chk)) (report_checks res)
= [(Statement 4, Decided Check_Proved)]
| _ ⇒ False)"
by eval
text ‹
The endpoint below reads a result, so the answer is named rather than only
inspected: \<^const>‹Analysed› is what this configuration returns on this
program, and the check above is the check column it returns.
›
lemma certificate_demo_analysed:
"∃res. run_voblint certificate_config
certificate_demo_prog = Analysed res
∧ map (λchk. (check_point chk, check_verdict chk)) (report_checks res)
= [(Statement 4, Decided Check_Proved)]"
using certificate_demo_report
by (cases "run_voblint certificate_config
certificate_demo_prog")
auto
subsection ‹One source run, constructed›
text ‹
The endpoint speaks about a source execution, so this one is built rather than
assumed: start every variable at ‹0›, run both calls and the check, and end with
‹a = 2› and ‹b = 42›. Two facts about the source semantics are needed and are
general rather than about this program --- a check steps to \<^const>‹SKIP›
without touching the store, and a call whose body is a single \<^const>‹Return›
completes in three steps: enter the callee, publish the return value, and pop
the frame writing the destination.
›
lemma pcompletes_Check: "pcompletes 𝒢 Π (VIMP_Proc.gcom.Check () l cond) s s"
by (rule star.step) (rule pstep.Check, rule star.refl)
lemma pcompletes_Call_return:
assumes p: "Π p = Some decl"
and bd: "body decl = VIMP_Proc.gcom.Return () (Some e)"
and arity: "length actuals = length (formals decl)"
and dist: "distinct (formals decl)"
and glob: "¬ 𝒢 ret_var"
shows "pcompletes 𝒢 Π (VIMP_Proc.gcom.Call () dst p actuals) s
(combine_assign dst
(⟦e⟧⇩e (bind_formals (formals decl) (map (λa. ⟦a⟧⇩e s) actuals)
(enter_state 𝒢 s)))
(combine_env 𝒢 s
(bind_formals (formals decl) (map (λa. ⟦a⟧⇩e s) actuals)
(enter_state 𝒢 s))))"
proof -
let ?callee = "bind_formals (formals decl) (map (λa. ⟦a⟧⇩e s) actuals) (enter_state 𝒢 s)"
let ?entered =
"VIMP_Proc.gcom.Seq (VIMP_Proc.gcom.Return () (Some e)) (VIMP_Proc.gcom.Restore ())"
let ?unwinding = "VIMP_Proc.gcom.Seq (VIMP_Proc.gcom.Unwind ()) (VIMP_Proc.gcom.Restore ())"
have c1: "𝒢, Π ⊢ (VIMP_Proc.gcom.Call () dst p actuals, s, [])
→⇩p (?entered, ?callee, [Frame s dst])"
using arity bd dist p pstep_Call by fastforce
have c2: "𝒢, Π ⊢ (?entered, ?callee, [Frame s dst])
→⇩p (?unwinding, ?callee(ret_var := ⟦e⟧⇩e ?callee), [Frame s dst])"
by (rule pstep.Seq2) (rule pstep.ReturnSome)
have c3: "𝒢, Π ⊢ (?unwinding, ?callee(ret_var := ⟦e⟧⇩e ?callee), [Frame s dst])
→⇩p (VIMP_Proc.gcom.SKIP (),
combine_assign dst (⟦e⟧⇩e ?callee) (combine_env 𝒢 s ?callee), [])"
using pstep.UnwindAct [where 𝒢 = 𝒢 and Π = Π and dst = dst and fr = s and frs = "[]"
and s = "?callee(ret_var := ⟦e⟧⇩e ?callee)"]
by (simp add: glob)
show ?thesis
using c1 c2 c3 by (meson star.refl star.step)
qed
lemma certificate_demo_table:
"prog_table certificate_demo_prog (STR ''bump'')
= Some ⦇formals = [STR ''n''],
body = VIMP_Proc.gcom.Return () (Some (Plus (V (STR ''n'')) (N 1)))⦈"
by (simp add: certificate_demo_prog_def prog_main_name_def)
lemma certificate_demo_main:
"main_body (prog_table certificate_demo_prog)
= VIMP_Proc.gcom.Seq
(VIMP_Proc.gcom.Seq (VIMP_Proc.gcom.Call () (Some (STR ''a'')) (STR ''bump'') [N 1])
(VIMP_Proc.gcom.Call () (Some (STR ''b'')) (STR ''bump'') [N 41]))
(VIMP_Proc.gcom.Check () (0, 0) (Less (N 0) (V (STR ''b''))))"
by (simp add: certificate_demo_prog_def main_body_def prog_main_name_def)
lemma certificate_demo_no_globals: "declared_global certificate_demo_prog = (λ_. False)"
by (simp add: certificate_demo_prog_def fun_eq_iff)
lemma certificate_demo_call:
"pcompletes (declared_global certificate_demo_prog) (prog_table certificate_demo_prog)
(VIMP_Proc.gcom.Call () (Some x) (STR ''bump'') [N k]) s (s(x := k + 1))"
using pcompletes_Call_return
[where Π = "prog_table certificate_demo_prog" and p = "STR ''bump''"
and decl = "⦇formals = [STR ''n''],
body = VIMP_Proc.gcom.Return () (Some (Plus (V (STR ''n'')) (N 1)))⦈"
and e = "Plus (V (STR ''n'')) (N 1)" and actuals = "[N k]" and dst = "Some x"
and 𝒢 = "declared_global certificate_demo_prog" and s = s,
OF certificate_demo_table]
by (simp add: certificate_demo_no_globals enter_state_def combine_env_def)
lemma certificate_demo_calls:
"pcompletes (declared_global certificate_demo_prog) (prog_table certificate_demo_prog)
(VIMP_Proc.gcom.Seq (VIMP_Proc.gcom.Call () (Some (STR ''a'')) (STR ''bump'') [N 1])
(VIMP_Proc.gcom.Call () (Some (STR ''b'')) (STR ''bump'') [N 41]))
(λ_. 0) ((λ_. 0)(STR ''a'' := 2, STR ''b'' := 42))"
proof -
have c1: "pcompletes (declared_global certificate_demo_prog)
(prog_table certificate_demo_prog)
(VIMP_Proc.gcom.Call () (Some (STR ''a'')) (STR ''bump'') [N 1]) (λ_. 0)
((λ_. 0)(STR ''a'' := 2))"
using certificate_demo_call [where x = "STR ''a''" and k = 1 and s = "λ_. 0"] by simp
have c2: "pcompletes (declared_global certificate_demo_prog)
(prog_table certificate_demo_prog)
(VIMP_Proc.gcom.Call () (Some (STR ''b'')) (STR ''bump'') [N 41])
((λ_. 0)(STR ''a'' := 2))
((λ_. 0)(STR ''a'' := 2, STR ''b'' := 42))"
using certificate_demo_call
[where x = "STR ''b''" and k = 41 and s = "(λ_. 0)(STR ''a'' := 2)"]
by simp
show ?thesis by (rule pcompletes_Seq [OF c1 c2])
qed
lemma certificate_demo_run:
"pcompletes (declared_global certificate_demo_prog) (prog_table certificate_demo_prog)
(main_body (prog_table certificate_demo_prog)) (λ_. 0)
((λ_. 0)(STR ''a'' := 2, STR ''b'' := 42))"
unfolding certificate_demo_main
by (rule pcompletes_Seq [OF certificate_demo_calls pcompletes_Check])
text ‹The same run stopped one step short of the check: both calls are done and
\<^const>‹VIMP_Proc.gcom.Check› is the command about to run.›
lemma certificate_demo_to_check:
"declared_global certificate_demo_prog, prog_table certificate_demo_prog ⊢ (main_body (prog_table certificate_demo_prog), λ_. 0, [])
→⇩p⇧* (VIMP_Proc.gcom.Check () (0, 0) (Less (N 0) (V (STR ''b''))),
(λ_. 0)(STR ''a'' := 2, STR ''b'' := 42), [])"
unfolding certificate_demo_main
using psteps_Seq2 [OF certificate_demo_calls] by (meson Seq1 star.step star.refl star_trans)
lemma certificate_demo_init: "(λ_. 0) ∈ cinit_stores (declared_global certificate_demo_prog)"
by (simp add: cinit_stores_def)
subsection ‹The same run in the graph, at a node this theory can name›
text ‹
\<^const>‹csim› is structural and not functional, so the endpoint below can only
say ∗‹some› node represents where the run stopped. Naming the check's own node
takes a second witness, built in the graph rather than in the source: the
collecting semantics at ‹Statement 4› really does contain the store this
program computes, which is what makes the verdict claim there bite.
Walking it takes one hop the collecting vocabulary does not close over
step by step: \<^const>‹node_collect› is closed under intra edges but not under a
call or a return alone, since a return has to pop the trace's ∗‹own› caller.
A call and its matching return together do compose, and that is
‹node_collect_call_return_step› in
\<^theory>‹Voblint_CFG.Activation_Trace_Collect›; the two hops through ‹bump› below are its two
instances.
›
lemma certificate_demo_entry_eval:
"cfg_entry (prog_cfg certificate_demo_prog) = FunctionEntry (STR ''main'')"
by (simp only: prog_cfg_def cfg_entry_compile_prog prog_main_name_def)
lemma certificate_demo_intra_eval:
"intra (prog_cfg certificate_demo_prog) =
{(FunctionEntry (STR ''bump''), EA_Body (STR ''bump''), Statement 0),
(Statement 0, EA_Ret (Some (Plus (V (STR ''n'')) (N 1))) (STR ''bump''),
FunctionResult (STR ''bump'')),
(Statement 1, EA_Ret None (STR ''bump''), FunctionResult (STR ''bump'')),
(FunctionEntry (STR ''main''), EA_Body (STR ''main''), Statement 2),
(Statement 5, EA_Ret None (STR ''main''), FunctionResult (STR ''main'')),
(Statement 4, EA_Check (0, 0) (Less (N 0) (V (STR ''b''))), Statement 5)}"
unfolding prog_cfg_def by eval
lemma certificate_demo_calls_eval:
"calls (prog_cfg certificate_demo_prog) =
{(Statement 3, CallEdge (Some (STR ''b'')) [STR ''n''] [N 41],
FunctionEntry (STR ''bump''), Statement 4),
(Statement 2, CallEdge (Some (STR ''a'')) [STR ''n''] [N 1],
FunctionEntry (STR ''bump''), Statement 3)}"
unfolding prog_cfg_def by eval
text ‹
A call to ‹bump› runs its whole body inside the callee's own activation: enter
with the formal bound, take the body edge, then the return edge, which is where
the returned value is published.
›
lemma certificate_demo_bump_body:
"intra_path (prog_cfg certificate_demo_prog)
(FunctionEntry (STR ''bump''), (λ_. 0)(STR ''n'' := k))
(FunctionResult (STR ''bump''), ((λ_. 0)(STR ''n'' := k))(ret_var := k + 1))"
proof (rule star_trans)
show "intra_path (prog_cfg certificate_demo_prog)
(FunctionEntry (STR ''bump''), (λ_. 0)(STR ''n'' := k))
(Statement 0, (λ_. 0)(STR ''n'' := k))"
by (rule intra_path_single [where a = "EA_Body (STR ''bump'')"])
(auto simp: certificate_demo_intra_eval)
next
show "intra_path (prog_cfg certificate_demo_prog)
(Statement 0, (λ_. 0)(STR ''n'' := k))
(FunctionResult (STR ''bump''), ((λ_. 0)(STR ''n'' := k))(ret_var := k + 1))"
by (rule intra_path_single
[where a = "EA_Ret (Some (Plus (V (STR ''n'')) (N 1))) (STR ''bump'')"])
(auto simp: certificate_demo_intra_eval)
qed
text ‹
The two store maps a call crosses, at this program's one procedure: entry resets
the locals and binds the formal, and the return writes the published value into
the destination while the caller keeps its own locals. No globals are declared,
so nothing survives entry but the binding.
›
lemma certificate_demo_enter:
"call_enter (declared_global certificate_demo_prog) (CallEdge dst [STR ''n''] [e]) s
= (λ_. 0)(STR ''n'' := ⟦e⟧⇩e s)"
by (simp add: certificate_demo_no_globals call_enter_CallEdge enter_binding_def
enter_frame_def fun_eq_iff)
lemma certificate_demo_combine:
"combine_collect (declared_global certificate_demo_prog) (Some x) s
(((λ_. 0)(STR ''n'' := k))(ret_var := v)) = s(x := v)"
by (simp add: certificate_demo_no_globals combine_collect_def combine_env_def
ret_var_def fun_eq_iff)
lemma certificate_demo_reaches_check:
"(λ_. 0)(STR ''a'' := 2, STR ''b'' := 42)
∈ 𝒞⇘declared_global certificate_demo_prog,prog_cfg certificate_demo_prog,cinit_stores (declared_global certificate_demo_prog)⇙ (Statement 4)"
proof -
have e0: "(λ_. 0) ∈ 𝒞⇘declared_global certificate_demo_prog,prog_cfg certificate_demo_prog,cinit_stores (declared_global certificate_demo_prog)⇙
(FunctionEntry (STR ''main''))"
using node_collect_init
[OF certificate_demo_init,
where 𝒢 = "declared_global certificate_demo_prog"
and g = "prog_cfg certificate_demo_prog"]
by (simp add: certificate_demo_entry_eval)
have s2:
"(λ_. 0) ∈ 𝒞⇘declared_global certificate_demo_prog,prog_cfg certificate_demo_prog,cinit_stores (declared_global certificate_demo_prog)⇙ (Statement 2)"
by (rule node_collect_intra_step [OF e0, where a = "EA_Body (STR ''main'')"])
(auto simp: certificate_demo_intra_eval)
have ce1: "(Statement 2, CallEdge (Some (STR ''a'')) [STR ''n''] [N 1],
FunctionEntry (STR ''bump''), Statement 3)
∈ calls (prog_cfg certificate_demo_prog)"
by (simp add: certificate_demo_calls_eval)
have bd1: "intra_path (prog_cfg certificate_demo_prog)
(FunctionEntry (STR ''bump''),
call_enter (declared_global certificate_demo_prog)
(CallEdge (Some (STR ''a'')) [STR ''n''] [N 1]) (λ_. 0))
(FunctionResult (STR ''bump''), ((λ_. 0)(STR ''n'' := 1))(ret_var := 1 + 1))"
using certificate_demo_bump_body [where k = 1]
by (simp add: certificate_demo_enter)
have s3: "(λ_. 0)(STR ''a'' := 2)
∈ 𝒞⇘declared_global certificate_demo_prog,prog_cfg certificate_demo_prog,cinit_stores (declared_global certificate_demo_prog)⇙ (Statement 3)"
using node_collect_call_return_step [OF s2 ce1 bd1]
by (simp add: certificate_demo_combine)
have ce2: "(Statement 3, CallEdge (Some (STR ''b'')) [STR ''n''] [N 41],
FunctionEntry (STR ''bump''), Statement 4)
∈ calls (prog_cfg certificate_demo_prog)"
by (simp add: certificate_demo_calls_eval)
have bd2: "intra_path (prog_cfg certificate_demo_prog)
(FunctionEntry (STR ''bump''),
call_enter (declared_global certificate_demo_prog)
(CallEdge (Some (STR ''b'')) [STR ''n''] [N 41]) ((λ_. 0)(STR ''a'' := 2)))
(FunctionResult (STR ''bump''), ((λ_. 0)(STR ''n'' := 41))(ret_var := 41 + 1))"
using certificate_demo_bump_body [where k = 41]
by (simp add: certificate_demo_enter)
show ?thesis
using node_collect_call_return_step [OF s3 ce2 bd2]
by (simp add: certificate_demo_combine)
qed
subsection ‹What the solve owes›
text ‹
The solver's own run is the first. \<^const>‹dg_pipeline.root_query› has no
code equation of its own --- its type does not mention the domain, so the
generator cannot see its sort hypothesis --- and a call-string bound is a
runtime argument, so no registration inlined it here. Unfolding it once is what
the reflection below needs to reach ‹eval›.
›
lemma certificate_demo_solve_c:
"TD_side_rule_Interp_solve_c Globals_Join
(dg_pipeline.equations (mcp_comp (activation certificate_analyses))
(mcp_init (activation certificate_analyses))
Analysis_Buffer (Analysis_Global :: vname ⇒ (vname, cfg_node list) global_unknown)
Activation_Seed (λ_. cs_route 1) []
(λ𝒢 c. dg_spec_of c) (λ𝒢 d. Bot) (λ𝒢 p. [])
(declared_global certificate_demo_prog) certificate_demo_prog)
(dg_pipeline.root_query [] certificate_demo_prog) ≠ None"
unfolding dg_pipeline.root_query_def by eval
lemma certificate_demo_terminates:
"mcp_cs_rule.terminates certificate_analyses 1 Globals_Join
(declared_global certificate_demo_prog) certificate_demo_prog"
by (rule mcp_cs_rule.terminates_of_solve_c [OF certificate_demo_solve_c])
text ‹
The theorems below owe no termination fact: an analysed answer exists only where
the executable solve returned. The lemma above evaluates termination anyway,
because the table lemma below is stated about this configuration's own solve.
›
subsection ‹What the printed verdict means at that node›
text ‹
The check the configuration lists carries its own expression, so it is worth
reading back in full rather than by point and verdict alone.
›
lemma certificate_demo_report_full:
"(case run_voblint certificate_config
certificate_demo_prog of
Analysed res ⇒
map (λchk. (check_point chk, check_exp chk, check_verdict chk)) (report_checks res)
= [(Statement 4, Less (N 0) (V (STR ''b'')), Decided Check_Proved)]
| _ ⇒ False)"
by eval
lemma certificate_demo_check:
assumes ans: "run_voblint certificate_config
certificate_demo_prog = Analysed res"
shows "∃chk. report_checks res = [chk] ∧ check_point chk = Statement 4
∧ check_exp chk = Less (N 0) (V (STR ''b''))
∧ check_verdict chk = Decided Check_Proved"
using certificate_demo_report_full assms by (cases "report_checks res") auto
text ‹
The table this configuration's own solve builds, and the fact that it is sound for
this program: \<^const>‹analysis_report_of› builds its report from exactly this
table.
›
abbreviation certificate_demo_table where
"certificate_demo_table ≡
mcp_cs_rule.result certificate_analyses 1 Globals_Join (declared_global certificate_demo_prog)
certificate_demo_prog"
lemma certificate_demo_covered_table:
"covered_table certificate_demo_prog certificate_demo_table
(mcp_gamma_v (activation certificate_analyses))"
by (rule activation_table.covered [OF mcp_cs_rule_table
[OF wf_program_compile_input_exec_sound [OF certificate_demo_wf]
certificate_demo_terminates]])
text ‹
The endpoint's report conjunct, at the check's node rather than at an existential
witness: the store the program computes lies in the report's semantics at that
node, that is, in the state filed there under the context the run's own call string
produced.
›
lemma certificate_demo_report_covers_at_check:
assumes ans: "run_voblint certificate_config certificate_demo_prog = Analysed res"
shows "(λ_. 0)(STR ''a'' := 2, STR ''b'' := 42) ∈ ℛ⇘res⇙ (Statement 4)"
using run_voblint_covers [OF ans] certificate_demo_reaches_check by blast
text ‹
And the endpoint's verdict conjunct at the same node: the \<^const>‹Check_Proved› the
report lists is not a claim about the analyzer's table but about every execution the
semantics admits there.
›
lemma certificate_demo_verdicts_at_check:
assumes ans: "run_voblint certificate_config
certificate_demo_prog = Analysed res"
and mem:
"s ∈ 𝒞⇘declared_global certificate_demo_prog,prog_cfg certificate_demo_prog,cinit_stores (declared_global certificate_demo_prog)⇙ (Statement 4)"
shows "s ∈ 𝒱⇘res⇙ (Statement 4)"
using run_voblint_collect_sound [OF ans] mem by blast
theorem certificate_demo_check_semantically_true:
assumes ans: "run_voblint certificate_config
certificate_demo_prog = Analysed res"
shows "∀s ∈ 𝒞⇘declared_global certificate_demo_prog,prog_cfg certificate_demo_prog,cinit_stores (declared_global certificate_demo_prog)⇙ (Statement 4).
truthy (⟦Less (N 0) (V (STR ''b''))⟧⇩e s)"
proof (intro ballI)
fix s :: store
assume mem:
"s ∈ 𝒞⇘declared_global certificate_demo_prog,prog_cfg certificate_demo_prog,cinit_stores (declared_global certificate_demo_prog)⇙ (Statement 4)"
obtain chk where r: "report_checks res = [chk]" and rp: "check_point chk = Statement 4"
and re: "check_exp chk = Less (N 0) (V (STR ''b''))"
and rv: "check_verdict chk = Decided Check_Proved"
using certificate_demo_check [OF ans] by blast
from certificate_demo_verdicts_at_check [OF ans mem] r rp re rv
show "truthy (⟦Less (N 0) (V (STR ''b''))⟧⇩e s)"
unfolding verdict_stores_eq by simp
qed
text ‹
Everything above, in one place and with every witness named. The generic endpoint
is existential in the node and the frame stack because \<^const>‹csim› is
structural; here the node is ‹Statement 4›, the store is the one the program
computes, and the answer is the one \<^const>‹run_voblint› returns --- so each
conjunct of the headline theorem can be read off separately rather than inferred
from an existential.
›
theorem certificate_demo_full_certificate:
obtains res where
"run_voblint certificate_config
certificate_demo_prog = Analysed res"
"map (λchk. (check_point chk, check_exp chk, check_verdict chk)) (report_checks res)
= [(Statement 4, Less (N 0) (V (STR ''b'')), Decided Check_Proved)]"
"pcompletes (declared_global certificate_demo_prog) (prog_table certificate_demo_prog)
(main_body (prog_table certificate_demo_prog)) (λ_. 0)
((λ_. 0)(STR ''a'' := 2, STR ''b'' := 42))"
"(λ_. 0)(STR ''a'' := 2, STR ''b'' := 42)
∈ 𝒞⇘declared_global certificate_demo_prog,prog_cfg certificate_demo_prog,cinit_stores (declared_global certificate_demo_prog)⇙ (Statement 4)"
"(λ_. 0)(STR ''a'' := 2, STR ''b'' := 42) ∈ ℛ⇘res⇙ (Statement 4)"
"(λ_. 0)(STR ''a'' := 2, STR ''b'' := 42) ∈ 𝒱⇘res⇙ (Statement 4)"
"truthy (⟦Less (N 0) (V (STR ''b''))⟧⇩e ((λ_. 0)(STR ''a'' := 2, STR ''b'' := 42)))"
proof (cases "run_voblint certificate_config
certificate_demo_prog")
case (Analysed res)
then have checks:
"map (λchk. (check_point chk, check_exp chk, check_verdict chk)) (report_checks res)
= [(Statement 4, Less (N 0) (V (STR ''b'')), Decided Check_Proved)]"
using certificate_demo_report_full by simp
have true_here:
"truthy (⟦Less (N 0) (V (STR ''b''))⟧⇩e ((λ_. 0)(STR ''a'' := 2, STR ''b'' := 42)))"
using certificate_demo_check_semantically_true [OF Analysed]
certificate_demo_reaches_check
by blast
show thesis
by (rule that [OF Analysed checks certificate_demo_run certificate_demo_reaches_check
certificate_demo_report_covers_at_check [OF Analysed]
certificate_demo_verdicts_at_check
[OF Analysed certificate_demo_reaches_check] true_here])
qed (use certificate_demo_report in simp_all)
subsection ‹The endpoint, with nothing left to assume›
text ‹
Nothing is left to assume. The run is the one built above and the answer is the one
computed above, so the endpoint's conclusion holds outright: the store the program
actually ends with lies in the report's semantics at its node, in the state the
always-join solve filed under that activation's own call string, and the
\<^const>‹Check_Proved› check the configuration listed is true of it.
›
theorem certificate_demo_source_certified:
"∃res v.
run_voblint certificate_config
certificate_demo_prog = Analysed res
∧ map (λchk. (check_point chk, check_verdict chk)) (report_checks res)
= [(Statement 4, Decided Check_Proved)]
∧ certificate_demo_prog, (λ_. 0) ⊢ (SKIP (), (λ_. 0)(STR ''a'' := 2, STR ''b'' := 42), []) ⊳ v
∧ (λ_. 0)(STR ''a'' := 2, STR ''b'' := 42)
∈ 𝒞⇘declared_global certificate_demo_prog,prog_cfg certificate_demo_prog,cinit_stores (declared_global certificate_demo_prog)⇙ v
∧ (λ_. 0)(STR ''a'' := 2, STR ''b'' := 42) ∈ ℛ⇘res⇙ v
∧ (λ_. 0)(STR ''a'' := 2, STR ''b'' := 42) ∈ 𝒱⇘res⇙ v"
proof (cases "run_voblint certificate_config
certificate_demo_prog")
case (Analysed res)
then have checks: "map (λchk. (check_point chk, check_verdict chk)) (report_checks res)
= [(Statement 4, Decided Check_Proved)]"
using certificate_demo_report by simp
from run_voblint_source_sound [OF certificate_demo_init certificate_demo_run Analysed]
obtain v where "certificate_demo_prog, (λ_. 0)
⊢ (SKIP (), (λ_. 0)(STR ''a'' := 2, STR ''b'' := 42), []) ⊳ v"
and "(λ_. 0)(STR ''a'' := 2, STR ''b'' := 42)
∈ 𝒞⇘declared_global certificate_demo_prog,prog_cfg certificate_demo_prog,cinit_stores (declared_global certificate_demo_prog)⇙ v"
and "(λ_. 0)(STR ''a'' := 2, STR ''b'' := 42) ∈ ℛ⇘res⇙ v"
and "(λ_. 0)(STR ''a'' := 2, STR ''b'' := 42) ∈ 𝒱⇘res⇙ v"
by blast
with Analysed checks show ?thesis by - (intro exI conjI; assumption)
qed (use certificate_demo_report in simp_all)
text ‹
The check theorem, with nothing left to assume. The run stopped just before the
check finds the report's check for the checked condition at a node that store
reaches, and the \<^const>‹Check_Proved› in it is true of the store.
›
theorem certificate_demo_check_listed_sound:
"∃res. run_voblint certificate_config
certificate_demo_prog = Analysed res
∧ (∃chk ∈ set (report_checks res). check_exp chk = Less (N 0) (V (STR ''b''))
∧ (λ_. 0)(STR ''a'' := 2, STR ''b'' := 42)
∈ 𝒞⇘declared_global certificate_demo_prog,prog_cfg certificate_demo_prog,cinit_stores (declared_global certificate_demo_prog)⇙ (check_point chk)
∧ check_verdict chk = Decided Check_Proved
∧ truthy (⟦Less (N 0) (V (STR ''b''))⟧⇩e
((λ_. 0)(STR ''a'' := 2, STR ''b'' := 42))))"
proof (cases "run_voblint certificate_config
certificate_demo_prog")
case (Analysed res)
have checks: "map (λchk. (check_point chk, check_verdict chk)) (report_checks res)
= [(Statement 4, Decided Check_Proved)]"
using certificate_demo_report Analysed by simp
from run_voblint_check_sound
[OF certificate_demo_init certificate_demo_to_check next_check.simps(1) Analysed]
obtain chk
where listed: "chk ∈ set (report_checks res)"
and re: "check_exp chk = Less (N 0) (V (STR ''b''))"
and mem: "(λ_. 0)(STR ''a'' := 2, STR ''b'' := 42)
∈ 𝒞⇘declared_global certificate_demo_prog,prog_cfg certificate_demo_prog,cinit_stores (declared_global certificate_demo_prog)⇙ (check_point chk)"
and pr: "check_verdict chk = Decided Check_Proved
⟶ truthy (⟦Less (N 0) (V (STR ''b''))⟧⇩e
((λ_. 0)(STR ''a'' := 2, STR ''b'' := 42)))"
by blast
have "(check_point chk, check_verdict chk) ∈ set [(Statement 4, Decided Check_Proved)]"
unfolding checks [symmetric] using listed by auto
then have "check_verdict chk = Decided Check_Proved" by simp
with Analysed listed re mem pr show ?thesis by blast
qed (use certificate_demo_report in simp_all)
end