Create a store with a narrower axiom policy

Start a store that accepts only propext and Quot.sound, and read which axioms each accepted object uses.

Without --axioms, lema init gives a new store Lean’s three standard axioms: propext, Quot.sound and Classical.choice (decision 0028). Narrow the axiom policy when you want the store to refuse anything that relies on other axioms.

Before you start

• lema built, and a path for the new store that holds no store yet.
• A runtime configuration for lema serve.
• In the commands, $STORE is a directory that does not hold a store yet (lema init refuses an existing one), $CONFIG your runtime configuration and $SOCK the server’s socket.

Steps

1. Create the store with the policy you want:

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

   It prints created store, the path and the namespace ID. Separate the names with commas and no spaces: a space becomes part of the name. An empty list (--axioms '') allows no axioms at all.

   An axiom of the fixed floor is refused, and no store is created:

   lema: sorryAx is below the fixed floor; no policy allows it

   The floor is sorryAx, Lean.ofReduceBool, Lean.ofReduceNat, Lean.trustCompiler, any axiom with a _native name component (what native_decide adds), and unsafe constants.

2. Start the server and confirm the policy:

   lema serve --store $STORE --runtime $CONFIG --socket $SOCK &
   lema --socket $SOCK info

   info lists the policy under allowed_axioms.

3. Publish as usual. Kernel replay with the pinned Lean 4.34.1 kernel works out each declaration’s axiom footprint over its whole closure. If any object uses an axiom outside the policy, the whole submission is refused, and the error names the object and the axiom:

   <id> depends on Classical.choice, outside the store's axiom policy

   Some existing work needs the default policy. Std.Text’s UTF-8 validation uses Classical.choice through Lean’s own UTF-8 proofs, and so do some Init lemmas about fixed-width integers. A narrow store refuses objects that rely on them.

See which axioms an object uses

Each kernel receipt records its object’s axiom footprint.

1. Find the object’s ID through its alias:

   lema --socket $SOCK call find --params '{"prefix": "app."}'

2. Show the object:

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

   The response holds object, receipt and names. receipt.axioms is the footprint, for example ["Quot.sound","propext"], or [] for an object that uses no axiom.

Only declarations, records, families and externals have receipts. A statement, template, proof or satisfaction is accepted through a declaration that uses it, so its receipt is null: show that declaration instead. There is no query by axiom yet, so you read receipts one object at a time.

Moving to another policy

The policy is written to the store’s store.json when the store is created, and no command changes it. To work under another policy, create a new store and publish into it. Objects imported from another store are replayed and checked against the receiving store’s own policy. Receipts are never copied between stores.

To re-check every footprint against its receipt, see Re-check a store from scratch.