Module 05

Crystallisation phases

Plasma -> Gas -> Liquid -> Solid -> Crystal.

Concept · grounded · RICH E4

Plasma

Crystallisation phase: intent as prose.

Worked examples

# Plasma: "We want a contract that imports the Year 10 project as a demonstrator without inheriting its safety authority."

The Plasma phase of crystallisation is unstructured intent, written as prose. Nothing is typed yet; this is the raw goal before any VSL exists.

# parser-spec.varro  (phase: plasma)
We want to parse HSC papers into a structured KG.
Open question: how do we model multi-part questions?
# ...no `type`/`action`/`workflow` declarations yet

At the Plasma phase a `.varro` file is essentially a Quarto markdown document: design thinking and rationale as prose, with no formal VSL declarations yet. Consistency is maintained by human memory and the cost of change is near zero. Crucially the file is already under version control, so the specification's history begins here. Evaluate it as the hottest, most malleable state — the same artefact that will later acquire `type` and `action` blocks, not a throwaway design doc that gets discarded once "real" specs start.

Concept · grounded · RICH E4

Gas

Crystallisation phase: formal VSL declarations.

Worked examples

system magatama.seed.year10_demonstrator { ... }

The Gas phase is the first formal condensation of prose intent into VSL declarations: systems, types, enums, workflows. It is structured but not yet property-checked.

# parser-spec.varro  (phase: gas)
## Rationale: papers decompose into parts...   <- prose persists
type QuestionPart {                            <- formal VSL emerges
  field part_id: string required
}

At the Gas phase formal VSL declarations (type/workflow/action) begin to crystallise inside the same `.varro` file, mixed with the surviving prose. It is parser-validated by `varro check vsl` but has no formal properties; the spec is queryable by agents yet not semantically complete. Evaluate the key design choice: the prose is not replaced by the VSL — documentation and specification coexist in one file, which is what eliminates doc/spec drift by construction.

# Prose: rooms can be free, held, or booked.
# Convert the prose into checked VSL declarations.

system mentormind.facilities.room_booking {
  mission "Specify a governed room-booking surface for a campus, exposing booking state as typed contracts under research authority"
  authority lane "operator:research"
  domain education
  maturity draft

  context root = "helios://local/mentormind/facilities/room-booking?view=detail&tab=contract&bind=auto"

  enum RoomState {
    value free
    value held
    value booked
  }

  type Room {
    field room_id: string required
    field capacity: integer required
    field state: RoomState required
  }

  compile booking-runtime -> varro

  action hold-room {
    risk low
    binding required
    input room_id: string required
  }

  query rooms.free {
    output Room[]
  }

  workflow reserve-room {
    inspect selection
    resolve rooms.free
    check hold-room
    render center.detail
  }

  runtime specification {
    host governed
    commit-mode host-only
  }
}

Concept · grounded · RICH E4

Liquid

Crystallisation phase: VSL + Lean-spec properties, consistency-checked.

Worked examples

# VSL + Lean-spec property: forall import. import.safety_case_ref present

The Liquid phase pairs the VSL with Lean-spec properties and checks them for consistency. The structure of Gas is now backed by stated invariants that hold together.

# parser-spec.varro  (phase: liquid)
# VSL @ checked maturity   (structure)
# Lean-spec properties     (invariants, e.g. total_marks == sum(part.marks))
# both machine-checked against each other

At the Liquid phase the VSL sits at checked maturity and is joined by authored Lean-spec properties for key invariants; an internal Lean representation of the VSL structure is consistency-checked against the `.varro` file. Authority is dual: VSL owns structure, Lean-spec owns properties. This is where the spec is most actively governed because both shape and invariants are machine-checked. Evaluate the human cost: you author properties, not proofs — the correspondence proof is generated later at Solid/Crystal.

Concept · grounded · RICH E4

Solid

Crystallisation phase: Rust generated from VSL + Lean-spec.

Worked examples

# parser-spec.varro  (phase: solid)
# Rust generated from joint VSL + Lean-spec authority.
# It compiles and passes tests; Lean proofs may contain `sorry`.

At the Solid phase Rust is generated from the joint VSL + Lean-spec authority, the compiler enforces structural consistency, and the generated code compiles and passes tests — but Lean proofs may still be partial (`sorry` permitted). The specification is executable but not yet fully proved. Critically, VSL is not deleted here: it remains the human-readable surface, and editing it triggers regeneration of the Rust. Evaluate solid as a legitimate long-term resting state: not everything needs to reach Crystal.

# parser-spec.varro  (phase: solid)
# Rust generated from joint VSL + Lean-spec authority.
# It compiles and passes tests; Lean proofs may contain `sorry`.

At the Solid phase Rust is generated from the joint VSL + Lean-spec authority, the compiler enforces structural consistency, and the generated code compiles and passes tests — but Lean proofs may still be partial (`sorry` permitted). The specification is executable but not yet fully proved. Critically, VSL is not deleted here: it remains the human-readable surface, and editing it triggers regeneration of the Rust. Evaluate solid as a legitimate long-term resting state: not everything needs to reach Crystal.

Concept · grounded · RICH E4

Crystal

Crystallisation phase: Rust fully proved against Lean-spec (zero sorry).

Worked examples

-- all obligations discharged; no `sorry` remains

The Crystal phase is the terminal state: the generated Rust is fully proved against the Lean-spec with zero `sorry`. Intent has crystallised end to end from prose to verified code.

# parser-spec.varro  (phase: crystal)
# Rust fully proved against Lean-spec; zero `sorry` in proof files.
# correspondence proof generated and checked -> mathematical certainty

Crystal is the coldest, most constrained phase: the generated Rust is fully proved against the Lean-spec with zero `sorry`, and the correspondence proof is generated and checked, yielding mathematical certainty for every stated property. As at Solid, VSL is not discarded — it remains the editable surface, and an edit triggers re-verification rather than a free-text change. Evaluate the endpoint: Crystal is certainty for stated properties only; it does not invent invariants you never wrote at Liquid.