# Theory PromelaStatistics

theory PromelaStatistics
imports
CAVA_Base.CAVA_Base
begin

code_printing
code_module PromelaStatistics ⇀ (SML) ‹
structure PromelaStatistics = struct
val active = Unsynchronized.ref false
val parseTime = Unsynchronized.ref Time.zeroTime
val time = Unsynchronized.ref Time.zeroTime

fun is_active () = !active

fun start () = (
active := true;
if !parseTime = Time.zeroTime then () else parseTime := Time.- (Time.now (), !parseTime);
time := Time.now ())
fun start_parse () = (active := true; parseTime := Time.now())
fun stop_timer () = (time := Time.- (Time.now (), !time))

fun to_string () = let
val t = Time.toMilliseconds (!time)
val pt = Time.toMilliseconds (!parseTime)
in
(if pt = 0 then "" else
"Parsing time : " ^ IntInf.toString pt ^ "ms\n")
^ "Building time: " ^ IntInf.toString t ^ "ms\n"
end

val _ = Statistics.register_stat ("Promela",is_active,to_string)
end
›
code_reserved SML PromelaStatistics

ML_val ‹@{code hd}›

consts
start :: "unit ⇒ unit"
start_parse :: "unit ⇒ unit"
stop_timer :: "unit ⇒ unit"

code_printing
constant start ⇀ (SML) "PromelaStatistics.start"
| constant start_parse ⇀ (SML) "PromelaStatistics.start'_parse"
| constant stop_timer ⇀ (SML) "PromelaStatistics.stop'_timer"

hide_const (open) start start_parse stop_timer

end


# Theory PromelaAST

section "Abstract Syntax Tree"
theory PromelaAST
imports Main
begin

text ‹
The abstract syntax tree is generated from the handwritten SML parser.
This theory only mirrors the data structures from the SML level to make them available in
Isabelle.
›

context
begin

local_setup ‹
Local_Theory.map_background_naming (Name_Space.mandatory_path "AST")
›

datatype binOp =
| BinOpSub
| BinOpMul
| BinOpDiv
| BinOpMod
| BinOpBitAnd
| BinOpBitXor
| BinOpBitOr
| BinOpGr
| BinOpLe
| BinOpGEq
| BinOpLEq
| BinOpEq
| BinOpNEq
| BinOpShiftL
| BinOpShiftR
| BinOpAnd
| BinOpOr

datatype unOp =
UnOpComp
| UnOpMinus
| UnOpNeg

datatype expr =
ExprBinOp binOp (*left*) expr (*right*) expr
| ExprUnOp unOp expr
| ExprCond (*cond*) expr (*exprTrue*) expr (*exprFalse*) expr
| ExprLen varRef
| ExprPoll varRef "recvArg list"
| ExprRndPoll varRef "recvArg list"
| ExprVarRef varRef
| ExprConst integer
| ExprTimeOut
| ExprNP
| ExprEnabled expr
| ExprPC expr
| ExprRemoteRef (*name*) String.literal
(*num*) "expr option"
(*label*) String.literal
| ExprGetPrio expr
| ExprSetPrio (*expr*) expr (*prio*) expr
| ExprFull varRef
| ExprEmpty varRef
| ExprNFull varRef
| ExprNEmpty varRef

and varRef = VarRef (*name*) String.literal
(*index*) "expr option"
(*next*) "varRef option"

and recvArg = RecvArgVar varRef
| RecvArgEval expr
| RecvArgConst integer

datatype range =
RangeFromTo (*var*) varRef
(*from*) expr
(*to*)  expr
| RangeIn (*var*) varRef (*inside*) varRef

datatype varType =
VarTypeBit
| VarTypeBool
| VarTypeByte
| VarTypePid
| VarTypeShort
| VarTypeInt
| VarTypeMType
| VarTypeChan
| VarTypeUnsigned
| VarTypeCustom String.literal

datatype varDecl =
VarDeclNum  (*name*) String.literal
(*size*) "integer option"
(*init*) "expr option"
| VarDeclChan (*name*) String.literal
(*size*) "integer option"
(*capacityTypes*) "(integer * varType list) option"
| VarDeclUnsigned (*name*) String.literal
(*bits*) integer
(*init*) "expr option"
| VarDeclMType (*name*) String.literal
(*size*) "integer option"
(*init*) "String.literal option"

datatype decl =
Decl (*vis*) "bool option"
(*sort*) varType
(*decl*) "varDecl list"

datatype stmnt =
StmntIf "(step list) list"
| StmntDo "(step list) list"
| StmntFor range "step list"
| StmntAtomic "step list"
| StmntDStep "step list"
| StmntSelect range
| StmntSeq "step list"
| StmntSend varRef "expr list"
| StmntSortSend varRef "expr list"
| StmntRecv varRef "recvArg list"
| StmntRndRecv varRef "recvArg list"
| StmntRecvX varRef "recvArg list"
| StmntRndRecvX varRef "recvArg list"
| StmntAssign varRef expr
| StmntIncr varRef
| StmntDecr varRef
| StmntElse
| StmntBreak
| StmntGoTo String.literal
| StmntLabeled String.literal stmnt
| StmntPrintF String.literal "expr list"
| StmntPrintM String.literal
| StmntRun (*name*) String.literal
(*args*) "expr list"
(*prio*) "integer option"
| StmntAssert expr
| StmntCond expr
| StmntCall String.literal "varRef list"

and step = StepStmnt stmnt (*unless*) "stmnt option"
| StepDecl decl
| StepXR "varRef list"
| StepXS "varRef list"

datatype module =
ProcType (*active*) "(integer option) option"
(*name*)   String.literal
(*decls*)  "decl list"
(*prio*)   "integer option"
(*prov*)   "expr option"
(*seq*)    "step list"
| DProcType (*active*) "(integer option) option"
(*name*)   String.literal
(*decls*)  "decl list"
(*prio*)   "integer option"
(*prov*)   "expr option"
(*seq*)    "step list"
| Init (*prio*) "integer option" "step list"
| Never "step list"
| Trace "step list"
| NoTrace "step list"
| Inline String.literal "String.literal list" "step list"
| TypeDef String.literal "decl list"
| MType "String.literal list"
| ModuDecl decl
| Ltl (*name*) String.literal (*formula*) String.literal

end
end


section "Data structures as used in Promela"
imports
CAVA_Base.CAVA_Base
CAVA_Base.Lexord_List
PromelaAST
"HOL-Library.IArray"
Deriving.Compare_Instances
CAVA_Base.CAVA_Code_Target
begin

(*<*)
no_notation test_bit (infixl "!!" 100)
(*>*)

subsection ‹Abstract Syntax Tree \emph{after} preprocessing›

text ‹
From the plain AST stemming from the parser, we'd like to have one containing more information while also removing duplicated constructs. This is achieved in the preprocessing step.

\begin{itemize}
\item variable type (including whether it represents a channel or not)
\item global vs local variable
\end{itemize}

Also certain constructs are expanded (like for-loops) or different nodes in the
AST are collapsed into one parametrized node (e.g.\ the different send-operations).

This preprocessing phase also tries to detect certain static errors and will bail out with an exception if such is encountered.
›

| BinOpSub
| BinOpMul
| BinOpDiv
| BinOpMod
| BinOpGr
| BinOpLe
| BinOpGEq
| BinOpLEq
| BinOpEq
| BinOpNEq
| BinOpAnd
| BinOpOr

datatype unOp = UnOpMinus
| UnOpNeg

datatype expr = ExprBinOp binOp (*left*) expr (*right*) expr
| ExprUnOp unOp expr
| ExprCond (*cond*) expr (*exprTrue*) expr (*exprFalse*) expr
| ExprLen chanRef
| ExprVarRef varRef
| ExprConst integer
| ExprMConst integer String.literal (* MType replaced by constant *)
| ExprTimeOut
| ExprFull chanRef
| ExprEmpty chanRef
| ExprPoll chanRef "recvArg list" bool (* sorted *)

and varRef = VarRef (*global*) bool
(*name*) String.literal
(*index*) "expr option"
and chanRef = ChanRef varRef ― ‹explicit type for channels›
and recvArg = RecvArgVar varRef
| RecvArgEval expr
| RecvArgConst integer
| RecvArgMConst integer String.literal

datatype varType = VTBounded integer integer
| VTChan

text ‹Variable declarations at the beginning of a proctype or at global level.›
datatype varDecl = VarDeclNum (*bounds*) integer integer
(*name*) String.literal
(*size*) "integer option"
(*init*) "expr option"
| VarDeclChan (*name*) String.literal
(*size*) "integer option"
(*capacityTypes*) "(integer * varType list) option"

text ‹Variable declarations during a proctype.›
datatype procVarDecl = ProcVarDeclNum  (*bounds*) integer integer
(*name*) String.literal
(*size*) "integer option"
(*init*) "expr option"
| ProcVarDeclChan (*name*) String.literal
(*size*) "integer option"

datatype procArg = ProcArg varType String.literal

datatype stmnt = StmntIf "(step list) list"
| StmntDo "(step list) list"
| StmntAtomic "step list"
| StmntSeq "step list"
| StmntSend chanRef "expr list" bool (*sorted*)
| StmntRecv chanRef "recvArg list" bool (*sorted*) bool (*remove?*)
| StmntAssign varRef expr
| StmntElse
| StmntBreak
| StmntSkip
| StmntGoTo String.literal
| StmntLabeled String.literal stmnt
| StmntRun (*name*) String.literal
(*args*) "expr list"
| StmntCond expr
| StmntAssert expr

and step = StepStmnt stmnt (*unless*) "stmnt option"
| StepDecl "procVarDecl list"
| StepSkip

datatype proc = ProcType (*active*) "(integer option) option"
(*name*)   String.literal
(*args*)  "procArg list"
(*decls*) "varDecl list"
(*seq*)    "step list"
| Init "varDecl list" "step list"

type_synonym ltl = "― ‹name:› String.literal × ― ‹formula:› String.literal"
type_synonym promela = "varDecl list × proc list × ltl list"

subsection ‹Preprocess the AST of the parser into our variant›

text ‹We setup some functionality for printing warning or even errors.

All those constants are logically @{term undefined}, but replaced by the parser
for something meaningful.›
consts
warn :: "String.literal ⇒ unit"

abbreviation "with_warn msg e ≡ let _ = warn msg in e"
abbreviation "the_warn opt msg ≡ case opt of None ⇒ () | _ ⇒ warn msg"

text ‹‹usc›: "Unsupported Construct"›
definition [code del]: "usc (c :: String.literal) ≡ undefined"

definition  [code del]: "err (e :: String.literal) = undefined"
abbreviation "errv e v ≡ err (e + v)"

definition [simp, code del]: "abort (msg :: String.literal) f = f ()"
abbreviation "abortv msg v f ≡ abort (msg + v) f"

code_printing
code_module PromelaUtils ⇀ (SML) ‹
structure PromelaUtils = struct
exception UnsupportedConstruct of string
exception StaticError of string
exception RuntimeError of string
fun warn msg = TextIO.print ("Warning: " ^ msg ^ "\n")
fun usc  c   = raise (UnsupportedConstruct c)
fun err  e   = raise (StaticError e)
fun abort msg _ = raise (RuntimeError msg)
end›
| constant warn ⇀ (SML) "PromelaUtils.warn"
| constant usc ⇀ (SML) "PromelaUtils.usc"
| constant err ⇀ (SML) "PromelaUtils.err"
| constant abort ⇀ (SML) "PromelaUtils.abort"
code_reserved SML PromelaUtils

(*<*)
ML_val ‹@{code hd}› (* Test code-printing setup. If this fails, the setup is skewed. *)
(*>*)

text ‹The preprocessing is done for each type on its own.›

primrec ppBinOp :: "AST.binOp ⇒ binOp"
where
| "ppBinOp AST.BinOpSub = BinOpSub"
| "ppBinOp AST.BinOpMul = BinOpMul"
| "ppBinOp AST.BinOpDiv = BinOpDiv"
| "ppBinOp AST.BinOpMod = BinOpMod"
| "ppBinOp AST.BinOpGr = BinOpGr"
| "ppBinOp AST.BinOpLe = BinOpLe"
| "ppBinOp AST.BinOpGEq = BinOpGEq"
| "ppBinOp AST.BinOpLEq = BinOpLEq"
| "ppBinOp AST.BinOpEq = BinOpEq"
| "ppBinOp AST.BinOpNEq = BinOpNEq"
| "ppBinOp AST.BinOpAnd = BinOpAnd"
| "ppBinOp AST.BinOpOr = BinOpOr"
| "ppBinOp AST.BinOpBitAnd = usc STR ''BinOpBitAnd''"
| "ppBinOp AST.BinOpBitXor = usc STR ''BinOpBitXor''"
| "ppBinOp AST.BinOpBitOr = usc STR ''BinOpBitOr''"
| "ppBinOp AST.BinOpShiftL = usc STR ''BinOpShiftL''"
| "ppBinOp AST.BinOpShiftR = usc STR ''BinOpShiftR''"

primrec ppUnOp :: "AST.unOp ⇒ unOp"
where
"ppUnOp AST.UnOpMinus = UnOpMinus"
| "ppUnOp AST.UnOpNeg = UnOpNeg"
| "ppUnOp AST.UnOpComp = usc STR ''UnOpComp''"

text ‹The data structure holding all information on variables we found so far.›
type_synonym var_data = "
(String.literal, (integer option × bool)) lm ― ‹channels›
× (String.literal, (integer option × bool)) lm ― ‹variables›
× (String.literal, integer) lm ― ‹mtypes›
× (String.literal, varRef) lm ― ‹aliases (used for inlines)›"

definition dealWithVar
:: "var_data ⇒ String.literal
⇒ (String.literal ⇒ integer option × bool ⇒ expr option ⇒ 'a)
⇒ (String.literal ⇒ integer option × bool ⇒ expr option ⇒ 'a)
⇒ (integer ⇒ 'a) ⇒ 'a"
where
"dealWithVar cvm n fC fV fM ≡ (
let (c,v,m,a) = cvm in
let (n, idx) = case lm.lookup n a of
None ⇒ (n, None)
| Some (VarRef _ name idx) ⇒ (name, idx)
in
case lm.lookup n m of
Some i ⇒ (case idx of None ⇒ fM i
| _ ⇒ err STR ''Array subscript used on MType (via alias).'')
| None ⇒ (case lm.lookup n v of
Some g ⇒ fV n g idx
| None ⇒ (case lm.lookup n c of
Some g ⇒ fC n g idx
| None ⇒ err (STR ''Unknown variable referenced: '' + n))))"

primrec enforceChan :: "varRef + chanRef ⇒ chanRef" where
"enforceChan (Inl _) = err STR ''Channel expected. Got normal variable.''"
| "enforceChan (Inr c) = c"

fun liftChan :: "varRef + chanRef ⇒ varRef" where
"liftChan (Inl v) = v"
| "liftChan (Inr (ChanRef v)) = v"

fun resolveIdx :: "expr option ⇒ expr option ⇒ expr option"
where
"resolveIdx None None = None"
| "resolveIdx idx  None = idx"
| "resolveIdx None aliasIdx = aliasIdx"
| "resolveIdx _   _     = err STR ''Array subscript used twice (via alias).''"

fun ppExpr :: "var_data ⇒ AST.expr ⇒ expr"
and ppVarRef :: "var_data ⇒ AST.varRef ⇒ varRef + chanRef"
and ppRecvArg :: "var_data ⇒ AST.recvArg ⇒ recvArg"
where
"ppVarRef cvm (AST.VarRef name idx None) = dealWithVar cvm name
(λname (_,g) aIdx. let idx = map_option (ppExpr cvm) idx in
Inr (ChanRef (VarRef g name (resolveIdx idx aIdx))))
(λname (_,g) aIdx. let idx = map_option (ppExpr cvm) idx in
Inl (VarRef g name (resolveIdx idx aIdx)))
(λ_. err STR ''Variable expected. Got MType.'')"
| "ppVarRef cvm (AST.VarRef _ _ (Some _)) =
usc STR ''next operation on variables''"

| "ppExpr cvm AST.ExprTimeOut = ExprTimeOut"
| "ppExpr cvm (AST.ExprConst c) = ExprConst c"

| "ppExpr cvm (AST.ExprBinOp bo l r) =
ExprBinOp (ppBinOp bo) (ppExpr cvm l) (ppExpr cvm r)"
| "ppExpr cvm (AST.ExprUnOp uo e) =
ExprUnOp (ppUnOp uo) (ppExpr cvm e)"
| "ppExpr cvm (AST.ExprCond c t f) =
ExprCond (ppExpr cvm c) (ppExpr cvm t) (ppExpr cvm f)"

| "ppExpr cvm (AST.ExprLen v) =
ExprLen (enforceChan (ppVarRef cvm v))"
| "ppExpr cvm (AST.ExprFull v) =
ExprFull (enforceChan (ppVarRef cvm v))"
| "ppExpr cvm (AST.ExprEmpty v) =
ExprEmpty (enforceChan (ppVarRef cvm v))"
(* the following two are special constructs in Promela for helping Partial Order Reductions
we don't have such things (yet), so use simple negation *)
| "ppExpr cvm (AST.ExprNFull v) =
ExprUnOp UnOpNeg (ExprFull (enforceChan (ppVarRef cvm v)))"
| "ppExpr cvm (AST.ExprNEmpty v) =
ExprUnOp UnOpNeg (ExprEmpty (enforceChan (ppVarRef cvm v)))"

| "ppExpr cvm (AST.ExprVarRef v) = (
let to_exp = λ_. ExprVarRef (liftChan (ppVarRef cvm v)) in
case v of
AST.VarRef name None None ⇒
dealWithVar cvm name
(λ_ _ _. to_exp())
(λ_ _ _. to_exp())
(λi. ExprMConst i name)
| _ ⇒ to_exp())"

| "ppExpr cvm (AST.ExprPoll v es) =
ExprPoll (enforceChan (ppVarRef cvm v)) (map (ppRecvArg cvm) es) False"
| "ppExpr cvm (AST.ExprRndPoll v es) =
ExprPoll (enforceChan (ppVarRef cvm v)) (map (ppRecvArg cvm) es) True"

| "ppExpr cvm AST.ExprNP = usc STR ''ExprNP''"
| "ppExpr cvm (AST.ExprEnabled _) = usc STR ''ExprEnabled''"
| "ppExpr cvm (AST.ExprPC _) = usc STR ''ExprPC''"
| "ppExpr cvm (AST.ExprRemoteRef _ _ _) = usc STR ''ExprRemoteRef''"
| "ppExpr cvm (AST.ExprGetPrio _) = usc STR ''ExprGetPrio''"
| "ppExpr cvm (AST.ExprSetPrio _ _) = usc STR ''ExprSetPrio''"

| "ppRecvArg cvm (AST.RecvArgVar v) = (
let to_ra = λ_. RecvArgVar (liftChan (ppVarRef cvm v)) in
case v of
AST.VarRef name None None ⇒
dealWithVar cvm name
(λ_ _ _. to_ra())
(λ_ _ _. to_ra())
(λi. RecvArgMConst i name)
| _ ⇒ to_ra())"
| "ppRecvArg cvm (AST.RecvArgEval e) = RecvArgEval (ppExpr cvm e)"
| "ppRecvArg cvm (AST.RecvArgConst c) = RecvArgConst c"

primrec ppVarType :: "AST.varType ⇒ varType" where
"ppVarType AST.VarTypeBit = VTBounded 0 1"
| "ppVarType AST.VarTypeBool = VTBounded 0 1"
| "ppVarType AST.VarTypeByte = VTBounded 0 255"
| "ppVarType AST.VarTypePid = VTBounded 0 255"
| "ppVarType AST.VarTypeShort = VTBounded (-(2^15)) ((2^15) - 1)"
| "ppVarType AST.VarTypeInt = VTBounded (-(2^31)) ((2^31) - 1)"
| "ppVarType AST.VarTypeMType = VTBounded 1 255"
| "ppVarType AST.VarTypeChan = VTChan"
| "ppVarType AST.VarTypeUnsigned = usc STR ''VarTypeUnsigned''"
| "ppVarType (AST.VarTypeCustom _) = usc STR ''VarTypeCustom''"

fun ppVarDecl
:: "var_data ⇒ varType ⇒ bool ⇒ AST.varDecl ⇒ var_data × varDecl"
where
"ppVarDecl (c,v,m,a) (VTBounded l h) g
(AST.VarDeclNum name sze init) = (
case lm.lookup name v of
Some _ ⇒ errv STR ''Duplicate variable '' name
| _ ⇒ (case lm.lookup name a of
Some _ ⇒ errv
STR ''Variable name clashes with alias: '' name
| _ ⇒ ((c, lm.update name (sze,g) v, m, a),
VarDeclNum l h name sze
(map_option (ppExpr (c,v,m,a)) init))))"
| "ppVarDecl _ _ g (AST.VarDeclNum name sze init) =
err STR ''Assiging num to non-num''"

| "ppVarDecl (c,v,m,a) VTChan g
(AST.VarDeclChan name sze cap) = (
let cap' = map_option (apsnd (map ppVarType)) cap in
case lm.lookup name c of
Some _ ⇒ errv STR ''Duplicate variable '' name
| _ ⇒ (case lm.lookup name a of
Some _ ⇒ errv
STR ''Variable name clashes with alias: '' name
| _ ⇒ ((lm.update name (sze, g) c, v, m, a),
VarDeclChan name sze cap')))"
| "ppVarDecl _ _ g (AST.VarDeclChan name sze init) =
err STR ''Assiging chan to non-chan''"

| "ppVarDecl (c,v,m,a) (VTBounded l h) g
(AST.VarDeclMType name sze init) = (
let init = map_option (λmty.
case lm.lookup mty m of
None ⇒ errv STR ''Unknown MType '' mty
| Some mval ⇒ ExprMConst mval mty) init in
case lm.lookup name c of
Some _ ⇒ errv STR ''Duplicate variable '' name
| _ ⇒ (case lm.lookup name a of Some _
⇒ errv STR ''Variable name clashes with alias: '' name
| _ ⇒ ((c, lm.update name (sze,g) v, m, a),
VarDeclNum l h name sze init)))"

| "ppVarDecl _ _ g (AST.VarDeclMType name sze init) =
err STR ''Assiging num to non-num''"

| "ppVarDecl _ _ _ (AST.VarDeclUnsigned _ _ _) =
usc STR ''VarDeclUnsigned''"

definition ppProcVarDecl
:: "var_data ⇒ varType ⇒ bool ⇒ AST.varDecl ⇒ var_data × procVarDecl"
where
"ppProcVarDecl cvm ty g v = (case ppVarDecl cvm ty g v of
(cvm, VarDeclNum l h name sze init) ⇒ (cvm, ProcVarDeclNum l h name sze init)
| (cvm, VarDeclChan name sze None) ⇒ (cvm, ProcVarDeclChan name sze)
| _ ⇒ err STR ''Channel initilizations only allowed at the beginning of proctypes.'')"

fun ppProcArg
:: "var_data ⇒ varType ⇒ bool ⇒ AST.varDecl ⇒ var_data × procArg"
where
"ppProcArg (c,v,m,a) (VTBounded l h) g
(AST.VarDeclNum name None None) = (
case lm.lookup name v of
Some _ ⇒ errv STR ''Duplicate variable '' name
| _ ⇒ (case lm.lookup name a of
Some _ ⇒ errv
STR ''Variable name clashes with alias: '' name
| _ ⇒ ((c, lm.update name (None, g) v, m, a),
ProcArg (VTBounded l h) name)))"
| "ppProcArg _ _ _ (AST.VarDeclNum _ _ _) =
err STR ''Invalid proctype arguments''"

| "ppProcArg (c,v,m,a) VTChan g
(AST.VarDeclChan name None None) = (
case lm.lookup name c of
Some _ ⇒ errv STR ''Duplicate variable '' name
| _ ⇒ (case lm.lookup name a of
Some _ ⇒ errv
STR ''Variable name clashes with alias: '' name
| _ ⇒ ((lm.update name (None, g) c, v, m, a), ProcArg VTChan name)))"
| "ppProcArg _ _ _ (AST.VarDeclChan _ _ _) =
err STR ''Invalid proctype arguments''"

| "ppProcArg (c,v,m,a) (VTBounded l h) g
(AST.VarDeclMType name None None) = (
case lm.lookup name v of
Some _ ⇒ errv STR ''Duplicate variable '' name
| _ ⇒ (case lm.lookup name a of
Some _ ⇒ errv
STR ''Variable name clashes with alias: '' name
| _ ⇒ ((c, lm.update name (None, g) v, m, a),
ProcArg (VTBounded l h) name)))"
| "ppProcArg _ _ _ (AST.VarDeclMType _ _ _) =
err STR ''Invalid proctype arguments''"

| "ppProcArg _ _ _ (AST.VarDeclUnsigned _ _ _) = usc STR ''VarDeclUnsigned''"

text ‹Some preprocessing functions enrich the @{typ var_data} argument and hence return
a new updated one. When chaining multiple calls to such functions after another, we need to make
sure, the @{typ var_data} is passed accordingly. @{term cvm_fold} does exactly that for such a
function @{term g} and a list of nodes @{term ss}.›

definition cvm_fold where
"cvm_fold g cvm ss = foldl (λ(cvm,ss) s. apsnd (λs'. ss@[s']) (g cvm s))
(cvm, []) ss"

lemma cvm_fold_cong[fundef_cong]:
assumes "cvm = cvm'"
and "stepss = stepss'"
and "⋀x d. x ∈ set stepss ⟹ g d x = g' d x"
shows "cvm_fold g cvm stepss = cvm_fold g' cvm' stepss'"
unfolding cvm_fold_def
using assms
by (fastforce intro: foldl_cong split: prod.split)

fun liftDecl where
"liftDecl f g cvm (AST.Decl vis t decls) = (
let _ = the_warn vis STR ''Visibility in declarations not supported. Ignored.'' in
let t = ppVarType t in
cvm_fold (λcvm. f cvm t g) cvm decls)"

definition ppDecl
:: "bool ⇒ var_data ⇒ AST.decl ⇒ var_data × varDecl list"
where
"ppDecl = liftDecl ppVarDecl"

definition ppDeclProc
:: "var_data ⇒ AST.decl ⇒ var_data × procVarDecl list"
where
"ppDeclProc = liftDecl ppProcVarDecl False"

definition ppDeclProcArg
:: "var_data ⇒ AST.decl ⇒ var_data × procArg list"
where
"ppDeclProcArg = liftDecl ppProcArg False"

(* increment *)
definition incr :: "varRef ⇒ stmnt" where
"incr v = StmntAssign v (ExprBinOp BinOpAdd (ExprVarRef v) (ExprConst 1))"

(* decrement *)
definition decr :: "varRef ⇒ stmnt" where
"decr v = StmntAssign v (ExprBinOp BinOpSub (ExprVarRef v) (ExprConst 1))"

text ‹
Transforms
\verb+for (i : lb .. ub) steps+
into
\begin{verbatim} {
i = lb;
do
:: i =< ub -> steps; i++
:: else -> break
od
} \end{verbatim}
›
definition forFromTo :: "varRef ⇒ expr ⇒ expr ⇒ step list ⇒ stmnt" where
"forFromTo i lb ub steps = (
let
― ‹‹i = lb››
loop_pre = StepStmnt (StmntAssign i lb) None;
― ‹‹i ≤ ub››
loop_cond = StepStmnt (StmntCond
(ExprBinOp BinOpLEq (ExprVarRef i) ub))
None;
― ‹‹i++››
loop_incr = StepStmnt (incr i) None;
― ‹‹i ≤ ub -> ...; i++››
loop_body = loop_cond # steps @ [loop_incr];
― ‹‹else -> break››
loop_abort = [StepStmnt StmntElse None, StepStmnt StmntBreak None];
― ‹‹do :: i ≤ ub -> ... :: else -> break od››
loop = StepStmnt (StmntDo [loop_body, loop_abort]) None
in
StmntSeq [loop_pre, loop])"

text ‹
Transforms (where @{term a} is an array with @{term N} entries)
\verb+for (i in a) steps+
into
\begin{verbatim}{
i = 0;
do
:: i < N -> steps; i++
:: else -> break
od
}\end{verbatim}
›
definition forInArray :: "varRef ⇒ integer ⇒ step list ⇒ stmnt" where
"forInArray i N steps = (
let
― ‹‹i = 0››
loop_pre = StepStmnt (StmntAssign i (ExprConst 0)) None;
― ‹‹i < N››
loop_cond = StepStmnt (StmntCond
(ExprBinOp BinOpLe (ExprVarRef i)
(ExprConst N)))
None;
― ‹‹i++››
loop_incr = StepStmnt (incr i) None;
― ‹‹i < N -> ...; i++››
loop_body = loop_cond # steps @ [loop_incr];
― ‹‹else -> break››
loop_abort = [StepStmnt StmntElse None, StepStmnt StmntBreak None];
― ‹‹do :: i < N -> ... :: else -> break od››
loop = StepStmnt (StmntDo [loop_body, loop_abort]) None
in
StmntSeq [loop_pre, loop])"

text ‹
Transforms (where @{term c} is a channel)
\verb+for (msg in c) steps+
into
\begin{verbatim}{
byte :tmp: = 0;
do
:: :tmp: < len(c) ->
c?msg; c!msg;
steps;
:tmp:++
:: else -> break
od
}\end{verbatim}
›
definition forInChan :: "varRef ⇒ chanRef ⇒ step list ⇒ stmnt" where
"forInChan msg c steps = (
let
― ‹‹byte :tmp: = 0››
tmpStr = STR '':tmp:'';
loop_pre = StepDecl
[ProcVarDeclNum 0 255 tmpStr None (Some (ExprConst 0))];
tmp = VarRef False tmpStr None;
― ‹‹:tmp: < len(c)››
loop_cond = StepStmnt (StmntCond
(ExprBinOp BinOpLe (ExprVarRef tmp)
(ExprLen c)))
None;
― ‹‹:tmp:++››
loop_incr = StepStmnt (incr tmp) None;
― ‹‹c?msg››
recv = StepStmnt (StmntRecv c [RecvArgVar msg] False True) None;
― ‹‹c!msg››
send = StepStmnt (StmntSend c [ExprVarRef msg] False) None;
― ‹‹:tmp: < len(c) -> c?msg; c!msg; ...; :tmp:++››
loop_body = [loop_cond, recv, send] @ steps @ [loop_incr];
― ‹‹else -> break››
loop_abort = [StepStmnt StmntElse None, StepStmnt StmntBreak None];
― ‹‹do :: :tmp: < len(c) -> ... :: else -> break od››
loop = StepStmnt (StmntDo [loop_body, loop_abort]) None
in
StmntSeq [loop_pre, loop])"

text ‹
Transforms
\verb+select (i : lb .. ub)+
into
\begin{verbatim}{
i = lb;
do
:: i < ub -> i++
:: break
od
}\end{verbatim}
›
definition select :: "varRef ⇒ expr ⇒ expr ⇒ stmnt" where
"select i lb ub = (
let
― ‹‹i = lb››
pre = StepStmnt (StmntAssign i lb) None;
― ‹‹i < ub››
cond = StepStmnt (StmntCond (ExprBinOp BinOpLe (ExprVarRef i) ub))
None;
― ‹‹i++››
incr = StepStmnt (incr i) None;
― ‹‹i < ub -> i++››
loop_body = [cond, incr];
― ‹‹break››
loop_abort = [StepStmnt StmntBreak None];
― ‹‹do :: i < ub -> ... :: break od››
loop = StepStmnt (StmntDo [loop_body, loop_abort]) None
in
StmntSeq [pre, loop])"

type_synonym inlines =
"(String.literal, String.literal list × (var_data ⇒ var_data × step list)) lm"
type_synonym stmnt_data =
" bool × varDecl list × inlines × var_data"

fun ppStep :: "stmnt_data ⇒ AST.step ⇒ stmnt_data * step"
and ppStmnt :: "stmnt_data ⇒ AST.stmnt ⇒ stmnt_data * stmnt"
where
"ppStep cvm (AST.StepStmnt s u) = (
let (cvm', s') = ppStmnt cvm s in
case u of None ⇒ (cvm', StepStmnt s' None)
| Some u ⇒ let (cvm'',u') = ppStmnt cvm' u in
(cvm'', StepStmnt s' (Some u')))"
| "ppStep (False, ps, i, cvm) (AST.StepDecl d) =
map_prod (λcvm. (False, ps, i, cvm)) StepDecl (ppDeclProc cvm d)"
| "ppStep (True, ps, i, cvm) (AST.StepDecl d) = (
let (cvm', ps') = ppDecl False cvm d
in ((True, ps@ps', i, cvm'), StepSkip))"
| "ppStep (_,cvm) (AST.StepXR _) =
with_warn STR ''StepXR not supported. Ignored.'' ((False,cvm), StepSkip)"
| "ppStep (_,cvm) (AST.StepXS _) =
with_warn STR ''StepXS not supported. Ignored.'' ((False,cvm), StepSkip)"

| "ppStmnt (_,cvm) (AST.StmntBreak) = ((False,cvm), StmntBreak)"
| "ppStmnt (_,cvm) (AST.StmntElse) = ((False,cvm), StmntElse)"
| "ppStmnt (_,cvm) (AST.StmntGoTo l) = ((False,cvm), StmntGoTo l)"
| "ppStmnt (_,cvm) (AST.StmntLabeled l s) =
apsnd (StmntLabeled l) (ppStmnt (False,cvm) s)"
| "ppStmnt (_,ps,i,cvm) (AST.StmntCond e) =
((False,ps,i,cvm), StmntCond (ppExpr cvm e))"
| "ppStmnt (_,ps,i,cvm) (AST.StmntAssert e) =
((False,ps,i,cvm), StmntAssert (ppExpr cvm e))"
| "ppStmnt (_,ps,i,cvm) (AST.StmntAssign v e) =
((False,ps,i,cvm), StmntAssign (liftChan (ppVarRef cvm v)) (ppExpr cvm e))"
| "ppStmnt (_,ps,i,cvm) (AST.StmntSend v es) =
((False,ps,i,cvm), StmntSend (enforceChan (ppVarRef cvm v))
(map (ppExpr cvm) es) False)"
| "ppStmnt (_,ps,i,cvm) (AST.StmntSortSend v es) =
((False,ps,i,cvm), StmntSend (enforceChan (ppVarRef cvm v))
(map (ppExpr cvm) es) True)"
| "ppStmnt (_,ps,i,cvm) (AST.StmntRecv v rs) =
((False,ps,i,cvm), StmntRecv (enforceChan (ppVarRef cvm v))
(map (ppRecvArg cvm) rs) False True)"
| "ppStmnt (_,ps,i,cvm) (AST.StmntRecvX v rs) =
((False,ps,i,cvm), StmntRecv (enforceChan (ppVarRef cvm v))
(map (ppRecvArg cvm) rs) False False)"
| "ppStmnt (_,ps,i,cvm) (AST.StmntRndRecv v rs) =
((False,ps,i,cvm), StmntRecv (enforceChan (ppVarRef cvm v))
(map (ppRecvArg cvm) rs) True True)"
| "ppStmnt (_,ps,i,cvm) (AST.StmntRndRecvX v rs) =
((False,ps,i,cvm), StmntRecv (enforceChan (ppVarRef cvm v))
(map (ppRecvArg cvm) rs) True False)"
| "ppStmnt (_,ps,i,cvm) (AST.StmntRun n es p) = (
let _ = the_warn p STR ''Priorities for 'run' not supported. Ignored.'' in
((False,ps,i,cvm), StmntRun n (map (ppExpr cvm) es)))"
| "ppStmnt (_,cvm) (AST.StmntSeq ss) =
apsnd StmntSeq (cvm_fold ppStep (False,cvm) ss)"
| "ppStmnt (_,cvm) (AST.StmntAtomic ss) =
apsnd StmntAtomic (cvm_fold ppStep (False,cvm) ss)"
| "ppStmnt (_,cvm) (AST.StmntIf sss) =
apsnd StmntIf (cvm_fold (cvm_fold ppStep) (False,cvm) sss)"
| "ppStmnt (_,cvm) (AST.StmntDo sss) =
apsnd StmntDo (cvm_fold (cvm_fold ppStep) (False,cvm) sss)"

(* Replace i++ and i-- by i = i + 1 / i = i - 1 *)
| "ppStmnt (_,ps,i,cvm) (AST.StmntIncr v) =
((False,ps,i,cvm), incr (liftChan (ppVarRef cvm v)))"
| "ppStmnt (_,ps,i,cvm) (AST.StmntDecr v) =
((False,ps,i,cvm), decr (liftChan (ppVarRef cvm v)))"

| "ppStmnt (_,cvm) (AST.StmntPrintF _ _) =
with_warn STR ''PrintF ignored'' ((False,cvm), StmntSkip)"
| "ppStmnt (_,cvm) (AST.StmntPrintM _) =
with_warn STR ''PrintM ignored'' ((False,cvm), StmntSkip)"

| "ppStmnt (_,ps,inl,cvm) (AST.StmntFor
(AST.RangeFromTo i lb ub)
steps) = (
let
i = liftChan (ppVarRef cvm i);
(lb,ub) = (ppExpr cvm lb, ppExpr cvm ub)
in
apsnd (forFromTo i lb ub) (cvm_fold ppStep (False,ps,inl,cvm) steps))"
| "ppStmnt (_,ps,inl,cvm) (AST.StmntFor
(AST.RangeIn i v)
steps) = (
let
i = liftChan (ppVarRef cvm i);
(cvm',steps) = cvm_fold ppStep (False,ps,inl,cvm) steps
in
case ppVarRef cvm v of
Inr c ⇒ (cvm', forInChan i c steps)
| Inl (VarRef _ _ (Some _)) ⇒ err STR ''Iterating over array-member.''
| Inl (VarRef _ name None) ⇒ (
let (_,v,_) = cvm in
case fst (the (lm.lookup name v)) of
None ⇒ err STR ''Iterating over non-array variable.''
| Some N ⇒ (cvm', forInArray i N steps)))"

| "ppStmnt (_,ps,inl,cvm) (AST.StmntSelect
(AST.RangeFromTo i lb ub)) = (
let
i = liftChan (ppVarRef cvm i);
(lb, ub) = (ppExpr cvm lb, ppExpr cvm ub)
in
((False,ps,inl,cvm), select i lb ub))"
| "ppStmnt (_,cvm) (AST.StmntSelect (AST.RangeIn _ _)) =
err STR ''\"in\" not allowed in select''"

| "ppStmnt (_,ps,inl,cvm) (AST.StmntCall macro args) = (
let
args = map (liftChan ∘ ppVarRef cvm) args;
(c,v,m,a) = cvm
in
case lm.lookup macro inl of
None ⇒ errv STR ''Calling unknown macro '' macro
| Some (names,sF) ⇒
if length names ≠ length args then
(err STR ''Called macro with wrong number of arguments.'')
else
let a' = foldl (λa (k,v). lm.update k v a) a (zip names args) in
let ((c,v,m,_),steps) = sF (c,v,m,a') in
((False,ps,inl,c,v,m,a), StmntSeq steps))"

| "ppStmnt cvm (AST.StmntDStep _) = usc STR ''StmntDStep''"

fun ppModule
:: "var_data × inlines ⇒ AST.module
⇒ var_data × inlines × (varDecl list + proc + ltl)"
where
"ppModule (cvm, inl) (AST.ProcType act name args prio prov steps) = (
let
_ = the_warn prio STR ''Priorities for procs not supported. Ignored.'';
_ = the_warn prov STR ''Priov (??) for procs not supported. Ignored.'';
(cvm', args) = cvm_fold ppDeclProcArg cvm args;
((_, vars, _, _), steps) = cvm_fold ppStep (True,[],inl,cvm') steps
in
(cvm, inl, Inr (Inl (ProcType act name (concat args) vars steps))))"

| "ppModule (cvm,inl) (AST.Init prio steps) = (
let _ = the_warn prio STR ''Priorities for procs not supported. Ignored.'' in
let ((_, vars, _, _), steps) = cvm_fold ppStep (True,[],inl,cvm) steps in
(cvm, inl, Inr (Inl (Init vars steps))))"

| "ppModule (cvm,inl) (AST.Ltl name formula) =
(cvm, inl, Inr (Inr (name, formula)))"

| "ppModule (cvm,inl) (AST.ModuDecl decl) =
apsnd (λds. (inl,Inl ds)) (ppDecl True cvm decl)"

| "ppModule (cvm,inl) (AST.MType mtys) = (
let (c,v,m,a) = cvm in
let num = integer_of_nat (lm.size m) + 1 in
let (m',_) = foldr (λmty (m,num).
let m' = lm.update mty num m
in (m',num+1)) mtys (m,num)
in
((c,v,m',a), inl, Inl []))"

| "ppModule (cvm,inl) (AST.Inline name args steps) = (
let stepF = (λcvm. let ((_,_,_,cvm),steps) =
cvm_fold ppStep (False,[],inl,cvm) steps
in (cvm,steps))
in let inl = lm.update name (args, stepF) inl
in (cvm,inl, Inl[]))"

| "ppModule cvm (AST.DProcType _ _ _ _ _ _) = usc STR ''DProcType''"
| "ppModule cvm (AST.Never _) = usc STR ''Never''"
| "ppModule cvm (AST.Trace _) = usc STR ''Trace''"
| "ppModule cvm (AST.NoTrace _) = usc STR ''NoTrace''"
| "ppModule cvm (AST.TypeDef _ _) = usc STR ''TypeDef''"

definition preprocess :: "AST.module list ⇒ promela" where
"preprocess ms = (
let
dflt_vars = [(STR ''_pid'', (None, False)),
(STR ''__assert__'', (None, True)),
(STR ''_'', (None, True))];
cvm = (lm.empty(), lm.to_map dflt_vars, lm.empty(), lm.empty());
(_,_,pr) = (foldl (λ(cvm,inl,vs,ps,ls) m.
let (cvm', inl', m') = ppModule (cvm,inl) m in
case m' of
Inl v ⇒ (cvm',inl',vs@v,ps,ls)
| Inr (Inl p) ⇒ (cvm',inl',vs,ps@[p],ls)
| Inr (Inr l) ⇒ (cvm',inl',vs,ps,ls@[l]))
(cvm, lm.empty(),[],[],[]) ms)
in
pr)"

fun extractLTL
:: "AST.module ⇒ ltl option"
where
"extractLTL (AST.Ltl name formula) = Some (name, formula)"
| "extractLTL _ = None"

primrec extractLTLs
:: "AST.module list ⇒ (String.literal, String.literal) lm"
where
"extractLTLs [] = lm.empty()"
| "extractLTLs (m#ms) = (case extractLTL m of
None ⇒ extractLTLs ms
| Some (n,f) ⇒ lm.update n f (extractLTLs ms))"

definition lookupLTL
:: "AST.module list ⇒ String.literal ⇒ String.literal option"
where "lookupLTL ast k = lm.lookup k (extractLTLs ast)"

subsection ‹The transition system›

text ‹
The edges in our transition system consist of a condition (evaluated under the current environment) and an effect (modifying the current environment).
Further they may be atomic, \ie a whole row of such edges is taken before yielding a new state.
Additionally, they carry a priority: the edges are checked from highest to lowest priority, and if one edge on a higher level can be taken, the lower levels are ignored.

The states of the system do not carry any information.
›

datatype edgeCond = ECElse
| ECTrue
| ECFalse
| ECExpr expr
| ECRun String.literal
| ECSend chanRef
| ECRecv chanRef "recvArg list" bool (* sorted *)

datatype edgeEffect = EEEnd
| EEId
| EEGoto
| EEAssert expr
| EEAssign varRef expr
| EEDecl procVarDecl
| EERun String.literal "expr list"
| EESend chanRef "expr list" bool (*sorted*)
| EERecv chanRef "recvArg list" bool (*sorted*) bool (*remove*)

datatype edgeIndex = Index nat | LabelJump String.literal "nat option"
datatype edgeAtomic = NonAtomic | Atomic | InAtomic

record edge =
cond   :: edgeCond
effect :: edgeEffect
target :: edgeIndex
prio   :: integer
atomic :: edgeAtomic

definition isAtomic :: "edge ⇒ bool" where
"isAtomic e = (case atomic e of Atomic ⇒ True | _ ⇒ False)"

definition inAtomic :: "edge ⇒ bool" where
"inAtomic e = (case atomic e of NonAtomic ⇒ False | _ ⇒ True)"

subsection ‹State›

datatype variable = Var varType integer
| VArray varType nat "integer iarray"

datatype channel = Channel integer "varType list" "integer list list"
| HSChannel "varType list" (* handshake channel *)
| InvChannel (* Invalid / closed channel *)

type_synonym var_dict = "(String.literal, variable) lm"
type_synonym labels   = "(String.literal, nat) lm"
type_synonym ltls     = "(String.literal, String.literal) lm"
type_synonym states   = "(― ‹prio:› integer × edge list) iarray"
type_synonym channels = "channel list"

type_synonym process  =
"nat ― ‹offset›
× edgeIndex ― ‹start›
× procArg list ― ‹args›
× varDecl list ― ‹top decls›"

record program =
processes :: "process iarray"
labels :: "labels iarray"
states :: "states iarray"
proc_names :: "String.literal iarray"
proc_data :: "(String.literal, nat) lm"

record pState = ― ‹State of a process›
pid      :: nat             ― ‹Process identifier›
vars     :: var_dict        ― ‹Dictionary of variables›
pc       :: nat             ― ‹Program counter›
channels :: "integer list"  ― ‹List of channels created in the process. Used to close them on finalization.›
idx :: nat                  ― ‹Offset into the arrays of @{type program}›

hide_const (open) idx

record gState = ― ‹Global state›
vars      :: var_dict      ― ‹Global variables›
channels  :: channels      ― ‹Channels are by construction part of the global state, even when created in a process.›
timeout   :: bool          ― ‹Set to True if no process can take a transition.›
procs     :: "pState list" ― ‹List of all running processes. A process is removed from it, when there is no running one
with a higher index.›

record gState⇩I = gState + ― ‹Additional internal infos›
handshake :: nat
hsdata    :: "integer list " ― ‹Data transferred via a handshake.›
exclusive :: nat     ― ‹Set to the PID of the process, which is in an exclusive (= atomic) state.›
else      :: bool    ― ‹Set to True for each process, if it can not take a transition. Used before timeout.›

subsection ‹Printing›

primrec printBinOp :: "binOp ⇒ string" where
| "printBinOp BinOpSub = ''-''"
| "printBinOp BinOpMul = ''*''"
| "printBinOp BinOpDiv = ''/''"
| "printBinOp BinOpMod = ''mod''"
| "printBinOp BinOpGr = ''>''"
| "printBinOp BinOpLe = ''<''"
| "printBinOp BinOpGEq = ''>=''"
| "printBinOp BinOpLEq = ''=<''"
| "printBinOp BinOpEq = ''==''"
| "printBinOp BinOpNEq = ''!=''"
| "printBinOp BinOpAnd = ''&&''"
| "printBinOp BinOpOr = ''||''"

primrec printUnOp :: "unOp ⇒ string" where
"printUnOp UnOpMinus = ''-''"
| "printUnOp UnOpNeg = ''!''"

definition printList :: "('a ⇒ string) ⇒ 'a list ⇒ string ⇒ string ⇒ string ⇒ string"
where
"printList f xs l r sep = (
let f' = (λstr x. if str = [] then f x
else str @ sep @ f x)
in l @ (foldl f' [] xs) @ r)"

lemma printList_cong [fundef_cong]:
assumes "xs = xs'"
and "l = l'"
and "r = r'"
and "sep = sep'"
and "⋀x. x ∈ set xs ⟹ f x = f' x"
shows "printList f xs l r sep = printList f' xs' l' r' sep'"
unfolding printList_def
using assms
by (auto intro: foldl_cong)

fun printExpr :: "(integer ⇒ string) ⇒ expr ⇒ string"
and printFun ::  "(integer ⇒ string) ⇒ string ⇒ chanRef ⇒ string"
and printVarRef :: "(integer ⇒ string) ⇒ varRef ⇒ string"
and printChanRef :: "(integer ⇒ string) ⇒ chanRef ⇒ string"
and printRecvArg :: "(integer ⇒ string) ⇒ recvArg ⇒ string" where
"printExpr f ExprTimeOut = ''timeout''"
| "printExpr f (ExprBinOp binOp left right) =
printExpr f left @ '' '' @ printBinOp binOp @ '' '' @ printExpr f right"
| "printExpr f (ExprUnOp unOp e) = printUnOp unOp @ printExpr f e"
| "printExpr f (ExprVarRef varRef) = printVarRef f varRef"
| "printExpr f (ExprConst i) = f i"
| "printExpr f (ExprMConst i m) = String.explode m"
| "printExpr f (ExprCond c l r) =
''( (( '' @ printExpr f c @ '' )) -> ''
@ printExpr f l @ '' : ''
@ printExpr f r @ '' )''"
| "printExpr f (ExprLen chan) = printFun f ''len'' chan"
| "printExpr f (ExprEmpty chan) = printFun f ''empty'' chan"
| "printExpr f (ExprFull chan) = printFun f ''full'' chan"
| "printExpr f (ExprPoll chan es srt) = (
let p = if srt then ''??'' else ''?'' in
printChanRef f chan @ p
@ printList (printRecvArg f) es ''['' '']'' '', '')"

| "printVarRef _ (VarRef _ name None) = String.explode name"
| "printVarRef f (VarRef _ name (Some indx)) =
String.explode name @ ''['' @ printExpr f indx @ '']''"

| "printChanRef f (ChanRef v) = printVarRef f v"

| "printFun f fun var = fun @ ''('' @ printChanRef f var @ '')''"

| "printRecvArg f (RecvArgVar v) = printVarRef f v"
| "printRecvArg f (RecvArgConst c) = f c"
| "printRecvArg f (RecvArgMConst _ m) = String.explode m"
| "printRecvArg f (RecvArgEval e) = ''eval('' @ printExpr f e @ '')''"

fun printVarDecl :: "(integer ⇒ string) ⇒ procVarDecl ⇒ string" where
"printVarDecl f (ProcVarDeclNum _ _ n None None) =
String.explode n @ '' = 0''"
| "printVarDecl f (ProcVarDeclNum _ _ n None (Some e)) =
String.explode n @ '' = '' @ printExpr f e"
| "printVarDecl f (ProcVarDeclNum _ _ n (Some i) None) =
String.explode n @ ''['' @ f i @ ''] = 0''"
| "printVarDecl f (ProcVarDeclNum _ _ n (Some i) (Some e)) =
String.explode n @ ''[''@ f i @ ''] = '' @ printExpr f e"
| "printVarDecl f (ProcVarDeclChan n None) =
''chan '' @ String.explode n"
| "printVarDecl f (ProcVarDeclChan n (Some i)) =
''chan '' @ String.explode n @ ''['' @ f i @ '']''"

primrec printCond :: "(integer ⇒ string) ⇒ edgeCond ⇒ string" where
"printCond f ECElse = ''else''"
| "printCond f ECTrue = ''true''"
| "printCond f ECFalse = ''false''"
| "printCond f (ECRun n) = ''run '' @ String.explode n @ ''(...)''"
| "printCond f (ECExpr e) = printExpr f e"
| "printCond f (ECSend c) = printChanRef f c @ ''! ...''"
| "printCond f (ECRecv c _ _) = printChanRef f c @ ''? ...''"

primrec printEffect :: "(integer ⇒ string) ⇒ edgeEffect ⇒ string" where
"printEffect f EEEnd = ''-- end --''"
| "printEffect f EEId = ''ID''"
| "printEffect f EEGoto = ''goto''"
| "printEffect f (EEAssert e) = ''assert('' @ printExpr f e @'')''"
| "printEffect f (EERun n _) = ''run '' @ String.explode n @ ''(...)''"
| "printEffect f (EEAssign v expr) =
printVarRef f v @ '' = '' @ printExpr f expr"
| "printEffect f (EEDecl d) = printVarDecl f d"
| "printEffect f (EESend v es srt) = (
let s = if srt then ''!!'' else ''!'' in
printChanRef f v @ s @ printList (printExpr f) es ''('' '')'' '', '')"
| "printEffect f (EERecv v rs srt rem) = (
let p = if srt then ''??'' else ''?'' in
let (l,r) = if rem then (''('', '')'') else (''<'', ''>'') in
printChanRef f v @ p @ printList (printRecvArg f) rs l r '', '')"

primrec printIndex :: "(integer ⇒ string) ⇒ edgeIndex ⇒ string" where
"printIndex f (Index pos) = f (integer_of_nat pos)"
| "printIndex _ (LabelJump l _) = String.explode l"

definition printEdge :: "(integer ⇒ string) ⇒ nat ⇒ edge ⇒ string" where
"printEdge f indx e = (
let
tStr = printIndex f (target e);
pStr = if prio e < 0 then '' Prio: '' @ f (prio e) else [];
atom = if isAtomic e then λx. x @ '' {A}'' else id;
pEff = λ_. atom (printEffect f (effect e));
contStr = case (cond e) of
ECTrue ⇒ pEff ()
| ECFalse ⇒ pEff ()
| ECSend _ ⇒ pEff()
| ECRecv _ _ _⇒ pEff()
| _ ⇒  atom (''(( '' @ printCond f (cond e) @ '' ))'')
in
f (integer_of_nat indx) @ '' ---> '' @ tStr @ '' => '' @ contStr @ pStr)"

definition printEdges :: "(integer ⇒ string) ⇒ states ⇒ string list" where
"printEdges f es = concat (map (λn. map (printEdge f n) (snd (es !! n)))
(rev [0..<IArray.length es]))"

definition printLabels :: "(integer ⇒ string) ⇒ labels ⇒ string list" where
"printLabels f ls = lm.iterate ls (λ(k,l) res.
(''Label '' @ String.explode k @ '': ''
@ f (integer_of_nat l)) # res) []"

fun printProcesses :: "(integer ⇒ string) ⇒ program ⇒ string list" where
"printProcesses f prog = lm.iterate (proc_data prog)
(λ(k,idx) res.
let (_,start,_,_) = processes prog !! idx in
[] # (''Process '' @ String.explode k) # [] # printEdges f (states prog !! idx)
@ [''START ---> '' @ printIndex f start, []]
@ printLabels f (labels prog !! idx) @ res) []"

(*<*)
(*section {* Instantiations *}
text {* Here instantiations for classes @{class linorder} and @{class hashable} are given for our datatypes.
As we include other structures, which sometime also lack those instantiations, this is done here too. *}
subsection {* Others *}
text {* The following lemmas are needed to make our hashing and linorder sound.

NB: It cannot be proven that
@{prop "Assoc_List.update k v (Assoc_List.update k2 v2 ls) = Assoc_List.update k2 v2 (Assoc_List.update k v ls)"}

Hence our implementation becomes unsound when order of insertion is not fix. *}*)

lemma AL_update_idem:
assumes "Assoc_List.lookup ls k = Some v"
shows "Assoc_List.update k v ls = ls"
proof -
obtain lsl where lsl: "lsl = Assoc_List.impl_of ls" by blast

with assms have "map_of lsl k = Some v" by (simp add: Assoc_List.lookup_def)
hence "AList.update_with_aux v k (λ_. v) lsl = lsl" by (induct lsl) auto
with lsl show ?thesis by (simp add: Assoc_List.update_def Assoc_List.update_with_def Assoc_List_impl_of)
qed

lemma AL_update_update_idem:
assumes "Assoc_List.lookup ls k = Some v"
shows "Assoc_List.update k v (Assoc_List.update k v2 ls) = ls"
proof -
obtain lsl where lsl: "lsl = Assoc_List.impl_of ls" by blast

with assms have "map_of lsl k = Some v" by (simp add: Assoc_List.lookup_def)
hence "AList.update_with_aux v k (λ_. v) (AList.update_with_aux v2 k (λ_. v2) lsl) = lsl" by (induct lsl) auto
with lsl show ?thesis by (metis Assoc_List.update_def Assoc_List_impl_of impl_of_update_with)
qed

lemma AL_update_delete_idem:
assumes "Assoc_List.lookup ls k = None"
shows "Assoc_List.delete k (Assoc_List.update k v ls) = ls"
proof -
obtain lsl where lsl: "lsl = Assoc_List.impl_of ls" by blast

with assms have "map_of lsl k = None" by (simp add: Assoc_List.lookup_def)
hence "AList.delete_aux k (AList.update_with_aux v k (λ_. v) lsl) = lsl" by (induct lsl) auto
with lsl show ?thesis by (simp add: Assoc_List.delete_def Assoc_List.update_def assoc_list.impl_of_inverse impl_of_update_with)
qed

instantiation assoc_list :: (hashable,hashable) hashable
begin
definition "def_hashmap_size (_::('a,'b) assoc_list itself) ≡ (10 :: nat)"
definition [simp]: "hashcode ≡ hashcode ∘ Assoc_List.impl_of"
instance
end

(*
instantiation XXX :: (hashable_uint, hashable_uint) hashable
begin
definition hashcode_XXX :: "('a, 'b) XXX ⇒ nat"
where "hashcode_XXX ≡ hashcode_nat"

definition bounded_hashcode_XXX :: "nat ⇒ ('a, 'b) XXX ⇒ nat"
where "bounded_hashcode_XXX = bounded_hashcode_nat"

definition def_hashmap_size_XXX :: "('a, 'b) XXX itself ⇒ nat"
where "def_hashmap_size_XXX ≡ def_hashmap_size_uint"

instance
apply standard
unfolding def_hashmap_size_XXX_def bounded_hashcode_XXX_def
using hashable_from_hashable_uint by auto
end
*)

instantiation assoc_list :: (linorder,linorder) linorder
begin
definition [simp]: "less_eq_assoc_list (a :: ('a,'b) assoc_list) (b :: ('a,'b) assoc_list) ⟷ lexlist (Assoc_List.impl_of a) ≤ lexlist (Assoc_List.impl_of b)"
definition [simp]: "less_assoc_list (a :: ('a,'b) assoc_list) (b :: ('a,'b) assoc_list) ⟷ lexlist (Assoc_List.impl_of a) < lexlist (Assoc_List.impl_of b)"

instance
apply standard
apply (auto)
apply (metis assoc_list_ext lexlist_ext lexlist_def)
done
end

(* Other instantiations for types from Main *)
(*instantiation iarray :: (linorder) linorder
begin
definition [simp]: "less_eq_iarray (a :: 'a iarray) (b :: 'a iarray) ⟷ lexlist (IArray.list_of a) ≤ lexlist (IArray.list_of b)"
definition [simp]: "less_iarray (a :: 'a iarray) (b :: 'a iarray) ⟷ lexlist (IArray.list_of a) < lexlist (IArray.list_of b)"

instance
apply standard
apply auto
apply (metis iarray.exhaust list_of.simps lexlist_ext lexlist_def)
done
end*)
derive linorder iarray

instantiation lexlist :: (hashable) hashable
begin
definition "def_hashmap_size_lexlist = (λ_ :: 'a lexlist itself. 2 * def_hashmap_size TYPE('a))"

definition "hashcode_lexlist = hashcode o unlex"
instance
proof
from def_hashmap_size[where ?'a = "'a"]
show "1 < def_hashmap_size TYPE('a lexlist)"
qed
end

text ‹Instead of operating on the list representation of an @{const IArray}, we walk it directly,
using the indices.›

primrec walk_iarray' :: "('b ⇒ 'a ⇒ 'b) ⇒ 'a iarray ⇒ 'b ⇒ nat ⇒ nat ⇒ 'b" where
"walk_iarray' _ _ x 0 _ = x"
| "walk_iarray' f a x (Suc l) p = (let y = f x (a !! p)
in walk_iarray' f a y l (p + 1))"

lemma walk_iarray'_Cons:
"walk_iarray' f (IArray (a#xs)) x l (Suc p) = walk_iarray' f (IArray xs) x l p"
by (induct l arbitrary: p x) simp_all

definition walk_iarray :: "('b ⇒ 'a ⇒ 'b) ⇒ 'a iarray ⇒ 'b ⇒ 'b" where
"walk_iarray f a x = walk_iarray' f a x (IArray.length a) 0"

lemma walk_iarray_Cons:
"walk_iarray f (IArray (a#xs)) b = walk_iarray f (IArray xs) (f b a)"

lemma walk_iarray_append:
"walk_iarray f (IArray (xs@[x])) b = f (walk_iarray f (IArray xs) b) x"

lemma walk_iarray_foldl':
"walk_iarray f (IArray xs) x = foldl f x xs"

lemma walk_iarray_foldl:
"walk_iarray f a x = foldl f x (IArray.list_of a)"
by (cases a) (simp add: walk_iarray_foldl')

instantiation iarray :: (hashable) hashable
begin
definition [simp]: "hashcode a = foldl (λh v. h * 33 + hashcode v) 0 (IArray.list_of a)"
definition "def_hashmap_size = (λ_ :: 'a iarray itself. 10)"
instance by standard (simp_all add: def_hashmap_size_iarray_def)

lemma [code]: "hashcode a = walk_iarray (λh v. h * 33 + hashcode v) a 0"
end

(* Other instantiations for types from Main *)
instantiation array :: (linorder) linorder
begin

definition [simp]: "less_eq_array (a :: 'a array) (b :: 'a array) ⟷ lexlist (list_of_array a) ≤ lexlist (list_of_array b)"
definition [simp]: "less_array (a :: 'a array) (b :: 'a array) ⟷ lexlist (list_of_array a) < lexlist (list_of_array b)"

instance
apply standard
apply auto
apply (metis array.exhaust list_of_array.simps lexlist_ext lexlist_def)
done
end

text ‹Same for arrays from the ICF.›
primrec walk_array' :: "('b ⇒ 'a ⇒ 'b) ⇒ 'a array ⇒ 'b ⇒ nat ⇒ nat ⇒ 'b" where
"walk_array' _ _ x 0 _ = x"
| "walk_array' f a x (Suc l) p = (let y = f x (array_get a p)
in walk_array' f a y l (p + 1))"

lemma walk_array'_Cons:
"walk_array' f (Array (a#xs)) x l (Suc p) = walk_array' f (Array xs) x l p"
by (induct l arbitrary: p x) simp_all

definition walk_array :: "('b ⇒ 'a ⇒ 'b) ⇒ 'a array ⇒ 'b ⇒ 'b" where
"walk_array f a x = walk_array' f a x (array_length a) 0"

lemma walk_array_Cons:
"walk_array f (Array (a#xs)) b = walk_array f (Array xs) (f b a)"

lemma walk_array_append:
"walk_array f (Array (xs@[x])) b = f (walk_array f (Array xs) b) x"

lemma walk_array_foldl':
"walk_array f (Array xs) x = foldl f x xs"

lemma walk_array_foldl:
"walk_array f a x = foldl f x (list_of_array a)"
by (cases a) (simp add: walk_array_foldl')

(* TODO: Move to array.thy *)
instantiation array :: (hashable) hashable
begin
definition [simp]: "hashcode a = foldl (λh v. h * 33 + hashcode v) 0 (list_of_array a)"
definition "def_hashmap_size = (λ_ :: 'a array itself. 10)"
instance by standard (simp_all add: def_hashmap_size_array_def)

lemma [code]: "hashcode a = walk_array (λh v. h * 33 + hashcode v) a 0"
end

(*subsection {* Ours *}*)

derive linorder varType
derive linorder variable

instantiation varType :: hashable
begin

definition "def_hashmap_size_varType (_::varType itself) ≡ (10::nat)"

fun hashcode_varType where
"hashcode_varType (VTBounded i1 i2) = hashcode (i1,i2)" |
"hashcode_varType VTChan = 23"

instance by standard (simp add: def_hashmap_size_varType_def)
end

instantiation variable :: hashable
begin

definition "def_hashmap_size_variable (_::variable itself) ≡ (10::nat)"

fun hashcode_variable where
"hashcode_variable (Var i1 i2) = hashcode (i1,i2)" |
"hashcode_variable (VArray i1 i2 ia) = hashcode (i1,i2,ia)"

instance by standard (simp add: def_hashmap_size_variable_def)
end

fun channel_to_tuple where
"channel_to_tuple (Channel io vs iss) = (3::nat,io,lexlist vs, lexlist (map lexlist iss))"
| "channel_to_tuple (HSChannel vs) = (2,0,lexlist vs, lexlist [])"
| "channel_to_tuple InvChannel = (1,0,lexlist [], lexlist [])"

instantiation channel :: linorder
begin
definition [simp]: "less_eq_channel xs ys ⟷ channel_to_tuple xs ≤ channel_to_tuple ys"
definition [simp]: "less_channel xs ys ⟷ channel_to_tuple xs < channel_to_tuple ys"

instance
apply standard
apply (auto)
apply (case_tac x)
apply (case_tac [!] y)
apply (auto dest!: map_inj_on
intro!: inj_onI lexlist_ext
simp: Lex_inject lexlist_def)
done
end

instantiation channel :: hashable
begin

definition "def_hashmap_size_channel (_::channel itself) ≡ (10::nat)"

fun hashcode_channel where
"hashcode_channel (Channel io vs iss) = hashcode (io, vs, iss)"
| "hashcode_channel (HSChannel vs) = 42 * hashcode vs"
| "hashcode_channel InvChannel = 4711"

instance by standard (simp add: def_hashmap_size_channel_def)
end

function pState2HASH where
"pState2HASH ⦇ pid = p, vars = v, pc = c, channels = ch, idx = s, … = m ⦈ = (p, v, c, lexlist ch, s, m)"
by (metis pState.surjective) force
termination by lexicographic_order

lemma pState2HASH_eq:
"pState2HASH x = pState2HASH y ⟹ x = y"
by (cases x, cases y) (auto intro: lexlist_ext simp: lexlist_def)

instantiation pState_ext :: (linorder) linorder
begin
definition [simp]: "less_eq_pState_ext (a :: 'a pState_ext) (b :: 'a pState_ext) ⟷ pState2HASH a ≤ pState2HASH b"
definition [simp]: "less_pState_ext (a :: 'a pState_ext) (b :: 'a pState_ext) ⟷ pState2HASH a < pState2HASH b"

instance by standard (auto simp: pState2HASH_eq)
end

instantiation pState_ext :: (hashable) hashable
begin
definition "def_hashmap_size_pState_ext (_::'a pState_ext itself) ≡ (10::nat)"
definition [simp]: "hashcode ≡ hashcode ∘ pState2HASH"

instance by standard (simp_all add: def_hashmap_size_pState_ext_def)
end

function gState2HASH where
"gState2HASH ⦇ gState.vars = v, channels = ch, timeout = t, procs = p, … = m ⦈ = (v, lexlist ch, t, lexlist p, m)"
by (metis gState.surjective) force
termination by lexicographic_order

lemma gState2HASH_eq:
"gState2HASH x = gState2HASH y ⟹ x = y"
by (cases x, cases y) (auto intro: lexlist_ext simp: lexlist_def)

instantiation gState_ext :: (linorder) linorder
begin
definition [simp]: "less_eq_gState_ext (a :: 'a gState_ext) (b :: 'a gState_ext) ⟷ gState2HASH a ≤ gState2HASH b"
definition [simp]: "less_gState_ext (a :: 'a gState_ext) (b :: 'a gState_ext) ⟷ gState2HASH a < gState2HASH b"

instance by standard (auto simp: gState2HASH_eq)
end

instantiation gState_ext :: (hashable) hashable
begin
definition "def_hashmap_size_gState_ext (_::'a gState_ext itself) ≡ (10::nat)"
definition [simp]: "hashcode ≡ hashcode ∘ gState2HASH"

instance by standard (simp_all add: def_hashmap_size_gState_ext_def)
end

(*>*)
end


# Theory PromelaInvariants

section "Invariants for Promela data structures"
theory PromelaInvariants
begin

text ‹
The different data structures used in the Promela implementation require different invariants,
which are specified in this file. As there is no (useful) way of specifying \emph{correctness} of the implementation,
those invariants are tailored towards proving the finitness of the generated state-space.
›

(*<*)
(*subsection {* Auxiliary lemmas *}*)
lemma foldli_set:
"set (foldli list (λ_. True) (#) xs) = set xs ∪ set list"
by (induct list arbitrary: xs) simp_all

lemma foldli_conj:
"foldli list id (λkv σ. P kv) b ⟷ b ∧ (∀x ∈ set list. P x)"
by (induct list arbitrary: b) simp_all

(* Destroy the evil border of abstraction... *)
lemma lm_ball_Assoc_List_set:
"lm.ball m P ⟷ (∀x ∈ Assoc_List.set m. P x)"
unfolding Assoc_List.set_def
poly_map_iteratei_defs.iteratei_def it_to_it_def Assoc_List.iteratei_def
foldli_conj)

lemma lm_to_list_Assoc_List_set:
"set (lm.to_list l) = Assoc_List.set l"
unfolding Assoc_List.set_def
poly_map_iteratei_defs.iteratei_def it_to_it_def Assoc_List.iteratei_def
foldli_set)

lemma dom_lm_α_Assoc_List_set:
"dom (lm.α v) = fst  (Assoc_List.set v)"
by (simp add: icf_rec_unf Assoc_List.lookup_def Assoc_List.set_def
dom_map_of_conv_image_fst)

lemma ran_lm_α_Assoc_List_set:
"ran (lm.α v) = snd  (Assoc_List.set v)"
by (simp add: icf_rec_unf Assoc_List.lookup_def Assoc_List.set_def
ran_distinct)

lemma lm_ball_eq_ran:
"lm.ball v (λ(k,v). P v) ⟷ ran (lm.α v) ⊆ Collect P"
by (auto simp add: ran_lm_α_Assoc_List_set lm_ball_Assoc_List_set)

lemma lm_ball_lm_to_map_map_weaken:
"∀x ∈ f  set xs. P x ⟹ lm.ball (lm.to_map (map f xs)) P"
by (induct xs) (simp_all add: lm.correct)

lemma Assoc_List_set_eq_lookup:
"(k,v) ∈ Assoc_List.set vs ⟷ Assoc_List.lookup vs k = Some v"

(*>*)

subsection ‹Bounds›

text ‹
Finiteness requires that possible variable ranges are finite, as is the maximium number of processes.
Currently, they are supplied here as constants. In a perfect world, they should be able to be set dynamically.
›

(* NB! Make sure those values coincide with the bounds definied in @{const ppVarType} *)
definition min_var_value :: "integer" where
"min_var_value = -(2^31)"
definition max_var_value :: "integer" where
"max_var_value = (2^31) - 1"

lemma min_max_var_value_simps [simp, intro!]:
"min_var_value < max_var_value"
"min_var_value < 0"
"min_var_value ≤ 0"
"max_var_value > 0"
"max_var_value ≥ 0"

definition "max_procs ≡ 255"
definition "max_channels ≡ 65535"
definition "max_array_size = 65535"

subsection ‹Variables and similar›

fun varType_inv :: "varType ⇒ bool" where
"varType_inv (VTBounded l h)
⟷ l ≥ min_var_value ∧ h ≤ max_var_value ∧ l < h"
| "varType_inv VTChan ⟷ True"

fun variable_inv :: "variable ⇒ bool" where
"variable_inv (Var t val)
⟷ varType_inv t ∧ val ∈ {min_var_value..max_var_value}"
| "variable_inv (VArray t sz ar)
⟷ varType_inv t
∧ sz ≤ max_array_size
∧ IArray.length ar = sz
∧ set (IArray.list_of ar) ⊆ {min_var_value..max_var_value}"

fun channel_inv :: "channel ⇒ bool" where
"channel_inv (Channel cap ts q)
⟷ cap ≤ max_array_size
∧ cap ≥ 0
∧ set ts ⊆ Collect varType_inv
∧ length ts ≤ max_array_size
∧ length q ≤ max_array_size
∧ (∀x ∈ set q. length x = length ts
∧ set x ⊆ {min_var_value..max_var_value})"
| "channel_inv (HSChannel ts)
⟷ set ts ⊆ Collect varType_inv ∧ length ts ≤ max_array_size"
| "channel_inv InvChannel ⟷ True"

lemma varTypes_finite:
"finite (Collect varType_inv)"
proof (rule finite_subset)
show "Collect (varType_inv) ⊆
{VTChan}
∪ (λ(l,h). VTBounded l h)
 ({min_var_value..max_var_value} × {min_var_value..max_var_value})"
apply (rule subsetI)
apply (case_tac x)
apply auto
done

show "finite ..." by auto
qed

lemma variables_finite:
"finite (Collect variable_inv)"
proof (rule finite_subset)
let ?mm = "{min_var_value..max_var_value}"
let ?V1 = "(λ(t,val). Var t val)  ({vt. varType_inv vt} × ?mm)"
let ?V2 = "(λ(t,sz,ar). VArray t sz ar)
 ({vt. varType_inv vt}
× {0..max_array_size}
× {ar. IArray.length ar ≤ max_array_size
∧ set (IArray.list_of ar) ⊆ ?mm})"

{
fix A :: "'a set"
let ?LS = "{xs. set xs ⊆ A ∧ length xs ≤ max_array_size }"
let ?AS = "{ar. IArray.length ar ≤ max_array_size
∧ set (IArray.list_of ar) ⊆ A}"

assume "finite A"
hence "finite ?LS" by (simp add: finite_lists_length_le)
moreover have "?AS ⊆ IArray  ?LS"
apply (auto simp: image_def)
apply (rule_tac x = "IArray.list_of x" in exI)
apply auto
apply (metis iarray.exhaust list_of.simps)
done
ultimately have "finite ?AS" by (auto simp add: finite_subset)
} note finite_arr = this

show "Collect variable_inv ⊆ (?V1 ∪ ?V2)"
apply (rule subsetI)
apply (case_tac x)
done

show "finite ..." by (blast intro: varTypes_finite finite_arr)
qed

lemma channels_finite:
"finite (Collect channel_inv)"
proof (rule finite_subset)
let ?C1 =
"(λ(cap,ts,q). Channel cap ts q)
 ({0..max_array_size}
× {ts. set ts ⊆ Collect varType_inv ∧ length ts ≤ max_array_size}
× {q. set q ⊆ {x. set x ⊆ {min_var_value..max_var_value}
∧ length x ≤ max_array_size}
∧ length q ≤ max_array_size})"
let ?C2 =
"HSChannel  {ts. set ts ⊆ Collect varType_inv ∧ length ts ≤ max_array_size}"
let ?C3 = "{InvChannel}"

show "(Collect channel_inv) ⊆ ?C1 ∪ ?C2 ∪ ?C3"
apply (rule subsetI)
apply (case_tac x)
done

show "finite ..." by (blast intro: finite_lists_length_le varTypes_finite)+
qed

text ‹To give an upper bound of variable names, we need a way to calculate it.›

primrec procArgName :: "procArg ⇒ String.literal" where
"procArgName (ProcArg _ name) = name"

primrec varDeclName :: "varDecl ⇒ String.literal" where
"varDeclName (VarDeclNum _ _ name _ _) = name"
| "varDeclName (VarDeclChan name _ _) = name"

primrec procVarDeclName :: "procVarDecl ⇒ String.literal" where
"procVarDeclName (ProcVarDeclNum _ _ name _ _) = name"
| "procVarDeclName (ProcVarDeclChan name _) = name"

definition edgeDecls :: "edge ⇒ procVarDecl set" where
"edgeDecls e = (
case effect e of
EEDecl p ⇒ {p}
|  _ ⇒ {})"

lemma edgeDecls_finite:
"finite (edgeDecls e)"
by (simp add: edgeDecls_def split: edgeEffect.split)

definition edgeSet :: "states ⇒ edge set" where
"edgeSet s = set (concat (map snd (IArray.list_of s)))"

lemma edgeSet_finite:
"finite (edgeSet s)"

definition statesDecls :: "states ⇒ procVarDecl set" where
"statesDecls s = ⋃(edgeDecls  (edgeSet s))"

definition statesNames :: "states ⇒ String.literal set" where
"statesNames s = procVarDeclName  statesDecls s"

lemma statesNames_finite:
"finite (statesNames s)"
by (simp add: edgeSet_finite edgeDecls_finite statesNames_def statesDecls_def)

fun process_names :: "states ⇒ process ⇒ String.literal set" where
"process_names ss (_, _, args, decls) =
statesNames ss
∪ procArgName  set args
∪ varDeclName  set decls
∪ {STR ''_'', STR ''__assert__'', STR ''_pid''}" (* dunno if this is ok as a fixed set ... *)

lemma process_names_finite:
"finite (process_names ss p)"
by (cases p) (simp add: statesNames_finite)

definition vardict_inv :: "states ⇒ process ⇒ var_dict ⇒ bool" where
"vardict_inv ss p vs
⟷ lm.ball vs (λ(k,v). k ∈ process_names ss p ∧ variable_inv v)"

lemma vardicts_finite:
"finite (Collect (vardict_inv ss p))"
proof -
have "Assoc_List.set  Collect (vardict_inv ss p) ⊆
Pow (process_names ss p × {v. variable_inv v})"
by (auto simp add: lm_ball_Assoc_List_set vardict_inv_def)

moreover have "finite ..."
using process_names_finite variables_finite
by simp
ultimately show ?thesis by (metis finite_Assoc_List_set_image finite_subset)
qed

lemma lm_to_map_vardict_inv:
assumes "∀(k,v) ∈ set xs. k ∈ process_names ss proc ∧ variable_inv v"
shows "vardict_inv ss proc (lm.to_map xs)"
using assms
unfolding vardict_inv_def
by (auto simp add: lm.correct dest: map_of_SomeD)

subsection ‹Invariants of a process›

(* The definition of a channel to be between -1 and max_channels definitly lacks the necessary abstraction ... *)
definition pState_inv :: "program ⇒ pState ⇒ bool" where
"pState_inv prog p
⟷ pid p ≤ max_procs
∧ pState.idx p < IArray.length (states prog)
∧ IArray.length (states prog) = IArray.length (processes prog)
∧ pc p < IArray.length ((states prog) !! pState.idx p)
∧ set (pState.channels p) ⊆ {-1..<integer_of_nat max_channels}
∧ length (pState.channels p) ≤ max_channels
∧ vardict_inv ((states prog) !! pState.idx p)
((processes prog) !! pState.idx p)
(pState.vars p)"

lemma pStates_finite:
"finite (Collect (pState_inv prog))"
proof -
let ?P1 = "{..max_procs::nat}"
let ?P2 = "{..IArray.length (states prog)}"
let ?P3 = "{..Max (IArray.length  (set (IArray.list_of (states prog))))}"
let ?P4 = "{cs. set cs ⊆ {-1..<integer_of_nat max_channels}
∧ length cs ≤ max_channels}"
let ?P5 = "⋃x∈{..IArray.length (states prog)}.
Collect (vardict_inv (states prog !! x) (processes prog !! x))"
let ?P = "?P1 × ?P2 × ?P3 × ?P4 × ?P5"

have "{p. pState_inv prog p} ⊆
(λ(pid,idx,pc,channels,vars). pState.make pid vars pc channels idx)  ?P"
unfolding pState_inv_def image_def [of _ ?P]
apply (tactic ‹Record.split_simp_tac @{context} [] (K ~1) 1›)
apply auto
apply (rule order_trans [OF less_imp_le])
apply (auto intro!: Max_ge)
done
moreover
have "finite ?P4" by (fastforce intro: finite_lists_length_le)
hence "finite ?P" by (auto intro: finite_cartesian_product simp: vardicts_finite)

ultimately show ?thesis by (elim finite_subset) (rule finite_imageI)
qed

text ‹
Throughout the calculation of the semantic engine, a modified process is not necessarily part of @{term "procs g"}.
Hence we need to establish an additional constraint for the relation between a global and a process state.›

definition cl_inv :: "('a gState_scheme * pState) ⇒ bool" where
"cl_inv gp = (case gp of (g,p) ⇒
length (pState.channels p) ≤ length (gState.channels g))"

lemma cl_inv_lengthD:
"cl_inv (g,p) ⟹ length (pState.channels p) ≤ length (gState.channels g)"
unfolding cl_inv_def
by auto

lemma cl_invI:
"length (pState.channels p) ≤ length (gState.channels g) ⟹ cl_inv (g,p)"
unfolding cl_inv_def by auto

lemma cl_inv_trans:
"length (channels g) ≤ length (channels g') ⟹ cl_inv (g,p) ⟹ cl_inv (g',p)"

lemma cl_inv_vars_update[intro!]:
"cl_inv (g,p) ⟹ cl_inv (g, pState.vars_update vs p)"
"cl_inv (g,p) ⟹ cl_inv (gState.vars_update vs g, p)"

lemma cl_inv_handshake_update[intro!]:
"cl_inv (g,p) ⟹ cl_inv (g⦇handshake := h⦈,p)"

lemma cl_inv_hsdata_update[intro!]:
"cl_inv (g,p) ⟹ cl_inv (g⦇hsdata := h⦈,p)"

lemma cl_inv_procs_update[intro!]:
"cl_inv (g,p) ⟹ cl_inv (g⦇procs := ps⦈,p)"

lemma cl_inv_channels_update:
assumes "cl_inv (g,p)"
shows "cl_inv (gState.channels_update (λcs. cs[i:=c]) g, p)"
using assms unfolding cl_inv_def
by simp

subsection ‹Invariants of the global state›

text ‹Note that @{term gState_inv} must be defined in a way to be applicable to both @{typ gState} and @{typ gState⇩I}.›

definition gState_inv :: "program ⇒ 'a gState_scheme ⇒ bool" where
"gState_inv prog g
⟷ length (procs g) ≤ max_procs
∧ (∀p ∈ set (procs g). pState_inv prog p ∧ cl_inv (g,p))
∧ length (channels g) ≤ max_channels
∧ set (channels g) ⊆ Collect channel_inv
∧ lm.ball (vars g) (λ(k,v). variable_inv v)"

text ‹The set of global states adhering to the terms of @{const gState_inv} is not finite.
But the set of all global states that can be constructed by the semantic engine from one starting state is.
Thus we establish a progress relation, \ie all successors of a state @{term g} relate to @{term g} under this specification.›

definition gState_progress_rel :: "program ⇒ ('a gState_scheme) rel" where
"gState_progress_rel p = {(g,g'). gState_inv p g ∧ gState_inv p g'
∧ length (channels g) ≤ length (channels g')
∧ dom (lm.α (vars g)) = dom (lm.α (vars g'))}"

lemma gState_progress_rel_gState_invI1[intro]:
"(g,g') ∈ gState_progress_rel prog ⟹ gState_inv prog g"

lemma gState_progress_rel_gState_invI2[intro]:
"(g,g') ∈ gState_progress_rel prog ⟹ gState_inv prog g'"

lemma gState_progress_relI:
assumes "gState_inv prog g"
and "gState_inv prog g'"
and "length (channels g) ≤ length (channels g')"
and "dom (lm.α (vars g)) = dom (lm.α (vars g'))"
shows "(g,g') ∈ gState_progress_rel prog"
unfolding gState_progress_rel_def
using assms
by auto

lemma gState_progress_refl[simp,intro!]:
"gState_inv prog g ⟹ (g,g) ∈ (gState_progress_rel prog)"
unfolding gState_progress_rel_def
by auto

lemma refl_on_gState_progress_rel:
"refl_on (Collect (gState_inv prog)) (gState_progress_rel prog)"
by (auto intro!: refl_onI)

lemma trans_gState_progress_rel[simp]:
"trans (gState_progress_rel prog)"
by (intro transI) (simp add: gState_progress_rel_def)

lemmas gState_progress_rel_trans [trans] = trans_gState_progress_rel[THEN transD]

lemma gState_progress_rel_trancl_id[simp]:
"(gState_progress_rel prog)⇧+ = gState_progress_rel prog"
by simp

lemma gState_progress_rel_rtrancl_absorb:
assumes "gState_inv prog g"
shows "(gState_progress_rel prog)⇧*  {g} = gState_progress_rel prog  {g}"
using assms refl_on_gState_progress_rel
by (intro Image_absorb_rtrancl) auto

text ‹
The main theorem: The set of all global states reachable from an initial state, is finite.
›
lemma gStates_finite:
fixes g :: "gState"
shows "finite ((gState_progress_rel prog)⇧*  {g})"
proof (cases "gState_inv prog g")
case False hence "(gState_progress_rel prog)⇧*  {g} = {g}"
by (intro Image_empty_rtrancl_Image_id)
thus ?thesis by simp
next
case True
let ?G1 = "{m. dom (lm.α m) = dom (lm.α (vars g))
∧ ran (lm.α m) ⊆ Collect variable_inv }"
let ?G2 = "{cs. set cs ⊆ Collect channel_inv
∧ length cs ≤ max_channels}"
let ?G3 = "{True, False}"
let ?G4 = "{ps. set ps ⊆ Collect (pState_inv prog)
∧ length ps ≤ max_procs}"

let ?G = "?G1 × ?G2 × ?G3 × ?G4"
let ?G' = "(λ(vars,chans,t,ps). gState.make vars chans t ps)  ?G"

have G1: "finite ?G1"
proof (rule finite_subset)
show "?G1 ⊆ {v'. fst  Assoc_List.set v' = fst  Assoc_List.set (vars g)
∧ snd  Assoc_List.set v' ⊆ Collect variable_inv}"
show "finite ..." (is "finite ?X")
proof (rule finite_Assoc_List_set_image, rule finite_subset)
show "Assoc_List.set  ?X ⊆
Pow (fst  Assoc_List.set (vars g) × Collect variable_inv)"
by auto
show "finite ..." by (auto simp add: variables_finite dom_lm_α_Assoc_List_set[symmetric])
qed
qed

have "finite ((gState_progress_rel prog)  {g})"
proof (rule finite_subset)
show "(gState_progress_rel prog)  {g} ⊆
(λ(vars,chans,t,ps). gState.make vars chans t ps)  ?G"
apply (clarsimp simp add: image_def gState_inv_def gState.defs gState_progress_rel_def)
apply (rule_tac x = "vars x" in exI)
apply (rule_tac x = "channels x" in exI)
apply (case_tac "timeout x")
apply clarsimp
apply (rule_tac x="procs x" in exI)
apply auto
done
show "finite ..." using G1
by (blast intro: finite_lists_length_le channels_finite pStates_finite)
qed
with gState_progress_rel_rtrancl_absorb[OF True] show ?thesis by simp
qed

lemma gState_progress_rel_channels_update:
assumes "gState_inv prog g"
and "channel_inv c"
and "i < length (channels g)"
shows "(g,gState.channels_update (λcs. cs[i:=c]) g) ∈ gState_progress_rel prog"
using assms
by (auto intro!: gState_progress_relI
dest!: subsetD[OF set_update_subset_insert])

lemma gState_progress_rel_channels_update_step:
assumes "gState_inv prog g"
and step: "(g,g') ∈ gState_progress_rel prog"
and "channel_inv c"
and "i < length (channels g')"
shows "(g,gState.channels_update (λcs. cs[i:=c]) g') ∈ gState_progress_rel prog"
proof -
note step
also hence "gState_inv prog g'" by blast
note gState_progress_rel_channels_update[OF this assms(3,4)]
finally show ?thesis .
qed

subsection ‹Invariants of the program›

text ‹
Naturally, we need our program to also adhere to certain invariants. Else we can't show, that
the generated states are correct according to the invariants above.
›

definition program_inv where
"program_inv prog
⟷ IArray.length (states prog) > 0
∧ IArray.length (states prog) = IArray.length (processes prog)
∧ (∀s ∈ set (IArray.list_of (states prog)). IArray.length s > 0)
∧ lm.ball (proc_data prog)
(λ(_,sidx).
sidx < IArray.length (processes prog)
∧ fst (processes prog !! sidx) = sidx)
∧ (∀(sidx,start,procArgs,args) ∈ set (IArray.list_of (processes prog)).
(∃s. start = Index s ∧ s < IArray.length (states prog !! sidx)))"

lemma program_inv_length_states:
assumes "program_inv prog"
and "n < IArray.length (states prog)"
shows "IArray.length (states prog !! n) > 0"
using assms by (simp add: program_inv_def)

lemma program_invI:
assumes "0 < IArray.length (states prog)"
and "IArray.length (states prog) = IArray.length (processes prog)"
and "⋀s. s ∈ set (IArray.list_of (states prog))
⟹ 0 < IArray.length s"
and "⋀sidx. sidx ∈ ran (lm.α (proc_data prog))
⟹ sidx < IArray.length (processes prog)
∧ fst (processes prog !! sidx) = sidx"
and "⋀sidx start procArgs args.
(sidx,start,procArgs,args) ∈ set (IArray.list_of (processes prog))
⟹ ∃s. start = Index s ∧ s < IArray.length (states prog !! sidx)"
shows "program_inv prog"
unfolding program_inv_def
using assms

end


# Theory Promela

section "Formalization of Promela semantics"
theory Promela
imports
PromelaInvariants
PromelaStatistics
begin

text ‹Auxiliary›

lemma mod_integer_le:
"a ≤ b ⟹ 0 < a ⟹ x mod (a + 1) ≤ b" for a b x :: integer
by (metis add_pos_nonneg discrete not_less order.strict_trans2
unique_euclidean_semiring_numeral_class.pos_mod_bound zero_le_one)

lemma mod_integer_ge:
"b ≤ 0 ⟹ 0 < a ⟹ b ≤ x mod (a+1)" for a b x :: integer
unique_euclidean_semiring_numeral_class.pos_mod_sign)

text ‹
After having defined the datastructures, we present in this theory how to construct the transition system and how to generate the successors of a state, \ie the real semantics of a Promela program.
For the first task, we take the enriched AST as input, the second one operates on the transition system.
›

subsection ‹Misc Helpers›
definition add_label :: "String.literal ⇒ labels ⇒ nat ⇒ labels" where
"add_label l lbls pos = (
case lm.lookup l lbls of
None ⇒ lm.update l pos lbls
| Some _ ⇒ abortv STR ''Label given twice: '' l (λ_. lbls))"

definition min_prio :: "edge list ⇒ integer ⇒ integer" where
"min_prio es start = Min ((prio  set es) ∪ {start})"

lemma min_prio_code [code]:
"min_prio es start = fold  (λe pri. if prio e < pri then prio e else pri) es start"
proof -
from Min.set_eq_fold have "Min (set (start # map prio es)) = fold min (map prio es) start" by metis
also have "... = fold (min ∘ prio) es start" by (simp add: fold_map)
also have "... = fold  (λe pri. if prio e < pri then prio e else pri) es start" by (auto intro!: fold_cong)
finally show ?thesis by (simp add: min_prio_def)
qed

definition for_all :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"for_all f xs ⟷ (∀x ∈ set xs. f x)"

lemma for_all_code[code]:
"for_all f xs ⟷ foldli xs id (λkv σ. f kv) True"

definition find_remove :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a option × 'a list" where
"find_remove P xs = (case List.find P xs of None ⇒ (None, xs)
| Some x ⇒ (Some x, List.remove1 x xs))"

lemma find_remove_code [code]:
"find_remove P [] = (None, [])"
"find_remove P (x#xs) = (if P x then (Some x, xs)
else apsnd (Cons x) (find_remove P xs))"
by (induct xs) (auto simp add: find_remove_def dest: find_SomeD split: option.split)

lemma find_remove_subset:
"find_remove P xs = (res, xs') ⟹ set xs' ⊆ set xs"
unfolding find_remove_def
using set_remove1_subset
by (force split: option.splits)

lemma find_remove_length:
"find_remove P xs = (res, xs') ⟹ length xs' ≤ length xs"
unfolding find_remove_def
by (induct xs arbitrary: res xs') (auto split: if_splits option.splits)

subsection ‹Variable handling›

text ‹
Handling variables, with their different scopes (global vs. local),
and their different types (array vs channel vs bounded) is one of the main challenges
of the implementation.
›

fun lookupVar :: "variable ⇒ integer option ⇒ integer" where
"lookupVar (Var _ val) None = val"
| "lookupVar (Var _ _) (Some _) = abort STR ''Array used on var'' (λ_.0)"
| "lookupVar (VArray _ _ vals) None = vals !! 0" (* sic! *)
| "lookupVar (VArray _ siz vals) (Some idx) = vals !! nat_of_integer idx"

primrec checkVarValue :: "varType ⇒ integer ⇒ integer" where
"checkVarValue (VTBounded lRange hRange) val = (
if val ≤ hRange ∧ val ≥ lRange then val
else ― ‹overflowing is well-defined and may actually be used (e.g. bool)›
if lRange = 0 ∧ val > 0
then val mod (hRange + 1)
else ― ‹we do not want to implement C-semantics (ie type casts)›
abort STR ''Value overflow'' (λ_. lRange))"
| "checkVarValue VTChan val = (
if val < min_var_value ∨ val > max_var_value
then abort STR ''Value overflow'' (λ_. 0)
else val)"

lemma [simp]:
"variable_inv (Var VTChan 0)"
by simp

context
fixes type :: varType
assumes "varType_inv type"
begin

lemma checkVarValue_bounded:
"checkVarValue type val ∈ {min_var_value..max_var_value}"
using ‹varType_inv type›
by (cases type) (auto intro: mod_integer_le mod_integer_ge)

lemma checkVarValue_bounds:
"min_var_value ≤ checkVarValue type val"
"checkVarValue type val ≤ max_var_value"
using checkVarValue_bounded [of val] by simp_all

lemma checkVarValue_Var:
"variable_inv (Var type (checkVarValue type val))"
using ‹varType_inv type› by (simp add: checkVarValue_bounds)

end

fun editVar :: "variable ⇒ integer option ⇒ integer ⇒ variable" where
"editVar (Var type _ ) None val = Var type (checkVarValue type val)"
| "editVar (Var _ _) (Some _) _ = abort STR ''Array used on var'' (λ_. Var VTChan 0)"
| "editVar (VArray type siz vals) None val = (
let lv = IArray.list_of vals in
let v' = lv[0:=checkVarValue type val] in
VArray type siz (IArray v'))"
| "editVar (VArray type siz vals) (Some idx) val = (
let lv = IArray.list_of vals in
let v' = lv[(nat_of_integer idx):=checkVarValue type val] in
VArray type siz (IArray v'))"

lemma editVar_variable_inv:
assumes "variable_inv v"
shows "variable_inv (editVar v idx val)"
proof (cases v)
case (Var type val) with assms have "varType_inv type" by simp
with Var show ?thesis
by (cases idx)
(auto intro!: checkVarValue_Var
simp del: checkVarValue.simps variable_inv.simps)
next
case (VArray type siz vals)
with assms have [simp, intro!]: "varType_inv type" by simp

show ?thesis
proof (cases idx)
case None with assms VArray show ?thesis
by (cases "IArray.list_of vals") (auto intro!: checkVarValue_bounds)
next
case (Some i)
note upd_cases = in_set_upd_cases[where l="IArray.list_of vals" and i="nat_of_integer i"]

from Some VArray assms show ?thesis
by (cases type)
(auto elim!: upd_cases intro!: mod_integer_le mod_integer_ge simp add: min_var_value_def)
qed
qed

definition getVar'
:: "bool ⇒ String.literal ⇒ integer option
⇒ 'a gState_scheme ⇒ pState
⇒ integer option"
where
"getVar' gl v idx g p = (
let vars = if gl then gState.vars g else pState.vars p in
map_option (λx. lookupVar x idx) (lm.lookup v vars))"

definition setVar'
:: "bool ⇒ String.literal ⇒ integer option
⇒ integer
⇒ 'a gState_scheme ⇒ pState
⇒ 'a gState_scheme * pState"
where
"setVar' gl v idx val g p = (
if gl then
if v = STR ''_'' then (g,p) ― ‹‹''_''› is a write-only scratch variable›
else case lm.lookup v (gState.vars g) of
None ⇒ abortv STR ''Unknown global variable: '' v (λ_. (g,p))
| Some x ⇒ (g⦇gState.vars := lm.update v (editVar x idx val)
(gState.vars g)⦈
, p)
else
case lm.lookup v (pState.vars p) of
None ⇒ abortv STR ''Unknown proc variable: '' v (λ_. (g,p))
| Some x ⇒ (g, p⦇pState.vars := lm.update v (editVar x idx val)
(pState.vars p)⦈))"

lemma setVar'_gState_inv:
assumes "gState_inv prog g"
shows "gState_inv prog (fst (setVar' gl v idx val g p))"
unfolding setVar'_def using assms
by (auto simp add: gState_inv_def lm.correct
intro: editVar_variable_inv
split: option.splits)

lemma setVar'_gState_progress_rel:
assumes "gState_inv prog g"
shows "(g, fst (setVar' gl v idx val g p)) ∈ gState_progress_rel prog"
apply (intro gState_progress_relI)
apply (fact assms)
apply (fact setVar'_gState_inv[OF assms])
apply (auto simp: setVar'_def lm.correct split: option.splits)
done

lemma vardict_inv_process_names:
assumes "vardict_inv ss proc v"
and "lm.lookup k v = Some x"
shows "k ∈ process_names ss proc"
using assms
by (auto simp add: lm.correct vardict_inv_def)

lemma vardict_inv_variable_inv:
assumes "vardict_inv ss proc v"
and "lm.lookup k v = Some x"
shows "variable_inv x"
using assms
by (auto simp add: lm.correct vardict_inv_def)

lemma vardict_inv_updateI:
assumes "vardict_inv ss proc vs"
and "x ∈ process_names ss proc"
and "variable_inv v"
shows "vardict_inv ss proc (lm.update x v vs)"
using assms
by (auto simp add: lm.correct vardict_inv_def)

lemma update_vardict_inv:
assumes "vardict_inv ss proc v"
and "lm.lookup k v = Some x"
and "variable_inv x'"
shows "vardict_inv ss proc (lm.update k x' v)"
using assms
by (auto intro!: vardict_inv_updateI vardict_inv_process_names)

lemma setVar'_pState_inv:
assumes "pState_inv prog p"
shows "pState_inv prog (snd (setVar' gl v idx val g p))"
unfolding setVar'_def using assms
by (auto split: if_splits option.splits
intro: update_vardict_inv editVar_variable_inv vardict_inv_variable_inv)

lemma setVar'_cl_inv:
assumes "cl_inv (g,p)"
shows "cl_inv (setVar' gl v idx val g p)"
unfolding setVar'_def using assms
by (auto split: if_splits option.splits)

definition withVar'
:: "bool ⇒ String.literal ⇒ integer option
⇒ (integer ⇒ 'x)
⇒ 'a gState_scheme ⇒ pState
⇒ 'x"
where
"withVar' gl v idx f g p = f (the (getVar' gl v idx g p))"

definition withChannel'
:: "bool ⇒ String.literal ⇒ integer option
⇒ (nat ⇒ channel ⇒ 'x)
⇒ 'a gState_scheme ⇒ pState
⇒ 'x"
where
"withChannel' gl v idx f g p = (
let error = λ_. abortv STR ''Variable is not a channel: '' v
(λ_. f 0 InvChannel) in
let abort = λ_. abortv STR ''Channel already closed / invalid: '' v
(λ_. f 0 InvChannel)
in withVar' gl v idx (λi. let i = nat_of_integer i in
if i ≥ length (channels g) then error ()
else let c = channels g ! i in
case c of
InvChannel ⇒ abort ()
| _ ⇒ f i c) g p)"

subsection ‹Expressions›

text ‹Expressions are free of side-effects.

This is in difference to SPIN, where @{term run} is an expression with side-effect. We treat @{term run} as a statement.›

abbreviation "trivCond x ≡ if x then 1 else 0"

fun exprArith :: "'a gState_scheme ⇒ pState ⇒ expr ⇒ integer"
and pollCheck :: "'a gState_scheme ⇒ pState ⇒ channel ⇒ recvArg list ⇒ bool
⇒ bool"
and recvArgsCheck :: "'a gState_scheme ⇒ pState ⇒ recvArg list ⇒ integer list
⇒ bool"
where
"exprArith g p (ExprConst x) = x"
| "exprArith g p (ExprMConst x _) = x"

| "exprArith g p ExprTimeOut = trivCond (timeout g)"

| "exprArith g p (ExprLen (ChanRef (VarRef gl name None))) =
withChannel' gl name None (
λ_ c. case c of
Channel _ _ q ⇒ integer_of_nat (length q)
| HSChannel _ ⇒ 0) g p"

| "exprArith g p (ExprLen (ChanRef (VarRef gl name (Some idx)))) =
withChannel' gl name (Some (exprArith g p idx)) (
λ_ c. case c of
Channel _ _ q ⇒ integer_of_nat (length q)
| HSChannel _ ⇒ 0) g p"

| "exprArith g p (ExprEmpty (ChanRef (VarRef gl name None))) =
trivCond (withChannel' gl name None (
λ_ c. case c of Channel _ _ q ⇒ (q = [])
| HSChannel _ ⇒ True) g p)"

| "exprArith g p (ExprEmpty (ChanRef (VarRef gl name (Some idx)))) =
trivCond (withChannel' gl name (Some (exprArith g p idx)) (
λ_ c. case c of Channel _ _ q ⇒ (q = [])
| HSChannel _ ⇒ True) g p)"

| "exprArith g p (ExprFull (ChanRef(VarRef gl name None))) =
trivCond (withChannel' gl name None (
λ_ c. case c of
Channel cap _ q ⇒ integer_of_nat (length q) ≥ cap
| HSChannel _ ⇒ False) g p)"

| "exprArith g p (ExprFull (ChanRef(VarRef gl name (Some idx)))) =
trivCond (withChannel' gl name (Some (exprArith g p idx)) (
λ_ c. case c of
Channel cap _ q ⇒ integer_of_nat (length q) ≥ cap
| HSChannel _ ⇒ False) g p)"

| "exprArith g p (ExprVarRef (VarRef gl name None)) =
withVar' gl name None id g p"

| "exprArith g p (ExprVarRef (VarRef gl name (Some idx))) =
withVar' gl name (Some (exprArith g p idx)) id g p"

| "exprArith g p (ExprUnOp UnOpMinus expr) = 0 - exprArith g p expr"
| "exprArith g p (ExprUnOp UnOpNeg expr) = ((exprArith g p expr) + 1) mod 2"

| "exprArith g p (ExprBinOp BinOpAdd lexpr rexpr) =
(exprArith g p lexpr) + (exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpSub lexpr rexpr) =
(exprArith g p lexpr) - (exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpMul lexpr rexpr) =
(exprArith g p lexpr) * (exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpDiv lexpr rexpr) =
(exprArith g p lexpr) div (exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpMod lexpr rexpr) =
(exprArith g p lexpr) mod (exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpGr lexpr rexpr) =
trivCond (exprArith g p lexpr > exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpLe lexpr rexpr) =
trivCond (exprArith g p lexpr < exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpGEq lexpr rexpr) =
trivCond (exprArith g p lexpr ≥ exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpLEq lexpr rexpr) =
trivCond (exprArith g p lexpr ≤ exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpEq lexpr rexpr) =
trivCond (exprArith g p lexpr = exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpNEq lexpr rexpr) =
trivCond (exprArith g p lexpr ≠ exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpAnd lexpr rexpr) =
trivCond (exprArith g p lexpr ≠ 0 ∧ exprArith g p rexpr ≠ 0)"

| "exprArith g p (ExprBinOp BinOpOr lexpr rexpr) =
trivCond (exprArith g p lexpr ≠ 0 ∨ exprArith g p rexpr ≠ 0)"

| "exprArith g p (ExprCond cexpr texpr fexpr) =
(if exprArith g p cexpr ≠ 0 then exprArith g p texpr
else exprArith g p fexpr)"

| "exprArith g p (ExprPoll (ChanRef (VarRef gl name None)) rs srt) =
trivCond (withChannel' gl name None (
λ_ c. pollCheck g p c rs srt) g p)"

| "exprArith g p (ExprPoll (ChanRef (VarRef gl name (Some idx))) rs srt) =
trivCond (withChannel' gl name (Some (exprArith g p idx)) (
λ_ c. pollCheck g p c rs srt) g p)"

| "pollCheck g p InvChannel _ _ =
abort STR ''Channel already closed / invalid.'' (λ_. False)"
| "pollCheck g p (HSChannel _) _ _ = False"
| "pollCheck g p (Channel _ _ q) rs srt = (
if q = [] then False
else if ¬ srt then recvArgsCheck g p rs (hd q)
else List.find (recvArgsCheck g p rs) q ≠ None)"

| "recvArgsCheck _ _ [] [] = True"
| "recvArgsCheck _ _ _  [] =
abort STR ''Length mismatch on receiving.'' (λ_. False)"
| "recvArgsCheck _ _ []  _ =
abort STR ''Length mismatch on receiving.'' (λ_. False)"
| "recvArgsCheck g p (r#rs) (v#vs) = ((
case r of
RecvArgConst c ⇒ c = v
| RecvArgMConst c _ ⇒ c = v
| RecvArgVar var ⇒ True
| RecvArgEval e ⇒ exprArith g p e = v ) ∧ recvArgsCheck g p rs vs)"

text ‹@{const getVar'} etc.\ do operate on name, index, \ldots directly. Lift them to use @{const VarRef} instead.›

fun liftVar where
"liftVar f (VarRef gl v idx) argm g p =
f gl v (map_option (exprArith g p) idx) argm g p"

definition "getVar v = liftVar (λgl v idx arg. getVar' gl v idx) v ()"
definition "setVar = liftVar setVar'"
definition "withVar = liftVar withVar'"

primrec withChannel
where "withChannel (ChanRef v) = liftVar withChannel' v"

lemma setVar_gState_progress_rel:
assumes "gState_inv prog g"
shows "(g, fst (setVar v val g p)) ∈ gState_progress_rel prog"
unfolding setVar_def
by (cases v) (simp add: setVar'_gState_progress_rel[OF assms])

lemmas setVar_gState_inv =
setVar_gState_progress_rel[THEN gState_progress_rel_gState_invI2]

lemma setVar_pState_inv:
assumes "pState_inv prog p"
shows "pState_inv prog (snd (setVar v val g p))"
unfolding setVar_def
by (cases v) (auto simp add: setVar'_pState_inv assms)

lemma setVar_cl_inv:
assumes "cl_inv (g,p)"
shows "cl_inv (setVar v val g p)"
unfolding setVar_def
by (cases v) (auto simp add: setVar'_cl_inv assms)

subsection ‹Variable declaration›

lemma channel_inv_code [code]:
"channel_inv (Channel cap ts q)
⟷ cap ≤ max_array_size
∧ 0 ≤ cap
∧ for_all varType_inv ts
∧ length ts ≤ max_array_size
∧ length q ≤ max_array_size
∧ for_all (λx. length x = length ts
∧ for_all (λy. y ≥ min_var_value
∧ y ≤ max_var_value) x) q"
"channel_inv (HSChannel ts)
⟷ for_all varType_inv ts ∧ length ts ≤ max_array_size"
by (auto simp add: for_all_def) force+

primrec toVariable
:: "'a gState_scheme ⇒ pState ⇒ varDecl ⇒ String.literal * variable * channels"
where
"toVariable g p (VarDeclNum lb hb name siz init) = (
let type = VTBounded lb hb in
if ¬ varType_inv type then abortv STR ''Invalid var def (varType_inv failed): '' name
(λ_. (name, Var VTChan 0, []))
else
let
init = checkVarValue type (case init of
None ⇒ 0
| Some e ⇒ exprArith g p e);
v = (case siz of
None ⇒ Var type init
| Some s ⇒ if nat_of_integer s ≤ max_array_size
then VArray type (nat_of_integer s)
(IArray.tabulate (s, λ_. init))
else abortv STR ''Invalid var def (array too large): '' name
(λ_. Var VTChan 0))
in
(name, v, []))"

| "toVariable g p (VarDeclChan name siz types) = (
let
size = (case siz of None ⇒ 1 | Some s ⇒ nat_of_integer s);
chans = (case types of
None ⇒ []
| Some (cap, tys) ⇒
let C = (if cap = 0 then HSChannel tys
else Channel cap tys []) in
if ¬ channel_inv C
then abortv STR ''Invalid var def (channel_inv failed): ''
name (λ_. [])
else replicate size C);
cidx = (case types of
None ⇒ 0
| Some _ ⇒ integer_of_nat (length (channels g)));
v = (case siz of
None ⇒ Var VTChan cidx
| Some s ⇒ if nat_of_integer s ≤ max_array_size
then VArray VTChan (nat_of_integer s)
(IArray.tabulate (s,
λi. if cidx = 0 then 0
else i + cidx))
else abortv STR ''Invalid var def (array too large): ''
name (λ_. Var VTChan 0))
in
(name, v, chans))"

lemma toVariable_variable_inv:
assumes "gState_inv prog g"
shows "variable_inv (fst (snd (toVariable g p v)))"
using assms
apply (cases v)
apply (auto intro!: checkVarValue_Var
simp del: variable_inv.simps checkVarValue.simps varType_inv.simps
split: if_splits option.splits)
apply (auto intro!: mod_integer_ge mod_integer_le simp add: min_var_value_def)
max_channels_def max_var_value_def min_var_value_def max_array_size_def)
including integer.lifting
apply (transfer', simp)+
done

lemma toVariable_channels_inv:
shows "∀x ∈ set (snd (snd (toVariable g p v))). channel_inv x"
by (cases v) auto

lemma toVariable_channels_inv':
shows "toVariable g p v = (a,b,c) ⟹ ∀x ∈ set c. channel_inv x"
using toVariable_channels_inv
by (metis snd_conv)

lemma toVariable_variable_inv':
shows "gState_inv prog g ⟹ toVariable g p v = (a,b,c) ⟹ variable_inv b"
by (metis snd_conv fst_conv toVariable_variable_inv)

definition mkChannels
:: "'a gState_scheme ⇒ pState ⇒ channels ⇒ 'a gState_scheme * pState"
where
"mkChannels g p cs = (
if cs = [] then (g,p) else
let l = length (channels g) in
if l + length cs > max_channels
then abort STR ''Too much channels'' (λ_.  (g,p))
else let
cs⇩p = map integer_of_nat [l..<l + length cs];
g' = g⦇channels := channels g @ cs⦈;
p' = p⦇pState.channels := pState.channels p @ cs⇩p⦈
in
(g', p'))"

lemma mkChannels_gState_progress_rel:
"gState_inv prog g
⟹ set cs ⊆ Collect channel_inv
⟹ (g, fst (mkChannels g p cs)) ∈ gState_progress_rel prog"
unfolding mkChannels_def
by (intro gState_progress_relI)
(auto simp add: gState_inv_def gState.defs cl_inv_def)

lemmas mkChannels_gState_inv =
mkChannels_gState_progress_rel[THEN gState_progress_rel_gState_invI2]

lemma mkChannels_pState_inv:
"pState_inv prog p
⟹ cl_inv (g,p)
⟹ pState_inv prog (snd (mkChannels g p cs))"
unfolding mkChannels_def
including integer.lifting
apply (auto simp add: pState_inv_def pState.defs gState_inv_def dest!: cl_inv_lengthD)
apply (transfer', simp)+
done

lemma mkChannels_cl_inv:
"cl_inv (g,p) ⟹ cl_inv (mkChannels g p cs)"
unfolding mkChannels_def
by (auto simp add: pState.defs dest: cl_inv_lengthD intro!: cl_invI)

definition mkVarChannel
:: "varDecl
⇒ ((var_dict ⇒ var_dict) ⇒ 'a gState_scheme * pState
⇒ 'a gState_scheme * pState)
⇒ 'a gState_scheme ⇒ pState
⇒ 'a gState_scheme * pState"
where
"mkVarChannel v upd g p = (
let
(k,v,cs) = toVariable g p v;
(g',p') = upd (lm.update k v) (g,p)
in
mkChannels g' p' cs)"

lemma mkVarChannel_gState_inv:
assumes "gState_inv prog g"
and "⋀k v' cs. toVariable g p v = (k,v',cs)
⟹ gState_inv prog (fst (upd (lm.update k v') (g,p)))"
shows "gState_inv prog (fst (mkVarChannel v upd g p))"
using assms unfolding mkVarChannel_def
by (force split: varDecl.split prod.split
intro!: mkChannels_gState_inv
dest: toVariable_channels_inv')

lemma mkVarChannel_gState_progress_rel:
assumes "gState_inv prog g"
and "⋀k v' cs. toVariable g p v = (k,v',cs)
⟹ (g, fst (upd (lm.update k v') (g,p))) ∈ gState_progress_rel prog"
shows "(g, fst (mkVarChannel v upd g p)) ∈ gState_progress_rel prog"
proof -
obtain k v' cs where 1: "toVariable g p v = (k,v',cs)" by (metis prod.exhaust)
obtain g' p' where 2: "(g',p') = upd (lm.update k v') (g,p)" by (metis prod.exhaust)
with 1 assms have *: "(g, g') ∈ gState_progress_rel prog" by (metis fst_conv)

also from 1 2 have "(g', fst (mkChannels g' p' cs)) ∈ gState_progress_rel prog"
by (force intro!: mkChannels_gState_progress_rel gState_progress_rel_gState_invI2[OF *]
dest: toVariable_channels_inv')
finally have "(g, fst (mkChannels g' p' cs)) ∈ gState_progress_rel prog" .
thus ?thesis using 1 2 by (auto simp add: mkVarChannel_def split: prod.split)
qed

lemma mkVarChannel_pState_inv:
assumes "pState_inv prog p"
and "cl_inv (g,p)"
and "⋀k v' cs. toVariable g p v = (k,v',cs)
⟹ cl_inv (upd (lm.update k v') (g,p))"
and "⋀k v' cs. toVariable g p v = (k,v',cs)
⟹ pState_inv prog (snd (upd (lm.update k v') (g,p)))"
shows "pState_inv prog (snd (mkVarChannel v upd g p))"
using assms unfolding mkVarChannel_def
by (force split: varDecl.split prod.split
intro!: mkChannels_pState_inv)

lemma mkVarChannel_cl_inv:
assumes "cl_inv (g,p)"
and "⋀k v' cs. toVariable g p v = (k,v',cs)
⟹ cl_inv (upd (lm.update k v') (g,p))"
shows "cl_inv (mkVarChannel v upd g p)"
using assms unfolding mkVarChannel_def
by (force split: varDecl.split prod.splits
intro!: mkChannels_cl_inv)

definition mkVarChannelProc
:: "procVarDecl ⇒ 'a gState_scheme ⇒ pState ⇒ 'a gState_scheme * pState"
where
"mkVarChannelProc v g p = (
let
v' = case v of
ProcVarDeclNum lb hb name siz init ⇒
VarDeclNum lb hb name siz init
| ProcVarDeclChan name siz ⇒
VarDeclChan name siz None;
(k,v,cs) = toVariable g p v'
in
mkVarChannel v' (apsnd ∘ pState.vars_update) g p)"

lemma mkVarChannelProc_gState_progress_rel:
assumes "gState_inv prog g"
shows "(g, fst (mkVarChannelProc v g p)) ∈ gState_progress_rel prog"
unfolding mkVarChannelProc_def
using assms
by (auto intro!: mkVarChannel_gState_progress_rel)

lemmas mkVarChannelProc_gState_inv =
mkVarChannelProc_gState_progress_rel[THEN gState_progress_rel_gState_invI2]

lemma toVariable_name:
"toVariable g p (VarDeclNum lb hb name sz init) = (x,a,b) ⟹ x = name"
"toVariable g p (VarDeclChan name sz t) = (x, a, b) ⟹ x = name"
by (auto split: if_splits)

declare toVariable.simps[simp del]

lemma statesDecls_process_names:
assumes "v ∈ statesDecls (states prog !! (pState.idx p))"
shows "procVarDeclName v ∈ process_names (states prog !! (pState.idx p))
(processes prog !! (pState.idx p))"
using assms
by (cases "processes prog !! (pState.idx p)") (auto simp add: statesNames_def)

lemma mkVarChannelProc_pState_inv:
assumes "pState_inv prog p"
and "gState_inv prog g"
and "cl_inv (g, p)"
and decl: "v ∈ statesDecls (states prog !! (pState.idx p))"
shows "pState_inv prog (snd (mkVarChannelProc v g p))"
unfolding mkVarChannelProc_def
using assms statesDecls_process_names[OF decl]
by (auto intro!: mkVarChannel_pState_inv)
(auto dest: toVariable_name
split: procVarDecl.splits
intro: toVariable_variable_inv' vardict_inv_updateI

lemma mkVarChannelProc_cl_inv:
assumes "cl_inv (g,p)"
shows "cl_inv (mkVarChannelProc v g p)"
unfolding mkVarChannelProc_def using assms
by (auto intro!: mkVarChannel_cl_inv)

subsection ‹Folding›
text ‹
Fold over lists (and lists of lists) of @{typ step}/@{typ stmnt}. The folding functions are
doing a bit more than that, e.g.\ ensuring the offset into the program array is correct.
›

definition step_fold' where
"step_fold' g steps (lbls :: labels) pri pos
(nxt :: edgeIndex) (onxt :: edgeIndex option) iB =
foldr (λstep (pos, nxt, lbls, es).
let (e,enxt,lbls) = g step (lbls, pri, pos, nxt, onxt, iB)
in (pos + length e, enxt, lbls, es@e)
) steps (pos, nxt, lbls, [])"

definition step_fold where
"step_fold g steps lbls pri pos nxt onxt iB = (
let (_,nxt,lbls,s) = step_fold' g steps lbls pri pos nxt onxt iB
in (s,nxt,lbls))"

lemma step_fold'_cong:
assumes "lbls = lbls'"
and "pri = pri'"
and "pos = pos'"
and "steps = steps'"
and "nxt = nxt'"
and "onxt = onxt'"
and "iB = iB'"
and "⋀x d. x ∈ set steps ⟹ g x d = g' x d"
shows "step_fold' g steps lbls pri pos nxt onxt iB =
step_fold' g' steps' lbls' pri' pos' nxt' onxt' iB'"
unfolding step_fold'_def
by (auto intro: foldr_cong simp add: assms)

lemma step_fold_cong[fundef_cong]:
assumes "lbls = lbls'"
and "pri = pri'"
and "pos = pos'"
and "steps = steps'"
and "nxt = nxt'"
and "onxt = onxt'"
and "iB = iB'"
and "⋀x d. x ∈ set steps ⟹ g x d = g' x d"
shows "step_fold g steps lbls pri pos nxt onxt iB =
step_fold g' steps' lbls' pri' pos' nxt' onxt' iB'"
unfolding step_fold_def
by (auto simp: assms cong: step_fold'_cong)

fun step_foldL_step where
"step_foldL_step _ _ _ [] (pos, nxt, lbls, es, is) = (pos, nxt, lbls, es, is)"
| "step_foldL_step g pri onxt (s#steps) (pos, nxt, lbls, es, is) = (
let (pos', nxt', lbls', ss') = step_fold' g steps lbls pri pos nxt onxt False in
let (s', nxt'', lbls'') = g s (lbls',pri,pos',nxt',onxt,True) in
let rs = butlast s'; s'' = last s' in
(pos' + length rs, nxt, lbls'', es@ss'@rs, s''#is))"

definition step_foldL where
"step_foldL g stepss lbls pri pos nxt onxt =
foldr (step_foldL_step g pri onxt) stepss (pos,nxt,lbls,[],[])"

lemma step_foldL_step_cong:
assumes "pri = pri'"
and "onxt = onxt'"
and "s = s'"
and "d = d'"
and "⋀x d. x ∈ set s ⟹ g x d = g' x d"
shows "step_foldL_step g pri onxt s d = step_foldL_step g' pri' onxt' s' d'"
using assms
by (cases d', cases s') (simp_all cong: step_fold'_cong)

lemma step_foldL_cong[fundef_cong]:
assumes "lbls = lbls'"
and "pri = pri'"
and "pos = pos'"
and "stepss = stepss'"
and "nxt = nxt'"
and "onxt = onxt'"
and "⋀x x' d. x ∈ set stepss ⟹ x' ∈ set x ⟹ g x' d = g' x' d"
shows "step_foldL g stepss lbls pri pos nxt onxt =
step_foldL g' stepss' lbls' pri' pos' nxt' onxt'"
unfolding step_foldL_def
using assms
apply (cases stepss')
apply simp
apply (force intro!: foldr_cong step_foldL_step_cong)
done

subsection ‹Starting processes›
definition modProcArg
:: "(procArg * integer) ⇒ String.literal * variable"
where
"modProcArg x = (
case x of
(ProcArg ty name, val) ⇒ if varType_inv ty
then let init = checkVarValue ty val
in (name, Var ty init)
else abortv STR ''Invalid proc arg (varType_inv failed)''
name (λ_. (name, Var VTChan 0)))"

definition emptyProc :: "pState"
― ‹The empty process.›
where
"emptyProc = ⦇pid = 0, vars = lm.empty (), pc = 0, channels = [], idx = 0 ⦈"

lemma vardict_inv_empty:
"vardict_inv ss proc (lm.empty())"
unfolding vardict_inv_def

lemma emptyProc_cl_inv[simp]:
"cl_inv (g, emptyProc)"

lemma emptyProc_pState_inv:
assumes "program_inv prog"
shows "pState_inv prog emptyProc"
proof -
from assms have "IArray.length (states prog !! 0) > 0"
by (intro program_inv_length_states) (auto simp add: program_inv_def)
with assms show ?thesis
unfolding pState_inv_def program_inv_def emptyProc_def
qed

fun mkProc
:: "'a gState_scheme ⇒ pState
⇒ String.literal ⇒ expr list ⇒ process ⇒ nat
⇒ 'a gState_scheme * pState"
where
"mkProc g p name args (sidx, start, argDecls, decls) pidN = (
let start = case start of
Index x ⇒ x
| _ ⇒ abortv STR ''Process start is not index: '' name (λ_. 0)
in
― ‹sanity check›
if length args ≠ length argDecls
then abortv STR ''Signature mismatch: '' name (λ_. (g,emptyProc))
else
let
― ‹evaluate args (in the context of the calling process)›
eArgs = map (exprArith g p) args;

― ‹replace the init part of ‹argDecls››
argVars = map modProcArg (zip argDecls eArgs);

pidI = integer_of_nat pidN;
argVars = (STR ''_pid'', Var (VTBounded 0 pidI) pidI)#argVars;
argVars = lm.to_map argVars;

― ‹our new process›
p = ⦇ pid = pidN, vars = argVars, pc = start, channels = [], idx = sidx ⦈
in
― ‹apply the declarations›
foldl (λ(g,p) d. mkVarChannel d (apsnd ∘ pState.vars_update) g p)
(g,p)
decls)"

lemma mkProc_gState_progress_rel:
assumes "gState_inv prog g"
shows "(g, fst (mkProc g p name args (processes prog !! sidx) pidN)) ∈
gState_progress_rel prog"
proof -
obtain sidx' start argDecls decls  where
p: "processes prog !! sidx = (sidx', start, argDecls, decls)"
by (metis prod.exhaust)

from assms have
"⋀p. (g, fst (foldl (λ(g,p) d. mkVarChannel d (apsnd ∘ pState.vars_update) g p)
(g,p) decls))
∈ gState_progress_rel prog"
proof (induction decls arbitrary: g p)
case (Cons d decls)
obtain g' p' where
new: "(g',p') = (mkVarChannel d (apsnd ∘ pState.vars_update) g p)"
by (metis prod.exhaust)
hence "g' = fst ..." by (metis fst_conv)
with Cons.prems have g_g': "(g,g') ∈ gState_progress_rel prog"
by (auto intro: mkVarChannel_gState_progress_rel)
also note Cons.IH[OF g_g'[THEN gState_progress_rel_gState_invI2], of p']
finally show ?case by (auto simp add: o_def new)
qed simp
thus ?thesis using assms p by auto
qed

lemmas mkProc_gState_inv =
mkProc_gState_progress_rel[THEN gState_progress_rel_gState_invI2]

lemma mkProc_pState_inv:
assumes "program_inv prog"
and "gState_inv prog g"
and "pidN ≤ max_procs" and "pidN > 0"
and "sidx < IArray.length (processes prog)"
and "fst (processes prog !! sidx) = sidx"
shows "pState_inv prog (snd (mkProc g p name args (processes prog !! sidx) pidN))"
proof -
obtain sidx' start argDecls decls  where
"processes prog !! sidx = (sidx', start, argDecls, decls)"
by (metis prod.exhaust)
with assms have
p_def: "processes prog !! sidx = (sidx, start, argDecls, decls)"
"IArray.list_of (processes prog) ! sidx = (sidx, start, argDecls, decls)"
by simp_all
with assms have "(sidx,start,argDecls,decls) ∈ set (IArray.list_of (processes prog))"
by (force dest: nth_mem)

with assms obtain s where s: "start = Index s" "s < IArray.length (states prog !! sidx)"
unfolding program_inv_def by auto

hence P_inv: "pState_inv prog ⦇
pid = pidN,
vars = lm.to_map
((STR ''_pid'', Var (VTBounded 0 (integer_of_nat pidN))
(integer_of_nat pidN))
# map modProcArg (zip argDecls (map (exprArith g p) args))),
pc = s, channels = [], idx = sidx⦈"
unfolding pState_inv_def
using assms[unfolded program_inv_def]
including integer.lifting
apply (intro lm_to_map_vardict_inv)
apply auto
apply transfer'
apply simp
apply transfer'
apply simp
apply transfer'
apply simp
apply transfer'
apply simp
apply (drule set_zip_leftD)
split: procArg.splits if_splits
intro!: image_eqI)
split: procArg.splits if_splits
simp del: variable_inv.simps)
apply (intro checkVarValue_Var)
apply assumption
done

from p_def have
"varDeclName  set decls ⊆
process_names (states prog !! sidx) (processes prog !! sidx)"
by auto
with ‹gState_inv prog g› have
F_inv: "⋀p. ⟦ pState_inv prog p; sidx = pState.idx p; cl_inv (g,p) ⟧
⟹ pState_inv prog
(snd (foldl (λ(g,p) d. mkVarChannel d (apsnd ∘ pState.vars_update) g p)
(g,p) decls))"
proof (induction decls arbitrary: g p)
case (Cons d ds) hence
decl: "varDeclName d ∈ process_names (states prog !! pState.idx p)
(processes prog !! pState.idx p)"
by simp

obtain g' p' where
new: "(g',p') = (mkVarChannel d (apsnd ∘ pState.vars_update) g p)"
by (metis prod.exhaust)
hence p': "p' = snd ..." and g': "g' = fst ..."
by (metis snd_conv fst_conv)+
with Cons.prems have "pState_inv prog p'"
apply (auto intro!: mkVarChannel_pState_inv)
apply (intro vardict_inv_updateI)
apply simp
apply (cases d)
apply (force dest!: toVariable_name)
apply (force dest!: toVariable_name)
apply (intro toVariable_variable_inv')
apply assumption+
done
moreover
from p' Cons.prems have "pState.idx p' = sidx"
by (auto simp add: mkVarChannel_def mkChannels_def split: prod.split)
moreover
from new Cons.prems have "cl_inv (g',p')"
by (auto intro!: mkVarChannel_cl_inv)
moreover
from g' Cons.prems have "gState_inv prog g'"
by (auto intro!: mkVarChannel_gState_inv)
moreover
from Cons.prems have
"varDeclName  set ds ⊆
process_names (states prog !! sidx) (processes prog !! sidx)"
by simp
ultimately
have
"pState_inv prog
(snd (foldl (λ(g,p) d. mkVarChannel d (apsnd ∘ pState.vars_update) g p)
(g',p') ds))"
using Cons.IH[of p' g'] by (simp add: o_def)
with new show ?case by (simp add: o_def)
qed simp

show ?thesis
by (auto simp add: p_def s cl_inv_def
intro: F_inv[OF P_inv])
(blast intro: emptyProc_pState_inv assms)
qed

lemma mkProc_cl_inv:
assumes "cl_inv (g,p)"
shows "cl_inv (mkProc g p name args (processes prog !! sidx) pidN)"
proof -
note IArray.sub_def [simp del]
obtain sidx' start argDecls decls
where [simp]: "processes prog !! sidx = (sidx', start, argDecls, decls)"
by (metis prod.exhaust)

have
P_inv: "⋀s v. cl_inv (g, ⦇pid = pidN, vars = v, pc = s, channels = [], idx = sidx' ⦈)"

have
"⋀p. cl_inv(g,p) ⟹
cl_inv (foldl (λ(g,p) d. mkVarChannel d (apsnd ∘ pState.vars_update) g p)
(g,p) decls)"
proof (induction decls arbitrary: g p)
case (Cons d ds)
obtain g' p' where
new: "(g',p') = (mkVarChannel d (apsnd ∘ pState.vars_update) g p)"
by (metis prod.exhaust)
with Cons.prems have "cl_inv (g',p')"
by (auto intro!: mkVarChannel_cl_inv)

from Cons.IH[OF this] new show ?case by (simp add: o_def)
qed simp

from this[OF P_inv] show ?thesis by auto
qed

declare mkProc.simps[simp del]

definition runProc
:: "String.literal ⇒ expr list ⇒ program
⇒ 'a gState_scheme ⇒ pState
⇒ 'a gState_scheme * pState"
where
"runProc name args prog g p = (
if length (procs g) ≥ max_procs
then abort STR ''Too many processes'' (λ_. (g,p))
else let pid = length (procs g) + 1 in
case lm.lookup name (proc_data prog) of
None ⇒ abortv STR ''No such process: '' name
(λ_. (g,p))
| Some proc_idx ⇒
let (g', proc) = mkProc g p name args (processes prog !! proc_idx) pid
in (g'⦇procs := procs g @ [proc]⦈, p))"

lemma runProc_gState_progress_rel:
assumes "program_inv prog"
and "gState_inv prog g"
and "pState_inv prog p"
and "cl_inv (g,p)"
shows "(g, fst (runProc name args prog g p)) ∈ gState_progress_rel prog"
proof (cases "length (procs g) < max_procs")
note IArray.sub_def [simp del]

case True thus ?thesis
proof (cases "lm.lookup name (proc_data prog)")
case (Some proc_idx)
hence *: "proc_idx < IArray.length (processes prog)"
"fst (processes prog !! proc_idx) = proc_idx"
using assms

obtain g' p' where
new: "(g',p') = mkProc g p name args (processes prog !! proc_idx) (length (procs g) + 1)"
by (metis prod.exhaust)
hence g': "g' = fst ..." and p': "p' = snd ..."
by (metis snd_conv fst_conv)+
from assms g' have "(g, g') ∈ gState_progress_rel prog "
by (auto intro!: mkProc_gState_progress_rel)

moreover
from * assms True p' have "pState_inv prog p'"
by (auto intro!: mkProc_pState_inv)
moreover
from assms new have "cl_inv (g',p')"
by (auto intro!: mkProc_cl_inv)
ultimately show ?thesis
using True Some new assms
unfolding runProc_def gState_progress_rel_def
by (clarsimp split: prod.split)
next
case None with assms show ?thesis by (auto simp add: runProc_def)
qed
next
case False with assms show ?thesis by (auto simp add: runProc_def)
qed

lemmas runProc_gState_inv =
runProc_gState_progress_rel[THEN gState_progress_rel_gState_invI2]

lemma runProc_pState_id:
"snd (runProc name args prog g p) = p"
unfolding runProc_def
by (auto split: if_splits split: option.split prod.split)

lemma runProc_pState_inv:
assumes "pState_inv prog p"
shows "pState_inv prog (snd (runProc name args prog g p))"

lemma runProc_cl_inv:
assumes "program_inv prog"
and "gState_inv prog g"
and "pState_inv prog p"
and "cl_inv (g,p)"
shows "cl_inv (runProc name args prog g p)"
proof -
obtain g' p' where *: "runProc name args prog g p = (g',p')"
by (metis prod.exhaust)
with runProc_gState_progress_rel[OF assms, of name args] have
"length (channels g) ≤ length (channels g')"
moreover from * runProc_pState_id have "p' = p" by (metis snd_conv)
ultimately show ?thesis by (metis ‹cl_inv (g,p)› * cl_inv_trans)
qed

subsection ‹AST to edges›

type_synonym ast = "AST.module list"

text ‹In this section, the AST is translated into the transition system.›

text ‹
Handling atomic blocks is non-trivial. Therefore, we do this in an extra pass:
@{term lp} and @{term hp} are the positions of the start and the end of
the atomic block. Every edge pointing into this range is therefore marked as
@{term Atomic}. If they are pointing somewhere else, they are set to @{term InAtomic},
meaning: they start \emph{in} an atomic block, but leave it afterwards.
›
definition atomize :: "nat ⇒ nat ⇒ edge list ⇒ edge list" where
"atomize lp hp es = fold (λe es.
let e' = case target e of
LabelJump _ None ⇒
― ‹Labels are checked again later on, when they›
― ‹are going to be resolved. Hence it is safe to say›
― ‹‹atomic› here, especially as the later algorithm›
― ‹relies on targets in atomic blocks to be marked as such.›
e⦇ atomic := InAtomic ⦈
| LabelJump _ (Some via) ⇒
if lp ≤ via ∧ hp ≥ via then e⦇ atomic := Atomic ⦈
else e⦇ atomic := InAtomic ⦈
| Index p' ⇒
if lp ≤ p' ∧ hp ≥ p' then e⦇ atomic := Atomic ⦈
else e⦇ atomic := InAtomic ⦈
in e'#es) es []"

fun skip ― ‹No-(edge)›
where
"skip (lbls, pri, pos, nxt, _) =
([[⦇cond = ECExpr (ExprConst 1),
effect = EEId, target = nxt, prio = pri,
atomic = NonAtomic⦈]], Index pos, lbls)"

text ‹
The AST is walked backwards. This allows to know the next state directly.

Parameters used:
\begin{description}
\item[lbls] Map of Labels
\item[pri] Current priority
\item[pos] Current position in the array
\item[nxt] Next state
\item[onxt] Previous 'next state' (where to jump after a 'do')
\item[inBlock] Needed for certain constructs to calculate the layout of the array
\end{description}
›

fun stepToState
:: "step
⇒ (labels * integer * nat * edgeIndex * edgeIndex option * bool)
⇒ edge list list * edgeIndex * labels"
and stmntToState
:: "stmnt
⇒ (labels * integer * nat * edgeIndex * edgeIndex option * bool)
⇒ edge list list * edgeIndex * labels"
where
"stepToState (StepStmnt s None) data = stmntToState s data"
| "stepToState (StepStmnt s (Some u)) (lbls, pri, pos, nxt, onxt, _) = (
let
― ‹the ‹unless› part›
(ues,_,lbls') = stmntToState u (lbls, pri, pos, nxt, onxt, True);
u = last ues; ues = butlast ues;
pos' = pos + length ues;

― ‹find minimal current priority›
pri = min_prio u pri;

― ‹the guarded part --›
― ‹priority is decreased, because there is now a new unless part with›
― ‹higher prio›
(ses,spos,lbls'') = stmntToState s (lbls', pri - 1, pos', nxt, onxt, False);

― ‹add an edge to the unless part for each generated state›
ses = map (List.append u) ses
in
(ues@ses,spos,lbls''))"

| "stepToState (StepDecl decls) (lbls, pri, pos, nxt, onxt, _) = (
let edgeF = λd (lbls,pri,pos,nxt,_).
([[⦇cond = ECTrue, effect = EEDecl d, target = nxt,
prio = pri, atomic = NonAtomic⦈]], Index pos, lbls)
in
step_fold edgeF decls lbls pri pos nxt onxt False)"

| "stepToState StepSkip (lbls,_,_,nxt,_) = ([],nxt,lbls)"

| "stmntToState (StmntAtomic steps) (lbls, pri, pos, nxt, onxt, inBlock) = (
let (es,pos',lbls') = step_fold stepToState steps lbls pri pos nxt onxt inBlock in
let es' = map (atomize pos (pos + length es)) es in
(es', pos', lbls'))"

| "stmntToState (StmntLabeled l s) (lbls, pri, pos, d) = (
let
(es, pos', lbls) = stmntToState s (lbls, pri, pos, d);

― ‹We don't resolve goto-chains. If the labeled stmnt returns only a jump,›
― ‹use this goto state.›
lpos = case pos' of Index p ⇒ p | _ ⇒ pos;
lbls' = add_label l lbls lpos
in
(es, pos', lbls'))"

| "stmntToState (StmntDo stepss) (lbls, pri, pos, nxt, onxt, inBlock) = (
let
― ‹construct the different branches›
― ‹‹nxt› in those branches points current pos (it is a loop after all)›
― ‹‹onxt› then is the current ‹nxt› (needed for break, f.ex.)›
(_,_,lbls,es,is) = step_foldL stepToState stepss lbls pri
(pos+1) (Index pos) (Some nxt);

― ‹put the branch starting points (‹is›) into the array›
es' = concat is # es
in
if inBlock then
― ‹inside another DO or IF or UNLESS›
― ‹‹⟶› append branches again, so they can be consumed›
(es' @ [concat is], Index pos, lbls)
else
(es', Index pos, lbls)
)"

| "stmntToState (StmntIf stepss) (lbls, pri, pos, nxt, onxt, _) = (
let (pos,_,lbls,es,is) = step_foldL stepToState stepss lbls pri pos nxt onxt
in (es @ [concat is], Index pos, lbls))"

| "stmntToState (StmntSeq steps) (lbls, pri, pos, nxt, onxt, inBlock) =
step_fold stepToState steps lbls pri pos nxt onxt inBlock"

| "stmntToState (StmntAssign v e) (lbls, pri, pos, nxt, _) =
([[⦇cond = ECTrue, effect = EEAssign v e, target = nxt, prio = pri,
atomic = NonAtomic⦈]], Index pos, lbls)"

| "stmntToState (StmntAssert e) (lbls, pri, pos, nxt, _) =
([[⦇cond = ECTrue, effect = EEAssert e, target = nxt, prio = pri,
atomic = NonAtomic⦈]], Index pos, lbls)"

| "stmntToState (StmntCond e) (lbls, pri, pos, nxt, _) =
([[⦇cond = ECExpr e, effect = EEId, target = nxt, prio = pri,
atomic = NonAtomic⦈]], Index pos, lbls)"

| "stmntToState StmntElse (lbls, pri, pos, nxt, _) =
([[⦇cond = ECElse, effect = EEId, target = nxt, prio = pri,
atomic = NonAtomic ⦈]], Index pos, lbls)"

| "stmntToState StmntBreak (lbls,pri,_,_,Some onxt,_) =
([[⦇cond = ECTrue, effect = EEGoto, target = onxt, prio = pri,
atomic = NonAtomic ⦈]], onxt, lbls)"
| "stmntToState StmntBreak (_,_,_,_,None,_) =
abort STR ''Misplaced break'' (λ_. ([],Index 0,lm.empty()))"

| "stmntToState (StmntRun n args) (lbls, pri, pos, nxt, onxt, _) =
([[⦇cond = ECRun n, effect = EERun n args, target = nxt, prio = pri,
atomic = NonAtomic ⦈]], Index pos,lbls)"

| "stmntToState (StmntGoTo l) (lbls, pri, pos, _) =
([[⦇cond = ECTrue, effect = EEGoto, target = LabelJump l None, prio = pri,
atomic = NonAtomic ⦈]], LabelJump l (Some pos), lbls)"

| "stmntToState (StmntSend v e srt) (lbls, pri, pos, nxt, _) =
([[⦇cond = ECSend v, effect = EESend v e srt, target = nxt, prio = pri,
atomic = NonAtomic ⦈]], Index pos, lbls)"

| "stmntToState (StmntRecv v r srt rem) (lbls, pri, pos, nxt, _) =
([[⦇cond = ECRecv v r srt, effect = EERecv v r srt rem, target = nxt, prio = pri,
atomic = NonAtomic ⦈]], Index pos, lbls)"

| "stmntToState StmntSkip d = skip d"

subsubsection ‹Setup›
definition endState :: "edge list" where
― ‹An extra state added to each process marking its end.›
"endState = [⦇ cond = ECFalse, effect = EEEnd, target = Index 0, prio = 0,
atomic = NonAtomic⦈]"

definition resolveLabel :: "String.literal ⇒ labels ⇒ nat" where
"resolveLabel l lbls = (
case lm.lookup l lbls of
None ⇒ abortv STR ''Unresolved label: '' l (λ_. 0)
| Some pos ⇒ pos)"

primrec resolveLabels :: "edge list list ⇒ labels ⇒ edge list ⇒ edge list" where
"resolveLabels _ _ [] = []"
| "resolveLabels edges lbls (e#es) = (
let check_atomic = λpos. fold (λe a. a ∧ inAtomic e) (edges ! pos) True in
case target e of
Index _ ⇒ e
| LabelJump l None ⇒
let pos = resolveLabel l lbls in
e⦇target := Index pos,
atomic := if inAtomic e then
if check_atomic pos then Atomic
else InAtomic
else NonAtomic ⦈
| LabelJump l (Some via) ⇒
let pos = resolveLabel l lbls in
e⦇target := Index pos,
― ‹NB: ‹isAtomic› instead of ‹inAtomic›, cf ‹atomize()››
atomic := if isAtomic e then
if check_atomic pos ∧ check_atomic via then Atomic
else InAtomic
else atomic e ⦈
) # (resolveLabels edges lbls es)"

definition calculatePrios :: "edge list list ⇒ (integer * edge list) list" where
"calculatePrios ess = map (λes. (min_prio es 0, es)) ess"

definition toStates :: "step list ⇒ states * edgeIndex * labels" where
"toStates steps = (
let
(states,pos,lbls) = step_fold stepToState steps (lm.empty())
0 1 (Index 0) None False;
pos = (case pos of
Index _ ⇒ pos
| LabelJump l _ ⇒ Index (resolveLabel l lbls));
states = endState # states;
states = map (resolveLabels states lbls) states;
states = calculatePrios states
in
case pos of Index s ⇒
if s < length states then (IArray states, pos, lbls)
else abort STR ''Start index out of bounds'' (λ_. (IArray states, Index 0, lbls)))"

lemma toStates_inv:
assumes "toStates steps = (ss,start,lbls)"
shows "∃s. start = Index s ∧ s < IArray.length ss"
and "IArray.length ss > 0"
using assms
unfolding toStates_def calculatePrios_def
by (auto split: prod.splits edgeIndex.splits if_splits)

(* returns: states * is_active * name * labels * process *)
primrec toProcess
:: "nat ⇒ proc ⇒ states * nat * String.literal * (labels * process)"
where
"toProcess sidx (ProcType act name args decls steps) = (
let
(states, start, lbls) = toStates steps;
act = (case act of
None ⇒ 0
| Some None ⇒ 1
| Some (Some x) ⇒ nat_of_integer x)
in
(states, act, name, lbls, sidx, start, args, decls))"
| "toProcess sidx (Init decls steps) = (
let (states, start, lbls) = toStates steps in
(states, 1, STR '':init:'', lbls, sidx, start, [], decls))"

lemma toProcess_sidx:
"toProcess sidx p = (ss,a,n,l,idx,r) ⟹ idx = sidx"
by (cases p) (simp_all split: prod.splits)

lemma toProcess_states_nonempty:
"toProcess sidx p = (ss,a,n,l,idx,r) ⟹ IArray.length ss > 0"
by (cases p) (force split: prod.splits dest: toStates_inv(2))+

lemma toProcess_start:
"toProcess sidx p = (ss,a,n,l,idx,start,r)
⟹ ∃s. start = Index s ∧ s < IArray.length ss"
by (cases p) (force split: prod.splits dest: toStates_inv(1))+

lemma toProcess_startE:
assumes "toProcess sidx p = (ss,a,n,l,idx,start,r)"
obtains s where "start = Index s" "s < IArray.length ss"
using toProcess_start[OF assms]
by blast

text ‹
The main construction function. Takes an AST
and returns  an initial state,
and the program (= transition system).
›

definition setUp :: "ast ⇒ program × gState" where
"setUp ast = (
let
(decls, procs, _) = preprocess ast;
assertVar = Var (VTBounded 0 1) 0;

pre_procs = map (case_prod toProcess) (List.enumerate 1 procs);

procs = IArray ((0, Index 0, [], []) # map (λ(_,_,_,_,p). p) pre_procs);
labels = IArray (lm.empty() # map (λ(_,_,_,l,_). l) pre_procs);
states = IArray (IArray [(0,[])] # map (λ(s,_). s) pre_procs);
names = IArray (STR ''invalid'' # map (λ(_,_,n,_). n) pre_procs);

proc_data = lm.to_map (map (λ(_,_,n,_,idx,_). (n,idx)) pre_procs);

prog = ⦇ processes = procs, labels = labels, states = states,
proc_names = names, proc_data = proc_data ⦈;

g = ⦇ vars = lm.sng (STR ''__assert__'') assertVar,
channels = [InvChannel], timeout = False, procs = [] ⦈;
g' = foldl (λg d.
fst (mkVarChannel d (apfst ∘ gState.vars_update) g emptyProc)
) g decls;
g'' = foldl (λg (_,a,name,_).
foldl (λg name.
fst (runProc name [] prog g emptyProc)
) g (replicate a name)
) g' pre_procs
in
(prog, g''))"

lemma setUp_program_inv':
"program_inv (fst (setUp ast))"
proof (rule program_invI, goal_cases)
case 1 show ?case by (simp add: setUp_def split: prod.split)
next
case 2 show ?case by (simp add: setUp_def split: prod.split)
next
case 3 thus ?case
by (auto simp add: setUp_def o_def
split: prod.splits
dest!: toProcess_states_nonempty)
next
case 4 thus ?case
unfolding setUp_def
by (auto simp add: lm.correct o_def in_set_enumerate_eq nth_enumerate_eq
dest!: subsetD[OF Misc.ran_map_of] toProcess_sidx
split: prod.splits)
(* TODO: Change name Misc.ran_map_of ⟶ ran_map_of_ss, as it collides
with AList.ran_map_of *)
next
case 5 thus ?case
apply (auto simp add: setUp_def o_def split: prod.splits)
apply (frule toProcess_sidx)
apply (frule toProcess_start)
apply (auto simp: in_set_enumerate_eq nth_enumerate_eq)
done
qed

lemma setUp_program_inv:
assumes "setUp ast = (prog,g)"
shows "program_inv prog"
using assms setUp_program_inv'
by (metis fst_conv)

lemma setUp_gState_inv:
assumes "setUp ast = (prog, g)"
shows "gState_inv prog g"
proof -
from assms have p_INV: "program_inv prog" by (fact setUp_program_inv)

{
fix prog :: program
assume *: "program_inv prog"
let ?g = "⦇ vars = lm.sng (STR ''__assert__'') (Var (VTBounded 0 1) 0),
channels = [InvChannel], timeout = False, procs = [] ⦈"

have g1: "gState_inv prog ?g"
by (simp add: gState_inv_def max_channels_def lm_correct max_var_value_def)
{
fix g decls
assume "gState_inv prog g"
hence "gState_inv prog (foldl (λg d.
fst (mkVarChannel d (apfst ∘ gState.vars_update) g emptyProc)
) g decls)"
apply (rule foldl_rule)
apply (intro mkVarChannel_gState_inv)
apply simp
apply (frule_tac g=σ in toVariable_variable_inv')
apply assumption
apply (auto simp add: gState_inv_def lm.correct)
done
}
note g2 = this[OF g1]

{
fix g :: "'a gState_scheme" and pre_procs
assume "gState_inv prog g"
hence "gState_inv prog (foldl (λg (_,a,name,_).
foldl (λg name.
fst (runProc name [] prog g emptyProc)
) g (replicate a name)
) g pre_procs)"
apply (rule foldl_rule)
apply (clarsimp split: prod.splits)
apply (rule foldl_rule)
apply (auto intro!: runProc_gState_inv emptyProc_pState_inv *)
done
}
note this[OF g2]
} note g_INV = this

from assms p_INV show ?thesis
unfolding setUp_def
by (auto split: prod.splits intro!: g_INV)
qed

subsection ‹Semantic Engine›

text ‹
After constructing the transition system, we are missing the final part:
The successor function on this system. We use SPIN-nomenclature and call it
\emph{semantic engine}.
›

definition "assertVar ≡ VarRef True (STR ''__assert__'') None"

subsubsection ‹Evaluation of Edges›

fun evalRecvArgs
:: "recvArg list ⇒ integer list ⇒ gState⇩I ⇒ pState ⇒ gState⇩I * pState"
where
"evalRecvArgs [] [] g l = (g,l)"
| "evalRecvArgs _  [] g l =
abort STR ''Length mismatch on receiving.'' (λ_. (g,l))"
| "evalRecvArgs []  _ g l =
abort STR ''Length mismatch on receiving.'' (λ_. (g,l))"
| "evalRecvArgs (r#rs) (v#vs) g l = (
let (g,l) =
case r of
RecvArgVar var ⇒ setVar var v g l
| _ ⇒ (g,l)
in evalRecvArgs rs vs g l)"

primrec evalCond
:: "edgeCond ⇒ gState⇩I ⇒ pState ⇒ bool"
where
"evalCond ECTrue _ _ ⟷ True"
| "evalCond ECFalse _ _ ⟷ False"
| "evalCond (ECExpr e) g l ⟷ exprArith g l e ≠ 0"
| "evalCond (ECRun _) g l ⟷ length (procs g) < 255"
| "evalCond ECElse g l ⟷ gState⇩I.else g"
| "evalCond (ECSend v) g l ⟷
withChannel v (λ_ c.
case c of
Channel cap _ q ⇒ integer_of_nat (length q) < cap
| HSChannel _ ⇒ True) g l"
| "evalCond (ECRecv v rs srt) g l ⟷
withChannel v (λi c.
case c of
HSChannel _ ⇒ handshake g ≠ 0 ∧ recvArgsCheck g l rs (hsdata g)
| _ ⇒ pollCheck g l c rs srt) g l"

fun evalHandshake
:: "edgeCond ⇒ nat ⇒  gState⇩I ⇒ pState ⇒ bool"
where
"evalHandshake (ECRecv v _ _) h g l
⟷ h = 0
∨ withChannel v (λi c. case c of
HSChannel _ ⇒ i = h
| Channel _ _ _ ⇒ False) g l"
| "evalHandshake _ h _ _ ⟷ h = 0"

primrec evalEffect
:: "edgeEffect ⇒ program ⇒ gState⇩I ⇒ pState ⇒ gState⇩I * pState"
where
"evalEffect EEEnd _ g l = (g,l)"
| "evalEffect EEId _ g l = (g,l)"
| "evalEffect EEGoto _ g l = (g,l)"
| "evalEffect (EEAssign v e) _ g l = setVar v (exprArith g l e) g l"
| "evalEffect (EEDecl d) _ g l = mkVarChannelProc d g l"
| "evalEffect (EERun name args) prog g l = runProc name args prog g l"
| "evalEffect (EEAssert e) _ g l = (
if exprArith g l e = 0
then setVar assertVar 1 g l
else (g,l))"
| "evalEffect (EESend v es srt) _ g l = withChannel v (λi c.
let
ab = λ_. abort STR ''Length mismatch on sending.'' (λ_. (g,l));
es = map (exprArith g l) es
in
if ¬ for_all (λx. x ≥ min_var_value ∧ x ≤ max_var_value) es
then abort STR ''Invalid Channel'' (λ_. (g,l))
else
case c of
Channel cap ts q ⇒
if length ts ≠ length es ∨ ¬ (length q < max_array_size)
then ab()
else let
q' = if ¬ srt then q@[es]
else let
q = map lexlist q;
q' = insort (lexlist es) q
in map unlex q';
g = gState.channels_update (λcs.
cs[ i := Channel cap ts q' ]) g
in (g,l)
| HSChannel ts ⇒
if length ts ≠ length es then ab()
else (g⦇hsdata := es, handshake := i⦈, l)
| InvChannel ⇒ abort STR ''Trying to send on invalid channel'' (λ_. (g,l))
) g l"
| "evalEffect (EERecv v rs srt rem) _ g l = withChannel v (λi c.
case c of
Channel cap ts qs ⇒
if qs = [] then abort STR ''Recv from empty channel'' (λ_. (g,l))
else
let
(q', qs') = if ¬ srt then (hd qs, tl qs)
else apfst the (find_remove (recvArgsCheck g l rs) qs);
(g,l) = evalRecvArgs rs q' g l;
g = if rem
then gState.channels_update (λcs. cs[ i := Channel cap ts qs']) g
else g
― ‹messages are not removed -- so no need to update anything›
in (g,l)
| HSChannel _ ⇒
let (g,l) = evalRecvArgs rs (hsdata g) g l in
let g = g⦇ handshake := 0, hsdata := [] ⦈
in (g,l)
| InvChannel ⇒ abort STR ''Receiving on invalid channel'' (λ_. (g,l))
) g l"

lemma statesDecls_effect:
assumes "ef ∈ effect  edgeSet ss"
and "ef = EEDecl d"
shows "d ∈ statesDecls ss"
proof -
from assms obtain e where "e ∈ edgeSet ss" "ef = effect e" by auto
thus ?thesis  using assms
unfolding statesDecls_def
intro!: bexI[where x = e]
split: edgeEffect.split)
qed

lemma evalRecvArgs_pState_inv:
assumes "pState_inv prog p"
shows "pState_inv prog (snd (evalRecvArgs rargs xs g p))"
using assms
proof (induction rargs xs arbitrary: p g rule: list_induct2')
case (4 r rs x xs) thus ?case
proof (cases r)
case (RecvArgVar v)
obtain g' p' where  new: "setVar v x g p = (g',p')" by (metis prod.exhaust)
hence "p' = snd (setVar v x g p)" by simp
with "4" have "pState_inv prog p'" by (auto intro!: setVar_pState_inv)
from "4.IH"[OF this] RecvArgVar new show ?thesis by simp
qed simp_all
qed simp_all

lemma evalRecvArgs_pState_inv':
assumes "evalRecvArgs rargs xs g p = (g', p')"
and "pState_inv prog p"
shows "pState_inv prog p'"
using assms evalRecvArgs_pState_inv
by (metis snd_conv)

lemma evalRecvArgs_gState_progress_rel:
assumes "gState_inv prog g"
shows "(g, fst (evalRecvArgs rargs xs g p)) ∈ gState_progress_rel prog"
using assms
proof (induction rargs xs arbitrary: p g rule: list_induct2')
case (4 r rs x xs) thus ?case
proof (cases r)
case (RecvArgVar v)
obtain g' p' where new: "setVar v x g p = (g',p')" by (metis prod.exhaust)
hence "g' = fst (setVar v x g p)" by simp
with "4" have "(g, g') ∈ gState_progress_rel prog"
by (auto intro!: setVar_gState_progress_rel)
also hence "gState_inv prog g'"
by (rule gState_progress_rel_gState_invI2)
note "4.IH"[OF this, of p']
finally show ?thesis using RecvArgVar new by simp
qed simp_all
qed simp_all

lemmas evalRecvArgs_gState_inv =
evalRecvArgs_gState_progress_rel[THEN gState_progress_rel_gState_invI2]

lemma evalRecvArgs_cl_inv:
assumes "cl_inv (g,p)"
shows "cl_inv (evalRecvArgs rargs xs g p)"
using assms
proof (induction rargs xs arbitrary: p g rule: list_induct2')
case (4 r rs x xs) thus ?case
proof (cases r)
case (RecvArgVar v)
with 4 have "cl_inv (setVar v x g p)"
by (auto intro!: setVar_cl_inv)
with "4.IH" RecvArgVar show ?thesis
by (auto split: prod.splits)
qed simp_all
qed simp_all

lemma evalEffect_pState_inv:
assumes "pState_inv prog p"
and "gState_inv prog g"
and "cl_inv (g,p)"
and "e ∈ effect  edgeSet (states prog !! pState.idx p)"
shows "pState_inv prog (snd (evalEffect e prog g p))"
using assms
proof (cases e)
case (EEDecl d)
with assms have "d ∈ statesDecls (states prog !! pState.idx p)"
using statesDecls_effect
by simp
with assms EEDecl show ?thesis
by (auto simp del: IArray.sub_def
intro!: mkVarChannelProc_pState_inv)
next
case (EESend c es srt)
then obtain v where "ChanRef v = c" by (cases c) simp
with EESend assms show ?thesis
by (cases v) (auto simp add: withChannel'_def withVar'_def split: channel.split)
next
case (EERecv c es srt)
then obtain v where "ChanRef v = c" by (cases c) simp
with EERecv assms show ?thesis
by (cases v)
(auto simp: withChannel'_def withVar'_def
split: prod.splits channel.split
dest: evalRecvArgs_pState_inv')
qed (clarsimp_all intro!: setVar_pState_inv runProc_pState_inv)

lemma evalEffect_gState_progress_rel:
assumes "program_inv prog"
and "gState_inv prog g"
and "pState_inv prog p"
and "cl_inv (g,p)"
shows "(g, fst (evalEffect e prog g p)) ∈ gState_progress_rel prog"
using assms
proof (cases e)
case EEAssert
with assms show ?thesis
by (auto intro: setVar_gState_progress_rel)
next
case EEAssign
with assms show ?thesis
by (auto intro: setVar_gState_progress_rel)
next
case EEDecl
with assms show ?thesis
by (auto intro: mkVarChannelProc_gState_progress_rel)
next
case EERun
with assms show ?thesis
by (auto intro: runProc_gState_progress_rel)
next
case (EESend c es srt)
then obtain v where v: "c = ChanRef v" by (metis chanRef.exhaust)
obtain idx where idx: "nat_of_integer (the (getVar v g p)) = idx" by blast
note idx' = idx[symmetric, unfolded getVar_def]
show ?thesis
proof (cases "idx < length (gState.channels g)")
case True
note DEF = True EESend v idx' assms

show ?thesis
proof (cases "gState.channels g ! idx")
case (Channel cap ts q)
with True have "Channel cap ts q ∈ set (gState.channels g)"
by (metis nth_mem)
with assms have "channel_inv (Channel cap ts q)"
by (auto simp add: gState_inv_def simp del: channel_inv.simps)
with Channel DEF show ?thesis
by (cases v)
(auto simp add: withChannel'_def withVar'_def for_all_def
split: channel.split
intro!: gState_progress_rel_channels_update)
next
case HSChannel with DEF show ?thesis
by (cases v)
(auto simp: withChannel'_def withVar'_def gState_progress_rel_def
gState_inv_def
split: channel.split)
next
case InvChannel with DEF show ?thesis
by (cases v) (auto simp add: withChannel'_def withVar'_def)
qed
next
case False with EESend idx' v assms show ?thesis
by (cases v) (auto simp add: withChannel'_def withVar'_def)
qed
next
case (EERecv c rs srt rem)
then obtain v where v: "c = ChanRef v" by (metis chanRef.exhaust)
obtain idx where idx: "nat_of_integer (the (getVar v g p)) = idx" by blast
note idx' = idx[symmetric, unfolded getVar_def]
show ?thesis
proof (cases "idx < length (gState.channels g)")
case True
note DEF = True EERecv v idx' assms
show ?thesis
proof (cases "gState.channels g ! idx")
note channel_inv.simps[simp del]
case (Channel cap ts q)
with True have "Channel cap ts q ∈ set (gState.channels g)"
by (metis nth_mem)
with assms have c_inv: "channel_inv (Channel cap ts q)"
by (auto simp add: gState_inv_def simp del: channel_inv.simps)
moreover obtain res q' where
"apfst the (find_remove (recvArgsCheck g p rs) q) = (res, q')"
by (metis prod.exhaust)
moreover hence "q' = snd (find_remove (recvArgsCheck g p rs) q)"
by (simp add: apfst_def map_prod_def split: prod.splits)
with find_remove_subset find_remove_length have
"set q' ⊆ set q" "length q' ≤ length q"
by (metis surjective_pairing)+
with c_inv have "channel_inv (Channel cap ts q')"
moreover {
assume "q ≠ []"
hence "set (tl q) ⊆ set q" using tl_subset by auto
with c_inv have "channel_inv (Channel cap ts (tl q))"
}
moreover {
fix res g' p'
assume "evalRecvArgs rs res g p = (g',p')"
with evalRecvArgs_gState_progress_rel assms have
"(g,g') ∈ gState_progress_rel prog"
by (metis fst_conv)
hence "length (channels g) ≤ length (channels g')"
}
ultimately show ?thesis using Channel DEF
apply (cases v)
apply (auto simp add: withChannel'_def withVar'_def for_all_def
split: channel.split prod.split
elim: fstE
intro!: evalRecvArgs_gState_progress_rel
gState_progress_rel_channels_update_step)
apply force+
done
next
case HSChannel
obtain g' p' where *: "evalRecvArgs rs (hsdata g) g p = (g',p')"
by (metis prod.exhaust)
with assms have "(g,g') ∈ gState_progress_rel prog"
by (auto elim!: fstE intro!: evalRecvArgs_gState_progress_rel)
also hence "gState_inv prog g'" by blast
hence "(g',g'⦇handshake := 0, hsdata := []⦈) ∈ gState_progress_rel prog"
by (auto simp add: gState_progress_rel_def gState_inv_def)
finally
have "(g,g'⦇handshake := 0, hsdata := []⦈) ∈ gState_progress_rel prog" .
with DEF HSChannel * show ?thesis
by (cases v) (auto simp add: withChannel'_def withVar'_def for_all_def
split: channel.split prod.split)
next
case InvChannel with DEF show ?thesis
by (cases v) (auto simp add: withChannel'_def withVar'_def)
qed
next
case False with EERecv idx' v assms show ?thesis
by (cases v) (auto simp add: withChannel'_def withVar'_def)
qed
qed simp_all

lemma evalEffect_cl_inv:
assumes "cl_inv (g,p)"
and "program_inv prog"
and "gState_inv prog g"
and "pState_inv prog p"
shows "cl_inv  (evalEffect e prog g p)"
using assms
proof (cases e)
case EERun with assms show ?thesis by (force intro!: runProc_cl_inv)
next
case (EESend c es srt) then obtain v where "ChanRef v = c" by (cases c) simp
with EESend assms show ?thesis
by (cases v)
(auto simp add: withChannel'_def withVar'_def split: channel.split
intro!: cl_inv_channels_update)
next
case (EERecv c es srt) then obtain v where "ChanRef v = c" by (cases c) simp
with EERecv assms show ?thesis
apply (cases v)
apply (auto simp add: withChannel'_def withVar'_def split: channel.split prod.split
intro!: cl_inv_channels_update)
apply (metis evalRecvArgs_cl_inv)+
done

subsubsection ‹Executable edges›

text ‹
To find a successor global state, we first need to find all those edges which are executable
(\ie the condition evaluates to true).
›
type_synonym choices = "(edge * pState) list"
― ‹A choice is an executable edge and the process it belongs to.›

definition getChoices :: "gState⇩I ⇒ pState ⇒ edge list ⇒ choices" where
"getChoices g p = foldl (λE e.
if evalHandshake (cond e) (handshake g) g p ∧ evalCond (cond e) g p
then (e,p)#E
else E) []"

lemma getChoices_sub_edges_fst:
"fst  set (getChoices g p es) ⊆ set es"
unfolding getChoices_def
by (rule foldl_rule_aux) auto

lemma getChoices_sub_edges:
"(a,b) ∈ set (getChoices g p es) ⟹ a ∈ set es"
using getChoices_sub_edges_fst
by force

lemma getChoices_p_snd:
"snd  set (getChoices g p es) ⊆ {p}"
unfolding getChoices_def
by (rule foldl_rule_aux) auto

lemma getChoices_p:
"(a,b) ∈ set (getChoices g p es) ⟹ b = p"
using getChoices_p_snd
by force

definition sort_by_pri where
"sort_by_pri min_pri edges = foldl (λes e.
let idx = nat_of_integer (abs (prio e))
in if idx > min_pri
then abort STR ''Invalid priority'' (λ_. es)
else let ep = e # (es ! idx) in es[idx := ep]
) (replicate (min_pri + 1) []) edges"

lemma sort_by_pri_edges':
assumes "set edges ⊆ A"
shows "set (sort_by_pri min_pri edges) ⊆ {xs. set xs ⊆ A}"
using assms
unfolding sort_by_pri_def
apply (rule_tac I="λσ _. (∀x ∈ set σ. set x ⊆ A) ∧ length σ = min_pri + 1" in foldl_rule_aux_P)
apply simp
apply (force dest!: subsetD[OF set_update_subset_insert]
split: if_splits)
apply force
done

lemma sort_by_pri_edges:
assumes "set edges ⊆ A"
and "es ∈ set (sort_by_pri min_pri edges)"
shows "set es ⊆ A"
using sort_by_pri_edges'[OF assms(1)] assms
by auto

lemma sort_by_pri_length:
"length (sort_by_pri min_pri edges) = min_pri + 1"
unfolding sort_by_pri_def
by (rule foldl_rule_aux_P [where I="λσ _. length σ = min_pri + 1"])
simp_all

definition executable
:: "states iarray ⇒ gState⇩I ⇒ choices nres"
― ‹Find all executable edges›
where
"executable ss g = (
let procs = procs g in
nfoldli procs (λ_. True) (λp E.
if (exclusive g = 0 ∨ exclusive g = pid p) then do {
let (min_pri, edges) = (ss !! pState.idx p) !! pc p;
ASSERT(set edges ⊆ edgeSet (ss !! pState.idx p));

(E',_,_) ←
if min_pri = 0 then do {
WHILE⇩T (λ(E,brk,_). E = [] ∧ brk = 0) (λ (_, _, ELSE). do {
let g = g⦇gState⇩I.else := ELSE⦈;
E = getChoices g p edges
in
if E = [] then (
if ¬ ELSE then RETURN (E, 0::nat, True)
else RETURN (E, 1, False))
else RETURN (E, 1, ELSE) }) ([], 0::nat, False)
} else do {
let min_pri = nat_of_integer (abs min_pri);
let pri_edges = sort_by_pri min_pri edges;
ASSERT (∀es ∈ set pri_edges.
set es ⊆ edgeSet (ss !! pState.idx p));
let pri_edges = IArray pri_edges;

WHILE⇩T (λ(E,pri,_). E = [] ∧ pri ≤ min_pri) (λ(_, pri, ELSE). do {
let es = pri_edges !! pri;
let g = g⦇gState⇩I.else := ELSE⦈;
let E = getChoices g p es;
if E = [] then (
if ¬ ELSE then RETURN (E,pri,True)
else RETURN (E, pri + 1, False))
else RETURN (E, pri, ELSE) }) ([], 0, False)
};
RETURN (E'@E)
} else RETURN E
) []
)"

definition
"while_rel1 =
measure (λx. if x = [] then 1 else 0)
<*lex*> measure (λx. if x = 0 then 1 else 0)
<*lex*> measure (λx. if ¬ x then 1 else 0)"

lemma wf_while_rel1:
"wf while_rel1"
unfolding while_rel1_def
by auto

definition
"while_rel2 mp =
measure (λx. if x = [] then 1 else 0)
<*lex*> measure (λx. (mp + 1) - x)
<*lex*> measure (λx. if ¬ x then 1 else 0)"

lemma wf_while_rel2:
"wf (while_rel2 mp)"
unfolding while_rel2_def
by auto

lemma executable_edgeSet:
assumes "gState_inv prog g"
and "program_inv prog"
and "ss = states prog"
shows "executable ss g
≤ SPEC (λcs. ∀(e,p) ∈ set cs.
e ∈ edgeSet (ss !! pState.idx p)
∧ pState_inv prog p
∧ cl_inv (g,p))"
unfolding executable_def
using assms
apply (refine_rcg refine_vcg nfoldli_rule[where
I="λ_ _ cs. ∀(e,p) ∈ set cs.
e ∈ edgeSet (ss !! pState.idx p)
∧ pState_inv prog p
∧ cl_inv (g,p)"])
apply simp
apply (rename_tac p l1 l2 σ e p')
apply (subgoal_tac "pState_inv prog p")
apply (clarsimp simp add: edgeSet_def pState_inv_def)[]
apply (rule_tac x="IArray.list_of
(IArray.list_of (states prog) ! pState.idx p) ! pc p" in bexI)
apply simp
apply (force intro!: nth_mem)
apply (refine_rcg refine_vcg wf_while_rel1 WHILET_rule[where
I="λ(cs,_,_). ∀(e,p) ∈ set cs.
e ∈ edgeSet (ss !! pState.idx p)
∧ pState_inv prog p
∧ cl_inv (g,p)"
and R=while_rel1])
apply (vc_solve solve: asm_rl simp add: while_rel1_def)
apply (frule getChoices_p)
using  getChoices_sub_edges apply (force simp add: gState_inv_def)
using sort_by_pri_edges apply fastforce
apply (rename_tac min_pri pri_edges)
apply (rule_tac I="λ(cs,_,_). ∀(e,p) ∈ set cs.
e ∈ edgeSet (ss !! pState.idx p)
∧ pState_inv prog p
∧ cl_inv (g,p)"
and R="while_rel2 (nat_of_integer (abs min_pri))"
in WHILET_rule)
apply simp
apply (refine_rcg refine_vcg)
apply (clarsimp_all split: prod.split simp add: while_rel2_def)
apply (metis diff_less_mono lessI)
apply (rename_tac idx' else e p')
apply (frule getChoices_p)
apply (frule getChoices_sub_edges)
apply (subgoal_tac
"sort_by_pri (nat_of_integer ¦min_pri¦) pri_edges ! idx'
∈ set (sort_by_pri (nat_of_integer ¦min_pri¦) pri_edges)")
apply (auto simp add: assms gState_inv_def)[]
done

lemma executable_edgeSet':
assumes "gState_inv prog g"
and "program_inv prog"
shows "executable (states prog) g
≤ SPEC (λcs. ∀(e,p) ∈ set cs.
e ∈ edgeSet ((states prog) !! pState.idx p)
∧ pState_inv prog p
∧ cl_inv(g,p))"
using executable_edgeSet[where ss = "states prog"] assms
by simp

schematic_goal executable_refine:
"RETURN (?ex s g) ≤ executable s g"
unfolding executable_def
by (refine_transfer)

concrete_definition executable_impl for s g uses executable_refine

subsubsection ‹Successor calculation›

function to⇩I where
"to⇩I ⦇ gState.vars = v, channels = ch, timeout = t, procs = p ⦈
= ⦇ gState.vars = v, channels = ch, timeout = False, procs = p,
handshake = 0, hsdata = [], exclusive = 0, gState⇩I.else = False ⦈"
by (metis gState.cases) (metis gState.ext_inject)
termination by lexicographic_order

function "from⇩I" where
"from⇩I ⦇ gState.vars = v, channels = ch, timeout = t, procs = p, … = m ⦈
= ⦇ gState.vars = v, channels = ch, timeout = t, procs = p ⦈"
by (metis gState.surjective) (metis gState.ext_inject)
termination by lexicographic_order

function reset⇩I where
"reset⇩I ⦇ gState.vars = v, channels = ch, timeout = t, procs = p,
handshake = hs, hsdata = hsd, exclusive = _, gState⇩I.else = _ ⦈
= ⦇ gState.vars = v, channels = ch, timeout = False, procs = p,
handshake = 0, hsdata = if hs ≠ 0 then hsd else [], exclusive = 0,
gState⇩I.else = False ⦈"
by (metis (full_types)  gState⇩I.surjective unit.exhaust)
(metis gState.select_convs gState⇩I.select_convs)
termination by lexicographic_order

lemma gState_inv_to⇩I:
"gState_inv prog g = gState_inv prog (to⇩I g)"
by (cases g, simp add: gState_inv_def cl_inv_def)

lemma gState_inv_from⇩I:
"gState_inv prog g = gState_inv prog (from⇩I g)"
by (cases g, simp add: gState_inv_def cl_inv_def)

lemma gState_inv_reset⇩I:
"gState_inv prog g = gState_inv prog (reset⇩I g)"
by (cases g, simp add: gState_inv_def cl_inv_def)

lemmas gState_inv_I_simps =
gState_inv_to⇩I gState_inv_from⇩I gState_inv_reset⇩I

definition removeProcs
― ‹Remove ended processes, if there is no running one with a higher pid.›
where
"removeProcs ps = foldr (λp (dead,sd,ps,dcs).
if dead ∧ pc p = 0 then (True, True, ps, pState.channels p @ dcs)
else (False, sd, p#ps, dcs)) ps (True, False, [], [])"

lemma removeProcs_subset':
"set (fst (snd (snd (removeProcs ps)))) ⊆ set ps"
unfolding removeProcs_def
apply (subst foldr_conv_foldl)
apply (rule foldl_rule_aux_P[where I="λ(_,_,ps',_) _. set ps' ⊆ set ps"])
apply simp
apply (clarsimp split: if_splits)
apply force
apply (rename_tac p)
apply (case_tac "p = x")
apply (subst set_rev[symmetric])
apply simp
apply force
apply force
done

lemma removeProcs_length':
"length (fst (snd (snd (removeProcs ps)))) ≤ length ps"
unfolding removeProcs_def
apply (subst foldr_conv_foldl)
apply (rule foldl_rule_aux_P[where
I="λ(_,_,ps',_) ps''. length ps' + length ps'' ≤ length ps"])
apply (auto split: if_splits)
done

lemma removeProcs_subset:
"removeProcs ps = (dead,sd,ps',dcs) ⟹ set ps' ⊆ set ps"
using removeProcs_subset'
by (metis fst_conv snd_conv)

lemma removeProcs_length:
"removeProcs ps = (dead,sd,ps',dcs) ⟹ length ps' ≤ length ps"
using removeProcs_length'
by (metis fst_conv snd_conv)

definition cleanChans :: "integer list ⇒ channels ⇒ channels"
― ‹Mark channels of closed processes as invalid.›
where
"cleanChans dchans cs = snd (foldl (λ(i,cs) c.
if List.member dchans i then (i + 1, cs@[InvChannel])
else (i + 1, cs@[c])) (0, []) cs)"

lemma cleanChans_channel_inv:
assumes "set cs ⊆ Collect channel_inv"
shows "set (cleanChans dchans cs) ⊆ Collect channel_inv"
using assms
unfolding cleanChans_def
apply (rule_tac foldl_rule_aux)
apply (force split: if_splits)+
done

lemma cleanChans_length:
"length (cleanChans dchans cs) = length cs"
unfolding cleanChans_def
by (rule foldl_rule_aux_P[where
I="λ(_,cs') cs''. length cs' + length cs'' = length cs"])
(force split: if_splits)+

definition checkDeadProcs :: "'a gState_scheme ⇒ 'a gState_scheme" where
using assms cleanChans_length[where