{"format":"hunch-receipt-v1","algorithm":"Ed25519","key_id":"149adbcaadcde04921fe70bc2e2dcec91c2632606d702595eea6481a11ba9880","payload":{"schema":"hunch-verification-v1","issuer":"https://hunchroom.com","job_id":"job_5f992c37ab9102277c0c7a38e8f72bc0ec7af6016823511d53a5c73b193d6376","checked_at":"2026-10-08T06:01:02.356Z","target":{"kind":"submission","id":8,"problem_id":23,"statement_hash":"daa2cbedd59be36b26a221343083d9a3b05f9a48b0d88df275369df5e4524987","module_hash":null},"challenge":{"statement":"(fun (born : List Nat → Nat → List Nat) =>\n(fun (position : List Nat → Nat → Nat) =>\n(fun (insertAt : List Nat → Nat → Nat → List Nat) =>\n(fun (replay : List Nat → Nat → List Nat) =>\n∀ (order : List Nat) (n : Nat), order.Nodup →\n(∀ time < n, time ∈ order) → (∀ time ∈ order, time < n) →\n(∀ cut ≤ n, replay order cut = born order cut) ∧\n(∀ time < n, position order time ≤ (replay order time).length) ∧\nreplay order n = order\n) (fun order cut => Nat.rec []\n  (fun time state => insertAt state (position order time) time) cut)\n) (fun state pos value => state.take pos ++ value :: state.drop pos)\n) (fun order time => (born (order.takeWhile (fun x => x != time)) time).length)\n) (fun order cut => order.filter (fun time => time < cut))","profile":"core","module_pins":[]},"source":{"sha256":"660a68c788f18bb904771409fb89f378fcaf3d9d2159f85031549e26e30240a6","bundle_url":"https://hunchroom.com/api/v1/problems/23/bundle?submission=8","url":"https://hunchroom.com/api/v1/submissions/8/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":"825e40cd80dd4fecd97cdf5da00ccec864221c263f3059f3bffcf2cdf13b708753cb0e53d790009a22595908fc5959ebbbc8ea5b0018118f13ea2c23c3ba000b"}