)]}'
{
  "commit": "8e51c01311160b54c2a2701f7ee75f650d97cd0c",
  "tree": "351df68c35a6d0796493506744bba3d751027cd7",
  "parents": [
    "c1a8dfd916f12dc4ca7c150318106e144598db8c"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Oct 30 02:43:13 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Oct 30 02:51:11 2026 +0000"
  },
  "message": "perf: make the `Expr` hash combinator a bijection in each argument\n\nThis PR fixes a quadratic slowdown in the kernel when checking terms that contain long chains of the same application, such as `\"ff…f\" \u003d String.ofList (List.replicate n \u0027f\u0027)`.\n\n`Expr` stores a 32-bit hash. The hash of `f a` was the low 32 bits of `mixHash` applied to the data of `f` and `a`. Truncating to 32 bits makes the map from the hash of `a` to the hash of `f a` non-injective. Iterating such a map, as in `f a`, `f (f a)`, `f (f (f a))`, ..., enters a cycle after about 2^16 steps on average (13,146 cells for `\u0027f\u0027`). From then on, chains of different lengths share hashes, each lookup in the kernel caches compares them structurally, and the check becomes quadratic.\n\nThis PR adds `mixHash32 : UInt32 → UInt32 → UInt32`, based on the block step of `MurmurHash3_x86_32`. With either argument fixed, it is a bijection in the other. `Expr.data` now uses it to combine the hashes of subterms. Then `hash (fⁿ a) \u003d hash (fⁿ⁺ᵏ a)` implies `hash a \u003d hash (fᵏ a)`, so the chain can only repeat by returning to the hash of `a`, which takes about 2^31 steps on average. The PR also:\n* gives `lam` and `forallE` distinct tags; before, `fun x : A \u003d\u003e b` and `∀ x : A, b` always had the same hash,\n* includes the `nondep` flag of `letE` in its hash, and\n* no longer mixes `approxDepth` into the hash.\n\nInstructions for the kernel check of `\"ff…f\" \u003d String.ofList (List.replicate n \u0027f\u0027)` (excluding `import Lean`):\n\n| n | Before | After |\n|---|---|---|\n| 10,000 | 1.07G | 1.07G |\n| 20,000 | 7.22G | 2.14G |\n| 40,000 | 201.4G | 4.28G |\n| 80,000 | 2,746G | 8.56G |\n| 160,000 | \u003ctimeout\u003e | 17.1G |\n| 320,000 | \u003ctimeout\u003e | 34.2G |\n\nOn Mathlib, the change costs +0.08% instructions, with no change in memory.\n\nWe are considering increasing the `Expr` hash to 64 bits. That would make accidental collisions negligible, but it adds 8 bytes to every `Expr` node. On Mathlib, this increases the total size of the `.olean` files by 17% (+984 MB), memory use by about 3.5%, and CPU time by about 1%.\n\nCloses #16103\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "ebe3b4ff14629d9b20b4a47cea5f5e7ad53a34e2",
      "old_mode": 33188,
      "old_path": "src/Init/Prelude.lean",
      "new_id": "2c81501c437a1ed436f9cab99c9d68da0d7434dc",
      "new_mode": 33188,
      "new_path": "src/Init/Prelude.lean"
    },
    {
      "type": "modify",
      "old_id": "86f4a1e0436e629e314cbd18aa7be504d3ca2bc2",
      "old_mode": 33188,
      "old_path": "src/Lean/Expr.lean",
      "new_id": "e901ae93c912afa458e3337617b82a2dd47acebf",
      "new_mode": 33188,
      "new_path": "src/Lean/Expr.lean"
    },
    {
      "type": "modify",
      "old_id": "9e2e71ae7dcf379bbe5dc678afa36b8c02f52b5a",
      "old_mode": 33188,
      "old_path": "src/include/lean/lean.h",
      "new_id": "95fbc83eb2540e5dd905c7be8280a2189a4c6c86",
      "new_mode": 33188,
      "new_path": "src/include/lean/lean.h"
    },
    {
      "type": "modify",
      "old_id": "e1c15582016df5bc5346bfc224c569181917e4f1",
      "old_mode": 33188,
      "old_path": "src/kernel/expr.cpp",
      "new_id": "48be4dc637e66be12ef27029cd252a3c6b1f3630",
      "new_mode": 33188,
      "new_path": "src/kernel/expr.cpp"
    },
    {
      "type": "modify",
      "old_id": "105ec6ca67d3ed18b0e64dffd8a96a256697490e",
      "old_mode": 33188,
      "old_path": "src/runtime/hash.h",
      "new_id": "7f1be748160c7293300a3ed8ea42f02a79f2e208",
      "new_mode": 33188,
      "new_path": "src/runtime/hash.h"
    },
    {
      "type": "modify",
      "old_id": "9b2dd0c4b376418cc8ea398950117b35d7b2f4c3",
      "old_mode": 33188,
      "old_path": "src/runtime/object.cpp",
      "new_id": "72163f2365b18530ffef0d183d15d2845dcacd9d",
      "new_mode": 33188,
      "new_path": "src/runtime/object.cpp"
    },
    {
      "type": "modify",
      "old_id": "3baec9ac0fdd7e712e519058688bded2cada4bf1",
      "old_mode": 33188,
      "old_path": "stage0/src/stdlib_flags.h",
      "new_id": "d96a46b866db79bc86653c7b95882a61bcd85113",
      "new_mode": 33188,
      "new_path": "stage0/src/stdlib_flags.h"
    },
    {
      "type": "modify",
      "old_id": "6c3f3fe6934ed739e8cfbc574177c7de891fc975",
      "old_mode": 33188,
      "old_path": "tests/compile/expr.lean.out.expected",
      "new_id": "411309cad9462ce73990b175dacc295ed8d2ecab",
      "new_mode": 33188,
      "new_path": "tests/compile/expr.lean.out.expected"
    },
    {
      "type": "modify",
      "old_id": "84d2251e5467dd621ebaeea6bb3955d28aa55d21",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_ematch_diag_2.lean",
      "new_id": "0a6258bd47d41428f6d1796df769a78e766005f0",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_ematch_diag_2.lean"
    },
    {
      "type": "modify",
      "old_id": "b6a29c58e607aba04eaa44b38f614937da82cf7f",
      "old_mode": 33188,
      "old_path": "tests/elab/issue_14576.lean",
      "new_id": "0743186d0429268c3b534a169b874547d86fe3a3",
      "new_mode": 33188,
      "new_path": "tests/elab/issue_14576.lean"
    },
    {
      "type": "modify",
      "old_id": "b82fd0828f981b6b8f2f566bd5d9ee323605d30f",
      "old_mode": 33188,
      "old_path": "tests/elab/kernel_is_def_eq_equiv_manager_1.lean",
      "new_id": "7cc44e34fe6a1653604bae325f1d02f3402cea51",
      "new_mode": 33188,
      "new_path": "tests/elab/kernel_is_def_eq_equiv_manager_1.lean"
    }
  ]
}