✓
Passing This code compiles and runs correctly.
Code
// CHALLENGE 800_010 — "deadbolt": a two-vault counting desk under a
// two-lock ordering protocol.
//
// Three lifecycles interleave every round:
// *Vault free! <-> held! seized in canonical id order,
// released LIFO — never out of order,
// never left held.
// *Guard none -> one -> two the depth witness. It cannot stand
// down at <two!> and cannot pair at
// <none!> — LIFO is the only path the
// types admit.
// *Attest open! the notary, borrowed (never consumed)
// through every round, sealed at close.
//
// Custody moves by recursion: every tor CONSUMES the obligations
// (<!free>, <!none>) at its params and hands them to the next call —
// the loop-carry vehicle this language offers. The base arm owns
// teardown: closing balances read, both vaults and the guard retired
// inside the session. Every arm discharges: | short releases both
// vaults in LIFO order just like | moved does.
//
// Two frontiers stand adjacent (observed here, unpinned):
// - record-field obligations die across any call boundary, so the
// { g, lo, hi } bundle tors this protocol wants are unwriteable —
// the |> chains here carry the same bindings instead;
// - a producing if can only yield a record it constructs literally
// (`.{ }` repack), so each decision level is its own tor — every
// if below sits at a subflow's top level, never nested.
import std/io
import app/lib/vault
import app/lib/order
tor amt-for { i: i64 } -> i64
amt-for -> @mod(i * 53 + 17, 120)
tor session-end { moved: i64, shorts: i64, fa: i64, fb: i64 } -> { moved: i64, shorts: i64, fa: i64, fb: i64 }
session-end -> { moved, shorts, fa, fb }
// One ordered acquisition + transfer + LIFO release, dir a->b,
// canonical seize order a first.
tor ab-a { i: i64, n: i64, g: *app/lib/vault:Guard<!none>, va: *app/lib/vault:Vault<!free>, vb: *app/lib/vault:Vault<!free>, a: *app/lib/vault:Attest<open>, moved: i64, shorts: i64, amt: i64 } -> { moved: i64, shorts: i64, fa: i64, fb: i64 }
ab-a = app/lib/order:post(g): g1
|> app/lib/order:seize(v: va): lo
|> app/lib/order:seize(v: vb): hi
|> app/lib/order:pair-up(g: g1): g2
|> app/lib/vault:witness(a)
|> app/lib/vault:shift(src: lo, dst: hi, amt)
| moved m |> std/io:print.ln(" moved {{ m:d }}")
|> app/lib/order:yield-inner(g: g2): g3
|> app/lib/order:hand-back(v: hi): hf
|> app/lib/order:stand-down(g: g3): g4
|> app/lib/order:hand-back(v: lo): lf
|> round(i: i + 1, n, g: g4, va: lf, vb: hf, a, moved: moved + 1, shorts): rec -> { rec.moved, rec.shorts, rec.fa, rec.fb }
| short |> std/io:print.ln(" move {{ amt:d }} SHORT — insufficient")
|> app/lib/order:yield-inner(g: g2): g3
|> app/lib/order:hand-back(v: hi): hf
|> app/lib/order:stand-down(g: g3): g4
|> app/lib/order:hand-back(v: lo): lf
|> round(i: i + 1, n, g: g4, va: lf, vb: hf, a, moved, shorts: shorts + 1): rec -> { rec.moved, rec.shorts, rec.fa, rec.fb }
// Same transfer, canonical order b first (b carries the lower id).
tor ab-b { i: i64, n: i64, g: *app/lib/vault:Guard<!none>, va: *app/lib/vault:Vault<!free>, vb: *app/lib/vault:Vault<!free>, a: *app/lib/vault:Attest<open>, moved: i64, shorts: i64, amt: i64 } -> { moved: i64, shorts: i64, fa: i64, fb: i64 }
ab-b = app/lib/order:post(g): g1
|> app/lib/order:seize(v: vb): lo
|> app/lib/order:seize(v: va): hi
|> app/lib/order:pair-up(g: g1): g2
|> app/lib/vault:witness(a)
|> app/lib/vault:shift(src: hi, dst: lo, amt)
| moved m |> std/io:print.ln(" moved {{ m:d }}")
|> app/lib/order:yield-inner(g: g2): g3
|> app/lib/order:hand-back(v: hi): hf
|> app/lib/order:stand-down(g: g3): g4
|> app/lib/order:hand-back(v: lo): lf
|> round(i: i + 1, n, g: g4, va: hf, vb: lf, a, moved: moved + 1, shorts): rec -> { rec.moved, rec.shorts, rec.fa, rec.fb }
| short |> std/io:print.ln(" move {{ amt:d }} SHORT — insufficient")
|> app/lib/order:yield-inner(g: g2): g3
|> app/lib/order:hand-back(v: hi): hf
|> app/lib/order:stand-down(g: g3): g4
|> app/lib/order:hand-back(v: lo): lf
|> round(i: i + 1, n, g: g4, va: hf, vb: lf, a, moved, shorts: shorts + 1): rec -> { rec.moved, rec.shorts, rec.fa, rec.fb }
// Direction b->a, canonical seize order a first.
tor ba-a { i: i64, n: i64, g: *app/lib/vault:Guard<!none>, va: *app/lib/vault:Vault<!free>, vb: *app/lib/vault:Vault<!free>, a: *app/lib/vault:Attest<open>, moved: i64, shorts: i64, amt: i64 } -> { moved: i64, shorts: i64, fa: i64, fb: i64 }
ba-a = app/lib/order:post(g): g1
|> app/lib/order:seize(v: va): lo
|> app/lib/order:seize(v: vb): hi
|> app/lib/order:pair-up(g: g1): g2
|> app/lib/vault:witness(a)
|> app/lib/vault:shift(src: hi, dst: lo, amt)
| moved m |> std/io:print.ln(" moved {{ m:d }}")
|> app/lib/order:yield-inner(g: g2): g3
|> app/lib/order:hand-back(v: hi): hf
|> app/lib/order:stand-down(g: g3): g4
|> app/lib/order:hand-back(v: lo): lf
|> round(i: i + 1, n, g: g4, va: lf, vb: hf, a, moved: moved + 1, shorts): rec -> { rec.moved, rec.shorts, rec.fa, rec.fb }
| short |> std/io:print.ln(" move {{ amt:d }} SHORT — insufficient")
|> app/lib/order:yield-inner(g: g2): g3
|> app/lib/order:hand-back(v: hi): hf
|> app/lib/order:stand-down(g: g3): g4
|> app/lib/order:hand-back(v: lo): lf
|> round(i: i + 1, n, g: g4, va: lf, vb: hf, a, moved, shorts: shorts + 1): rec -> { rec.moved, rec.shorts, rec.fa, rec.fb }
// Direction b->a, canonical seize order b first.
tor ba-b { i: i64, n: i64, g: *app/lib/vault:Guard<!none>, va: *app/lib/vault:Vault<!free>, vb: *app/lib/vault:Vault<!free>, a: *app/lib/vault:Attest<open>, moved: i64, shorts: i64, amt: i64 } -> { moved: i64, shorts: i64, fa: i64, fb: i64 }
ba-b = app/lib/order:post(g): g1
|> app/lib/order:seize(v: vb): lo
|> app/lib/order:seize(v: va): hi
|> app/lib/order:pair-up(g: g1): g2
|> app/lib/vault:witness(a)
|> app/lib/vault:shift(src: lo, dst: hi, amt)
| moved m |> std/io:print.ln(" moved {{ m:d }}")
|> app/lib/order:yield-inner(g: g2): g3
|> app/lib/order:hand-back(v: hi): hf
|> app/lib/order:stand-down(g: g3): g4
|> app/lib/order:hand-back(v: lo): lf
|> round(i: i + 1, n, g: g4, va: hf, vb: lf, a, moved: moved + 1, shorts): rec -> { rec.moved, rec.shorts, rec.fa, rec.fb }
| short |> std/io:print.ln(" move {{ amt:d }} SHORT — insufficient")
|> app/lib/order:yield-inner(g: g2): g3
|> app/lib/order:hand-back(v: hi): hf
|> app/lib/order:stand-down(g: g3): g4
|> app/lib/order:hand-back(v: lo): lf
|> round(i: i + 1, n, g: g4, va: hf, vb: lf, a, moved, shorts: shorts + 1): rec -> { rec.moved, rec.shorts, rec.fa, rec.fb }
// The order decision for direction a->b: peek both ids, seize the
// lower first.
tor dir-ab { i: i64, n: i64, g: *app/lib/vault:Guard<!none>, va: *app/lib/vault:Vault<!free>, vb: *app/lib/vault:Vault<!free>, a: *app/lib/vault:Attest<open>, moved: i64, shorts: i64 } -> { moved: i64, shorts: i64, fa: i64, fb: i64 }
dir-ab = amt-for(i): amt
|> app/lib/vault:id-of(v: va): ida
|> app/lib/vault:id-of(v: vb): idb
|> std/io:print.ln("round {{ i:d }}: move {{ amt:d }} vault {{ ida:d }} -> vault {{ idb:d }}")
|> if(ida < idb)
| then |> std/io:print.ln(" seize {{ ida:d }} then {{ idb:d }}")
|> ab-a(i, n, g, va, vb, a, moved, shorts, amt): rec -> { rec.moved, rec.shorts, rec.fa, rec.fb }
| else |> std/io:print.ln(" seize {{ idb:d }} then {{ ida:d }}")
|> ab-b(i, n, g, va, vb, a, moved, shorts, amt): rec -> { rec.moved, rec.shorts, rec.fa, rec.fb }
// The order decision for direction b->a.
tor dir-ba { i: i64, n: i64, g: *app/lib/vault:Guard<!none>, va: *app/lib/vault:Vault<!free>, vb: *app/lib/vault:Vault<!free>, a: *app/lib/vault:Attest<open>, moved: i64, shorts: i64 } -> { moved: i64, shorts: i64, fa: i64, fb: i64 }
dir-ba = amt-for(i): amt
|> app/lib/vault:id-of(v: va): ida
|> app/lib/vault:id-of(v: vb): idb
|> std/io:print.ln("round {{ i:d }}: move {{ amt:d }} vault {{ idb:d }} -> vault {{ ida:d }}")
|> if(ida < idb)
| then |> std/io:print.ln(" seize {{ ida:d }} then {{ idb:d }}")
|> ba-a(i, n, g, va, vb, a, moved, shorts, amt): rec -> { rec.moved, rec.shorts, rec.fa, rec.fb }
| else |> std/io:print.ln(" seize {{ idb:d }} then {{ ida:d }}")
|> ba-b(i, n, g, va, vb, a, moved, shorts, amt): rec -> { rec.moved, rec.shorts, rec.fa, rec.fb }
// Direction alternates by parity.
tor dispatch { i: i64, n: i64, g: *app/lib/vault:Guard<!none>, va: *app/lib/vault:Vault<!free>, vb: *app/lib/vault:Vault<!free>, a: *app/lib/vault:Attest<open>, moved: i64, shorts: i64 } -> { moved: i64, shorts: i64, fa: i64, fb: i64 }
dispatch = if(@mod(i, 2) == 0)
| then |> dir-ab(i, n, g, va, vb, a, moved, shorts): rec -> { rec.moved, rec.shorts, rec.fa, rec.fb }
| else |> dir-ba(i, n, g, va, vb, a, moved, shorts): rec -> { rec.moved, rec.shorts, rec.fa, rec.fb }
// The desk's session: recurse the rounds; at the base the desk
// itself retires the vaults and the guard — the session owns the
// whole lifecycle.
tor round { i: i64, n: i64, g: *app/lib/vault:Guard<!none>, va: *app/lib/vault:Vault<!free>, vb: *app/lib/vault:Vault<!free>, a: *app/lib/vault:Attest<open>, moved: i64, shorts: i64 } -> { moved: i64, shorts: i64, fa: i64, fb: i64 }
round = if(i == n)
| then |> app/lib/vault:peek-bal(v: va): fa
|> app/lib/vault:peek-bal(v: vb): fb
|> app/lib/vault:retire-vault(v: va)
|> app/lib/vault:retire-vault(v: vb)
|> app/lib/vault:retire-guard(g)
|> session-end(moved, shorts, fa, fb): rec -> { rec.moved, rec.shorts, rec.fa, rec.fb }
| else |> dispatch(i, n, g, va, vb, a, moved, shorts): rec -> { rec.moved, rec.shorts, rec.fa, rec.fb }
// ── the run ──────────────────────────────────────────────────────
// vault b carries the LOWER id (1) — every round's canonical seize
// order is vault 1 first, whichever direction money moves.
app/lib/vault:mint-vault(id: 2, bal: 300): va
|> app/lib/vault:mint-vault(id: 1, bal: 80): vb
|> app/lib/vault:mint-guard(): g
|> app/lib/vault:mint-attest(): att
|> std/io:print.ln("desk open: vault 2 bal 300, vault 1 bal 80")
|> round(i: 0, n: 8, g, va, vb, a: att, moved: 0, shorts: 0): res
|> app/lib/vault:seal-attest(a: att): attested
|> std/io:print.ln("desk closed: vault 2 bal {{ res.fa:d }}, vault 1 bal {{ res.fb:d }}")
|> std/io:print.ln("moved {{ res.moved:d }}, short {{ res.shorts:d }}, attested {{ attested:d }}")
Supporting Files
// The ordering protocol — pure Koru, no proc anywhere in the file.
//
// Each tor consumes one phantom state off a vault.kz resource and
// issues the next. The resources are minted and discharged in
// vault.kz; the entire middle of every lifecycle is retagged here,
// across the module seam.
//
// Guard: none! --post--> one! --pair-up--> two!
// none! <--stand-down-- one! <--yield-inner-- two!
//
// Vault: free! --seize--> held! --hand-back--> free!
//
// LIFO is the only path the types admit: stand-down will not accept
// a guard at <two!>, so hi must leave before lo's <free!> can exist.
// These are primitives only — the { g, lo, hi } bundle tors this
// protocol wants are unwriteable today (record-field obligations
// die across call boundaries — see README "Frontiers"); input.k
// chains them inline.
import app/lib/vault
pub tor seize { v: *app/lib/vault:Vault<!free> } -> *app/lib/vault:Vault<held!>
seize -> v
pub tor hand-back { v: *app/lib/vault:Vault<!held> } -> *app/lib/vault:Vault<free!>
hand-back -> v
pub tor post { g: *app/lib/vault:Guard<!none> } -> *app/lib/vault:Guard<one!>
post -> g
pub tor pair-up { g: *app/lib/vault:Guard<!one> } -> *app/lib/vault:Guard<two!>
pair-up -> g
pub tor yield-inner { g: *app/lib/vault:Guard<!two> } -> *app/lib/vault:Guard<one!>
yield-inner -> g
pub tor stand-down { g: *app/lib/vault:Guard<!one> } -> *app/lib/vault:Guard<none!>
stand-down -> g
// CHALLENGE 800_010 — "deadbolt": the host side of the vault desk.
//
// Every tor here is a LEAF: mint, borrow-inspect, one mutating
// primitive (shift), one counter (witness), and the dischargers.
// No lifecycle rule lives in this file — the whole protocol
// (seize order, pair depth, LIFO release) is pure Koru in
// lib/order.k. A proc body the compiler cannot see never touches
// a phantom; it only allocates, mutates, and frees.
const std = @import("std");
const Vault = struct { id: i64, bal: i64 };
const Guard = struct { depth: i64 };
const Attest = struct { count: i64 };
~pub tor mint-vault { id: i64, bal: i64 } -> *Vault<free!>
~proc mint-vault|zig {
const v = std.heap.page_allocator.create(Vault) catch unreachable;
v.* = .{ .id = id, .bal = bal };
return v;
}
~pub tor mint-guard {} -> *Guard<none!>
~proc mint-guard|zig {
const g = std.heap.page_allocator.create(Guard) catch unreachable;
g.* = .{ .depth = 0 };
return g;
}
~pub tor mint-attest {} -> *Attest<open!>
~proc mint-attest|zig {
const a = std.heap.page_allocator.create(Attest) catch unreachable;
a.* = .{ .count = 0 };
return a;
}
// Peek the id while the vault is still <free> — the ordering rule
// reads the id BEFORE it is allowed to seize anything.
~pub tor id-of { v: *Vault<free> } -> i64
~proc id-of|zig {
return v.id;
}
// Peek the balance of a HELD vault — the desk can only count a
// vault's money while the desk holds it.
~pub tor bal-of { v: *Vault<held> } -> i64
~proc bal-of|zig {
return v.bal;
}
// The closing read — a <free> vault can still be counted, just not
// moved from.
~pub tor peek-bal { v: *Vault<free> } -> i64
~proc peek-bal|zig {
return v.bal;
}
// The one mutating primitive. Both vaults must be HELD — a borrow
// on <held>, no consume. Resolves | moved amt when the source can
// cover, | short when it cannot. Cleanup after either arm is the
// caller's problem — and the caller's type.
~pub tor shift { src: *Vault<held>, dst: *Vault<held>, amt: i64 }
| moved i64
| short
~proc shift|zig {
if (src.bal >= amt) {
src.bal -= amt;
dst.bal += amt;
return .{ .moved = amt };
}
return .{ .short = .{} };
}
// The notary borrow — ticks once per transfer, never consumes.
~pub tor witness { a: *Attest<open> }
~proc witness|zig {
a.count += 1;
}
// The dischargers — the ONLY ways these resources may leave the
// world. A vault leaves <free>, a guard leaves <none>, an attest
// leaves <open>. Anything else is a refusal, not a convention.
~pub tor retire-vault { v: *Vault<!free> }
~proc retire-vault|zig {
std.heap.page_allocator.destroy(v);
}
~pub tor retire-guard { g: *Guard<!none> }
~proc retire-guard|zig {
std.heap.page_allocator.destroy(g);
}
~pub tor seal-attest { a: *Attest<!open> } -> i64
~proc seal-attest|zig {
const n = a.count;
std.heap.page_allocator.destroy(a);
return n;
}
Actual
desk open: vault 2 bal 300, vault 1 bal 80
round 0: move 17 vault 2 -> vault 1
seize 1 then 2
moved 17
round 1: move 70 vault 1 -> vault 2
seize 1 then 2
moved 70
round 2: move 3 vault 2 -> vault 1
seize 1 then 2
moved 3
round 3: move 56 vault 1 -> vault 2
seize 1 then 2
move 56 SHORT — insufficient
round 4: move 109 vault 2 -> vault 1
seize 1 then 2
moved 109
round 5: move 42 vault 1 -> vault 2
seize 1 then 2
moved 42
round 6: move 95 vault 2 -> vault 1
seize 1 then 2
moved 95
round 7: move 28 vault 1 -> vault 2
seize 1 then 2
moved 28
desk closed: vault 2 bal 216, vault 1 bal 164
moved 7, short 1, attested 8
Expected output
desk open: vault 2 bal 300, vault 1 bal 80
round 0: move 17 vault 2 -> vault 1
seize 1 then 2
moved 17
round 1: move 70 vault 1 -> vault 2
seize 1 then 2
moved 70
round 2: move 3 vault 2 -> vault 1
seize 1 then 2
moved 3
round 3: move 56 vault 1 -> vault 2
seize 1 then 2
move 56 SHORT — insufficient
round 4: move 109 vault 2 -> vault 1
seize 1 then 2
moved 109
round 5: move 42 vault 1 -> vault 2
seize 1 then 2
moved 42
round 6: move 95 vault 2 -> vault 1
seize 1 then 2
moved 95
round 7: move 28 vault 1 -> vault 2
seize 1 then 2
moved 28
desk closed: vault 2 bal 216, vault 1 bal 164
moved 7, short 1, attested 8
Flows
subflow ~ab-a click a branch to expand · @labels scroll to their anchor
post (g)
subflow ~ab-b click a branch to expand · @labels scroll to their anchor
post (g)
subflow ~ba-a click a branch to expand · @labels scroll to their anchor
post (g)
subflow ~ba-b click a branch to expand · @labels scroll to their anchor
post (g)
subflow ~dir-ab click a branch to expand · @labels scroll to their anchor
amt-for (i)
subflow ~dir-ba click a branch to expand · @labels scroll to their anchor
amt-for (i)
subflow ~dispatch click a branch to expand · @labels scroll to their anchor
if (@mod(i, 2) == 0)
subflow ~round click a branch to expand · @labels scroll to their anchor
if (i == n)
flow ~mint-vault click a branch to expand · @labels scroll to their anchor
mint-vault (id: 2, bal: 300)
Test Configuration
MUST_RUN