Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/metareflection/dafny-replay/llms.txt

Use this file to discover all available pages before exploring further.

ColorWheel generates five-color HSL palettes that satisfy mood-based saturation/lightness bounds and harmony-based hue patterns. The invariant is maintained by a Normalize function that falls back to Custom mood or harmony when a user adjustment would otherwise violate the constraints. The app also demonstrates a deliberate separation between spec and proof to prevent LLM-generated proofs from silently weakening the specification.

​
Domain model

datatype Color = Color(h: int, s: int, l: int)

datatype Mood =
  | Vibrant      // S ≥ 70,  40 ≤ L ≤ 60
  | SoftMuted    // 20 ≤ S ≤ 45, 55 ≤ L ≤ 75
  | Pastel       // S ≤ 35,  L ≥ 75
  | DeepJewel    // S ≥ 60,  25 ≤ L ≤ 45
  | Earth        // 15 ≤ S ≤ 40, 30 ≤ L ≤ 60
  | Neon         // S ≥ 90,  50 ≤ L ≤ 65
  | Custom       // No S/L constraints

datatype Harmony =
  | Complementary    // [H₀, H₀+180°] + 3 variations
  | Triadic          // [H₀, H₀+120°, H₀+240°] + 2 variations
  | Analogous        // [H₀-30°, H₀-15°, H₀, H₀+15°, H₀+30°]
  | SplitComplement  // [H₀, H₀+150°, H₀+210°] + 2 variations
  | Square           // [H₀, H₀+90°, H₀+180°, H₀+270°] + 1 variation
  | Custom           // No hue relationship

datatype Model = Model(
  baseHue: int,          // 0–359, anchor for harmony calculations
  mood: Mood,
  harmony: Harmony,
  colors: seq<Color>,    // always exactly 5 HSL colors
  contrastPair: (int, int),
  adjustmentH: int,
  adjustmentS: int,
  adjustmentL: int
)

​
Key invariants

The invariant is defined in ColorWheelSpec.dfy: 
predicate Inv(m: Model) {
  && ValidBaseHue(m.baseHue)          // 0 ≤ baseHue < 360
  && |m.colors| == 5
  && (forall i | 0 <= i < 5 :: ValidColor(m.colors[i]))
  && 0 <= m.contrastPair.0 < 5
  && 0 <= m.contrastPair.1 < 5
  // Mood Satisfaction: non-Custom mood implies all colors satisfy S/L bounds
  && (m.mood != Mood.Custom ==>
        forall i | 0 <= i < 5 :: ColorSatisfiesMood(m.colors[i], m.mood))
  // Harmony Coherence: non-Custom harmony implies hues follow the pattern
  && HuesMatchHarmony(m.colors, m.baseHue, m.harmony)
}
Mood Satisfaction — if the current mood is not Custom, every color’s saturation and lightness must fall within that mood’s bounds. For example, Vibrant requires S ≥ 70 and 40 ≤ L ≤ 60. Harmony Coherence — if the current harmony is not Custom, the five hues must match the pattern computed from baseHue. Complementary produces hues at H₀ and H₀+180° plus three spread variations; Analogous produces five hues evenly spaced around H₀. Graceful Degradation — when an adjustment (AdjustColor, AdjustPalette, SetColorDirect) would break either constraint, the model transitions to Custom mood or Custom harmony instead of failing. This is the graceful degradation property: the palette always remains valid.

​
Normalize repairs any violation

Apply can produce intermediate states that violate the invariant (for example, a palette palette with hues that no longer match the active harmony). Normalize repairs these by falling back to Custom: 
function Normalize(m: Model): Model {
  // ...clamp colors and baseHue...
  var finalMood :=
    if m.mood == Mood.Custom then Mood.Custom
    else if AllColorsSatisfyMood(normalizedColors, m.mood) then m.mood
    else Mood.Custom;

  var finalHarmony :=
    if m.harmony == Harmony.Custom then Harmony.Custom
    else if HuesMatchHarmony(normalizedColors, normalizedBaseHue, m.harmony) then m.harmony
    else Harmony.Custom;

  m.(baseHue := normalizedBaseHue, colors := normalizedColors,
     mood := finalMood, harmony := finalHarmony, ...)
}

​
Spec/proof separation

The ColorWheel domain splits its Dafny code across two files:
  • ColorWheelSpec.dfy — user-facing types, predicates, and the Apply function. This file defines what the invariant is and what the actions do. It is kept separate so that an LLM assisting with proofs cannot quietly modify the spec to make proofs easier.
  • ColorWheelProof.dfy — all lemmas, including InitSatisfiesInv and StepPreservesInv.
The PROVED.md file in the colorwheel/ directory records exactly what has been formally verified and what has been shipped without verification.
When using an LLM to help write Dafny proofs, keeping the spec in a separate file prevents the model from making silent changes to predicates in order to satisfy proof obligations. Any spec change requires explicit human review.

​
Actions

ActionDescription
GeneratePaletteGenerate a fresh five-color palette from a base hue, mood, harmony, and ten random seeds
AdjustColorIndependently adjust one color’s H/S/L; auto-transitions to Custom if constraints break
AdjustPaletteShift all colors together (linked mode); auto-transitions to Custom mood if bounds break
RegenerateMoodReplace S/L values to satisfy a new mood while keeping existing hues
RegenerateHarmonyReplace hues to satisfy a new harmony while keeping existing S/L values
RandomizeBaseHuePick a new base hue and regenerate the full palette
SetColorDirectSet one color to an exact value; preserves mood/harmony if possible

​
Running the app

cd colorwheel
npm install
npm run dev

Replay kernel

ColorWheel uses the Replay kernel for local undo/redo with invariant preservation.

Guarantees reference

What is proved, what is trusted, and where the verification boundary lies.

Build docs developers (and LLMs) love

Get started for freeTalk to us