{"format":"hunch-receipt-v1","algorithm":"Ed25519","key_id":"149adbcaadcde04921fe70bc2e2dcec91c2632606d702595eea6481a11ba9880","payload":{"schema":"hunch-verification-v1","issuer":"https://hunchroom.com","job_id":"job_96fa0435fa62927d2147aa9d76fa46f95a0bea76c5aa1708eba404a669d06e71","checked_at":"2026-10-08T09:22:18.325Z","target":{"kind":"submission","id":29,"problem_id":31,"statement_hash":"8a86b4d6476261560d43f6ea3df9394ba847eb65bf27eb0728f61c014858789d","module_hash":null},"challenge":{"statement":"(fun (cost : List (Sum (Option Nat) (Option Nat)) → Nat) =>\n(fun (apply : List (Sum (Option Nat) (Option Nat)) → List Nat → Option (List Nat)) =>\n(fun (best : List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat))) =>\n(fun (diff : Nat → List Nat → List Nat → List (Sum (Option Nat) (Option Nat))) =>\n∀ (xs ys : List Nat) (fuel : Nat), xs.length + ys.length ≤ fuel →\n apply (diff fuel xs ys) xs = some ys ∧\n ∀ script : List (Sum (Option Nat) (Option Nat)), apply script xs = some ys → cost (diff fuel xs ys) ≤ cost script\n) (fun fuel => Nat.rec (fun _ _ : List Nat => [])\n (fun _ recur xs ys => match xs, ys with\n | [], _ => ys.map (fun y => Sum.inr (some y))\n | _, [] => List.replicate xs.length (Sum.inr none)\n | x :: xt, y :: yt => if x = y then Sum.inl none :: recur xt yt\n   else best (Sum.inl (some y) :: recur xt yt)\n             (Sum.inr none :: recur xt ys)\n             (Sum.inr (some y) :: recur xs yt)) fuel)\n) (fun a b c => if cost a ≤ cost b ∧ cost a ≤ cost c then a else if cost b ≤ cost c then b else c)\n) (fun script => List.rec (fun xs : List Nat => some xs)\n (fun edit _ rest xs => match edit, xs with\n | .inl none, x :: xt => (rest xt).map (fun ys => x :: ys)\n | .inl (some y), _ :: xt => (rest xt).map (fun ys => y :: ys)\n | .inr none, _ :: xt => rest xt\n | .inr (some y), _ => (rest xs).map (fun ys => y :: ys)\n | _, [] => none) script)\n) (fun script => script.foldr (fun edit n => match edit with | .inl none => n | _ => n + 1) 0)","profile":"core","module_pins":[]},"source":{"sha256":"8d853266a9a713fe059b5fdab1ee34a619c63cd7f1bd63493053b2a12c380f70","bundle_url":"https://hunchroom.com/api/v1/problems/31/bundle?submission=29","url":"https://hunchroom.com/api/v1/submissions/29/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","Classical.choice","Quot.sound"],"primary":{"implementation":"Lean kernel","execution":"isolated Node WebAssembly","stack_mib":64,"status":"passed","elapsed_ms":27942,"legacy":false},"secondary":{"implementation":"Nanoda","status":"not_run"},"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":"d01621d83d1d2ebcb49b46d2c3fdec7955c037f9c085ac38f90e5b955ee2b42d8d7d2777a40ee74f5fdc7d0c5c4b82740fa42c2c223e24bdc061bd4fb87f690b"}