Theory PromelaDatastructures
section "Data structures as used in Promela"
theory PromelaDatastructures
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.
The additional information contains:
\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.
›
datatype binOp = BinOpAdd
| BinOpSub
| BinOpMul
| BinOpDiv
| BinOpMod
| BinOpGr
| BinOpLe
| BinOpGEq
| BinOpLEq
| BinOpEq
| BinOpNEq
| BinOpAnd
| BinOpOr
datatype unOp = UnOpMinus
| UnOpNeg
datatype expr = ExprBinOp binOp expr expr
| ExprUnOp unOp expr
| ExprCond expr expr expr
| ExprLen chanRef
| ExprVarRef varRef
| ExprConst integer
| ExprMConst integer String.literal
| ExprTimeOut
| ExprFull chanRef
| ExprEmpty chanRef
| ExprPoll chanRef "recvArg list" bool
and varRef = VarRef bool
String.literal
"expr option"
and chanRef = ChanRef varRef
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 integer integer
String.literal
"integer option"
"expr option"
| VarDeclChan String.literal
"integer option"
"(integer * varType list) option"
text ‹Variable declarations during a proctype.›
datatype procVarDecl = ProcVarDeclNum integer integer
String.literal
"integer option"
"expr option"
| ProcVarDeclChan String.literal
"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
| StmntRecv chanRef "recvArg list" bool bool
| StmntAssign varRef expr
| StmntElse
| StmntBreak
| StmntSkip
| StmntGoTo String.literal
| StmntLabeled String.literal stmnt
| StmntRun String.literal
"expr list"
| StmntCond expr
| StmntAssert expr
and step = StepStmnt stmnt "stmnt option"
| StepDecl "procVarDecl list"
| StepSkip
datatype proc = ProcType "(integer option) option"
String.literal
"procArg list"
"varDecl list"
"step list"
| Init "varDecl list" "step list"
type_synonym ltl = " String.literal × 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}›
text ‹The preprocessing is done for each type on its own.›
primrec ppBinOp :: "AST.binOp ⇒ binOp"
where
"ppBinOp AST.BinOpAdd = BinOpAdd"
| "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
× (String.literal, (integer option × bool)) lm
× (String.literal, integer) lm
× (String.literal, varRef) lm "
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))"
| "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"
definition incr :: "varRef ⇒ stmnt" where
"incr v = StmntAssign v (ExprBinOp BinOpAdd (ExprVarRef v) (ExprConst 1))"
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
loop_pre = StepStmnt (StmntAssign i lb) None;
loop_cond = StepStmnt (StmntCond
(ExprBinOp BinOpLEq (ExprVarRef i) ub))
None;
loop_incr = StepStmnt (incr i) None;
loop_body = loop_cond # steps @ [loop_incr];
loop_abort = [StepStmnt StmntElse None, StepStmnt StmntBreak None];
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
loop_pre = StepStmnt (StmntAssign i (ExprConst 0)) None;
loop_cond = StepStmnt (StmntCond
(ExprBinOp BinOpLe (ExprVarRef i)
(ExprConst N)))
None;
loop_incr = StepStmnt (incr i) None;
loop_body = loop_cond # steps @ [loop_incr];
loop_abort = [StepStmnt StmntElse None, StepStmnt StmntBreak None];
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
tmpStr = STR '':tmp:'';
loop_pre = StepDecl
[ProcVarDeclNum 0 255 tmpStr None (Some (ExprConst 0))];
tmp = VarRef False tmpStr None;
loop_cond = StepStmnt (StmntCond
(ExprBinOp BinOpLe (ExprVarRef tmp)
(ExprLen c)))
None;
loop_incr = StepStmnt (incr tmp) None;
recv = StepStmnt (StmntRecv c [RecvArgVar msg] False True) None;
send = StepStmnt (StmntSend c [ExprVarRef msg] False) None;
loop_body = [loop_cond, recv, send] @ steps @ [loop_incr];
loop_abort = [StepStmnt StmntElse None, StepStmnt StmntBreak None];
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
pre = StepStmnt (StmntAssign i lb) None;
cond = StepStmnt (StmntCond (ExprBinOp BinOpLe (ExprVarRef i) ub))
None;
incr = StepStmnt (incr i) None;
loop_body = [cond, incr];
loop_abort = [StepStmnt StmntBreak None];
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)"
| "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
datatype edgeEffect = EEEnd
| EEId
| EEGoto
| EEAssert expr
| EEAssign varRef expr
| EEDecl procVarDecl
| EERun String.literal "expr list"
| EESend chanRef "expr list" bool
| EERecv chanRef "recvArg list" bool bool
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"
| InvChannel
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 = "( integer × edge list) iarray"
type_synonym channels = "channel list"
type_synonym process =
"nat
× edgeIndex
× procArg list
× varDecl list "
record program =
processes :: "process iarray"
labels :: "labels iarray"
states :: "states iarray"
proc_names :: "String.literal iarray"
proc_data :: "(String.literal, nat) lm"
record pState =
pid :: nat
vars :: var_dict
pc :: nat
channels :: "integer list"
idx :: nat
hide_const (open) idx
record gState =
vars :: var_dict
channels :: channels
timeout :: bool
procs :: "pState list"
record gState⇩I = gState +
handshake :: nat
hsdata :: "integer list "
exclusive :: nat
else :: bool
subsection ‹Printing›
primrec printBinOp :: "binOp ⇒ string" where
"printBinOp BinOpAdd = ''+''"
| "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) []"
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
by standard (simp_all add: def_hashmap_size_assoc_list_def)
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
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)"
by(simp add: def_hashmap_size_lexlist_def)
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)"
by (simp add: walk_iarray_def walk_iarray'_Cons)
lemma walk_iarray_append:
"walk_iarray f (IArray (xs@[x])) b = f (walk_iarray f (IArray xs) b) x"
by (induct xs arbitrary: b) (simp add: walk_iarray_def, simp add: walk_iarray_Cons)
lemma walk_iarray_foldl':
"walk_iarray f (IArray xs) x = foldl f x xs"
by (induction xs rule: rev_induct) (simp add: walk_iarray_def, simp add: walk_iarray_append)
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"
by (simp add: walk_iarray_foldl)
end
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)"
by (simp add: walk_array_def walk_array'_Cons)
lemma walk_array_append:
"walk_array f (Array (xs@[x])) b = f (walk_array f (Array xs) b) x"
by (induct xs arbitrary: b) (simp add: walk_array_def, simp add: walk_array_Cons)
lemma walk_array_foldl':
"walk_array f (Array xs) x = foldl f x xs"
by (induction xs rule: rev_induct) (simp add: walk_array_def, simp add: walk_array_append)
lemma walk_array_foldl:
"walk_array f a x = foldl f x (list_of_array a)"
by (cases a) (simp add: walk_array_foldl')
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"
by (simp add: walk_array_foldl)
end
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 Promela
section "Formalization of Promela semantics"
theory Promela
imports
PromelaDatastructures
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
by (metis dual_order.trans less_add_one order.strict_trans
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"
by (simp add: for_all_def foldli_conj)
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"
| "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
if lRange = 0 ∧ val > 0
then val mod (hRange + 1)
else
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)
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
simp add: pState_inv_def
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)
apply (simp_all add: assms gState_inv_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
simp add: pState_inv_def)
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"
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
by (simp add: lm.correct)
lemma emptyProc_cl_inv[simp]:
"cl_inv (g, emptyProc)"
by (simp add: cl_inv_def emptyProc_def)
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
by (auto simp add: vardict_inv_empty)
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
if length args ≠ length argDecls
then abortv STR ''Signature mismatch: '' name (λ_. (g,emptyProc))
else
let
eArgs = map (exprArith g p) args;
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;
p = ⦇ pid = pidN, vars = argVars, pc = start, channels = [], idx = sidx ⦈
in
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 (simp add: p_def)
apply (intro lm_to_map_vardict_inv)
apply auto
apply (simp add: max_procs_def max_var_value_def)
apply transfer'
apply simp
apply transfer'
apply simp
apply (simp add: min_var_value_def)
apply transfer'
apply simp
apply (simp add: max_var_value_def max_procs_def)
apply transfer'
apply simp
apply (drule set_zip_leftD)
apply (force simp add: modProcArg_def
split: procArg.splits if_splits
intro!: image_eqI)
apply (clarsimp simp add: modProcArg_def
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 (simp add: pState_inv_def)
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' ⦈)"
by (simp add: cl_inv_def)
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
by (simp_all add: lm.correct program_inv_def)
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)
(auto simp add: gState_inv_def cl_inv_def)
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))"
by (simp add: assms runProc_pState_id)
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')"
by (simp add: gState_progress_rel_def)
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 ⇒
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
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
(ues,_,lbls') = stmntToState u (lbls, pri, pos, nxt, onxt, True);
u = last ues; ues = butlast ues;
pos' = pos + length ues;
pri = min_prio u pri;
(ses,spos,lbls'') = stmntToState s (lbls', pri - 1, pos', nxt, onxt, False);
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);
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
(_,_,lbls,es,is) = step_foldL stepToState stepss lbls pri
(pos+1) (Index pos) (Some nxt);
es' = concat is # es
in
if inBlock then
(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
"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,
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)
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)
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
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
by (auto simp add: edgeDecls_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')"
by (auto simp add: channel_inv.simps)
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))"
by (auto simp add: channel_inv.simps)
}
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')"
by (simp add: gState_progress_rel_def)
}
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
qed (simp_all add: setVar_cl_inv mkVarChannelProc_cl_inv)
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"
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"
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 (force simp add: gState_inv_def)
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 add: wf_while_rel2)
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)[]
apply (force simp add: sort_by_pri_length)
apply (auto simp add: assms)
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
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"
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
"checkDeadProcs g = (
let (_, soDied, procs, dchans) = removeProcs (procs g) in
if soDied then
g⦇ procs := procs, channels := cleanChans dchans (channels g)⦈
else g)"
lemma checkDeadProcs_gState_progress_rel:
assumes "gState_inv prog g"
shows "(g, checkDeadProcs g) ∈ gState_progress_rel prog"
using assms cleanChans_length[where