Checked example🔗

import Regula.Decision
/-! # Zero test

A decision that a natural number is zero, with no contract. -/
/-- Whether `n` is zero. -/
@[regula_decision] def isZero : Nat → Bool
  | 0 => true
  | _ + 1 => false

isZero (def) type=Nat → Bool axioms=[] -> kernel-only decision-result=other

- import Regula.Decision
- /-! # Zero test
- 
- A decision that a natural number is zero, with no contract. -/
- /-- Whether `n` is zero. -/
- @[regula_decision] def isZero : Nat → Bool
-   | 0 => true
-   | _ + 1 => false
+ import Regula.Contract
+ import Regula.Decision
+ /-! # Zero test
+ 
+ A decision that a natural number is zero, with its two-way contract. -/
+ /-- Whether `n` is zero. -/
+ @[regula_decision] def isZero : Nat → Bool
+   | 0 => true
+   | _ + 1 => false
+ theorem contract : Regula.ExecutableContract isZero (Regula.Decides (· = true) (· = 0)) :=
+   ⟨.of_iff (fun | 0 => ⟨fun _ => rfl, fun _ => rfl⟩ | _ + 1 => ⟨nofun, nofun⟩) ⟨0, rfl⟩ ⟨1, nofun⟩⟩

import Regula.Contract
import Regula.Decision
/-! # Zero test

A decision that a natural number is zero, with its two-way contract. -/
/-- Whether `n` is zero. -/
@[regula_decision] def isZero : Nat → Bool
  | 0 => true
  | _ + 1 => false
theorem contract : Regula.ExecutableContract isZero (Regula.Decides (· = true) (· = 0)) :=
  ⟨.of_iff (fun | 0 => ⟨fun _ => rfl, fun _ => rfl⟩ | _ + 1 => ⟨nofun, nofun⟩) ⟨0, rfl⟩ ⟨1, nofun⟩⟩

The correction registers the two-way contract of the unchanged zero test: it accepts exactly zero, with zero as the accepted input and one as the refused input.

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. Prove both directions and a witness of each outcome: ExecutableContract f (Decides (· = true) Spec), from an existing equivalence by Decides.of_iff.

2. State a deliberate one-way guarantee with DecidesSoundly (may refuse inputs that satisfy Spec) or DecidesCompletely (may accept inputs that do not).

3. Decide several arguments on their product, ExecutableContract f (fun g => Decides accepts Spec (Function.uncurry g)), or on a structure whose fields are the arguments; for a result type that depends on the arguments, decide Regula.Dependent.isSome g or isOk g (RG1007).

4. Return the proof with the verdict: def f (x : α) : Decidable (Spec x). Each result then carries a proof of Spec x or of its negation, and no contract is needed.

Why it matters🔗

A checker with no stated direction can refuse every input or accept every input, and an unstated one-way guarantee cannot be told from an omission. The tag makes the contract a requirement of the function itself, so deleting the contract while the function stays tagged fails the gate instead of removing the requirement with it.

Standard §7.5 requires that removing evidence while its requirement remains fails the gate. For a contract no caller consumes through ExecutableContract.run, deleting the theorem would delete the requirement with it. The registration keeps the requirement at the function: deleting the contract while the registration stays is this rule's finding.

A Decidable p result needs no contract: its accepting value carries a proof of p and its refusing value a proof of ¬p, so both directions hold by construction (standard §3.2.4). It carries no witness that both outcomes occur: Decidable True qualifies.

What triggers it🔗

The checker reads the @[regula_decision] registration of every owned declaration from the completed Lean environment, and whether the declaration's type, with its arguments opened and its result type reduced, ends in Decidable _. A registration counts whether the module that declares the function wrote it or another loaded module did.

A registered declaration whose result type is not Decidable _ is rejected, with applicability decision-contract, unless a declaration of the same inventory records an ExecutableContract that names it as the implementation, states a decision kind (Regula.DecidesSoundly, Regula.DecidesCompletely or Regula.Decides) and was not refused under RG1007. The inventory is the declarations of the audited environment that owns the function: its library, an executable root inspected alone, a file, or a group of documentation fences.

In a project audit, a contract of another claimed surface counts too when the manifest names the function's library in that surface's decides. It is the record that surface's environment holds in the same run, and that environment loaded the function's module from the same .olean file with the same imports.

Every registered declaration has the requirement, whatever else the checker records of it: one a project registers explicitly, such as a structure projection, and one named like a generated declaration. Lean applies the registration after compilation, so it is not copied to the _unary or _mutual definition Lean generates for a function defined by well-founded recursion.

The rule is decided after the declaration's other requirements (RG1001 to RG1007 and RG1009), so it is reported for a declaration that meets them. The editor does not render it: a contract normally follows its function, in a later command or module, so a snapshot of one command cannot decide whether the inventory has one.

Required proof shape🔗

ExecutableContract f (Regula.Decides accepts spec), or Regula.DecidesSoundly or Regula.DecidesCompletely for a declared one-way guarantee, in the library that declares f. RG1007 gives the supported shape of the registration, with a structure of the arguments for a function with a dependent argument type or a type argument, and an erasure of the result (Regula.Dependent.isSome or isOk) for one with a dependent result type. The registration may also be in a claimed surface whose decides names the library of f.

Or a result type Decidable (spec x), as a DecidablePred spec instance has.

What a passing result establishes🔗

Every owned declaration registered with @[regula_decision] whose result type is not Decidable _ is the implementation of an accepted decision contract of its inventory, or of a surface that the manifest relates to its own in the same run. The account reports its kind, and for a contract of another surface, that surface.

Removing that contract while the registration stays is rejected.

It does not establish:

• That every function that acts as a checker is registered: the registration is the project's own declaration, and removing it removes the requirement (R-INVARIANT).

• That the contract's specification is the intended one (R-INTENT), that a one-way kind should have been two-way, or which value an accepting result carries.

• For a Decidable result: that the decided proposition is the intended one, that both outcomes occur, or that the instance is computable.

• That callers act on the function's verdict (R-INVARIANT).

• That a relation the manifest declares between two surfaces is the intended one: the manifest is the project's configuration.

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

Configuration and exceptions🔗

@[regula_decision] is declared in Regula.Decision, a published checker interface a claimed module may import: import Regula.Decision, or meta import Regula.Decision in a file that is a module. Write it on the definition (@[regula_decision] def f), or with attribute [regula_decision] f in a module of the same library that imports f, for a function whose own module cannot import Regula.Decision.

A claimed surface of the manifest may list other claimed surfaces in decides. The recorded contracts of its declarations then count toward the registered decisions of each surface it names. The function stays registered in its own library.

Limitations and unsupported cases🔗

A contract in another library, executable root or file of the project does not count unless the manifest relates the two surfaces: the inventory is that of the audited environment that owns the function. Register the contract in the function's library, or name that library in the decides of the surface that holds the contract. A file or a group of documentation fences has no manifest that relates surfaces.

A registration that an audited module writes for a declaration outside its inventory stops the audit without a verdict, naming the module and the declaration: that inventory records no declaration to decide the requirement for. Register a function in a module of the library that declares it.

A function whose result type depends on its arguments in a way neither erasure removes, or for which no accepted or refused input can be given with a proof, has no decision kind (limitations of RG1007). Return Decidable _, or leave the function unregistered and record why.

A function in IO, MetaM or another monad comes into scope through the pure decision it runs: register that decision.

The registration is environment state an audited project writes. It only adds a requirement; no registration or option waives one.

The editor never reports this rule; lake lint or a file audit does.

Sources🔗

Normative clauses

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

Checklist rows

THEOREM-07, BUILD-03

Detector, policy and proof sources

lean/Regula/Decision.lean, lean/RegulaPolicy/Decision.lean, lean/RegulaPolicy/Specification.lean, lean/RegulaPolicy/Plan.lean, lean/Regula/Collect.lean, lean/RegulaCore/Policy.lean

Proved linkage

RegulaPolicy.policyFor decides the rule after the declaration's own requirements. policyFor_decisionContract_iff proves it reports the decision failure exactly for an inventory member that meets those requirements, is registered with a result type other than Decidable _, and is the implementation of no accepted decision contract of the inventory (DecisionRegistered); policyFor_ordered gives its place after the other failures, and Roles.decided_iff ties the decided implementations to the contracts the inventory counts (Inventory.decisionContracts). In a project census census_decided_iff states those contracts: the inventory's own and those of the surfaces the claim relates to its own (countedContracts), only its own where none is related (census_decided_iff_of_unrelated), and accepted_counted_judgment that each counted contract's registration met its own requirements in its own environment of the same accepted run. Project, file and documentation audits run it through Regula.Checker.Policy.checked_memberRule (ruleForMember_eq). The editor's decision does not run it (Regula.Checker.Policy.editor_decision_ne_decisionContract). Reading the registration and the result type (Regula.Collect) is operational, and so is each recorded contract.