Language Design, State Machine Mypyvy Rust

Defining a state machine:

type Element
type Log = seq<Element>

struct LogSpec {
  log: Log,
}

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

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

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

  step twostate stutter()
  {
  }
}

Crash-safe log spec:

use LogSpec;

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

statemachine CrashSafeLog {
  init predicate()
  {
    && persistent.init()
    && ephemeral == persistent
  }

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

  twostate partial_sync()
  affects ephemeral, persistent
  {
    && persistent' == ephemeral
  }

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

  step twostate crash()
  affects ephemeral
  {
    && ephemeral' == persistent
  }
}

use log_spec::Log;

struct DiskLog {
  log: Log,
  cached_superblock: CachedSuperblock,
  staged_length: nat,
}

statemachine DiskLog {
  init predicate() {
    && log == []
    && cached_superblock == CachedSuperblock::Unready
    && staged_length == 0
  }

  predicate supersedes_disk()
  {
    && cached_superblock == CachedSuperblock::Ready
    && cached_superblock.superblock.length <= |log|
  }

  // ?? disk_op is repeated for each step
  step twostate query(disk_op: DiskOp, idx: nat, result: Element)
  // affects nothing
  {
    && 0 <= idx < |log|
    && result == log[idx]
    && disk_op == DiskOp::NoDiskOp
  }

  step twostate fetch_element(disk_op: DiskOp, idx: Index, element: Element)
  affects log, staged_length // but not cached_superblock
  {
    && cached_superblock == CachedSuperblock::Ready
    && idx < cached_superblock.superblock.length
    && |log| == idx
    && disk_op == DiskOp::ReadOp(LBAType::index_to_lBA(idx), Log_sector(element))
    && log' == log + [element]
    // && cached_superblock' == cached_superblock (implied)
    && staged_length' == |log'|
  }
  
  step twostate stutter(disk_op: DiskOp)
  {
    && disk_op == DiskOp::NoDiskOp
  }

  // ?? does the implicit next need disk_op?
}

Combined state machine:

use DiskLog;
use Disk;

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

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

  step twostate machine()
  affects disk, machine
  {
    && next(disk) // invoke steps of combined state machines
    && next(machine)
  }

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

---

Alternative using :=:

  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 predicate()
    {
      && 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 next
    {
      // prove that steps preserve the invariant
    }

Refinement:

use CrashSafeLog;
use DiskLogSystem;
use LogSpec;

mod disk_log_system_refines_crash_safe_log {
  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)?
      }
    }

    on next { // prove the refinement
      match next {
        case step machine() => {
          match machine.next {
            case step query(disk_op: DiskOp, idt: nat, result: Element) => {
              // use the interpretation function to get a CrashSafeLog, and invoke the query step on the `ephemeral` state machine
              assert abstract().ephemeral.query(); 
              // use the interpretation function to get a CrashSafeLog, and invoke the `ephemeral_move` step
              assert abstract().ephemeral_move(); 
            }
            case step flush(disk_op: DiskOp) => {
              assert abstract.sync();
            }
            case step stutter(disk_op: DiskOp) => {
              assert abstract.ephemeral.stutter();
              assert abstract.ephemeral_move();
            }
          }
        }
        case step crash => {
          // ...
        }
      }
    }

  }
}

• We use a labeling mechanism to ensure that no cheating occurs on the state machine refinement (UIOp): we discussed whether we should have specialised syntax for it, and decided we should hold off to start, because we have not settled on a specific style for this yet (IronFleet and Veribetrfs are different in this regard, I believe).