# Theory BoolProgs

section ‹Boolean Programs›
theory BoolProgs
imports
CAVA_Base.CAVA_Base
begin

subsection ‹Syntax and Semantics›

datatype bexp = TT | FF | V nat | Not bexp | And bexp bexp | Or bexp bexp

type_synonym state = "bitset"

fun bval :: "bexp  state  bool" where
"bval TT s = True" |
"bval FF s = False" |
"bval (V n) s = bs_mem n s" |
"bval (Not b) s = (¬ bval b s)" |
"bval (And b1 b2) s = (bval b1 s & bval b2 s)" |
"bval (Or b1 b2) s = (bval b1 s | bval b2 s)"

datatype instr =
AssI "nat list" "bexp list" |
TestI bexp int |
ChoiceI "(bexp * int) list" |
GotoI int

type_synonym config =
type_synonym bprog =

text ‹
Semantics Notice:
To be equivalent in semantics with SPIN, there is no such thing as a
finite run:
\begin{itemize}
\item Deadlocks (i.e. empty Choice) are self-loops
\item program termination is self-loop
\end{itemize}
›

fun exec ::  where
"exec instr (pc,s) = (case instr of
AssI ns bs  let bvs = zip ns (map (λb. bval b s) bs) in
[(pc + 1, foldl (λs (n,bv). set_bit s n bv) s bvs)] |
TestI b d  [if bval b s then (pc+1, s) else (nat(int(pc+1)+d), s)] |
ChoiceI bis  let succs = [(nat(int(pc+1)+i), s) . (b,i) <- bis, bval b s]
in if succs = [] then [(pc,s)] else succs |
GotoI d  [(nat(int(pc+1)+d),s)])"

(* exec' is merely a stuttering optimization. It summarizes chains of choices
or jumps, as long as they go forward in the program. The forward-condition is
to ensure termination.

TODO: Make this explicit, and prove stuttering equivalence!
*)
function exec' :: "bprog  state  nat  nat list" where
"exec' ins s pc = (
if pc < array_length ins then (
case (array_get ins pc) of
AssI ns bs  [pc] |
TestI b d  (
if bval b s then exec' ins s (pc+1)
else let pc'=(nat(int(pc+1)+d)) in if pc'>pc then exec' ins s pc'
else [pc']
) |
ChoiceI bis  let succs = [(nat(int(pc+1)+i)) . (b,i) <- bis, bval b s]
in if succs = [] then [pc] else concat (map (λpc'. if pc'>pc then exec' ins s pc' else [pc']) succs) |
GotoI d  let pc' = nat(int(pc+1)+d) in (if pc'>pc then exec' ins s pc' else [pc'])
) else [pc]
)"
by pat_completeness auto
termination
apply (relation "measure (%(ins,s,pc). array_length ins - pc)")
apply auto
done

fun nexts1 ::  where
"nexts1 ins (pc,s) = (
if pc < array_length ins then
exec (array_get ins pc) (pc,s)
else
[(pc,s)])"

fun nexts ::  where
"nexts ins (pc,s) = concat (
map
(λ(pc,s). map (λpc. (pc,s)) (exec' ins s pc))
(nexts1 ins (pc,s))
)"

declare nexts.simps [simp del]

datatype
com = SKIP
| Assign "nat list" "bexp list"
| Seq    com  com
| GC  "(bexp * com)list"
| IfTE  bexp com com
| While  bexp com

locale BoolProg_Syntax begin
notation
Assign       ("_ ::= _" [999, 61] 61)
and Seq          ("_;/ _"  [60, 61] 60)
and GC           ("IF _ FI")
and IfTE         ("(IF _/ THEN _/ ELSE _)"  [0, 61, 61] 61)
and While        ("(WHILE _/ DO _)"  [0, 61] 61)
end

context begin interpretation BoolProg_Syntax .
fun comp' :: "com  instr list" where
"comp' SKIP = []" |
"comp' (Assign n b) = [AssI n b]" |
"comp' (c1;c2) = comp' c1 @ comp' c2" |
"comp' (IF gcs FI) =
(let cgcs = map (λ(b,c). (b,comp' c)) gcs in
let cc' = cc @ (if ins = [] then [] else [GotoI (int(length ins))]) in
let bis' = map (λ(b,i). (b, i + int(length cc'))) bis
in ((b,0)#bis', cc' @ ins)) in
let (bis,ins) = foldr addbc cgcs ([],[])
in ChoiceI bis # ins)" |
"comp' (IF b THEN c1 ELSE c2) =
(let ins1 = comp' c1 in let ins2 = comp' c2 in
let i1 = int(length ins1 + 1) in let i2 = int(length ins2)
in TestI b i1 # ins1 @ GotoI i2 # ins2)" |
"comp' (WHILE b DO c) =
(let ins = comp' c in
let i = int(length ins + 1)
in TestI b i # ins @ [GotoI (-(i+1))])"

(* a test: *)
value "comp' (IF [(V 0, [1,0] ::= [TT, FF]), (V 1, [0] ::= [TT])] FI)"

end

definition comp :: "com  bprog" where
"comp = array_of_list  comp'"

(*
Optimization

- Gotos: Resolve Goto-Chains: If a Goto referres to another Goto -- add the second offset to the first one.
If a Goto has a negative offset ignore it, to avoid problems with loops.

*)

fun opt' where
"opt' (GotoI d) ys = (let next = λi. (case i of GotoI d  d + 1 | _  0)
in if d < 0  nat d  length ys then (GotoI d)#ys
else let d' = d + next (ys ! nat d)
in (GotoI d' # ys))"
| "opt' x ys = x#ys"

definition opt ::  where
"opt instr = foldr opt' instr []"

definition optcomp :: "com  bprog" where
"optcomp  array_of_list  opt  comp'"

subsection ‹Finiteness of reachable configurations›

inductive_set reachable_configs
for bp :: bprog
and cs :: config ― ‹start configuration›
where
"cs  reachable_configs bp cs" |
"c  reachable_configs bp cs  x  set (nexts bp c)  x  reachable_configs bp cs"

lemmas reachable_configs_induct = reachable_configs.induct[split_format(complete),case_names 0 1]

fun offsets :: "instr  int set" where
"offsets (AssI _ _) = {0}" |
"offsets (TestI _ i) = {0,i}" |
"offsets (ChoiceI bis) = set(map snd bis)  {0}" |
"offsets (GotoI i) = {i}"

definition offsets_is ::  where
"offsets_is ins = (UN instr : set ins. offsets instr)"

definition max_next_pcs ::  where
"max_next_pcs ins = {nat(int(length ins + 1) + i) |i. i : offsets_is ins}"

lemma finite_max_next_pcs: "finite(max_next_pcs bp)"
proof-
{ fix instr have "finite (offsets instr)" by(cases instr) auto }
moreover
{ fix ins have "max_next_pcs ins = (UN i : offsets_is ins. {nat(int(length ins + 1) + i)})"
ultimately show ?thesis by(auto simp add: offsets_is_def)
qed

(* TODO: Move *)
lemma (in linorder) le_Max_insertI1: " finite A; x  b   x  Max (insert b A)"
by (metis Max_ge finite.insertI insert_iff order_trans)
lemma (in linorder) le_Max_insertI2: " finite A; A  {}; x  Max A   x  Max (insert b A)"
by(auto simp add: max_def not_le simp del: Max_less_iff)

lemma max_next_pcs_not_empty:
"pc<length bp  x : set (exec (bp!pc) (pc,s))  max_next_pcs bp  {}"
apply(drule nth_mem)
apply(fastforce simp: max_next_pcs_def offsets_is_def split: instr.splits)
done

lemma Max_lem2:
assumes "pc < length bp"
and "(pc', s')  set (exec (bp!pc) (pc, s))"
shows "pc'  Max (max_next_pcs bp)"
using assms
proof (cases "bp ! pc")
case (ChoiceI l)
show ?thesis
proof (cases "pc' = pc")
case True with assms ChoiceI show ?thesis
by (auto simp: Max_ge_iff max_next_pcs_not_empty finite_max_next_pcs)
(force simp add: max_next_pcs_def offsets_is_def dest: nth_mem)
next
case False with ChoiceI assms obtain b i where
bi: "bval b s" "(b,i)  set l" "pc' = nat(int(pc+1)+i)"
by (auto split: if_split_asm)
with ChoiceI assms have "i  (offsets  (set bp))" by (force dest: nth_mem)
with bi assms have "a. (a  max_next_pcs bp  pc'  a)"
unfolding max_next_pcs_def offsets_is_def by force
thus ?thesis
by (auto simp: Max_ge_iff max_next_pcs_not_empty[OF assms] finite_max_next_pcs)
qed
qed (auto simp: Max_ge_iff max_next_pcs_not_empty finite_max_next_pcs,
(force simp add: max_next_pcs_def offsets_is_def dest: nth_mem split: if_split_asm)+)

lemma Max_lem1: " pc < length bp; (pc', s')  set (exec (bp ! pc) (pc, s))
pc'  Max (insert x (max_next_pcs bp))"
apply(rule le_Max_insertI2)
apply(auto intro!: Max_lem2 simp del:exec.simps)
done

definition "pc_bound bp  max
(Max (max_next_pcs (list_of_array bp)) + 1)
(array_length bp + 1)"

declare exec'.simps[simp del]

lemma [simp]:  by (cases a) auto

lemma aux2:
assumes A: "pc < array_length ins"
assumes B: "ofs  offsets_is (list_of_array ins)"
shows "nat (1 + int pc + ofs) < pc_bound ins"
proof -
have "nat (int (1 + array_length ins) + ofs)
max_next_pcs (list_of_array ins)"
using B unfolding max_next_pcs_def
by auto
with A show ?thesis
unfolding pc_bound_def
apply -
apply (rule max.strict_coboundedI1)
apply auto
apply (drule Max_ge[OF finite_max_next_pcs])
apply simp
done
qed

lemma array_idx_in_set:
" pc < array_length ins; array_get ins pc = x
x  set (list_of_array ins)"
by (induct ins) auto

lemma rcs_aux:
assumes "pc < pc_bound bp"
assumes "pc'set (exec' bp s pc)"
shows "pc' < pc_bound bp"
using assms
proof (induction bp s pc arbitrary: pc' rule: exec'.induct[case_names C])
case (C ins s pc pc')
from C.prems show ?case
apply (subst (asm) exec'.simps)
apply (split if_split_asm instr.split_asm)+

apply (simp split: if_split_asm add: Let_def)
apply (frule (2) C.IH(1), auto) []
apply (auto simp: pc_bound_def) []
apply (frule (2) C.IH(2), auto) []
apply (rename_tac bexp int)
apply (subgoal_tac "int  offsets_is (list_of_array ins)")
apply (blast intro: aux2)
apply (auto simp: offsets_is_def) []
apply (rule_tac x="TestI bexp int" in bexI, auto simp: array_idx_in_set) []

apply (rename_tac list)
apply (auto split: if_split_asm)[]
apply (frule (1) C.IH(3), auto) []
apply (force)
apply (force)
apply (subgoal_tac "ba  offsets_is (list_of_array ins)")
apply (blast intro: aux2)
apply (auto simp: offsets_is_def) []
apply (rule_tac x="ChoiceI list" in bexI, auto simp: array_idx_in_set) []

apply (rename_tac int)
apply (simp split: if_split_asm add: Let_def)
apply (frule (1) C.IH(4), auto) []
apply (subgoal_tac "int  offsets_is (list_of_array ins)")
apply (blast intro: aux2)
apply (auto simp: offsets_is_def) []
apply (rule_tac x="GotoI int" in bexI, auto simp: array_idx_in_set) []

apply simp
done
qed

primrec bexp_vars :: "bexp  nat set" where
"bexp_vars TT = {}"
| "bexp_vars FF = {}"
| "bexp_vars (V n) = {n}"
| "bexp_vars (Not b) = bexp_vars b"
| "bexp_vars (And b1 b2) = bexp_vars b1  bexp_vars b2"
| "bexp_vars (Or b1 b2) = bexp_vars b1  bexp_vars b2"

primrec instr_vars :: "instr  nat set" where
"instr_vars (AssI xs bs) = set xs  (bexp_varsset bs)"
| "instr_vars (TestI b _) = bexp_vars b"
| "instr_vars (ChoiceI cs) = (bexp_varsfstset cs)"
| "instr_vars (GotoI _) = {}"

find_consts "'a array  'a list"

definition bprog_vars :: "bprog  nat set" where
"bprog_vars bp = (instr_vars`set (list_of_array bp))"

definition "state_bound bp s0
{s. bs_α s - bprog_vars bp = bs_α s0 - bprog_vars bp}"
abbreviation "config_bound bp s0  {0..< pc_bound bp} × state_bound bp s0"

lemma exec_bound:
assumes PCB: "pc < array_length bp"
assumes SB: "s  state_bound bp s0"
shows "set (exec (array_get bp pc) (pc,s))  config_bound bp s0"
proof (clarsimp simp del: exec.simps, intro conjI)

obtain instrs where BP_eq[simp]: "bp = Array instrs" by (cases bp)
from PCB have PCB'[simp]: "pc < length instrs" by simp

fix pc' s'
assume STEP: "(pc',s')  set (exec (array_get bp pc) (pc,s))"
hence STEP': "(pc',s')  set (exec (instrs!pc) (pc,s))" by simp

show "pc' < pc_bound bp"
using Max_lem2[OF PCB' STEP']
unfolding pc_bound_def by simp

show "s'  state_bound bp s0"
using STEP' SB
proof (cases "instrs!pc")
case (AssI xs vs)

have "set xs  instr_vars (instrs!pc)"
also have "  bprog_vars bp"
by (metis PCB' UN_upper nth_mem)
finally have XSB: "set xs  bprog_vars bp" .

{
fix x s v
assume A: "x  bprog_vars bp" "s  state_bound bp s0"

have SB_CNV: "bs_α (set_bit s x v)
= (if v then (insert x (bs_α s)) else (bs_α s - {x}))"
apply (cases v)
apply simp_all
apply (fold bs_insert_def bs_delete_def)
done

from A have "set_bit s x v  state_bound bp s0"
unfolding state_bound_def
by (auto simp: SB_CNV)
} note aux=this

{
fix vs
have "foldl (λs (x, y). set_bit s x y) s (zip xs vs)
state_bound (Array instrs) s0"
using SB XSB
apply (induct xs arbitrary: vs s)
apply simp
apply (case_tac vs)
apply simp
using aux
apply (auto)
done
} note aux2=this

thus ?thesis using STEP'
qed (auto split: if_split_asm)
qed

lemma in_bound_step:
notes [simp del] = exec.simps
assumes BOUND: "c  config_bound bp s0"
assumes STEP: "c'set (nexts bp c)"
shows "c'  config_bound bp s0"
using BOUND STEP
apply (cases c)
apply (auto
split: if_split_asm)
apply (frule (2) exec_bound[THEN subsetD])
apply clarsimp
apply (frule (1) rcs_aux)
apply simp

apply (frule (2) exec_bound[THEN subsetD])
apply clarsimp

apply (frule (1) rcs_aux)
apply simp
done

lemma reachable_configs_in_bound:
"c  config_bound bp s0  reachable_configs bp c  config_bound bp s0"
proof
fix c'
assume "c'  reachable_configs bp c" "c  config_bound bp s0"
thus "c'  config_bound bp s0"
apply induction
apply simp
by (rule in_bound_step)
qed

lemma reachable_configs_out_of_bound: "(pc',s')reachable_configs bp (pc,s)
¬ pc < pc_bound bp  (pc',s') = (pc,s)"
proof (induct rule: reachable_configs_induct)
case (1 pc' s' pc'' s'')
hence [simp]: "pc'=pc" "s'=s" by auto
from 1(4) have "¬ pc < array_length bp" unfolding pc_bound_def by auto
with 1(3) show ?case
by (auto simp add: nexts.simps exec'.simps)
qed auto

lemma finite_bexp_vars[simp, intro!]: "finite (bexp_vars be)"
by (induction be) auto

lemma finite_instr_vars[simp, intro!]: "finite (instr_vars ins)"
by (cases ins) auto

lemma finite_bprog_vars[simp, intro!]: "finite (bprog_vars bp)"
unfolding bprog_vars_def by simp

lemma finite_state_bound[simp, intro!]: "finite (state_bound bp s0)"
unfolding state_bound_def
apply (rule finite_imageD[where f=bs_α])
apply (rule finite_subset[where
B = "{s. s - bprog_vars bp = bs_α s0 - bprog_vars bp}"])
apply auto []
apply (rule finite_if_eq_beyond_finite)
apply simp

apply (rule inj_onI)
apply (fold bs_eq_def)
apply (auto simp: bs_eq_correct)
done

lemma finite_config_bound[simp, intro!]: "finite (config_bound bp s0)"
by blast

lemma reachable_configs_finite[simp, intro!]:
"finite (reachable_configs bp c)"
proof (cases c, clarsimp)
fix pc s
show "finite (reachable_configs bp (pc, s))"
proof (cases "pc < pc_bound bp")
case False from reachable_configs_out_of_bound[OF _ False, where s=s]
have "reachable_configs bp (pc, s)  {(pc,s)}" by auto
thus ?thesis by (rule finite_subset) auto
next
case True
hence "(pc,s)  config_bound bp s"
thus ?thesis
by (rule finite_subset[OF reachable_configs_in_bound]) simp
qed
qed

definition "bpc_is_run bpc r  let (bp,c)=bpc in r 0 = c  (i. r (Suc i)  set (BoolProgs.nexts bp (r i)))"
definition "bpc_props c  bs_α (snd c)"
definition "bpc_lang bpc  {bpc_props o r | r. bpc_is_run bpc r}"

(* Printing *)
(*definition print_list where
"print_list f sep s = (let f' = (λstr s. if str = [] then f s
else str @ sep @ f s)
in ''['' @ (foldl f' [] s) @ '']'')"

fun bool_list_to_prop_list where
"bool_list_to_prop_list _ [] props = props"
| "bool_list_to_prop_list n (x#xs) props = (let props' = if x then n#props else props
in bool_list_to_prop_list (Suc n) xs props')"
*)

fun print_config ::
"(nat  string)  (bitset  string)  config  string" where
"print_config f fx (p,s) = f p @ '' '' @ fx s"

end