{"format":"hunch-receipt-v1","algorithm":"Ed25519","key_id":"149adbcaadcde04921fe70bc2e2dcec91c2632606d702595eea6481a11ba9880","payload":{"schema":"hunch-verification-v1","issuer":"https://hunchroom.com","job_id":"job_2e995482c6b71db96b13fa2489230f07f15caade1781a69e5ddd018742b433e3","checked_at":"2026-10-08T06:44:46.974Z","target":{"kind":"submission","id":14,"problem_id":30,"statement_hash":"628148448355c1412fae271dced53a7a4b49e9b683daeed6e046f9397beb04e6","module_hash":null},"challenge":{"statement":"(fun (source target : List (Sum Nat (Sum Nat Nat)) → List Nat)\n     (cost keeps : List (Sum Nat (Sum Nat Nat)) → Nat) =>\n ∀ script : List (Sum Nat (Sum Nat Nat)),\n cost script + 2 * keeps script = (source script).length + (target script).length)\n(fun script => script.filterMap (fun edit => match edit with\n | .inl x => some x | .inr (.inl x) => some x | .inr (.inr _) => none))\n(fun script => script.filterMap (fun edit => match edit with\n | .inl x => some x | .inr (.inl _) => none | .inr (.inr x) => some x))\n(fun script => script.foldr (fun edit n => match edit with | .inl _ => n | .inr _ => n + 1) 0)\n(fun script => script.foldr (fun edit n => match edit with | .inl _ => n + 1 | .inr _ => n) 0)","profile":"std","module_pins":[]},"source":{"sha256":"494e8d86b7f07618d7c0613986ce6609a4bd6ceced694451e85c50cf32881bae","bundle_url":"https://hunchroom.com/api/v1/problems/30/bundle?submission=14","url":"https://hunchroom.com/api/v1/submissions/14/source"},"policy":"oa-lean-v1","runtime":null,"dependencies":[],"axioms":["propext","Quot.sound"],"primary":{"implementation":"Lean kernel","execution":"isolated WebAssembly","status":"passed","legacy":true},"secondary":{"implementation":"Nanoda","status":"not_run"},"statement_meaning":"Requires independent review; legacy runtime artifact hashes were not recorded."},"signature":"71c54b22e5efeac9c990012b334d80510730b18cd457002be02febe162f05a1ca59d0c977fb8a4518e0c07847c4c6843c77324264caab53d47f5efc278b92c0b"}