Language Design, State Machine Mockup

Defining a state machine:

module LogSpec {
  type Element
  type Log = seq<Element>

  datatype Index = Index(idx: int)

  state machine Constants() Variables(log: Log)

  init(c, v)
  {
    v == Variables([])
  }

  step Query(c, v, v', idx: Index, result: Element)
  {
    && 0 <= idx.idx < |s.log|
    && result == v.log[idx.idx]
    && v' == v
  }

  step Append(c, v, v', element: Element)
  {
    && v'.log == v.log + [element]
  }

  step Stutter()
  {
    && v' == v
  }
}

Combined state machine:

include "DiskLog.dfy"
include "Disk.dfy"

module DiskLogSystem {
  import DiskLog
  import Disk

  state machine
    Constants(disk: Disk.Constants, machine: DiskLog.Constants)
    Variables(disk: Disk.Variables<DiskLog.LBAType.LBA, DiskLog.Sector>, machine: DiskLog.Variables)

  init(c, v)
  {
    && DiskLog.Mkfs(c.machine, c.disk, v.disk)
    && DiskLog.Init(c.machine, v.machine)
  }

  step Machine(c, v, v', something: Something, diskOp: DiskLog.DiskOp)
  {
    && DiskLog.Next(c.machine, v.machine, v'.machine, diskOp)
    && Disk.Next(c.disk, v.disk, v'.disk, diskOp)
  }

  step Crash(c, v, v', something: Something)
  {
    && DiskLog.Init(c.machine, v'.machine)
    && v'.disk == v.disk
  }
}

Predicates (e.g. invariants):

module DiskLogSystemInv {
  import state machine DiskLogSystem

  // ...

  predicate MemoryMatchesDisk(c, v)
  requires DiskIsValidLog(c.disk, v.disk)
  {
    forall idx: Index :: 0 <= idx.idx < |v.machine.log| && (
      || idx.idx < v.machine.stagedLength
      || IndexValidForDiskLog(c.disk, v.disk, idx)) ==> (
        && IsALogSectorBlock(v.disc.blocks, idx)
        && v.machine.log[idx.idx] == ElementFromDiskLog(c.disk, v.disk, idx)
    )
  }

  predicate Inv(c, v)
  {
    && DiskIsValidLog(c.disk, v.disk)
    && MachinePersistentWhenReadyMatchesDiskSuperblock(k, s)
    && StagedTrailsLogLength(k, s)
    && MemoryMatchesDisk(k, s)
    && LogIsZeroLengthWhenUnready(k, s)
  }

  lemma InitImpliesInv(c, v)
    on init(c, v)
    ensures Inv(c, v)
  {
  }

  lemma NextPreservesInv(c, v, v')
    requires Inv(c, s)
    on step(c, v, v')
    ensures Inv(c, v')
  {
  }

In refinement proofs:

• how to express interpretation functions?
• how to express the refinement lemma? original example

Bryan questions:

• It seems like many of the variables above don't have types. Is the expectation that they will be inferred?
  • [Andrea:] we were taking a page out of Rust's book here, where self is required syntactically but doesn't name a type; the types here are implicitly the declared types Constants and Variables (thus, they don't need to be inferred, they're just implicit)
• We had some preliminary discussion about this, but just to document it: I like Ivy's more imperative-style steps, since they make it (a) look more natural, and (b) makes it less likely that you accidentally leave all but one of the fields in the new state underspecified.

Nested updates syntax alternatives

Ivy inspired imperative update with fallback to two vocabulary formula:

r(a) := true

r := * suchthat forall X. r(X) <-> (old r(X) | X = a)

r :| r.x == old(r.x) && r.y == old(r.y) + 1

r := r' :| r'.x == r.x && r'.y == r.y + 1

Alternatives for field and nested field updates:

r.x.y := 7 ;
r.x := {y: 8, ..};

r[x.y := 7, z[a]:= 8, z[b] := 6]

r.x.y := 7;

r.z[a] := 8;
r.z[b] := 6;

z[a := 8][b := 6]

r' = r[
  x := @[
    y := 7
  ]
]

r[x := 1][x:= 2]

r.x := 7;
r.y := 8;

r.x := 7;
r.y := r.x + 1;

ML syntax:

{ r with x = { r.x with y = 5 }, z = { r.z with a = 9 }}

Rust syntax:

struct Inner {
    a: nat,
    b: nat,
}

struct State {
    x: Inner,
    y: nat,
    z: nat,
}

fn transition(before: State) -> State {
    State {
        y: before.y + 1,
        ..before
    }
}

fn transition(before: State) -> State {
    let x = before.x;
    State {
        x: Inner {
            a: x.a - 1,
            ..x
        },
        y: before.y + 1,
        ..before
    }
}