Contract syntax

The read-only text form in which the view method shows stored laws and definitions, with its constructs, precedences and faithfulness tests.

The contract syntax is how people read stored statements and definitions: the laws a library promises and the contracts it defines. It is a small subset of Lean’s term syntax, and each construct means what Lean means by it. The server’s view method renders objects in it, and lema site build writes it into static pages. Implementations and proofs are still written in restricted Lean; no method accepts contract-syntax text for publishing.

The specification is docs/contract-syntax.md; the renderer and parser are crates/lema-core/src/view.rs.

Forms

A law with its binders in the header:

law Std.Map.find_insert {α : Type} {β : Type} (x : Std.Map.Order α) (y : α) (z : β) (w : List (α × β)) (a : α) :
  (Std.Map.find? x a (Std.Map.insertSorted x y z w)) = (if (Std.Map.Order.compare x a y) = Ordering.eq then some z else Std.Map.find? x a w)

Its source in lean/std/Map.lean, without the tactic proof that follows by:

theorem find_insert {K V : Type} (o : Order K) (k : K) (v : V)
    (l : List (K × V)) (k'' : K) :
    find? o k'' (insertSorted o k v l) =
      if o.compare k'' k = .eq then some v else find? o k'' l := by

The names in the rendering are the published ones, and the binder names are the renderer’s.

Names

• A published name is shown without the LemaDraft. prefix. The prefix stays when the name without it is one of Lean’s (LemaDraft.List.length).
• Lean’s constants are shown by Lean’s names.
• A published name is shown only if it is plain identifiers separated by dots, none of them a keyword (fun, let, max and others), and it is not some, none, true, false or obj_…. An identifier starts with a letter or _ and continues with letters, digits and _ ' ? !, and contains no character that shows nothing or changes how the text around it shows (a Hangul filler, a zero-width or other format character, a bidirectional control).
• An object with no such name is shown as obj_ and the first 12 hex digits of its ID, with a role suffix for a record’s or family’s members: .mk, .rec, .ctor_1, .field_0.
• Each name denotes one stored object, by identity. Display names follow aliases, which can change; the names map that comes with each text is the authority for what it refers to.

Binder names

The store keeps no binder names, so the renderer invents them: α, … for types, h, … for hypotheses, and x, y, z, … for the rest. No invented name is the first part of a shown name, so x.f never reads as a field of a bound x.

Constructs

Precedence

Operators bind as in Lean. Application binds tightest. ∀, fun, ∃, let and if extend as far right as they can.

The renderer also parenthesizes every compound operand, argument and arrow domain, and an arrow’s result when it is an ↔, so a reader does not need this table to read a rendering.

Hidden arguments

A constant’s implicit and instance arguments are hidden only when Lean would infer the same ones: the constant’s parameter kinds are known (from its stored type, or for Lean’s constants from lean/view/external-binders.json), the application ends in an explicit argument with no implicit or instance parameter right after it, and each hidden argument is determined by the explicit ones. Otherwise every argument is shown after @. Universe levels of constants are never shown; Lean infers them.

Not accepted

The syntax has no tactics (by), no sorry, no match, no comments, and no notation or macros of a library’s own. A definition is shown only if its value holds no proofs. A raw structure projection, which Lean source cannot write, is not shown.

A string shows printable ASCII, letters and digits as themselves, and every other character (format, bidirectional, combining, separator, the blank Hangul fillers) by its code point, so a string never hides or reorders what it holds.

The view method

view renders accepted objects through the server:

lema --socket $SOCK call view --params-file view.json

{"render": ["LemaDraft.Std.Map.find_insert"], "names": {…}}

Every name in render must resolve to an accepted object. The response maps each one to a result:

view does not check its output. It renders; it does not parse the text back or elaborate it. Faithfulness is tested on the contracts the tests render, not proved, and not re-tested on each call. The text leaves some parts to Lean: the instance behind + or ≤, the type of =, an if’s Decidable instance, a numeral’s OfNat instance, hidden arguments and universe levels. Those parts are what Lean would infer, not something the text shows. Rendering reads each object’s closure, proofs included, so its memory use grows with the closure.

Faithfulness

A wrong rendering would have a person approve something other than what the store holds, so the renderer is tested, not trusted. Two round trips exist.

The native round trip

For every contract the tests render, the text is parsed back with Lean’s precedences, each name is resolved to the object it denotes, and the result is written as Lean source: a law becomes theorem t binders : statement := <the stored theorem>, a definition def t : type := value. Lean elaborates it, and the result must be the identical statement (or statement and template) object, with the same ID. A rendering that dropped an argument, a binder kind or a coercion fails.

docs/roadmap.md records the API run as 70 of 70 identical objects, over every law and contract definition of Std.Map and its client, Std.Text, Std.Json and HTTP v1’s HealthEchoV1. The HTTP v1 chain is retired under decision 0033.

The structural round trip

The static pages, and the approval views a review can bind, re-derive every text they show without Lean (lema_core::view::rederive). The text is parsed under the name map it is shown with, the canonical expressions it denotes are rebuilt, and the statement (and template) objects they make must have the declaration’s own IDs. What the text shows is rebuilt from the text alone. What it leaves to Lean is taken from the stored object: universe levels, hidden implicit and instance arguments, the hidden arguments of =, +, if and numerals, the binder kind of ∃’s function, and a let’s nondep flag. A text that does not re-derive is marked as not faithful, and one the syntax cannot show as unsupported; neither can be approved.

This checks the parser’s reading of each shown text against the stored object, but not that Lean would infer the hidden parts as stored, which is the native round trip’s job. The pages therefore list every argument the text leaves to Lean, as stored, and the whole declaration with nothing hidden. crates/lema-core/tests/rederive.rs checks that every declaration the renderer shows on the committed fixtures re-derives its IDs. The renderer’s version (view::renderer_sha256, over view.rs without its tests and lean/view/external-binders.json) is part of what a display-bound review binds.

Examples

These renderings are committed in crates/lema-site/tests/golden/ref.html. The site test renders them from the fixture crates/lema-store/fixtures/protected/draft.json, an untrusted draft of lean/core/Protected.lean and its dependencies with placeholder receipts, under the aliases counter.contract, counter.impl, counter.start, counter.conforms and counter.tracks. Contract, Impl and Implements have no alias in that fixture, so they are shown by ID.

def counter.contract :
  obj_9958f0803ab4 Nat (fun (x : Nat) => Nat) Nat :=
  obj_9958f0803ab4.mk (fun (x : Nat) => fun (y : Nat) => y < 2000) (fun (x : Nat) => fun (y : Nat) => fun (z : Nat) => x + 1) (fun (x : Nat) => fun (y : Nat) => fun (z : Nat) => z = x)

def counter.impl :
  obj_19362f1abf24 Nat (fun (x : Nat) => Nat) Nat :=
  obj_19362f1abf24.mk (fun (x : Nat) => fun (y : Nat) => (x, x + 1))

def counter.start :
  Nat :=
  0

law counter.conforms :
  obj_81186ce4539d counter.contract counter.impl Protected.Tracks

law counter.tracks :
  Protected.Tracks counter.start counter.start

The source they come from:

def wide : Received.Contract Nat (fun _ => Nat) Nat :=
  Received.mkContract (fun _ k => k < 2000) (fun s _ _ => s + 1) (fun s _ r => r = s)

def start : Nat := 0
def plainStart : Nat := 0

def plain : Received.Impl Nat (fun _ => Nat) Nat := Received.mkImpl (fun m _ => (m, m + 1))

def Tracks (s m : Nat) : Prop := m = s

theorem plain_implements : Received.Implements wide plain Tracks := by
  intro s m _ h _
  exact ⟨h, congrArg (· + 1) h⟩

theorem tracks_start : Tracks start plainStart := rfl

start and plainStart have the same term, so they are one object, and counter.tracks shows it twice under one name. The object page crates/lema-site/tests/golden/object.html shows counter.start with nothing hidden as @OfNat.ofNat.{0} Nat (nat_lit 0) (@instOfNatNat (nat_lit 0)).