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=[] shared-through-types=[]

  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 test that only the declaration of the input type names is no part of the specification at any input. A kind compares accepts (f x) with spec x for each x. A change of the test changes which inputs there are, on the two sides together, and the comparison at an input is the one that it was. A specification that names the input type in another way can depend on the test at an input, and the test is counted.

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

The checker does not enter the declaration of the input type of the kind from the input (RegulaPolicy.StatementReading.reads). It reads the specification from the body of its function abstraction under its variable. When the specification is a definition, alone or applied to its variable alone, the search reads the body of that definition's value. It does not follow a projection of a field of the input back to the input type, or to the type that an abbrev input type unfolds to. It follows everything else as before.

The checker reads the acceptance predicate by the rule of a statement, the declaration of the result type included. A value of the result type occurs only in accepts (f x), so a test that the declaration of the result type names can be a part of that side.

A test that the two sides share only through the declaration of the input type, such as a test that an invariant of a field of the input states, is not counted. The report names it after shared-through-types=. A specification that names the input type in any other way, or that reads a field whose result type has such an invariant and is not the input type, reaches the test, and it is counted.

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, apart from the declaration of the input type that the search enters from the input.

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.

• Anything about a test that the two sides share only through the declaration of the input type (shared-through-types=), such as a test that an invariant of the input states. Whether the invariant is the intended one remains review.

• 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, apart from the declaration of the input type that it enters from the input, and from the acceptance predicate. From the implementation it follows the types of constants and the unfoldable values of definitions. 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 it searches the two sides, finds no shared test, and one of two cases holds. Each side reaches an imported constant with no value in the file, a function or not, whose value the search of that side would read. Or one side reaches one, and the other side reaches a test that the rule counts. A specification that is such an imported definition, alone or applied to its variable alone, is such a constant: the editor does not read it through its type, since lake lint reads its body.

A definition that the body of the specification names among other terms, or that the value of a named specification names, has its type read. Where that type names the input type, the search reads the declaration of the input type there. So fun input => AdmitSpec input ∧ 0 < input.amount reads the declaration of the type of input, and plain AdmitSpec does not.

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 type that the specification passes to a function that is no projection of a field is read, with its declaration: the reading cannot tell a function that quantifies over its type argument from one that does not. So xs[i] reads the element type of an array, which it passes to the instance of GetElem. A registration whose specification indexes a collection of a type whose invariant names a test of the implementation is refused.

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/RegulaPolicy/StatementReading.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). What the search follows from each constant of the specification is the decision RegulaPolicy.StatementReading.reads, with the two-way kind RegulaPolicy.StatementReading.checked_reads, and RegulaPolicy.StatementReading.reading closes it over the records of the observing pass (reading_some). It reaches only what the rule of a statement reaches (read_subset_withTypes), so it refuses no registration that the earlier search accepted. What the rule reaches and the reading does not, the rule reaches from a constant of the input type that the reading does not reach (RegulaPolicy.StatementReading.through_input), and a name is shared only through the input type exactly as RegulaPolicy.mem_sharedNames_throughTypes states. The acceptance predicate is read by the rule of a statement. A record that names no test has no test that the reading of the specification reaches and that the implementation or the acceptance predicate reaches (RegulaPolicy.StatementReading.no_shared_test). The observing pass, the search for the implementation and the reading of each definition (Regula.Collect) are operational.