first version of full port ord_live.lean port (from ord_live.ivy) has issues

[asgeir386]

/-
 Purpose: port the Apple open-source ord_live.ivy ordering model to Veil

 The following is a test case with the features required for the (safety property part) of the model:
   1) event structure
   2) global issue time LClockType
   3) arrival clocks
   4) ordering check relation: prevents from Ken McMillans FMCAD 2016 paper

 Initially will only port the inductive invariant and safety properties, but when liveness
 properties become available in Veil will port that portion of the model too

 Location of the model in the Ivy repository:
  https://github.com/kenmcmil/ivy/blob/master/doc/examples/apple/ord_live.ivy
 Reference:
  Ken McMillan, "Toward liveness proofs at scale", CAV2024 uses this model

  CURRENT ISSUES:

  Only run with one export (plus initial state) at a time so I comment out all actions except one for
  each run and I frequently exit vscode and re-invoke (because I saw some issues when I
  didn't do that e.g. veil/lean would get stuck)

  Changed 'if-then-else' to sequence of 'if' because the 'if-then-else' part seems to have worse performance

  Didn't get match (see selectOpAck) to work with enum, i.e. this would decrease the nesting level
  compared to e.g. the let op_ack in step_north

  1. step_north
     - doesn't complete and aborts when (I think) it runs out of memory e.g. I've seen 80G in top -o cpu
     - I remember that this action on and off has caused issues in Ivy when I modified it)
  2. had a typo where perform was an action instead of procedure and with all other actions commented out
     except 'after_init' this caused an issue
     - is it legal in veil to call an action from another action?
  3. simplified min t derivation in step_south for run-time reasons
     - cvc5 and z3 support minimizing natively i.e. the minimizing construct that is used in ord_live.ivy
  4. step_if_fabric
     - inv_77 fails but no CTI is created only a WP
     - separate issue: inv_10 says that all the evs_* functions are in the initial state, for time 0, but
       the CTI ignore this part and start at time 0 i.e. violate inv_10 (not a majore issue)
  5. step_memc
     - simp` failed: maximum number of steps exceeded
  6. step_cf_fabric
     - semantic difference between veil and ivy (see comment below for step_cf_fabric)
     - get error in #gen_spec step to the effect that something can't be proven after exhaustive search

 The inductive invariants pass for step_south, dramc_step_rd and dramc_step_wr
-/
import Veil

veil module ord_live

set_option maxRecDepth 16384
set_option maxHeartbeats 10000000
set_option synthInstance.maxHeartbeats 80000

type Proc
type mem_type
type addr_type

enum OpType       = {write,read,wr_cmp,rrsp,nop}
enum mem_loc_type = {mem_loc_init,mem_memc,pio_memc}

enum op_ack_type  = {nGnRnE,nGnRE,nGRE,GRE,normal}

enum LocType      = {init_l,cf_mem_l,cf_pio_l,cf_cmp_l,if_l,memc_l,dramc_l,arm_l}

enum ph_type      = {nop_ph,wr_ph,rd_ph,cpl_ph}

/- global issue time-/
type LClockType

instantiate LClock : TotalOrderWithZero LClockType


/- mem_c arrival time-/
type        tar_clock_type

instantiate tar_clock     : TotalOrderWithZero tar_clock_type

type tar_cf_clock_type
instantiate tar_cf_clock     : TotalOrderWithZero tar_cf_clock_type

individual ltime     : LClockType                -- maximum issue time
individual lt_tar_cf : tar_cf_clock_type         -- maximum arrival time cf
function   lt_tar    : mem_type → tar_clock_type -- maximum arrival time dramc

/- break out evs fields as a workaround (for now) -/

function evs_p            : LClockType → Proc
function evs_m            : LClockType → mem_type
function evs_a            : LClockType → addr_type
function evs_req          : LClockType → OpType
function evs_cmp          : LClockType → OpType
function evs_op_ack       : LClockType → op_ack_type
function evs_mem_loc      : LClockType → mem_loc_type
function evs_l_req        : LClockType → LocType
function evs_l_cmp        : LClockType → LocType
function evs_serialized   : LClockType → Bool

function evs_lt_tar       : LClockType → tar_clock_type    -- lt when reaches target: write->wr_cmp or read->rrsp
function evs_lt_arr       : LClockType → tar_clock_type
function evs_lt_arr_cf    : LClockType → tar_cf_clock_type

relation wr  : Proc → mem_type → addr_type → LClockType → Bool
relation rd  : Proc → mem_type → addr_type → LClockType → Bool

relation rsp : Proc → mem_type → addr_type → LClockType → Bool

#gen_state
ghost relation cmp_active (T:LClockType) := evs_l_cmp T=cf_mem_l ∨ evs_l_cmp T=cf_pio_l ∨ evs_l_cmp T=cf_cmp_l  ∨ evs_l_cmp T=if_l ∨ evs_l_cmp T=memc_l ∨ evs_l_cmp T=dramc_l ∨ evs_l_cmp T=arm_l

theory ghost relation lt   (x y : LClockType) := (LClock.le x y ∧ x ≠ y)
theory ghost relation le   (x y : LClockType) := (LClock.le x y)
theory ghost relation next (x y : LClockType) := (lt x y ∧ ∀ z, lt x z → LClock.le y z)

theory ghost relation lt_arr_cf_c   (x y : tar_cf_clock_type) := (tar_cf_clock.le x y ∧ x ≠ y)
theory ghost relation le_arr_cf_c   (x y : tar_cf_clock_type) := (tar_cf_clock.le x y)
theory ghost relation arr_cf_c_next (x y : tar_cf_clock_type) := (lt_arr_cf_c x y ∧ ∀ z, lt_arr_cf_c x z → tar_cf_clock.le y z)

theory ghost relation lt_arr_c   (x y : tar_clock_type) := (tar_clock.le x y ∧ x ≠ y)
theory ghost relation le_arr_c   (x y : tar_clock_type) := (tar_clock.le x y)
theory ghost relation arr_c_next (x y : tar_clock_type) := (lt_arr_c x y ∧ ∀ z, lt_arr_c x z → tar_clock.le y z)

ghost relation pnd_or_ser_wr(P:Proc)(M:mem_type)(A:addr_type)(T:LClockType) := (wr P M A T) ∨ (evs_cmp T)=wr_cmp ∧ (evs_p T)=P ∧ (evs_m T)=M ∧ (evs_a T)=A ∧ (evs_serialized T)
ghost relation pnd_or_ser_rd(P:Proc)(M:mem_type)(A:addr_type)(T:LClockType) := (rd P M A T) ∨ (evs_cmp T)=rrsp ∧ (evs_p T)=P ∧ (evs_m T)=M ∧ (evs_a T)=A ∧ (evs_serialized T)

infix:50 "<" => lt
infix:50 "<" => lt_arr_cf_c
infix:50 "<" => lt_arr_c

infix:50 "≤" => le
infix:50 "≤" => le_arr_cf_c
infix:50 "≤" => le_arr_c

-- instance : Zero LClockType        := ⟨LClock.zero⟩
-- instance : Zero tar_clock_type    := ⟨tar_clock.zero⟩
-- instance : Zero tar_cf_clock_type := ⟨tar_cf_clock.zero⟩

ghost relation same_addr(x y : LClockType) := (evs_m x) = (evs_m y) ∧ (evs_a x) = (evs_a y)

ghost relation both_normal(T0 T1 : LClockType) := (evs_op_ack T0)=normal  ∧ (evs_op_ack T1)=normal
ghost relation both_nGnR(T0 T1 : LClockType)   := ((evs_op_ack T0)=nGnRnE ∨ (evs_op_ack T0)=nGnRE) ∧ ((evs_op_ack T1)=nGnRnE ∨ (evs_op_ack T1)=nGnRE)
ghost relation both_nGR(T0 T1 : LClockType)     := ((evs_op_ack T0)=nGRE   ∨ (evs_op_ack T0)=GRE)   ∧ ((evs_op_ack T1)=nGRE   ∨ (evs_op_ack T1)=GRE)
ghost relation nGR(OP_ACK : op_ack_type)       := (OP_ACK=nGRE    ∨ OP_ACK=GRE)
ghost relation nGnR(OP_ACK : op_ack_type)      := (OP_ACK=nGnRE   ∨ OP_ACK=nGnRnE)

ghost relation dev(T:LClockType)           := (evs_op_ack T)=nGRE ∨ (evs_op_ack T)=GRE ∨ (evs_op_ack T)=nGnRnE ∨ (evs_op_ack T)=nGnRE
ghost relation pio(T:LClockType)           := dev T ∧ (evs_mem_loc T)=pio_memc

ghost relation same_attr(x y : LClockType) := both_nGnR (x) (y) ∨ both_nGR (x) (y) ∨ both_normal (x) (y)
--


-- in the actual model the prevents has evs_p T = evs_p t (but want to bring out failure in test case)


ghost relation mem_memc_exception(T0 T1 :LClockType) := (evs_cmp T0)=rrsp ∧ (evs_cmp T1)=rrsp ∧
                                                       (evs_m T0)=(evs_m T1) ∧ (evs_a T0)=(evs_a T1) ∧ (same_attr T0 T1) ∧
                                                       (evs_mem_loc T0)=mem_memc ∧ (evs_mem_loc T1)=mem_memc

ghost relation prevents (T1 : LClockType) := (∀ T0,
                                 ((evs_req T0)≠nop ∨ (evs_cmp T0)≠nop) ∧ ((¬(evs_serialized T0) ∧ (evs_serialized T1) ∨ (evs_l_cmp T0)≠init_l ∧ (evs_l_cmp T1)=init_l)
                                     ∧ (T0<T1) ∨
                                     (evs_l_req T1)≠init_l ∧ (evs_serialized T0) ∧ (T1<T0)
                                 )
                               ∧ (evs_p T0)=(evs_p T1)
                               ∧ (evs_m T0)=(evs_m T1) ∧ (evs_a T0)=(evs_a T1) ∧ (same_attr T0 T1)
                               ∧ ¬(mem_memc_exception T0 T1))

-- ghost relation prevents(t : LClockType) := ∀ T, lt LClock.zero t ∧ (lt T ltime → ¬ (evs_l_req T = dramc_l ∧ lt t T))

after_init {
  ltime            := LClock.zero       -- maximum issue time
  lt_tar_cf        := tar_cf_clock.zero
  lt_tar M         := tar_clock.zero

  wr P M A T       := false
  rd P M A T       := false
  rsp P M A T      := false

  evs_req T        := nop
  evs_cmp T        := nop
  evs_op_ack T     := normal
  evs_serialized T := true
  evs_l_req T      := init_l
  evs_l_cmp T      := init_l
  evs_mem_loc T    := mem_loc_init

  evs_lt_arr T     := tar_clock.zero
  evs_lt_tar T     := tar_clock.zero
  evs_lt_arr_cf T  := tar_cf_clock.zero
}

procedure succ (n : LClockType) {
   let k :| next n k
   return k
}

procedure succ_lt_arr_cf (n : tar_cf_clock_type) {
   let k :| arr_cf_c_next n k
   return k
}

procedure succ_lt_arr (n : tar_clock_type) {
   let k :| arr_c_next n k
   return k
}

procedure perform_grd (t:LClockType)  {
-- update the global memory state

  let m := (evs_m t)

  let next_lt_tar_m ← succ_lt_arr (lt_tar m)
  -- assert ¬ (evs_serialized t)

  if (evs_req t)=read then
    evs_l_req t     := init_l

    evs_req t       := nop

    evs_cmp t       := rrsp

    lt_tar (evs_m t) := next_lt_tar_m
    evs_lt_tar t     :=  lt_tar (evs_m t)

  if (evs_req t)=write then
-- serialize at current global time
    evs_serialized t := true

    evs_l_req t      := init_l

    evs_cmp t        := wr_cmp
    evs_req t        := nop

    lt_tar (evs_m t) := next_lt_tar_m
    evs_lt_tar t     := lt_tar (evs_m t)

  }
-- forward messages to dramc and keep them in order
-----------------------------------------------------------------------------------

--
-------------------------------------------------------------------------------------

action dramc_step_rd(m:mem_type) {
  let t :| (evs_l_req t = dramc_l) ∧ ∀ p a tt, ((rd p m a tt ∧ evs_req tt=read ∨ wr p m a tt ∧ evs_req tt=write) ∧ (evs_l_req tt) = dramc_l) → ((evs_lt_arr t)<(evs_lt_arr tt) ∨ t=tt)

  let ordpip := (evs_req t)=write

  if (evs_l_req t)=dramc_l ∧ ¬ordpip then
    rsp (evs_p t) (evs_m t) (evs_a t) t := true

    perform_grd t

    -- assert ¬ prevents t

    evs_l_cmp t := memc_l
  }

/-
action dramc_step_wr(m:mem_type) {
  let t :| (evs_l_req t=dramc_l) ∧ ∀ p a tt, ((rd p m a tt ∧ evs_req tt=read ∨ wr p m a tt ∧ evs_req tt=write) ∧ (evs_l_req tt)=dramc_l) → ((evs_lt_arr t)<(evs_lt_arr tt) ∨ t=tt)

  let ordpip := (evs_req t)=read

  if (evs_l_req t)=dramc_l ∧ ¬ordpip then
    perform_grd t

    evs_l_cmp t := memc_l

    assert ¬ prevents t
  }
-/
-- create new requests
-----------------------------------------------------------------------------

procedure create (p : Proc)(m : mem_type)(a : addr_type)(req : OpType)(l_req : LocType)(op_ack:op_ack_type)(mem_loc:mem_loc_type) {
  evs_p       ltime    := p
  evs_m       ltime    := m
  evs_a       ltime    := a
  evs_req     ltime    := req
  evs_l_req   ltime    := l_req
  evs_op_ack  ltime    := op_ack
  evs_mem_loc ltime    := mem_loc

  evs_lt_arr_cf ltime  := tar_cf_clock.zero

  evs_serialized ltime := false
}


/-
def selectOpAck (mem_loc : mem_loc_type) (choose : op_ack_type) : op_ack_type :=
    match mem_loc, choose with
    | mem_memc,GRE                  => GRE
    | mem_memc,nGRE                 => nGRE
    | mem_memc,normal               => normal
    | mem_memc, _                   => normal
    | _, _                          => choose
-/

/-
action step_north (ph : ph_type)(p : Proc)(m : mem_type)(a : addr_type)(choose_op_ack : op_ack_type)(mem_loc_arg : mem_loc_type) {
  let next_ltime ← succ ltime
  -- determine next arrival time larger than arr_mem_c_max
  let next_arr_cf ←  succ_lt_arr_cf lt_tar_cf
--  let OrdPip := ∃ T, (evs_l_req T = cf_mem_l ∧ evs_p T = evs_p t) ∧ lt T t

  let dram_new := true
  let pio_new  := false

  let wr_new   := ph=wr_ph
  let rd_new   := ph=rd_ph

  let devb     := false

 -- let t :| (evs_req t=read ∨ evs_req t=write ∨ evs_cmp t=rrsp ∨ evs_cmp t=wr_cmp) ∧ evs_m t=m ∧ evs_a t=a

  let t :| ∃ P, wr P m a t ∨ rd P m a t

  let op_ack :=
    if (evs_req t=read ∨ evs_req t=write ∨ evs_cmp t=rrsp ∨ evs_cmp t=wr_cmp) ∧ evs_m t=m ∧ evs_a t=a then
      if evs_mem_loc t=mem_memc then
        if choose_op_ack=normal ∨ choose_op_ack=GRE ∨ choose_op_ack=nGRE then
          choose_op_ack
        else
          normal  -- pick one
      else
        if choose_op_ack=nGnRnE ∨ choose_op_ack=nGnRE ∨ choose_op_ack=GRE ∨ choose_op_ack=nGRE then
          choose_op_ack
        else
          nGnRnE
    else
      normal

  let mem_loc_arg := if mem_loc_arg=mem_memc then mem_memc else pio_memc

  let mem_loc :=
    if (evs_req t=read ∨ evs_req t=write ∨ evs_cmp t=rrsp ∨ evs_cmp t=wr_cmp) ∧ evs_m t=m ∧ evs_a t=a then
      evs_mem_loc t
    else
      if op_ack=normal then
        mem_memc
      else
        if op_ack=nGnRnE ∨ op_ack=nGnRE then
          pio_memc
        else
          mem_loc_arg

--  let op_ack :=
--    if ((evs_req t)=read ∨ (evs_req t)=write ∨ (evs_cmp t)=rrsp ∨ (evs_cmp t)=wr_cmp) ∧ (evs_m t)=m ∧ (evs_a t)=a then
--      selectOpAck (evs_mem_loc t) choose_op_ack
--    else
--      normal
--  let ordser_wr := false
  let ordser_wr :=  ∃ M A T, wr_new ∧ devb ∧ nGnR op_ack ∧ wr p M A T  ∧ (evs_req T=write ∨ evs_cmp T=wr_cmp  ∧ cmp_active T)  ∧ dev T  ∧ nGnR (evs_op_ack T)  ∧ pio_new ∧ ¬(M=m ∧ A=a) ∨
                             wr_new ∧ devb ∧ nGnR op_ack ∧ rd p M A T ∧ (evs_req T=read ∨ evs_cmp T=rrsp ∧ cmp_active T) ∧ dev T ∧ nGnR (evs_op_ack T) ∨
                             wr_new ∧ devb ∧ nGnR op_ack ∧ rd p M A T ∧ (evs_req T=read ∨ evs_cmp T=rrsp ∧ cmp_active T) ∧ dev T ∧ nGR (evs_op_ack T) ∨
                             wr_new ∧ devb ∧ nGR op_ack  ∧ rd p M A T ∧ (evs_req T=read ∨ evs_cmp T=rrsp ∧ cmp_active T) ∧ dev T ∧ nGnR (evs_op_ack T) ∨
                             wr_new ∧ devb ∧ nGR op_ack  ∧ rd p M A T ∧ (evs_req T=read ∨ evs_cmp T=rrsp ∧ cmp_active T) ∧ dev T ∧ nGR (evs_op_ack T) ∨
                             wr_new ∧ ¬devb ∧ wr p m a T ∧ (evs_req T=write ∨ evs_cmp T=wr_cmp ∧ cmp_active T) ∧ ¬(dev T) ∧ dram_new ∨
                             wr_new ∧ ¬devb ∧ wr p m a T ∧ (evs_req T=write ∨ evs_cmp T=wr_cmp ∧ cmp_active T) ∧ ¬(dev T) ∧ pio_new ∨
                             wr_new ∧ ¬devb ∧ rd p M A T ∧ (evs_req T=read ∨ evs_cmp T=rrsp ∧ cmp_active T) ∧ ¬(dev T)

  let ordser_rd := ∃ M A T, rd_new ∧ devb ∧ nGnR op_ack ∧ wr p M A T ∧ (evs_req T=write ∨ evs_cmp T=wr_cmp ∧ cmp_active T) ∧ dev T ∧ nGnR (evs_op_ack T) ∧ dram_new ∨
                            rd_new ∧ devb ∧ nGnR op_ack ∧ wr p M A T ∧ (evs_req T=write ∨ evs_cmp T=wr_cmp ∧ cmp_active T) ∧ dev T ∧ nGnR (evs_op_ack T) ∧ pio_new ∨
                            rd_new ∧ devb ∧ nGnR op_ack ∧ rd p M A T ∧ (evs_req T=read ∨ evs_cmp T=rrsp ∧ cmp_active T) ∧ dev T ∧ nGnR (evs_op_ack T) ∧ pio_new ∧ ¬(M=m ∧ A=a) ∨
                            rd_new ∧ devb ∧ nGR op_ack ∧ wr p m a T ∧ (evs_req T=write ∨ evs_cmp T=wr_cmp ∧ cmp_active T) ∧ dev T ∧ nGR (evs_op_ack T) ∧ dram_new ∨
                            rd_new ∧ devb ∧ nGR op_ack ∧ wr p m a T ∧ (evs_req T=write ∨ evs_cmp T=wr_cmp ∧ cmp_active T) ∧ dev T ∧ nGR (evs_op_ack T) ∧ pio_new ∨
                            rd_new ∧ ¬devb ∧ wr p m a T ∧ (evs_req T=write ∨ evs_cmp T=wr_cmp ∧ cmp_active T) ∧ ¬(dev T) ∧ dram_new ∨
                            rd_new ∧ ¬devb ∧ wr p m a T ∧ (evs_req T=write ∨ evs_cmp T=wr_cmp ∧ cmp_active T) ∧ ¬(dev T) ∧ pio_new ∨
                            rd_new ∧ ¬devb ∧ rd p m a T ∧ (evs_req T=read ∨ evs_cmp T=rrsp ∧ cmp_active T) ∧ ¬(dev T) ∧ dram_new ∨
                            rd_new ∧ ¬devb ∧ rd p m a T ∧ (evs_req T=read ∨ evs_cmp T=rrsp ∧ cmp_active T) ∧ ¬(dev T) ∧ pio_new

  if wr_new ∧ ¬ordser_wr ∧ mem_loc=mem_memc then
    ltime := next_ltime -- increment max issue time

    create p m a write cf_mem_l op_ack mem_loc

    wr p m a ltime := true

  if wr_new ∧ ¬ordser_wr ∧ mem_loc=pio_memc then
      ltime := next_ltime -- increment max issue time

      create p m a write cf_pio_l op_ack mem_loc

      wr p m a ltime := true

  if rd_new ∧ ¬ordser_rd ∧ mem_loc=mem_memc then
    ltime := next_ltime -- increment max issue time

    create p m a read cf_mem_l op_ack mem_loc

    lt_tar_cf           := next_arr_cf
    evs_lt_arr_cf ltime := next_arr_cf

    rd p m a ltime := true

  if rd_new ∧ ¬ordser_rd ∧ mem_loc=pio_memc then
      ltime := next_ltime -- increment max issue time

      create p m a read cf_pio_l op_ack mem_loc

      wr p m a ltime := true
}
-/
/-
  XXX when procedure is replaced with action bad things happen
  - comment out all other actions, and then only the initial state check remains, but the build doesn't complete
    in reasonable time
-/
procedure perform (t:LClockType) {
-- update the global memory state
  if evs_cmp t=rrsp then
      -- serialize at current global time
      evs_serialized t := true

  evs_l_cmp  t := init_l
}
/-
action step_south (ph:ph_type)(pp:Proc) {

  /- XXX this is code corresponding to ord_live.ivy but didn't work, or at least took a long time so re-wrote it with equivalent expression -/
  -- let t :| evs_l_cmp t≠init_l ∧ evs_p t=pp ∧ (evs_cmp t=wr_cmp ∨ evs_cmp t=rrsp) ∧ ∀ tt, evs_p tt=pp ∧ (evs_cmp tt=wr_cmp ∨ evs_cmp tt=rrsp) ∧ evs_l_cmp tt≠init_l → (lt t tt ∨ t=tt)

  let t :| ¬evs_serialized t ∧ evs_p t=pp ∧ ∀ tt, ¬evs_serialized tt ∧ evs_p tt=pp → (lt t tt ∨ tt=t)

  let m := evs_m t
  let a := evs_a t

  if ph=cpl_ph ∧ evs_l_cmp t=arm_l ∧ evs_cmp t=rrsp then
    perform t

    assert ¬ prevents t

    rsp pp m a t  := false
    rd  pp m a t  := false

  if ph=cpl_ph ∧ evs_l_cmp t=arm_l ∧ evs_cmp t=wr_cmp then
    perform t

    assert ¬ prevents t

    wr pp m a t    := false

}
-/
-- forward messages to memc and keep messages from same arm instance in-order
--------------------------------------------------------------------------------------
-- 1) uncomment tcmp argument, 2) comment out let for cmp and tcmp
/-
action step_cf_fabric (ph:ph_type)(sel_memc:Bool) { -- (tcmp : LClockType) {

  let min_rd_mem :| (evs_l_req min_rd_mem=cf_mem_l) ∧  sel_memc ∧ ∀ t, evs_req t=read  ∧ evs_l_req t=cf_mem_l   → (lt_arr_cf_c (evs_lt_arr_cf min_rd_mem) (evs_lt_arr_cf t) ∨ min_rd_mem=t)
  let min_rd_pio :| (evs_l_req min_rd_pio=cf_pio_l) ∧ ¬sel_memc ∧ ∀ t, (evs_req t=read  ∧ evs_l_req t=cf_pio_l) → (lt min_rd_pio t ∨ min_rd_pio=t)

  let min_wr_mem :| (evs_l_req min_wr_mem=cf_mem_l) ∧  sel_memc ∧ ∀ t, (evs_req t=write ∧ evs_l_req t=cf_mem_l) → (lt min_wr_mem t ∨ min_wr_mem=t)
  let min_wr_pio :| (evs_l_req min_wr_pio=cf_pio_l) ∧ ¬sel_memc ∧ ∀ t, (evs_req t=write ∧ evs_l_req t=cf_pio_l) → (lt min_wr_pio t ∨ min_wr_pio=t)

  let new_rd  := ph=rd_ph ∧ (sel_memc ∧ evs_l_req min_rd_mem=cf_mem_l ∨ ¬ sel_memc ∧ evs_l_req min_rd_pio=cf_pio_l)
  let new_wr  := ph=wr_ph ∧ (sel_memc ∧ evs_l_req min_wr_mem=cf_mem_l ∨ ¬ sel_memc ∧ evs_l_req min_wr_pio=cf_pio_l)

  let t :=
    if ph=wr_ph then
      if sel_memc then
        min_wr_mem
      else
        min_wr_pio
    else
      if sel_memc then
        min_rd_mem
      else
        min_rd_pio

  let p    := evs_p t

  /- the following two lines are redundant compared to ivy model i.e. including tcmp as an argument in
     action is sufficient -/
  let cmp  := ph=cpl_ph ∧ ∃ tcmp, (evs_cmp tcmp=rrsp ∨ evs_cmp tcmp=wr_cmp) ∧ evs_l_cmp tcmp=cf_cmp_l
  let tcmp :| ∃ tcmp, (evs_cmp tcmp=rrsp ∨ evs_cmp tcmp=wr_cmp) ∧ evs_l_cmp tcmp=cf_cmp_l

  let ordpip0 := new_rd ∧ ∃ M A T, rd p M A T ∧ evs_req T=read  ∧ (evs_l_req T=cf_mem_l ∨ evs_l_req T=cf_pio_l) ∧ evs_mem_loc t=evs_mem_loc T ∧ evs_mem_loc t=mem_memc ∧ lt_arr_cf_c (evs_lt_arr_cf T) (evs_lt_arr_cf t)
  let ordpip1 := new_wr ∧ ∃ M A T, wr p M A T ∧ evs_req T=write ∧ (evs_l_req T=cf_mem_l ∨ evs_l_req T=cf_pio_l) ∧ evs_mem_loc t=evs_mem_loc T ∧ evs_mem_loc t=mem_memc ∧ lt T t
  let ordpip2 := new_rd ∧ ∃ M A T, rd p M A T ∧ evs_req T=read  ∧ (evs_l_req T=cf_mem_l ∨ evs_l_req T=cf_pio_l) ∧ evs_mem_loc t=evs_mem_loc T ∧ evs_mem_loc t=pio_memc ∧ lt T t
  let ordpip3 := new_wr ∧ ∃ M A T, wr p M A T ∧ evs_req T=write ∧ (evs_l_req T=cf_mem_l ∨ evs_l_req T=cf_pio_l) ∧ evs_mem_loc t=evs_mem_loc T ∧ evs_mem_loc t=pio_memc ∧ lt T t

  let ordpip := ordpip0 ∨ ordpip1 ∨ ordpip2 ∨ ordpip3

  if (new_rd ∨ new_wr) ∧ ¬ ordpip ∧ evs_mem_loc t=mem_memc then
    evs_l_req t := memc_l

  if (new_rd ∨ new_wr) ∧ ¬ ordpip ∧ evs_mem_loc t=pio_memc then
    evs_l_req t := if_l

  if cmp then
    evs_l_cmp tcmp := arm_l

}
-/
-- if switching fabric (rudimentary)
--------------------------------------------------------------------------------------

/- XXX inv_77 fails but no CTI is created only a WP -/
/-
action step_if_fabric (ph:ph_type)(m:mem_type)(a:addr_type)(p:Proc)(tcmp:LClockType) {

  let min_rd_issue :| (evs_l_req min_rd_issue=if_l) ∧ ∀ t, (evs_req t=read  ∧ evs_l_req t=if_l) → (lt min_rd_issue t ∨ min_rd_issue = t)
  let min_wr_issue :| (evs_l_req min_wr_issue=if_l) ∧ ∀ t, (evs_req t=write ∧ evs_l_req t=if_l) → (lt min_wr_issue t ∨ min_wr_issue = t)

  let new_rd  := ph=rd_ph ∧ evs_l_req min_rd_issue=if_l
  let new_wr  := ph=wr_ph ∧ evs_l_req min_wr_issue=if_l

  let t       := if ph=wr_ph then min_wr_issue else min_rd_issue

  let cmp     := ph=cpl_ph ∧ evs_l_cmp tcmp=if_l

  let ordpip0 := new_rd ∧ ∃ M A T, rd p M A T ∧ evs_req T=read  ∧ evs_l_req T=if_l ∧ lt T t -- processed
  let ordpip1 := new_wr ∧ ∃ M A T, wr p M A T ∧ evs_req T=write ∧ evs_l_req T=if_l ∧ lt T t -- processed

  let ordpip := ordpip0 ∨ ordpip1

  if (new_rd ∨ new_wr) ∧ ¬ ordpip  ∧ (evs_mem_loc t=mem_memc ∨ evs_mem_loc t=pio_memc) then
      evs_l_req t := memc_l

  if cmp then
    evs_l_cmp tcmp := cf_cmp_l

}
-/

/- XXX `simp` failed: maximum number of steps exceeded -/
/-
action step_memc(ph:ph_type)(p:Proc)(m:mem_type)(a:addr_type)(tcmp:LClockType) {

let next_arr_c ←  succ_lt_arr (lt_tar m)


let rd_bp := ∃ T, evs_req T=read ∧ evs_m T=m ∧ evs_a T=a ∧ evs_l_req T=dramc_l
let wr_bp := ∃ T, evs_req T=write ∧ evs_m T=m ∧ evs_a T=a ∧ evs_l_req T=dramc_l

let t_rd :| (evs_l_req t_rd=memc_l) ∧ ∀ p t, evs_l_req t=memc_l ∧ rd p m a t → (lt t_rd t ∨ t_rd=t)
let t_wr :| (evs_l_req t_wr=memc_l) ∧ ∀ p t, evs_l_req t=memc_l ∧ wr p m a t → (lt t_wr t ∨ t_wr=t)

if ph=rd_ph ∧ evs_l_req t_rd=memc_l ∧ evs_mem_loc t_rd=mem_memc ∧ ¬ rd_bp then
  evs_l_req t_rd   := dramc_l

  lt_tar m         := next_arr_c
  evs_lt_arr t_rd  := next_arr_c

if ph=wr_ph ∧ evs_l_req t_wr=memc_l ∧ evs_mem_loc t_wr=mem_memc ∧ ¬ wr_bp then
  evs_l_req t_wr   := dramc_l

  lt_tar m         := next_arr_c
  evs_lt_arr t_wr  := next_arr_c

if ph=rd_ph ∧ evs_l_req t_rd=memc_l ∧ evs_mem_loc t_rd=pio_memc then

  rsp (evs_p t_rd) (evs_m t_rd) (evs_a t_rd) t_rd  := true

  perform_grd t_rd

  evs_l_cmp t_rd := memc_l

  assert ¬ prevents t_rd

if ph=wr_ph ∧ evs_l_req t_wr=memc_l ∧ evs_mem_loc t_wr=pio_memc then

  perform_grd t_wr

  evs_l_cmp t_wr := memc_l

  assert ¬ prevents t_wr

if ph=cpl_ph ∧ evs_l_cmp tcmp=memc_l ∧ (evs_cmp tcmp=rrsp ∨ evs_cmp tcmp=wr_cmp) ∧ evs_mem_loc tcmp=mem_memc then
  evs_l_cmp tcmp := cf_cmp_l

if ph=cpl_ph ∧ evs_l_cmp tcmp=memc_l ∧ (evs_cmp tcmp=rrsp ∨ evs_cmp tcmp=wr_cmp) ∧ evs_mem_loc tcmp=pio_memc then
  evs_l_cmp tcmp := if_l

}
-/

invariant [only_write] ((evs_req T)=nop ∨ (evs_req T)=write)

----
invariant [inv_0] (evs_req T)=read ∧ (evs_l_req T)=cf_mem_l ∧ (evs_mem_loc T)=mem_memc ∧ T=ltime -> (evs_lt_arr_cf T)=lt_tar_cf

invariant [inv_1] (evs_req T)=read ∧ (evs_l_req T)=cf_mem_l ∧ (evs_mem_loc T)=mem_memc -> evs_lt_arr_cf T ≠ tar_cf_clock.zero
invariant [inv_2] (evs_req T)=read ∧ (evs_l_req T)=cf_mem_l ∧ (evs_mem_loc T)=mem_memc -> (evs_lt_arr_cf T)≤lt_tar_cf

invariant [inv_3] (evs_cmp T)=rrsp ∧ (evs_mem_loc T)=mem_memc -> (evs_lt_arr_cf T)≤lt_tar_cf

invariant [inv_4] (evs_lt_arr_cf T) ≤ lt_tar_cf

invariant [inv_5] (
           (evs_req T0)=read ∧ (evs_l_req T0)=cf_mem_l ∧ (evs_mem_loc T0)=mem_memc ∧
           (evs_req T1)=read ∧ (evs_l_req T1)=cf_mem_l ∧ (evs_mem_loc T1)=mem_memc ∧
           T0<T1
          )
          ->
          (evs_lt_arr_cf T0)<(evs_lt_arr_cf T1)
----

invariant [inv_6] (ltime=T ∧ ¬(T=LClock.zero)) -> ¬((evs_req T)=nop ∧ (evs_cmp T)=nop)

invariant [inv_7] (ltime<T ∨ T=LClock.zero) -> (evs_lt_arr T)=tar_clock.zero ∧ (evs_lt_arr_cf T)=tar_cf_clock.zero
invariant [inv_8] ltime=LClock.zero         -> lt_tar_cf=tar_cf_clock.zero

invariant [inv_9] ((evs_req T)=nop ∧ (evs_cmp T)=nop ∨ (evs_req T)=write ∨  (evs_cmp T)=wr_cmp ∨ ((evs_req T)=read ∨ (evs_cmp T)=rrsp) ∧ ¬((evs_mem_loc T)=mem_memc))
           ->
           (evs_lt_arr_cf T)=tar_cf_clock.zero

invariant [inv_10] (evs_req LClock.zero)=nop ∧ (evs_l_req LClock.zero)=init_l ∧ (evs_cmp LClock.zero)=nop ∧ (evs_l_cmp LClock.zero)=init_l ∧ (evs_lt_arr LClock.zero)=tar_clock.zero ∧ (evs_lt_arr_cf LClock.zero)=tar_cf_clock.zero

invariant [inv_11] ((evs_req T)=write ∨ (evs_req T)=read ∨ (evs_cmp T)=wr_cmp ∨ (evs_cmp T)=rrsp) ∧ (evs_mem_loc T)=pio_memc
           ->
          (evs_lt_arr T)=tar_clock.zero

invariant [inv_12] ((evs_req T)=write ∨ (evs_req T)=read) ∧ (evs_m T)=M ∧ (evs_a T)=A ∧ (evs_l_req T)=dramc_l
           ->
            ¬((evs_lt_arr T)=tar_clock.zero)

invariant [inv_13] ((evs_req T)=write ∨ (evs_req T)=read) ∧ (evs_m T)=M ∧ (evs_a T)=A ∧ ¬((evs_l_req T)=dramc_l)
           ->
           (evs_lt_arr T)=tar_clock.zero

invariant [inv_14] (evs_req T)=read  -> (evs_l_cmp T)=init_l
invariant [inv_15] (evs_req T)=write -> (evs_l_cmp T)=init_l

invariant [inv_16]  (evs_req T)=nop -> (evs_l_req T)=init_l

invariant [inv_17] ((evs_req T)=read ∨ (evs_req T)=write ∨ (evs_req T)=nop)
invariant [inv_18] ((evs_cmp T)=rrsp ∨ (evs_cmp T)=wr_cmp ∨ (evs_cmp T)=nop)

invariant [inv_19] (evs_req T)≠nop -> (evs_cmp T)=nop
invariant [inv_20] (evs_cmp T)≠nop -> (evs_req T)=nop

invariant [inv_21] (∀ P M A, ¬((wr P M A T) ∨ (rd P M A T))) -> ((evs_l_req T)=init_l ∧ (evs_l_cmp T)=init_l)

invariant [inv_22] (((evs_req T)=write ∨ (evs_req T)=read) ∧ (evs_mem_loc T)=mem_memc ∧ (evs_l_req T)=dramc_l)
           ->
           ¬((lt_tar (evs_m T))<(evs_lt_arr T))

invariant [inv_23] (((evs_cmp T)=wr_cmp ∨ (evs_cmp T)=rrsp) ∧ (evs_mem_loc T)=mem_memc)
           ->
           (evs_lt_arr T)<(evs_lt_tar T)

invariant [inv_24] (
            ((evs_req T0)=write ∧ (evs_l_req T0)=dramc_l ∨ (evs_req T0)=read ∧ (evs_l_req T0)=dramc_l) ∧ (evs_mem_loc T0)=mem_memc ∧
            ((evs_cmp T1)=wr_cmp ∨ (evs_cmp T1)=rrsp) ∧ (evs_mem_loc T1)=mem_memc ∧ (evs_l_cmp T1)=dramc_l ∧
            (evs_m T0)=(evs_m T1) ∧
            T0≠T1
           )
           ->
           ((evs_lt_arr T0)≠(evs_lt_tar T1) ∧ (evs_lt_arr T0)≠(evs_lt_arr T1))

invariant [inv_25] (
            ((evs_req T0)=write ∧ (evs_l_req T0)=dramc_l ∨ (evs_cmp T0)=wr_cmp ∨ (evs_req T0)=read ∧ (evs_l_req T0)=dramc_l ∨ (evs_cmp T0)=rrsp) ∧ (evs_mem_loc T0)=mem_memc ∧
            ((evs_req T1)=write ∧ (evs_l_req T1)=dramc_l ∨ (evs_cmp T1)=wr_cmp ∧ (evs_l_cmp T1)=dramc_l ∨ (evs_req T1)=read ∧ (evs_l_req T1)=dramc_l ∨ (evs_cmp T1)=rrsp ∧ (evs_l_cmp T1)=dramc_l) ∧ (evs_mem_loc T1)=mem_memc ∧
            (evs_m T0)=(evs_m T1) ∧
            T0≠T1
           )
           ->
           (
            (evs_lt_arr T0)≠(evs_lt_arr T1) ∧
            (((evs_cmp T0)=wr_cmp ∨ (evs_cmp T0)=rrsp) -> (evs_lt_tar T0)≠(evs_lt_arr T1)) ∧
            (((evs_cmp T1)=wr_cmp ∨ (evs_cmp T1)=rrsp) -> (evs_lt_arr T0)≠(evs_lt_tar T1))
           )

invariant [inv_26] (
            ((evs_cmp T0)=wr_cmp ∨ (evs_cmp T0)=rrsp) ∧ (evs_mem_loc T0)=mem_memc ∧
            ((evs_cmp T1)=wr_cmp ∨ (evs_cmp T1)=rrsp) ∧ (evs_mem_loc T1)=mem_memc ∧
            (evs_m T0)=(evs_m T1) ∧
            T0≠T1
           )
           ->
           ((evs_lt_arr T0)≠(evs_lt_arr T1) ∧ (evs_lt_tar T0)≠(evs_lt_tar T1))

invariant [inv_27] ¬(
            (evs_req T0)=write ∧ (evs_cmp T1)=rrsp ∧
            (evs_mem_loc T0)=mem_memc ∧ (evs_mem_loc T1)=mem_memc ∧
            (evs_m T0)=(evs_m T1) ∧
            (evs_a T0)=(evs_a T1) ∧
            (evs_l_req T0)=dramc_l ∧
            ((evs_lt_arr T0)<(evs_lt_arr T1))
            )

invariant [inv_28] (
            (evs_req T0)=read ∧ (evs_cmp T1)=rrsp ∧
            (evs_p T0)=(evs_p T1) ∧
            (evs_mem_loc T0)=mem_memc ∧ (evs_mem_loc T1)=mem_memc ∧
            (evs_m T0)=(evs_m T1) ∧
            (evs_a T0)=(evs_a T1) ∧
            (same_attr T0 T1) ∧
            T0<T1
            )
            ->
            ((evs_lt_arr T0)<(evs_lt_arr T1))

-- No RR or WW to same address in mem_memc from arm (normal)
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

invariant [inv_29] ¬(
            ((evs_req T0)=read ∧ (evs_req T1)=read ∨ (evs_req T0)=write ∧ (evs_req T1)=write) ∧
            (evs_op_ack T0)=normal ∧
            (evs_p T0)=(evs_p T1) ∧
            (evs_mem_loc T0)=mem_memc ∧ (evs_mem_loc T1)=mem_memc ∧
            (evs_m T0)=(evs_m T1) ∧
            (evs_a T0)=(evs_a T1) ∧
            (same_attr T0 T1) ∧
            T0<T1
            )

-- RR and WW to same address in mem_memc stay in order
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

invariant [inv_30] (
            ((evs_req T0)=write ∧ (evs_req T1)=write ∨ (evs_req T0)=read ∧ (evs_req T1)=read) ∧
            (evs_mem_loc T0)=mem_memc ∧ (evs_mem_loc T1)=mem_memc ∧
            (evs_p T0)=(evs_p T1) ∧
            (evs_m T0)=(evs_m T1) ∧
            (evs_a T0)=(evs_a T1) ∧
            (evs_l_req T0)=dramc_l ∧ (evs_l_req T1)=dramc_l ∧
            (same_attr T0 T1) ∧
            T0<T1
           )
           ->
           (
            ((evs_lt_arr T0)<(evs_lt_arr T1))
           )

invariant [inv_31] ((evs_cmp T)=wr_cmp ∨ (evs_cmp T)=rrsp) -> ¬((lt_tar (evs_m T))<(evs_lt_tar T))

invariant [inv_32] (
            ((evs_cmp T0)=wr_cmp ∨ (evs_cmp T0)=rrsp) ∧
            ((evs_cmp T1)=wr_cmp ∨ (evs_cmp T1)=rrsp) ∧
            (evs_m T0)=(evs_m T1) ∧
            T0≠T1
           )
           ->
           ((evs_lt_tar T0)≠(evs_lt_tar T1))

invariant [inv_33] (
            (evs_cmp T0)=wr_cmp ∧ (evs_cmp T1)=rrsp ∧
            (evs_p T0)=(evs_p T1) ∧
            (evs_m T0)=(evs_m T1) ∧
            (evs_a T0)=(evs_a T1) ∧
            (same_attr T0 T1) ∧
            T0<T1
           )
           ->
           (
            ((evs_lt_tar T0) < (evs_lt_tar T1))
           )

invariant [inv_34] (
             (evs_req T0)=read ∧ (evs_req T1)=read ∧
             (evs_p T0)=(evs_p T1) ∧
             (evs_mem_loc T0)=pio_memc ∧ (evs_mem_loc T1)=pio_memc ∧
             (evs_m T0)=(evs_m T1) ∧
             (evs_a T0)=(evs_a T1) ∧
             (same_attr T0 T1) ∧
             T0<T1
           )
           ->
           (
            (evs_l_req T0)=cf_pio_l       ∧ ((evs_l_req T1)=cf_pio_l) ∨
            (evs_l_req T0)=if_l       ∧ ((evs_l_req T1)=if_l  ∨ (evs_l_req T1)=cf_pio_l) ∨
            (evs_l_req T0)=memc_l      ∧ ((evs_l_req T1)=memc_l ∨ (evs_l_req T1)=if_l ∨ (evs_l_req T1)=cf_pio_l)
           )

invariant [inv_35] (((evs_cmp T)=wr_cmp ∨ (evs_cmp T)=rrsp) ∧ (evs_serialized T))
           ->
           (
            (evs_mem_loc T)=mem_memc ∨
            (evs_mem_loc T)=pio_memc
           )
--
----------------------------------------------------------------------------------------------------------------------------------------------------------------

invariant [inv_36] (evs_req T)=write -> ¬(evs_serialized T)
invariant [inv_37] (evs_req T)=read  -> ¬(evs_serialized T)

invariant [inv_38] ((evs_req T)=nop   ∧ (evs_cmp T)=wr_cmp) -> (evs_serialized T)

invariant [inv_39] (evs_serialized T) -> ((evs_req T)=nop ∨ (evs_cmp T)=nop ∨ (evs_cmp T)=rrsp ∨ (evs_cmp T)=wr_cmp)

invariant [inv_40] (((evs_cmp T)=wr_cmp ∨ (evs_cmp T)=rrsp))
           ->
           (
            ((evs_cmp T)=wr_cmp ∨ (evs_cmp T)=rrsp ∧ ¬(evs_serialized T)) ∧ (
            (evs_mem_loc T)=mem_memc ∧ ((evs_l_cmp T)=dramc_l ∨ (evs_l_cmp T)=memc_l ∨ (evs_l_cmp T)=cf_cmp_l ∨ (evs_l_cmp T)=arm_l) ∨
            (evs_mem_loc T)=pio_memc ∧ ((evs_l_cmp T)=memc_l ∨ (evs_l_cmp T)=if_l ∨ (evs_l_cmp T)=cf_cmp_l ∨ (evs_l_cmp T)=arm_l)
            ) ∨

            (evs_serialized T) ∧ ((evs_cmp T)=rrsp ∨ (evs_cmp T)=wr_cmp) ∧ (evs_l_cmp T)=init_l
           )

invariant [inv_41] (((evs_req T)=write ∨ (evs_req T)=read))
           ->
           (
            (evs_mem_loc T)=mem_memc ∧ ((evs_l_req T)=dramc_l ∨ (evs_l_req T)=memc_l ∨ (evs_l_req T)=cf_mem_l) ∨
            (evs_mem_loc T)=pio_memc ∧ ((evs_l_req T)=memc_l ∨ (evs_l_req T)=if_l ∨ (evs_l_req T)=cf_pio_l)
           )

invariant [inv_42] ¬(
            ((evs_req T0)=write ∧ (evs_cmp T1)=wr_cmp ∧ (evs_l_cmp T1)=init_l ∨ ((evs_req T0)=read ∨ (evs_cmp T0)=rrsp) ∧ (evs_cmp T1)=rrsp) ∧
            ¬(evs_serialized T0) ∧ (evs_serialized T1) ∧
            (evs_p T0)=(evs_p T1) ∧
            (evs_m T0)=(evs_m T1) ∧
            (evs_a T0)=(evs_a T1) ∧
            (same_attr T0 T1) ∧
            T0<T1
           )

invariant [inv_43] ¬(evs_serialized T) -> ¬((evs_mem_loc T)=mem_loc_init)

-- initialized to mem_loc_init, but once used has same mapping for all agents

invariant [inv_44] ((evs_req T)=nop ∧ (evs_cmp T)=nop) -> (evs_mem_loc T)=mem_loc_init

invariant [inv_45] (((evs_req T0)≠nop ∨ (evs_cmp T0)≠nop) ∧ ((evs_req T1)≠nop ∨ (evs_cmp T1)≠nop) ∧ (evs_m T0)=(evs_m T1) ∧ (evs_a T0)=(evs_a T1))
           ->
           (
            (evs_mem_loc T0)=(evs_mem_loc T1)
           )

invariant [inv_46] (((evs_req T0)≠nop ∨ (evs_cmp T0)≠nop) ∧ ((evs_req T1)≠nop ∨ (evs_cmp T1)≠nop) ∧ (evs_m T0)=(evs_m T1) ∧ (evs_a T0)=(evs_a T1))
           ->
           (
            (evs_mem_loc T0)=mem_memc ∨ (evs_mem_loc T0)=pio_memc
           )

invariant [inv_47] (((evs_req T)≠nop ∨ (evs_cmp T)≠nop) ∧ ¬(dev T)) -> (evs_op_ack T)=normal

invariant [inv_48] (((evs_req T)≠nop ∨ (evs_cmp T)≠nop) ∧ (dev T)) -> (((evs_op_ack T)=nGnRE ∨ (evs_op_ack T)=nGnRnE) ∨ ((evs_op_ack T)=GRE ∨ (evs_op_ack T)=nGRE))

invariant [inv_49] ¬(
             (evs_req T0)=read ∧ ((evs_req T1)=read ∨ (evs_cmp T1)=rrsp) ∧ ¬(evs_serialized T0) ∧ ¬(evs_serialized T1) ∧
             (evs_p T0)=(evs_p T1) ∧
             (evs_mem_loc T0)=mem_memc ∧ (evs_mem_loc T1)=mem_memc ∧
             (evs_m T0)=(evs_m T1) ∧ (evs_a T0)=(evs_a T1) ∧
             (both_normal T0 T1) ∧
             T0<T1
           )

invariant [inv_50] ((evs_req T)=nop ∨ (evs_cmp T)=nop ∨ (evs_req T)=write ∨ (evs_cmp T)=wr_cmp ∨ (evs_req T)=read ∨ (evs_cmp T)=rrsp)

invariant [inv_51] (wr P M A T)  -> T≠LClock.zero
invariant [inv_52] (rd P M A T)  -> T≠LClock.zero

invariant [inv_53] (evs_mem_loc T)=pio_memc -> (dev T)

invariant [inv_54] (((wr P M A T) ∨ (rd P M A T)) ∧ (dev T)) -> (((evs_op_ack T)=nGRE ∨ (evs_op_ack T)=GRE) ∨ ((evs_op_ack T)=nGnRnE ∨ (evs_op_ack T)=nGnRE))
invariant [inv_55] (((wr P M A T) ∨ (rd P M A T)) ∧ ¬(dev T)) -> (evs_op_ack T)=normal

invariant [inv_56] ¬((pnd_or_ser_wr P M1 A1 T1) ∧ (rd P M0 A0 T0) ∧ (same_attr T0 T1) ∧ M0=M1 ∧ A0=A1 ∧ T0<T1)

invariant [inv_57] ¬((pnd_or_ser_rd P M1 A1 T1) ∧ (wr P M0 A0 T0) ∧ T0<T1 ∧  (dev T0) ∧  (dev T1) ∧ (both_nGnR T0 T1))

invariant [inv_58] ¬((pnd_or_ser_rd P M1 A1 T1) ∧ (wr P M0 A0 T0) ∧ T0<T1 ∧  (dev T0) ∧  (dev T1) ∧ (both_nGR T0 T1) ∧ (same_addr T0 T1))

-- Never >1 to Normal to/from same address

invariant [inv_59] ¬((pnd_or_ser_rd P M A T1) ∧ (rd P M A T0) ∧ T0<T1 ∧ ¬(dev T0) ∧ ¬(dev T1))
invariant [inv_60] ¬((pnd_or_ser_rd P M A T1) ∧ (wr P M A T0) ∧ T0<T1 ∧ ¬(dev T0) ∧ ¬(dev T1))
invariant [inv_61] ¬((pnd_or_ser_wr P M A T1) ∧ (rd P M A T0) ∧ T0<T1 ∧ ¬(dev T0) ∧ ¬(dev T1))
invariant [inv_62] ¬((pnd_or_ser_wr P M A T1) ∧ (wr P M A T0) ∧ T0<T1 ∧ ¬(dev T0) ∧ ¬(dev T1))

----------------------------------------------------------------------------------------------------------------------------------------------------------------
-- SECTION: ref
--
-- lt keeps track of the largest value of the logical time value. Starts at
--        value 0 and is then incremented when each write/read is issued
--

invariant [inv_63] (T=LClock.zero ∨ ltime<T) -> ((evs_req T)=nop ∧ (evs_cmp T)=nop ∧ (evs_serialized T))

invariant [inv_64] (wr P M A T)
           <->
           (((evs_req T)=write ∧ ¬(evs_serialized T) ∨ (evs_cmp T)=wr_cmp ∧ (evs_l_cmp T)≠init_l ∧ (evs_serialized T)) ∧ (evs_p T)=P ∧ (evs_m T)=M ∧ (evs_a T)=A)

------

invariant [inv_65] ((rd P M A T) ∧ ¬(rsp P M A T))
           <->
           ((evs_req T)=read ∧ ¬(evs_serialized T) ∧ (evs_p T)=P ∧ (evs_m T)=M ∧ (evs_a T)=A)

invariant [inv_66] ((rd P M A T) ∧ (rsp P M A T))
           <->
           ((evs_cmp T)=rrsp ∧ ¬(evs_serialized T) ∧ (evs_p T)=P ∧ (evs_m T)=M ∧ (evs_a T)=A)

invariant [inv_67] (evs_req T)=read ->  ¬(evs_serialized T)

------

invariant [inv_68] ((evs_cmp T)=rrsp ∧ ¬(evs_serialized T)) -> (evs_l_cmp T) ≠ dramc_l

----------------------------------------------------------------------------------------------------------------------------------------------------------------
-- SECTION: arm

invariant [inv_69] (((evs_req T)=read ∨ (evs_cmp T)=rrsp) ∧ (dev T))  -> ((evs_op_ack T)=nGnRnE ∨ (evs_op_ack T)=nGnRE ∨ (evs_op_ack T)=nGRE ∨ (evs_op_ack T)=GRE)
invariant [inv_70] (((evs_req T)=read ∨ (evs_cmp T)=rrsp) ∧ ¬(dev T)) -> (evs_op_ack T)=normal

invariant [inv_71] (((evs_req T)=write ∨ (evs_cmp T)=wr_cmp) ∧ (dev T)) -> ((evs_op_ack T)=nGnRnE ∨ (evs_op_ack T)=nGnRE ∨ (evs_op_ack T)=nGRE ∨ (evs_op_ack T)=GRE)
invariant [inv_72] (((evs_req T)=write ∨ (evs_cmp T)=wr_cmp) ∧ ¬(dev T)) -> (evs_op_ack T)=normal

-- PIO writes (to same address) can be pipelined and stay in order

invariant [inv_73] (
            ((evs_req T0)=write ∨ (evs_cmp T0)=wr_cmp) ∧
            ((evs_req T1)=write ∨ (evs_cmp T1)=wr_cmp) ∧
            (evs_p T0)=(evs_p T1) ∧
            (evs_m T0)=(evs_m T1) ∧
            (evs_a T0)=(evs_a T1) ∧
            (same_attr T0 T1) ∧
            T0<T1
           )
           ->
           ¬((evs_serialized T1) ∧ ¬(evs_serialized T0))

invariant [inv_74] (
            ((evs_req T0)=write ∧ (evs_req T1)=write ∨ (evs_req T0)=read ∧ (evs_req T1)=read) ∧
            ¬(evs_serialized T0) ∧
            (evs_p T0)=(evs_p T1) ∧
            (evs_m T0)=(evs_m T1) ∧
            (evs_a T0)=(evs_a T1) ∧
            (evs_mem_loc T0)=mem_memc ∧ (evs_mem_loc T1)=mem_memc ∧
            T0<T1
           )
           ->
           (
            (evs_l_req T0)=cf_mem_l  ∧ (evs_l_req T1)=cf_mem_l   ∨
            (evs_l_req T0)=memc_l ∧ ((evs_l_req T1)=memc_l ∨ (evs_l_req T1)=cf_mem_l) ∨
            (evs_l_req T0)=dramc_l  ∧ ((evs_l_req T1)=dramc_l  ∨ (evs_l_req T1)=memc_l ∨ (evs_l_req T1)=cf_mem_l)
           )

invariant [inv_75] ¬(
            (((evs_req T0)=read ∨ (evs_cmp T0)=rrsp) ∧ ((evs_req T1)=write ∨ (evs_cmp T1)=wr_cmp)) ∧
            ¬(evs_serialized T0) ∧
            (evs_p T0)=(evs_p T1) ∧
            (evs_m T0)=(evs_m T1) ∧
            (evs_a T0)=(evs_a T1) ∧
            (evs_mem_loc T0)=pio_memc ∧ (evs_mem_loc T1)=pio_memc ∧
            T0<T1
           )

invariant [inv_76] ¬(
            ((evs_req T0)=write ∧ ((evs_req T1)=read ∨ (evs_cmp T1)=rrsp)) ∧
            (evs_p T0)=(evs_p T1) ∧
            (evs_m T0)=(evs_m T1) ∧
            (evs_a T0)=(evs_a T1) ∧
            (evs_mem_loc T0)=pio_memc ∧ (evs_mem_loc T1)=pio_memc ∧
            (same_attr T0 T1) ∧
            T0<T1
           )

invariant [inv_77] (
            ((evs_req T0)=write ∧ (evs_req T1)=write ∨ (evs_req T0)=read ∧ (evs_req T1)=read) ∧
            (evs_p T0)=(evs_p T1) ∧
            (evs_m T0)=(evs_m T1) ∧
            (evs_a T0)=(evs_a T1) ∧
            (evs_mem_loc T0)=pio_memc ∧ (evs_mem_loc T1)=pio_memc ∧
            T0<T1
           )
           ->
           (
            (evs_l_req T0)=cf_pio_l  ∧ (evs_l_req T1)=cf_pio_l ∨
            (evs_l_req T0)=if_l  ∧ ((evs_l_req T1)=if_l ∨ (evs_l_req T1)=cf_pio_l) ∨
            (evs_l_req T0)=memc_l ∧ ((evs_l_req T1)=memc_l ∨ (evs_l_req T1)=if_l ∨ (evs_l_req T1)=cf_pio_l)
           )

----------------------------------------------------------------------------------------------------------------------------------------------------------------
-- dramc_mod
--

invariant [inv_78] ((evs_req T0)=write ∧ (evs_l_req T0)=dramc_l ∧ (evs_req T1)=write ∧ (evs_l_req T1)=dramc_l ∧ (evs_m T0)=(evs_m T1) ∧ (evs_a T0)=(evs_a T1)) -> T0=T1
invariant [inv_79] ((evs_req T0)=read  ∧ (evs_l_req T0)=dramc_l ∧ (evs_req T1)=read ∧ (evs_l_req T1)=dramc_l ∧ (evs_m T0)=(evs_m T1) ∧ (evs_a T0)=(evs_a T1)) -> T0=T1

------

--RAR

invariant [inv_80] (
            (evs_req T0)=read ∧ ¬(evs_serialized T0) ∧
            (evs_req T1)=read ∧
            (evs_p T0)=(evs_p T1) ∧
            (evs_mem_loc T0)=mem_memc ∧ (evs_mem_loc T1)=mem_memc ∧
            (evs_m T0)=(evs_m T1) ∧
            (evs_a T0)=(evs_a T1) ∧
            T0<T1
           )
           ->
           (
            (evs_req T1)=read ∧ (evs_l_req T1)=cf_mem_l  ∧ (evs_req T0)=read ∧ ((evs_l_req T0)=cf_mem_l ∨ (evs_l_req T0)=memc_l ∨ (evs_l_req T0)=dramc_l) ∨
            (evs_req T1)=read ∧ (evs_l_req T1)=memc_l ∧ (evs_req T0)=read ∧ ((evs_l_req T0)=memc_l ∨ (evs_l_req T0)=dramc_l) ∨
            (evs_req T1)=read ∧ (evs_l_req T1)=dramc_l  ∧ (evs_req T0)=read ∧ (evs_l_req T0)=dramc_l
           )

--WAW
invariant [inv_81] (
            (evs_req T0)=write ∧ ¬(evs_serialized T0) ∧
            (evs_req T1)=write ∧
            (evs_p T0)=(evs_p T1) ∧
            (evs_mem_loc T0)=mem_memc ∧ (evs_mem_loc T1)=mem_memc ∧
            (evs_m T0)=(evs_m T1) ∧
            (evs_a T0)=(evs_a T1) ∧
            T0<T1
           )
           ->
           (
            (evs_l_req T0)=cf_mem_l  ∧ (evs_l_req T1)=cf_mem_l ∨
            (evs_l_req T0)=memc_l ∧ ((evs_l_req T1)=memc_l ∨ (evs_l_req T1)=cf_mem_l) ∨
            (evs_l_req T0)=dramc_l  ∧ ((evs_l_req T1)=dramc_l  ∨ (evs_l_req T1)=memc_l ∨ (evs_l_req T1)=cf_mem_l)
           )
--RAR
invariant [inv_82] (
            (evs_req T0)=read ∧ ¬(evs_serialized T0) ∧
            (evs_cmp T1)=rrsp ∧
            (evs_p T0)=(evs_p T1) ∧
            (evs_mem_loc T0)=mem_memc ∧ (evs_mem_loc T1)=mem_memc ∧
            (evs_m T0)=(evs_m T1) ∧
            (evs_a T0)=(evs_a T1) ∧
            (same_attr T0 T1) ∧
            T0<T1
           )
           ->
           (
            (evs_l_req T0)=dramc_l ∧ ((evs_l_cmp T1)=dramc_l ∨ (evs_l_cmp T1)=memc_l ∨ (evs_l_cmp T1)=cf_mem_l ∨ (evs_l_cmp T1)=arm_l)
           )

--RAR/WAW

-- RR to mem_memc is OrdSer for arm
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

invariant [inv_83] ¬(
             (evs_req T0)=read ∧ (evs_cmp T1)=rrsp ∧
             (evs_p T0)=(evs_p T1) ∧
             (evs_m T0)=(evs_m T1) ∧ (evs_a T0)=(evs_a T1) ∧
             (same_attr T0 T1) ∧
             T0<T1
           )

-- WW to same address stay in order, and therefore can't have wr_cmp for younger before older
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

invariant [inv_84] ¬(
             (evs_req T0)=write ∧ (evs_cmp T0)=nop ∧ (evs_req T1)=nop ∧ (evs_cmp T1)=wr_cmp ∧
             (evs_p T0)=(evs_p T1) ∧
             (evs_m T0)=(evs_m T1) ∧ (evs_a T0)=(evs_a T1) ∧
             (same_attr T0 T1) ∧
             T0<T1
           )

invariant [inv_85] (
            ((evs_req T0)=read ∨ (evs_cmp T0)=rrsp) ∧ (pio T0) ∧
            ((evs_req T1)=read ∨ (evs_cmp T1)=rrsp) ∧ (pio T1) ∧
             (evs_m T0)=(evs_m T1) ∧ (evs_a T0)=(evs_a T1) ∧
             (evs_p T0)=(evs_p T1) ∧
             (same_attr T0 T1) ∧
             T0<T1
           )
           ->
           ¬(¬(evs_serialized T0) ∧ (evs_serialized T1))

invariant [inv_86] (
            ((evs_req T0)=read ∨ (evs_cmp T0)=rrsp) ∧
            ((evs_req T1)=read ∨ (evs_cmp T1)=rrsp) ∧
             (evs_m T0)=(evs_m T1) ∧ (evs_a T0)=(evs_a T1) ∧
             (evs_p T0)=(evs_p T1) ∧
             (same_attr T0 T1) ∧
             T0<T1
           )
           ->
           ¬(¬(evs_serialized T0) ∧ (evs_serialized T1))

#time #gen_spec
--
-- #model_check { LClockType := Fin 5,Proc := Fin 3, tar_clock_type := Fin 3, tar_cf_clock_type := Fin 3, mem_type := Fin 1, addr_type := Fin 1}{ }

#check_invariants

end ord_live

[asgeir386]

Some improvement to report

ord_live-0.2.txt (attached)

1. Instead of assigning to true or false put in the correct expressions for the following
   and moved them to be after the derivation of mem_loc and op_ack

   let dram_new := mem_loc=mem_memc
   let pio_new := mem_loc=pio_memc
   let devb := op_ack=nGnRnE ∨ op_ack=nGnRE ∨ op_ack=GRE ∨ op_ack=nGRE

2. simp timeout in #gen_spec

   doubled the MaxHeartBeats to 20000000

   now made it through #gen_spec

   aborted in #check_invariants step i.e. top -o cpu reached 80G in the memory column lean process
   (with about 700 %CPU) dissapeared

ord_live-0.3.txt (attached)

1. add back in the if-then-else and refactor

   could not put the wr p m a ltime and rd p m a ltime because lean/veil said syntax pattern
   didn't match (seems to be a parsing bug)

2. moved the assignments into create to get past syntax issue

   made it to #gen_spec

   memory image 120G apparently became too large

--
changed the extension to .txt to be able to upload

ord_live-0.2.txt

ord_live-0.3.txt

[dranov]

Thank you, @asgeir386.

This is by far the largest specification we've seen and we've had issues with simp on much smaller specifications. We'll dedicate some time next week to investigate this thoroughly and see if there's some other problem happening, but simp performance is likely the culprit.

For what it's worth, our colleague @volodeyka is working with the Lean FRO to improve performance of simplification specifically for verifiers via a new SymM monad (e.g. leanprover/lean4#12100 and leanprover/lean4#12101). Preliminary results show an order of magnitude improvement.

This is a priority both for us and for the Lean FRO — they want to make verifiers embedded in Lean as performant as possible. We're planning to integrate this SymM work into Veil as soon as it's ready.

I'll give you an update towards an end of next week.

[dranov]

@zqy1018

Here's the profile for a single VC here. Almost all of the time is spent in instantiateMVars, which I believe is due to this line in the discharger (VCDischarger.fromTerm):

let witness ← instantiateMVars $ ← withSynthesize (postpone := .no) $
              withoutErrToSorry $ elabTermEnsuringType term (← vcStatement.type)

[Elab.async] [159.063357] elaborating proof of ord_live.dramc_step_rd_only_write ▼
  [definition.value] [157.211683] ord_live.dramc_step_rd_only_write ▼
    [step] [14.265870] veil_solve_wp ▼
      [] [14.265842] veil_solve_wp ▼
        [] [14.131217] veil_solve_wp ▼
          [veil.perf.tactic] [14.130572] veil_solve_wp ▼
            [Elab.step] [14.130491] veil_intros;
                  veil_wp;
                  veil_concretize_wp;
                  veil_fol;
                  veil_smt ▼
              [] [0.024983] veil_intros ▶
              [] [0.123407] veil_wp ▶
              [] [6.297589] veil_concretize_wp ▶
              [] [3.217090] veil_fol ▶
              [] [4.467348] veil_smt ▼
                [veil.perf.tactic] [4.467246] veil_smt ▶
    [Meta.instantiateMVars] [142.590576] fun m th st h => ...

@volodeyka mentioned that @nomeata rewrote instantiateMVars in Lean: leanprover/lean4#12233

The previous implementation had quadratic complexity when instantiating expressions with long chains of nested delayed-assigned MVars. Such chains arise naturally from repeated intro/apply tactic sequences, where each step creates a new delayed assignment wrapping the previous one. The new two-pass approach resolves the entire chain in a single traversal with a fused fvar substitution, reducing this to linear complexity.

Hopefully this solves the issue for us.

[dranov]

@asgeir386 I've had the time to look into this and it appears that it might be a performance issue in Lean itself, which has been recently fixed. The fix is still only on the Lean nightly branch, but we'll try it to see if it solves the performance problems you're facing.

[nomeata]

If it helps I can create a throw-away PR that backports that change to your version of lean, so that you can test if it solves the issue. Or you switch to nightlies, of course.

[dranov]

If it helps I can create a throw-away PR that backports that change to your version of lean, so that you can test if it solves the issue.

@nomeata That would be very helpful. Thank you so much! We are currently on v4.27.0 for the veil-2.0-preview branch.

(Otherwise we'd have to change our upstream dependencies, lean-cvc5 and lean-smt to nightly as well, which would be a hassle.)

[nomeata]

I created leanprover/lean4#13060, a throw-away PR that backports the instantiateMVars rewrite to v4.27.0.

You can test it by setting your lean-toolchain to:

leanprover/lean4-pr-releases:pr-release-13060

(This toolchain will be available once the PR's CI builds the release artifact, which may take a bit.)

Let me know if it helps with the performance issue!

[nomeata]

Ok, seems like the toolchain is available now.

[dranov]

@nomeata I can confirm that this fixes the issue (instantiateMVars execution time went down from 142.5s to 3.5s). Thank you very much!

[Elab.async] [18.043582] elaborating proof of ord_live.dramc_step_rd_only_write ▼
  [definition.value] [15.832849] ord_live.dramc_step_rd_only_write ▼
    [step] [11.929376] veil_solve_wp ▶
    [Meta.instantiateMVars] [3.574259] fun m th st h =>

[dranov]

To be more precise, this reduces the elaboration time if the theorem is written directly in the buffer. In reality, we run it in a Command.wrapAsyncAsSnapshot, like this:

let witness ← instantiateMVars $ ← withSynthesize (postpone := .no) $
  withoutErrToSorry $ elabTermEnsuringType term (← vcStatement.type)
if witness.hasMVar || witness.hasFVar || witness.hasSyntheticSorry then
  throwError "unsolved goals"

That still seems to be very slow, especially when multiple tasks run in parallel, but that might be a different issue. I need to investigate more. (This is almost certainly an issue in Veil at this stage, not one in Lean.)

VCStatement.type also relies on instantiateMVars:

def VCStatement.type (vc : VCStatement) : TermElabM Expr := do
  Term.elabBinders vc.params fun vs => do
  let body ← withSynthesize (postpone := .no) $
    withoutErrToSorry $ elabTerm vc.statement (Expr.sort levelZero)
  let typ ← Meta.mkForallFVars vs body >>= instantiateMVars
  if typ.hasMVar || typ.hasFVar || typ.hasSorry then
    throwError "VCStatement.type: {vc.name}'s type is not fully determined"
  return typ

@nomeata, does anything seem wrong with this, performance-wise? I'll do more profiling later to try to understand what's going on.

[dranov]

@nomeata Is there any reason your new implementation of instantiateMVars would work less efficiently in Command.wrapAsyncAsSnapshot?

I don't get a profile for it using set_option trace.profiler true, but wrapping it manually in a trace node, like this:

let expr ←
  withTraceNode (`veil.perf.elaborateProof ++ dischargerId.name) (fun _ => return s!"elaborating discharger {dischargerId.name}") $
  withSynthesize (postpone := .no) $ withoutErrToSorry $ elabTermEnsuringType term (← vcStatement.type)
let witness ← (
  withTraceNode (`veil.perf.instantiateMVars ++ dischargerId.name) (fun _ => return s!"instantiating MVars for discharger {dischargerId.name}") $
    instantiateMVars expr)

Gives this output, which suggests instantiateMVars takes about ~4x longer than what we get just elaborating the theorem in the main editor buffer:

[Elab.async] [27.240076] Veil.VCDischarger.fromTerm ▼
  [veil.perf.discharger.dramc_step_rd_only_write_0_WP] [27.239187] discharger dramc_step_rd_only_write_0_WP ▼
    [Elab.step] [0.012318] expected type: Type, term DecidableEq.{1} Proc 
    [elaborateProof.dramc_step_rd_only_write_0_WP] [12.662884] elaborating discharger dramc_step_rd_only_write_0_WP ▶
    [instantiateMVars.dramc_step_rd_only_write_0_WP] [14.195902] instantiating MVars for discharger dramc_step_rd_only_write_0_WP 

The relevant code is in VCDischarger.fromTerm.

[nomeata]

Hmm, it may be slow to run instantiateMVars too early, before all MVars are assigned. But the withSynthesize should take care of that, so I'm not sure. Maybe this is an independent issue that's just the next bottleneck after the plain instantiateMVars issue? No concrete idea though from afar.