Theory VIMP_Proc

theory VIMP_Proc
  imports VIMP_Special "HOL-IMP.Star"
begin

section ‹Procedure commands and activation frames›

text ‹
  A call evaluates its actuals in the caller store, binds them in a fresh
  activation, and pushes a frame holding the caller store and the optional
  destination. ‹Restore› and ‹Unwind› never occur in source programs:
  ‹Restore› marks the activation boundary inside sequential syntax, and
  ‹Unwind› is the state after a ‹Return› has published its value through
  ‹ret_var›, discarding pending commands up to the nearest ‹Restore›.

  A check carries a label naming where it was written. The semantics never reads
  it; compilation copies it onto the check's edge, and the analysis result lists
  each check under it, so a report can be matched to its source check by label
  instead of by position in a list. The CLI parser writes the line and column of
  the check's ▩‹__voblint_check› keyword; a program written in Isabelle
  notation carries the placeholder ‹(0, 0)›.
›

type_synonym check_label = "nat × nat"

text ‹Every statement carries an annotation ‹'a›. Source programs written by hand or
  produced by the parser carry ‹()›; elaboration replaces it with a statement identity.
  The semantics never reads it: a step copies the annotation of the command it reduces
  onto what it leaves behind, so a residual still names the statement it came from. The
  variable and expression payloads are parameters too, so a later resolved or typed
  front end instantiates the same command syntax.›
datatype ('a, 'v, 'e) gcom =
    is_SKIP: SKIP 'a
  | Assign 'a (assign_var: 'v) (assign_rhs: 'e)
  | Check  'a check_label (check_cond: 'e)
  | Seq    (seq_first: "('a, 'v, 'e) gcom") (seq_second: "('a, 'v, 'e) gcom")
  | If     'a (if_cond: 'e) (if_then: "('a, 'v, 'e) gcom") (if_else: "('a, 'v, 'e) gcom")
  | While  'a (while_cond: 'e) (while_body: "('a, 'v, 'e) gcom")
  | Call   'a (call_dest: "'v option") (call_proc: pname) (call_args: "'e list")
  | Return 'a (return_val: "'e option")
  | is_Restore: Restore 'a
  | Unwind 'a

type_synonym 'a acom = "('a, vname, exp) gcom"
type_synonym com = "unit acom"

text ‹The discriminators read as the equations they replace, so automation that used to
  substitute ‹c = SKIP› still finds the constructor.›
lemma is_SKIP_iff [simp]: "is_SKIP c ⟷ (∃i. c = SKIP i)"
  by (cases c) auto

lemma is_Restore_iff [simp]: "is_Restore c ⟷ (∃i. c = Restore i)"
  by (cases c) auto

text ‹Activation -- fresh locals and formal binding -- happens at the call site,
  so a declaration records only what a call site looks up by name.›
record 'a gproc_decl =
  formals :: "vname list"
  body    :: "'a acom"

type_synonym proc_decl = "unit gproc_decl"

text ‹The reserved local ‹ret_var› carries a published result to the restore
  boundary. It is absent from source programs, so a value-less completion
  leaves it at ‹enter_state›'s zero.›
definition ret_var :: vname where
  "ret_var = STR ''#ret''"

type_synonym 'a ptable = "pname ⇒ 'a gproc_decl option"
type_synonym proc_table = "unit ptable"

datatype frame = Frame (frame_store: store) (frame_dest: "vname option")

text ‹Formal binding is the same fold over the concrete store and over every
  abstract state, so it is one polymorphic abbreviation.›
abbreviation bind_formals :: "vname list ⇒ 'v list ⇒ (vname ⇒ 'v) ⇒ vname ⇒ 'v" where
  "bind_formals xs vs s ≡ fold (λ(x, v) st. st(x := v)) (zip xs vs) s"

lemma bind_formals_other:
  "x ∉ set xs ⟹ bind_formals xs vs s x = s x"
proof (induction xs arbitrary: vs s)
  case Nil then show ?case by simp
next
  case (Cons y ys)
  then show ?case by (cases vs) simp_all
qed

text ‹Whole procedure entry, for the same reason: reset every local to a chosen
  value, keep the globals, then bind the formals to the actuals evaluated in the
  caller's own state. Which state and which evaluator is all that separates the
  concrete entry from an abstract one -- the concrete semantics runs it at
  const‹aval› and the reset value ‹0›, an abstract domain at its own
  evaluator and its own ‹top› -- so it is one definition, not a concrete one
  with an ‹_abs› copy beside it.›
definition enter_binding ::
  "(vname ⇒ bool) ⇒ 'a ⇒ (exp ⇒ (vname ⇒ 'a) ⇒ 'a)
   ⇒ vname list ⇒ exp list ⇒ (vname ⇒ 'a) ⇒ (vname ⇒ 'a)"
where
  "enter_binding 𝒢 reset_val ev xs es s =
     bind_formals xs (map (λe. ev e s) es) (enter_frame 𝒢 reset_val s)"

text ‹The concrete instance, spelled out: this is the equation that lets a
  soundness statement about the shared constant be read as one about the entry
  store the source semantics actually builds.›
lemma enter_binding_concrete:
  "enter_binding 𝒢 0 aval xs es s
     = bind_formals xs (map (λe. ⟦e⟧e s) es) (enter_state 𝒢 s)"
  by (simp add: enter_binding_def enter_state_def)

text ‹The return-slot write is a pure per-variable update, generic in the codomain:
  the concrete VIMP semantics uses it at ‹store = vname ⇒ int›, and every abstract
  domain's own ‹vname ⇒ 'a› state reuses the same definition rather than restating
  an ‹_abs› copy of it.›
fun combine_assign :: "vname option ⇒ 'a ⇒ (vname ⇒ 'a) ⇒ (vname ⇒ 'a)" where
  "combine_assign None _ s = s"
| "combine_assign (Some x) v s = s(x := v)"

subsection ‹Frame-stack small-step semantics›

text ‹The reference semantics every soundness claim is ultimately about.  A configuration is
  a command, a store, and a stack of caller frames; a call pushes one frame and continues in
  the callee body followed by ‹Restore›, a return writes the return slot and hands control to
  ‹Unwind›, which discards the rest of the callee body until that ‹Restore› pops the frame.
  ‹Restore› and ‹Unwind› exist only here, in configurations the semantics builds; no source
  program contains them.›
inductive
  pstep :: "(vname ⇒ bool) ⇒ 'a ptable ⇒ 'a acom × store × frame list
                       ⇒ 'a acom × store × frame list ⇒ bool"
    ("(_,_ ⊢/ _ →p/ _)" [51, 51, 51, 51] 50)
  for 𝒢 :: "vname ⇒ bool" and Π :: "'a ptable"
where
  Assign:  "𝒢, Π ⊢ (Assign i x a, s, frs) →p (SKIP i, s(x := ⟦a⟧e s), frs)"
| Check:   "𝒢, Π ⊢ (Check i l c, s, frs) →p (SKIP i, s, frs)"
| Seq1:    "𝒢, Π ⊢ (Seq (SKIP i) c2, s, frs) →p (c2, s, frs)"
| Seq2:    "𝒢, Π ⊢ (c1, s, frs) →p (c1', s', frs')
             ⟹ 𝒢, Π ⊢ (Seq c1 c2, s, frs) →p (Seq c1' c2, s', frs')"
| IfTrue:  "truthy (⟦b⟧e s) ⟹ 𝒢, Π ⊢ (If i b c1 c2, s, frs) →p (c1, s, frs)"
| IfFalse: "¬ truthy (⟦b⟧e s) ⟹ 𝒢, Π ⊢ (If i b c1 c2, s, frs) →p (c2, s, frs)"
| While:   "𝒢, Π ⊢ (While i b c, s, frs)
                      →p (If i b (Seq c (While i b c)) (SKIP i), s, frs)"
| Call:    "Π p = Some decl
             ⟹ length actuals = length (formals decl)
             ⟹ distinct (formals decl)
             ⟹ vals = map (λe. ⟦e⟧e s) actuals
             ⟹ callee = bind_formals (formals decl) vals (enter_state 𝒢 s)
             ⟹ 𝒢, Π ⊢ (Call i dst p actuals, s, frs)
                 →p (Seq (body decl) (Restore i),
                  callee,
                  Frame s dst # frs)"
| Special: "special_table p = Some desc
             ⟹ classify_special desc actuals = Some sc
             ⟹ special_result sc s v
             ⟹ 𝒢, Π ⊢ (Call i (Some x) p actuals, s, frs) →p (SKIP i, s(x := v), frs)"
| RestoreStep:
    "𝒢, Π ⊢ (Restore i, s, Frame fr dst # frs)
       →p (SKIP i, combine_assign dst (s ret_var) (combine_env 𝒢 fr s), frs)"
| ReturnSome:
    "𝒢, Π ⊢ (Return i (Some e), s, frs)
       →p (Unwind i, s(ret_var := ⟦e⟧e s), frs)"
| ReturnNone:
    "𝒢, Π ⊢ (Return i None, s, frs) →p (Unwind i, s, frs)"
| UnwindDead:
    "¬ is_Restore c2
     ⟹ 𝒢, Π ⊢ (Seq (Unwind i) c2, s, frs) →p (Unwind i, s, frs)"
| UnwindAct:
    "𝒢, Π ⊢ (Seq (Unwind j) (Restore i), s, Frame fr dst # frs)
       →p (SKIP i, combine_assign dst (s ret_var) (combine_env 𝒢 fr s), frs)"

abbreviation
  psteps :: "(vname ⇒ bool) ⇒ 'a ptable ⇒ 'a acom × store × frame list
                        ⇒ 'a acom × store × frame list ⇒ bool"
    ("(_,_ ⊢/ _ →p*/ _)" [51, 51, 51, 51] 50)
where "psteps 𝒢 Π x y ≡ star (pstep 𝒢 Π) x y"

declare pstep.intros [simp, intro]

inductive_cases SkipSE[elim!]:
  "𝒢, Π ⊢ (SKIP i, s, frs) →p cfg"
inductive_cases AssignSE[elim!]:
  "𝒢, Π ⊢ (Assign i x a, s, frs) →p cfg"
inductive_cases CheckSE[elim!]:
  "𝒢, Π ⊢ (Check i l c, s, frs) →p cfg"
inductive_cases SeqSE[elim]:
  "𝒢, Π ⊢ (Seq c1 c2, s, frs) →p cfg"
inductive_cases IfSE[elim!]:
  "𝒢, Π ⊢ (If i b c1 c2, s, frs) →p cfg"
inductive_cases WhileSE[elim]:
  "𝒢, Π ⊢ (While i b c, s, frs) →p cfg"
inductive_cases CallSE[elim]:
  "𝒢, Π ⊢ (Call i dst p actuals, s, frs) →p cfg"
inductive_cases RestoreSE[elim!]:
  "𝒢, Π ⊢ (Restore i, s, frs) →p cfg"
inductive_cases ReturnSE[elim!]:
  "𝒢, Π ⊢ (Return i e, s, frs) →p cfg"
inductive_cases UnwindSE[elim!]:
  "𝒢, Π ⊢ (Unwind i, s, frs) →p cfg"

lemmas star_pstep_induct =
  star.induct[of "pstep 𝒢 Π", split_format(complete), case_names refl step]

subsection ‹Completing runs›

text ‹A run completes when it reaches ‹SKIP› with the frame stack it started
  with; ‹SKIP› under a non-empty stack is stuck, not finished.›
abbreviation pcompletes :: "(vname ⇒ bool) ⇒ proc_table ⇒ com ⇒ store ⇒ store ⇒ bool" where
  "pcompletes 𝒢 Π c s t ≡ 𝒢, Π ⊢ (c, s, []) →p* (SKIP (), t, [])"

lemma pcompletes_skip: "pcompletes 𝒢 Π (SKIP ()) s s"
  by (rule star.refl)

lemma pcompletes_assign: "pcompletes 𝒢 Π (Assign () x a) s (s(x := ⟦a⟧e s))"
  by simp

lemma pcompletes_special_nondet_int:
  "pcompletes 𝒢 Π (Call () (Some x) special_pname_nondet_int []) s (s(x := v))"
  by (simp add: special_table_def)

lemma psteps_Seq2:
  "𝒢, Π ⊢ (c1, s, frs) →p* (c1', s', frs')
   ⟹ 𝒢, Π ⊢ (Seq c1 c2, s, frs) →p* (Seq c1' c2, s', frs')"
  by (induction rule: star_pstep_induct) (auto intro: star.step)

lemma pcompletes_Seq:
  assumes "pcompletes 𝒢 Π c1 s s2" and "pcompletes 𝒢 Π c2 s2 t"
  shows "pcompletes 𝒢 Π (Seq c1 c2) s t"
  using psteps_Seq2[OF assms(1)] assms(2) by (meson Seq1 star.step star_trans)

lemma pcompletes_IfTrue:
  "truthy (⟦b⟧e s) ⟹ pcompletes 𝒢 Π c1 s t ⟹ pcompletes 𝒢 Π (If () b c1 c2) s t"
  by (meson IfTrue star.step)

lemma pcompletes_IfFalse:
  "¬ truthy (⟦b⟧e s) ⟹ pcompletes 𝒢 Π c2 s t ⟹ pcompletes 𝒢 Π (If () b c1 c2) s t"
  by (meson IfFalse star.step)

subsection ‹Frame-stack extension›

text ‹A step never inspects the frames below the one it works on, so any run stays valid
  with more callers underneath.  This is what lets a proof about a procedure in isolation be
  reused at an arbitrary call depth.›
lemma pstep_frame_extend:
  "𝒢, Π ⊢ (c, s, frs) →p (c', s', frs') ⟹
   𝒢, Π ⊢ (c, s, frs @ extra) →p (c', s', frs' @ extra)"
  by (induction "(c, s, frs)" "(c', s', frs')"
        arbitrary: c s frs c' s' frs' rule: pstep.induct)
     auto

lemma psteps_frame_extend:
  "𝒢, Π ⊢ (c, s, frs) →p* (c', s', frs') ⟹
   𝒢, Π ⊢ (c, s, frs @ extra) →p* (c', s', frs' @ extra)"
  by (induction rule: star_pstep_induct) (auto intro: pstep_frame_extend star.step)

lemma psteps_frame_mono:
  "𝒢, Π ⊢ (c, s, []) →p* (SKIP i, t, []) ⟹
   𝒢, Π ⊢ (c, s, extra) →p* (SKIP i, t, extra)"
  using psteps_frame_extend[where frs = "[]" and frs' = "[]" and extra = extra]
  by simp

subsection ‹Call completion›

text ‹Running a whole call in one step of reasoning: a body that finishes under its own
  frame lets the caller resume with the frame popped and the return slot written.  Callers
  use these instead of replaying the ‹Restore› bookkeeping at every call site.›
lemma combine_env_ret_var_irrelevant [simp]:
  "¬ 𝒢 ret_var ⟹ combine_env 𝒢 fr (t(ret_var := v)) = combine_env 𝒢 fr t"
  by (rule ext) simp

lemma psteps_Seq_Restore_body:
  assumes "𝒢, Π ⊢ (c, s0, [Frame fr dst]) →p* (SKIP i, t', [Frame fr dst])"
  shows "𝒢, Π ⊢ (Seq c (Restore j), s0, [Frame fr dst])
           →p* (SKIP j, combine_assign dst (t' ret_var) (combine_env 𝒢 fr t'), [])"
  using psteps_Seq2[OF assms] by (meson Seq1 RestoreStep star.refl star.step star_trans)

lemma pstep_Call:
  assumes "Π p = Some decl"
      and "length actuals = length (formals decl)"
      and "distinct (formals decl)"
  shows "𝒢, Π ⊢ (Call i dst p actuals, s, frs)
           →p (Seq (body decl) (Restore i),
            bind_formals (formals decl) (map (λe. ⟦e⟧e s) actuals) (enter_state 𝒢 s),
            Frame s dst # frs)"
  using assms by (rule Call) (rule refl)+

lemma pstep_Call_parameterless [intro]:
  assumes "Π p = Some (⦇formals = [], body = c⦈)"
  shows
    "𝒢, Π ⊢ (Call i dst p [], s, frs) →p (Seq c (Restore i), enter_state 𝒢 s, Frame s dst # frs)"
proof -
  have "𝒢, Π ⊢ (Call i dst p [], s, frs)
          →p (Seq (body (⦇formals = [], body = c⦈)) (Restore i),
           bind_formals (formals (⦇formals = [], body = c⦈))
             (map (λe. ⟦e⟧e s) []) (enter_state 𝒢 s),
           Frame s dst # frs)"
    using assms by (rule pstep_Call) simp_all
  then show ?thesis by simp
qed

text ‹A value reaches the destination only through an explicit ‹Return›;
  otherwise the destination receives ‹ret_var›'s ‹enter_state› value ‹0›.›
lemma pcompletes_Call:
  assumes p: "Π p = Some decl"
      and arity: "length actuals = length (formals decl)"
      and distinct_formals: "distinct (formals decl)"
      and body: "pcompletes 𝒢 Π (body decl)
                   (bind_formals (formals decl) (map (λe. ⟦e⟧e s) actuals) (enter_state 𝒢 s)) t'"
  shows "pcompletes 𝒢 Π (Call () dst p actuals) s
           (combine_assign dst (t' ret_var) (combine_env 𝒢 s t'))"
  by (rule star.step, rule pstep_Call[where Π = Π and p = p, OF p arity distinct_formals])
     (rule psteps_Seq_Restore_body[OF psteps_frame_mono[OF body]])

section ‹Source-program well-formedness›

text ‹
  Source syntax excludes the runtime markers const‹Restore› and
  const‹Unwind›. The reserved const‹ret_var› belongs to the
  call mechanism, so source expressions, assignments, destinations, and formal
  parameters cannot mention it.
›

subsection ‹Finite syntactic variable sets›

fun com_vnames :: "'a acom ⇒ vname set" where
  "com_vnames (SKIP _) = {}"
| "com_vnames (Assign _ x a) = insert x (exp_vnames a)"
| "com_vnames (Check _ l c) = exp_vnames c"
| "com_vnames (Seq c1 c2) = com_vnames c1 ∪ com_vnames c2"
| "com_vnames (If _ b c1 c2) =
    exp_vnames b ∪ com_vnames c1 ∪ com_vnames c2"
| "com_vnames (While _ b c) = exp_vnames b ∪ com_vnames c"
| "com_vnames (Call _ dst _ actuals) =
    (case dst of None ⇒ {} | Some x ⇒ {x}) ∪
    ⋃ (set (map exp_vnames actuals))"
| "com_vnames (Return _ e) = (case e of None ⇒ {} | Some a ⇒ exp_vnames a)"
| "com_vnames (Restore _) = {}"
| "com_vnames (Unwind _) = {}"

lemma finite_com_vnames [simp]: "finite (com_vnames c)"
  by (induction c) (auto split: option.splits)

fun source_com :: "'a acom ⇒ bool" where
  "source_com (SKIP _) = True"
| "source_com (Assign _ x a) = True"
| "source_com (Check _ l c) = True"
| "source_com (Seq c1 c2) = (source_com c1 ∧ source_com c2)"
| "source_com (If _ b c1 c2) = (source_com c1 ∧ source_com c2)"
| "source_com (While _ b c) = source_com c"
| "source_com (Call _ dst p actuals) = True"
| "source_com (Return _ e) = True"
| "source_com (Restore _) = False"
| "source_com (Unwind _) = False"

definition source_pi :: "'a ptable ⇒ bool" where
  "source_pi Π = (∀p decl. Π p = Some decl ⟶ source_com (body decl))"

definition source_exp :: "exp ⇒ bool" where
  "source_exp a ⟷ ret_var ∉ exp_vnames a"

definition valid_formal :: "(vname ⇒ bool) ⇒ vname ⇒ bool" where
  "valid_formal 𝒢 x ⟷ ¬ 𝒢 x ∧ x ≠ ret_var"

subsection ‹Procedure result contract›

text ‹
  Declarations carry no return-kind annotation. A body is a value provider when
  every syntactic way to finish the body reaches const‹Return› with a value.
  The analysis is conservative: a loop may fall through because its guard may be
  false, and a call resumes normally after its callee completes.
›

fun may_fallthrough :: "'a acom ⇒ bool" where
  "may_fallthrough (SKIP _) = True"
| "may_fallthrough (Assign _ _ _) = True"
| "may_fallthrough (Check _ _ _) = True"
| "may_fallthrough (Seq c1 c2) = (may_fallthrough c1 ∧ may_fallthrough c2)"
| "may_fallthrough (If _ _ c1 c2) = (may_fallthrough c1 ∨ may_fallthrough c2)"
| "may_fallthrough (While _ _ _) = True"
| "may_fallthrough (Call _ _ _ _) = True"
| "may_fallthrough (Return _ _) = False"
| "may_fallthrough (Restore _) = False"
| "may_fallthrough (Unwind _) = False"

fun may_return_none :: "'a acom ⇒ bool" where
  "may_return_none (Seq c1 c2) =
     (may_return_none c1 ∨ (may_fallthrough c1 ∧ may_return_none c2))"
| "may_return_none (If _ _ c1 c2) = (may_return_none c1 ∨ may_return_none c2)"
| "may_return_none (While _ _ c) = may_return_none c"
| "may_return_none (Return _ e) = (e = None)"
| "may_return_none _ = False"

fun may_return_value :: "'a acom ⇒ bool" where
  "may_return_value (Seq c1 c2) =
     (may_return_value c1 ∨ (may_fallthrough c1 ∧ may_return_value c2))"
| "may_return_value (If _ _ c1 c2) = (may_return_value c1 ∨ may_return_value c2)"
| "may_return_value (While _ _ c) = may_return_value c"
| "may_return_value (Return _ e) = (e ≠ None)"
| "may_return_value _ = False"

definition value_providing :: "'a acom ⇒ bool" where
  "value_providing c ⟷
     source_com c ∧ ¬ may_fallthrough c ∧
     ¬ may_return_none c ∧ may_return_value c"

subsection ‹Commands, declarations, and programs›

text ‹
  Every call names a declared procedure and supplies one actual per formal. A
  destination requires a value-providing callee; a destination-less call may
  discard a published value. Procedure formals are distinct local names, and the
  distinguished root command contains no return.
›

fun wf_source_com :: "'a ptable ⇒ 'a acom ⇒ bool" where
  "wf_source_com Π (SKIP _) = True"
| "wf_source_com Π (Assign _ x a) = (x ≠ ret_var ∧ source_exp a)"
| "wf_source_com Π (Check _ l c) = source_exp c"
| "wf_source_com Π (Seq c1 c2) = (wf_source_com Π c1 ∧ wf_source_com Π c2)"
| "wf_source_com Π (If _ b c1 c2) =
     (source_exp b ∧ wf_source_com Π c1 ∧ wf_source_com Π c2)"
| "wf_source_com Π (While _ b c) = (source_exp b ∧ wf_source_com Π c)"
| "wf_source_com Π (Call _ dst p actuals) =
     (case special_table p of
        Some desc ⇒
          classify_special desc actuals ≠ None ∧ list_all source_exp actuals ∧
          (case dst of None ⇒ False | Some x ⇒ x ≠ ret_var)
      | None ⇒
          (case Π p of
             None ⇒ False
           | Some decl ⇒
               length actuals = length (formals decl) ∧
               list_all source_exp actuals ∧
               (case dst of
                  None ⇒ True
                | Some x ⇒ x ≠ ret_var ∧ value_providing (body decl))))"
| "wf_source_com Π (Return _ e) = (case e of None ⇒ True | Some a ⇒ source_exp a)"
| "wf_source_com Π (Restore _) = False"
| "wf_source_com Π (Unwind _) = False"

fun no_return :: "'a acom ⇒ bool" where
  "no_return (Seq c1 c2) = (no_return c1 ∧ no_return c2)"
| "no_return (If _ _ c1 c2) = (no_return c1 ∧ no_return c2)"
| "no_return (While _ _ c) = no_return c"
| "no_return (Return _ _) = False"
| "no_return _ = True"

definition wf_proc_decl :: "(vname ⇒ bool) ⇒ 'a ptable ⇒ 'a gproc_decl ⇒ bool" where
  "wf_proc_decl 𝒢 Π decl ⟷
     distinct (formals decl) ∧
     list_all (valid_formal 𝒢) (formals decl) ∧
     wf_source_com Π (body decl)"

definition reserved_ret_var :: "(vname ⇒ bool) ⇒ bool" where
  "reserved_ret_var 𝒢 ⟷ ¬ 𝒢 ret_var"

text ‹The entry procedure is fixed: a program has exactly one, it is called ‹main›, and the
  parser rejects formals on it.  Naming it here rather than threading it as a parameter means
  the compiler and its contract take a table and a callee list and nothing else.›
definition prog_main_name :: pname where
  "prog_main_name = STR ''main''"

text ‹The entry body, looked up rather than passed alongside the table.  The lookup cannot
  fail where ‹wf_source_program› holds --- its second conjunct is exactly that the entry is
  declared --- so an undeclared entry is an invariant violation, and aborts in generated code
  rather than compiling to a plausible empty program.›
definition main_body :: "'a ptable ⇒ 'a acom" where
  "main_body Π =
     (case Π prog_main_name of
        Some decl ⇒ body decl
      | None ⇒ Code.abort (STR ''main_body: entry procedure not declared'') (λ_. SKIP undefined))"

text ‹Deliberately not ‹[simp]›: ‹wf_source_program›'s entry conjunct has the shape
  ‹Π prog_main_name = Some ⦇formals = [], body = main_body Π⦈›, against which
  this rule would rewrite ‹main_body Π› to itself.›
definition wf_source_program :: "(vname ⇒ bool) ⇒ 'a ptable ⇒ bool" where
  "wf_source_program 𝒢 Π ⟷
     reserved_ret_var 𝒢 ∧
     Π prog_main_name = Some (⦇formals = [], body = main_body Π⦈) ∧
     wf_source_com Π (main_body Π) ∧ no_return (main_body Π) ∧
     (∀p decl. Π p = Some decl ⟶ wf_proc_decl 𝒢 Π decl) ∧
     (∀p. Π p ≠ None ⟶ special_table p = None)"

text ‹The compiler-input well-formedness defined in the compiler session unfolds
  through this pair before reaching const‹wf_source_com›; every site
  discharging that obligation shares the unfold skeleton, so it is collected
  here and the downstream definition adds itself to the same collection.›
named_theorems wf_compile_input_simps

declare
  wf_proc_decl_def [wf_compile_input_simps]
  wf_source_program_def [wf_compile_input_simps]

lemma wf_source_com_source_com:
  "wf_source_com Π c ⟹ source_com c"
  by (induction c) (auto split: option.splits)

lemma wf_source_programD:
  assumes "wf_source_program 𝒢 Π"
  shows "reserved_ret_var 𝒢"
    and "Π prog_main_name = Some ⦇formals = [], body = main_body Π⦈"
    and "wf_source_com Π (main_body Π)"
    and "no_return (main_body Π)"
    and "Π p = Some decl ⟹ wf_proc_decl 𝒢 Π decl"
    and "Π p = Some decl ⟹ special_table p = None"
    and "source_pi Π"
    and "source_com (main_body Π)"
  using assms wf_source_com_source_com
  unfolding wf_source_program_def source_pi_def wf_proc_decl_def by blast+


section ‹The semantics is inhabited›

text ‹
  Every theorem above is conditional on a step or a run existing, so this theory ends by
  exhibiting one that exercises the parts most easily got wrong: a procedure call that pushes
  a frame, returns a value, and pops the frame again.  Globals are empty here, so nothing the
  callee wrote survives except the returned value --- which is what has to reach ‹x›.
›

definition witness_ret1_pi :: proc_table where
  "witness_ret1_pi p =
     (if p = STR ''ret1'' then Some ⦇formals = [], body = Return () (Some (N 1))⦈ else None)"

theorem pcompletes_witness:
  "∃t. pcompletes (λ_. False) witness_ret1_pi
         (Call () (Some (STR ''x'')) (STR ''ret1'') []) s t
     ∧ t (STR ''x'') = 1"
proof -
  let ?𝒢 = "λ_ :: vname. False"
  let ?fr = "[Frame s (Some (STR ''x''))]"
  let ?en = "enter_state ?𝒢 s"
  let ?s' = "?en(ret_var := ⟦N 1⟧e ?en)"
  let ?t  = "(combine_env ?𝒢 s ?s')(STR ''x'' := ⟦N 1⟧e ?en)"
  have q: "witness_ret1_pi (STR ''ret1'') = Some ⦇formals = [], body = Return () (Some (N 1))⦈"
    by (simp add: witness_ret1_pi_def)
  have s1: "?𝒢, witness_ret1_pi ⊢ (Call () (Some (STR ''x'')) (STR ''ret1'') [], s, [])
              →p (Seq (Return () (Some (N 1))) (Restore ()), ?en, ?fr)"
    using q by (rule pstep_Call_parameterless)
  have s2: "?𝒢, witness_ret1_pi ⊢ (Seq (Return () (Some (N 1))) (Restore ()), ?en, ?fr)
              →p (Seq (Unwind ()) (Restore ()), ?s', ?fr)"
    by (intro Seq2 ReturnSome)
  have s3: "?𝒢, witness_ret1_pi ⊢ (Seq (Unwind ()) (Restore ()), ?s', ?fr) →p (SKIP (), ?t, [])"
    using UnwindAct[of ?𝒢 witness_ret1_pi "()" "()" ?s' s "Some (STR ''x'')" "[]"] by simp
  from s1 s2 s3
  have "pcompletes ?𝒢 witness_ret1_pi (Call () (Some (STR ''x'')) (STR ''ret1'') []) s ?t"
    by (meson star.refl star.step)
  moreover have "?t (STR ''x'') = 1" by simp
  ultimately show ?thesis by blast
qed

end