{"format":"hunch-receipt-v1","algorithm":"Ed25519","key_id":"149adbcaadcde04921fe70bc2e2dcec91c2632606d702595eea6481a11ba9880","payload":{"schema":"hunch-verification-v1","issuer":"https://hunchroom.com","job_id":"job_a9d321fe52f4d0ec1f45db481554a9cb8921684a6b9a9f35aff671b210ce161a","checked_at":"2026-10-08T10:23:43.444Z","target":{"kind":"submission","id":31,"problem_id":42,"statement_hash":"71a28134bc109775da3760becb062ee8e394fecff3394802c45e6b224eafba39","module_hash":null},"challenge":{"statement":"∀ (Row : Type) (leftRank rightRank actor sequence : Row → Nat),\n(fun (keyBefore : Row → Row → Bool) =>\n(fun (literalScan : Row → List Row → Nat → Bool → Nat → Nat) =>\n(fun (stopPredicate : Row → Row → Bool) =>\n(fun (clearPredicate : Row → Row → Bool) =>\n(fun (startPredicate : Row → Row → Bool) =>\n(fun (firstStop : Row → List Row → Nat) =>\n(fun (lastClearBeforeStop : Row → List Row → Option Nat) =>\n(fun (firstStartAfterClear : Row → List Row → Option Nat) =>\n(fun (selectedDestination : Row → List Row → Nat → Nat) =>\n∀ (incoming : Row) (rows : List Row) (position : Nat), literalScan incoming rows position false position = selectedDestination incoming rows position\n) (fun incoming rows position => position + (firstStartAfterClear incoming rows).getD (firstStop incoming rows))\n) (fun incoming rows =>\n  ((((rows.take (firstStop incoming rows)).zipIdx).drop (((lastClearBeforeStop incoming rows).map Nat.succ).getD 0)).find? (fun pair => startPredicate incoming pair.1)).map Prod.snd)\n) (fun incoming rows => ((((rows.take (firstStop incoming rows)).zipIdx).reverse.find?\n    (fun pair => clearPredicate incoming pair.1)).map Prod.snd))\n) (fun incoming rows => (((rows.zipIdx).find? (fun pair => stopPredicate incoming pair.1)).map\n    Prod.snd).getD rows.length)\n) (fun incoming other => decide ((leftRank other) = (leftRank incoming) ∧\n    (rightRank other) < (rightRank incoming)))\n) (fun incoming other => decide ((leftRank other) = (leftRank incoming) ∧\n    (rightRank incoming) ≤ (rightRank other)))\n) (fun incoming other => decide ((leftRank other) < (leftRank incoming)) ||\n    (decide ((leftRank other) = (leftRank incoming) ∧\n      (rightRank other) = (rightRank incoming)) && keyBefore incoming other))\n) (fun incoming rows => List.foldr (fun other tail position scanning back =>\n  if (leftRank other) = (leftRank incoming) then\n        if (rightRank other) = (rightRank incoming) then\n          if keyBefore incoming other then\n            if scanning then back else position\n          else tail (position + 1) false back\n        else if (rightRank other) < (rightRank incoming) then\n          tail (position + 1) true\n            (if scanning then back else position)\n        else tail (position + 1) false back\n      else if (leftRank other) < (leftRank incoming) then\n        if scanning then back else position\n      else tail (position + 1) scanning back) (fun position scanning back => if scanning then back else position) rows)\n) (fun incoming other => decide (actor incoming < actor other ∨ (actor incoming = actor other ∧ sequence incoming < sequence other)))","profile":"core","module_pins":[]},"source":{"sha256":"55686db56bcbebd1540f2841f9bd56045853e660010dab7a50d08f4d9a7f64ac","bundle_url":"https://hunchroom.com/api/v1/problems/42/bundle?submission=31","url":"https://hunchroom.com/api/v1/submissions/31/source"},"policy":"oa-lean-v1","runtime":{"sha256":"0c3043007435d47e9e0d0436e8a34c86f3e0f2c8c1b6f2f95b554e4e040008b1","verifier_sha256":"4070d198757866bf4f1c03e821f5045749fbbcb72c7429a87b5be11418020091","url":"https://hunchroom.com/api/v1/verification/manifests/0c3043007435d47e9e0d0436e8a34c86f3e0f2c8c1b6f2f95b554e4e040008b1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","browser_lean_commit":"355dfe02680154b1449f09b9e83bff15cb53a1f4","mathlib_commit":"de3a9cf33016bbb6d15880d7680643f7ca2d25ba"},"dependencies":[],"axioms":["propext","Quot.sound"],"primary":{"implementation":"Lean kernel","execution":"isolated WebAssembly","stack_mib":null,"status":"passed","elapsed_ms":39189,"legacy":false},"secondary":{"implementation":"Nanoda","status":"error","diagnostic":"export file declares unpermitted axiom \"instDecidableAnd._proof_1\"","export_sha256":"c0651f37e93d1f75658551e66bb98a71266f48e82bfd02ec25a119b979596177","checker_sha256":"ab9650346052bcc6947332de49b6553eee9030ade4ba1ea596dfd4fa7e124ad4"},"statement_meaning":"Requires independent review; this receipt certifies formal checking only.","execution_limits":{"verification_timeout_seconds":1200,"bridge_timeout_seconds":1320,"browser_timeout_seconds":1440,"workflow_timeout_seconds":1500,"checker_lease_seconds":7200,"cli_wait_timeout_seconds":3600,"worker_cpu_seconds":300,"upload_timeout_seconds":1200,"api_request_timeout_seconds":300,"memory_initial_mib":3072,"cli_memory_initial_mib":2048,"memory_max_mib":4096,"cli_stack_mib":64,"cli_stack_max_mib":256,"hosted_stack_mib":64,"heartbeats":20000000,"recursion_depth":16384,"concurrent_platform_checks":8,"pending_checks_per_account":50,"pending_checks_platform":5000,"active_uploads":8,"account_upload_bytes_per_day":1073741824,"verification_requests_per_minute":10,"write_requests_per_minute":60}},"signature":"2bc0671fddd1cd610f36e82e8320f946dd5e5f9815752a2be02601746693d75a5398898247a7b19894d8b37f3fb1cbddcb9d6ac0c970a722f8047acf6fc5ec00"}