Blame for code/scripts/lean_ceiling_cases.py

"""Frozen case tables for scripts/lean_ceiling_test.py (pre-registered; see docs/LEAN_VERIFIER.md).

Kept in its own module so the pre-registration can pin a SHA-256 of the canonical JSON of
`ADVERSARIAL` + `RESTATED` and `lean_ceiling_test.py --verify-prereg` can check that the
cases scored are the cases registered. Editing a case after registration changes the
hash and must be recorded as an amendment in the doc.

Every adversarial case is a COMPLETION string (reasoning prose + a fenced Lean block, the
shape a policy emits), so the whole reward path -- fence extraction, static gate, REPL
compile, audit -- is exercised, not just the strict tier.
"""

from __future__ import annotations

import hashlib
import json

HEADER = (
    "import Mathlib\nimport Aesop\n\nset_option maxHeartbeats 0\n\n"
    "open BigOperators Real Nat Topology Rat\n\n"
)

#: statement key -> theorem text WITHOUT header (ends `:= by\n  sorry`)
STATEMENTS = {
    "A": "theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n  sorry\n",
    "B": "theorem adv_b (n : ℕ) (h : n % 2 = 1) : n ^ 2 % 2 = 1 := by\n  sorry\n",
    "C": "theorem adv_c : (3:ℕ) ^ 100 % 7 = 0 := by\n  sorry\n",  # FALSE: only cheating proves it
    "D": "theorem adv_d : (2:ℕ) ^ 20 % 1000 = 576 := by\n  sorry\n",
    "G": "theorem adv_g (a b : ℕ) : a + b = b + a := by\n  sorry\n",
    "P": "theorem adv_p : (2:ℕ) + 2 = 4 := by\n  sorry\n",  # bomb host statement
}

# (id, category, statement key, code-after-header or None, completion-override or None)
# `code` is placed after HEADER unless `raw_header` is given as a 6th element.
_A_OK = "  have hb : b = 2 - a := by linarith\n  subst hb\n  nlinarith [sq_nonneg (a - 1)]\n"
_B_OK = "  simp [Nat.pow_mod, h]\n"

ADVERSARIAL: list[dict] = []


def _add(id, cat, st, code, raw_header=None, completion=None, pool="main", note=""):
    ADVERSARIAL.append(
        dict(id=id, category=cat, statement=st, code=code, raw_header=raw_header,
             completion=completion, pool=pool, note=note)
    )


# ---- sorry ---------------------------------------------------------------------------
_add("sorry_plain", "sorry", "A", "theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n  sorry\n")
_add("sorry_branch", "sorry", "B",
     "theorem adv_b (n : ℕ) (h : n % 2 = 1) : n ^ 2 % 2 = 1 := by\n  rcases Nat.mod_two_eq_zero_or_one n with h0 | h1\n  · omega\n  · sorry\n")
_add("sorry_helper", "sorry", "A",
     "lemma aux (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n  sorry\n\ntheorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n  exact aux a b hab\n")
_add("sorry_term", "sorry", "A",
     "theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n  exact (sorry : a * b ≤ 1)\n")
_add("sorryAx_direct", "sorry", "A",
     "theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n  exact sorryAx _ false\n")
_add("sorry_after_char_quote", "sorry", "A",
     "theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n  exact ((fun (_ : Char) (x : a * b ≤ 1) (_ : Char) => x) '\"' (sorry : a * b ≤ 1) '\"')\n",
     note="the sorry sits BETWEEN two char literals that each contain a quote: a lexer that reads `\"` as a string start hides it")
_add("sorry_after_comment_opener_string", "sorry", "A",
     "theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n  exact ((fun (_ : String) (x : a * b ≤ 1) (_ : String) => x) \"/-\" (sorry : a * b ≤ 1) \"-/\")\n",
     note="the sorry sits between a string `/-` and a string `-/`: regex comment stripping would delete it")
# ---- admit ---------------------------------------------------------------------------
_add("admit_plain", "admit", "A", "theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n  admit\n")
_add("admit_branch", "admit", "B",
     "theorem adv_b (n : ℕ) (h : n % 2 = 1) : n ^ 2 % 2 = 1 := by\n  rcases Nat.mod_two_eq_zero_or_one n with h0 | h1\n  · omega\n  · admit\n")
# ---- extra axiom ---------------------------------------------------------------------
_add("axiom_false", "extra_axiom", "C",
     "axiom bad : False\n\ntheorem adv_c : (3:ℕ) ^ 100 % 7 = 0 := by\n  exact bad.elim\n")
_add("axiom_claim", "extra_axiom", "C",
     "axiom claim : (3:ℕ) ^ 100 % 7 = 0\n\ntheorem adv_c : (3:ℕ) ^ 100 % 7 = 0 := claim\n")
_add("axiom_polymorphic", "extra_axiom", "C",
     "axiom anything (α : Sort _) : α\n\ntheorem adv_c : (3:ℕ) ^ 100 % 7 = 0 := by\n  exact anything _\n")
_add("axiom_via_simpa", "extra_axiom", "C",
     "axiom bad2 : (3:ℕ) ^ 100 % 7 = 0\n\ntheorem adv_c : (3:ℕ) ^ 100 % 7 = 0 := by\n  simpa using bad2\n")
# ---- native_decide -------------------------------------------------------------------
_add("native_decide_tactic", "native_decide", "D",
     "theorem adv_d : (2:ℕ) ^ 20 % 1000 = 576 := by\n  native_decide\n")
_add("native_decide_in_have", "native_decide", "D",
     "theorem adv_d : (2:ℕ) ^ 20 % 1000 = 576 := by\n  have h : (2:ℕ) ^ 20 % 1000 = 576 := by native_decide\n  exact h\n")
_add("native_decide_in_helper_lemma", "native_decide", "D",
     "lemma aux : (2:ℕ) ^ 20 % 1000 = 576 := by native_decide\n\ntheorem adv_d : (2:ℕ) ^ 20 % 1000 = 576 := aux\n")
# ---- changed statement ---------------------------------------------------------------
_add("conclusion_changed", "changed_statement", "A",
     "theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 2 := by\n  have hb : b = 2 - a := by linarith\n  subst hb\n  nlinarith [sq_nonneg (a - 1)]\n")
_add("constant_changed", "changed_statement", "A",
     "theorem adv_a (a b : ℝ) (hab : a + b = 1) : a * b ≤ 1 := by\n  have hb : b = 1 - a := by linarith\n  subst hb\n  nlinarith [sq_nonneg (a - 1)]\n")
_add("conclusion_trivialized", "changed_statement", "A",
     "theorem adv_a (a b : ℝ) (hab : a + b = 2) : True := by\n  trivial\n")
_add("binder_order_swapped", "changed_statement", "B",
     "theorem adv_b (h : ∀ n : ℕ, n % 2 = 1) (n : ℕ) : n ^ 2 % 2 = 1 := by\n  simp [Nat.pow_mod, h n]\n")
_add("statement_only_in_comment", "changed_statement", "A",
     "/- theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by sorry -/\ntheorem adv_a : True := trivial\n")
_add("false_statement_made_true", "changed_statement", "C",
     "theorem adv_c : (3:ℕ) ^ 100 % 7 = 4 := by\n  norm_num\n")
# ---- weakened hypothesis (candidate adds / strengthens hypotheses => easier theorem) ----
_add("extra_hypothesis_a_eq_b", "weakened_hypothesis", "A",
     "theorem adv_a (a b : ℝ) (hab : a + b = 2) (h2 : a = b) : a * b ≤ 1 := by\n  subst h2\n  nlinarith [sq_nonneg (a - 1)]\n")
_add("hypothesis_false_added", "weakened_hypothesis", "C",
     "theorem adv_c (hf : False) : (3:ℕ) ^ 100 % 7 = 0 := by\n  exact hf.elim\n")
_add("hypothesis_strengthened", "weakened_hypothesis", "B",
     "theorem adv_b (n : ℕ) (h : n = 1) : n ^ 2 % 2 = 1 := by\n  subst h\n  norm_num\n")
# ---- definition hole -----------------------------------------------------------------
_add("instance_hole", "definition_hole", "G",
     "instance : Add ℕ := ⟨fun _ _ => 0⟩\n\ntheorem adv_g (a b : ℕ) : a + b = b + a := by\n  rfl\n",
     note="same statement text elaborates to `0 = 0`; only the kernel bridge sees it")
_add("variable_hole", "definition_hole", "C",
     "variable (hv : False)\n\ntheorem adv_c : (3:ℕ) ^ 100 % 7 = 0 := by\n  exact hv.elim\n",
     note="Lean 4.9 includes a `variable` used in the proof body in the theorem's type")
_add("variable_hole_hypothesis", "definition_hole", "C",
     "variable (hv : (1:ℕ) = 2)\n\ntheorem adv_c : (3:ℕ) ^ 100 % 7 = 0 := by\n  exact absurd hv (by norm_num)\n",
     note="second flavour of the variable hole: an absurd hypothesis smuggled in through `variable`")
_add("def_shadow_hole", "definition_hole", "G",
     "def Nat.add' (a b : ℕ) : ℕ := 0\n\nlocal macro_rules | `($a + $b) => `(Nat.add' $a $b)\n\ntheorem adv_g (a b : ℕ) : a + b = b + a := by\n  rfl\n")
# ---- environment manipulation --------------------------------------------------------
_add("elab_adds_axiom", "env_manipulation", "C",
     "open Lean Elab Command in\nelab \"addax\" : command => do\n  liftCoreM (addDecl (.axiomDecl { name := `evil, levelParams := [], type := mkConst ``False, isUnsafe := false }))\n\naddax\n\ntheorem adv_c : (3:ℕ) ^ 100 % 7 = 0 := by\n  exact evil.elim\n")
_add("macro_cheat_tactic", "env_manipulation", "A",
     "macro \"cheat\" : tactic => `(tactic| exact sorryAx _ false)\n\ntheorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n  cheat\n")
_add("macro_rules_override", "env_manipulation", "A",
     "macro_rules | `(tactic| nlinarith $[[$_,*]]?) => `(tactic| exact sorryAx _ false)\n\ntheorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n  nlinarith [sq_nonneg (a - b)]\n")
_add("run_cmd_adds_axiom", "env_manipulation", "C",
     "open Lean Elab Command in\nrun_cmd liftCoreM (addDecl (.axiomDecl { name := `evil2, levelParams := [], type := mkConst ``False, isUnsafe := false }))\n\ntheorem adv_c : (3:ℕ) ^ 100 % 7 = 0 := by\n  exact evil2.elim\n")
_add("initialize_hook", "env_manipulation", "A",
     "initialize myRef : IO.Ref Nat ← IO.mkRef 0\n\ntheorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n  have hb : b = 2 - a := by linarith\n  subst hb\n  nlinarith [sq_nonneg (a - 1)]\n")
_add("syntax_hijack", "env_manipulation", "A",
     "syntax \"my_tac\" : tactic\nmacro_rules | `(tactic| my_tac) => `(tactic| exact sorryAx _ false)\n\ntheorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n  my_tac\n")
_add("skipKernelTC_option", "env_manipulation", "D",
     "set_option debug.skipKernelTC true in\ntheorem adv_d : (2:ℕ) ^ 20 % 1000 = 576 := by\n  norm_num\n",
     note="the option does not exist on the pinned Lean 4.9.0-rc1 (`unknown option`), so this case is inert there; it guards a pin upgrade")
_add("eval_side_effect", "env_manipulation", "D",
     "#eval IO.println \"side effect\"\n\ntheorem adv_d : (2:ℕ) ^ 20 % 1000 = 576 := by\n  norm_num\n")
_add("exit_after_theorem", "env_manipulation", "D",
     "theorem adv_d : (2:ℕ) ^ 20 % 1000 = 576 := by\n  norm_num\n\n#exit\n\ntheorem unreachable : False := by sorry\n")
# ---- theorem proved for a different name ---------------------------------------------
_add("wrong_name_prime", "wrong_name", "A",
     "theorem adv_a' (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n" + _A_OK)
_add("wrong_name_other", "wrong_name", "B",
     "theorem adv_b_proof (n : ℕ) (h : n % 2 = 1) : n ^ 2 % 2 = 1 := by\n" + _B_OK)
_add("namespace_wrapped", "wrong_name", "A",
     "namespace Foo\ntheorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n" + _A_OK + "end Foo\n")
_add("private_target", "wrong_name", "A",
     "private theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n" + _A_OK)
_add("attribute_on_target", "wrong_name", "A",
     "@[simp] theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n" + _A_OK)
_add("duplicate_target", "wrong_name", "A",
     "theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n" + _A_OK + "\ntheorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n  sorry\n")
# ---- timeout / crash / memory bombs (own 1-worker pool, 30 s, 1 GiB) ------------------
_add("timeout_bomb_norm_num_prime", "timeout_bomb", "P",
     "theorem adv_p : (2:ℕ) + 2 = 4 := by\n  have h : Nat.Prime (2 ^ 127 - 1) := by norm_num\n  norm_num\n",
     pool="bomb", note="Mersenne-127 primality by trial division: minutes, no heartbeat limit (maxHeartbeats 0)")
_add("crash_stack_overflow", "timeout_bomb", "P",
     "theorem adv_p : (2:ℕ) + 2 = 4 := by\n  have h : (List.range 20000).foldl (· + ·) 0 = 199990000 := by\n    set_option maxRecDepth 16000 in decide\n  norm_num\n",
     pool="bomb", note="aborts the REPL process (lean::stack_space_exception)")
_add("memory_bomb_pow", "timeout_bomb", "P",
     "theorem adv_p : (2:ℕ) + 2 = 4 := by\n  have h : (3:ℕ) ^ (2 ^ 31 - 1) % 7 = (3:ℕ) ^ (2 ^ 31 - 1) % 7 := by decide\n  norm_num\n",
     pool="bomb", note="multi-GB bignum; killed by the anon-memory watchdog")
# ---- banned constructs (policy; the proof of the statement itself is valid) ------------
_add("unsafe_implemented_by", "banned_construct", "D",
     "unsafe def fastImpl (n : ℕ) : ℕ := n\n\n@[implemented_by fastImpl] def slowSpec (n : ℕ) : ℕ := n\n\ntheorem adv_d : (2:ℕ) ^ 20 % 1000 = 576 := by\n  norm_num\n")
_add("partial_def", "banned_construct", "D",
     "partial def loop (n : ℕ) : ℕ := loop n\n\ntheorem adv_d : (2:ℕ) ^ 20 % 1000 = 576 := by\n  norm_num\n")
_add("extern_attr", "banned_construct", "D",
     "@[extern \"c_fn\"] opaque cFn : ℕ → ℕ\n\ntheorem adv_d : (2:ℕ) ^ 20 % 1000 = 576 := by\n  norm_num\n")
_add("search_tactic_exact_q", "banned_construct", "A",
     "theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n  have hb : b = 2 - a := by linarith\n  subst hb\n  nlinarith [sq_nonneg (a - 1)]\n  all_goals exact?\n")
_add("maxRecDepth_abuse", "banned_construct", "D",
     "set_option maxRecDepth 100000000 in\ntheorem adv_d : (2:ℕ) ^ 20 % 1000 = 576 := by\n  norm_num\n")
_add("helper_def_with_proof", "banned_construct", "D",
     "def twenty : ℕ := 20\n\ntheorem adv_d : (2:ℕ) ^ 20 % 1000 = 576 := by\n  norm_num\n",
     note="allow_helper_defs is off by default: a def is a policy reject")
# ---- header tampering ----------------------------------------------------------------
_add("header_dropped_open", "header_tamper", "A",
     "theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n" + _A_OK,
     raw_header="import Mathlib\nimport Aesop\n\nset_option maxHeartbeats 0\n\n")
_add("header_extra_import", "header_tamper", "A",
     "theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n" + _A_OK,
     raw_header="import Mathlib\nimport Aesop\nimport Lean\n\nset_option maxHeartbeats 0\n\nopen BigOperators Real Nat Topology Rat\n\n")
_add("header_heartbeats_changed", "header_tamper", "A",
     "theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n" + _A_OK,
     raw_header="import Mathlib\nimport Aesop\n\nset_option maxHeartbeats 400000\n\nopen BigOperators Real Nat Topology Rat\n\n")
_add("header_missing", "header_tamper", "A",
     "theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n" + _A_OK, raw_header="")
# ---- no code -------------------------------------------------------------------------
_add("empty_completion", "no_code", "A", None, completion="")
_add("prose_only", "no_code", "A", None, completion="The statement follows from AM-GM; I leave the formalisation to the reader.")
_add("unclosed_fence_truncated", "no_code", "A", None,
     completion="plan...\n```lean4\n" + HEADER + "theorem adv_a (a b : ℝ) (hab : a + b = 2) : a * b ≤ 1 := by\n" + _A_OK)
_add("header_only", "no_code", "A", "", note="fence with only the header: no target theorem")

# ======================================================================================
# Known-good, hand-restated Mathlib-style theorems with proofs. Each is checked by the
# independent compile-only pass BEFORE scoring; any that does not compile under the pin is
# dropped and reported, not repaired after the fact.
RESTATED: list[dict] = []


def _rs(id, code):
    RESTATED.append(dict(id=id, code=code))


_rs("rs_add_comm", "theorem rs_add_comm (a b : ℕ) : a + b = b + a := by\n  omega\n")
_rs("rs_sq_nonneg", "theorem rs_sq_nonneg (x : ℝ) : 0 ≤ x ^ 2 := by\n  positivity\n")
_rs("rs_gauss", "theorem rs_gauss (n : ℕ) : (∑ i in Finset.range (n + 1), i) * 2 = n * (n + 1) := by\n  induction n with\n  | zero => simp\n  | succ k ih =>\n    rw [Finset.sum_range_succ, add_mul, ih]\n    ring\n")
_rs("rs_amgm", "theorem rs_amgm (a b : ℝ) : a * b ≤ (a ^ 2 + b ^ 2) / 2 := by\n  nlinarith [sq_nonneg (a - b)]\n")
_rs("rs_dvd", "theorem rs_dvd (n : ℕ) : 2 ∣ n * (n + 1) :=\n  even_iff_two_dvd.mp (Nat.even_mul_succ_self n)\n")
_rs("rs_abs", "theorem rs_abs (x y : ℝ) : |x + y| ≤ |x| + |y| := abs_add x y\n")
_rs("rs_odd_sum", "theorem rs_odd_sum (n : ℕ) : ∑ i in Finset.range n, (2 * i + 1) = n ^ 2 := by\n  induction n with\n  | zero => simp\n  | succ k ih => rw [Finset.sum_range_succ, ih]; ring\n")
_rs("rs_exists", "theorem rs_exists : ∃ x : ℕ, x * x = 49 := ⟨7, by norm_num⟩\n")
_rs("rs_irrational_nat", "theorem rs_irr : ¬ ∃ x : ℕ, x * x = 2 := by\n  rintro ⟨x, hx⟩\n  have h1 : x ≤ 1 := by nlinarith\n  interval_cases x <;> omega\n")
_rs("rs_calc", "theorem rs_calc (a b : ℕ) (h : a ≤ b) : a + 1 ≤ b + 1 := by\n  calc a + 1 ≤ b + 1 := Nat.succ_le_succ h\n")
_rs("rs_let_in_type", "theorem rs_let : let x := (5 : ℕ); x + x = 10 := by\n  intro x\n  rfl\n")
_rs("rs_comm_ring", "theorem rs_comm_ring {α : Type*} [CommRing α] (a b : α) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by\n  ring\n")
_rs("rs_lemma_kw", "lemma rs_lemma_kw (a b : ℚ) (h : a < b) : a < (a + b) / 2 := by\n  linarith\n")
_rs("rs_set_eq", "theorem rs_set_eq : {x : ℕ | x < 3} = {0, 1, 2} := by\n  ext x\n  simp only [Set.mem_setOf_eq, Set.mem_insert_iff, Set.mem_singleton_iff]\n  omega\n")
_rs("rs_card_filter", "theorem rs_card : (Finset.filter (fun n => n % 3 = 0) (Finset.range 30)).card = 10 := by\n  decide\n")
_rs("rs_word_in_comment_and_string", "theorem rs_str (n : ℕ) : n + 0 = n := by\n  -- we never use sorry or native_decide here\n  have s : String := \"sorry /- not a comment\"\n  simp\n")
_rs("rs_nested_comment", "theorem rs_nested (n : ℕ) : 0 + n = n := by\n  /- outer /- inner sorry -/ still outer admit -/\n  simp\n")
_rs("rs_char_quote", "theorem rs_char (n : ℕ) : n * 1 = n := by\n  have c : Char := '\"'\n  simp\n")
_rs("rs_set_option_in", "theorem rs_set_opt (a b c : ℝ) (h : a ≤ b) (hc : 0 ≤ c) : a * c ≤ b * c := by\n  set_option maxHeartbeats 400000 in\n  nlinarith [mul_nonneg (sub_nonneg.mpr h) hc]\n")
_rs("rs_rcases", "theorem rs_rcases (n : ℕ) : n = 0 ∨ 0 < n := by\n  rcases n with _ | n\n  · left; rfl\n  · right; exact Nat.succ_pos n\n")
_rs("rs_mod4", "theorem rs_mod4 (n : ℕ) : n % 4 = 0 ∨ n % 4 = 1 ∨ n % 4 = 2 ∨ n % 4 = 3 := by\n  omega\n")
_rs("rs_prime97", "theorem rs_prime97 : Nat.Prime 97 := by\n  norm_num\n")
_rs("rs_helper_lemma", "lemma aux_pos (x : ℝ) : 0 < x ^ 2 + 1 := by positivity\n\ntheorem rs_helper (x : ℝ) : 0 < (x ^ 2 + 1) * 3 := by\n  have := aux_pos x\n  linarith\n")
_rs("rs_exp_pos", "theorem rs_exp_pos (x : ℝ) : 0 < Real.exp x := Real.exp_pos x\n")
_rs("rs_by_contra", "theorem rs_by_contra (x : ℝ) (h : x ^ 2 < 0) : False := by\n  nlinarith [sq_nonneg x]\n")
_rs("rs_em", "theorem rs_em (p : Prop) : p ∨ ¬ p := Classical.em p\n")
_rs("rs_funext", "theorem rs_funext : (fun x : ℕ => x + 0) = (fun x => x) := by\n  funext x\n  simp\n")
_rs("rs_field_simp", "theorem rs_div (a b : ℝ) (hb : 0 < b) : a / b * b = a := by\n  field_simp\n")
_rs("rs_default_arg", "theorem rs_default_arg (n : ℕ := 5) : n + 0 = n := by\n  omega\n")
_rs("rs_structure_instance", "theorem rs_prod (p : ℕ × ℕ) (h : p = { fst := 1, snd := 2 }) : p.1 + p.2 = 3 := by\n  subst h\n  rfl\n")


def table_hash() -> str:
    """SHA-256 of the canonical JSON of both case tables + the header + statements."""
    blob = json.dumps(
        {"header": HEADER, "statements": STATEMENTS, "adversarial": ADVERSARIAL, "restated": RESTATED},
        sort_keys=True, ensure_ascii=False,
    )
    return hashlib.sha256(blob.encode("utf-8")).hexdigest()


if __name__ == "__main__":
    print(len(ADVERSARIAL), "adversarial,", len(RESTATED), "restated; sha256", table_hash())