{"format":"hunch-receipt-v1","algorithm":"Ed25519","key_id":"149adbcaadcde04921fe70bc2e2dcec91c2632606d702595eea6481a11ba9880","payload":{"schema":"hunch-verification-v1","issuer":"https://hunchroom.com","job_id":"job_8de66afcd605888a43f47df400f0fb94c57dc9ea917fc10eb71032fe47b059ba","checked_at":"2026-10-08T05:03:14.981Z","target":{"kind":"submission","id":6,"problem_id":21,"statement_hash":"5956bd42558b9be5fd135292544f65e24932e5aaea27e57b1e6060b98f0f9f0b","module_hash":null},"challenge":{"statement":"(fun (run : List (Bool × Bool) → Nat → Option Nat → Sum Nat (Nat × Option Nat)) =>\n(fun (active : List (Bool × Bool) → List (Bool × Bool)) =>\n(fun (lastClear : List (Bool × Bool) → Option Nat) =>\n(fun (firstStart : List (Bool × Bool) → Option Nat → Option Nat) =>\n(fun (summarize : List (Bool × Bool) → Nat → Option Nat → Sum Nat (Nat × Option Nat)) =>\n∀ actions position saved, run actions position saved = summarize actions position saved\n) (fun actions position saved =>\n(fun chunk =>\n(fun clear =>\n(fun start =>\n(fun finalSaved =>\nif chunk.length < actions.length then .inl (finalSaved.getD (position + chunk.length))\nelse .inr (position + chunk.length, finalSaved))\n((if clear.isSome then none else saved).or (start.map (position + ·))))\n(firstStart chunk clear)) (lastClear chunk)) (active actions))\n) (fun chunk clear =>\n(((chunk.zipIdx).drop (clear.map Nat.succ |>.getD 0)).find? (fun pair => !pair.1.1 && pair.1.2)).map Prod.snd)\n) (fun chunk =>\n((chunk.zipIdx.reverse).find? (fun pair => pair.1.1 && !pair.1.2)).map Prod.snd)\n) (fun actions => actions.takeWhile (fun action => !action.1 || !action.2))\n) (fun actions =>\nList.rec (fun position saved => .inr (position, saved))\n(fun action _ rest position saved =>\nif action.1 then\n  if action.2 then .inl (saved.getD position) else rest (position + 1) none\nelse\n  if action.2 then rest (position + 1) (some (saved.getD position))\n  else rest (position + 1) saved) actions)","profile":"core","module_pins":[]},"source":{"sha256":"e52dc21e7eeeb49d564f0a55570278c50403b731961b6caed9101682b32f62f6","bundle_url":"https://hunchroom.com/api/v1/problems/21/bundle?submission=6","url":"https://hunchroom.com/api/v1/submissions/6/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":"1402ac0a254c13aa27b96e147c420f516c71e0aebf96de53a0c172de13f50be522d73b187ec14fde22fa582abdd494f863875af5587f2a671e695f3a64bcc00d"}