Email Gateway (Aug 18 2022 at 12:39): Email Gateway (Aug 18 2022 at 12:39):From: Liu Jian <gjk.liu@gmail.com>
Dear All,
I am now interested in the work of the following paper
David Cock, Gerwin Klein and Thomas Sewell "Secure Microkernels, State
Monads nad Scalable Refinement"
But a question about how to define a longer computation for "bind"
operator of State monad
As the paper says "bind" can be defined as following:
bind :: ('s, 'a) state-monad => ('a => ('s, 'b) state-mond) => ('s,
'b) state-monad
bind f g == % s. let (v, s') = f s in g v s'
And, "The expression bind f g is abbreivated as f >>= g, To allow
concise description for longer computations,
we define a do syntax in sa similar fashion to Haskell"
do x <- f; g x od == f >>= g
But how to write the real isabelle statements for the above
definition? (Note there is parameter "x")
Moreover, from the above syntax, we can write the following monad code:
(in Kevin Elphinstoen, Gerwin Klein etc. "Formalising a
High-Performance Microkernel")
activateThread ==
do thread <- getCurThread;
state <- getWaitState thread;
case state of
NotWaiting => return ()
| WaitingToSend eptr badge fault cap =>
if cap = None then
doIPCTransfer thread (waitingIPCPartner state)
else arbitrary
| WaitinToRecieve eptr =>
doIPCTransfer (waitingIPCPartner state) thread
| => arbitrary
od
Note that there are three monad binded in the above definition. But in
the "do ... od" statement definition only contain two,
How to deal with it? If possible could you give a example real
isabelle definition for above definition?
cheers:)
Liu Jian
Email Gateway (Aug 18 2022 at 12:39):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Liu Jian wrote:
It's fairly standard syntax black magic and works roughly like the normal let
bindings in Isabelle (e.g. see HOL/HOL.thy).
A more complex example directly with "do" syntax can be found in
HOL/Library/StateMonad.thy. It's slightly different from the one in our
papers, but the effect is the same.
Cheers,
Gerwin
Email Gateway (Aug 18 2022 at 12:40):From: Liu Jian <gjk.liu@gmail.com>
Thanks Gerwin! following your direction, I write the following statements
types ('s, 'a)state_monad = " 's => ('a , 's)"
constdefs bind :: "('s, 'a)state_monad =>('a => ('s, 'b)state_monad)
=>('s, 'b)state_monad" (infixr ">>=" 60)
" f >>= g == % s . let (v, s') = f s in g v s'"
nonterminals
dobind
syntax
"_bind" :: "[pttrn, 'a] => dobind" ("(2_ <-/ _)" 10)
"_do" :: "[dobind, 'a] => 'b" ("( do _ ;/ _
od )" [0,0] 10)
translations
" do x <- f ; g od" == " f >>= (% x. g)"
Now, binding two monads is easy. But How to bind three or more monads
in a "do ... od"
statement? Moreover, what is the association attribute of "bind"
operator? infixr or infixl.
In the above definition I use the former. But I can not hold the
difference between them.
cheers:)
Liu Jian
Email Gateway (Aug 18 2022 at 12:40):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Hi Liu,
you need to do the rest as well, see lines 125-192 in
HOL/Library/StateMonad.thy. The file is part of Isabelle2008 already, I
believe, if not, you can find it in the Isabelle development snapshot.
Specifically, you will need _scomp (and _fcomp if you want to leave out the
"_ <-" part) and for printing also the ML print translation. Florian Haftmann
wrote that specific theory, he'll be able to explain in more detail how it works.
Cheers,
Gerwin
Liu Jian wrote:
Email Gateway (Aug 18 2022 at 12:40):From: Liu Jian <gjk.liu@gmail.com>
Hi,
I have tried a test like "StateMonad.thy" under your direction, But
A error occur when deal with "if ... then ... else..." or "case ...
of ..." statement as following
activateThread ==
do thread <- getCurThread;
state <- getWaitState thread;
case state of
NotWaiting => return ()
| WaitingToSend eptr badge fault cap =>
if cap = None then
doIPCTransfer thread (waitingIPCPartner state)
else arbitrary
| WaitinToReciev Note idefinition
| WaitingToReceive eptr =>
doIPCTransfer (waitingIPCPartner state) thread
| => arbitrary
Note in the above definition, monads embeds in a case statement.
As "State_Monad.thy" says there are some "do...done" examples in
"HOL/ex/Random.thy".
Lines 101~107 (Random.thy) show me a example as following:
range :: "index => seed => index => seed"
where
"range k = (do
v <- range_aux (log 2147483561 k) 1;
return (v mod k)
done)"
When you simply change it as following, a error occurs.
range :: "index => seed => index => seed"
where
"range k = (do
v <- range_aux (log 2147483561 k) 1;
if True return (v mod k) else return (v mod k)
done)"
cheers,
Liu Jian
BTW:
what's the meaning of following lines. Here, I can not understand the
meaning of "CONST" and the difference between "=>" and "==" in a
translation
translations
"_do f" => "CONST run f"
Email Gateway (Aug 18 2022 at 12:43):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Liu Jian,
When you simply change it as following, a error occurs.
range :: "index => seed => index => seed"
where
"range k = (do
v <- range_aux (log 2147483561 k) 1;
if True return (v mod k) else return (v mod k)
done)"
The reason for this failure is the HOL if syntax: it demands a "then",
an in most cases has to be put in brackets:
"range k = (do
v <- range_aux (log 2147483561 k) 1;
(if True then return (v mod k) else return (v mod k))
done)"
what's the meaning of following lines. Here, I can not understand the
meaning of "CONST" and the difference between "=>" and "==" in a
translationtranslations
"_do f" => "CONST run f"
The "CONST" is a technical detail - for historical reasons, there are
two syntactic classes of constants: constants which are represented with
their proper qualified names in the syntax layer ("authentic constants")
and constants which are represented just by their base name
("non-authentic constants"). New-style definition tools (definition,
inductive, function, primrec with new "where"-syntax ...) yield
authentic constants, whereas older devices do not (consts, constdefs,
...). The "CONST" marker states that "run" is an authentic constant.
The difference between "=>" and "==" in first approximation is that "=>"
is only applied in input direction, whereas "==" is applied during input
and reversely during output. For a detailed description on how the
syntax layer work I have to redirect you to the old Isabelle Reference
Manual http://isabelle.in.tum.de/dist/Isabelle/doc/ref.pdf which is
outdated in huge passages but the chapter on syntax still represents the
current implementation fairly well.
Hope this helps
Florian
signature.asc
Email Gateway (Aug 18 2022 at 12:46):From: Makarius <makarius@sketis.net>
In fact, the CONST marker will always do the right thing, both for
new-style constants with "authentic syntax" and the old-style ones. But
for authentic consts you cannot do it otherwise, while old-style
non-authentic ones could be given as unqualified (and unchecked) base
names, although this is not recommended.
In other words: always use explicit CONST if you refer to constants at the
level of syntax translations.
Makarius
Last updated: May 03 2024 at 12:27 UTC