Verdicts

The whole golden table, current.

This is test/golden.txt — every function in the example corpus, run on every build. SAFE and UNSAFE cases in near-equal measure, on purpose: a verifier that says SAFE to everything must fail loudly here. The four modules escalate — basics, composition, inductive data, arrays.

22SAFE

4UNSAFE — with counterexample

1UNSUPPORTED — deliberate mismatch

4Modules

Demo

basics + counterexamples · Demo.purs / Demo.lps

`abs`	Safe	Both branches land in `Nat`.
`sign`	Safe	Guards + `otherwise`; result stays in `[-1, 1]`.
`double`	Safe	`let m = n + n` — the bind enters the context as an equality.
`clamp`	Safe	Dependent spec across binders: result in `[lo, hi]`.
`low`	Safe	`min n 0 <= 0` — discharged once the corpus supplies `min`'s spec.
`flag`	Safe	Boolean-result refinement: returns `true` when `n >= 0`.
`bad`	Unsafe	`bad n = n - 1` is not always `>= 0`. at Demo.purs:9:9 · counterexample: n = 0
`once`	Unsupported	Deliberate spec/type mismatch — the spec declares 2 arguments, the type has 1. Caught by the `docs.json` cross-check before solving.

P1

compositional — call sites, recursion, assume · P1.purs / P1.lps

`myAbs`	Safe	The reusable `Nat`-returning absolute value.
`dist`	Safe	Calls `myAbs`; its postcondition is assumed at the site.
`sumTo`	Safe	Recursion — the recursive call assumes `sumTo`'s own spec.
`inc`	Safe	Precondition `n >= 0` ⇒ result `>= 1`.
`callGood`	Safe	`inc (myAbs n)` — `myAbs`'s postcondition discharges `inc`'s precondition.
`low2`	Safe	`min n 0 <= 0`, via the trusted `min` spec.
`size`	Safe	Multi-alternative `case` on `Int` literals; result in `[0, 2]`.
`callBad`	Unsafe	`inc n` without `myAbs` — `n` may be negative, so `inc`'s precondition fails at the call site. at P1.purs:21:13 · counterexample: n = -1

P2

inductive ADTs via measures · P2.purs / P2.lps

`count`	Safe	Proves `count l == len l` by induction (own-spec recursion).
`append`	Safe	Proves `len (append a b) == len a + len b` via constructor facts.
`singleton`	Safe	`len (ICons x INil) == 1` through nested constructor applications.
`headOr`	Safe	Total head — the `INil` case supplies the default.
`badCount`	Unsafe	Forgets the `+ 1`, so the count can't equal `len l`. at P2.purs:21:16 · counterexample: a non-empty list — the dropped step makes the count disagree with the measure

Arrays

built-in length measure + library specs · Arrays.purs / Arrays.lps

`three`	Safe	`[1,2,3]` has length exactly 3 — literals contribute exact lengths.
`grow`	Safe	`cons 0 xs` — length grows by one.
`mid`	Safe	Valid index via Euclidean division, under a non-empty precondition.
`firstHalf`	Safe	`take (length xs / 2) xs` — result no longer than `xs`.
`rest`	Safe	`drop 1` off a non-empty array — length is exactly one less.
`badMid`	Unsafe	Same body as `mid` but without the non-empty precondition: `badMid [] = 0` is not `< length []`. at Arrays.purs:18:13 · counterexample: xs = []

Why the failures are the point. Each UNSAFE case is a working function that would compile and run — it's the refinement it fails, and the tool pins the failing span and hands back an input that breaks it. once, the lone UNSUPPORTED, is a spec that has drifted from its type; the tool refuses to solve rather than guess. Nothing here is a silent pass.