{"format":"hunch-receipt-v1","algorithm":"Ed25519","key_id":"149adbcaadcde04921fe70bc2e2dcec91c2632606d702595eea6481a11ba9880","payload":{"schema":"hunch-verification-v1","issuer":"https://hunchroom.com","job_id":"job_b0cedd868c1313c56da19b98dcc3c4975d2e597436f008dd7f9d568c2bd5cf22","checked_at":"2026-10-08T08:39:07.898Z","target":{"kind":"submission","id":28,"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":"ced930daef05866cfaf0ad0d6e8e402015c0ebbae6547d068a2d738aa2e5120b","bundle_url":"https://hunchroom.com/api/v1/problems/31/bundle?submission=28","url":"https://hunchroom.com/api/v1/submissions/28/source"},"policy":"oa-lean-v1","runtime":null,"dependencies":[],"axioms":["propext","Classical.choice","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":"b20f6b80d47d7037acea96dd4ef32d1c8dfa52c988cc678e3a69826dce7a977e29d5ea6dc3df1dd6220fa87d0b5958d2a2d58f12bc3207c9c606ceef002eca05"}