Theory Voblint_Examples_Parity.Example_Parity_DG_Flagship
section ‹Flagship: parity analysis of an even-step loop, executed and certified on the D/G spine›
text ‹
❙‹Second domain, same assembly.› Parity reaches source-level soundness through
its own production unit-context registration ‹parity_rule›, at the always-join
rule ‹Globals_Join› --- the context-insensitive instance of the routed analysis --- with
∗‹no› example-local registration, ‹strategy_tree›, ‹Inl›/‹Inr›, or manual
post-solution transport lemmas. A VIMP program is compiled to a CFG; the generic
D/G framework generates the equation system; the ∗‹verified› always-join solver
∗‹computes› a parity solution inside Isabelle (the lattice is finite, so no
widening is needed); and the assembly's source-level soundness theorem lifts that
result to actual source runs.
The result is informative: the analysis ∗‹discovers› that ‹x› is even at
every program point (‹x = 0› initially, then ‹x := x + 2› preserves parity),
so the invariant holds without any guard refinement --- parity ignores the
guard. ‹Gcount›, incremented by one on the same back edge, alternates and
joins to ‹PTop›; the two locals therefore separate what the loop preserves
from what it destroys.
The local unknown carries the whole reachability-lifted ‹parity default_st›,
locals and ‹total› (the one declared global) alike, with no separate
flow-insensitive ‹G› slot to reconstruct through. ‹total› is therefore read back
exactly as ‹x› and ‹Gcount› are: through the local unknown at a program point,
not through a global summary.
›
theory Example_Parity_DG_Flagship
imports
"Voblint_Analysis_Parity.Parity_Analyses"
"Voblint_VIMP.VIMP_Notation"
begin
subsection ‹The VIMP source program›
text ‹
A bounded counting loop that increments by two: initialise ‹x› to ‹0›, add
‹2› while ‹x < 20›. No procedures beyond ‹main›; ‹x› is a single
flow-sensitive local, ‹Gcount› a second, ‹G›-prefixed local, and ‹total› the
one declared global despite carrying no naming hint. The parity of ‹x› stays
even at every reachable point regardless of the guard, which the analysis
must discover, not assume.
›
definition parity_program :: imp_prog where
"parity_program = program {
global total;
fun main() {
x = 0;
Gcount=1;
while (x < 20) {
x = x + 2;
Gcount=Gcount + 1;
}
total= x + Gcount;
}
}"
definition parity_prog :: "VIMP_Proc.com" where
"parity_prog = prog_main parity_program"
text ‹The storage classifier: ‹total› is declared global despite its plain
name, and ‹Gcount› stays local despite its ‹G› prefix, so ‹parity_gs› reads
the program's own declaration rather than a naming convention. The two
lemmas below pin both directions.›
abbreviation parity_gs :: "vname ⇒ bool" where
"parity_gs ≡ declared_global parity_program"
lemma parity_total_global [simp]: "parity_gs (STR ''total'')"
by (simp add: parity_program_def)
lemma parity_gcount_not_global [simp]: "¬ parity_gs (STR ''Gcount'')"
by (simp add: parity_program_def)
text ‹
The Base construction routes the whole abstract state through the local
unknown, reachability-lifted: ‹parity_lookup› reads a computed
‹default_st lifted› value back through \<^const>‹default_st_to_fun›,
matching Sign's own DG flagship -- a genuinely unreachable local unknown
(‹Bot›) reads back as ‹PTop›, never spuriously observed here since every
inspected node below is reachable.
›
abbreviation parity_lookup :: "parity default_st lifted ⇒ vname ⇒ parity" where
"parity_lookup d x ≡
(case ρ⇘parity_gs⇙ d of Lifted f ⇒ f x | Bot ⇒ PTop)"
definition parity_pi :: proc_table where
"parity_pi = prog_table parity_program"
subsection ‹CFG construction›
text ‹
The source compiles to an interprocedural CFG by ‹compile_prog›. The whole
program is the body of ‹main›, so it runs between
‹FunctionEntry (STR ''main'')› and ‹FunctionResult (STR ''main'')›, and the
compiler allocates one ‹Statement› point per command in source order: ‹0›
before ‹x := 0›, ‹1› before ‹Gcount := 1›, ‹2› the loop head carrying the
guard ‹x < 20›, ‹3› the loop body's first point before ‹x := x + 2›, ‹4›
before ‹Gcount := Gcount + 1› (whose edge closes the loop back to ‹2›), ‹5›
where the guard's false edge leaves the loop, and ‹6› after
‹total := x + Gcount›. The readings further below inspect ‹2› and ‹5›.
›
definition parity_cfg :: cfg where
"parity_cfg = compile_prog parity_pi []"
text ‹Interpreting \<^locale>‹compiled_cfg› at that defining equation supplies
finiteness of both edge relations, the entry and exit nodes, and
well-formedness at once, already phrased in this file's own graph name.›
interpretation parity_flagship: compiled_cfg parity_pi "[]" parity_cfg
by (unfold_locales; unfold parity_cfg_def; simp add: compile_prog_finite)
lemma parity_cfg_prog_cfg: "parity_cfg = prog_cfg parity_program"
by (simp add: parity_cfg_def parity_pi_def prog_cfg_def parity_program_def)
lemma parity_wf: "wf_compile_input parity_gs parity_pi []"
unfolding wf_compile_input_def
by (auto simp: wf_compile_input_simps parity_pi_def parity_prog_def parity_program_def
split: if_splits)
subsection ‹Equation generation and the executable solve›
text ‹The equation system is ‹parity_rule.equations› at this program: the
routed generator at the unit context, over the local-state specification. The
always-join solver suffices because parity has finite height.›
definition parity_eqs ::
"pp × unit
⇒ (pp × unit, (unit, unit) global_unknown,
(parity default_st lifted, parity default_st lifted) dg_state) strategy_tree" where
"parity_eqs = parity_rule.equations parity_gs parity_program"
lemma parity_terminates_c:
"TD_side_rule_Interp_solve_c Globals_Join parity_eqs (cfg_exit parity_cfg, ()) ≠ None"
by eval
lemma parity_terminates: "parity_rule.terminates Globals_Join parity_gs parity_program"
unfolding parity_rule.terminates_code
using TD_side_rule_Interp.solve_dom_of_solve_c[OF parity_terminates_c]
by (simp add: parity_eqs_def parity_cfg_prog_cfg)
definition parity_sol ::
"(pp × unit) set
× (pp × unit + (unit, unit) global_unknown
⇒ (parity default_st lifted, parity default_st lifted) dg_state)" where
"parity_sol = TD_side_rule_Interp_solve Globals_Join parity_eqs (cfg_exit parity_cfg, ())"
subsection ‹Inspecting the certified result›
text ‹Four readings of the solved table, all through the same local unknown.
‹x› is ‹PEven› at the loop head and still ‹PEven› where the loop is left, so
the even-step invariant survives the join with the back edge. ‹Gcount› does
not survive it: incremented by one, it joins odd against even and reaches
‹PTop›. ‹total›, the declared global, is read at the same node out of the
same unknown as the two locals, and still carries its zero-initialised
‹PEven› there because the loop never writes it.›
lemma parity_head_computed:
"parity_lookup (dg_local (snd parity_sol (Inl (Statement 2, ())))) (STR ''x'') = PEven"
unfolding parity_sol_def parity_eqs_def by eval
lemma parity_head_gcount_computed:
"parity_lookup (dg_local (snd parity_sol (Inl (Statement 2, ())))) (STR ''Gcount'') = PTop"
unfolding parity_sol_def parity_eqs_def by eval
lemma parity_exit_computed:
"parity_lookup (dg_local (snd parity_sol (Inl (Statement 5, ())))) (STR ''x'') = PEven"
unfolding parity_sol_def parity_eqs_def by eval
lemma parity_exit_total_computed:
"parity_lookup (dg_local (snd parity_sol (Inl (Statement 5, ())))) (STR ''total'') = PEven"
unfolding parity_sol_def parity_eqs_def by eval
subsection ‹Source-level soundness through the production assembly›
text ‹
‹parity_rule.fun_route_source_sound› turns the single ▩‹by eval› solver success
‹parity_terminates_c› into a source-level guarantee: every reachable VIMP store
is described by the state published at its matched program point, under the one
context ‹()› the unit route names. No transport lemma,
\<^const>‹part_post_solution›, or equation about the function a carrier
state represents appears in this proof.
›
lemma parity_main_body [simp]: "main_body parity_pi = parity_prog"
by (simp add: main_body_def prog_main_name_def parity_pi_def parity_program_def
parity_prog_def)
theorem parity_source_run_sound:
assumes run: "parity_gs, parity_pi ⊢ (parity_prog, s, []) →⇩p⇧* (residual, t, frs)"
and init: "s ∈ cinit_stores parity_gs"
shows "∃v stk. parity_pi, parity_cfg, prog_main_name ⊢ (residual, t, frs) ≈ (v, t, stk)
∧ t ∈ γ (parity_rule.state_at Globals_Join parity_gs parity_program () v)"
proof -
have run':
"parity_gs, prog_table parity_program ⊢ (main_body (prog_table parity_program), s, []) →⇩p⇧* (residual, t, frs)"
using run by (simp flip: parity_pi_def)
have wf: "wf_compile_input parity_gs (prog_table parity_program) (prog_procs parity_program)"
using parity_wf parity_cfg_prog_cfg
by (simp add: parity_pi_def parity_program_def)
have unit_route: "⋀u ctx d ca s. route_unit u ctx d ca = enterc_unit u ctx s" by simp
show ?thesis
using parity_rule.fun_route_source_sound[OF unit_route wf parity_terminates init run']
by (simp add: parity_cfg_prog_cfg parity_pi_def)
qed
subsection ‹The result is not vacuous›
text ‹
‹parity_source_run_sound› would say nothing if the state it reads through
concretized to all of \<^const>‹UNIV›. It does not: the published state at the
loop head maps ‹x› to ‹PEven›, whose concretization holds no odd integer, so
it rejects the constant store ‹λ_. 1›. A store is therefore genuinely
excluded, which is what makes the guarantee informative.
›
lemma parity_head_proper:
"parity_lookup (dg_local (snd parity_sol (Inl (Statement 2, ())))) (STR ''x'') ≠ PTop"
by (simp add: parity_head_computed)
lemma parity_head_excludes_odd:
fixes n :: int
assumes "n ∈ gamma_parity
(parity_lookup (dg_local (snd parity_sol (Inl (Statement 2, ())))) (STR ''x''))"
shows "even n"
using assms by (simp add: parity_head_computed)
lemma parity_state_at_head_x:
"parity_rule.state_at Globals_Join parity_gs parity_program () (Statement 2) (STR ''x'') = PEven"
unfolding parity_rule.state_at_unfold by eval
theorem parity_head_excludes_odd_store:
"(λ_. 1) ∉ γ (parity_rule.state_at Globals_Join parity_gs parity_program () (Statement 2))"
proof
assume "(λ_. 1) ∈ γ (parity_rule.state_at Globals_Join parity_gs parity_program () (Statement 2))"
then have "(1::int) ∈ gamma_parity
(parity_rule.state_at Globals_Join parity_gs parity_program () (Statement 2) (STR ''x''))"
by (simp add: gamma_state_def)
then show False by (simp add: parity_state_at_head_x)
qed
end