Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Symbolic execution in Isabelle.


view this post on Zulip Email Gateway (Apr 18 2021 at 09:29):

From: Thomas Melham <tom.melham@cs.ox.ac.uk>
Dear Isabelle Users,

Please excuse me for a beginners’ question!

My student Dapeng Gao and I are looking into using Isabelle for symbolic execution of large microprocessor instruction set specifications. Our starting point is the translation into Isabelle definitions of the SAIL specification for the CHERI RSIC-V ISA:

https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri-risc-v.html

This consists of a large number of function definitions that define the effect on visible architectural state of each of the CHERI RISC-V machine instructions – functions of the form

InstructionX ins1 ins2 ... insn = <effect on an architectural state monad>

where ins1, ins2, ... insn are variables raging over fields of the machine instruction X. E.g. register addresses, immediate data, etc.

We want to be able to use Isabelle in “forward proof” mode, in which we specialise some or all of the variables ins1, ins2, ... insn to data structures containing some variables (for example a list of Boolean bits, each represented by a variable). And then use rewriting and simplification to compute a kind of normal form effect on machine state as a function of the inputs. I.e. get a simplified logical expression on the RHS – which we can then traverse and translate into another language outside the logic.

Is this kind of thing possible in Isabelle? We don’t want to have to type the right-and sides in, so goal directed proof is no use to us.

Best regards,

Tom

view this post on Zulip Email Gateway (Apr 19 2021 at 01:04):

From: Peter Gammie <peteg42@gmail.com>
Tom,

I’m sure there are a variety of ways to do this at the ML level, e.g. using the mechanisms the subst and simp methods leverage. This is likely to be the way to go for robustness. Look at the (Pure/)Conv structure for instance, which I expect is similar to what’s in HOL(4).

At the Isar (surface) level you can try to use schematic_goal. There is some documentation somewhere — try the Isar reference manual. Thomas Sewell helped me with this:

https://www.isa-afp.org/browser_info/current/AFP/ConcurrentGC/Tactics.html
-> schematic_goal system_responds_actionE

Note that schematic variables are sometimes aggressively instantiated by some tools. For instance I’d expect

schematic_goal “1 + 2 = ?x” by simp

to instantiate ?x to 1 + 2. Hence the very ginger small steps (mostly resolution) taken in the above theory. IIRC this behaviour is in the default simplifier solver setup, which you should be able to tweak without too much hassle but may result in breaking other things.

cheers,
peter

view this post on Zulip Email Gateway (Apr 19 2021 at 10:14):

From: Makarius <makarius@sketis.net>
The attached Scratch.thy provides some entry points that might actually help
to the original questions on this thread: to be explored in Isabelle/jEdit
with C-hover-click on the various embedded items. If you also open
$ISABELLE_HOME/src/Pure/ROOT.ML (e.g. via the Documentation panel) you get IDE
markup for the Isabelle/Pure implementation: this is important to understand them.

These are just some abstract hints to get started with the correct mindset and
toolset.

Makarius
Scratch.thy

view this post on Zulip Email Gateway (Apr 19 2021 at 11:22):

From: Makarius <makarius@sketis.net>
Yes, the classic way to "drive the prover" in ML following the LCF paradigm
works very well in Isabelle. You merely need to keep in mind that Isabelle/ML
is always embedded into Isabelle/Isar, with a formal theory or proof context
around it. Even the toplevel ML bindings are stored in the formal context.

As a start, just take Isabelle/jEdit and produce a theory file with some 'ML'
snippets, e.g. copied from the sources of the manuals in
$ISABELLE_HOME/src/Doc or other examples.

By expanding such Isabelle/ML snippets, they eventually become your tool
implementation: experimentation and implementation is intertwined.

Isabelle/ML text that grows too large becomes its own ML file eventually. See
also the isar-ref manual on commands like 'ML', 'ML_file', but also 'ML_val'
for exploring proof states.

Makarius

view this post on Zulip Email Gateway (Apr 19 2021 at 20:24):

From: Thomas Sewell <tals4@cam.ac.uk>
Hi Thomas.

I think it's worth adding that there are two sides to this story.

Isabelle is a fairly flexible tool. You can probably use the simplifier,
in some form or another, to help you doing this rewriting, and it's
possible that it gets the job done easily.

However, it's not clear to me from your explanation that Isabelle is the
right tool for the job. Isabelle is an interactive theorem prover, so
I'd
expect you to be using it if you want to prove some theorem, and you
accept
some interactive work as a cost of doing that. If you're just
preprocessing
a function definition to pass to some other tool, perhaps you don't need
that? If Isabelle doesn't turn out to solve your problems easily,
perhaps
you could investigate some of the other SAIL backends.

To extend on Pete Gammie's remark, you can also run the simplifier as a
rewriter from within a theory file like this:

ML {*
Simplifier.rewrite
(@{context} addsimps @{thms id_def})
@{cterm "f x"}
*}

Working within a theory file can be very convenient for experimentation.
I've used the old ASCII syntax above for reasons to do with email
formatting.

Cheers,
Thomas.


Last updated: Sep 28 2021 at 20:18 UTC