This page documents Regula 0.5.0. The latest release is Regula 0.11.1: this page in Regula 0.11.1.

RG4004: Teaching examples require authenticated compiler classification🔗

Category Documentation
Scope documentation fence
Subreason trusted-example

A fence marked lean-trusted-compiler did not elaborate warning-free with an authenticated compiler-trusting declaration: it contains no native proof, or authentication failed.

What to do. Use the marker only for an example that demonstrates native_decide, decide +native or bv_decide (or another authenticated compiler-trusting mechanism); otherwise remove it.

Requirement: A lean-trusted-compiler fence elaborates warning-free and contains an authenticated compiler-trusting declaration.
Reported in: Docs examples
Enforcement: Strict, like every rule: see how rules are enforced.

Checked example🔗

Violating input

✗ Rejecteddocs/Example.mdsource examples/rules/RG4004/Violation.md

<!-- lean-trusted-compiler -->
```lean
/-! # Reflexivity

Reflexivity for every natural number. -/
theorem reflexive (n : Nat) : n = n := rfl
```

Findings of the violating run

RG4004 error violation documentation example

Subject Example.md:2 at project Example.md:2

trusted marker found no compiler-trusting declaration

Correction

Change to docs/Example.md

- <!-- lean-trusted-compiler -->
  ```lean
  /-! # Reflexivity
  
  ⋯ 3 unchanged lines

✓ Passesdocs/Example.mdsource examples/rules/RG4004/Fixed.md

```lean
/-! # Reflexivity

Reflexivity for every natural number. -/
theorem reflexive (n : Nat) : n = n := rfl
```

The correction labels the same kernel proof as a positive example rather than as native teaching.

Checked by a documentation fence audit of <example>/docs: violating run rejected, corrected run completed.

How to fix it🔗

Remove the marker from an example that is an ordinary kernel proof; it is then checked as a positive example.
For a genuine teaching example, keep the native proof and import only the module that provides its tactic (for example import Init, or import Std.Tactic.BVDecide for bv_decide).

Why it matters🔗

Conforming claims reject compiler-trusting proofs (RG1004). A teaching fence is how the documentation shows one: it is classified and never counts as a conforming positive. A marker on an ordinary example would hide it from positive checking.

What triggers it🔗

A teaching fence must elaborate warning-free and the checker must authenticate at least one compiler-trusting declaration in it, using the same fresh-frontend evidence as RG1004. If none is found, or authentication fails, the fence is rejected with applicability trusted-example.

The fence is also rejected, with the underlying finding, when any declaration in it fails the declaration rules under the teaching request (for example RG1001 for an axiom or RG1006 for an unsafe or partial declaration).

What a passing result establishes🔗

The teaching fence elaborated warning-free and contains an authenticated compiler-trusting declaration.

It does not establish:

Any conformance of the teaching example; it is classified, never counted as a positive proof.

It leaves these review obligations open: R-QUALIFY.

Configuration and exceptions🔗

There is no name-based allowlist for native proofs; authentication is required for every teaching fence.

Limitations and unsupported cases🔗

Teaching fences are re-elaborated for authentication, so their imports are paid twice; keep them small.

Sources🔗

Normative clauses: standard §7.7 Check Lean Documentation Verbatim
Checklist rows: DOC-05
Detector, policy and proof sources: lean/Regula/Checker/Documentation.lean, lean/Regula/Checker/Frontend.lean, lean/RegulaPolicy/Decision.lean
Proved linkage: RegulaPolicy.checked_memberFoundation and Regula.Checker.Policy.labelOf_member.