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()
  {
  }
}

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
  }
}

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
    }

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

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