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

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

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

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

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