codegen for predicates · General

I am trying to use the codegen's extension code_pred to generate equational specifications from an inductive predicate. The hope is that from there I can then extract functional code.
The motivation for doing this is to have a reliable reference interpreter for the operational semantics described by the Isabelle code.

The problem is that for some reason the code_pred command does not succeed, and trying to invoke the predicate equation gives an error. I think probably the error was due to the predicate not being regularly defined in an inductive way. I did a bit of research into the codegen reference manual and it gave an example where a non-inductively defined predicate can be made inductive by making the conditions described by inductive predicates (e.g. describing lexicographic order by the append predicate). Is it the case that the code_pred extension compiler only works when the inductive rules' premises are made of inductive predicates themselves? In general, how can one turn an irregular predicate definition into an inductive one (for example in my example listed below)? I have put a MWE below for the predicate that failed code_pred.

theory Predicate_to_code imports
  Main
begin




datatype RegNum = Reg nat
type_synonym Val = int
datatype MESI_State = Modified| Exclusive| Shared| Invalid
datatype ClusterID = Dev nat
datatype BlockID = Block nat
datatype UTID = Utid nat
datatype CoreID = Core nat


record CLEntry =
  content :: "Val option"
  block_state :: MESI_State


type_synonym ClusterMap = "CoreID ⇒ BlockID ⇀ CLEntry"

type_synonym DevCLMap = "ClusterID ⇒ ClusterMap"


(*Alternative of using tuples, waiting to be seen which is better*)
type_synonym Cluster_State_Table = "ClusterID ⇀ MESI_State "
text ‹the name cl_state_mapping seems quite un-friendly for first time readers›



record HostCLMap =
  cl_content_mapping  :: "BlockID ⇒ Val"
  cl_state_mapping    :: "BlockID ⇒ Cluster_State_Table"



datatype Instruction =
      Write ClusterID CoreID BlockID Val RegNum
    | Read ClusterID CoreID BlockID RegNum
    | Evict ClusterID CoreID BlockID
(*a sequence of events one cluster issues, a sequence of events another cluster issues
read event v.s. load
cluster  issue messages *)
type_synonym Program = "ClusterID ⇒ (CoreID ⇒ Instruction list)"

definition empty_program :: Program where [simp]:
"empty_program ≡ λclid. λcoreid. []"

fun add_i :: "Program ⇒ Instruction ⇒ ClusterID ⇒ CoreID ⇒ Program"
  where "add_i P i clid core = P (clid := ( (P clid  ) (  core := (P clid core) @ [i])))"

definition write1 :: Instruction where "write1 = (Write (Dev 1) (Core 1) (Block 1) 2 (Reg 1))"
definition write2 :: Instruction where "write2 = (Write (Dev 2) (Core 2) (Block 1) 3 (Reg 1))"


definition two_devices_writing_at_same_location :: Program where
"two_devices_writing_at_same_location = add_i (add_i empty_program write1 (Dev 1) (Core 1)) write2 (Dev 2) (Core 2)"

datatype DTHReqType = RdShared | RdOwn | RdOwnNoData | RdAny | RdCurr | CleanEvict | DirtyEvict | CleanEvictNoData |
  ItoMWrite | WrCur | CLFlush | CacheFlushed | WOWrInv | WOWrInvF | WrInv



record DTHReq =
  utid :: UTID
  bid :: BlockID
  dthreqtype :: DTHReqType
  clid :: ClusterID


type_synonym DTHReqs = "ClusterID ⇒ DTHReq list"


datatype DTHRespType = RspIHitI | RspIHitSE |RspSHitSE | RspVHitV | RspIFwdM  | RspVFwdV  | RspSFwdM

record DTHResp =
  utid:: UTID
  bid :: BlockID
  dthresptype :: DTHRespType
  clid :: ClusterID



record DTHData =
  utid:: UTID
  bid :: BlockID
  content :: Val
  clid :: ClusterID
  bogus :: bool





type_synonym DTHResps = "ClusterID ⇒ DTHResp list"



type_synonym DTHDatas = "ClusterID ⇒ DTHData list"


definition empty_dthreqs :: DTHReqs where [simp]:
"empty_dthreqs ≡ λclid. []"


definition empty_dthdatas :: DTHDatas where [simp]:
"empty_dthdatas ≡ λclid. []"
definition empty_dthresps :: DTHResps where [simp]:
"empty_dthresps ≡ λclid. []"



datatype HTDReqType = SnpData | SnpInv | SnpCur

record HTDReq =
  utid :: UTID
  bid :: BlockID
  htdreqtype :: HTDReqType
  clid :: ClusterID

datatype HTDRespType = GO | GO_WritePull | GO_WritePullDrop | WritePull |
    GO_Err | FastGO_WritePull | GO_Err_WritePull | ExtCmp


record HTDResp =
  utid :: UTID
  bid :: BlockID
  htdresptype :: HTDRespType
  clid :: ClusterID
  state_granted :: MESI_State

record HTDData =
  utid :: UTID
  bid :: BlockID
  content :: Val
  clid :: ClusterID



type_synonym HTDReqs = "ClusterID ⇒ HTDReq list"



type_synonym HTDResps = "ClusterID ⇒ HTDResp list"

type_synonym HTDDatas = "ClusterID ⇒ HTDData list"

record DevTracker =
  clusterid :: ClusterID
  coreid  :: CoreID
  bid     :: BlockID
  st      :: MESI_State
  dNeeded :: bool
  dataCompleted  :: bool
  rRecvd  :: bool
  dthreqtype :: DTHReqType

text ‹Our model only deals with transactions initiated by a DTHRequest.›

type_synonym DevTrackers = "UTID ⇀ DevTracker"



record HostTracker =
  clusterid :: ClusterID
  coreid  :: CoreID
  bid     :: BlockID
  st      :: MESI_State
  dNeeded :: bool
  dSent  :: bool
  rSent  :: bool
  dthreqtype :: DTHReqType

text ‹Our model only deals with transactions initiated by a DTHRequest. Likewise trackers only
records DTH request types.›

type_synonym HostTrackers = "UTID ⇀ HostTracker"



record Type1State =
  hostclmap      :: HostCLMap
  devclmap    :: DevCLMap
  dthreqs           :: DTHReqs
  dthresps          :: DTHResps
  dthdatas          :: DTHDatas
  htdreqs           :: HTDReqs
  htdresps          :: HTDResps
  htddatas          :: HTDDatas
  hosttrackers         :: HostTrackers
  devtrackers         :: DevTrackers






text ‹ for CXL ›
fun differ_one_instruction :: "Program ⇒ Program ⇒
  ClusterID ⇒ CoreID ⇒ Instruction ⇒ bool"
  where "differ_one_instruction P P' dev_i core_j i =
    (P = P'(dev_i := (P' dev_i) (core_j := (i # P' dev_i core_j ))))"

fun host_mapping_state :: "Type1State ⇒ ClusterID ⇒
  BlockID ⇒ MESI_State ⇒ bool"
  where "host_mapping_state Σ dev_i X mesi_state =
    ((cl_state_mapping (hostclmap Σ) ) X dev_i = Some mesi_state)"


fun dequeued_dthreq :: "Type1State ⇒ Type1State ⇒ ClusterID ⇒ DTHReq ⇒ bool"
  where "dequeued_dthreq Σ Σ' dev_i msg =
    (Σ' = Σ ⦇dthreqs := ((dthreqs Σ) (dev_i := (dthreqs Σ) dev_i  @ [msg] )) ⦈ ) "



(*Still psuedo-code, should express Σ and Σ' only differ in those
places, rather than "they are different in these places, can be arbitrary
in other places we didn't mention. Need to use Σ[ i := X] type of syntax"*)
inductive external_trans :: "(Type1State * Program * nat * Instruction option * UTID) ⇒ (Type1State * Program * nat * Instruction option * UTID) ⇒ bool"
(infixr "↝ext" 30)
where
RdOwn_start:
" ⟦
    differ_one_instruction P P' dev_i core_j (Write dev_i core_j block_X v reg) ;

    host_mapping_state Σ dev_i block_X Invalid;

    utid2 = Utid UCounter;
    dequeued_dthreq Σ Σ' dev_i ⦇DTHReq.utid = utid2, bid = block_X, dthreqtype = RdOwn, clid = dev_i ⦈;

    (devclmap Σ) dev_i core_j block_X = Some ⦇CLEntry.content = Some v, block_state = Invalid ⦈;
    (devclmap Σ) = (devclmap Σ');

    devtrackers Σ  utid2 = None;
    devtrackers Σ' utid2 = Some ⦇DevTracker.clusterid = dev_i, coreid = core_j, DevTracker.bid  = block_X, st = Invalid,
    dNeeded = True, dataCompleted = False, rRecvd = False, dthreqtype = RdOwn ⦈


⟧
⟹
(Σ, P, UCounter, None, _) ↝ext (Σ', P', UCounter + 1, Some (Write dev_i core_j block_X v reg), utid2 )"
|
RdOwn_finish:
" ⟦

    host_mapping_state Σ dev_i block_X Exclusive;
    (cl_content_mapping (hostclmap Σ)) block_X = v';

    (devclmap Σ) dev_i core_j block_X = Some ⦇CLEntry.content = Some v', block_state = Exclusive ⦈;
    (devclmap Σ') dev_i core_j block_X = Some ⦇CLEntry.content = Some v'', block_state = Modified ⦈;

    (hosttrackers Σ) utid2 = None;

    (devtrackers Σ) utid2 = None

⟧
⟹
(Σ, P, UCounter,  Some (Write dev_i core_j block_X v'' reg), utid2) ↝ext (Σ', P', UCounter, None, _ )"


code_pred external_trans .

thm external_trans.equation
export_code external_trans_i_o in Scala

I am trying to generate code for external_trans, which is used to capture the operational semantics for some low-level memory protocols. The rules involve updates to lists, records and functions. Are the updates of records and function mappings inherently non-inductive, making the whole rule external_trans impossible to be turned inductive?

Maximilian Schaeffeler (May 15 2023 at 09:30):

I only get an error in the last line (wellsortedness error). It is due to the function differ_one_instruction that compares two programs P and P' using function equality, which is of course not executable in general. To make it executable, the code generator requires the input types to be enumerable. You probably want to make differ_one_instruction executable by explicitly stating and proving a code equation for differ_one_instruction first.

Chengsong Tan (May 15 2023 at 19:30):

Thank you for responding! This is very helpful that I am now able to locate which bits are not executable. I understand that comparing equalities of two arbitrary functions can't be turned into executable code in general (because it is basically halting problem?), but for this function differ_one_instruction the comparison is basically saying two functions are just key-value pairs which only differ in one entry. Could you tell me what type of code equation is needed for this?

Chengsong Tan (May 15 2023 at 20:17):

More generally, do all the premises have to be expressed via recursive predicates so that an inductive rule can be turned into executable code?

Maximilian Schaeffeler (May 16 2023 at 08:59):

The code equation should implement the comparison in terms of executable functions:

lemma differ_one_instruction[code]: "differ_one_instruction P P' dev_i core_j i = [executable version of the definition]"
  sorry

However, for your example, I don't think it's possible to implement that check, can you tell me how you would do it in another programming language?

Chengsong Tan (May 18 2023 at 19:21):

I got your point. The comparison requires two programs to be equal at every other device and core, which is impossible to compute if the domain (devices and cores) is not finite. I guess for that I need to restrict the constructors of ClusterID and CoreID to take a natural number from only a finite set (rather than all possible nats).
Thank you!

Chengsong Tan (May 31 2023 at 22:30):

Can you ask code_pred to generate equational specifications with different modes (that might not be one of those inferred automatically)?
The tutorial on codegen seems to suggest yes at section 4.1 (alternative names for functions) on the bottom of page 21, where you can specify the modes you want with new names for these functions like modes: i => o => i as suffix) append1 .. But after trying out this, I got this error message from Isabelle "not a constant: suffix" when trying to generate code for that. It seems the request to generate a custom output function has been ignored. Is there any recent changes to code_pred that I need to be aware?

inductive append1 :: "'a list ⇒ 'a list ⇒ 'a list ⇒ bool"
  where
    "append1 [] ys ys"
  | "append1 xs ys zs ⟹ append1 (x # xs) ys (x # zs)"

code_pred append1 .

thm append1.equation

export_code append1_i_i_i in Scala


values "{zs. append1 [(1::nat), 2, 3] [4, 5] zs}"


code_pred (modes: i ⇒ o ⇒ i ⇒ bool as suffix,
                  o ⇒ o ⇒ i ⇒ bool as split,
                  i ⇒ i ⇒ o ⇒ bool as concat) append1 .


thm append1.equation

export_code suffix in Scala

Mathias Fleury (Jun 01 2023 at 05:03):

Mathias Fleury (Jun 01 2023 at 05:10):

Chengsong Tan (Jun 01 2023 at 08:21):

Chengsong Tan (Jun 01 2023 at 08:22):

Chengsong Tan (Jun 01 2023 at 22:32):

It seems that code_pred does not support records very well (because they are not inductive datatypes)?
Suppose we have a record type MiniMulticore:

datatype Instruction =
      Write int
    | Read

record MiniMulticore =
  program1 :: "Instruction list"
  program2 :: "Instruction list"
  mem      :: int
  reg      :: int

inductive nondet_execution :: "MiniMulticore ⇒ MiniMulticore ⇒ bool"
 (infixr "↝n" 30)  where
 core2_write : "⦇program1 = P1, program2 = Write v # P2, mem = v', reg = w ⦈ ↝n ⦇program1 = P1, program2 = P2, mem = v, reg = w ⦈"

, the code_pred command does not generate any code equations: invoking the code_pred nonet_execution command
give the following error message:

Error in case expression:
Not a datatype constructor: "Predicate_practice.MiniMulticore.MiniMulticore_ext"
In clause
(⦇program1 = P1_, program2 = Write v_ # P2_, mem = v'_, reg = w_⦈, ⦇program1 = P1a_, program2 = P2a_, mem = va_, reg = wa_⦈) ⇒
  if w_ = wa_ ∧ P2_ = P2a_ ∧ v_ = va_ ∧ P1_ = P1a_ then Predicate.single () else bot

It seems that record is not supported at all for code_pred. Is it because record is not an inductive datatype and therefore can't be handled?
A MWE:

datatype Instruction =
      Write int
    | Read

\<comment> \<open> a mini multi-core computer
with non-determinism about which core is able to execute
\<close>

record MiniMulticore =
  program1 :: "Instruction list"
  program2 :: "Instruction list"
  mem      :: int
  reg      :: int

definition read_and_write :: MiniMulticore
  where "read_and_write = ⦇program1 = [Write 1],
                           program2 = [Read],
                           mem = 0,
                           reg = 42 ⦈"

fun differ_instruction1 ::
  "MiniMulticore ⇒ Instruction  ⇒ MiniMulticore"
  (" _  [+=i1 _] " [100, 0] 101)
  where "(C [+=i1 I] ) = C ⦇ MiniMulticore.program1 := (I # (program1 C))  ⦈"

fun differ_instruction2 ::
  "MiniMulticore ⇒ Instruction  ⇒ MiniMulticore"
  (" _  [+=i2 _] " [100, 0] 101)
  where "(C [+=i2 I] ) = C ⦇ MiniMulticore.program2 := (I # (program2 C))  ⦈"

fun differ_mem ::
    "MiniMulticore ⇒ int  ⇒ MiniMulticore"
  (" _  [ _ ]m " [100, 0] 101)
  where "(C [v]m ) = C ⦇ MiniMulticore.mem := v  ⦈"

fun differ_reg ::
    "MiniMulticore ⇒ int  ⇒ MiniMulticore"
  (" _  [ _ ]r " [100, 0] 101)
  where "(C [v]r ) = C ⦇ MiniMulticore.reg := v  ⦈"

inductive nondet_execution :: "MiniMulticore ⇒ MiniMulticore ⇒ bool"
 (infixr "↝n" 30)  where
 core2_write : "⦇program1 = P1, program2 = Write v # P2, mem = v', reg = w ⦈ ↝n ⦇program1 = P1, program2 = P2, mem = v, reg = w ⦈"
|core1_write : "C ⦇ program1 := (Write v # program1 C) ⦈ ↝n C ⦇ mem := v⦈"
(*
| core1_write : "C[+=i1 Write v] ↝n C[v]m"
| core1_read : "⟦C = C'[+=i1 Read ][v]r; reg C = v  ⟧ ⟹ C ↝n C'"
| core2_read : "⟦C = C'[+=i2 Read ][v]r; reg C = v  ⟧ ⟹ C ↝n C'"

*)

code_pred nondet_execution .
thm nondet_execution.equation

Chengsong Tan (Jun 02 2023 at 14:39):

I have sent out an email with the issue to the address cl-isabelle-users-request@lists.cam.ac.uk
but it did not show up in the daily digest, is there some rules I am missing in reporting to the Isabelle mailing list?

Wolfgang Jeltsch (Jun 02 2023 at 17:22):

Spontaneously, I guess the addresses with -request are for sending commands to the mailing list manager via e-mail. There should be a web interface for registering you as a member of this list, and then you should just send to the address with the -request removed. In any case, you should register as a member of this list, since you might not be able to post there without being a member and people might send their answers only to the list, as they expect senders being on the list and want to continue the discussion on the list (mailing lists are a bit like old-style discussion forums).

Chengsong Tan (Jun 04 2023 at 21:30):

Thank you for the answer! I think I subscribed as a digest user, which allows me to see a daily digest from that email address (with the -request suffix). I think that should be enough to report things, no? I will try sending messages again removing that -request.

Wolfgang Jeltsch (Jun 04 2023 at 23:11):

I’ve never used the digest functionality, but I’m quite sure that the address with -request is not for posting but for controlling your mailing list settings. For some reason, it seems to be used also as the sender address for digests, probably because digests are not regular mailing list e-mails.

Dustin Bryant (Jun 06 2023 at 17:01):

I wrote the following procedure:
procedure funny_count "(t_bound :: nat, max_iter :: nat)" over state
= "iter:=0;
counter:=0;
t:=0;
while iter < max_iter
inv
(iter ≤ max_iter ) ∧
(counter ≤ iter * t)

  do t:=0;
    while t < t_bound
      inv (t ≤ t_bound) ∧
          (counter ≤ t + (iter*t_bound))
      do 
        counter := counter + 1;
        t:= t + 1
      od;
    iter:=iter+1   
  od

"
And I'm trying to use the verification condition generator (VCG) tactic to verify the following:
lemma "H{True}funny_count(t_bound, max_iter){counter = t_bound*max_iter}"
proof(vcg)
oops

But the goals to show seem weird and I think I need better invariants (under inv). Also I was thinking of creating a new stream just for program verification using VCG and would appreciate some feedback on that idea as well.

Stream: General

Topic: codegen for predicates

Chengsong Tan (May 13 2023 at 21:05):

Maximilian Schaeffeler (May 15 2023 at 09:30):

Chengsong Tan (May 15 2023 at 19:30):

Chengsong Tan (May 15 2023 at 20:17):

Maximilian Schaeffeler (May 16 2023 at 08:59):

Chengsong Tan (May 18 2023 at 19:21):

Chengsong Tan (May 31 2023 at 22:30):

Mathias Fleury (Jun 01 2023 at 05:03):

Mathias Fleury (Jun 01 2023 at 05:03):

Mathias Fleury (Jun 01 2023 at 05:10):

Mathias Fleury (Jun 01 2023 at 05:10):

Chengsong Tan (Jun 01 2023 at 08:21):

Chengsong Tan (Jun 01 2023 at 08:22):

Chengsong Tan (Jun 01 2023 at 22:32):

Chengsong Tan (Jun 02 2023 at 14:39):

Wolfgang Jeltsch (Jun 02 2023 at 17:22):

Chengsong Tan (Jun 04 2023 at 21:30):

Wolfgang Jeltsch (Jun 04 2023 at 23:11):

Dustin Bryant (Jun 06 2023 at 17:01):