| """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" |
| ) |
|
|
| |
| 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", |
| "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", |
| } |
|
|
| |
| |
| _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) |
| ) |
|
|
|
|
| |
| _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") |
| |
| _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") |
| |
| _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") |
| |
| _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") |
| |
| _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") |
| |
| _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") |
| |
| _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") |
| |
| _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") |
| |
| _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") |
| |
| _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") |
| |
| _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") |
| |
| _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="") |
| |
| _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") |
|
|
| |
| |
| |
| |
| 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()) |
|
|
