)]}'
{
  "commit": "672ccdb7fceeed333ae1cbd13f1a0d815336ef83",
  "tree": "3c1928dbcaf12cc93d4991255ffa987e2644c5ac",
  "parents": [
    "0eea228cad3663a86246a562cc005aa1cc1ecc6a"
  ],
  "author": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Mon Aug 10 08:58:05 2026 +0000"
  },
  "committer": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Thu Aug 13 04:16:16 2026 +0000"
  },
  "message": "feat: certify the kernel\u0027s nested inductive elimination against a model\n\nThis PR makes the kernel check the declarations it produces for a nested inductive type. It eliminates the nesting exactly as before, and then requires that every type, constructor and recursor it declared is realised by a definition in an independently built model, and that every computation rule it makes definitional holds there. Nothing the kernel already did is removed.\n\nThe elimination, and the rewrite of its result back into the nested presentation, is the step the kernel does not otherwise justify. The restored types and rules are type checked, but nothing says the rules may be made definitional, that there is anything at all in which they hold. `Lean.Meta.NestedGen` now builds a second, independent account of the same declaration from the environment as it stood before any of it was added: the mutual model, the four bridge components relating each auxiliary copy to the type it stands for, the declaration\u0027s constants presented as definitions over that model, and a proof of every rule that does not already hold definitionally there.\n\nThe kernel states the rules itself rather than accepting them along with their proofs, so what gets proved is what is about to be believed. A definition is what makes them say something: were the model to hold the recursor the kernel declared, its rules would hold by the very fiat they are meant to justify. And the model is built before the declaration exists, so a rule cannot be discharged by the recursor it is meant to justify. The proofs are ordinary terms and the model an ordinary environment, so checking a certificate is ordinary type checking and adds nothing to the trusted code base; both go into a scratch environment that is discarded, so the only possible effect is to reject.\n\nAn unsafe declaration is declared uncertified: the bridges are definitions and the rule proofs are theorems, and neither may mention an unsafe constant.\n\nCo-Authored-By: Claude \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "7acba898530b90e18acae3b31c11296472e15d5a",
      "old_mode": 33188,
      "old_path": "src/Lean/Environment.lean",
      "new_id": "1fedf8b17e41eae73853aec14c9ba6a22d8e6feb",
      "new_mode": 33188,
      "new_path": "src/Lean/Environment.lean"
    },
    {
      "type": "modify",
      "old_id": "816489e3a1e0de0388a4034be437eef73d7b0ffb",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta.lean",
      "new_id": "b18166fc81eb2100cf4eb147a507c3cac11e5f99",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "a5744550fdfabfa0f71e27a26426881b68b94388",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/NestedInductive.lean"
    },
    {
      "type": "modify",
      "old_id": "118ed7badeb3940a4a2dc1dd6c2e11ca5a50c664",
      "old_mode": 33188,
      "old_path": "src/kernel/inductive.cpp",
      "new_id": "fe2022b4c6fc2f7fd108ef2aeb934e1191ba7ec4",
      "new_mode": 33188,
      "new_path": "src/kernel/inductive.cpp"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "7f05ab2462231120c0589373cc92abe63b1e3112",
      "new_mode": 33188,
      "new_path": "tests/elab/nested_inductive_certificate.lean"
    }
  ]
}