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.

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.

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.

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.

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.

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.

• 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.

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/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 (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) is operational.