[Property tracking] improved design: replace prose marker with typechecked statement-proof pair

[williamdemeo]

Context

PR #1226 (issue #1225) introduced the property catalog (build-tools/scripts/property-tracking/properties.yaml), the scanner (build-tools/scripts/property-tracking/scan_properties.py), and the generated dashboard.

Status of each property is derived, never declared:

• no module → idea;
• module named but module file absent → planned;
• module file exists and contains the phrase "coming soon" → stated;
• otherwise → proved.

The Agda --safe typecheck in the main CI guarantees that whatever Agda exists has no holes or postulates; the scanner guarantees the bookkeeping matches the files.

Problem

The stated/proved distinction rests entirely on a prose marker. A module could formally state a property as an uninhabited type definition (e.g. pp-wellFormed-invariant : Type in src/Ledger/Conway/Specification/Chain/Properties/PParamsWellFormed.lagda.md), which typechecks cleanly. If the *Proof*. (coming soon) line is dropped or forgotten, the dashboard reports the property as ✅ proved with every CI job green: a false positive in the dangerous direction, caught by nothing automated. Some of the currently-stated Conway properties have this shape.

Proposed re-design

Make the statement and the proof separately named artifacts, record both names in the catalog, and let the typechecker, not prose, certify the relationship between them.

Catalog

In the properties.yaml catalog,

• each record represents a single property;
• rename defs to def; this field will contain a single value instead of a list; it is the name of the type that defines the property.
• add a field called proof; it contains a single value: the name of the inhabitant of the type named in def.

Each entry continues to describe exactly one property. Replace defs (a list, currently decorative) with two scalar fields, as in the following example:

  - id: conway-ledger-pov
    title: "LEDGER preserves value"
    era: conway
    sts: LEDGER
    module: Ledger.Conway.Specification.Ledger.Properties.PoV
    anchor: thm:LEDGER-PoV
    def: LEDGER-pov          # the property, stated as a type
    proof: LEDGER-pov-proof  # the inhabitant of that type
    issues: [1238]
    notes: ""

def names the property definition as a type; supporting lemmas stay out of the catalog; where a module proves several, the entry names the headline theorem only (though we should be able to have multiple yaml records for a single module).

New rules for determining status

• module field empty → idea;
• module field nonempty but module file absent → planned;
• module file exists but def field is empty → planned;
• module file exists, def field nonempty →
  • proof field empty → stated
  • proof field non-empty it names an inhabitant of the type named in def → proved

Module convention

Each property module states the property as a type definition and proves it with a literal one-line ascription; for example, instead of what we have now:

  LEDGER-pov : {Γ : LEnv} {s s' : LState}
    → txId ∉ mapˢ proj₁ (dom (UTxOOf s))
    → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → getCoin s ≡ getCoin s'

  LEDGER-pov
    {s  = s}
    {s' = s'}
    h (LEDGER-V {utxoSt' = utxoSt''} ( valid , UTXOW⇒UTXO st@(UTXO-induction r) , h' , _ )) =
  -- abridged --

we would change the Ledger PoV type/proof to the following format:

  LEDGER-pov : Type
  LEDGER-pov = {Γ : LEnv} {s s' : LState}
    → txId ∉ mapˢ proj₁ (dom (UTxOOf s))
    → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → getCoin s ≡ getCoin s'

  LEDGER-pov-proof : LEDGER-pov
  LEDGER-pov-proof
    {s  = s}
    {s' = s'}
    h (LEDGER-V {utxoSt' = utxoSt''} ( valid , UTXOW⇒UTXO st@(UTXO-induction r) , h' , _ )) =
  -- abridged ---

That way, the scan_properties script really only has to check that the line LEDGER-pov-proof : LEDGER-pov appears to confirm that the property is proved.

More generally, if a yaml record has

  - id: conway-ledger-property
    def: PropertyType
    proof: PropertyProof

Then the scanner must find a line containing the string PropertyProof : PropertyType.