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. State a decision kind about such an implementation at its own universe parameters. State a decision kind about an implementation applied to every argument: a kind whose result is still a function is refused.

4. For a checker, state the direction with a kind: ExecutableContract check (Decides (· = true) Spec), or DecidesSoundly or DecidesCompletely for a one-way guarantee, with Spec stated without check. Decide several arguments through Function.uncurry, or on a structure whose fields are the arguments: fun g => Decides accepts Spec (fun x : Input => g x.a x.b). For a result type that depends on the arguments, decide Regula.Dependent.isSome g or isOk g.

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 on its arguments, on a packing of them, or with its result erased. A packing is f applied to every field of the variable of one function, each field once and in the order of the fields, where the variable's type has one constructor and no index (RegulaPolicy.FieldPacking.covers). Function.uncurry and the two erasures (Regula.Dependent.isSome and Regula.Dependent.isOk) can each be applied, any number of times, to f or to that field application. No other way of supplying the arguments is read as a packing, and no other function of the result as an erasure: these three constants are read by name.

A function that fixes an argument or gives a field twice decides f on part of its domain. A structure with a field that f does not take, such as a proof about the other fields, can restrict the domain, and so can an index: a type with an index holds only the tuples whose fields compute that index. Lean's structure command makes no projection for such a type, but Lean's kernel admits a primitive projection on it, so the checker reads the index count from the type's kernel-checked declaration. It reads whether an argument is a field from the kernel-checked value of the projection, not from Lean's record of projection functions, which a project can write.

It rejects a decision registration whose decided function has a result that is a function: f with an argument left, through f itself, Function.uncurry or a field application. The result type of the kind, with every definition unfolded, then has a leading binder, and the finding gives the number of them. The decision on the packing and on that number is one pure function (RegulaPolicy.DecidedFunction.covers).

That refusal is a conservative structural restriction. A kind whose acceptance predicate reads a function-valued result at one fixed value of the argument is the kind of one slice of f (Regula.Decides.iff_slice) and says nothing of f at another value. A kind whose acceptance predicate quantifies over the argument can constrain every value, and the checker, which does not read the acceptance predicate, refuses it too. The remedy for both is to supply the argument.

It rejects a decision registration that states its kind about f at universe levels other than the universe parameters of f, each once: such a kind holds of some universe instances of f and not of the others. The finding names the levels.

It rejects a decision registration 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, with every argument supplied: fun g => Regula.Decides accepts spec (Function.uncurry g) for two arguments, with spec over the pairs, and one more Function.uncurry for each further argument.

Where the type of an argument depends on an earlier argument, or an argument is a type, an instance or a proof, the kind is stated about f applied to every field of one structure, in the order of the fields: fun g => Regula.Decides accepts spec (fun input : Input => g input.a input.b input.c), with spec over Input, a structure whose fields are the arguments. For two arguments the structure can be a pair (Prod, Sigma, PSigma or Subtype). A kind about a function with universe parameters is stated at those parameters, as @f.{u} in a registration with the universe parameter u.

Where the result type depends on the arguments, the kind is stated about an erasure of the result, a function whose type does not depend on the input: Regula.Dependent.isSome g for an Option of a payload and Regula.Dependent.isOk g for an Except of one, both to Bool. So R is fun g => Regula.Decides (· = true) spec (Regula.Dependent.isOk g), and the acceptance predicate reads the erased result and nothing else.

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.

For a decision registration: the report names each function outside Lean's own library that the specification and f or the acceptance predicate both reach, by name, in two classes. A function with a result of Bool or BEq is named at any depth, and RG1009 refuses the registration for it. Each other function is named where the specification reaches it first, and no registration is refused for it. The search for that class stops at each named function, so a function of that class that only a named function calls is not named. A function with a result of Bool or BEq that the two sides share only through the declaration of the input type is named apart, and no registration is refused for 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.

• 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, and so does a copy of a helper), the direction a one-way kind leaves open, and which value an accepting result carries.

• For a decision registration: anything about a function that the report names as shared. When the specification and f both call a function, a change of that function changes the two together. Each direction then holds or fails as its proof does, and a proof that goes through the shared function on the two sides can stay valid although the meaning changed. The same holds of a function that the specification and the acceptance predicate both call. Whether the specification is about the function, as it is about an encoding or a state transition, or only uses it to prepare the input, remains review (R-INTENT). Where the function has a result of Bool or BEq, RG1009 refuses the registration.

• For a decision registration: that the acceptance predicate is the intended reading of a result (R-INTENT). A constant function has no two-way kind (Regula.Decides.not_of_constant). But when the result of f determines its input, as the result of the identity function does, an acceptance predicate can restate the specification: Regula.Decides spec spec id holds of every specification that some input satisfies and some input does not.

• 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 result type whose dependency on the input neither erasure removes, such as an inductive family indexed by the input, has no kind: return Decidable _, or register an ordinary requirement, which is reported with no kind. A registration cannot supply an erasure of its own: one stated for every payload type can read the payload type, and "the payload type has a value" is the specification of a proof-carrying payload, whatever the function returns.

A result of a subtype type that depends on the input, {r : ρ // P x r}, has no kind until issue 243 is decided: an erasure that returns the value of the subtype would keep a free acceptance predicate on a data value. Such a function returns Decidable p, or is registered with an ordinary requirement.

In a file with a module header, the editor does not read a decision kind whose decided function applies to its variable an imported constant that Lean gives the file as an axiom, as it gives the projection function of a proof field: the editor cannot tell whether that argument is a field. It reports the reading as incomplete under RG2005 and names lake lint, which reads the kind.

The fields are those of one structure: a field of a field, as in a nested pair, is not read as a field. Nested dependent pairs are also costly: each projection of a pair carries the pair's type, so the elaborated statement grows by a large factor with each argument. Declare one structure for three or more arguments whose types depend on each other.

A kind requires an input with a proof: an accepted input for a sound kind and a refused input for a complete kind. For a function with universe parameters the witness is at every universe level, so its types are universe-polymorphic, such as PUnit.

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.

The search for shared functions compares names. The specification and the acceptance predicate are statements. For each of the two it follows the types of constants, the unfoldable values of definitions, a definition of a proposition among them, and the constructors of inductive types, and it reads no value of a Decidable instance. For f it follows the unfoldable values of definitions and the types of constants that are no inductive type, constructor or recursor. It reads the value of a Decidable instance, which a function runs. It does not read the value of a definition of a type, of a proposition or of a record of propositions, which a function does not run. It does not read the body of a named proof declaration, and it reads no module of Lean's own library. A proof term that is written inline in the specification or in the acceptance predicate is a part of that term, so the search reads the constants that it names. For a function with a result of Bool or BEq it reads at any depth, also below a named function of the other class. For the other class it does not read below a named function. A second definition with the text of a helper is a different constant, and the search does not find it. A second definition with a theorem that the two are equal is not named either, and it is not a second statement of the meaning.

Data and statements are not named: an inductive type with its constructors, its recursor and its projection functions, a definition whose value is a type, a proposition or a record of propositions, a proof, a definition with a result of Decidable p, and a constant that is no function. Whether a definition is a function is read from its type alone: it takes an argument, or its result is a structure with a field that takes one, as BEq is. Which definitions Lean generated for a type or as a matcher is read from Lean's records, which a project can write. That reading only keeps a function out of the second class: a function with a result of Bool or BEq is named unless its kernel-checked value is a field's projection function. A field of a structure is read one level deep, at the arguments of the structure type.

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/RegulaPolicy/Domain.lean, lean/RegulaPolicy/MentionSearch.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 reading of the decided function and of its universe levels, is operational. Three decisions in it are proved. The search that guards each reduction, and the search for a mention of the implementation, return a route exactly when a constant of the term leads to a target through the records of the observing pass, and a returned route follows those records (RegulaPolicy.MentionSearch.checked_search, search_sound). What a record lists is read from the environment, and that a constant with no record leads to no target is argued and is not machine-checked. A head constant is read as a kind exactly when it is that kind's structure (RegulaPolicy.DecisionKind.ofStructureName?_eq_some_iff), and a decided function of a form that is read is accepted exactly when its field application, if it has one, is on a type with one constructor and no index with the arguments its fields in order, and the kind's result type has no leading binder (RegulaPolicy.DecidedFunction.covers_iff with RegulaPolicy.FieldPacking.covers_iff). Two steps from those numbers to the claim are argued from Lean's typing rules and are not machine-checked. A result type with no leading binder is the type of a result that takes no argument, so no argument of the implementation is left. A type with one constructor and no index has a value for every tuple of fields, so the packing reaches every tuple of arguments, which is the hypothesis of Regula.Decides.of_packing. The names of the shared functions are proved over what the search reads of each shared definition (RegulaPolicy.SharedDefinition: its kind, whether its value is a projection function, and the form of its result type). A name is in a class of the record exactly when a definition of that class has it (RegulaPolicy.mem_sharedNames_booleans, RegulaPolicy.mem_sharedNames_others), and each class is a stated condition on those readings (RegulaPolicy.SharedDefinition.class_eq_boolean_iff, class_eq_other_iff). The search that finds the shared definitions, and the reading of each, are operational.