Axiom policy and the fixed floor

Which axioms an accepted object may depend on, how a store's policy is set, and how the footprint is audited at replay.

Every accepted object has an axiom footprint: the axioms its closure depends on, as the pinned Lean 4.34.1 kernel’s replay reports them. Two limits apply to it. The fixed floor is a set of axioms and constants that no store accepts. The axiom policy is the set of axioms a store allows above the floor, recorded when the store is created.

Objects carry no axiom claims, so neither the floor nor a policy is part of any ID (decision 0027).

The fixed floor

The floor is checked at every stage:

• the exporter refuses a draft constant whose footprint is below the floor (“assumption below the fixed floor”), an unsafe declaration, and an unsafe or below-floor external;
• the decoder installs every definition as safe, refuses an unsafe external, and refuses any installed constant or external whose footprint is below the floor;
• the Rust side refuses a replay result or a stored receipt that lists a floor axiom, before it consults any policy;
• lema init --axioms refuses to list a floor axiom: “<axiom> is below the fixed floor; no policy allows it”.

Stored declarations cannot carry implemented_by or extern attributes. The Init functions that do (Array.foldlM, for example) affect only execution, so they are assumed compiler and runtime trust, not refused (docs/identity.md §7).

The default policy

A store created by lema init without --axioms allows Lean’s three standard axioms:

A well-founded definition on a Nat measure brings propext and Quot.sound from its termination proof. Classical.choice reaches Std.Text’s validation through Lean’s proof that its UTF-8 validator decides IsValidUTF8, and Init lemmas on fixed-width integers such as Int64.toInt_div_of_ne_left depend on it.

This is lema_store::standard_policy (decision 0028). Through M2 the default was the narrower propext and Quot.sound. Policy::default() in crates/lema-check stays that narrower policy: its tests use it, and engine.rs is part of the translation identity that keys module caches.

Choosing a policy

lema init --store $STORE                            # propext, Quot.sound, Classical.choice
lema init --store $STORE --axioms propext,Quot.sound

• --axioms takes a comma-separated list. Empty items are ignored, so an empty list allows no axioms.
• A floor axiom in the list is refused.
• The store records its policy in store.json when it is created, and no command changes it. Editing store.json would be an operator action outside the tools. A policy change would re-address nothing, but it would require re-checking the affected receipts against the new ceiling, and no tool does that yet.
• The info method reports the policy as allowed_axioms.

Create a store with a narrower axiom policy gives the steps.

How the footprint is audited

1. Elaboration: the exporter runs collectAxioms on every draft constant and refuses floor axioms. This output is untrusted, because it shares a process with the draft.
2. Replay: the decoder re-adds each declaration with the kernel (addDeclCore), then runs collectAxioms on every installed constant and every listed external, refuses floor axioms, and writes replay-result.json (lema.replay-result/v2).
3. Judging the result (engine::interpret): the Rust side checks that replay ran under the namespace’s Lean and installed exactly the payload’s constants, takes the union of the footprints of each object’s kernel names, refuses any axiom below the floor or outside the store’s policy, and writes one receipt per declaration, record, family and external, with its footprint in axioms.
4. Accepting (check_policy in crates/lema-store): every receipt the submission uses, including receipts reused from a cached module, must name this object and namespace, be a kernel receipt from the pinned checker, and have a footprint above the floor and within this store’s policy.
5. Re-checking: lema reverify replays everything accepted from scratch, without modules, and requires every footprint to equal its receipt’s.

The kernel’s verdict comes only from a file the decoder writes at the kernel boundary, never from log text. A kernel that runs out of a resource gives an inconclusive result, not a refusal.

Reading a footprint

A receipt records the footprint, not the policy. show returns it:

lema --socket $SOCK call show --params '{"id":"<object id>"}'

There is no filter by axiom yet. The pages that lema site build writes show each declaration’s actual footprint, with the store’s policy beside it as the ceiling.

Choice and running code

The policy is a footprint ceiling, not a rule about proofs only. Classical.choice is accepted in any object, including noncomputable definitions (with Classical.choose, or an if on a classical decision). Such definitions can be used in specifications but cannot run. Acceptance does nothing to keep choice out of executed code; two other checks do:

Classical.choose and Classical.propDecidable reach execution only through the compiler, so their refusal is assumed, not tested by the vocabulary. Kernel evaluation (decide, rfl) does not reduce choice, so a proof that must compute stays constructive.

The restricted Lean reference lists the vocabulary’s rules, and Checked, tested and assumed explains the three evidence words.