Checked example🔗

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

A decision of a bound whose specification calls the test that the function runs. -/
/-- Whether `n` is below four. -/
def small (n : Nat) : Bool := decide (n < 4)
/-- Whether `n` is below four. -/
@[regula_decision] def check (n : Nat) : Bool := small n
theorem contract : Regula.ExecutableContract check (Regula.Decides (· = true) (small · = true)) :=
  ⟨.of_iff (fun _ => Iff.rfl) ⟨0, rfl⟩ ⟨4, by decide⟩⟩

contract (theorem) [Prop] type=Regula.ExecutableContract check (Regula.Decides (fun x => x = true) fun x => small x = true) axioms=[] -> kernel-only executable-contract=check decision-kind=sound-and-complete requires=Regula.Decides (fun x => x = true) (fun x => small x = true) check shared-booleans=["small"] shared-others=[]

  import Regula.Contract
  import Regula.Decision
  /-! # Bound test
  
- A decision of a bound whose specification calls the test that the function runs. -/
- /-- Whether `n` is below four. -/
- def small (n : Nat) : Bool := decide (n < 4)
- /-- Whether `n` is below four. -/
- @[regula_decision] def check (n : Nat) : Bool := small n
- theorem contract : Regula.ExecutableContract check (Regula.Decides (· = true) (small · = true)) :=
-   ⟨.of_iff (fun _ => Iff.rfl) ⟨0, rfl⟩ ⟨4, by decide⟩⟩
+ A bound stated as a proposition. -/
+ /-- `n` is below four. -/
+ def Small (n : Nat) : Prop := n < 4
+ instance (n : Nat) : Decidable (Small n) := n.decLt 4
+ /-- Whether `n` is below four. -/
+ @[regula_decision] def check (n : Nat) : Bool := decide (Small n)
+ theorem contract : Regula.ExecutableContract check (Regula.Decides (· = true) Small) :=
+   ⟨.of_iff (fun _ => ⟨of_decide_eq_true, decide_eq_true⟩) ⟨0, rfl⟩ ⟨4, by decide⟩⟩

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

A bound stated as a proposition. -/
/-- `n` is below four. -/
def Small (n : Nat) : Prop := n < 4
instance (n : Nat) : Decidable (Small n) := n.decLt 4
/-- Whether `n` is below four. -/
@[regula_decision] def check (n : Nat) : Bool := decide (Small n)
theorem contract : Regula.ExecutableContract check (Regula.Decides (· = true) Small) :=
  ⟨.of_iff (fun _ => ⟨of_decide_eq_true, decide_eq_true⟩) ⟨0, rfl⟩ ⟨4, by decide⟩⟩

The correction states the bound as the proposition Small, which the function decides, so the specification names no test that the function runs.

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. Replace def small (n : Nat) : Bool := n < 4 in the specification by def Small (n : Nat) : Prop := n < 4 with instance (n : Nat) : Decidable (Small n) := by unfold Small; infer_instance, and write decide (Small n) or if Small n then … else … in the function.

2. Where a function that the two sides share calls the test, change that function: it decides the proposition, and the specification then reaches the proposition and not the test.

3. For a type with a derived BEq that the two sides compare, derive DecidableEq and state the specification with =. Lean's own BEq of a type with DecidableEq is not counted.

4. Use a test of Lean's own library directly, such as Char.isWhitespace or Nat.ble: the rule does not count a function of that library.

Why it matters🔗

A kind is a theorem about the present definitions. When the specification and the implementation call one test, a change of that test changes the two together, and a proof that goes through the test on the two sides can stay valid although the meaning changed. A proposition in the place of the test states the meaning a second time, in other terms.

A kind is a theorem about the present definitions. When the specification and the implementation both call test, a change of test changes the two together. Each direction then holds or fails as its proof does, and a proof that goes through test on the two sides stays valid although the meaning changed. In the smallest case the specification is test x = true, the function is test, and the proof of the two directions is Iff.rfl.

A proposition in the place of the test is a second statement, in other terms: a quantifier, an order relation or an equation in place of a fold, a comparison function or a BEq. The theorem that the test decides the proposition, or the Decidable instance that the function runs, is then a proof that connects two statements.

What triggers it🔗

For each ExecutableContract registration with a decision kind that RG1007 does not refuse, the checker searches the two sides of the kind. One side is the specification. The other side is the implementation with the acceptance predicate.

The registration is rejected, with applicability shared-test, when the specification reaches a function with a result of Bool, or a definition with a result of BEq, that the other side reaches too. The search for such a function reads at any depth: also below a function of another result type that the two sides share. The finding names each such function after shared-booleans=.

A function of Lean's own library is not counted, and no module of that library is read. A structure projection is not counted. A definition with a result of Decidable p is not counted, and the specification's side does not read its value.

The rule is decided after RG1007 for the same registration and before RG1005. The editor renders it at the registration theorem.

Required proof shape🔗

def P (x : α) : Prop := …, instance (x : α) : Decidable (P x) := …, a function that runs decide (P x) or if P x then … else …, and ExecutableContract f (Regula.Decides accepts P).

Or a function that keeps its test, a theorem test x = true ↔ P x, and an instance decidable_of_iff _ (test_iff x): the specification names P, and the function reaches the test through the instance.

For a comparison of values of a type with a derived BEq: deriving DecidableEq, and = in the specification.

What a passing result establishes🔗

The record of every accepted decision registration names no function with a result of Bool or BEq, outside Lean's own library, that the specification and the other side both reach, at any depth of the specification.

The account still names each other function that the two sides share, where the specification reaches it first (shared-others=).

It does not establish:

• That the specification is the intended one (R-INTENT). The rule compares names. A copy of a test under a second name is a different constant and passes, and so does a proposition that copies the expression of the test with = true. A test with no name of its own passes too: a function abstraction inside a shared function, or inside a shared record of functions.

• Anything about a shared function of another result type, such as a function that returns a list or a record. The account names it and no registration is refused for it. Whether the specification is about that function, as it is about an encoding or a state transition, remains review (R-INTENT).

• Anything about a test of Lean's own library, which the two sides can both call.

• A test that only a runtime replacement runs (implemented_by, extern, csimp): the search reads kernel-checked values. RG3001 and RG3002 account for the replacement.

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

Limitations and unsupported cases🔗

The search compares constants by name. It follows the types of constants, the unfoldable values of definitions and the constructors of inductive types from the specification and the acceptance predicate, and the unfoldable values of definitions from the implementation. It does not read the body of a named proof declaration, and it reads no value of a Decidable instance on the specification's side (limitations of RG1007). A proof term that is written inline in a specification is a part of that term, so a test that it names is counted and the registration is refused, which is the safe side.

In a file with a module header, the editor has an imported function as an axiom when its module does not export the value. The class of such a function is read from its type, so the editor refuses a registration that shares one with a result of Bool or BEq. The editor does not read below such a function. Where a test could be shared only below one, the editor reports the reading as incomplete under RG2005 and names lake lint, which has each value. That is where each side reaches such a function, or one side reaches one and the other side reaches a test.

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. A constant of type Bool is not a function and is not counted.

A registration that RG1007 refuses, and one with no decision kind, has no search and names no function.

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/RegulaPolicy/Decision.lean, lean/RegulaPolicy/Specification.lean, lean/RegulaPolicy/Domain.lean, lean/Regula/Collect.lean, lean/Regula/Contract.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. The decision of this rule is RegulaPolicy.sharedTestFailure, which declarationFailure runs after the recorded refusals of the contract. RegulaPolicy.checked_sharedTestFailure proves that it reports nothing exactly when the record names no function of the class boolean (RegulaPolicy.SharedTestOK). A name is in that class of the record exactly when the search read a definition of that class with that name (RegulaPolicy.mem_sharedNames_booleans), and the class is a stated condition on what was read of the definition (RegulaPolicy.SharedDefinition.class_eq_boolean_iff). The search that finds the definitions (Regula.Collect), and the reading of each, are operational.