PrimeCert interval versus quadratic-nonresidue kernel replay

README.md

PrimeCert interval witness replay

Place IntervalBench.lean at PrimeCertTest/IntervalBench.lean on the PR branch and run:

INTERVAL_SAMPLES=/tmp/interval-samples.csv lake build PrimeCertTest.IntervalBench

Lean 4.33.0. Each sample uses a fresh Kernel.check, after imports and expression construction. The equality application checks the result; false-result controls must fail. Four adjacent AB/BA blocks, 64 checks per arm per block. A is the existing prime quadratic-nonresidue mode (7, 3, 3); B is the new interval mode. The latter two cases are the two Curve25519 cube-root nodes. CSV columns: block, r, interval, repetition, nanoseconds. record.json contains the CPU affinity and host context. unaffined-samples.csv retains the earlier completed run without CPU affinity. These timings cover just the nonsquare obligation, not the whole primality certificate.

hex-sieve-invalid-cached-log-record.json

{
  "cpu": 0,
  "load_before": [
    3.2314453125,
    3.3984375,
    3.904296875
  ],
  "rows": [
    {
      "block": 0,
      "arm": "m1",
      "stdout": "\u2139 [70/70] Built HexPrimality.SieveToolsProbe (1.3s)\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_WITNESS_CONTROL rejected\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1261680\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1269531\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1214580\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1191776\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1189093\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1177886\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1187490\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1182313\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\nBuild completed successfully (70 jobs).\n",
      "stderr": "",
      "returncode": 0,
      "source": "module\npublic import HexPrimality.Cert\npublic import Lean\npublic meta import Lean\npublic section\nset_option maxRecDepth 100000\nopen Hex.Nat\nmutual\n@[expose] def oldCheck : PrimeCert \u2192 Bool\n  | .small n => tableSearch n\n  | .pock n fs => checkPockArith n fs && oldChildren fs\n  | .pock3 n r s w fs => checkPock3Arith n r s w fs && oldChildren fs\n  | .pock3Sieve n r s w m fs => checkPock3SieveArith n r s w m fs && oldChildren fs\n@[expose] def oldChildren : List (Nat \u00d7 Nat \u00d7 PrimeCert) \u2192 Bool\n  | [] => true\n  | (_, _, c) :: cs => oldCheck c && oldChildren cs\nend\n\ndef certificate : PrimeCert := .pock3 9223372036904058881 1677731 167772 1677730 [(3, 19, .small 2), (2, 0, .small 5)]\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime 9223372036904058881 := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n\nmeta partial def inlineLocal (env : Lean.Environment) (e : Lean.Expr) : Lean.Expr :=\n  e.replace fun sub => match sub with\n    | .const n levels =>\n      if env.isImportedConst n then none else\n        match env.find? n with\n        | some info => (info.value? (allowOpaque := true)).map fun value =>\n            inlineLocal env (value.instantiateLevelParams info.levelParams levels)\n        | none => none\n    | _ => none\n\nrun_cmd do\n  let env \u2190 Lean.getEnv\n  let some (.thmInfo info) := env.find? `result\n    | throwError \"missing result theorem\"\n  let value := inlineLocal env info.value\n  let type := inlineLocal env info.type\n  unless (value.getUsedConstants ++ type.getUsedConstants).all env.isImportedConst do\n    throwError \"unexpanded local proof dependency\"\n  -- The identity application checks the proof against its declared goal type.\n  let proof := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) value\n  -- Explicitly finish pending elaboration-time kernel tasks before timing.\n  let ready \u2190 IO.mkRef env.toKernelEnv\n  let ready \u2190 ready.get\n  let env := Lean.Environment.ofKernelEnv ready\n  -- An invalid equality must be rejected by this same kernel entry point.\n  let badType := Lean.mkApp3 (Lean.mkConst ``Eq [.succ .zero])\n    (Lean.mkConst ``Bool) (Lean.mkConst ``Bool.true) (Lean.mkConst ``Bool.false)\n  let badProof := Lean.mkApp (Lean.mkLambda `h .default badType (Lean.mkBVar 0))\n    Lean.reflBoolTrue\n  match Lean.Kernel.check env {} badProof with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the negative control\"\n  let corrupt := value.replace fun e => match e with\n    | .lit (.natVal n) => if n == 9223372036904058881 then some (Lean.mkRawNatLit (n + 2)) else none\n    | _ => none\n  if corrupt == value then throwError \"subject corruption did not change the proof\"\n  let corrupt := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corrupt\n  match Lean.Kernel.check env {} corrupt with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the corrupted proof\"\n  -- Change only a Hex witness base: subjects, products, and ordering remain\n  -- intact, so this control must reach the witness arithmetic.\n  let corruptWitness := value.replace fun e => Id.run do\n    unless e.isAppOfArity `Hex.Nat.PrimeCert.pock 2 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3 5 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3Sieve 6 do return none\n    let args := e.getAppArgs\n    let fs := args.back!\n    unless fs.isAppOfArity ``List.cons 3 do return none\n    let fsArgs := fs.getAppArgs\n    let entry := fsArgs[1]!\n    unless entry.isAppOfArity ``Prod.mk 4 do return none\n    let entryArgs := entry.getAppArgs\n    let entry := Lean.mkAppN entry.getAppFn (entryArgs.set! 2 (Lean.mkRawNatLit 0))\n    let fs := Lean.mkAppN fs.getAppFn (fsArgs.set! 1 entry)\n    return some (Lean.mkAppN e.getAppFn (args.set! (args.size - 1) fs))\n  let needsWitness := value.getUsedConstants.any fun name =>\n    name == `Hex.Nat.PrimeCert.pock || name == `Hex.Nat.PrimeCert.pock3 ||\n      name == `Hex.Nat.PrimeCert.pock3Sieve\n  if needsWitness && corruptWitness == value then\n    throwError \"witness corruption did not change the proof\"\n  if corruptWitness != value then\n    let bad := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corruptWitness\n    match Lean.Kernel.check env {} bad with\n    | .error _ => pure ()\n    | .ok _ => throwError \"kernel accepted the zero witness base\"\n    Lean.logInfo \"DIRECT_WITNESS_CONTROL rejected\"\n  for _ in [:8] do\n    let input \u2190 IO.mkRef (env, proof)\n    let (env, proof) \u2190 input.get\n    let start \u2190 IO.monoNanosNow\n    let checked \u2190 IO.mkRef (Lean.Kernel.check env {} proof)\n    let checked \u2190 checked.get\n    let stop \u2190 IO.monoNanosNow\n    match checked with\n    | .error _ => throwError \"kernel recheck failed\"\n    | .ok _ => pure ()\n    Lean.logInfo m!\"DIRECT_KERNEL_NS {stop - start}\"\n    Lean.logInfo m!\"DIRECT_DEPENDENCIES {value.getUsedConstants}\"\n",
      "ns": [
        1261680,
        1269531,
        1214580,
        1191776,
        1189093,
        1177886,
        1187490,
        1182313
      ]
    },
    {
      "block": 0,
      "arm": "m4",
      "stdout": "\u2139 [70/70] Built HexPrimality.SieveToolsProbe (1.3s)\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_WITNESS_CONTROL rejected\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1027243\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 993423\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 986442\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1034273\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 970819\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 968166\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 962127\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 956548\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\nBuild completed successfully (70 jobs).\n",
      "stderr": "",
      "returncode": 0,
      "source": "module\npublic import HexPrimality.Cert\npublic import Lean\npublic meta import Lean\npublic section\nset_option maxRecDepth 100000\nopen Hex.Nat\nmutual\n@[expose] def oldCheck : PrimeCert \u2192 Bool\n  | .small n => tableSearch n\n  | .pock n fs => checkPockArith n fs && oldChildren fs\n  | .pock3 n r s w fs => checkPock3Arith n r s w fs && oldChildren fs\n  | .pock3Sieve n r s w m fs => checkPock3SieveArith n r s w m fs && oldChildren fs\n@[expose] def oldChildren : List (Nat \u00d7 Nat \u00d7 PrimeCert) \u2192 Bool\n  | [] => true\n  | (_, _, c) :: cs => oldCheck c && oldChildren cs\nend\n\ndef certificate : PrimeCert := .pock3Sieve 9223372036904058881 47 4194304 0 4 [(3, 19, .small 2)]\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime 9223372036904058881 := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n\nmeta partial def inlineLocal (env : Lean.Environment) (e : Lean.Expr) : Lean.Expr :=\n  e.replace fun sub => match sub with\n    | .const n levels =>\n      if env.isImportedConst n then none else\n        match env.find? n with\n        | some info => (info.value? (allowOpaque := true)).map fun value =>\n            inlineLocal env (value.instantiateLevelParams info.levelParams levels)\n        | none => none\n    | _ => none\n\nrun_cmd do\n  let env \u2190 Lean.getEnv\n  let some (.thmInfo info) := env.find? `result\n    | throwError \"missing result theorem\"\n  let value := inlineLocal env info.value\n  let type := inlineLocal env info.type\n  unless (value.getUsedConstants ++ type.getUsedConstants).all env.isImportedConst do\n    throwError \"unexpanded local proof dependency\"\n  -- The identity application checks the proof against its declared goal type.\n  let proof := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) value\n  -- Explicitly finish pending elaboration-time kernel tasks before timing.\n  let ready \u2190 IO.mkRef env.toKernelEnv\n  let ready \u2190 ready.get\n  let env := Lean.Environment.ofKernelEnv ready\n  -- An invalid equality must be rejected by this same kernel entry point.\n  let badType := Lean.mkApp3 (Lean.mkConst ``Eq [.succ .zero])\n    (Lean.mkConst ``Bool) (Lean.mkConst ``Bool.true) (Lean.mkConst ``Bool.false)\n  let badProof := Lean.mkApp (Lean.mkLambda `h .default badType (Lean.mkBVar 0))\n    Lean.reflBoolTrue\n  match Lean.Kernel.check env {} badProof with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the negative control\"\n  let corrupt := value.replace fun e => match e with\n    | .lit (.natVal n) => if n == 9223372036904058881 then some (Lean.mkRawNatLit (n + 2)) else none\n    | _ => none\n  if corrupt == value then throwError \"subject corruption did not change the proof\"\n  let corrupt := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corrupt\n  match Lean.Kernel.check env {} corrupt with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the corrupted proof\"\n  -- Change only a Hex witness base: subjects, products, and ordering remain\n  -- intact, so this control must reach the witness arithmetic.\n  let corruptWitness := value.replace fun e => Id.run do\n    unless e.isAppOfArity `Hex.Nat.PrimeCert.pock 2 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3 5 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3Sieve 6 do return none\n    let args := e.getAppArgs\n    let fs := args.back!\n    unless fs.isAppOfArity ``List.cons 3 do return none\n    let fsArgs := fs.getAppArgs\n    let entry := fsArgs[1]!\n    unless entry.isAppOfArity ``Prod.mk 4 do return none\n    let entryArgs := entry.getAppArgs\n    let entry := Lean.mkAppN entry.getAppFn (entryArgs.set! 2 (Lean.mkRawNatLit 0))\n    let fs := Lean.mkAppN fs.getAppFn (fsArgs.set! 1 entry)\n    return some (Lean.mkAppN e.getAppFn (args.set! (args.size - 1) fs))\n  let needsWitness := value.getUsedConstants.any fun name =>\n    name == `Hex.Nat.PrimeCert.pock || name == `Hex.Nat.PrimeCert.pock3 ||\n      name == `Hex.Nat.PrimeCert.pock3Sieve\n  if needsWitness && corruptWitness == value then\n    throwError \"witness corruption did not change the proof\"\n  if corruptWitness != value then\n    let bad := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corruptWitness\n    match Lean.Kernel.check env {} bad with\n    | .error _ => pure ()\n    | .ok _ => throwError \"kernel accepted the zero witness base\"\n    Lean.logInfo \"DIRECT_WITNESS_CONTROL rejected\"\n  for _ in [:8] do\n    let input \u2190 IO.mkRef (env, proof)\n    let (env, proof) \u2190 input.get\n    let start \u2190 IO.monoNanosNow\n    let checked \u2190 IO.mkRef (Lean.Kernel.check env {} proof)\n    let checked \u2190 checked.get\n    let stop \u2190 IO.monoNanosNow\n    match checked with\n    | .error _ => throwError \"kernel recheck failed\"\n    | .ok _ => pure ()\n    Lean.logInfo m!\"DIRECT_KERNEL_NS {stop - start}\"\n    Lean.logInfo m!\"DIRECT_DEPENDENCIES {value.getUsedConstants}\"\n",
      "ns": [
        1027243,
        993423,
        986442,
        1034273,
        970819,
        968166,
        962127,
        956548
      ]
    },
    {
      "block": 1,
      "arm": "m4",
      "stdout": "\u2139 [70/70] Replayed HexPrimality.SieveToolsProbe\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_WITNESS_CONTROL rejected\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1027243\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 993423\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 986442\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1034273\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 970819\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 968166\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 962127\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 956548\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\nBuild completed successfully (70 jobs).\n",
      "stderr": "",
      "returncode": 0,
      "source": "module\npublic import HexPrimality.Cert\npublic import Lean\npublic meta import Lean\npublic section\nset_option maxRecDepth 100000\nopen Hex.Nat\nmutual\n@[expose] def oldCheck : PrimeCert \u2192 Bool\n  | .small n => tableSearch n\n  | .pock n fs => checkPockArith n fs && oldChildren fs\n  | .pock3 n r s w fs => checkPock3Arith n r s w fs && oldChildren fs\n  | .pock3Sieve n r s w m fs => checkPock3SieveArith n r s w m fs && oldChildren fs\n@[expose] def oldChildren : List (Nat \u00d7 Nat \u00d7 PrimeCert) \u2192 Bool\n  | [] => true\n  | (_, _, c) :: cs => oldCheck c && oldChildren cs\nend\n\ndef certificate : PrimeCert := .pock3Sieve 9223372036904058881 47 4194304 0 4 [(3, 19, .small 2)]\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime 9223372036904058881 := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n\nmeta partial def inlineLocal (env : Lean.Environment) (e : Lean.Expr) : Lean.Expr :=\n  e.replace fun sub => match sub with\n    | .const n levels =>\n      if env.isImportedConst n then none else\n        match env.find? n with\n        | some info => (info.value? (allowOpaque := true)).map fun value =>\n            inlineLocal env (value.instantiateLevelParams info.levelParams levels)\n        | none => none\n    | _ => none\n\nrun_cmd do\n  let env \u2190 Lean.getEnv\n  let some (.thmInfo info) := env.find? `result\n    | throwError \"missing result theorem\"\n  let value := inlineLocal env info.value\n  let type := inlineLocal env info.type\n  unless (value.getUsedConstants ++ type.getUsedConstants).all env.isImportedConst do\n    throwError \"unexpanded local proof dependency\"\n  -- The identity application checks the proof against its declared goal type.\n  let proof := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) value\n  -- Explicitly finish pending elaboration-time kernel tasks before timing.\n  let ready \u2190 IO.mkRef env.toKernelEnv\n  let ready \u2190 ready.get\n  let env := Lean.Environment.ofKernelEnv ready\n  -- An invalid equality must be rejected by this same kernel entry point.\n  let badType := Lean.mkApp3 (Lean.mkConst ``Eq [.succ .zero])\n    (Lean.mkConst ``Bool) (Lean.mkConst ``Bool.true) (Lean.mkConst ``Bool.false)\n  let badProof := Lean.mkApp (Lean.mkLambda `h .default badType (Lean.mkBVar 0))\n    Lean.reflBoolTrue\n  match Lean.Kernel.check env {} badProof with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the negative control\"\n  let corrupt := value.replace fun e => match e with\n    | .lit (.natVal n) => if n == 9223372036904058881 then some (Lean.mkRawNatLit (n + 2)) else none\n    | _ => none\n  if corrupt == value then throwError \"subject corruption did not change the proof\"\n  let corrupt := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corrupt\n  match Lean.Kernel.check env {} corrupt with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the corrupted proof\"\n  -- Change only a Hex witness base: subjects, products, and ordering remain\n  -- intact, so this control must reach the witness arithmetic.\n  let corruptWitness := value.replace fun e => Id.run do\n    unless e.isAppOfArity `Hex.Nat.PrimeCert.pock 2 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3 5 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3Sieve 6 do return none\n    let args := e.getAppArgs\n    let fs := args.back!\n    unless fs.isAppOfArity ``List.cons 3 do return none\n    let fsArgs := fs.getAppArgs\n    let entry := fsArgs[1]!\n    unless entry.isAppOfArity ``Prod.mk 4 do return none\n    let entryArgs := entry.getAppArgs\n    let entry := Lean.mkAppN entry.getAppFn (entryArgs.set! 2 (Lean.mkRawNatLit 0))\n    let fs := Lean.mkAppN fs.getAppFn (fsArgs.set! 1 entry)\n    return some (Lean.mkAppN e.getAppFn (args.set! (args.size - 1) fs))\n  let needsWitness := value.getUsedConstants.any fun name =>\n    name == `Hex.Nat.PrimeCert.pock || name == `Hex.Nat.PrimeCert.pock3 ||\n      name == `Hex.Nat.PrimeCert.pock3Sieve\n  if needsWitness && corruptWitness == value then\n    throwError \"witness corruption did not change the proof\"\n  if corruptWitness != value then\n    let bad := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corruptWitness\n    match Lean.Kernel.check env {} bad with\n    | .error _ => pure ()\n    | .ok _ => throwError \"kernel accepted the zero witness base\"\n    Lean.logInfo \"DIRECT_WITNESS_CONTROL rejected\"\n  for _ in [:8] do\n    let input \u2190 IO.mkRef (env, proof)\n    let (env, proof) \u2190 input.get\n    let start \u2190 IO.monoNanosNow\n    let checked \u2190 IO.mkRef (Lean.Kernel.check env {} proof)\n    let checked \u2190 checked.get\n    let stop \u2190 IO.monoNanosNow\n    match checked with\n    | .error _ => throwError \"kernel recheck failed\"\n    | .ok _ => pure ()\n    Lean.logInfo m!\"DIRECT_KERNEL_NS {stop - start}\"\n    Lean.logInfo m!\"DIRECT_DEPENDENCIES {value.getUsedConstants}\"\n",
      "ns": [
        1027243,
        993423,
        986442,
        1034273,
        970819,
        968166,
        962127,
        956548
      ]
    },
    {
      "block": 1,
      "arm": "m1",
      "stdout": "\u2139 [70/70] Built HexPrimality.SieveToolsProbe (1.3s)\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_WITNESS_CONTROL rejected\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1257264\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1220570\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1259448\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1199929\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1188922\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1186960\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1186279\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1182913\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\nBuild completed successfully (70 jobs).\n",
      "stderr": "",
      "returncode": 0,
      "source": "module\npublic import HexPrimality.Cert\npublic import Lean\npublic meta import Lean\npublic section\nset_option maxRecDepth 100000\nopen Hex.Nat\nmutual\n@[expose] def oldCheck : PrimeCert \u2192 Bool\n  | .small n => tableSearch n\n  | .pock n fs => checkPockArith n fs && oldChildren fs\n  | .pock3 n r s w fs => checkPock3Arith n r s w fs && oldChildren fs\n  | .pock3Sieve n r s w m fs => checkPock3SieveArith n r s w m fs && oldChildren fs\n@[expose] def oldChildren : List (Nat \u00d7 Nat \u00d7 PrimeCert) \u2192 Bool\n  | [] => true\n  | (_, _, c) :: cs => oldCheck c && oldChildren cs\nend\n\ndef certificate : PrimeCert := .pock3 9223372036904058881 1677731 167772 1677730 [(3, 19, .small 2), (2, 0, .small 5)]\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime 9223372036904058881 := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n\nmeta partial def inlineLocal (env : Lean.Environment) (e : Lean.Expr) : Lean.Expr :=\n  e.replace fun sub => match sub with\n    | .const n levels =>\n      if env.isImportedConst n then none else\n        match env.find? n with\n        | some info => (info.value? (allowOpaque := true)).map fun value =>\n            inlineLocal env (value.instantiateLevelParams info.levelParams levels)\n        | none => none\n    | _ => none\n\nrun_cmd do\n  let env \u2190 Lean.getEnv\n  let some (.thmInfo info) := env.find? `result\n    | throwError \"missing result theorem\"\n  let value := inlineLocal env info.value\n  let type := inlineLocal env info.type\n  unless (value.getUsedConstants ++ type.getUsedConstants).all env.isImportedConst do\n    throwError \"unexpanded local proof dependency\"\n  -- The identity application checks the proof against its declared goal type.\n  let proof := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) value\n  -- Explicitly finish pending elaboration-time kernel tasks before timing.\n  let ready \u2190 IO.mkRef env.toKernelEnv\n  let ready \u2190 ready.get\n  let env := Lean.Environment.ofKernelEnv ready\n  -- An invalid equality must be rejected by this same kernel entry point.\n  let badType := Lean.mkApp3 (Lean.mkConst ``Eq [.succ .zero])\n    (Lean.mkConst ``Bool) (Lean.mkConst ``Bool.true) (Lean.mkConst ``Bool.false)\n  let badProof := Lean.mkApp (Lean.mkLambda `h .default badType (Lean.mkBVar 0))\n    Lean.reflBoolTrue\n  match Lean.Kernel.check env {} badProof with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the negative control\"\n  let corrupt := value.replace fun e => match e with\n    | .lit (.natVal n) => if n == 9223372036904058881 then some (Lean.mkRawNatLit (n + 2)) else none\n    | _ => none\n  if corrupt == value then throwError \"subject corruption did not change the proof\"\n  let corrupt := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corrupt\n  match Lean.Kernel.check env {} corrupt with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the corrupted proof\"\n  -- Change only a Hex witness base: subjects, products, and ordering remain\n  -- intact, so this control must reach the witness arithmetic.\n  let corruptWitness := value.replace fun e => Id.run do\n    unless e.isAppOfArity `Hex.Nat.PrimeCert.pock 2 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3 5 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3Sieve 6 do return none\n    let args := e.getAppArgs\n    let fs := args.back!\n    unless fs.isAppOfArity ``List.cons 3 do return none\n    let fsArgs := fs.getAppArgs\n    let entry := fsArgs[1]!\n    unless entry.isAppOfArity ``Prod.mk 4 do return none\n    let entryArgs := entry.getAppArgs\n    let entry := Lean.mkAppN entry.getAppFn (entryArgs.set! 2 (Lean.mkRawNatLit 0))\n    let fs := Lean.mkAppN fs.getAppFn (fsArgs.set! 1 entry)\n    return some (Lean.mkAppN e.getAppFn (args.set! (args.size - 1) fs))\n  let needsWitness := value.getUsedConstants.any fun name =>\n    name == `Hex.Nat.PrimeCert.pock || name == `Hex.Nat.PrimeCert.pock3 ||\n      name == `Hex.Nat.PrimeCert.pock3Sieve\n  if needsWitness && corruptWitness == value then\n    throwError \"witness corruption did not change the proof\"\n  if corruptWitness != value then\n    let bad := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corruptWitness\n    match Lean.Kernel.check env {} bad with\n    | .error _ => pure ()\n    | .ok _ => throwError \"kernel accepted the zero witness base\"\n    Lean.logInfo \"DIRECT_WITNESS_CONTROL rejected\"\n  for _ in [:8] do\n    let input \u2190 IO.mkRef (env, proof)\n    let (env, proof) \u2190 input.get\n    let start \u2190 IO.monoNanosNow\n    let checked \u2190 IO.mkRef (Lean.Kernel.check env {} proof)\n    let checked \u2190 checked.get\n    let stop \u2190 IO.monoNanosNow\n    match checked with\n    | .error _ => throwError \"kernel recheck failed\"\n    | .ok _ => pure ()\n    Lean.logInfo m!\"DIRECT_KERNEL_NS {stop - start}\"\n    Lean.logInfo m!\"DIRECT_DEPENDENCIES {value.getUsedConstants}\"\n",
      "ns": [
        1257264,
        1220570,
        1259448,
        1199929,
        1188922,
        1186960,
        1186279,
        1182913
      ]
    },
    {
      "block": 2,
      "arm": "m1",
      "stdout": "\u2139 [70/70] Replayed HexPrimality.SieveToolsProbe\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_WITNESS_CONTROL rejected\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1257264\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1220570\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1259448\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1199929\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1188922\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1186960\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1186279\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1182913\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\nBuild completed successfully (70 jobs).\n",
      "stderr": "",
      "returncode": 0,
      "source": "module\npublic import HexPrimality.Cert\npublic import Lean\npublic meta import Lean\npublic section\nset_option maxRecDepth 100000\nopen Hex.Nat\nmutual\n@[expose] def oldCheck : PrimeCert \u2192 Bool\n  | .small n => tableSearch n\n  | .pock n fs => checkPockArith n fs && oldChildren fs\n  | .pock3 n r s w fs => checkPock3Arith n r s w fs && oldChildren fs\n  | .pock3Sieve n r s w m fs => checkPock3SieveArith n r s w m fs && oldChildren fs\n@[expose] def oldChildren : List (Nat \u00d7 Nat \u00d7 PrimeCert) \u2192 Bool\n  | [] => true\n  | (_, _, c) :: cs => oldCheck c && oldChildren cs\nend\n\ndef certificate : PrimeCert := .pock3 9223372036904058881 1677731 167772 1677730 [(3, 19, .small 2), (2, 0, .small 5)]\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime 9223372036904058881 := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n\nmeta partial def inlineLocal (env : Lean.Environment) (e : Lean.Expr) : Lean.Expr :=\n  e.replace fun sub => match sub with\n    | .const n levels =>\n      if env.isImportedConst n then none else\n        match env.find? n with\n        | some info => (info.value? (allowOpaque := true)).map fun value =>\n            inlineLocal env (value.instantiateLevelParams info.levelParams levels)\n        | none => none\n    | _ => none\n\nrun_cmd do\n  let env \u2190 Lean.getEnv\n  let some (.thmInfo info) := env.find? `result\n    | throwError \"missing result theorem\"\n  let value := inlineLocal env info.value\n  let type := inlineLocal env info.type\n  unless (value.getUsedConstants ++ type.getUsedConstants).all env.isImportedConst do\n    throwError \"unexpanded local proof dependency\"\n  -- The identity application checks the proof against its declared goal type.\n  let proof := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) value\n  -- Explicitly finish pending elaboration-time kernel tasks before timing.\n  let ready \u2190 IO.mkRef env.toKernelEnv\n  let ready \u2190 ready.get\n  let env := Lean.Environment.ofKernelEnv ready\n  -- An invalid equality must be rejected by this same kernel entry point.\n  let badType := Lean.mkApp3 (Lean.mkConst ``Eq [.succ .zero])\n    (Lean.mkConst ``Bool) (Lean.mkConst ``Bool.true) (Lean.mkConst ``Bool.false)\n  let badProof := Lean.mkApp (Lean.mkLambda `h .default badType (Lean.mkBVar 0))\n    Lean.reflBoolTrue\n  match Lean.Kernel.check env {} badProof with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the negative control\"\n  let corrupt := value.replace fun e => match e with\n    | .lit (.natVal n) => if n == 9223372036904058881 then some (Lean.mkRawNatLit (n + 2)) else none\n    | _ => none\n  if corrupt == value then throwError \"subject corruption did not change the proof\"\n  let corrupt := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corrupt\n  match Lean.Kernel.check env {} corrupt with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the corrupted proof\"\n  -- Change only a Hex witness base: subjects, products, and ordering remain\n  -- intact, so this control must reach the witness arithmetic.\n  let corruptWitness := value.replace fun e => Id.run do\n    unless e.isAppOfArity `Hex.Nat.PrimeCert.pock 2 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3 5 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3Sieve 6 do return none\n    let args := e.getAppArgs\n    let fs := args.back!\n    unless fs.isAppOfArity ``List.cons 3 do return none\n    let fsArgs := fs.getAppArgs\n    let entry := fsArgs[1]!\n    unless entry.isAppOfArity ``Prod.mk 4 do return none\n    let entryArgs := entry.getAppArgs\n    let entry := Lean.mkAppN entry.getAppFn (entryArgs.set! 2 (Lean.mkRawNatLit 0))\n    let fs := Lean.mkAppN fs.getAppFn (fsArgs.set! 1 entry)\n    return some (Lean.mkAppN e.getAppFn (args.set! (args.size - 1) fs))\n  let needsWitness := value.getUsedConstants.any fun name =>\n    name == `Hex.Nat.PrimeCert.pock || name == `Hex.Nat.PrimeCert.pock3 ||\n      name == `Hex.Nat.PrimeCert.pock3Sieve\n  if needsWitness && corruptWitness == value then\n    throwError \"witness corruption did not change the proof\"\n  if corruptWitness != value then\n    let bad := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corruptWitness\n    match Lean.Kernel.check env {} bad with\n    | .error _ => pure ()\n    | .ok _ => throwError \"kernel accepted the zero witness base\"\n    Lean.logInfo \"DIRECT_WITNESS_CONTROL rejected\"\n  for _ in [:8] do\n    let input \u2190 IO.mkRef (env, proof)\n    let (env, proof) \u2190 input.get\n    let start \u2190 IO.monoNanosNow\n    let checked \u2190 IO.mkRef (Lean.Kernel.check env {} proof)\n    let checked \u2190 checked.get\n    let stop \u2190 IO.monoNanosNow\n    match checked with\n    | .error _ => throwError \"kernel recheck failed\"\n    | .ok _ => pure ()\n    Lean.logInfo m!\"DIRECT_KERNEL_NS {stop - start}\"\n    Lean.logInfo m!\"DIRECT_DEPENDENCIES {value.getUsedConstants}\"\n",
      "ns": [
        1257264,
        1220570,
        1259448,
        1199929,
        1188922,
        1186960,
        1186279,
        1182913
      ]
    },
    {
      "block": 2,
      "arm": "m4",
      "stdout": "\u2139 [70/70] Built HexPrimality.SieveToolsProbe (1.3s)\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_WITNESS_CONTROL rejected\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1035335\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1002676\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1042386\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 978731\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 974275\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 965521\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 968265\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 967354\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\nBuild completed successfully (70 jobs).\n",
      "stderr": "",
      "returncode": 0,
      "source": "module\npublic import HexPrimality.Cert\npublic import Lean\npublic meta import Lean\npublic section\nset_option maxRecDepth 100000\nopen Hex.Nat\nmutual\n@[expose] def oldCheck : PrimeCert \u2192 Bool\n  | .small n => tableSearch n\n  | .pock n fs => checkPockArith n fs && oldChildren fs\n  | .pock3 n r s w fs => checkPock3Arith n r s w fs && oldChildren fs\n  | .pock3Sieve n r s w m fs => checkPock3SieveArith n r s w m fs && oldChildren fs\n@[expose] def oldChildren : List (Nat \u00d7 Nat \u00d7 PrimeCert) \u2192 Bool\n  | [] => true\n  | (_, _, c) :: cs => oldCheck c && oldChildren cs\nend\n\ndef certificate : PrimeCert := .pock3Sieve 9223372036904058881 47 4194304 0 4 [(3, 19, .small 2)]\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime 9223372036904058881 := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n\nmeta partial def inlineLocal (env : Lean.Environment) (e : Lean.Expr) : Lean.Expr :=\n  e.replace fun sub => match sub with\n    | .const n levels =>\n      if env.isImportedConst n then none else\n        match env.find? n with\n        | some info => (info.value? (allowOpaque := true)).map fun value =>\n            inlineLocal env (value.instantiateLevelParams info.levelParams levels)\n        | none => none\n    | _ => none\n\nrun_cmd do\n  let env \u2190 Lean.getEnv\n  let some (.thmInfo info) := env.find? `result\n    | throwError \"missing result theorem\"\n  let value := inlineLocal env info.value\n  let type := inlineLocal env info.type\n  unless (value.getUsedConstants ++ type.getUsedConstants).all env.isImportedConst do\n    throwError \"unexpanded local proof dependency\"\n  -- The identity application checks the proof against its declared goal type.\n  let proof := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) value\n  -- Explicitly finish pending elaboration-time kernel tasks before timing.\n  let ready \u2190 IO.mkRef env.toKernelEnv\n  let ready \u2190 ready.get\n  let env := Lean.Environment.ofKernelEnv ready\n  -- An invalid equality must be rejected by this same kernel entry point.\n  let badType := Lean.mkApp3 (Lean.mkConst ``Eq [.succ .zero])\n    (Lean.mkConst ``Bool) (Lean.mkConst ``Bool.true) (Lean.mkConst ``Bool.false)\n  let badProof := Lean.mkApp (Lean.mkLambda `h .default badType (Lean.mkBVar 0))\n    Lean.reflBoolTrue\n  match Lean.Kernel.check env {} badProof with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the negative control\"\n  let corrupt := value.replace fun e => match e with\n    | .lit (.natVal n) => if n == 9223372036904058881 then some (Lean.mkRawNatLit (n + 2)) else none\n    | _ => none\n  if corrupt == value then throwError \"subject corruption did not change the proof\"\n  let corrupt := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corrupt\n  match Lean.Kernel.check env {} corrupt with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the corrupted proof\"\n  -- Change only a Hex witness base: subjects, products, and ordering remain\n  -- intact, so this control must reach the witness arithmetic.\n  let corruptWitness := value.replace fun e => Id.run do\n    unless e.isAppOfArity `Hex.Nat.PrimeCert.pock 2 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3 5 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3Sieve 6 do return none\n    let args := e.getAppArgs\n    let fs := args.back!\n    unless fs.isAppOfArity ``List.cons 3 do return none\n    let fsArgs := fs.getAppArgs\n    let entry := fsArgs[1]!\n    unless entry.isAppOfArity ``Prod.mk 4 do return none\n    let entryArgs := entry.getAppArgs\n    let entry := Lean.mkAppN entry.getAppFn (entryArgs.set! 2 (Lean.mkRawNatLit 0))\n    let fs := Lean.mkAppN fs.getAppFn (fsArgs.set! 1 entry)\n    return some (Lean.mkAppN e.getAppFn (args.set! (args.size - 1) fs))\n  let needsWitness := value.getUsedConstants.any fun name =>\n    name == `Hex.Nat.PrimeCert.pock || name == `Hex.Nat.PrimeCert.pock3 ||\n      name == `Hex.Nat.PrimeCert.pock3Sieve\n  if needsWitness && corruptWitness == value then\n    throwError \"witness corruption did not change the proof\"\n  if corruptWitness != value then\n    let bad := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corruptWitness\n    match Lean.Kernel.check env {} bad with\n    | .error _ => pure ()\n    | .ok _ => throwError \"kernel accepted the zero witness base\"\n    Lean.logInfo \"DIRECT_WITNESS_CONTROL rejected\"\n  for _ in [:8] do\n    let input \u2190 IO.mkRef (env, proof)\n    let (env, proof) \u2190 input.get\n    let start \u2190 IO.monoNanosNow\n    let checked \u2190 IO.mkRef (Lean.Kernel.check env {} proof)\n    let checked \u2190 checked.get\n    let stop \u2190 IO.monoNanosNow\n    match checked with\n    | .error _ => throwError \"kernel recheck failed\"\n    | .ok _ => pure ()\n    Lean.logInfo m!\"DIRECT_KERNEL_NS {stop - start}\"\n    Lean.logInfo m!\"DIRECT_DEPENDENCIES {value.getUsedConstants}\"\n",
      "ns": [
        1035335,
        1002676,
        1042386,
        978731,
        974275,
        965521,
        968265,
        967354
      ]
    },
    {
      "block": 3,
      "arm": "m4",
      "stdout": "\u2139 [70/70] Replayed HexPrimality.SieveToolsProbe\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_WITNESS_CONTROL rejected\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1035335\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1002676\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1042386\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 978731\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 974275\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 965521\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 968265\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 967354\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\nBuild completed successfully (70 jobs).\n",
      "stderr": "",
      "returncode": 0,
      "source": "module\npublic import HexPrimality.Cert\npublic import Lean\npublic meta import Lean\npublic section\nset_option maxRecDepth 100000\nopen Hex.Nat\nmutual\n@[expose] def oldCheck : PrimeCert \u2192 Bool\n  | .small n => tableSearch n\n  | .pock n fs => checkPockArith n fs && oldChildren fs\n  | .pock3 n r s w fs => checkPock3Arith n r s w fs && oldChildren fs\n  | .pock3Sieve n r s w m fs => checkPock3SieveArith n r s w m fs && oldChildren fs\n@[expose] def oldChildren : List (Nat \u00d7 Nat \u00d7 PrimeCert) \u2192 Bool\n  | [] => true\n  | (_, _, c) :: cs => oldCheck c && oldChildren cs\nend\n\ndef certificate : PrimeCert := .pock3Sieve 9223372036904058881 47 4194304 0 4 [(3, 19, .small 2)]\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime 9223372036904058881 := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n\nmeta partial def inlineLocal (env : Lean.Environment) (e : Lean.Expr) : Lean.Expr :=\n  e.replace fun sub => match sub with\n    | .const n levels =>\n      if env.isImportedConst n then none else\n        match env.find? n with\n        | some info => (info.value? (allowOpaque := true)).map fun value =>\n            inlineLocal env (value.instantiateLevelParams info.levelParams levels)\n        | none => none\n    | _ => none\n\nrun_cmd do\n  let env \u2190 Lean.getEnv\n  let some (.thmInfo info) := env.find? `result\n    | throwError \"missing result theorem\"\n  let value := inlineLocal env info.value\n  let type := inlineLocal env info.type\n  unless (value.getUsedConstants ++ type.getUsedConstants).all env.isImportedConst do\n    throwError \"unexpanded local proof dependency\"\n  -- The identity application checks the proof against its declared goal type.\n  let proof := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) value\n  -- Explicitly finish pending elaboration-time kernel tasks before timing.\n  let ready \u2190 IO.mkRef env.toKernelEnv\n  let ready \u2190 ready.get\n  let env := Lean.Environment.ofKernelEnv ready\n  -- An invalid equality must be rejected by this same kernel entry point.\n  let badType := Lean.mkApp3 (Lean.mkConst ``Eq [.succ .zero])\n    (Lean.mkConst ``Bool) (Lean.mkConst ``Bool.true) (Lean.mkConst ``Bool.false)\n  let badProof := Lean.mkApp (Lean.mkLambda `h .default badType (Lean.mkBVar 0))\n    Lean.reflBoolTrue\n  match Lean.Kernel.check env {} badProof with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the negative control\"\n  let corrupt := value.replace fun e => match e with\n    | .lit (.natVal n) => if n == 9223372036904058881 then some (Lean.mkRawNatLit (n + 2)) else none\n    | _ => none\n  if corrupt == value then throwError \"subject corruption did not change the proof\"\n  let corrupt := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corrupt\n  match Lean.Kernel.check env {} corrupt with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the corrupted proof\"\n  -- Change only a Hex witness base: subjects, products, and ordering remain\n  -- intact, so this control must reach the witness arithmetic.\n  let corruptWitness := value.replace fun e => Id.run do\n    unless e.isAppOfArity `Hex.Nat.PrimeCert.pock 2 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3 5 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3Sieve 6 do return none\n    let args := e.getAppArgs\n    let fs := args.back!\n    unless fs.isAppOfArity ``List.cons 3 do return none\n    let fsArgs := fs.getAppArgs\n    let entry := fsArgs[1]!\n    unless entry.isAppOfArity ``Prod.mk 4 do return none\n    let entryArgs := entry.getAppArgs\n    let entry := Lean.mkAppN entry.getAppFn (entryArgs.set! 2 (Lean.mkRawNatLit 0))\n    let fs := Lean.mkAppN fs.getAppFn (fsArgs.set! 1 entry)\n    return some (Lean.mkAppN e.getAppFn (args.set! (args.size - 1) fs))\n  let needsWitness := value.getUsedConstants.any fun name =>\n    name == `Hex.Nat.PrimeCert.pock || name == `Hex.Nat.PrimeCert.pock3 ||\n      name == `Hex.Nat.PrimeCert.pock3Sieve\n  if needsWitness && corruptWitness == value then\n    throwError \"witness corruption did not change the proof\"\n  if corruptWitness != value then\n    let bad := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corruptWitness\n    match Lean.Kernel.check env {} bad with\n    | .error _ => pure ()\n    | .ok _ => throwError \"kernel accepted the zero witness base\"\n    Lean.logInfo \"DIRECT_WITNESS_CONTROL rejected\"\n  for _ in [:8] do\n    let input \u2190 IO.mkRef (env, proof)\n    let (env, proof) \u2190 input.get\n    let start \u2190 IO.monoNanosNow\n    let checked \u2190 IO.mkRef (Lean.Kernel.check env {} proof)\n    let checked \u2190 checked.get\n    let stop \u2190 IO.monoNanosNow\n    match checked with\n    | .error _ => throwError \"kernel recheck failed\"\n    | .ok _ => pure ()\n    Lean.logInfo m!\"DIRECT_KERNEL_NS {stop - start}\"\n    Lean.logInfo m!\"DIRECT_DEPENDENCIES {value.getUsedConstants}\"\n",
      "ns": [
        1035335,
        1002676,
        1042386,
        978731,
        974275,
        965521,
        968265,
        967354
      ]
    },
    {
      "block": 3,
      "arm": "m1",
      "stdout": "\u2139 [70/70] Built HexPrimality.SieveToolsProbe (1.3s)\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_WITNESS_CONTROL rejected\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1250123\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1216513\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1193489\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1245787\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1196273\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1187290\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1181812\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1175964\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\nBuild completed successfully (70 jobs).\n",
      "stderr": "",
      "returncode": 0,
      "source": "module\npublic import HexPrimality.Cert\npublic import Lean\npublic meta import Lean\npublic section\nset_option maxRecDepth 100000\nopen Hex.Nat\nmutual\n@[expose] def oldCheck : PrimeCert \u2192 Bool\n  | .small n => tableSearch n\n  | .pock n fs => checkPockArith n fs && oldChildren fs\n  | .pock3 n r s w fs => checkPock3Arith n r s w fs && oldChildren fs\n  | .pock3Sieve n r s w m fs => checkPock3SieveArith n r s w m fs && oldChildren fs\n@[expose] def oldChildren : List (Nat \u00d7 Nat \u00d7 PrimeCert) \u2192 Bool\n  | [] => true\n  | (_, _, c) :: cs => oldCheck c && oldChildren cs\nend\n\ndef certificate : PrimeCert := .pock3 9223372036904058881 1677731 167772 1677730 [(3, 19, .small 2), (2, 0, .small 5)]\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime 9223372036904058881 := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n\nmeta partial def inlineLocal (env : Lean.Environment) (e : Lean.Expr) : Lean.Expr :=\n  e.replace fun sub => match sub with\n    | .const n levels =>\n      if env.isImportedConst n then none else\n        match env.find? n with\n        | some info => (info.value? (allowOpaque := true)).map fun value =>\n            inlineLocal env (value.instantiateLevelParams info.levelParams levels)\n        | none => none\n    | _ => none\n\nrun_cmd do\n  let env \u2190 Lean.getEnv\n  let some (.thmInfo info) := env.find? `result\n    | throwError \"missing result theorem\"\n  let value := inlineLocal env info.value\n  let type := inlineLocal env info.type\n  unless (value.getUsedConstants ++ type.getUsedConstants).all env.isImportedConst do\n    throwError \"unexpanded local proof dependency\"\n  -- The identity application checks the proof against its declared goal type.\n  let proof := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) value\n  -- Explicitly finish pending elaboration-time kernel tasks before timing.\n  let ready \u2190 IO.mkRef env.toKernelEnv\n  let ready \u2190 ready.get\n  let env := Lean.Environment.ofKernelEnv ready\n  -- An invalid equality must be rejected by this same kernel entry point.\n  let badType := Lean.mkApp3 (Lean.mkConst ``Eq [.succ .zero])\n    (Lean.mkConst ``Bool) (Lean.mkConst ``Bool.true) (Lean.mkConst ``Bool.false)\n  let badProof := Lean.mkApp (Lean.mkLambda `h .default badType (Lean.mkBVar 0))\n    Lean.reflBoolTrue\n  match Lean.Kernel.check env {} badProof with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the negative control\"\n  let corrupt := value.replace fun e => match e with\n    | .lit (.natVal n) => if n == 9223372036904058881 then some (Lean.mkRawNatLit (n + 2)) else none\n    | _ => none\n  if corrupt == value then throwError \"subject corruption did not change the proof\"\n  let corrupt := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corrupt\n  match Lean.Kernel.check env {} corrupt with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the corrupted proof\"\n  -- Change only a Hex witness base: subjects, products, and ordering remain\n  -- intact, so this control must reach the witness arithmetic.\n  let corruptWitness := value.replace fun e => Id.run do\n    unless e.isAppOfArity `Hex.Nat.PrimeCert.pock 2 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3 5 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3Sieve 6 do return none\n    let args := e.getAppArgs\n    let fs := args.back!\n    unless fs.isAppOfArity ``List.cons 3 do return none\n    let fsArgs := fs.getAppArgs\n    let entry := fsArgs[1]!\n    unless entry.isAppOfArity ``Prod.mk 4 do return none\n    let entryArgs := entry.getAppArgs\n    let entry := Lean.mkAppN entry.getAppFn (entryArgs.set! 2 (Lean.mkRawNatLit 0))\n    let fs := Lean.mkAppN fs.getAppFn (fsArgs.set! 1 entry)\n    return some (Lean.mkAppN e.getAppFn (args.set! (args.size - 1) fs))\n  let needsWitness := value.getUsedConstants.any fun name =>\n    name == `Hex.Nat.PrimeCert.pock || name == `Hex.Nat.PrimeCert.pock3 ||\n      name == `Hex.Nat.PrimeCert.pock3Sieve\n  if needsWitness && corruptWitness == value then\n    throwError \"witness corruption did not change the proof\"\n  if corruptWitness != value then\n    let bad := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corruptWitness\n    match Lean.Kernel.check env {} bad with\n    | .error _ => pure ()\n    | .ok _ => throwError \"kernel accepted the zero witness base\"\n    Lean.logInfo \"DIRECT_WITNESS_CONTROL rejected\"\n  for _ in [:8] do\n    let input \u2190 IO.mkRef (env, proof)\n    let (env, proof) \u2190 input.get\n    let start \u2190 IO.monoNanosNow\n    let checked \u2190 IO.mkRef (Lean.Kernel.check env {} proof)\n    let checked \u2190 checked.get\n    let stop \u2190 IO.monoNanosNow\n    match checked with\n    | .error _ => throwError \"kernel recheck failed\"\n    | .ok _ => pure ()\n    Lean.logInfo m!\"DIRECT_KERNEL_NS {stop - start}\"\n    Lean.logInfo m!\"DIRECT_DEPENDENCIES {value.getUsedConstants}\"\n",
      "ns": [
        1250123,
        1216513,
        1193489,
        1245787,
        1196273,
        1187290,
        1181812,
        1175964
      ]
    }
  ],
  "load_after": [
    3.35009765625,
    3.4189453125,
    3.90625
  ],
  "invalid_reason": "Consecutive identical sources replayed Lake logs instead of executing fresh kernel checks."
}

hex-sieve-record.json

{
  "cpu": 0,
  "load_before": [
    3.6943359375,
    3.51123046875,
    3.91943359375
  ],
  "rows": [
    {
      "block": 0,
      "arm": "m1",
      "stdout": "\u2139 [70/70] Built HexPrimality.SieveToolsProbe (1.3s)\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_WITNESS_CONTROL rejected\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1277594\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1302702\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1207980\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1204115\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1193720\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1191136\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1191337\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1185898\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\nBuild completed successfully (70 jobs).\n",
      "stderr": "",
      "returncode": 0,
      "source": "module\npublic import HexPrimality.Cert\npublic import Lean\npublic meta import Lean\npublic section\nset_option maxRecDepth 100000\nopen Hex.Nat\nmutual\n@[expose] def oldCheck : PrimeCert \u2192 Bool\n  | .small n => tableSearch n\n  | .pock n fs => checkPockArith n fs && oldChildren fs\n  | .pock3 n r s w fs => checkPock3Arith n r s w fs && oldChildren fs\n  | .pock3Sieve n r s w m fs => checkPock3SieveArith n r s w m fs && oldChildren fs\n@[expose] def oldChildren : List (Nat \u00d7 Nat \u00d7 PrimeCert) \u2192 Bool\n  | [] => true\n  | (_, _, c) :: cs => oldCheck c && oldChildren cs\nend\n\ndef certificate : PrimeCert := .pock3 9223372036904058881 1677731 167772 1677730 [(3, 19, .small 2), (2, 0, .small 5)]\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime 9223372036904058881 := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n\nmeta partial def inlineLocal (env : Lean.Environment) (e : Lean.Expr) : Lean.Expr :=\n  e.replace fun sub => match sub with\n    | .const n levels =>\n      if env.isImportedConst n then none else\n        match env.find? n with\n        | some info => (info.value? (allowOpaque := true)).map fun value =>\n            inlineLocal env (value.instantiateLevelParams info.levelParams levels)\n        | none => none\n    | _ => none\n\nrun_cmd do\n  let env \u2190 Lean.getEnv\n  let some (.thmInfo info) := env.find? `result\n    | throwError \"missing result theorem\"\n  let value := inlineLocal env info.value\n  let type := inlineLocal env info.type\n  unless (value.getUsedConstants ++ type.getUsedConstants).all env.isImportedConst do\n    throwError \"unexpanded local proof dependency\"\n  -- The identity application checks the proof against its declared goal type.\n  let proof := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) value\n  -- Explicitly finish pending elaboration-time kernel tasks before timing.\n  let ready \u2190 IO.mkRef env.toKernelEnv\n  let ready \u2190 ready.get\n  let env := Lean.Environment.ofKernelEnv ready\n  -- An invalid equality must be rejected by this same kernel entry point.\n  let badType := Lean.mkApp3 (Lean.mkConst ``Eq [.succ .zero])\n    (Lean.mkConst ``Bool) (Lean.mkConst ``Bool.true) (Lean.mkConst ``Bool.false)\n  let badProof := Lean.mkApp (Lean.mkLambda `h .default badType (Lean.mkBVar 0))\n    Lean.reflBoolTrue\n  match Lean.Kernel.check env {} badProof with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the negative control\"\n  let corrupt := value.replace fun e => match e with\n    | .lit (.natVal n) => if n == 9223372036904058881 then some (Lean.mkRawNatLit (n + 2)) else none\n    | _ => none\n  if corrupt == value then throwError \"subject corruption did not change the proof\"\n  let corrupt := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corrupt\n  match Lean.Kernel.check env {} corrupt with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the corrupted proof\"\n  -- Change only a Hex witness base: subjects, products, and ordering remain\n  -- intact, so this control must reach the witness arithmetic.\n  let corruptWitness := value.replace fun e => Id.run do\n    unless e.isAppOfArity `Hex.Nat.PrimeCert.pock 2 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3 5 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3Sieve 6 do return none\n    let args := e.getAppArgs\n    let fs := args.back!\n    unless fs.isAppOfArity ``List.cons 3 do return none\n    let fsArgs := fs.getAppArgs\n    let entry := fsArgs[1]!\n    unless entry.isAppOfArity ``Prod.mk 4 do return none\n    let entryArgs := entry.getAppArgs\n    let entry := Lean.mkAppN entry.getAppFn (entryArgs.set! 2 (Lean.mkRawNatLit 0))\n    let fs := Lean.mkAppN fs.getAppFn (fsArgs.set! 1 entry)\n    return some (Lean.mkAppN e.getAppFn (args.set! (args.size - 1) fs))\n  let needsWitness := value.getUsedConstants.any fun name =>\n    name == `Hex.Nat.PrimeCert.pock || name == `Hex.Nat.PrimeCert.pock3 ||\n      name == `Hex.Nat.PrimeCert.pock3Sieve\n  if needsWitness && corruptWitness == value then\n    throwError \"witness corruption did not change the proof\"\n  if corruptWitness != value then\n    let bad := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corruptWitness\n    match Lean.Kernel.check env {} bad with\n    | .error _ => pure ()\n    | .ok _ => throwError \"kernel accepted the zero witness base\"\n    Lean.logInfo \"DIRECT_WITNESS_CONTROL rejected\"\n  for _ in [:8] do\n    let input \u2190 IO.mkRef (env, proof)\n    let (env, proof) \u2190 input.get\n    let start \u2190 IO.monoNanosNow\n    let checked \u2190 IO.mkRef (Lean.Kernel.check env {} proof)\n    let checked \u2190 checked.get\n    let stop \u2190 IO.monoNanosNow\n    match checked with\n    | .error _ => throwError \"kernel recheck failed\"\n    | .ok _ => pure ()\n    Lean.logInfo m!\"DIRECT_KERNEL_NS {stop - start}\"\n    Lean.logInfo m!\"DIRECT_DEPENDENCIES {value.getUsedConstants}\"\n\n-- Measurement block 0, arm m1.\n",
      "ns": [
        1277594,
        1302702,
        1207980,
        1204115,
        1193720,
        1191136,
        1191337,
        1185898
      ]
    },
    {
      "block": 0,
      "arm": "m4",
      "stdout": "\u2139 [70/70] Built HexPrimality.SieveToolsProbe (1.3s)\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_WITNESS_CONTROL rejected\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1028285\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 992482\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 987313\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 966193\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 962978\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 949147\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 953464\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 952462\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\nBuild completed successfully (70 jobs).\n",
      "stderr": "",
      "returncode": 0,
      "source": "module\npublic import HexPrimality.Cert\npublic import Lean\npublic meta import Lean\npublic section\nset_option maxRecDepth 100000\nopen Hex.Nat\nmutual\n@[expose] def oldCheck : PrimeCert \u2192 Bool\n  | .small n => tableSearch n\n  | .pock n fs => checkPockArith n fs && oldChildren fs\n  | .pock3 n r s w fs => checkPock3Arith n r s w fs && oldChildren fs\n  | .pock3Sieve n r s w m fs => checkPock3SieveArith n r s w m fs && oldChildren fs\n@[expose] def oldChildren : List (Nat \u00d7 Nat \u00d7 PrimeCert) \u2192 Bool\n  | [] => true\n  | (_, _, c) :: cs => oldCheck c && oldChildren cs\nend\n\ndef certificate : PrimeCert := .pock3Sieve 9223372036904058881 47 4194304 0 4 [(3, 19, .small 2)]\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime 9223372036904058881 := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n\nmeta partial def inlineLocal (env : Lean.Environment) (e : Lean.Expr) : Lean.Expr :=\n  e.replace fun sub => match sub with\n    | .const n levels =>\n      if env.isImportedConst n then none else\n        match env.find? n with\n        | some info => (info.value? (allowOpaque := true)).map fun value =>\n            inlineLocal env (value.instantiateLevelParams info.levelParams levels)\n        | none => none\n    | _ => none\n\nrun_cmd do\n  let env \u2190 Lean.getEnv\n  let some (.thmInfo info) := env.find? `result\n    | throwError \"missing result theorem\"\n  let value := inlineLocal env info.value\n  let type := inlineLocal env info.type\n  unless (value.getUsedConstants ++ type.getUsedConstants).all env.isImportedConst do\n    throwError \"unexpanded local proof dependency\"\n  -- The identity application checks the proof against its declared goal type.\n  let proof := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) value\n  -- Explicitly finish pending elaboration-time kernel tasks before timing.\n  let ready \u2190 IO.mkRef env.toKernelEnv\n  let ready \u2190 ready.get\n  let env := Lean.Environment.ofKernelEnv ready\n  -- An invalid equality must be rejected by this same kernel entry point.\n  let badType := Lean.mkApp3 (Lean.mkConst ``Eq [.succ .zero])\n    (Lean.mkConst ``Bool) (Lean.mkConst ``Bool.true) (Lean.mkConst ``Bool.false)\n  let badProof := Lean.mkApp (Lean.mkLambda `h .default badType (Lean.mkBVar 0))\n    Lean.reflBoolTrue\n  match Lean.Kernel.check env {} badProof with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the negative control\"\n  let corrupt := value.replace fun e => match e with\n    | .lit (.natVal n) => if n == 9223372036904058881 then some (Lean.mkRawNatLit (n + 2)) else none\n    | _ => none\n  if corrupt == value then throwError \"subject corruption did not change the proof\"\n  let corrupt := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corrupt\n  match Lean.Kernel.check env {} corrupt with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the corrupted proof\"\n  -- Change only a Hex witness base: subjects, products, and ordering remain\n  -- intact, so this control must reach the witness arithmetic.\n  let corruptWitness := value.replace fun e => Id.run do\n    unless e.isAppOfArity `Hex.Nat.PrimeCert.pock 2 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3 5 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3Sieve 6 do return none\n    let args := e.getAppArgs\n    let fs := args.back!\n    unless fs.isAppOfArity ``List.cons 3 do return none\n    let fsArgs := fs.getAppArgs\n    let entry := fsArgs[1]!\n    unless entry.isAppOfArity ``Prod.mk 4 do return none\n    let entryArgs := entry.getAppArgs\n    let entry := Lean.mkAppN entry.getAppFn (entryArgs.set! 2 (Lean.mkRawNatLit 0))\n    let fs := Lean.mkAppN fs.getAppFn (fsArgs.set! 1 entry)\n    return some (Lean.mkAppN e.getAppFn (args.set! (args.size - 1) fs))\n  let needsWitness := value.getUsedConstants.any fun name =>\n    name == `Hex.Nat.PrimeCert.pock || name == `Hex.Nat.PrimeCert.pock3 ||\n      name == `Hex.Nat.PrimeCert.pock3Sieve\n  if needsWitness && corruptWitness == value then\n    throwError \"witness corruption did not change the proof\"\n  if corruptWitness != value then\n    let bad := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corruptWitness\n    match Lean.Kernel.check env {} bad with\n    | .error _ => pure ()\n    | .ok _ => throwError \"kernel accepted the zero witness base\"\n    Lean.logInfo \"DIRECT_WITNESS_CONTROL rejected\"\n  for _ in [:8] do\n    let input \u2190 IO.mkRef (env, proof)\n    let (env, proof) \u2190 input.get\n    let start \u2190 IO.monoNanosNow\n    let checked \u2190 IO.mkRef (Lean.Kernel.check env {} proof)\n    let checked \u2190 checked.get\n    let stop \u2190 IO.monoNanosNow\n    match checked with\n    | .error _ => throwError \"kernel recheck failed\"\n    | .ok _ => pure ()\n    Lean.logInfo m!\"DIRECT_KERNEL_NS {stop - start}\"\n    Lean.logInfo m!\"DIRECT_DEPENDENCIES {value.getUsedConstants}\"\n\n-- Measurement block 0, arm m4.\n",
      "ns": [
        1028285,
        992482,
        987313,
        966193,
        962978,
        949147,
        953464,
        952462
      ]
    },
    {
      "block": 1,
      "arm": "m4",
      "stdout": "\u2139 [70/70] Built HexPrimality.SieveToolsProbe (1.3s)\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_WITNESS_CONTROL rejected\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1134873\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1007153\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1050347\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 971380\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 961375\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 967163\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 965872\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 962316\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\nBuild completed successfully (70 jobs).\n",
      "stderr": "",
      "returncode": 0,
      "source": "module\npublic import HexPrimality.Cert\npublic import Lean\npublic meta import Lean\npublic section\nset_option maxRecDepth 100000\nopen Hex.Nat\nmutual\n@[expose] def oldCheck : PrimeCert \u2192 Bool\n  | .small n => tableSearch n\n  | .pock n fs => checkPockArith n fs && oldChildren fs\n  | .pock3 n r s w fs => checkPock3Arith n r s w fs && oldChildren fs\n  | .pock3Sieve n r s w m fs => checkPock3SieveArith n r s w m fs && oldChildren fs\n@[expose] def oldChildren : List (Nat \u00d7 Nat \u00d7 PrimeCert) \u2192 Bool\n  | [] => true\n  | (_, _, c) :: cs => oldCheck c && oldChildren cs\nend\n\ndef certificate : PrimeCert := .pock3Sieve 9223372036904058881 47 4194304 0 4 [(3, 19, .small 2)]\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime 9223372036904058881 := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n\nmeta partial def inlineLocal (env : Lean.Environment) (e : Lean.Expr) : Lean.Expr :=\n  e.replace fun sub => match sub with\n    | .const n levels =>\n      if env.isImportedConst n then none else\n        match env.find? n with\n        | some info => (info.value? (allowOpaque := true)).map fun value =>\n            inlineLocal env (value.instantiateLevelParams info.levelParams levels)\n        | none => none\n    | _ => none\n\nrun_cmd do\n  let env \u2190 Lean.getEnv\n  let some (.thmInfo info) := env.find? `result\n    | throwError \"missing result theorem\"\n  let value := inlineLocal env info.value\n  let type := inlineLocal env info.type\n  unless (value.getUsedConstants ++ type.getUsedConstants).all env.isImportedConst do\n    throwError \"unexpanded local proof dependency\"\n  -- The identity application checks the proof against its declared goal type.\n  let proof := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) value\n  -- Explicitly finish pending elaboration-time kernel tasks before timing.\n  let ready \u2190 IO.mkRef env.toKernelEnv\n  let ready \u2190 ready.get\n  let env := Lean.Environment.ofKernelEnv ready\n  -- An invalid equality must be rejected by this same kernel entry point.\n  let badType := Lean.mkApp3 (Lean.mkConst ``Eq [.succ .zero])\n    (Lean.mkConst ``Bool) (Lean.mkConst ``Bool.true) (Lean.mkConst ``Bool.false)\n  let badProof := Lean.mkApp (Lean.mkLambda `h .default badType (Lean.mkBVar 0))\n    Lean.reflBoolTrue\n  match Lean.Kernel.check env {} badProof with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the negative control\"\n  let corrupt := value.replace fun e => match e with\n    | .lit (.natVal n) => if n == 9223372036904058881 then some (Lean.mkRawNatLit (n + 2)) else none\n    | _ => none\n  if corrupt == value then throwError \"subject corruption did not change the proof\"\n  let corrupt := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corrupt\n  match Lean.Kernel.check env {} corrupt with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the corrupted proof\"\n  -- Change only a Hex witness base: subjects, products, and ordering remain\n  -- intact, so this control must reach the witness arithmetic.\n  let corruptWitness := value.replace fun e => Id.run do\n    unless e.isAppOfArity `Hex.Nat.PrimeCert.pock 2 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3 5 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3Sieve 6 do return none\n    let args := e.getAppArgs\n    let fs := args.back!\n    unless fs.isAppOfArity ``List.cons 3 do return none\n    let fsArgs := fs.getAppArgs\n    let entry := fsArgs[1]!\n    unless entry.isAppOfArity ``Prod.mk 4 do return none\n    let entryArgs := entry.getAppArgs\n    let entry := Lean.mkAppN entry.getAppFn (entryArgs.set! 2 (Lean.mkRawNatLit 0))\n    let fs := Lean.mkAppN fs.getAppFn (fsArgs.set! 1 entry)\n    return some (Lean.mkAppN e.getAppFn (args.set! (args.size - 1) fs))\n  let needsWitness := value.getUsedConstants.any fun name =>\n    name == `Hex.Nat.PrimeCert.pock || name == `Hex.Nat.PrimeCert.pock3 ||\n      name == `Hex.Nat.PrimeCert.pock3Sieve\n  if needsWitness && corruptWitness == value then\n    throwError \"witness corruption did not change the proof\"\n  if corruptWitness != value then\n    let bad := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corruptWitness\n    match Lean.Kernel.check env {} bad with\n    | .error _ => pure ()\n    | .ok _ => throwError \"kernel accepted the zero witness base\"\n    Lean.logInfo \"DIRECT_WITNESS_CONTROL rejected\"\n  for _ in [:8] do\n    let input \u2190 IO.mkRef (env, proof)\n    let (env, proof) \u2190 input.get\n    let start \u2190 IO.monoNanosNow\n    let checked \u2190 IO.mkRef (Lean.Kernel.check env {} proof)\n    let checked \u2190 checked.get\n    let stop \u2190 IO.monoNanosNow\n    match checked with\n    | .error _ => throwError \"kernel recheck failed\"\n    | .ok _ => pure ()\n    Lean.logInfo m!\"DIRECT_KERNEL_NS {stop - start}\"\n    Lean.logInfo m!\"DIRECT_DEPENDENCIES {value.getUsedConstants}\"\n\n-- Measurement block 1, arm m4.\n",
      "ns": [
        1134873,
        1007153,
        1050347,
        971380,
        961375,
        967163,
        965872,
        962316
      ]
    },
    {
      "block": 1,
      "arm": "m1",
      "stdout": "\u2139 [70/70] Built HexPrimality.SieveToolsProbe (1.3s)\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_WITNESS_CONTROL rejected\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1277524\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1296692\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1208993\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1195012\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1185017\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1187571\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1175473\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1178547\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\nBuild completed successfully (70 jobs).\n",
      "stderr": "",
      "returncode": 0,
      "source": "module\npublic import HexPrimality.Cert\npublic import Lean\npublic meta import Lean\npublic section\nset_option maxRecDepth 100000\nopen Hex.Nat\nmutual\n@[expose] def oldCheck : PrimeCert \u2192 Bool\n  | .small n => tableSearch n\n  | .pock n fs => checkPockArith n fs && oldChildren fs\n  | .pock3 n r s w fs => checkPock3Arith n r s w fs && oldChildren fs\n  | .pock3Sieve n r s w m fs => checkPock3SieveArith n r s w m fs && oldChildren fs\n@[expose] def oldChildren : List (Nat \u00d7 Nat \u00d7 PrimeCert) \u2192 Bool\n  | [] => true\n  | (_, _, c) :: cs => oldCheck c && oldChildren cs\nend\n\ndef certificate : PrimeCert := .pock3 9223372036904058881 1677731 167772 1677730 [(3, 19, .small 2), (2, 0, .small 5)]\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime 9223372036904058881 := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n\nmeta partial def inlineLocal (env : Lean.Environment) (e : Lean.Expr) : Lean.Expr :=\n  e.replace fun sub => match sub with\n    | .const n levels =>\n      if env.isImportedConst n then none else\n        match env.find? n with\n        | some info => (info.value? (allowOpaque := true)).map fun value =>\n            inlineLocal env (value.instantiateLevelParams info.levelParams levels)\n        | none => none\n    | _ => none\n\nrun_cmd do\n  let env \u2190 Lean.getEnv\n  let some (.thmInfo info) := env.find? `result\n    | throwError \"missing result theorem\"\n  let value := inlineLocal env info.value\n  let type := inlineLocal env info.type\n  unless (value.getUsedConstants ++ type.getUsedConstants).all env.isImportedConst do\n    throwError \"unexpanded local proof dependency\"\n  -- The identity application checks the proof against its declared goal type.\n  let proof := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) value\n  -- Explicitly finish pending elaboration-time kernel tasks before timing.\n  let ready \u2190 IO.mkRef env.toKernelEnv\n  let ready \u2190 ready.get\n  let env := Lean.Environment.ofKernelEnv ready\n  -- An invalid equality must be rejected by this same kernel entry point.\n  let badType := Lean.mkApp3 (Lean.mkConst ``Eq [.succ .zero])\n    (Lean.mkConst ``Bool) (Lean.mkConst ``Bool.true) (Lean.mkConst ``Bool.false)\n  let badProof := Lean.mkApp (Lean.mkLambda `h .default badType (Lean.mkBVar 0))\n    Lean.reflBoolTrue\n  match Lean.Kernel.check env {} badProof with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the negative control\"\n  let corrupt := value.replace fun e => match e with\n    | .lit (.natVal n) => if n == 9223372036904058881 then some (Lean.mkRawNatLit (n + 2)) else none\n    | _ => none\n  if corrupt == value then throwError \"subject corruption did not change the proof\"\n  let corrupt := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corrupt\n  match Lean.Kernel.check env {} corrupt with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the corrupted proof\"\n  -- Change only a Hex witness base: subjects, products, and ordering remain\n  -- intact, so this control must reach the witness arithmetic.\n  let corruptWitness := value.replace fun e => Id.run do\n    unless e.isAppOfArity `Hex.Nat.PrimeCert.pock 2 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3 5 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3Sieve 6 do return none\n    let args := e.getAppArgs\n    let fs := args.back!\n    unless fs.isAppOfArity ``List.cons 3 do return none\n    let fsArgs := fs.getAppArgs\n    let entry := fsArgs[1]!\n    unless entry.isAppOfArity ``Prod.mk 4 do return none\n    let entryArgs := entry.getAppArgs\n    let entry := Lean.mkAppN entry.getAppFn (entryArgs.set! 2 (Lean.mkRawNatLit 0))\n    let fs := Lean.mkAppN fs.getAppFn (fsArgs.set! 1 entry)\n    return some (Lean.mkAppN e.getAppFn (args.set! (args.size - 1) fs))\n  let needsWitness := value.getUsedConstants.any fun name =>\n    name == `Hex.Nat.PrimeCert.pock || name == `Hex.Nat.PrimeCert.pock3 ||\n      name == `Hex.Nat.PrimeCert.pock3Sieve\n  if needsWitness && corruptWitness == value then\n    throwError \"witness corruption did not change the proof\"\n  if corruptWitness != value then\n    let bad := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corruptWitness\n    match Lean.Kernel.check env {} bad with\n    | .error _ => pure ()\n    | .ok _ => throwError \"kernel accepted the zero witness base\"\n    Lean.logInfo \"DIRECT_WITNESS_CONTROL rejected\"\n  for _ in [:8] do\n    let input \u2190 IO.mkRef (env, proof)\n    let (env, proof) \u2190 input.get\n    let start \u2190 IO.monoNanosNow\n    let checked \u2190 IO.mkRef (Lean.Kernel.check env {} proof)\n    let checked \u2190 checked.get\n    let stop \u2190 IO.monoNanosNow\n    match checked with\n    | .error _ => throwError \"kernel recheck failed\"\n    | .ok _ => pure ()\n    Lean.logInfo m!\"DIRECT_KERNEL_NS {stop - start}\"\n    Lean.logInfo m!\"DIRECT_DEPENDENCIES {value.getUsedConstants}\"\n\n-- Measurement block 1, arm m1.\n",
      "ns": [
        1277524,
        1296692,
        1208993,
        1195012,
        1185017,
        1187571,
        1175473,
        1178547
      ]
    },
    {
      "block": 2,
      "arm": "m1",
      "stdout": "\u2139 [70/70] Built HexPrimality.SieveToolsProbe (1.3s)\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_WITNESS_CONTROL rejected\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1252266\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1213399\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1198647\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1193089\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1191296\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1190195\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1187511\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1183024\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\nBuild completed successfully (70 jobs).\n",
      "stderr": "",
      "returncode": 0,
      "source": "module\npublic import HexPrimality.Cert\npublic import Lean\npublic meta import Lean\npublic section\nset_option maxRecDepth 100000\nopen Hex.Nat\nmutual\n@[expose] def oldCheck : PrimeCert \u2192 Bool\n  | .small n => tableSearch n\n  | .pock n fs => checkPockArith n fs && oldChildren fs\n  | .pock3 n r s w fs => checkPock3Arith n r s w fs && oldChildren fs\n  | .pock3Sieve n r s w m fs => checkPock3SieveArith n r s w m fs && oldChildren fs\n@[expose] def oldChildren : List (Nat \u00d7 Nat \u00d7 PrimeCert) \u2192 Bool\n  | [] => true\n  | (_, _, c) :: cs => oldCheck c && oldChildren cs\nend\n\ndef certificate : PrimeCert := .pock3 9223372036904058881 1677731 167772 1677730 [(3, 19, .small 2), (2, 0, .small 5)]\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime 9223372036904058881 := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n\nmeta partial def inlineLocal (env : Lean.Environment) (e : Lean.Expr) : Lean.Expr :=\n  e.replace fun sub => match sub with\n    | .const n levels =>\n      if env.isImportedConst n then none else\n        match env.find? n with\n        | some info => (info.value? (allowOpaque := true)).map fun value =>\n            inlineLocal env (value.instantiateLevelParams info.levelParams levels)\n        | none => none\n    | _ => none\n\nrun_cmd do\n  let env \u2190 Lean.getEnv\n  let some (.thmInfo info) := env.find? `result\n    | throwError \"missing result theorem\"\n  let value := inlineLocal env info.value\n  let type := inlineLocal env info.type\n  unless (value.getUsedConstants ++ type.getUsedConstants).all env.isImportedConst do\n    throwError \"unexpanded local proof dependency\"\n  -- The identity application checks the proof against its declared goal type.\n  let proof := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) value\n  -- Explicitly finish pending elaboration-time kernel tasks before timing.\n  let ready \u2190 IO.mkRef env.toKernelEnv\n  let ready \u2190 ready.get\n  let env := Lean.Environment.ofKernelEnv ready\n  -- An invalid equality must be rejected by this same kernel entry point.\n  let badType := Lean.mkApp3 (Lean.mkConst ``Eq [.succ .zero])\n    (Lean.mkConst ``Bool) (Lean.mkConst ``Bool.true) (Lean.mkConst ``Bool.false)\n  let badProof := Lean.mkApp (Lean.mkLambda `h .default badType (Lean.mkBVar 0))\n    Lean.reflBoolTrue\n  match Lean.Kernel.check env {} badProof with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the negative control\"\n  let corrupt := value.replace fun e => match e with\n    | .lit (.natVal n) => if n == 9223372036904058881 then some (Lean.mkRawNatLit (n + 2)) else none\n    | _ => none\n  if corrupt == value then throwError \"subject corruption did not change the proof\"\n  let corrupt := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corrupt\n  match Lean.Kernel.check env {} corrupt with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the corrupted proof\"\n  -- Change only a Hex witness base: subjects, products, and ordering remain\n  -- intact, so this control must reach the witness arithmetic.\n  let corruptWitness := value.replace fun e => Id.run do\n    unless e.isAppOfArity `Hex.Nat.PrimeCert.pock 2 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3 5 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3Sieve 6 do return none\n    let args := e.getAppArgs\n    let fs := args.back!\n    unless fs.isAppOfArity ``List.cons 3 do return none\n    let fsArgs := fs.getAppArgs\n    let entry := fsArgs[1]!\n    unless entry.isAppOfArity ``Prod.mk 4 do return none\n    let entryArgs := entry.getAppArgs\n    let entry := Lean.mkAppN entry.getAppFn (entryArgs.set! 2 (Lean.mkRawNatLit 0))\n    let fs := Lean.mkAppN fs.getAppFn (fsArgs.set! 1 entry)\n    return some (Lean.mkAppN e.getAppFn (args.set! (args.size - 1) fs))\n  let needsWitness := value.getUsedConstants.any fun name =>\n    name == `Hex.Nat.PrimeCert.pock || name == `Hex.Nat.PrimeCert.pock3 ||\n      name == `Hex.Nat.PrimeCert.pock3Sieve\n  if needsWitness && corruptWitness == value then\n    throwError \"witness corruption did not change the proof\"\n  if corruptWitness != value then\n    let bad := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corruptWitness\n    match Lean.Kernel.check env {} bad with\n    | .error _ => pure ()\n    | .ok _ => throwError \"kernel accepted the zero witness base\"\n    Lean.logInfo \"DIRECT_WITNESS_CONTROL rejected\"\n  for _ in [:8] do\n    let input \u2190 IO.mkRef (env, proof)\n    let (env, proof) \u2190 input.get\n    let start \u2190 IO.monoNanosNow\n    let checked \u2190 IO.mkRef (Lean.Kernel.check env {} proof)\n    let checked \u2190 checked.get\n    let stop \u2190 IO.monoNanosNow\n    match checked with\n    | .error _ => throwError \"kernel recheck failed\"\n    | .ok _ => pure ()\n    Lean.logInfo m!\"DIRECT_KERNEL_NS {stop - start}\"\n    Lean.logInfo m!\"DIRECT_DEPENDENCIES {value.getUsedConstants}\"\n\n-- Measurement block 2, arm m1.\n",
      "ns": [
        1252266,
        1213399,
        1198647,
        1193089,
        1191296,
        1190195,
        1187511,
        1183024
      ]
    },
    {
      "block": 2,
      "arm": "m4",
      "stdout": "\u2139 [70/70] Built HexPrimality.SieveToolsProbe (1.3s)\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_WITNESS_CONTROL rejected\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1068625\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1087793\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 989967\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 973042\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 965301\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 957269\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 967014\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 964840\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\nBuild completed successfully (70 jobs).\n",
      "stderr": "",
      "returncode": 0,
      "source": "module\npublic import HexPrimality.Cert\npublic import Lean\npublic meta import Lean\npublic section\nset_option maxRecDepth 100000\nopen Hex.Nat\nmutual\n@[expose] def oldCheck : PrimeCert \u2192 Bool\n  | .small n => tableSearch n\n  | .pock n fs => checkPockArith n fs && oldChildren fs\n  | .pock3 n r s w fs => checkPock3Arith n r s w fs && oldChildren fs\n  | .pock3Sieve n r s w m fs => checkPock3SieveArith n r s w m fs && oldChildren fs\n@[expose] def oldChildren : List (Nat \u00d7 Nat \u00d7 PrimeCert) \u2192 Bool\n  | [] => true\n  | (_, _, c) :: cs => oldCheck c && oldChildren cs\nend\n\ndef certificate : PrimeCert := .pock3Sieve 9223372036904058881 47 4194304 0 4 [(3, 19, .small 2)]\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime 9223372036904058881 := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n\nmeta partial def inlineLocal (env : Lean.Environment) (e : Lean.Expr) : Lean.Expr :=\n  e.replace fun sub => match sub with\n    | .const n levels =>\n      if env.isImportedConst n then none else\n        match env.find? n with\n        | some info => (info.value? (allowOpaque := true)).map fun value =>\n            inlineLocal env (value.instantiateLevelParams info.levelParams levels)\n        | none => none\n    | _ => none\n\nrun_cmd do\n  let env \u2190 Lean.getEnv\n  let some (.thmInfo info) := env.find? `result\n    | throwError \"missing result theorem\"\n  let value := inlineLocal env info.value\n  let type := inlineLocal env info.type\n  unless (value.getUsedConstants ++ type.getUsedConstants).all env.isImportedConst do\n    throwError \"unexpanded local proof dependency\"\n  -- The identity application checks the proof against its declared goal type.\n  let proof := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) value\n  -- Explicitly finish pending elaboration-time kernel tasks before timing.\n  let ready \u2190 IO.mkRef env.toKernelEnv\n  let ready \u2190 ready.get\n  let env := Lean.Environment.ofKernelEnv ready\n  -- An invalid equality must be rejected by this same kernel entry point.\n  let badType := Lean.mkApp3 (Lean.mkConst ``Eq [.succ .zero])\n    (Lean.mkConst ``Bool) (Lean.mkConst ``Bool.true) (Lean.mkConst ``Bool.false)\n  let badProof := Lean.mkApp (Lean.mkLambda `h .default badType (Lean.mkBVar 0))\n    Lean.reflBoolTrue\n  match Lean.Kernel.check env {} badProof with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the negative control\"\n  let corrupt := value.replace fun e => match e with\n    | .lit (.natVal n) => if n == 9223372036904058881 then some (Lean.mkRawNatLit (n + 2)) else none\n    | _ => none\n  if corrupt == value then throwError \"subject corruption did not change the proof\"\n  let corrupt := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corrupt\n  match Lean.Kernel.check env {} corrupt with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the corrupted proof\"\n  -- Change only a Hex witness base: subjects, products, and ordering remain\n  -- intact, so this control must reach the witness arithmetic.\n  let corruptWitness := value.replace fun e => Id.run do\n    unless e.isAppOfArity `Hex.Nat.PrimeCert.pock 2 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3 5 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3Sieve 6 do return none\n    let args := e.getAppArgs\n    let fs := args.back!\n    unless fs.isAppOfArity ``List.cons 3 do return none\n    let fsArgs := fs.getAppArgs\n    let entry := fsArgs[1]!\n    unless entry.isAppOfArity ``Prod.mk 4 do return none\n    let entryArgs := entry.getAppArgs\n    let entry := Lean.mkAppN entry.getAppFn (entryArgs.set! 2 (Lean.mkRawNatLit 0))\n    let fs := Lean.mkAppN fs.getAppFn (fsArgs.set! 1 entry)\n    return some (Lean.mkAppN e.getAppFn (args.set! (args.size - 1) fs))\n  let needsWitness := value.getUsedConstants.any fun name =>\n    name == `Hex.Nat.PrimeCert.pock || name == `Hex.Nat.PrimeCert.pock3 ||\n      name == `Hex.Nat.PrimeCert.pock3Sieve\n  if needsWitness && corruptWitness == value then\n    throwError \"witness corruption did not change the proof\"\n  if corruptWitness != value then\n    let bad := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corruptWitness\n    match Lean.Kernel.check env {} bad with\n    | .error _ => pure ()\n    | .ok _ => throwError \"kernel accepted the zero witness base\"\n    Lean.logInfo \"DIRECT_WITNESS_CONTROL rejected\"\n  for _ in [:8] do\n    let input \u2190 IO.mkRef (env, proof)\n    let (env, proof) \u2190 input.get\n    let start \u2190 IO.monoNanosNow\n    let checked \u2190 IO.mkRef (Lean.Kernel.check env {} proof)\n    let checked \u2190 checked.get\n    let stop \u2190 IO.monoNanosNow\n    match checked with\n    | .error _ => throwError \"kernel recheck failed\"\n    | .ok _ => pure ()\n    Lean.logInfo m!\"DIRECT_KERNEL_NS {stop - start}\"\n    Lean.logInfo m!\"DIRECT_DEPENDENCIES {value.getUsedConstants}\"\n\n-- Measurement block 2, arm m4.\n",
      "ns": [
        1068625,
        1087793,
        989967,
        973042,
        965301,
        957269,
        967014,
        964840
      ]
    },
    {
      "block": 3,
      "arm": "m4",
      "stdout": "\u2139 [70/70] Built HexPrimality.SieveToolsProbe (1.3s)\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_WITNESS_CONTROL rejected\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1046131\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1065450\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 993503\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 975416\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 973604\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 961336\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 968245\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 958150\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3Sieve,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\nBuild completed successfully (70 jobs).\n",
      "stderr": "",
      "returncode": 0,
      "source": "module\npublic import HexPrimality.Cert\npublic import Lean\npublic meta import Lean\npublic section\nset_option maxRecDepth 100000\nopen Hex.Nat\nmutual\n@[expose] def oldCheck : PrimeCert \u2192 Bool\n  | .small n => tableSearch n\n  | .pock n fs => checkPockArith n fs && oldChildren fs\n  | .pock3 n r s w fs => checkPock3Arith n r s w fs && oldChildren fs\n  | .pock3Sieve n r s w m fs => checkPock3SieveArith n r s w m fs && oldChildren fs\n@[expose] def oldChildren : List (Nat \u00d7 Nat \u00d7 PrimeCert) \u2192 Bool\n  | [] => true\n  | (_, _, c) :: cs => oldCheck c && oldChildren cs\nend\n\ndef certificate : PrimeCert := .pock3Sieve 9223372036904058881 47 4194304 0 4 [(3, 19, .small 2)]\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime 9223372036904058881 := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n\nmeta partial def inlineLocal (env : Lean.Environment) (e : Lean.Expr) : Lean.Expr :=\n  e.replace fun sub => match sub with\n    | .const n levels =>\n      if env.isImportedConst n then none else\n        match env.find? n with\n        | some info => (info.value? (allowOpaque := true)).map fun value =>\n            inlineLocal env (value.instantiateLevelParams info.levelParams levels)\n        | none => none\n    | _ => none\n\nrun_cmd do\n  let env \u2190 Lean.getEnv\n  let some (.thmInfo info) := env.find? `result\n    | throwError \"missing result theorem\"\n  let value := inlineLocal env info.value\n  let type := inlineLocal env info.type\n  unless (value.getUsedConstants ++ type.getUsedConstants).all env.isImportedConst do\n    throwError \"unexpanded local proof dependency\"\n  -- The identity application checks the proof against its declared goal type.\n  let proof := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) value\n  -- Explicitly finish pending elaboration-time kernel tasks before timing.\n  let ready \u2190 IO.mkRef env.toKernelEnv\n  let ready \u2190 ready.get\n  let env := Lean.Environment.ofKernelEnv ready\n  -- An invalid equality must be rejected by this same kernel entry point.\n  let badType := Lean.mkApp3 (Lean.mkConst ``Eq [.succ .zero])\n    (Lean.mkConst ``Bool) (Lean.mkConst ``Bool.true) (Lean.mkConst ``Bool.false)\n  let badProof := Lean.mkApp (Lean.mkLambda `h .default badType (Lean.mkBVar 0))\n    Lean.reflBoolTrue\n  match Lean.Kernel.check env {} badProof with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the negative control\"\n  let corrupt := value.replace fun e => match e with\n    | .lit (.natVal n) => if n == 9223372036904058881 then some (Lean.mkRawNatLit (n + 2)) else none\n    | _ => none\n  if corrupt == value then throwError \"subject corruption did not change the proof\"\n  let corrupt := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corrupt\n  match Lean.Kernel.check env {} corrupt with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the corrupted proof\"\n  -- Change only a Hex witness base: subjects, products, and ordering remain\n  -- intact, so this control must reach the witness arithmetic.\n  let corruptWitness := value.replace fun e => Id.run do\n    unless e.isAppOfArity `Hex.Nat.PrimeCert.pock 2 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3 5 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3Sieve 6 do return none\n    let args := e.getAppArgs\n    let fs := args.back!\n    unless fs.isAppOfArity ``List.cons 3 do return none\n    let fsArgs := fs.getAppArgs\n    let entry := fsArgs[1]!\n    unless entry.isAppOfArity ``Prod.mk 4 do return none\n    let entryArgs := entry.getAppArgs\n    let entry := Lean.mkAppN entry.getAppFn (entryArgs.set! 2 (Lean.mkRawNatLit 0))\n    let fs := Lean.mkAppN fs.getAppFn (fsArgs.set! 1 entry)\n    return some (Lean.mkAppN e.getAppFn (args.set! (args.size - 1) fs))\n  let needsWitness := value.getUsedConstants.any fun name =>\n    name == `Hex.Nat.PrimeCert.pock || name == `Hex.Nat.PrimeCert.pock3 ||\n      name == `Hex.Nat.PrimeCert.pock3Sieve\n  if needsWitness && corruptWitness == value then\n    throwError \"witness corruption did not change the proof\"\n  if corruptWitness != value then\n    let bad := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corruptWitness\n    match Lean.Kernel.check env {} bad with\n    | .error _ => pure ()\n    | .ok _ => throwError \"kernel accepted the zero witness base\"\n    Lean.logInfo \"DIRECT_WITNESS_CONTROL rejected\"\n  for _ in [:8] do\n    let input \u2190 IO.mkRef (env, proof)\n    let (env, proof) \u2190 input.get\n    let start \u2190 IO.monoNanosNow\n    let checked \u2190 IO.mkRef (Lean.Kernel.check env {} proof)\n    let checked \u2190 checked.get\n    let stop \u2190 IO.monoNanosNow\n    match checked with\n    | .error _ => throwError \"kernel recheck failed\"\n    | .ok _ => pure ()\n    Lean.logInfo m!\"DIRECT_KERNEL_NS {stop - start}\"\n    Lean.logInfo m!\"DIRECT_DEPENDENCIES {value.getUsedConstants}\"\n\n-- Measurement block 3, arm m4.\n",
      "ns": [
        1046131,
        1065450,
        993503,
        975416,
        973604,
        961336,
        968245,
        958150
      ]
    },
    {
      "block": 3,
      "arm": "m1",
      "stdout": "\u2139 [70/70] Built HexPrimality.SieveToolsProbe (1.3s)\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_WITNESS_CONTROL rejected\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1249562\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1213179\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1266197\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1205898\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1190104\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1186599\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1186038\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_KERNEL_NS 1181872\ninfo: HexPrimality/SieveToolsProbe.lean:33:0: DIRECT_DEPENDENCIES [Hex.Nat.prime_of_checkPrimeAt,\n OfNat.ofNat,\n Nat,\n instOfNatNat,\n Hex.Nat.PrimeCert.pock3,\n List.cons,\n Prod,\n Hex.Nat.PrimeCert,\n Prod.mk,\n Hex.Nat.PrimeCert.small,\n List.nil,\n of_decide_eq_true,\n Eq,\n Bool,\n Bool.and,\n BEq.beq,\n instBEqOfDecidableEq,\n instDecidableEqNat,\n Hex.Nat.PrimeCert.subject,\n Hex.Nat.checkPrime,\n Bool.true,\n instDecidableEqBool,\n id,\n Decidable.decide,\n Eq.refl]\nBuild completed successfully (70 jobs).\n",
      "stderr": "",
      "returncode": 0,
      "source": "module\npublic import HexPrimality.Cert\npublic import Lean\npublic meta import Lean\npublic section\nset_option maxRecDepth 100000\nopen Hex.Nat\nmutual\n@[expose] def oldCheck : PrimeCert \u2192 Bool\n  | .small n => tableSearch n\n  | .pock n fs => checkPockArith n fs && oldChildren fs\n  | .pock3 n r s w fs => checkPock3Arith n r s w fs && oldChildren fs\n  | .pock3Sieve n r s w m fs => checkPock3SieveArith n r s w m fs && oldChildren fs\n@[expose] def oldChildren : List (Nat \u00d7 Nat \u00d7 PrimeCert) \u2192 Bool\n  | [] => true\n  | (_, _, c) :: cs => oldCheck c && oldChildren cs\nend\n\ndef certificate : PrimeCert := .pock3 9223372036904058881 1677731 167772 1677730 [(3, 19, .small 2), (2, 0, .small 5)]\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime 9223372036904058881 := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n\nmeta partial def inlineLocal (env : Lean.Environment) (e : Lean.Expr) : Lean.Expr :=\n  e.replace fun sub => match sub with\n    | .const n levels =>\n      if env.isImportedConst n then none else\n        match env.find? n with\n        | some info => (info.value? (allowOpaque := true)).map fun value =>\n            inlineLocal env (value.instantiateLevelParams info.levelParams levels)\n        | none => none\n    | _ => none\n\nrun_cmd do\n  let env \u2190 Lean.getEnv\n  let some (.thmInfo info) := env.find? `result\n    | throwError \"missing result theorem\"\n  let value := inlineLocal env info.value\n  let type := inlineLocal env info.type\n  unless (value.getUsedConstants ++ type.getUsedConstants).all env.isImportedConst do\n    throwError \"unexpanded local proof dependency\"\n  -- The identity application checks the proof against its declared goal type.\n  let proof := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) value\n  -- Explicitly finish pending elaboration-time kernel tasks before timing.\n  let ready \u2190 IO.mkRef env.toKernelEnv\n  let ready \u2190 ready.get\n  let env := Lean.Environment.ofKernelEnv ready\n  -- An invalid equality must be rejected by this same kernel entry point.\n  let badType := Lean.mkApp3 (Lean.mkConst ``Eq [.succ .zero])\n    (Lean.mkConst ``Bool) (Lean.mkConst ``Bool.true) (Lean.mkConst ``Bool.false)\n  let badProof := Lean.mkApp (Lean.mkLambda `h .default badType (Lean.mkBVar 0))\n    Lean.reflBoolTrue\n  match Lean.Kernel.check env {} badProof with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the negative control\"\n  let corrupt := value.replace fun e => match e with\n    | .lit (.natVal n) => if n == 9223372036904058881 then some (Lean.mkRawNatLit (n + 2)) else none\n    | _ => none\n  if corrupt == value then throwError \"subject corruption did not change the proof\"\n  let corrupt := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corrupt\n  match Lean.Kernel.check env {} corrupt with\n  | .error _ => pure ()\n  | .ok _ => throwError \"kernel accepted the corrupted proof\"\n  -- Change only a Hex witness base: subjects, products, and ordering remain\n  -- intact, so this control must reach the witness arithmetic.\n  let corruptWitness := value.replace fun e => Id.run do\n    unless e.isAppOfArity `Hex.Nat.PrimeCert.pock 2 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3 5 ||\n        e.isAppOfArity `Hex.Nat.PrimeCert.pock3Sieve 6 do return none\n    let args := e.getAppArgs\n    let fs := args.back!\n    unless fs.isAppOfArity ``List.cons 3 do return none\n    let fsArgs := fs.getAppArgs\n    let entry := fsArgs[1]!\n    unless entry.isAppOfArity ``Prod.mk 4 do return none\n    let entryArgs := entry.getAppArgs\n    let entry := Lean.mkAppN entry.getAppFn (entryArgs.set! 2 (Lean.mkRawNatLit 0))\n    let fs := Lean.mkAppN fs.getAppFn (fsArgs.set! 1 entry)\n    return some (Lean.mkAppN e.getAppFn (args.set! (args.size - 1) fs))\n  let needsWitness := value.getUsedConstants.any fun name =>\n    name == `Hex.Nat.PrimeCert.pock || name == `Hex.Nat.PrimeCert.pock3 ||\n      name == `Hex.Nat.PrimeCert.pock3Sieve\n  if needsWitness && corruptWitness == value then\n    throwError \"witness corruption did not change the proof\"\n  if corruptWitness != value then\n    let bad := Lean.mkApp (Lean.mkLambda `h .default type (Lean.mkBVar 0)) corruptWitness\n    match Lean.Kernel.check env {} bad with\n    | .error _ => pure ()\n    | .ok _ => throwError \"kernel accepted the zero witness base\"\n    Lean.logInfo \"DIRECT_WITNESS_CONTROL rejected\"\n  for _ in [:8] do\n    let input \u2190 IO.mkRef (env, proof)\n    let (env, proof) \u2190 input.get\n    let start \u2190 IO.monoNanosNow\n    let checked \u2190 IO.mkRef (Lean.Kernel.check env {} proof)\n    let checked \u2190 checked.get\n    let stop \u2190 IO.monoNanosNow\n    match checked with\n    | .error _ => throwError \"kernel recheck failed\"\n    | .ok _ => pure ()\n    Lean.logInfo m!\"DIRECT_KERNEL_NS {stop - start}\"\n    Lean.logInfo m!\"DIRECT_DEPENDENCIES {value.getUsedConstants}\"\n\n-- Measurement block 3, arm m1.\n",
      "ns": [
        1249562,
        1213179,
        1266197,
        1205898,
        1190104,
        1186599,
        1186038,
        1181872
      ]
    }
  ],
  "load_after": [
    3.91064453125,
    3.568359375,
    3.931640625
  ]
}

hex-sieve-replay.md

Hex sieve replay comparison

Source: hex-dev 0e25d5f94. Target: 9223372036904058881 (64 bits).

Certificate	Factor product	Median kernel replay
Original pock3, m=1	2^20 × 5	1.193 ms
New pock3Sieve, m=4	2^20	0.970 ms

These are direct Lean.Kernel.check timings with the local proof expanded, not whole build times or native certificate construction. Both proofs use the same current Hex checker. The new certificate removes one witness entry in exchange for three divisor exclusions. This single example shows that tradeoff; it does not establish a general speedup.

Four adjacent blocks alternate arm order; each build performs eight fresh kernel checks. Every completed sample, full Lean source, output and shared-host load record is in hex-sieve-record.json. CPU affinity is selected by a lock. The runner changes source per arm/block so Lake cannot replay cached build logs. Invalid equality, subject and witness controls must be rejected.

An initial run mistakenly reused cached build logs. Its complete record is retained separately as hex-sieve-invalid-cached-log-record.json and is excluded from these timings because those entries are not new executions.

To reproduce on Linux, check out the source commit, run lake build, then:

python3 hex-sieve-replay.py /path/to/hex-dev /tmp/hex-sieve-replay

The summary above takes the median of all 32 observations per arm. This manual experiment is not added to CI. Host-specific absolute times will vary.

hex-sieve-replay.py

from pathlib import Path
import sys,json,math,subprocess,os,fcntl,statistics,re
root=Path(sys.argv[1]).resolve();sys.path.insert(0,str(root))
from scripts.bench.primality_table_replay import HEADER
from scripts.bench.primality_kernel_direct import SUFFIX
out=Path(sys.argv[2]).resolve();out.mkdir(parents=True,exist_ok=True)
n=9223372036904058881;F=2**20*5;R=(n-1)//F;r=R%(2*F);s=R//(2*F);w=math.isqrt(max(0,r*r-8*s))
a=next(a for a in range(2,100) if math.gcd(pow(a,(n-1)//5,n)-1,n)==1)
old=f'.pock3 {n} {r} {s} {w} [(3, 19, .small 2), ({a}, 0, .small 5)]'
new=f'.pock3Sieve {n} 47 4194304 0 4 [(3, 19, .small 2)]'
for cpu in sorted(os.sched_getaffinity(0)):
 f=open(f'/tmp/hex-benchmark-cpu-{cpu}.lock','w')
 try:fcntl.flock(f,fcntl.LOCK_EX|fcntl.LOCK_NB)
 except BlockingIOError:f.close();continue
 break
os.sched_setaffinity(0,{cpu});record=dict(cpu=cpu,load_before=os.getloadavg(),rows=[])
p=root/'HexPrimality/SieveToolsProbe.lean';assert not p.exists()
try:
 for block in range(4):
  for arm,cert in ([('m1',old),('m4',new)] if block%2==0 else [('m4',new),('m1',old)]):
   src=HEADER.replace('public import HexPrimality.Cert','public import HexPrimality.Cert\npublic import Lean\npublic meta import Lean')
   src+=f'\ndef certificate : PrimeCert := {cert}\ntheorem oldResult : oldCheck certificate = true := by decide +kernel\ntheorem result : Hex.Nat.Prime {n} := Hex.Nat.prime_of_checkPrimeAt (c := certificate) (by decide +kernel)\n'
   suffix=SUFFIX.replace('RESULT_NAME','result').replace('SUBJECT',str(n))
   marker=suffix.index('  let input ← IO.mkRef (env, proof)')
   suffix=suffix[:marker]+'  for _ in [:8] do\n'+'\n'.join('  '+l for l in suffix[marker:].splitlines())+'\n'
   src+=suffix+f"\n-- Measurement block {block}, arm {arm}.\n";p.write_text(src)
   res=subprocess.run(['lake','build','HexPrimality.SieveToolsProbe'],cwd=root,capture_output=True,text=True)
   row=dict(block=block,arm=arm,stdout=res.stdout,stderr=res.stderr,returncode=res.returncode,source=src)
   row['ns']=list(map(int,re.findall(r'DIRECT_KERNEL_NS (\d+)',res.stdout)))
   record['rows'].append(row);(out/'record.json').write_text(json.dumps(record,indent=2))
   if res.returncode or len(row['ns'])!=8 or 'DIRECT_WITNESS_CONTROL rejected' not in res.stdout:raise RuntimeError(res.stdout+res.stderr)
   print(block,arm,statistics.median(row['ns'])/1000,flush=True)
finally:p.unlink()
record['load_after']=os.getloadavg();(out/'record.json').write_text(json.dumps(record,indent=2))

IntervalBench.lean

module
import Lean
import PrimeCert.Pocklington3
meta import Lean
open Lean
set_option maxRecDepth 10000

run_cmd do
  let ready ← IO.mkRef (← getEnv).toKernelEnv
  let env := Environment.ofKernelEnv (← ready.get)
  let some path ← IO.getEnv "INTERVAL_SAMPLES" | throwError "set INTERVAL_SAMPLES"
  let file ← IO.FS.Handle.mk path .write
  let cases : List (Nat × Nat × Nat × Nat) :=
    [(69, 9, 68, 7), (4028945, 289, 4028944, 3),
     (2028478494862525422475607, 22304740449229861598212, 2028478494862525422475606, 3)]
  for block in [:4] do
    for (r, s, w, prime) in cases do
      let arms := if block % 2 == 0 then [false, true] else [true, false]
      for interval in arms do
        let mode := if interval then
          mkApp (mkConst ``PrimeCert.Pocklington3CertMode.interval) (mkRawNatLit w)
        else mkApp2 (mkConst ``PrimeCert.Pocklington3CertMode.prime) (mkRawNatLit prime)
          (mkConst (if prime == 3 then ``Nat.prime_three else ``Nat.prime_seven))
        let lhs := mkApp3 (mkConst ``PrimeCert.Pocklington3CertMode.calculate)
          mode (mkRawNatLit r) (mkRawNatLit s)
        let mkProof (b : Bool) :=
          let rhs := mkConst (if b then ``Bool.true else ``Bool.false)
          let type := mkApp3 (mkConst ``Eq [.succ .zero]) (mkConst ``Bool) lhs rhs
          mkApp (mkLambda `h .default type (mkBVar 0))
            (mkApp2 (mkConst ``Eq.refl [.succ .zero]) (mkConst ``Bool) rhs)
        let bad ← IO.mkRef (Kernel.check env {} (mkProof false))
        if (← bad.get).isOk then throwError "accepted wrong result"
        for i in [:64] do
          let input ← IO.mkRef (env, mkProof true)
          let (env, term) ← input.get
          let start ← IO.monoNanosNow
          let result ← IO.mkRef (Kernel.check env {} term)
          let result ← result.get
          let stop ← IO.monoNanosNow
          let _ ← ofExceptKernelException result
          file.putStrLn s!"{block},{r},{interval},{i},{stop-start}"
          file.flush

-- Retain fresh kernel checks under CPU affinity.

record.json

{
  "cpu": 90,
  "host": "chungus2",
  "load_before": [
    15.0458984375,
    30.59130859375,
    25.25537109375
  ],
  "stdout": "\u2714 [1954/1954] Built PrimeCertTest.IntervalBench (803ms)\nBuild completed successfully (1954 jobs).\n",
  "stderr": "",
  "returncode": 0,
  "load_after": [
    15.0458984375,
    30.59130859375,
    25.25537109375
  ]
}

replacement-cases.json

[
  {
    "n": 339392917,
    "bits": 29,
    "r": 17329,
    "s": 1,
    "w": 17328,
    "p": 3
  },
  {
    "n": 73471,
    "bits": 17,
    "r": 69,
    "s": 9,
    "w": 68,
    "p": 7
  },
  {
    "n": 32560621,
    "bits": 25,
    "r": 301,
    "s": 134,
    "w": 299,
    "p": 7
  },
  {
    "n": 3586530508831189,
    "bits": 52,
    "r": 71523,
    "s": 20763,
    "w": 71521,
    "p": 11
  },
  {
    "n": 236684654874665389773181956283167565443541280517430278333971,
    "bits": 198,
    "r": 111028891713715270858633,
    "s": 2169430279732,
    "w": 111028891713715270858632,
    "p": 3
  },
  {
    "n": 1809751,
    "bits": 21,
    "r": 239,
    "s": 14,
    "w": 238,
    "p": 11
  },
  {
    "n": 1923133,
    "bits": 21,
    "r": 631,
    "s": 3,
    "w": 630,
    "p": 5
  },
  {
    "n": 430751,
    "bits": 19,
    "r": 223,
    "s": 3,
    "w": 222,
    "p": 7
  },
  {
    "n": 31757755568855353,
    "bits": 55,
    "r": 1184777,
    "s": 1337,
    "w": 1184776,
    "p": 5
  },
  {
    "n": 74058212732561358302231226437062788676166966415465897661863160754340907,
    "bits": 236,
    "r": 284551513249666376365123,
    "s": 275754422668509854114502,
    "w": 284551513249666376365119,
    "p": 5
  },
  {
    "n": 411743,
    "bits": 19,
    "r": 23,
    "s": 61,
    "w": 6,
    "p": 3
  },
  {
    "n": 1469495262398780123809,
    "bits": 71,
    "r": 1728651,
    "s": 4232391,
    "w": 1728641,
    "p": 5
  },
  {
    "n": 97859369123353,
    "bits": 47,
    "r": 5439,
    "s": 2319,
    "w": 5437,
    "p": 7
  },
  {
    "n": 726838724295606890549323807888004534353641360687318060281490199180612328166730772686396383698676545930088884461843637361053498018365439,
    "bits": 448,
    "r": 523890102151522916311113076301980070234414163719,
    "s": 3637867751654793328228610486390601899590,
    "w": 523890102151522916311113076301980070234414163718,
    "p": 3
  },
  {
    "n": 18913,
    "bits": 15,
    "r": 5,
    "s": 1,
    "w": 4,
    "p": 3
  },
  {
    "n": 1257559732178653,
    "bits": 51,
    "r": 306251,
    "s": 139,
    "w": 306250,
    "p": 3
  }
]

replacement-record.json

{
  "cpu": 0,
  "load_before": [
    3.31884765625,
    6.9140625,
    8.5810546875
  ],
  "cases": 16,
  "stdout": "\u2714 [1962/1963] Built PrimeCertTest.ReplacementTest (2.5s)\n\u26a0 [1963/1963] Built PrimeCertTest.ReplacementBench (3.1s)\nwarning: PrimeCertTest/ReplacementBench.lean:27:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nwarning: PrimeCertTest/ReplacementBench.lean:37:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nBuild completed successfully (1963 jobs).\n",
  "stderr": "",
  "returncode": 0,
  "load_after": [
    3.45361328125,
    6.8818359375,
    8.5615234375
  ]
}

replacement-report.md

Replacing PrimeCert prime-QNR checks with interval checks

Local read-only review experiment on PR #170 at 3bfb28c. All 16 positive-QNR nodes from PrimeCertTest/PrimeListTest.lean were converted; the complete converted file built successfully, including Curve25519, Curve448 and the unchanged 3914-bit Proth example.

Fresh kernel checks of the nonsquare mode only, after imports and expression construction. Four alternating adjacent AB/BA blocks, 64 samples per arm per block; every completed sample retained. Wrong-result controls rejected. This is not total certificate replay or construction timing. Existing factor sets and auxiliary prime declarations retained.

Certificate bits	QNR prime	QNR µs	Interval µs	Speedup
29	3	63.44	29.62	2.14×
17	7	72.43	29.66	2.44×
25	7	72.49	29.63	2.45×
52	11	80.72	29.57	2.73×
198	3	63.96	31.42	2.04×
21	11	80.96	29.65	2.73×
21	5	71.99	29.69	2.42×
19	7	72.38	29.61	2.44×
55	5	71.74	29.61	2.42×
236	5	72.85	31.60	2.31×
19	3	63.53	29.67	2.14×
71	5	71.91	29.69	2.42×
47	7	72.79	29.71	2.45×
448	3	64.29	31.53	2.04×
15	3	63.69	29.65	2.15×
51	3	63.60	29.72	2.14×

Speedup range 2.04–2.73×; median per-node speedup 2.42×.

Reproduce

On PrimeCert commit 3bfb28c9e6bd890a3c8a2da3bf86799108cfe01c (the version exposing both modes), copy ReplacementBench.lean and ReplacementTest.lean into PrimeCertTest/, then run:

INTERVAL_SAMPLES=/tmp/replacement-samples.csv lake build PrimeCertTest.ReplacementBench PrimeCertTest.ReplacementTest

The benchmark hard-codes all sixteen cases, comparing each original prime-QNR witness against its interval witness. ReplacementTest.lean contains the converted complete example corpus. The measured run used CPU affinity (CPU 0); all raw samples and host context are included. These timings compare the two mode checks before removal of the QNR constructor. They do not measure automatic witness construction, import savings, or whole-certificate build times.

replacement-samples.csv

ReplacementBench.lean

module
import Lean
import PrimeCert.Pocklington3
meta import Lean
open Lean
set_option maxRecDepth 10000

run_cmd do
  let ready ← IO.mkRef (← getEnv).toKernelEnv
  let env := Environment.ofKernelEnv (← ready.get)
  let some path ← IO.getEnv "INTERVAL_SAMPLES" | throwError "set INTERVAL_SAMPLES"
  let file ← IO.FS.Handle.mk path .write
  let cases : List (Nat × Nat × Nat × Nat) :=
    [(17329, 1, 17328, 3),
     (69, 9, 68, 7),
     (301, 134, 299, 7),
     (71523, 20763, 71521, 11),
     (111028891713715270858633, 2169430279732, 111028891713715270858632, 3),
     (239, 14, 238, 11),
     (631, 3, 630, 5),
     (223, 3, 222, 7),
     (1184777, 1337, 1184776, 5),
     (284551513249666376365123, 275754422668509854114502, 284551513249666376365119, 5),
     (23, 61, 6, 3),
     (1728651, 4232391, 1728641, 5),
     (5439, 2319, 5437, 7),
     (523890102151522916311113076301980070234414163719, 3637867751654793328228610486390601899590, 523890102151522916311113076301980070234414163718, 3),
     (5, 1, 4, 3),
     (306251, 139, 306250, 3)]
  for block in [:4] do
    for (r, s, w, prime) in cases do
      let arms := if block % 2 == 0 then [false, true] else [true, false]
      for interval in arms do
        let mode := if interval then
          mkApp (mkConst ``PrimeCert.Pocklington3CertMode.interval) (mkRawNatLit w)
        else mkApp2 (mkConst ``PrimeCert.Pocklington3CertMode.prime) (mkRawNatLit prime)
          (mkConst (if prime == 3 then ``Nat.prime_three else if prime == 5 then ``Nat.prime_five else if prime == 7 then ``Nat.prime_seven else ``Nat.prime_eleven))
        let lhs := mkApp3 (mkConst ``PrimeCert.Pocklington3CertMode.calculate)
          mode (mkRawNatLit r) (mkRawNatLit s)
        let mkProof (b : Bool) :=
          let rhs := mkConst (if b then ``Bool.true else ``Bool.false)
          let type := mkApp3 (mkConst ``Eq [.succ .zero]) (mkConst ``Bool) lhs rhs
          mkApp (mkLambda `h .default type (mkBVar 0))
            (mkApp2 (mkConst ``Eq.refl [.succ .zero]) (mkConst ``Bool) rhs)
        let bad ← IO.mkRef (Kernel.check env {} (mkProof false))
        if (← bad.get).isOk then throwError "accepted wrong result"
        for i in [:64] do
          let input ← IO.mkRef (env, mkProof true)
          let (env, term) ← input.get
          let start ← IO.monoNanosNow
          let result ← IO.mkRef (Kernel.check env {} term)
          let result ← result.get
          let stop ← IO.monoNanosNow
          let _ ← ofExceptKernelException result
          file.putStrLn s!"{block},{r},{interval},{i},{stop-start}"
          file.flush

-- Retain fresh kernel checks under CPU affinity.

ReplacementTest.lean

/-
Copyright (c) 2025 Kenny Lau, Bhavik Mehta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau, Bhavik Mehta
-/

module

import PrimeCert

/-! # Example primality certificates

Demonstrates `pock3` and `prime_cert%` on primes up to 100+ digits, including the Ed25519
base point order and the Goldilocks prime `2^448 - 2^224 - 1`.

Helpful links:
* https://www.alpertron.com.ar/ECM.HTM (integer factorisation calculator using elliptic curves)
-/

set_option linter.style.longLine false

example : Nat.Prime 16290860017 := prime_cert%
  [small {3; 29},
   pock3 (339392917, 2, interval 17328, 2 ^ 2 * 3 ^ 4 * 29),
   pock3 (16290860017, 5, 0, 2 ^ 4 * 3 * 339392917)]

-- randomly generated 60-digit prime
example : Nat.Prime 236684654874665389773181956283167565443541280517430278333971 := prime_cert%
  [small {2; 3; 7; 11; 29; 31},
  pock3 (73471, 3, interval 68, 2 * 31),
  pock3 (32560621, 2, interval 299, 2 ^ 2 * 3 * 29),
  pock3 (3586530508831189, 2, interval 71521, 2 ^ 2 * 73471),
  pock3 (236684654874665389773181956283167565443541280517430278333971, 2, interval 111028891713715270858632, 2 * 32560621 * 3586530508831189)]

-- randomly generated 100-digit prime
set_option maxRecDepth 4000 in
example : Nat.Prime
    33706834100337092016588185336355794213783999136111596309066868786749483370039300586702754215489223467 := prime_cert%
  [small {5; 11},
   pock3 (1809751, 6, interval 238, 2 * 5 ^ 3),
   pock3 (1983088950781, 2, 0, 2 ^ 2 * 1809751),
   pock3 (47118193470556561, 7, 0, 2 ^ 4 * 1983088950781),
   pock3 (88792633576685840281427, 2, 0, 2 * 47118193470556561),
   pock3 (3933488715053265001346321205182867326957, 2, 0, 2 ^ 2 * 88792633576685840281427),
   pock3 (120470424957394687948621467206018925349715512075395521, 3, 0, 2 ^ 6 * 3933488715053265001346321205182867326957),
   pock3 (7333936561985354484046645851447308970826407201647529829078664035434709924691, 2, 0, 2 * 120470424957394687948621467206018925349715512075395521),
   pock3 (33706834100337092016588185336355794213783999136111596309066868786749483370039300586702754215489223467, 2, 0, 2 * 7333936561985354484046645851447308970826407201647529829078664035434709924691)]

set_option maxRecDepth 1000 in
example : Nat.Prime (2 ^ 255 - 19) := prime_cert%
  [small {3; 5; 7; 43},
   pock3 (1923133, 2, interval 630, 2 ^ 2 * 3 * 43),
   pock3 (430751, 17, interval 222, 2 * 5 ^ 3),
   pock3 (31757755568855353, 5, interval 1184776, 2 ^ 3 * 430751),
   pock3 (74058212732561358302231226437062788676166966415465897661863160754340907, 2, interval 284551513249666376365119, 2 * 3 * 1923133 * 31757755568855353),
   pock3 (57896044618658097711785492504343953926634992332820282019728792003956564819949, 2, 0, 2 ^ 2 * 74058212732561358302231226437062788676166966415465897661863160754340907)]

set_option exponentiation.threshold 448 in
example : Nat.Prime (2 ^ 448 - 2 ^ 224 - 1) := prime_cert%
  [small {3; 5; 7; 29; 67; 271; 641},
   pock3 (411743, 5, interval 6, 2 * 29),
   pock3 (1469495262398780123809, 17, interval 1728641, 2 ^ 5 * 411743),
   pock3 (97859369123353, 5, interval 5437, 2 ^ 3 * 67 * 271),
   pock3 (167773885276849215533569, 17, 0, 2 ^ 9 * 97859369123353),
   pock3 (726838724295606890549323807888004534353641360687318060281490199180612328166730772686396383698676545930088884461843637361053498018365439, 7, interval 523890102151522916311113076301980070234414163718, 2 * 641 * 1469495262398780123809 * 167773885276849215533569)]

-- 1178-digit prime 3 * 2 ^ 3912 + 1 (Proth form), certified with pock3
set_option maxRecDepth 2048 in
set_option exponentiation.threshold 3912 in
example : Nat.Prime (3 * 2 ^ 3912 + 1) := prime_cert%
  [small {3},
   pock3 (127780414391497973212171930170926986757577048484820926201064729783485263494817422495127775983679039078116803697168137524940219819335799478153348592755198599590903607242050230924443865709697486743641039970666450337071378658828331722728467720393963808366917988956767802913905167890490075236068196363700359481304279948916896583006686025357237170212018946813663108217900835975808683160984117514866915965161953626338070145596982334808959718966160701183250747572515090867613655044807172211728519357721287835503689517292364425608325467094686443862517374850243698013720305871319056887431952190952721719757200172695537054790570648290887720009455171821568413052107356003828041937567129362866696549587422369864562815134637684140271767482353107080370450890024342225936273158281477009232714640818424893445193089479459814572594522258577931514012256573162006292678354475638319009668319255772179069845291474717503333030909793536116894869761453687330048252587304656806182949368202671739705463406846852567720022377005763291104588535681445561286808586673846016527511475331939430139687698419185010117348285933672139833826832898565919546377321517928825162277951756632134321102813522053716838646284289, 11, 0, 2 ^ 3912 * 3)]

example : Nat.Prime 3999999999999999791 := prime_cert%
  [small {3; 5; 23; 211},
   pock3 (239851, 3, 0, 2 * 3 ^ 2 * 5 ^ 2),
   pock3 (399999999999999979, 2, 0, 2 * 3 ^ 3 * 23 * 211 * 239851),
   pock3 (3999999999999999791, 11, 0, 2 * 5 * 399999999999999979)]

example : Nat.Prime 3999999999999999691 := prime_cert%
  [small {3; 5; 11; 29; 41; 389},
   pock3 (18913, 7, interval 4, 2 ^ 5 * 3),
   pock3 (37379684141669, 2, 0, 2 ^ 2 * 11 * 389 * 18913),
   pock3 (3999999999999999691, 3, 0, 2 * 3 ^ 2 * 5 * 29 * 41 * 37379684141669)]

-- Ed25519 base point order ℓ = 2^252 + 27742317777372353535851937790883648493
set_option maxRecDepth 4000 in
example : Nat.Prime (2 ^ 252 + 27742317777372353535851937790883648493) := prime_cert%
  [small {3; 73},
   pock3 (3797, 2, 0, 2 ^ 2 * 73),
   pock3 (531581, 2, 0, 2 ^ 2 * 3797),
   pock3 (1257559732178653, 2, interval 306250, 2 ^ 2 * 531581),
   pock3 (4434155615661930479, 17, 0, 2 * 1257559732178653),
   pock3 (172054593956031949258510691, 2, 0, 2 * 4434155615661930479),
   pock3 (19757330305831588566944191468367130476339, 2, 0, 2 * 172054593956031949258510691),
   pock3 (276602624281642239937218680557139826668747, 2, 0, 2 * 19757330305831588566944191468367130476339),
   pock3 (7237005577332262213973186563042994240857116359379907606001950938285454250989, 2, 0, 2 ^ 2 * 276602624281642239937218680557139826668747)]

samples.csv

sieve-cases.json

[
  {
    "n": 37,
    "e": 2,
    "F": 4,
    "r": 1,
    "s": 1,
    "m": 1,
    "root": 2,
    "mode": ".lt",
    "bits": 6
  },
  {
    "n": 197,
    "e": 2,
    "F": 4,
    "r": 1,
    "s": 6,
    "m": 2,
    "root": 2,
    "mode": ".lt",
    "bits": 8
  },
  {
    "n": 9223372036904058881,
    "e": 20,
    "F": 1048576,
    "r": 47,
    "s": 4194304,
    "m": 4,
    "root": 3,
    "mode": ".lt",
    "bits": 64
  },
  {
    "n": 10633823966279326983230477372963684353,
    "e": 40,
    "F": 1099511627776,
    "r": 19,
    "s": 4398046511104,
    "m": 4,
    "root": 5,
    "mode": ".lt",
    "bits": 124
  },
  {
    "n": 14134776518227074636666380005943348126619871175013414145710152014563901441,
    "e": 80,
    "F": 1208925819614629174706176,
    "r": 7,
    "s": 4835703278458516698824704,
    "m": 4,
    "root": 13,
    "mode": ".lt",
    "bits": 244
  },
  {
    "n": 24973988402527937851052777838345330445988785141319769206873255677002973910558124960962448824508223685101169636846139109075628913189178501161287681,
    "e": 160,
    "F": 1461501637330902918203684832716283019655932542976,
    "r": 197,
    "s": 5846006549323611672814739330865132078623730171904,
    "m": 4,
    "root": 3,
    "mode": ".lt",
    "bits": 484
  }
]

sieve-find.py

import math,json
from pathlib import Path

def probable(n):
 d=n-1;s=0
 while d%2==0:d//=2;s+=1
 for a in (2,3,5,7,11,13,17,19,23,29,31,37):
  x=pow(a,d,n)
  if x in (1,n-1):continue
  for _ in range(s-1):
   x=x*x%n
   if x==n-1:break
  else:return False
 return True

def case(n,e):
 F=2**e;R=(n-1)//F;r=R%(2*F);s=R//(2*F)
 for m in range(1,65):
  if 2*s+m*m<(2*F+r)*m+2:break
 else:return None
 if any(n%(l*F+1)==0 for l in range(1,m)):return None
 d=r*r-8*s;w=math.isqrt(max(d,0))
 if s: mode='.lt' if d<0 else f'(.interval {w})' if w*w<d else None
 else:mode='.zero'
 if mode is None:return None
 for a in range(2,100):
  if pow(a,n-1,n)==1 and math.gcd(pow(a,(n-1)//2,n)-1,n)==1:break
 else:return None
 return dict(n=n,e=e,F=F,r=r,s=s,m=m,root=a,mode=mode,bits=n.bit_length())
cases=[case(37,2),case(197,2)]
for e in [20,40,80,160]:
 for k in range(1,10001,2):
  n=2**(3*e+3)+k*2**e+1
  if probable(n):
   c=case(n,e)
   if c:cases.append(c);break
print(json.dumps(cases,indent=2));Path('/tmp/pock3-investigation/cases.json').write_text(json.dumps(cases,indent=2))
s='module\nimport PrimeCert.Pocklington3\nset_option maxRecDepth 10000\n'
for c in cases:
 s+=f'\nexample : Nat.Prime {c["n"]} :=\n  PrimeCert.pocklington3_certK {c["n"]} {c["root"]} {c["m"]} {c["e"]} [] {c["mode"]} (by decide +kernel)\n'
 # Show m=1 fails for the same witnesses and F.
 if c['m']>1:s+=f'\nexample : PrimeCert.pocklington3_calculate {c["n"]} {c["e"]} {c["root"]} 1 [] {c["mode"]} = false := by decide +kernel\n'
Path('/tmp/pock3-investigation/Examples.lean').write_text(s)
p=Path('/home/kim/worktrees/PrimeCert/primecert-interval/PrimeCertTest/Investigation.lean');assert not p.exists();p.write_text(s)

sieve-HexExamples.lean

import HexPrimality.Cert

example : Hex.Nat.Prime 37 :=
  Hex.Nat.prime_of_checkPrimeAt
    (c := .pock3 37 1 1 0 [(2, 1, .small 2)]) (by decide +kernel)

example : Hex.Nat.checkPrime (.pock3 197 1 6 0 [(2, 1, .small 2)]) = false := by
  decide +kernel

sieve-investigation.md

Pocklington sieve-bound and pure-power investigation

Findings

PrimeCert at 7d015f6 accepts an empty odd-factor list in pocklington3_certK; only its pock3 syntax and #171 construction filter exclude this. The existing theorem proves 37 with F=4, root=2, m=1, negative discriminant. Hex's current checker accepts the corresponding literal (see HexExamples.lean).

The m=1 restriction is substantive in both search implementations. PrimeCert already proves the general theorem, while Hex Cert3.lean and checkPock3Arith specialize it to m=1. For n=197 and F=4, m=2 succeeds by additionally excluding the divisor 5. Both PrimeCert's m=1 arithmetic and Hex's existing checker reject that same factor product.

Examples.lean kernel-checks six direct proofs with F a power of two. Four constructed examples of 64, 124, 244 and 484 bits use m=4 and therefore just three extra divisibility tests. The same file checks that m=1 fails on those inputs. These are constructed examples, not standard cryptographic primes. cases.json records all parameters. find.py uses an untrusted probable-prime screen to find candidates; only the successful Lean builds establish primality.

Existing example certificates

Allowing m up to 64 in a diagnostic subset sweep finds smaller factor sets for five nodes in PrimeCertTest/PrimeListTest.lean (subsets.json). Two changes were validated in full kernel-checked ladders and timed:

Existing example	Change	Original m=1 ladder	Modified ladder	Reduction
Curve25519	Remove factor 3 from the 236-bit child, m=14	18.109 ms	15.812 ms	12.7%
Curve448	Remove factor 641 from the root, m=3	34.161 ms	27.925 ms	18.3%

These are full proof-term kernel checks of the existing example ladders on the interval PR, without #172's windowed powMod, not the different minimized ladder emitted by #171 and not Hex's optimized certificates. Every sample uses a fresh Kernel.check after imports, proof elaboration and term construction. Four adjacent alternating AB/BA blocks, eight samples per arm per block, pinned CPU 0 on the shared host; all completed samples retained. Each block favored the modified ladder. No native construction timings were collected. Failed build records are retained separately; these produced no timing samples.

Reproduce by copying Bench.lean to PrimeCertTest/InvestigationBench.lean at PrimeCert commit 7d015f68161bed3d07c3baea236f137ae39b531b, then running POCK3_SAMPLES=/tmp/pock3-samples.csv lake build PrimeCertTest.InvestigationBench. Examples.lean and HexExamples.lean can likewise be placed as temporary modules in the corresponding libraries and checked with lake build.

Recommendation

Fix the PrimeCert syntax to accept a lone power of two and remove the corresponding construction exclusion. Allow construction to use a bounded, explicitly budgeted m, sharing the existing minimum-m calculation and checking the added divisibility obligations. Include the cost of m-1 divisions in subset selection; fewer factors alone is not a replay-cost model.

For Hex, no power-of-two fix is needed. Supporting m>1 requires a Mathlib-free generalization of the theorem, checker and certificate representation, with existing m=1 literals retained. This should be a separate checker change.

Both construction routes currently call their factor provider before subset selection. Supporting m>1 alone can reduce recursive certificate and replay work, but will not automatically skip work already spent factoring. A further optimization is to try certificates from cheaply available partial factors before spending the remaining factor budget.

No PRs or tracked source files were changed during this investigation.

sieve-record.json

{
  "cpu": 0,
  "load_before": [
    3.39013671875,
    5.1552734375,
    5.43798828125
  ],
  "stdout": "\u26a0 [1308/1308] Built PrimeCertTest.InvestigationBench (4.0s)\nwarning: PrimeCertTest/InvestigationBench.lean:1:0: The current module only contains private declarations.\n\nConsider adding `@[expose] public section` at the beginning of the module, or selectively marking declarations as `public`.\n\nNote: This linter can be disabled with `set_option linter.privateModule false`\nBuild completed successfully (1308 jobs).\n",
  "stderr": "",
  "returncode": 0,
  "load_after": [
    3.439453125,
    5.1357421875,
    5.43017578125
  ]
}

sieve-samples.csv

sieve-subsets.json

[
  {
    "n": 339392917,
    "bits": 29,
    "old": [
      3,
      [
        [
          2,
          2
        ],
        [
          3,
          4
        ],
        [
          29,
          1
        ]
      ],
      9396,
      1,
      1
    ],
    "new": [
      2,
      [
        [
          2,
          2
        ],
        [
          3,
          4
        ]
      ],
      324,
      null,
      4
    ]
  },
  {
    "n": 32560621,
    "bits": 25,
    "old": [
      3,
      [
        [
          2,
          2
        ],
        [
          3,
          1
        ],
        [
          29,
          1
        ]
      ],
      348,
      1,
      1
    ],
    "new": [
      2,
      [
        [
          2,
          2
        ],
        [
          29,
          1
        ]
      ],
      116,
      null,
      6
    ]
  },
  {
    "n": 74058212732561358302231226437062788676166966415465897661863160754340907,
    "bits": 236,
    "old": [
      4,
      [
        [
          2,
          1
        ],
        [
          3,
          1
        ],
        [
          1923133,
          1
        ],
        [
          31757755568855353,
          1
        ]
      ],
      366446326442397009485694,
      1,
      1
    ],
    "new": [
      3,
      [
        [
          2,
          1
        ],
        [
          1923133,
          1
        ],
        [
          31757755568855353,
          1
        ]
      ],
      122148775480799003161898,
      null,
      14
    ]
  },
  {
    "n": 726838724295606890549323807888004534353641360687318060281490199180612328166730772686396383698676545930088884461843637361053498018365439,
    "bits": 448,
    "old": [
      4,
      [
        [
          2,
          1
        ],
        [
          641,
          1
        ],
        [
          1469495262398780123809,
          1
        ],
        [
          167773885276849215533569,
          1
        ]
      ],
      316068035706902087952262865703057298267656019522,
      1,
      1
    ],
    "new": [
      3,
      [
        [
          2,
          1
        ],
        [
          1469495262398780123809,
          1
        ],
        [
          167773885276849215533569,
          1
        ]
      ],
      493085859137132742515230679723958343631288642,
      null,
      3
    ]
  },
  {
    "n": 399999999999999979,
    "bits": 59,
    "old": [
      3,
      [
        [
          2,
          1
        ],
        [
          3,
          3
        ],
        [
          239851,
          1
        ]
      ],
      12951954,
      1,
      1
    ],
    "new": [
      2,
      [
        [
          2,
          1
        ],
        [
          239851,
          1
        ]
      ],
      479702,
      null,
      2
    ]
  }
]

SieveBench.lean

module
import Lean
import PrimeCert
meta import Lean
open Lean
set_option linter.style.longLine false
set_option maxRecDepth 10000
set_option exponentiation.threshold 448

theorem before255 : Nat.Prime (2 ^ 255 - 19) := prime_cert%
  [small {3; 5; 43},
   pock3 (1923133, 2, interval, 2 ^ 2 * 3 * 43),
   pock3 (430751, 17, interval, 2 * 5 ^ 3),
   pock3 (31757755568855353, 5, interval, 2 ^ 3 * 430751),
   pock3 (74058212732561358302231226437062788676166966415465897661863160754340907, 2, interval, 2 * 3 * 1923133 * 31757755568855353),
   pock3 (57896044618658097711785492504343953926634992332820282019728792003956564819949, 2, 0, 2 ^ 2 * 74058212732561358302231226437062788676166966415465897661863160754340907)]
theorem after255 : Nat.Prime (2 ^ 255 - 19) := prime_cert%
  [small {3; 5; 43},
   pock3 (1923133, 2, interval, 2 ^ 2 * 3 * 43),
   pock3 (430751, 17, interval, 2 * 5 ^ 3),
   pock3 (31757755568855353, 5, interval, 2 ^ 3 * 430751),
   pock3 (74058212732561358302231226437062788676166966415465897661863160754340907, 2, 14, interval, 2 * 1923133 * 31757755568855353),
   pock3 (57896044618658097711785492504343953926634992332820282019728792003956564819949, 2, 0, 2 ^ 2 * 74058212732561358302231226437062788676166966415465897661863160754340907)]

theorem before448 : Nat.Prime (2 ^ 448 - 2 ^ 224 - 1) := prime_cert%
  [small {29; 67; 271; 641},
   pock3 (411743, 5, interval, 2 * 29),
   pock3 (1469495262398780123809, 17, interval, 2 ^ 5 * 411743),
   pock3 (97859369123353, 5, interval, 2 ^ 3 * 67 * 271),
   pock3 (167773885276849215533569, 17, 0, 2 ^ 9 * 97859369123353),
   pock3 (726838724295606890549323807888004534353641360687318060281490199180612328166730772686396383698676545930088884461843637361053498018365439, 7, interval, 2 * 641 * 1469495262398780123809 * 167773885276849215533569)]
theorem after448 : Nat.Prime (2 ^ 448 - 2 ^ 224 - 1) := prime_cert%
  [small {29; 67; 271},
   pock3 (411743, 5, interval, 2 * 29),
   pock3 (1469495262398780123809, 17, interval, 2 ^ 5 * 411743),
   pock3 (97859369123353, 5, interval, 2 ^ 3 * 67 * 271),
   pock3 (167773885276849215533569, 17, 0, 2 ^ 9 * 97859369123353),
   pock3 (726838724295606890549323807888004534353641360687318060281490199180612328166730772686396383698676545930088884461843637361053498018365439, 7, 3, interval, 2 * 1469495262398780123809 * 167773885276849215533569)]

run_cmd do
  let ready ← IO.mkRef (← getEnv).toKernelEnv
  let env := Environment.ofKernelEnv (← ready.get)
  let some path ← IO.getEnv "POCK3_SAMPLES" | throwError "set POCK3_SAMPLES"
  let file ← IO.FS.Handle.mk path .write
  for block in [:4] do
    for (bits, before, after) in [(255, ``before255, ``after255), (448, ``before448, ``after448)] do
      for optimized in (if block % 2 == 0 then [false, true] else [true, false]) do
        let decl ← getConstInfo (if optimized then after else before)
        let some proof := decl.value? (allowOpaque := true) | throwError "missing proof"
        let term := mkApp (mkLambda `h .default decl.type (mkBVar 0)) proof
        for i in [:8] do
          let input ← IO.mkRef (env, term)
          let (env, term) ← input.get
          let start ← IO.monoNanosNow
          let result ← IO.mkRef (Kernel.check env {} term)
          let result ← result.get
          let stop ← IO.monoNanosNow
          let _ ← ofExceptKernelException result
          file.putStrLn s!"{block},{bits},{optimized},{i},{stop-start}"
          file.flush

SieveExamples.lean

module
import PrimeCert.Pocklington3
set_option maxRecDepth 10000

example : Nat.Prime 37 :=
  PrimeCert.pocklington3_certK 37 2 1 2 [] .lt (by decide +kernel)

example : Nat.Prime 197 :=
  PrimeCert.pocklington3_certK 197 2 2 2 [] .lt (by decide +kernel)

example : PrimeCert.pocklington3_calculate 197 2 2 1 [] .lt = false := by decide +kernel

example : Nat.Prime 9223372036904058881 :=
  PrimeCert.pocklington3_certK 9223372036904058881 3 4 20 [] .lt (by decide +kernel)

example : PrimeCert.pocklington3_calculate 9223372036904058881 20 3 1 [] .lt = false := by decide +kernel

example : Nat.Prime 10633823966279326983230477372963684353 :=
  PrimeCert.pocklington3_certK 10633823966279326983230477372963684353 5 4 40 [] .lt (by decide +kernel)

example : PrimeCert.pocklington3_calculate 10633823966279326983230477372963684353 40 5 1 [] .lt = false := by decide +kernel

example : Nat.Prime 14134776518227074636666380005943348126619871175013414145710152014563901441 :=
  PrimeCert.pocklington3_certK 14134776518227074636666380005943348126619871175013414145710152014563901441 13 4 80 [] .lt (by decide +kernel)

example : PrimeCert.pocklington3_calculate 14134776518227074636666380005943348126619871175013414145710152014563901441 80 13 1 [] .lt = false := by decide +kernel

example : Nat.Prime 24973988402527937851052777838345330445988785141319769206873255677002973910558124960962448824508223685101169636846139109075628913189178501161287681 :=
  PrimeCert.pocklington3_certK 24973988402527937851052777838345330445988785141319769206873255677002973910558124960962448824508223685101169636846139109075628913189178501161287681 3 4 160 [] .lt (by decide +kernel)

example : PrimeCert.pocklington3_calculate 24973988402527937851052777838345330445988785141319769206873255677002973910558124960962448824508223685101169636846139109075628913189178501161287681 160 3 1 [] .lt = false := by decide +kernel

unaffined-samples.csv