Theory Inca_Verification

theory Inca_Verification
  imports Inca 
begin

context inca begin


section ‹Strongest postcondition›

inductive sp_instr for F ret where
  Push:
    "sp_instr F ret (IPush d) Σ (Suc Σ)" |
  Pop:
    "sp_instr F ret IPop (Suc Σ) Σ" |
  Get:
    "sp_instr F ret (IGet n) Σ (Suc Σ)" |
  Set:
    "sp_instr F ret (ISet n) (Suc Σ) Σ" |
  Load:
    "sp_instr F ret (ILoad x) (Suc Σ) (Suc Σ)" |
  Store:
    "sp_instr F ret (IStore x) (Suc (Suc Σ)) Σ" |
  Op:
    "Σi = 𝔄𝔯𝔦𝔱𝔶 op + Σ ⟹
    sp_instr F ret (IOp op) Σi (Suc Σ)" |
  OpInl:
    "Σi = 𝔄𝔯𝔦𝔱𝔶 (𝔇𝔢ℑ𝔫𝔩 opinl) + Σ ⟹
    sp_instr F ret (IOpInl opinl) Σi (Suc Σ)" |
  CJump:
    "sp_instr F ret (ICJump l⇩t l⇩f) 1 0" |
  Call:
    "F f = Some (ar, r) ⟹ Σi = ar + Σ ⟹ Σo = r + Σ ⟹
    sp_instr F ret (ICall f) Σi Σo" |
  Return: "Σi = ret ⟹
    sp_instr F ret IReturn Σi 0"

text ‹@{const sp_instr} calculates the strongest postcondition of the arity of the operand stack.›

inductive sp_instrs for F ret where
  Nil:
    "sp_instrs F ret [] Σ Σ" |
  Cons:
    "sp_instr F ret instr Σi Σ ⟹ sp_instrs F ret instrs Σ Σo ⟹
    sp_instrs F ret (instr # instrs) Σi Σo"


section ‹Range validations›

fun local_var_in_range where
  "local_var_in_range n (IGet k) ⟷ k < n" |
  "local_var_in_range n (ISet k) ⟷ k < n" |
  "local_var_in_range _ _ ⟷ True"

fun jump_in_range where
  "jump_in_range L (ICJump l⇩t l⇩f) ⟷ {l⇩t, l⇩f} ⊆ L" |
  "jump_in_range L _ ⟷ True"

fun fun_call_in_range where
  "fun_call_in_range F (ICall f) ⟷ f ∈ dom F" |
  "fun_call_in_range F instr ⟷ True"


section ‹Basic block validation›

definition wf_basic_block where
  "wf_basic_block F L ret n bblock ⟷
    (let (label, instrs) = bblock in
     list_all (local_var_in_range n) instrs ∧
     list_all (jump_in_range L) instrs ∧
     list_all (fun_call_in_range F) instrs ∧
     list_all (λi. ¬ Inca.is_jump i ∧ ¬ Inca.is_return i) (butlast instrs) ∧
     instrs ≠ [] ∧
     sp_instrs F ret instrs 0 0)"


section ‹Function definition validation›

definition wf_fundef where
  "wf_fundef F fd ⟷
    body fd ≠ [] ∧
    list_all
      (wf_basic_block F (fst ` set (body fd)) (return fd) (arity fd + fundef_locals fd))
      (body fd)"


section ‹Program definition validation›

definition wf_prog where
  "wf_prog p ⟷
    (let F = F_get (prog_fundefs p) in
     pred_map (wf_fundef (map_option funtype ∘ F)) F)"

end

end