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.

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.

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, whose kind the account reports.

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

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.

Limitations and unsupported cases🔗

A contract in another library, executable root or file of the project does not count: the inventory is that of the audited environment that owns the function. Register the contract in the function's library.

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/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 inventory. 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.