[isabelle] Symbolic execution in Isabelle.



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

 

 



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.