Language Design, State Machine Mypyvy Rust

Defining a state machine:

type Element
type Log = seq<Element>

struct Index {
  qidx: int,
}

struct LogSpec {
  log: Log,
}

statemachine LogSpec {
  init // acts as a function `LogSpec -> bool`
  {
    log == []
  }

  step query(idx: Index, result: Element) // acts as a function `(LogSpec, LogSpec) -> bool`
  // no "affects" = no state changes
  {
    && 0 <= idx.idx < |log|
    && result == log[idx.idx]
  }

  step append(element: Element)
  affects log
  {
    && log' == log + [element]
  }

  step stutter()
  {
  }
}

Crash-safe log spec:

use LogSpec;

struct CrashSafeLog {
  persistent: LogSpec,
  ephemeral: LogSpec, // two "copies" of the same state machine (state)
}

statemachine CrashSafeLog {
  init
  {
    && persistent.init
    && ephemeral == persistent
  }

  step ephemeral_move
  affects ephemeral
  {
    // persistent' == persistent (implied)
    && ephemeral.next
  }

  step sync
  affects persistent
  {
    && persistent' == ephemeral
    // ephemeral' == ephemeral (implied)
  }

  step crash
  affects ephemeral
  {
    && ephemeral' == persistent
  }
}

Combined state machine:

use DiskLog;
use Disk;

struct DiskLogSystem {
  disk: Disk<DiskLog.LBAType.LBA, DiskLog.Sector>,
  machine: DiskLog,
}

statemachine DiskLogSystem {
  init
  {
    && machine.mkfs(disk)
    && machine.init
  }

  step machine(diskOp: DiskLog.DiskOp)
  affects disk, machine
  {
    && disk.next // invoke steps of combined state machines
    && machine.next
  }

  step crash()
  affects machine
  {
    && machine'.init
  }
}

Alternative to affects:

  step sync
  {
    && x > 0  // precondition
    && x := x - 1 // update
    && y := * // havoc, means we're modifying y
    && y' > x' // two-vocabulary assumptions about modified symbols
    && a.b := 5 // nested update, change only a.b, but leave other fields of a intact
    && a.arr[5] := 6 // nested array update
    && z' = z + 1 // syntax error, only way to make z' available is to use z := ...
  }
  // questions: how do these compose? what about if-then-else, disjunctions, aliasing, etc

Predicates (e.g. invariants):

mod disk_log_system_inv {
  with statemachine DiskLogSystem {

    // ...

    predicate memory_matches_disk
    requires disk.disk_is_valid_log
    {
      forall idx: Index :: 0 <= idx.idx < |machine.log| && (
        || idx.idx < machine.stagedLength
        || disk.index_valid_for_disk_log(idx)) ==> (
          && disk.is_a_log_sector_block(idx)
          && machine.log[idx.idx] == disk.element_from_disk_log(idx)
      )
    }

    inv
    {
      && disk.disk_is_valid_log
      && machine_persistent_when_ready_matches_disk_superblock
      && staged_trails_log_length
      && memory_matches_disk
      && log_is_zero_length_when_unready
      // ?? what if I need to refer to "this" (DiskLogSystem), e.g. to pass it as a parameter?
    }

    inv on init
    {
      // prove that init produces a state that satisfies the invariant
    }

    inv on crash
    {
      // prove that the `crash` step preserves the invariant
    }

Refinement:

use CrashSafeLog;
use DiskLogSystem;
use LogSpec;

refine DiskLogSystem from CrashSafeLog {

  // ...

  pure fn abstract_disk(disk: DiskLog) -> LogSpec {
    let log = if disk.is_valid_log {
      extract_disk_prefix(disk, disk.blocks[DiskLog::SuperblockLBA].superblock.length)
    } else {
      []
    };

    LogSpec { log }
  }

  pure fn abstract_ephemeral(sys: DiskLogSystem) -> LogSpec {
    if sys.machine.supersedes_disk {
      LogSpec { log: sys.machine.log }
    } else {
      interpret_disk(sys.disk)
    }
  }

  abstract // function DiskLogSystem -> CrashSafeLog (interpretation function)
  {
    CrashSafeLog {
      persistent: abstract_disk(disk),
      persistent: abstract_ephemeral(this), // ??: how to refer to "this" (DiskLogSystem)?
    }
  }

  step query { // prove the refinement of the `query` step in DiskLogSystem
    assert abstract.ephemeral.query; // use the interpretation function to get a CrashSafeLog, and invoke the query step on the `ephemeral` state machine
    assert abstract.ephemeral_move; // use the interpretation function to get a CrashSafeLog, and invoke the `ephemeral_move` step
  }

  step flush { // prove the refinement of the `query` step in DiskLogSystem
    assert abstract.sync;
  }

  step stutter {
    assert abstract.ephemeral.stutter;
    assert abstract.ephemeral_move;
  }

}