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 lt lf) 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 lt lf)  {lt, lf}  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