Checked example🔗

import Regula.Contract
/-! # Identity

Identity on natural numbers, with its full-domain contract. -/
/-- The identity function on natural numbers. -/
def identity (n : Nat) : Nat := n
theorem contract (n : Nat) :
    Regula.ExecutableContract (identity n) (fun value => value = n) := ⟨rfl⟩

contract (theorem) [Prop] type=∀ (n : Nat), Regula.ExecutableContract (identity n) fun value => value = n axioms=[] -> kernel-only executable-contract=[anonymous] requires=(fun value => value = n) (identity n) failure=registration must be closed; put the implementation's complete domain inside its predicate

  ⋯ 3 unchanged lines
  Identity on natural numbers, with its full-domain contract. -/
  /-- The identity function on natural numbers. -/
  def identity (n : Nat) : Nat := n
- theorem contract (n : Nat) :
-     Regula.ExecutableContract (identity n) (fun value => value = n) := ⟨rfl⟩
+ theorem contract : Regula.ExecutableContract identity (fun f => ∀ n, f n = n) :=
+   ⟨fun _ => rfl⟩

import Regula.Contract
/-! # Identity

Identity on natural numbers, with its full-domain contract. -/
/-- The identity function on natural numbers. -/
def identity (n : Nat) : Nat := n
theorem contract : Regula.ExecutableContract identity (fun f => ∀ n, f n = n) :=
  ⟨fun _ => rfl⟩

The correction moves the complete natural-number domain inside the identity contract's predicate, retaining the same pointwise equality.

Checked by a fresh single-file audit of <example>/Fixture.lean (axiomGate --file, claim kernel-only, execution checked): violating run rejected, corrected run completed.

How to fix it🔗

1. Move the quantified parameters into the predicate: replace theorem c (n : Nat) : ExecutableContract (f n) (fun v => v = n) by theorem c : ExecutableContract f (fun g => ∀ n, g n = n).

2. Name the computable, safe, non-partial definition that callers use; route callers through c.run.

3. Universe-polymorphic implementations are supported; explicit universe instantiation is recorded.

4. For a checker, state the direction with a kind: ExecutableContract check (Decides (· = true) Spec), or DecidesSoundly or DecidesCompletely for a one-way guarantee. Decide several arguments through fun g => Decides accepts Spec (Function.uncurry g), and state Spec without check.

Why it matters🔗

A contract is useful only if it constrains the code callers run. A registration over f n for a fixed parameter, or over an ineligible constant, says nothing about the executable definition across its domain; a specification that mentions f can restate f.

A checker with only a soundness theorem can refuse every input, and one with only a completeness theorem can accept every input. A one-way guarantee is often the right choice, as for a refusal that fails closed, but an unstated one cannot be told from an omission. A kind states the direction in the registration's type.

Each kind carries a witness about f itself: DecidesSoundly requires an input f accepts and DecidesCompletely an input it refuses. So the function that refuses every input has no sound kind and the function that accepts every input has no complete kind (Regula.DecidesSoundly.not_of_refuses_all, Regula.DecidesCompletely.not_of_accepts_all).

What triggers it🔗

The checker recognizes declarations of type Regula.ExecutableContract f R as executable promises about f. It rejects, with applicability executable-contract, a registration with free parameters, a partially applied or term-parameterized implementation, or an implementation that is missing, noncomputable, unsafe, partial, proposition-valued, type-producing or not an executable definition.

A registration whose requirement R f reduces to an application of Regula.DecidesSoundly, Regula.DecidesCompletely or Regula.Decides is a decision registration. The checker reads the kind from the head constant of that elaborated requirement, so an alias of a kind is recognized and no theorem text or name is matched, and it reports the kind with the direction a one-way kind leaves open.

It rejects a decision registration whose kind is stated about a function other than f or Function.uncurry applied to f one or more times, or whose acceptance predicate or specification mentions f: f is among the constants the term mentions, closed under the types and unfoldable values of those constants and the constructors of their inductive types. The finding names the constants through which f is reached.

Lean's type checker separately checks the supplied proof of R f.

Required proof shape🔗

ExecutableContract f R for a named constant f with R : type-of-f → Prop stating the full-domain requirement. The proof inhabits exactly R f; a weaker R changes the requirement and is a review failure.

For a function that acts as a checker, R is a decision kind over an acceptance predicate and a specification: Regula.Decides accepts spec for both directions, Regula.DecidesSoundly accepts spec when a refusal may be wrong, Regula.DecidesCompletely accepts spec when an acceptance may be. A function of several arguments is decided on their product: fun g => Regula.Decides accepts spec (Function.uncurry g), with spec over the pairs.

What a passing result establishes🔗

The registration is closed, names an eligible executable constant, and Lean checked a proof of the stated predicate about it.

For a decision registration: Lean checked the directions its kind names about f against the written specification, with an accepted input for a sound kind and a refused input for a complete kind, and neither the acceptance predicate nor the specification mentions f.

It does not establish:

• That R expresses the intended behavior (R-INTENT) and that every caller uses the contracted implementation (R-INVARIANT). Every accepted account lists these as open for each reported contract.

• That a function acting as a checker is registered, or registered with a kind: RG1008 requires a decision contract only of a function the project registers with @[regula_decision], and which functions are checkers is a project's own declaration (R-INVARIANT).

• For a decision registration: that the specification is the intended one or is independent of the implementation in substance (a copy of the implementation under another name passes), the direction a one-way kind leaves open, and which value an accepting result carries.

• Behavior of compiled code beyond the Lean definition; execution boundaries are RG3001 and RG3002.

It leaves these review obligations open: R-INTENT, R-INVARIANT, R-QUALIFY.

Limitations and unsupported cases🔗

Term-parameterized and partial-application registrations are unsupported shapes, not proofs of incorrectness; restate them as closed full-domain contracts.

A decision kind covers a function whose argument types do not depend on earlier arguments, through Function.uncurry. A function with a dependent or implicit argument is decided through a named function over a product, sigma or subtype domain, or registered with an ordinary requirement, which is reported with no kind.

A requirement that contains a kind inside a larger proposition, such as a conjunction, is reported with no kind: the kind is read from the head constant only. Register the further clauses separately.

A specification that mentions the implementation only inside a proof term written in the registration is refused like any other mention; state it without the implementation. A proof that Lean abstracts into an auxiliary theorem of a named definition is not followed: that theorem's statement is searched and its proof is not, so a mention that occurs only in such a proof is not reported. The specification does not depend on which proof of that statement it is.

Sources🔗

Normative clauses

standard §7.11 Opt-in Enforcing Build Linter, standard §7.5 Proof Completeness and Foundation Strength

Checklist rows

BUILD-03, THEOREM-07, SCOPE-02, SCOPE-03, TYPE-01, THEOREM-01, THEOREM-03, COMP-01, BUILD-01, BUILD-02

Detector, policy and proof sources

lean/Regula/Contract.lean, lean/Regula/Collect.lean, lean/Regula/Probe.lean, lean/RegulaCore/Policy.lean

Proved linkage

The shared declaration decision RegulaPolicy.declarationFailure (its first failed requirement, declarationFailure_ordered) is mapped to a rule by the injective Regula.ruleForFailure. Project, file and documentation audits run it through Regula.Checker.Policy.checked_memberRule (ruleForMember_eq); the editor runs Regula.Linter.checked_editorDecision. For the same member and request, the editor passes exactly when the project decision selects no rule or only RG1008, which the editor does not render (Regula.Checker.Policy.editor_decision_none_iff), a rule it renders is the project decision's rule (editor_decision_rule), and a pending result withholds a project rule whose failure needs generated-role evidence (editor_decision_pending). The editor's request domain is the project's without teaching (editor_request_sound, editor_request_complete). The observed declaration fields and generated-role evidence are hypotheses of these theorems. Extracting the contract observation (Regula.Collect), including the reduction that reads a decision kind and the search for a mention of the implementation, is operational; that a head constant is read as a kind exactly when it is that kind's structure is proved (RegulaPolicy.DecisionKind.ofStructureName?_eq_some_iff).