{"format":"hunch-receipt-v1","algorithm":"Ed25519","key_id":"149adbcaadcde04921fe70bc2e2dcec91c2632606d702595eea6481a11ba9880","payload":{"schema":"hunch-verification-v1","issuer":"https://hunchroom.com","job_id":"job_b4dabab46284d90898c858599c575c3234cf0e7257eceadc75c8b09430223b7b","checked_at":"2026-10-08T04:31:02.066Z","target":{"kind":"submission","id":4,"problem_id":16,"statement_hash":"665056b74ac2b6e5e2959f32a560c25196fc89e85394cf2032c3a868bb4e2884","module_hash":null},"challenge":{"statement":"(fun (indexOf : (Nat×Nat)→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option Nat) =>\n(fun (leftAfter : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option (Nat×Nat)→Except Nat Nat) =>\n(fun (rightBefore : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option (Nat×Nat)→Except Nat Nat) =>\n(fun (idBefore : (Nat×Nat)→(Nat×Nat)→Bool) =>\n(fun (scan : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))→Nat→Nat→Nat→Nat→Bool→Nat→Except Nat Nat) =>\n(fun (insert : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (apply : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (visible : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (generate : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(Nat×Nat)→(Sum (Nat×(Nat×Nat)×Nat) Nat)→Except Nat (Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))) =>\n(fun (replayOps : List (Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (replay : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (ids : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→List (Nat×Nat)) =>\n(fun (validExtension : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))→Prop) =>\n(fun (validHistory : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→Prop) =>\n(fun (reconstruct : List (Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>\n(fun (parentContext : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))→(List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))) =>\n∀ (history : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))) (finalState : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))),\nvalidHistory history→replay history = .ok finalState→∀ (event : ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))), event ∈ history→replay (parentContext history event) =\n.ok (reconstruct ((parentContext history event).map (fun e => e.2.2.2)) finalState)\n) (fun history event =>\nhistory.filter (fun previous => event.2.1.any (fun id => id == previous.1)))\n) (fun ops finalState =>\n(fun (born dead : List (Nat×Nat)) =>\n(finalState.filter (fun item => born.any (fun id => id == item.1.1))).map\n(fun item => (item.1, dead.any (fun id => id == item.1.1))))\n(ops.filterMap (fun op => match op with | .inl ins => some ins.1 | .inr _ => none))\n(ops.filterMap (fun op => match op with | .inl _ => none | .inr target => some target)))\n) (fun history =>\nList.rec (fun _ : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))) => True)\n(fun event _ rest pre => validExtension pre event ∧ rest (pre ++ [event])) history [])\n) (fun pre event =>\nevent.1 ∉ ids pre ∧\n(∀ id ∈ event.2.1, id ∈ ids pre) ∧\n(∀ previous ∈ pre, previous.1 ∈ event.2.1→∀ id ∈ previous.2.1, id ∈ event.2.1) ∧\n(∀ previous ∈ pre, previous.1.1 = event.1.1→previous.1.2 < event.1.2 ∧ previous.1 ∈ event.2.1) ∧\n∃ sourceState,\nreplay (pre.filter (fun previous => event.2.1.any (fun id => id == previous.1))) = .ok sourceState ∧\ngenerate sourceState event.1 event.2.2.1 = .ok event.2.2.2)\n) (fun history => history.map (fun event => event.1))\n) (fun history =>\nreplayOps (history.map (fun event => event.2.2.2)) [])\n) (fun ops start =>\nops.foldl (fun prior op => prior.bind (fun state => apply state op)) (.ok start))\n) (fun state fresh edit =>\nmatch edit with\n| .inl (pos, label, payload) => do\nif (visible state).length < pos then throw 4\n(fun (left : Option (Nat×Nat)) => do\nlet start ← leftAfter state left\nreturn .inl (fresh, label, payload, left, (state[start]?).map (fun x => x.1.1))) (if pos = 0 then none else ((visible state)[pos - 1]?).map (fun x => x.1.1))\n| .inr pos => match (visible state)[pos]? with\n| none => .error 4\n| some item => .ok (.inr item.1.1))\n) (fun state => state.filter (fun item => !item.2))\n) (fun state op =>\nmatch op with\n| .inl ins => insert state ins\n| .inr target =>\nif (indexOf target state).isSome then\n.ok (state.map fun item => if item.1.1 = target then (item.1, true) else item)\nelse .error 3)\n) (fun state ins => do\nif (indexOf ins.1 state).isSome then throw 1\nlet left ← leftAfter state ins.2.2.2.1\nlet right ← rightBefore state ins.2.2.2.2\nif right < left then throw 2\nlet dest ← scan state ins left right state.length left false left\nreturn state.take dest ++ [(ins, false)] ++ state.drop dest)\n) (fun state ins left right fuel =>\nNat.rec\n(fun i scanning back =>\nif right ≤ i then .ok (if scanning then back else i) else .error 5)\n(fun _ recur i scanning back => do\nif right ≤ i then return if scanning then back else i\nlet other ← match state[i]? with\n| none => .error 4\n| some item => .ok item\nif other.1.2.2.2.1 = ins.2.2.2.1 then\nif other.1.2.2.2.2 = ins.2.2.2.2 then\nif idBefore ins.1 other.1.1 then return if scanning then back else i\nelse recur (i + 1) false back\nelse\nlet otherRight ← rightBefore state other.1.2.2.2.2\nif otherRight < right then recur (i + 1) true (if scanning then back else i)\nelse recur (i + 1) false back\nelse\nlet otherLeft ← leftAfter state other.1.2.2.2.1\nif otherLeft < left then return if scanning then back else i\nelse recur (i + 1) scanning back)\nfuel)\n) (fun a b =>\na.1 < b.1 || (a.1 == b.1 && a.2 < b.2))\n) (fun state origin =>\nmatch origin with\n| none => .ok state.length\n| some id => match indexOf id state with\n| none => .error 0\n| some i => .ok i)\n) (fun state origin =>\nmatch origin with\n| none => .ok 0\n| some id => match indexOf id state with\n| none => .error 0\n| some i => .ok (i + 1))\n) (fun id state =>\nList.rec none (fun item _ tail => if item.1.1 = id then some 0 else tail.map Nat.succ) state)","profile":"core","module_pins":[]},"source":{"sha256":"d9809d0580a7d6894bfe27635cf37fbae80068853789f2a730e514f6e19b0a13","bundle_url":"https://hunchroom.com/api/v1/problems/16/bundle?submission=4","url":"https://hunchroom.com/api/v1/submissions/4/source"},"policy":"oa-lean-v1","runtime":null,"dependencies":[],"axioms":[],"primary":{"implementation":"Lean kernel","execution":"isolated WebAssembly","status":"failed","legacy":true},"secondary":{"implementation":"Nanoda","status":"not_run"},"statement_meaning":"Requires independent review; legacy runtime artifact hashes were not recorded."},"signature":"d84a97a7c5ee7e53941647b7589f54ff3b3b67839005fee53a4e832d737bcc0f85fc38cc6d6843f24ea2976991b96f52758d1453bb81349e42578a7e4cabae0f"}