{"challengeId":"proof-golf","entry":"verifier.mjs","sha256":"75f953709a20adb1d990275ff042b2ece8401e8539429d85eb36233daaf03601","scoreDirection":"minimize","scoreLabel":"proof units","seedPolicy":{"mode":"fixed","testCount":1},"source":"// Frozen verifier for proof-golf. This is a tiny, deterministic proof kernel\n// for boolean identities over variables a/b/c. A candidate submits pure strings;\n// the verifier parses and checks them on every assignment.\n\nconst REQUIRED = {\n  deMorganAnd: ['not(and(a,b))', 'or(not(a),not(b))'],\n  deMorganOr: ['not(or(a,b))', 'and(not(a),not(b))'],\n  xorSelf: ['xor(a,a)', 'and(a,not(a))'],\n  xorComm: ['xor(a,b)', 'xor(b,a)'],\n  assocOr: ['or(or(a,b),c)', 'or(a,or(b,c))'],\n  distribAndOr: ['and(a,or(b,c))', 'or(and(a,b),and(a,c))'],\n};\nconst MAX_EXPR = 240;\n\nfunction gate(name, pass, detail) {\n  return { name, pass, detail };\n}\n\nfunction bad(name, detail) {\n  return { ok: false, score: null, gates: [gate(name, false, detail)], behavior: {}, logs: [] };\n}\n\nfunction strip(s) {\n  return s.replace(/\\s+/g, '');\n}\n\nfunction splitTop(expr, sep) {\n  let depth = 0;\n  for (let i = 0; i <= expr.length - sep.length; i++) {\n    const ch = expr[i];\n    if (ch === '(') depth++;\n    else if (ch === ')') depth--;\n    else if (depth === 0 && expr.slice(i, i + sep.length) === sep) return [expr.slice(0, i), expr.slice(i + sep.length)];\n  }\n  return null;\n}\n\nfunction splitArgs(s) {\n  let depth = 0;\n  for (let i = 0; i < s.length; i++) {\n    const ch = s[i];\n    if (ch === '(') depth++;\n    else if (ch === ')') depth--;\n    else if (ch === ',' && depth === 0) return [s.slice(0, i), s.slice(i + 1)];\n  }\n  return null;\n}\n\nfunction parseTerm(s) {\n  if (s === 'a' || s === 'b' || s === 'c') return { type: 'var', name: s };\n  const m = /^([a-z]+)\\((.*)\\)$/.exec(s);\n  if (!m) throw new Error(`could not parse term \"${s}\"`);\n  const op = m[1];\n  const body = m[2];\n  if (op === 'not') return { type: 'not', x: parseTerm(body) };\n  if (op === 'and' || op === 'or' || op === 'xor' || op === 'eq') {\n    const args = splitArgs(body);\n    if (!args) throw new Error(`${op} expects two arguments`);\n    return { type: op, a: parseTerm(args[0]), b: parseTerm(args[1]) };\n  }\n  throw new Error(`unknown operator \"${op}\"`);\n}\n\nfunction parseTheorem(expr) {\n  const clean = strip(expr);\n  if (!clean || clean.length > MAX_EXPR) throw new Error(`expression must be 1..${MAX_EXPR} normalized chars`);\n  const parts = splitTop(clean, '==');\n  if (!parts) throw new Error('theorem must contain a top-level ==');\n  return { left: parseTerm(parts[0]), right: parseTerm(parts[1]), size: clean.length };\n}\n\nfunction evalTerm(t, env) {\n  switch (t.type) {\n    case 'var':\n      return env[t.name];\n    case 'not':\n      return !evalTerm(t.x, env);\n    case 'and':\n      return evalTerm(t.a, env) && evalTerm(t.b, env);\n    case 'or':\n      return evalTerm(t.a, env) || evalTerm(t.b, env);\n    case 'xor':\n      return evalTerm(t.a, env) !== evalTerm(t.b, env);\n    case 'eq':\n      return evalTerm(t.a, env) === evalTerm(t.b, env);\n  }\n}\n\nexport function verify(ctx) {\n  const sol = ctx.solution;\n  const lemmas = sol && typeof sol === 'object' ? sol.lemmas : undefined;\n  if (!lemmas || typeof lemmas !== 'object' || Array.isArray(lemmas)) {\n    return bad('structure', 'expected { lemmas: { [name]: theoremExpression } }');\n  }\n\n  const gates = [];\n  let proofUnits = 0;\n  for (const [name, expected] of Object.entries(REQUIRED)) {\n    const expr = lemmas[name];\n    if (typeof expr !== 'string') return bad('structure', `missing theorem expression for ${name}`);\n    let theorem;\n    let expectedTheorem;\n    try {\n      theorem = parseTheorem(expr);\n      expectedTheorem = { left: parseTerm(expected[0]), right: parseTerm(expected[1]) };\n    } catch (e) {\n      return bad('parse', `${name}: ${e.message}`);\n    }\n    proofUnits += theorem.size;\n    let fail = '';\n    for (let mask = 0; mask < 8; mask++) {\n      const env = { a: !!(mask & 1), b: !!(mask & 2), c: !!(mask & 4) };\n      const l = evalTerm(theorem.left, env);\n      const r = evalTerm(theorem.right, env);\n      const el = evalTerm(expectedTheorem.left, env);\n      const er = evalTerm(expectedTheorem.right, env);\n      if (l !== el) {\n        fail = `left side is not the frozen ${name} left side at a=${Number(env.a)} b=${Number(env.b)} c=${Number(env.c)}`;\n        break;\n      }\n      if (r !== er) {\n        fail = `right side is not the frozen ${name} right side at a=${Number(env.a)} b=${Number(env.b)} c=${Number(env.c)}`;\n        break;\n      }\n      if (l !== r) {\n        fail = `counterexample a=${Number(env.a)} b=${Number(env.b)} c=${Number(env.c)}`;\n        break;\n      }\n    }\n    gates.push(gate(name, !fail, fail || 'identity holds on all 8 assignments'));\n  }\n\n  const ok = gates.every((g) => g.pass);\n  return {\n    ok,\n    score: ok ? proofUnits : null,\n    gates,\n    behavior: { proofUnits, lemmas: Object.keys(REQUIRED).length },\n    logs: [`proofUnits=${proofUnits} lemmas=${Object.keys(REQUIRED).length}`],\n  };\n}\n"}