types.bend source
types.bend on the hub · documented module
import Base# Integer tower and the Solana account types.# Each integer has the U32 operations: inc, add, sub, mul, not, and, or, xor,# shl, shr, shln, shrn, cmp, is_eq, is_ne, is_lt, is_le, is_gt, is_ge,# is_zero, to_nat, from_nat, log2, div, mod, min, max, clamp, pow, is_even,# show, read. Unsigned shr is logical. Signed shr is arithmetic. div and mod# by zero follow U32 (div yields zero, mod yields the dividend). Signed div# truncates toward zero. Words wrap.def W.pred(n: Nat) -> Nat: match n: case 0n: 0n case 1n+p: pdef W.from_nat(+n: Nat, k: Nat) -> Word(n): match k: case 0n: Word.zero(n) case 1n+p: Word.inc(n, W.from_nat(n, p))def W.one(+n: Nat) -> Word(n): W.from_nat(n, 1n)def W.ten(+n: Nat) -> Word(n): W.from_nat(n, 10n)def W.is_zero(+n: Nat, a: Word(n)) -> Bool: Cmp.is_eq(Word.cmp(n, a, Word.zero(n)))def W.msb.go(p: Nat, b: Bool, t: Word(p)) -> Bool: match p: case 0n: b case 1n+q: match t: case WCon{b2, t2}: W.msb.go(q, b2, t2)def W.msb(n: Nat, w: Word(n)) -> Bool: match n: case 0n: False{} case 1n+p: match w: case WCon{b, t}: W.msb.go(p, b, t)def W.set_msb.go(p: Nat, b: Bool, t: Word(p), bit: Bool) -> Word(1n+p): match p: case 0n: WCon{bit, t} case 1n+q: match t: case WCon{b2, t2}: WCon{b, W.set_msb.go(q, b2, t2, bit)}def W.set_msb(n: Nat, w: Word(n), bit: Bool) -> Word(n): match n: case 0n: WNil{} case 1n+p: match w: case WCon{b, t}: W.set_msb.go(p, b, t, bit)def W.shln(+n: Nat, a: Word(n), k: Nat) -> Word(n): match k: case 0n: a case 1n+p: Word.shl(n, W.shln(n, a, p))def W.shrn(+n: Nat, a: Word(n), k: Nat) -> Word(n): match k: case 0n: a case 1n+p: Word.shr(n, W.shrn(n, a, p))def W.sshr(+n: Nat, +w: Word(n)) -> Word(n): W.set_msb(n, Word.shr(n, w), W.msb(n, w))def W.sshrn(+n: Nat, a: Word(n), k: Nat) -> Word(n): match k: case 0n: a case 1n+p: W.sshr(n, W.sshrn(n, a, p))def W.highbit(+n: Nat) -> Word(n): W.shln(n, W.one(n), W.pred(n))def W.divmod.fin( -p: Nat, +n: Nat, q: Word(p), +s: Word(n), +b: Word(n), g: Bool,) -> Word(1n+p) & Word(n): match g: case True{}: (WCon{True{}, q}, Word.sub(n, s, b)) case False{}: (WCon{False{}, q}, s)def W.divmod.shl( -p: Nat, +n: Nat, q: Word(p), +b: Word(n), ts: Bool & Word(n),) -> Word(1n+p) & Word(n): (t, s) = ts +s2 = {s : Word(n)} W.divmod.fin(p, n, q, s2, b, Bool.or(t, Cmp.is_ge(Word.cmp(n, s2, b))))def W.divmod.rec( -p: Nat, +n: Nat, a0: Bool, +b: Word(n), qr: Word(p) & Word(n),) -> Word(1n+p) & Word(n): (q, r) = qr W.divmod.shl(p, n, q, b, Word.shl.out(n, a0, r))def W.divmod(m: Nat, +n: Nat, a: Word(m), +b: Word(n)) -> Word(m) & Word(n): match m a: case 0n WNil{}: (WNil{}, Word.zero(n)) case 1n+p WCon{a0, hi}: W.divmod.rec(p, n, a0, b, W.divmod(p, n, hi, b))def W.quot(+n: Nat, qr: Word(n) & Word(n)) -> Word(n): (q, r) = qr qdef W.rem(+n: Nat, qr: Word(n) & Word(n)) -> Word(n): (q, r) = qr rdef W.div.if(+n: Nat, aw: Word(n), +b: Word(n), z: Bool) -> Word(n): match z: case True{}: Word.zero(n) case False{}: W.quot(n, W.divmod(n, n, aw, b))def W.div(+n: Nat, a: Word(n), +b: Word(n)) -> Word(n): W.div.if(n, a, b, W.is_zero(n, b))def W.mod.if(+n: Nat, aw: Word(n), +b: Word(n), z: Bool) -> Word(n): match z: case True{}: aw case False{}: W.rem(n, W.divmod(n, n, aw, b))def W.mod(+n: Nat, a: Word(n), +b: Word(n)) -> Word(n): W.mod.if(n, a, b, W.is_zero(n, b))def W.neg(+n: Nat, a: Word(n)) -> Word(n): Word.sub(n, Word.zero(n), a)def W.abs.if(+n: Nat, a: Word(n), neg: Bool) -> Word(n): match neg: case True{}: W.neg(n, a) case False{}: adef W.abs(+n: Nat, +a: Word(n)) -> Word(n): W.abs.if(n, a, W.msb(n, a))def W.sign_diff(+n: Nat, +a: Word(n), +b: Word(n)) -> Bool: Bool.xor(W.msb(n, a), W.msb(n, b))def W.apply_sign(+n: Nat, neg: Bool, mag: Word(n)) -> Word(n): match neg: case True{}: W.neg(n, mag) case False{}: magdef W.sdiv.if(+n: Nat, +a: Word(n), +b: Word(n), z: Bool) -> Word(n): match z: case True{}: Word.zero(n) case False{}: W.apply_sign(n, W.sign_diff(n, a, b), W.div(n, W.abs(n, a), W.abs(n, b)))def W.sdiv(+n: Nat, +a: Word(n), +b: Word(n)) -> Word(n): W.sdiv.if(n, a, b, W.is_zero(n, b))def W.smod.if(+n: Nat, +a: Word(n), +b: Word(n), z: Bool) -> Word(n): match z: case True{}: a case False{}: W.apply_sign(n, W.msb(n, a), W.mod(n, W.abs(n, a), W.abs(n, b)))def W.smod(+n: Nat, +a: Word(n), +b: Word(n)) -> Word(n): W.smod.if(n, a, b, W.is_zero(n, b))def W.scmp.fin(sa: Bool, sb: Bool, u: Cmp) -> Cmp: match sa sb: case False{} False{}: u case True{} True{}: u case True{} False{}: LT{} case False{} True{}: GT{}def W.scmp(+n: Nat, +a: Word(n), +b: Word(n)) -> Cmp: W.scmp.fin(W.msb(n, a), W.msb(n, b), Word.cmp(n, a, b))def W.log2.go(+k: Nat, +n: Nat, +v: Word(n), +d: Nat) -> Nat: match k: case 0n: d case 1n+p: W.log2.go( p, n, Word.shr(n, v), Nat.add( d, U32.to_nat(Bool.to_u32(Cmp.is_lt(Word.cmp(n, W.one(n), v)))), ), )def W.log2(+n: Nat, +v: Word(n)) -> Nat: W.log2.go(n, n, v, 0n)def W.pow(+n: Nat, +a: Word(n), k: Nat) -> Word(n): match k: case 0n: W.one(n) case 1n+p: Word.mul(n, a, W.pow(n, a, p))def W.digit(+n: Nat, x: U32) -> Word(n): W.from_nat(n, U32.to_nat(U32.sub(x, 48)))@unsafedef W.show.go(+f: Nat, +n: Nat, +v: Word(n), acc: String) -> String: match f: case 0n: acc case 1n+g: W.show.step(g, n, v, acc, W.is_zero(n, v))def W.show.step(+g: Nat, +n: Nat, +v: Word(n), acc: String, z: Bool) -> String: match z: case True{}: acc case False{}: W.show.go( g, n, W.div(n, v, W.ten(n)), SCon{ Chr{ U32.add(48, U32.from_nat(Word.to_nat(n, W.mod(n, v, W.ten(n))))), }, acc, }, )def W.show.if(+n: Nat, +digits: Nat, a: Word(n), z: Bool) -> String: match z: case True{}: SCon{Chr{48}, SNil{}} case False{}: W.show.go(digits, n, a, SNil{})def W.show(+n: Nat, +digits: Nat, +a: Word(n)) -> String: W.show.if(n, digits, a, W.is_zero(n, a))def W.sshow.if(+n: Nat, +digits: Nat, a: Word(n), neg: Bool) -> String: match neg: case True{}: SCon{Chr{45}, W.show(n, digits, W.abs(n, a))} case False{}: W.show(n, digits, a)def W.sshow(+n: Nat, +digits: Nat, +a: Word(n)) -> String: W.sshow.if(n, digits, a, W.msb(n, a))@unsafedef W.read.go(+n: Nat, s: String, +acc: Word(n)) -> Maybe<&2, Word(n)>: match s: case SNil{}: Some{acc} case SCon{Chr{x}, t}: +nxt = Word.add(n, Word.mul(n, acc, W.ten(n)), W.digit(n, x)) W.read.if(n, t, nxt, Cmp.is_eq(Word.cmp(n, W.div(n, nxt, W.ten(n)), acc)))def W.read.if(+n: Nat, t: String, nxt: Word(n), ok: Bool) -> Maybe<&2, Word(n)>: match ok: case True{}: W.read.go(n, t, nxt) case False{}: None{}def W.read(+n: Nat, s: String) -> Maybe<&2, Word(n)>: match s: case SNil{}: None{} case SCon{h, t}: W.read.go(n, SCon{h, t}, Word.zero(n))def W.sread.pos.if(+n: Nat, v: Word(n), hi: Bool) -> Maybe<&2, Word(n)>: match hi: case True{}: None{} case False{}: Some{v}def W.sread.pos(+n: Nat, m: Maybe<&2, Word(n)>) -> Maybe<&2, Word(n)>: match m: case None{}: None{} case Some{+v}: W.sread.pos.if(n, v, W.msb(n, v))def W.sread.neg.if(+n: Nat, v: Word(n), ok: Bool) -> Maybe<&2, Word(n)>: match ok: case True{}: Some{W.neg(n, v)} case False{}: None{}def W.sread.neg(+n: Nat, m: Maybe<&2, Word(n)>) -> Maybe<&2, Word(n)>: match m: case None{}: None{} case Some{+v}: W.sread.neg.if(n, v, Cmp.is_le(Word.cmp(n, v, W.highbit(n))))def W.sread.sign(+n: Nat, t: String, x: U32, minus: Bool) -> Maybe<&2, Word(n)>: match minus: case True{}: W.sread.neg(n, W.read(n, t)) case False{}: W.sread.pos(n, W.read(n, SCon{Chr{x}, t}))def W.sread(+n: Nat, s: String) -> Maybe<&2, Word(n)>: match s: case SNil{}: None{} case SCon{Chr{+x}, t}: W.sread.sign(n, t, x, U32.is_eq(x, 45))type u8 is Data: u8{data: Word(8n)}def u8.inc(a: u8) -> u8: match a: case u8{x}: u8{Word.inc(8n, x)}def u8.add(a: u8, b: u8) -> u8: match a b: case u8{x} u8{y}: u8{Word.add(8n, x, y)}def u8.sub(a: u8, b: u8) -> u8: match a b: case u8{x} u8{y}: u8{Word.sub(8n, x, y)}def u8.mul(a: u8, b: u8) -> u8: match a b: case u8{x} u8{y}: u8{Word.mul(8n, x, y)}def u8.not(a: u8) -> u8: match a: case u8{x}: u8{Word.not(8n, x)}def u8.and(a: u8, b: u8) -> u8: match a b: case u8{x} u8{y}: u8{Word.and(8n, x, y)}def u8.or(a: u8, b: u8) -> u8: match a b: case u8{x} u8{y}: u8{Word.or(8n, x, y)}def u8.xor(a: u8, b: u8) -> u8: match a b: case u8{x} u8{y}: u8{Word.xor(8n, x, y)}def u8.shl(a: u8) -> u8: match a: case u8{x}: u8{Word.shl(8n, x)}def u8.shr(a: u8) -> u8: match a: case u8{x}: u8{Word.shr(8n, x)}def u8.shrn(a: u8, k: Nat) -> u8: match a: case u8{x}: u8{W.shrn(8n, x, k)}def u8.cmp(a: u8, b: u8) -> Cmp: match a b: case u8{x} u8{y}: Word.cmp(8n, x, y)def u8.div(a: u8, +b: u8) -> u8: match a b: case u8{x} u8{+y}: u8{W.div(8n, x, y)}def u8.mod(a: u8, +b: u8) -> u8: match a b: case u8{x} u8{+y}: u8{W.mod(8n, x, y)}def u8.shln(a: u8, k: Nat) -> u8: match a: case u8{x}: u8{W.shln(8n, x, k)}def u8.is_eq(a: u8, b: u8) -> Bool: Cmp.is_eq(u8.cmp(a, b))def u8.is_ne(a: u8, b: u8) -> Bool: Bool.not(Cmp.is_eq(u8.cmp(a, b)))def u8.is_lt(a: u8, b: u8) -> Bool: Cmp.is_lt(u8.cmp(a, b))def u8.is_le(a: u8, b: u8) -> Bool: Cmp.is_le(u8.cmp(a, b))def u8.is_gt(a: u8, b: u8) -> Bool: Cmp.is_gt(u8.cmp(a, b))def u8.is_ge(a: u8, b: u8) -> Bool: Cmp.is_ge(u8.cmp(a, b))def u8.from_nat(k: Nat) -> u8: u8{W.from_nat(8n, k)}def u8.is_zero(a: u8) -> Bool: u8.is_eq(a, u8.from_nat(0n))def u8.to_nat(a: u8) -> Nat: match a: case u8{x}: Word.to_nat(8n, x)def u8.log2(+a: u8) -> Nat: match a: case u8{+x}: W.log2(8n, x)def u8.min(+a: u8, +b: u8) -> u8: Bool.pick(u8, u8.is_lt(a, b), a, b)def u8.max(+a: u8, +b: u8) -> u8: Bool.pick(u8, u8.is_lt(a, b), b, a)def u8.clamp(x: u8, lo: u8, hi: u8) -> u8: u8.min(u8.max(x, lo), hi)def u8.pow(+a: u8, k: Nat) -> u8: match a: case u8{+x}: u8{W.pow(8n, x, k)}def u8.is_even(a: u8) -> Bool: match a: case u8{+x}: W.is_zero(8n, Word.and(8n, x, W.one(8n)))def u8.show(+a: u8) -> String: match a: case u8{+x}: W.show(8n, 3n, x)def u8.read.wrap(m: Maybe<&2, Word(8n)>) -> Maybe<&2, u8>: match m: case None{}: None{} case Some{v}: Some{u8{v}}def u8.read(s: String) -> Maybe<&2, u8>: u8.read.wrap(W.read(8n, s))type u16 is Data: u16{data: Word(16n)}def u16.inc(a: u16) -> u16: match a: case u16{x}: u16{Word.inc(16n, x)}def u16.add(a: u16, b: u16) -> u16: match a b: case u16{x} u16{y}: u16{Word.add(16n, x, y)}def u16.sub(a: u16, b: u16) -> u16: match a b: case u16{x} u16{y}: u16{Word.sub(16n, x, y)}def u16.mul(a: u16, b: u16) -> u16: match a b: case u16{x} u16{y}: u16{Word.mul(16n, x, y)}def u16.not(a: u16) -> u16: match a: case u16{x}: u16{Word.not(16n, x)}def u16.and(a: u16, b: u16) -> u16: match a b: case u16{x} u16{y}: u16{Word.and(16n, x, y)}def u16.or(a: u16, b: u16) -> u16: match a b: case u16{x} u16{y}: u16{Word.or(16n, x, y)}def u16.xor(a: u16, b: u16) -> u16: match a b: case u16{x} u16{y}: u16{Word.xor(16n, x, y)}def u16.shl(a: u16) -> u16: match a: case u16{x}: u16{Word.shl(16n, x)}def u16.shr(a: u16) -> u16: match a: case u16{x}: u16{Word.shr(16n, x)}def u16.shrn(a: u16, k: Nat) -> u16: match a: case u16{x}: u16{W.shrn(16n, x, k)}def u16.cmp(a: u16, b: u16) -> Cmp: match a b: case u16{x} u16{y}: Word.cmp(16n, x, y)def u16.div(a: u16, +b: u16) -> u16: match a b: case u16{x} u16{+y}: u16{W.div(16n, x, y)}def u16.mod(a: u16, +b: u16) -> u16: match a b: case u16{x} u16{+y}: u16{W.mod(16n, x, y)}def u16.shln(a: u16, k: Nat) -> u16: match a: case u16{x}: u16{W.shln(16n, x, k)}def u16.is_eq(a: u16, b: u16) -> Bool: Cmp.is_eq(u16.cmp(a, b))def u16.is_ne(a: u16, b: u16) -> Bool: Bool.not(Cmp.is_eq(u16.cmp(a, b)))def u16.is_lt(a: u16, b: u16) -> Bool: Cmp.is_lt(u16.cmp(a, b))def u16.is_le(a: u16, b: u16) -> Bool: Cmp.is_le(u16.cmp(a, b))def u16.is_gt(a: u16, b: u16) -> Bool: Cmp.is_gt(u16.cmp(a, b))def u16.is_ge(a: u16, b: u16) -> Bool: Cmp.is_ge(u16.cmp(a, b))def u16.from_nat(k: Nat) -> u16: u16{W.from_nat(16n, k)}def u16.is_zero(a: u16) -> Bool: u16.is_eq(a, u16.from_nat(0n))def u16.to_nat(a: u16) -> Nat: match a: case u16{x}: Word.to_nat(16n, x)def u16.log2(+a: u16) -> Nat: match a: case u16{+x}: W.log2(16n, x)def u16.min(+a: u16, +b: u16) -> u16: Bool.pick(u16, u16.is_lt(a, b), a, b)def u16.max(+a: u16, +b: u16) -> u16: Bool.pick(u16, u16.is_lt(a, b), b, a)def u16.clamp(x: u16, lo: u16, hi: u16) -> u16: u16.min(u16.max(x, lo), hi)def u16.pow(+a: u16, k: Nat) -> u16: match a: case u16{+x}: u16{W.pow(16n, x, k)}def u16.is_even(a: u16) -> Bool: match a: case u16{+x}: W.is_zero(16n, Word.and(16n, x, W.one(16n)))def u16.show(+a: u16) -> String: match a: case u16{+x}: W.show(16n, 5n, x)def u16.read.wrap(m: Maybe<&2, Word(16n)>) -> Maybe<&2, u16>: match m: case None{}: None{} case Some{v}: Some{u16{v}}def u16.read(s: String) -> Maybe<&2, u16>: u16.read.wrap(W.read(16n, s))type u32 is Data: u32{data: Word(32n)}def u32.inc(a: u32) -> u32: match a: case u32{x}: u32{Word.inc(32n, x)}def u32.add(a: u32, b: u32) -> u32: match a b: case u32{x} u32{y}: u32{Word.add(32n, x, y)}def u32.sub(a: u32, b: u32) -> u32: match a b: case u32{x} u32{y}: u32{Word.sub(32n, x, y)}def u32.mul(a: u32, b: u32) -> u32: match a b: case u32{x} u32{y}: u32{Word.mul(32n, x, y)}def u32.not(a: u32) -> u32: match a: case u32{x}: u32{Word.not(32n, x)}def u32.and(a: u32, b: u32) -> u32: match a b: case u32{x} u32{y}: u32{Word.and(32n, x, y)}def u32.or(a: u32, b: u32) -> u32: match a b: case u32{x} u32{y}: u32{Word.or(32n, x, y)}def u32.xor(a: u32, b: u32) -> u32: match a b: case u32{x} u32{y}: u32{Word.xor(32n, x, y)}def u32.shl(a: u32) -> u32: match a: case u32{x}: u32{Word.shl(32n, x)}def u32.shr(a: u32) -> u32: match a: case u32{x}: u32{Word.shr(32n, x)}def u32.shrn(a: u32, k: Nat) -> u32: match a: case u32{x}: u32{W.shrn(32n, x, k)}def u32.cmp(a: u32, b: u32) -> Cmp: match a b: case u32{x} u32{y}: Word.cmp(32n, x, y)def u32.div(a: u32, +b: u32) -> u32: match a b: case u32{x} u32{+y}: u32{W.div(32n, x, y)}def u32.mod(a: u32, +b: u32) -> u32: match a b: case u32{x} u32{+y}: u32{W.mod(32n, x, y)}def u32.shln(a: u32, k: Nat) -> u32: match a: case u32{x}: u32{W.shln(32n, x, k)}def u32.is_eq(a: u32, b: u32) -> Bool: Cmp.is_eq(u32.cmp(a, b))def u32.is_ne(a: u32, b: u32) -> Bool: Bool.not(Cmp.is_eq(u32.cmp(a, b)))def u32.is_lt(a: u32, b: u32) -> Bool: Cmp.is_lt(u32.cmp(a, b))def u32.is_le(a: u32, b: u32) -> Bool: Cmp.is_le(u32.cmp(a, b))def u32.is_gt(a: u32, b: u32) -> Bool: Cmp.is_gt(u32.cmp(a, b))def u32.is_ge(a: u32, b: u32) -> Bool: Cmp.is_ge(u32.cmp(a, b))def u32.from_nat(k: Nat) -> u32: u32{W.from_nat(32n, k)}def u32.is_zero(a: u32) -> Bool: u32.is_eq(a, u32.from_nat(0n))def u32.to_nat(a: u32) -> Nat: match a: case u32{x}: Word.to_nat(32n, x)def u32.log2(+a: u32) -> Nat: match a: case u32{+x}: W.log2(32n, x)def u32.min(+a: u32, +b: u32) -> u32: Bool.pick(u32, u32.is_lt(a, b), a, b)def u32.max(+a: u32, +b: u32) -> u32: Bool.pick(u32, u32.is_lt(a, b), b, a)def u32.clamp(x: u32, lo: u32, hi: u32) -> u32: u32.min(u32.max(x, lo), hi)def u32.pow(+a: u32, k: Nat) -> u32: match a: case u32{+x}: u32{W.pow(32n, x, k)}def u32.is_even(a: u32) -> Bool: match a: case u32{+x}: W.is_zero(32n, Word.and(32n, x, W.one(32n)))def u32.show(+a: u32) -> String: match a: case u32{+x}: W.show(32n, 10n, x)def u32.read.wrap(m: Maybe<&2, Word(32n)>) -> Maybe<&2, u32>: match m: case None{}: None{} case Some{v}: Some{u32{v}}def u32.read(s: String) -> Maybe<&2, u32>: u32.read.wrap(W.read(32n, s))type u64 is Data: u64{data: Word(64n)}def u64.inc(a: u64) -> u64: match a: case u64{x}: u64{Word.inc(64n, x)}def u64.add(a: u64, b: u64) -> u64: match a b: case u64{x} u64{y}: u64{Word.add(64n, x, y)}def u64.sub(a: u64, b: u64) -> u64: match a b: case u64{x} u64{y}: u64{Word.sub(64n, x, y)}def u64.mul(a: u64, b: u64) -> u64: match a b: case u64{x} u64{y}: u64{Word.mul(64n, x, y)}def u64.not(a: u64) -> u64: match a: case u64{x}: u64{Word.not(64n, x)}def u64.and(a: u64, b: u64) -> u64: match a b: case u64{x} u64{y}: u64{Word.and(64n, x, y)}def u64.or(a: u64, b: u64) -> u64: match a b: case u64{x} u64{y}: u64{Word.or(64n, x, y)}def u64.xor(a: u64, b: u64) -> u64: match a b: case u64{x} u64{y}: u64{Word.xor(64n, x, y)}def u64.shl(a: u64) -> u64: match a: case u64{x}: u64{Word.shl(64n, x)}def u64.shr(a: u64) -> u64: match a: case u64{x}: u64{Word.shr(64n, x)}def u64.shrn(a: u64, k: Nat) -> u64: match a: case u64{x}: u64{W.shrn(64n, x, k)}def u64.cmp(a: u64, b: u64) -> Cmp: match a b: case u64{x} u64{y}: Word.cmp(64n, x, y)def u64.div(a: u64, +b: u64) -> u64: match a b: case u64{x} u64{+y}: u64{W.div(64n, x, y)}def u64.mod(a: u64, +b: u64) -> u64: match a b: case u64{x} u64{+y}: u64{W.mod(64n, x, y)}def u64.shln(a: u64, k: Nat) -> u64: match a: case u64{x}: u64{W.shln(64n, x, k)}def u64.is_eq(a: u64, b: u64) -> Bool: Cmp.is_eq(u64.cmp(a, b))def u64.is_ne(a: u64, b: u64) -> Bool: Bool.not(Cmp.is_eq(u64.cmp(a, b)))def u64.is_lt(a: u64, b: u64) -> Bool: Cmp.is_lt(u64.cmp(a, b))def u64.is_le(a: u64, b: u64) -> Bool: Cmp.is_le(u64.cmp(a, b))def u64.is_gt(a: u64, b: u64) -> Bool: Cmp.is_gt(u64.cmp(a, b))def u64.is_ge(a: u64, b: u64) -> Bool: Cmp.is_ge(u64.cmp(a, b))def u64.from_nat(k: Nat) -> u64: u64{W.from_nat(64n, k)}def u64.is_zero(a: u64) -> Bool: u64.is_eq(a, u64.from_nat(0n))def u64.to_nat(a: u64) -> Nat: match a: case u64{x}: Word.to_nat(64n, x)def u64.log2(+a: u64) -> Nat: match a: case u64{+x}: W.log2(64n, x)def u64.min(+a: u64, +b: u64) -> u64: Bool.pick(u64, u64.is_lt(a, b), a, b)def u64.max(+a: u64, +b: u64) -> u64: Bool.pick(u64, u64.is_lt(a, b), b, a)def u64.clamp(x: u64, lo: u64, hi: u64) -> u64: u64.min(u64.max(x, lo), hi)def u64.pow(+a: u64, k: Nat) -> u64: match a: case u64{+x}: u64{W.pow(64n, x, k)}def u64.is_even(a: u64) -> Bool: match a: case u64{+x}: W.is_zero(64n, Word.and(64n, x, W.one(64n)))def u64.show(+a: u64) -> String: match a: case u64{+x}: W.show(64n, 20n, x)def u64.read.wrap(m: Maybe<&2, Word(64n)>) -> Maybe<&2, u64>: match m: case None{}: None{} case Some{v}: Some{u64{v}}def u64.read(s: String) -> Maybe<&2, u64>: u64.read.wrap(W.read(64n, s))type u128 is Data: u128{data: Word(128n)}def u128.inc(a: u128) -> u128: match a: case u128{x}: u128{Word.inc(128n, x)}def u128.add(a: u128, b: u128) -> u128: match a b: case u128{x} u128{y}: u128{Word.add(128n, x, y)}def u128.sub(a: u128, b: u128) -> u128: match a b: case u128{x} u128{y}: u128{Word.sub(128n, x, y)}def u128.mul(a: u128, b: u128) -> u128: match a b: case u128{x} u128{y}: u128{Word.mul(128n, x, y)}def u128.not(a: u128) -> u128: match a: case u128{x}: u128{Word.not(128n, x)}def u128.and(a: u128, b: u128) -> u128: match a b: case u128{x} u128{y}: u128{Word.and(128n, x, y)}def u128.or(a: u128, b: u128) -> u128: match a b: case u128{x} u128{y}: u128{Word.or(128n, x, y)}def u128.xor(a: u128, b: u128) -> u128: match a b: case u128{x} u128{y}: u128{Word.xor(128n, x, y)}def u128.shl(a: u128) -> u128: match a: case u128{x}: u128{Word.shl(128n, x)}def u128.shr(a: u128) -> u128: match a: case u128{x}: u128{Word.shr(128n, x)}def u128.shrn(a: u128, k: Nat) -> u128: match a: case u128{x}: u128{W.shrn(128n, x, k)}def u128.cmp(a: u128, b: u128) -> Cmp: match a b: case u128{x} u128{y}: Word.cmp(128n, x, y)def u128.div(a: u128, +b: u128) -> u128: match a b: case u128{x} u128{+y}: u128{W.div(128n, x, y)}def u128.mod(a: u128, +b: u128) -> u128: match a b: case u128{x} u128{+y}: u128{W.mod(128n, x, y)}def u128.shln(a: u128, k: Nat) -> u128: match a: case u128{x}: u128{W.shln(128n, x, k)}def u128.is_eq(a: u128, b: u128) -> Bool: Cmp.is_eq(u128.cmp(a, b))def u128.is_ne(a: u128, b: u128) -> Bool: Bool.not(Cmp.is_eq(u128.cmp(a, b)))def u128.is_lt(a: u128, b: u128) -> Bool: Cmp.is_lt(u128.cmp(a, b))def u128.is_le(a: u128, b: u128) -> Bool: Cmp.is_le(u128.cmp(a, b))def u128.is_gt(a: u128, b: u128) -> Bool: Cmp.is_gt(u128.cmp(a, b))def u128.is_ge(a: u128, b: u128) -> Bool: Cmp.is_ge(u128.cmp(a, b))def u128.from_nat(k: Nat) -> u128: u128{W.from_nat(128n, k)}def u128.is_zero(a: u128) -> Bool: u128.is_eq(a, u128.from_nat(0n))def u128.to_nat(a: u128) -> Nat: match a: case u128{x}: Word.to_nat(128n, x)def u128.log2(+a: u128) -> Nat: match a: case u128{+x}: W.log2(128n, x)def u128.min(+a: u128, +b: u128) -> u128: Bool.pick(u128, u128.is_lt(a, b), a, b)def u128.max(+a: u128, +b: u128) -> u128: Bool.pick(u128, u128.is_lt(a, b), b, a)def u128.clamp(x: u128, lo: u128, hi: u128) -> u128: u128.min(u128.max(x, lo), hi)def u128.pow(+a: u128, k: Nat) -> u128: match a: case u128{+x}: u128{W.pow(128n, x, k)}def u128.is_even(a: u128) -> Bool: match a: case u128{+x}: W.is_zero(128n, Word.and(128n, x, W.one(128n)))def u128.show(+a: u128) -> String: match a: case u128{+x}: W.show(128n, 39n, x)def u128.read.wrap(m: Maybe<&2, Word(128n)>) -> Maybe<&2, u128>: match m: case None{}: None{} case Some{v}: Some{u128{v}}def u128.read(s: String) -> Maybe<&2, u128>: u128.read.wrap(W.read(128n, s))type i8 is Data: i8{data: Word(8n)}def i8.inc(a: i8) -> i8: match a: case i8{x}: i8{Word.inc(8n, x)}def i8.add(a: i8, b: i8) -> i8: match a b: case i8{x} i8{y}: i8{Word.add(8n, x, y)}def i8.sub(a: i8, b: i8) -> i8: match a b: case i8{x} i8{y}: i8{Word.sub(8n, x, y)}def i8.mul(a: i8, b: i8) -> i8: match a b: case i8{x} i8{y}: i8{Word.mul(8n, x, y)}def i8.not(a: i8) -> i8: match a: case i8{x}: i8{Word.not(8n, x)}def i8.and(a: i8, b: i8) -> i8: match a b: case i8{x} i8{y}: i8{Word.and(8n, x, y)}def i8.or(a: i8, b: i8) -> i8: match a b: case i8{x} i8{y}: i8{Word.or(8n, x, y)}def i8.xor(a: i8, b: i8) -> i8: match a b: case i8{x} i8{y}: i8{Word.xor(8n, x, y)}def i8.shl(a: i8) -> i8: match a: case i8{x}: i8{Word.shl(8n, x)}def i8.shr(+a: i8) -> i8: match a: case i8{+x}: i8{W.sshr(8n, x)}def i8.shrn(a: i8, k: Nat) -> i8: match a: case i8{x}: i8{W.sshrn(8n, x, k)}def i8.cmp(+a: i8, +b: i8) -> Cmp: match a b: case i8{+x} i8{+y}: W.scmp(8n, x, y)def i8.div(+a: i8, +b: i8) -> i8: match a b: case i8{+x} i8{+y}: i8{W.sdiv(8n, x, y)}def i8.mod(+a: i8, +b: i8) -> i8: match a b: case i8{+x} i8{+y}: i8{W.smod(8n, x, y)}def i8.shln(a: i8, k: Nat) -> i8: match a: case i8{x}: i8{W.shln(8n, x, k)}def i8.is_eq(a: i8, b: i8) -> Bool: Cmp.is_eq(i8.cmp(a, b))def i8.is_ne(a: i8, b: i8) -> Bool: Bool.not(Cmp.is_eq(i8.cmp(a, b)))def i8.is_lt(a: i8, b: i8) -> Bool: Cmp.is_lt(i8.cmp(a, b))def i8.is_le(a: i8, b: i8) -> Bool: Cmp.is_le(i8.cmp(a, b))def i8.is_gt(a: i8, b: i8) -> Bool: Cmp.is_gt(i8.cmp(a, b))def i8.is_ge(a: i8, b: i8) -> Bool: Cmp.is_ge(i8.cmp(a, b))def i8.from_nat(k: Nat) -> i8: i8{W.from_nat(8n, k)}def i8.is_zero(a: i8) -> Bool: i8.is_eq(a, i8.from_nat(0n))def i8.to_nat(a: i8) -> Nat: match a: case i8{x}: Word.to_nat(8n, x)def i8.log2(+a: i8) -> Nat: match a: case i8{+x}: W.log2(8n, x)def i8.min(+a: i8, +b: i8) -> i8: Bool.pick(i8, i8.is_lt(a, b), a, b)def i8.max(+a: i8, +b: i8) -> i8: Bool.pick(i8, i8.is_lt(a, b), b, a)def i8.clamp(x: i8, lo: i8, hi: i8) -> i8: i8.min(i8.max(x, lo), hi)def i8.pow(+a: i8, k: Nat) -> i8: match a: case i8{+x}: i8{W.pow(8n, x, k)}def i8.is_even(a: i8) -> Bool: match a: case i8{+x}: W.is_zero(8n, Word.and(8n, x, W.one(8n)))def i8.show(+a: i8) -> String: match a: case i8{+x}: W.sshow(8n, 3n, x)def i8.read.wrap(m: Maybe<&2, Word(8n)>) -> Maybe<&2, i8>: match m: case None{}: None{} case Some{v}: Some{i8{v}}def i8.read(s: String) -> Maybe<&2, i8>: i8.read.wrap(W.sread(8n, s))type i16 is Data: i16{data: Word(16n)}def i16.inc(a: i16) -> i16: match a: case i16{x}: i16{Word.inc(16n, x)}def i16.add(a: i16, b: i16) -> i16: match a b: case i16{x} i16{y}: i16{Word.add(16n, x, y)}def i16.sub(a: i16, b: i16) -> i16: match a b: case i16{x} i16{y}: i16{Word.sub(16n, x, y)}def i16.mul(a: i16, b: i16) -> i16: match a b: case i16{x} i16{y}: i16{Word.mul(16n, x, y)}def i16.not(a: i16) -> i16: match a: case i16{x}: i16{Word.not(16n, x)}def i16.and(a: i16, b: i16) -> i16: match a b: case i16{x} i16{y}: i16{Word.and(16n, x, y)}def i16.or(a: i16, b: i16) -> i16: match a b: case i16{x} i16{y}: i16{Word.or(16n, x, y)}def i16.xor(a: i16, b: i16) -> i16: match a b: case i16{x} i16{y}: i16{Word.xor(16n, x, y)}def i16.shl(a: i16) -> i16: match a: case i16{x}: i16{Word.shl(16n, x)}def i16.shr(+a: i16) -> i16: match a: case i16{+x}: i16{W.sshr(16n, x)}def i16.shrn(a: i16, k: Nat) -> i16: match a: case i16{x}: i16{W.sshrn(16n, x, k)}def i16.cmp(+a: i16, +b: i16) -> Cmp: match a b: case i16{+x} i16{+y}: W.scmp(16n, x, y)def i16.div(+a: i16, +b: i16) -> i16: match a b: case i16{+x} i16{+y}: i16{W.sdiv(16n, x, y)}def i16.mod(+a: i16, +b: i16) -> i16: match a b: case i16{+x} i16{+y}: i16{W.smod(16n, x, y)}def i16.shln(a: i16, k: Nat) -> i16: match a: case i16{x}: i16{W.shln(16n, x, k)}def i16.is_eq(a: i16, b: i16) -> Bool: Cmp.is_eq(i16.cmp(a, b))def i16.is_ne(a: i16, b: i16) -> Bool: Bool.not(Cmp.is_eq(i16.cmp(a, b)))def i16.is_lt(a: i16, b: i16) -> Bool: Cmp.is_lt(i16.cmp(a, b))def i16.is_le(a: i16, b: i16) -> Bool: Cmp.is_le(i16.cmp(a, b))def i16.is_gt(a: i16, b: i16) -> Bool: Cmp.is_gt(i16.cmp(a, b))def i16.is_ge(a: i16, b: i16) -> Bool: Cmp.is_ge(i16.cmp(a, b))def i16.from_nat(k: Nat) -> i16: i16{W.from_nat(16n, k)}def i16.is_zero(a: i16) -> Bool: i16.is_eq(a, i16.from_nat(0n))def i16.to_nat(a: i16) -> Nat: match a: case i16{x}: Word.to_nat(16n, x)def i16.log2(+a: i16) -> Nat: match a: case i16{+x}: W.log2(16n, x)def i16.min(+a: i16, +b: i16) -> i16: Bool.pick(i16, i16.is_lt(a, b), a, b)def i16.max(+a: i16, +b: i16) -> i16: Bool.pick(i16, i16.is_lt(a, b), b, a)def i16.clamp(x: i16, lo: i16, hi: i16) -> i16: i16.min(i16.max(x, lo), hi)def i16.pow(+a: i16, k: Nat) -> i16: match a: case i16{+x}: i16{W.pow(16n, x, k)}def i16.is_even(a: i16) -> Bool: match a: case i16{+x}: W.is_zero(16n, Word.and(16n, x, W.one(16n)))def i16.show(+a: i16) -> String: match a: case i16{+x}: W.sshow(16n, 5n, x)def i16.read.wrap(m: Maybe<&2, Word(16n)>) -> Maybe<&2, i16>: match m: case None{}: None{} case Some{v}: Some{i16{v}}def i16.read(s: String) -> Maybe<&2, i16>: i16.read.wrap(W.sread(16n, s))type i32 is Data: i32{data: Word(32n)}def i32.inc(a: i32) -> i32: match a: case i32{x}: i32{Word.inc(32n, x)}def i32.add(a: i32, b: i32) -> i32: match a b: case i32{x} i32{y}: i32{Word.add(32n, x, y)}def i32.sub(a: i32, b: i32) -> i32: match a b: case i32{x} i32{y}: i32{Word.sub(32n, x, y)}def i32.mul(a: i32, b: i32) -> i32: match a b: case i32{x} i32{y}: i32{Word.mul(32n, x, y)}def i32.not(a: i32) -> i32: match a: case i32{x}: i32{Word.not(32n, x)}def i32.and(a: i32, b: i32) -> i32: match a b: case i32{x} i32{y}: i32{Word.and(32n, x, y)}def i32.or(a: i32, b: i32) -> i32: match a b: case i32{x} i32{y}: i32{Word.or(32n, x, y)}def i32.xor(a: i32, b: i32) -> i32: match a b: case i32{x} i32{y}: i32{Word.xor(32n, x, y)}def i32.shl(a: i32) -> i32: match a: case i32{x}: i32{Word.shl(32n, x)}def i32.shr(+a: i32) -> i32: match a: case i32{+x}: i32{W.sshr(32n, x)}def i32.shrn(a: i32, k: Nat) -> i32: match a: case i32{x}: i32{W.sshrn(32n, x, k)}def i32.cmp(+a: i32, +b: i32) -> Cmp: match a b: case i32{+x} i32{+y}: W.scmp(32n, x, y)def i32.div(+a: i32, +b: i32) -> i32: match a b: case i32{+x} i32{+y}: i32{W.sdiv(32n, x, y)}def i32.mod(+a: i32, +b: i32) -> i32: match a b: case i32{+x} i32{+y}: i32{W.smod(32n, x, y)}def i32.shln(a: i32, k: Nat) -> i32: match a: case i32{x}: i32{W.shln(32n, x, k)}def i32.is_eq(a: i32, b: i32) -> Bool: Cmp.is_eq(i32.cmp(a, b))def i32.is_ne(a: i32, b: i32) -> Bool: Bool.not(Cmp.is_eq(i32.cmp(a, b)))def i32.is_lt(a: i32, b: i32) -> Bool: Cmp.is_lt(i32.cmp(a, b))def i32.is_le(a: i32, b: i32) -> Bool: Cmp.is_le(i32.cmp(a, b))def i32.is_gt(a: i32, b: i32) -> Bool: Cmp.is_gt(i32.cmp(a, b))def i32.is_ge(a: i32, b: i32) -> Bool: Cmp.is_ge(i32.cmp(a, b))def i32.from_nat(k: Nat) -> i32: i32{W.from_nat(32n, k)}def i32.is_zero(a: i32) -> Bool: i32.is_eq(a, i32.from_nat(0n))def i32.to_nat(a: i32) -> Nat: match a: case i32{x}: Word.to_nat(32n, x)def i32.log2(+a: i32) -> Nat: match a: case i32{+x}: W.log2(32n, x)def i32.min(+a: i32, +b: i32) -> i32: Bool.pick(i32, i32.is_lt(a, b), a, b)def i32.max(+a: i32, +b: i32) -> i32: Bool.pick(i32, i32.is_lt(a, b), b, a)def i32.clamp(x: i32, lo: i32, hi: i32) -> i32: i32.min(i32.max(x, lo), hi)def i32.pow(+a: i32, k: Nat) -> i32: match a: case i32{+x}: i32{W.pow(32n, x, k)}def i32.is_even(a: i32) -> Bool: match a: case i32{+x}: W.is_zero(32n, Word.and(32n, x, W.one(32n)))def i32.show(+a: i32) -> String: match a: case i32{+x}: W.sshow(32n, 10n, x)def i32.read.wrap(m: Maybe<&2, Word(32n)>) -> Maybe<&2, i32>: match m: case None{}: None{} case Some{v}: Some{i32{v}}def i32.read(s: String) -> Maybe<&2, i32>: i32.read.wrap(W.sread(32n, s))type i64 is Data: i64{data: Word(64n)}def i64.inc(a: i64) -> i64: match a: case i64{x}: i64{Word.inc(64n, x)}def i64.add(a: i64, b: i64) -> i64: match a b: case i64{x} i64{y}: i64{Word.add(64n, x, y)}def i64.sub(a: i64, b: i64) -> i64: match a b: case i64{x} i64{y}: i64{Word.sub(64n, x, y)}def i64.mul(a: i64, b: i64) -> i64: match a b: case i64{x} i64{y}: i64{Word.mul(64n, x, y)}def i64.not(a: i64) -> i64: match a: case i64{x}: i64{Word.not(64n, x)}def i64.and(a: i64, b: i64) -> i64: match a b: case i64{x} i64{y}: i64{Word.and(64n, x, y)}def i64.or(a: i64, b: i64) -> i64: match a b: case i64{x} i64{y}: i64{Word.or(64n, x, y)}def i64.xor(a: i64, b: i64) -> i64: match a b: case i64{x} i64{y}: i64{Word.xor(64n, x, y)}def i64.shl(a: i64) -> i64: match a: case i64{x}: i64{Word.shl(64n, x)}def i64.shr(+a: i64) -> i64: match a: case i64{+x}: i64{W.sshr(64n, x)}def i64.shrn(a: i64, k: Nat) -> i64: match a: case i64{x}: i64{W.sshrn(64n, x, k)}def i64.cmp(+a: i64, +b: i64) -> Cmp: match a b: case i64{+x} i64{+y}: W.scmp(64n, x, y)def i64.div(+a: i64, +b: i64) -> i64: match a b: case i64{+x} i64{+y}: i64{W.sdiv(64n, x, y)}def i64.mod(+a: i64, +b: i64) -> i64: match a b: case i64{+x} i64{+y}: i64{W.smod(64n, x, y)}def i64.shln(a: i64, k: Nat) -> i64: match a: case i64{x}: i64{W.shln(64n, x, k)}def i64.is_eq(a: i64, b: i64) -> Bool: Cmp.is_eq(i64.cmp(a, b))def i64.is_ne(a: i64, b: i64) -> Bool: Bool.not(Cmp.is_eq(i64.cmp(a, b)))def i64.is_lt(a: i64, b: i64) -> Bool: Cmp.is_lt(i64.cmp(a, b))def i64.is_le(a: i64, b: i64) -> Bool: Cmp.is_le(i64.cmp(a, b))def i64.is_gt(a: i64, b: i64) -> Bool: Cmp.is_gt(i64.cmp(a, b))def i64.is_ge(a: i64, b: i64) -> Bool: Cmp.is_ge(i64.cmp(a, b))def i64.from_nat(k: Nat) -> i64: i64{W.from_nat(64n, k)}def i64.is_zero(a: i64) -> Bool: i64.is_eq(a, i64.from_nat(0n))def i64.to_nat(a: i64) -> Nat: match a: case i64{x}: Word.to_nat(64n, x)def i64.log2(+a: i64) -> Nat: match a: case i64{+x}: W.log2(64n, x)def i64.min(+a: i64, +b: i64) -> i64: Bool.pick(i64, i64.is_lt(a, b), a, b)def i64.max(+a: i64, +b: i64) -> i64: Bool.pick(i64, i64.is_lt(a, b), b, a)def i64.clamp(x: i64, lo: i64, hi: i64) -> i64: i64.min(i64.max(x, lo), hi)def i64.pow(+a: i64, k: Nat) -> i64: match a: case i64{+x}: i64{W.pow(64n, x, k)}def i64.is_even(a: i64) -> Bool: match a: case i64{+x}: W.is_zero(64n, Word.and(64n, x, W.one(64n)))def i64.show(+a: i64) -> String: match a: case i64{+x}: W.sshow(64n, 20n, x)def i64.read.wrap(m: Maybe<&2, Word(64n)>) -> Maybe<&2, i64>: match m: case None{}: None{} case Some{v}: Some{i64{v}}def i64.read(s: String) -> Maybe<&2, i64>: i64.read.wrap(W.sread(64n, s))type i128 is Data: i128{data: Word(128n)}def i128.inc(a: i128) -> i128: match a: case i128{x}: i128{Word.inc(128n, x)}def i128.add(a: i128, b: i128) -> i128: match a b: case i128{x} i128{y}: i128{Word.add(128n, x, y)}def i128.sub(a: i128, b: i128) -> i128: match a b: case i128{x} i128{y}: i128{Word.sub(128n, x, y)}def i128.mul(a: i128, b: i128) -> i128: match a b: case i128{x} i128{y}: i128{Word.mul(128n, x, y)}def i128.not(a: i128) -> i128: match a: case i128{x}: i128{Word.not(128n, x)}def i128.and(a: i128, b: i128) -> i128: match a b: case i128{x} i128{y}: i128{Word.and(128n, x, y)}def i128.or(a: i128, b: i128) -> i128: match a b: case i128{x} i128{y}: i128{Word.or(128n, x, y)}def i128.xor(a: i128, b: i128) -> i128: match a b: case i128{x} i128{y}: i128{Word.xor(128n, x, y)}def i128.shl(a: i128) -> i128: match a: case i128{x}: i128{Word.shl(128n, x)}def i128.shr(+a: i128) -> i128: match a: case i128{+x}: i128{W.sshr(128n, x)}def i128.shrn(a: i128, k: Nat) -> i128: match a: case i128{x}: i128{W.sshrn(128n, x, k)}def i128.cmp(+a: i128, +b: i128) -> Cmp: match a b: case i128{+x} i128{+y}: W.scmp(128n, x, y)def i128.div(+a: i128, +b: i128) -> i128: match a b: case i128{+x} i128{+y}: i128{W.sdiv(128n, x, y)}def i128.mod(+a: i128, +b: i128) -> i128: match a b: case i128{+x} i128{+y}: i128{W.smod(128n, x, y)}def i128.shln(a: i128, k: Nat) -> i128: match a: case i128{x}: i128{W.shln(128n, x, k)}def i128.is_eq(a: i128, b: i128) -> Bool: Cmp.is_eq(i128.cmp(a, b))def i128.is_ne(a: i128, b: i128) -> Bool: Bool.not(Cmp.is_eq(i128.cmp(a, b)))def i128.is_lt(a: i128, b: i128) -> Bool: Cmp.is_lt(i128.cmp(a, b))def i128.is_le(a: i128, b: i128) -> Bool: Cmp.is_le(i128.cmp(a, b))def i128.is_gt(a: i128, b: i128) -> Bool: Cmp.is_gt(i128.cmp(a, b))def i128.is_ge(a: i128, b: i128) -> Bool: Cmp.is_ge(i128.cmp(a, b))def i128.from_nat(k: Nat) -> i128: i128{W.from_nat(128n, k)}def i128.is_zero(a: i128) -> Bool: i128.is_eq(a, i128.from_nat(0n))def i128.to_nat(a: i128) -> Nat: match a: case i128{x}: Word.to_nat(128n, x)def i128.log2(+a: i128) -> Nat: match a: case i128{+x}: W.log2(128n, x)def i128.min(+a: i128, +b: i128) -> i128: Bool.pick(i128, i128.is_lt(a, b), a, b)def i128.max(+a: i128, +b: i128) -> i128: Bool.pick(i128, i128.is_lt(a, b), b, a)def i128.clamp(x: i128, lo: i128, hi: i128) -> i128: i128.min(i128.max(x, lo), hi)def i128.pow(+a: i128, k: Nat) -> i128: match a: case i128{+x}: i128{W.pow(128n, x, k)}def i128.is_even(a: i128) -> Bool: match a: case i128{+x}: W.is_zero(128n, Word.and(128n, x, W.one(128n)))def i128.show(+a: i128) -> String: match a: case i128{+x}: W.sshow(128n, 39n, x)def i128.read.wrap(m: Maybe<&2, Word(128n)>) -> Maybe<&2, i128>: match m: case None{}: None{} case Some{v}: Some{i128{v}}def i128.read(s: String) -> Maybe<&2, i128>: i128.read.wrap(W.sread(128n, s))def u64.zero() -> u64: u64.from_nat(0n)def u64.from_u32(lo: U32) -> u64: u64.from_nat(U32.to_nat(lo))def u64.pack(lo: U32, hi: U32) -> u64: u64.or(u64.from_u32(lo), u64.shln(u64.from_u32(hi), 32n))def u64.lo(+a: u64) -> u32: u32.from_nat(u64.to_nat(a))def u64.hi(+a: u64) -> u32: u32.from_nat(u64.to_nat(u64.shrn(a, 32n)))def u64.would_ovf(+a: u64, +b: u64) -> Bool: u64.is_lt(u64.add(a, b), a)# 32-byte key, eight little-endian words.type Pubkey is Data: Pk{w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32}def Pubkey.eq(+a: Pubkey, +b: Pubkey) -> Bool: match a b: case Pk{+a0, +a1, +a2, +a3, +a4, +a5, +a6, +a7} Pk{+b0, +b1, +b2, +b3, +b4, +b5, +b6, +b7}: Bool.and( U32.is_eq(a0, b0), Bool.and( U32.is_eq(a1, b1), Bool.and( U32.is_eq(a2, b2), Bool.and( U32.is_eq(a3, b3), Bool.and( U32.is_eq(a4, b4), Bool.and( U32.is_eq(a5, b5), Bool.and(U32.is_eq(a6, b6), U32.is_eq(a7, b7)), ), ), ), ), ), )def Pubkey.zero() -> Pubkey: Pk{0, 0, 0, 0, 0, 0, 0, 0}# Byte window into a word buffer. off and len are bytes.type Slice is Data: Slice{words: List<&2, U32>, off: U32, len: U32}def as_bytes(xs: List<&2, U32>) -> Slice: Slice{xs, 0, 0}def slice(s: Slice, off: Nat, len: Nat) -> Slice: match s: case Slice{words, +base, n}: Slice{words, U32.add(base, U32.from_nat(off)), U32.from_nat(len)}def slice_len(s: Slice) -> U32: match s: case Slice{words, off, +n}: n# Ordered find_program_address seeds. The mark is not the hash.type Seeds is Data: Seeds{mark: U32}def seeds_nil() -> Seeds: Seeds{0}# One Solana account. lamports is a wrapping u64.type Account is Data: Acc{ key: Pubkey, owner: Pubkey, lamports: u64, data: List<&2, U32>, is_signer: Bool, is_writable: Bool, }def key(a: Account) -> Pubkey: match a: case Acc{+k, own, lams, bytes, signer, writable}: kdef owner(a: Account) -> Pubkey: match a: case Acc{k, +own, lams, bytes, signer, writable}: owndef is_signer(a: Account) -> Bool: match a: case Acc{k, own, lams, bytes, +signer, writable}: signerdef is_writable(a: Account) -> Bool: match a: case Acc{k, own, lams, bytes, signer, +writable}: writabledef lamports(a: Account) -> u64: match a: case Acc{k, own, +lams, bytes, signer, writable}: lamsdef data(a: Account) -> List<&2, U32>: match a: case Acc{k, own, lams, +bytes, signer, writable}: bytesdef set_lamports(a: Account, lams: u64) -> Account: match a: case Acc{k, own, old, bytes, signer, writable}: Acc{k, own, lams, bytes, signer, writable}def set_data(a: Account, bytes: List<&2, U32>) -> Account: match a: case Acc{k, own, lams, old, signer, writable}: Acc{k, own, lams, bytes, signer, writable}def empty_account() -> Account: Acc{Pubkey.zero(), Pubkey.zero(), u64.from_nat(0n), Nil{}, False{}, False{}}def read_i8(m: Maybe<&2, i8>) -> Bool: match m: case None{}: True{} case Some{v}: False{}def round_u8(m: Maybe<&2, u8>) -> Bool: match m: case None{}: False{} case Some{v}: u8.is_eq(v, u8.from_nat(42n))def round_i8(m: Maybe<&2, i8>) -> Bool: match m: case None{}: False{} case Some{v}: i8.is_eq(v, i8.sub(i8.from_nat(0n), i8.from_nat(1n)))def main() -> Bool: +neg1 = i8.sub(i8.from_nat(0n), i8.from_nat(1n)) +neg2 = i8.sub(i8.from_nat(0n), i8.from_nat(2n)) Bool.and( u8.is_eq(u8.add(u8.from_nat(200n), u8.from_nat(100n)), u8.from_nat(44n)), Bool.and( u8.is_eq(u8.not(u8.from_nat(0n)), u8.from_nat(255n)), Bool.and( i8.is_lt(neg1, i8.from_nat(0n)), Bool.and( i8.is_eq( i8.div( i8.sub(i8.from_nat(0n), i8.from_nat(5n)), i8.from_nat(2n), ), neg2, ), Bool.and( i8.is_eq(i8.shr(neg2), neg1), Bool.and( round_u8(u8.read(u8.show(u8.from_nat(42n)))), Bool.and( round_i8(i8.read(i8.show(neg1))), Bool.and( read_i8( i8.read( SCon{ Chr{49}, SCon{Chr{50}, SCon{Chr{56}, SNil{}}}, }, ), ), u64.is_eq( u64.add(u64.from_nat(1n), u64.from_nat(2n)), u64.from_nat(3n), ), ), ), ), ), ), ), ), )