Bitcoin proof of work in pure lambda calculus

README

$ npm i -g @alexo/lambda
└── @alexo/[email protected]

$ make
	node work2mlc.js getwork.json 381353fa >test.mlc
	lambda -pem lib.mlc -f test.mlc
3335648(653961), 17837 ms
v1, v2: v1
$ 

array.mlc

include(common.mlc)dnl

# Prepend <x1,..., xn> x0 = <x0,..., xn>
Prepend = a, x, z: a (z x);

# Append <x1,..., xn> xn+1 = <x1,..., xn+1>
Append = a, x, z: a z x;

# Repeat n x = <x,..., x>
Repeat = n, x: n (a: Append a x) I;

# Reduce f i n <x1,..., xn> = f (...(f i x1)...) xn
Reduce = f, i, n, x: x (n (g, j, y: g (f j y)) I i);

# Map f n <x1,..., xn> = <f x1,..., f xn>
Map = f: Reduce (a, y: Append a (f y)) I;

# Reverse n <x1,..., xn> = <xn,..., x1>
Reverse = Reduce Prepend I;

# Curry f n x1 ... xn = f <x1,..., xn>
Curry = f, n: n (f, a, x: f (Append a x)) f I;

# CurryN f n <k1,..., kn> x1_1 ... x1_k1 ... xn_1 ... xn_kn =
#   f <x1_1,..., x1_k1> ... <xn_1,..., xn_kn>
CurryN = f, n, s: Reduce (a, k, z: Curry (x: a (z x)) k) I
	n (Reverse n s) f;

# Split m n <x1,..., xm+n> = <<x1,..., xm>, <xm+1,..., xm+n>>
Split = m, n, x: x (Curry (y: Curry (Cons y) n) m);

# Shift n <x1,..., xn> = x1
Shift = n, x: Split 1 (-1 n) x T I;

# Pop n <x1,..., xn> = xn
Pop = n, x: Split (-1 n) 1 x F I;

# Optimize f n <k1,..., kn> = f_optimized
Optimize = f, n, s: Curry (a: Reduce * I n a (CurryN f n s)) n;

# Zip f n <x1,..., xn> <y1,..., yn> = <f x1 y1,..., f xn yn>
Zip_ = f, n, x, y, z: x (Reduce (a, w, t, v: a (t (f v w))) I
	n (Reverse n y) z);
Zip = f, n: Optimize (Zip_ f n) 2 (Cons n n);
Zip3 = f, n, x, y, z: Zip_ I n (Zip_ f n x y) z;

binary.mlc

include(array.mlc)dnl

# Bits representation
Z = F;
O = T;
ToBool = I;
Cout = Cons Or And;
Adder = a, b, c: Xor c (Xor a b);
Sum = a, b, c: Cons (Adder a b c) (Cout a b c);

# ToBin k "bk...b1" = <b1,..., bk>
ToBin = k: k (f, b, c: f (Append b (Odd? c O Z)) (/2 c)) T I;

# FromBin k <b1,..., bk> = "bk...b1"
FromBin = k, b: Reduce (c, x: ToBool x +1 I (* c 2)) 0
	k (Reverse k b);

# BinPri k <b1,..., bk> = _bk ... _b1
BinPri = k, b: Map (x: ToBool x _1 _0) k (Reverse k b) I;

# Bitwise operations
BinZero = k, b: Not (Reduce (a, x: Or a (ToBool x)) F k b);
BinXor3 = Zip3 Adder;
BinCh = Zip3 ToBool;
BinMaj = Zip3 Cout;
BinAdd_ = k, a, b: Reduce
	(p, x: p (r, c: x c (s, o: Cons (Append r s) o)))
	(Cons I Z) k (Zip_ Sum k a b) T;
BinAdd = k: Optimize (BinAdd_ k) 2 (Cons k k);
BinAdd4 = k, a, b, c, d:
	BinAdd_ k (BinAdd_ k a b) (BinAdd_ k c d);
BinAdd5 = k, a, b, c, d: BinAdd_ k (BinAdd4 k a b c d);
BinRot = k, b, n: Split n (- k n) b (x, y: * y x);
BinShr = k, b, n: Split n (- k n) b (x, y: * y (Repeat n Z));

# 32-bit arithmetic
Pri32 = BinPri 32;
Zero32 = BinZero 32;
Xor3 = BinXor3 32;
Add32_ = BinAdd_ 32;
Add32 = BinAdd 32;
Add4 = BinAdd4 32;
Add5 = BinAdd5 32;
Rot32 = BinRot 32;
Shr32 = BinShr 32;
Ch32 = BinCh 32;
Maj32 = BinMaj 32;

common.mlc

# Common combinators
I = x: x;
K = x, y: x;
S = x, y, z: x z (y z);
Y = (a: a a) (a, f: f (a a f));
T = K;
F = K I;

# Pairs/lists
[] = K T;
[]? = l: l (h, t: F);
Cons = h, t, x: x h t;

# Boolean operators
Not = p, a, b: p b a;
And = p, q: p q F;
Or = p: p T;
Xor = Cons Not I;

# Church arithmetic
+1 = n, f, x: (g: g (n g x)) (g: f g);
+ = m, n, f, x: (g: m g (n g x)) (g: f g);
* = m, n, f: n (m f);
^ = m, n: n m;
-1 = n, f, x: n (g, h: h (g f)) (K x) I;
- = m, n: n -1 m;
/2 = n, s, z: n (f, a, b: f b (s a)) T z z;
Odd? = n: n Not F;
0? = n: n (K F) T;

# Church numerals
0 = F;
1 = I;
2 = f, x: (g: g (g x)) (y: f y);
3 = +1 2;
4 = ^ 2 2;
5 = + 2 3;
6 = * 2 3;
7 = +1 6;
8 = ^ 2 3;
9 = ^ 3 2;
10 = * 2 5;
11 = +1 10;
13 = + 3 10;
15 = + 5 10;
16 = ^ 2 4;
17 = +1 16;
18 = +1 17;
19 = +1 18;
20 = * 2 10;
22 = + 2 20;
25 = + 5 20;
30 = * 3 10;
32 = ^ 2 5;
48 = * 3 16;
64 = ^ 2 6;
100 = ^ 10 2;
128 = ^ 2 7;
256 = ^ 2 8;
512 = ^ 2 9;
1k = ^ 10 3;
1ki = ^ 2 10;
1m = ^ 10 6;
1mi = ^ 2 20;
1g = ^ 10 9;
1gi = ^ 2 30;

getwork.json

{
	"error": null,
	"id": 1,
	"result": {
		"data": "00000002b15704f4ecae05d077e54f6ec36da7f20189ef73b77603225ae56d2b00000000b052cbbdeed2489ccb13a526b77fadceef4caf7d3bb82a9eb0b69ebb90f9f5a7510c27fd1c0e8a3700000000000000800000000000000000000000000000000000000000000000000000000000000000000000000000000080020000",
		"hash1": "00000000000000000000000000000000000000000000000000000000000000000000008000000000000000000000000000000000000000000000000000010000",
		"midstate": "509ee324c8bbfe1e915b54fbcaf31fdb6d356fa6f3c08274a8cac0acad0df100",
		"target": "ffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000"
	}
}

hex.mlc

divert(-1)

define(`invert', `ifelse(len($1), 0, `',
	`invert(substr($1, 1))' substr($1, 0, 1))')
define(`tobin16', `ifelse($1, 0,
	invert(eval(`0x'substr($2, 4, 4), 2, 16)),
	invert(eval(`0x'substr($2, 0, 4), 2, 16)))')
define(`tobin32', `tobin16(0, $1)tobin16(1, $1)')
define(`tobool', `translit(tobin32($1), 01, ZO)')
define(`hex', `(x: x`'tobool($1))')

divert(0)dnl
0h = hex(00000000);
1h = hex(00000001);
-1h = hex(ffffffff);

InitHash = x: x
	hex(6a09e667)
	hex(bb67ae85)
	hex(3c6ef372)
	hex(a54ff53a)
	hex(510e527f)
	hex(9b05688c)
	hex(1f83d9ab)
	hex(5be0cd19);

RoundConst = x: x
	hex(428a2f98)
	hex(71374491)
	hex(b5c0fbcf)
	hex(e9b5dba5)
	hex(3956c25b)
	hex(59f111f1)
	hex(923f82a4)
	hex(ab1c5ed5)
	hex(d807aa98)
	hex(12835b01)
	hex(243185be)
	hex(550c7dc3)
	hex(72be5d74)
	hex(80deb1fe)
	hex(9bdc06a7)
	hex(c19bf174)
	hex(e49b69c1)
	hex(efbe4786)
	hex(0fc19dc6)
	hex(240ca1cc)
	hex(2de92c6f)
	hex(4a7484aa)
	hex(5cb0a9dc)
	hex(76f988da)
	hex(983e5152)
	hex(a831c66d)
	hex(b00327c8)
	hex(bf597fc7)
	hex(c6e00bf3)
	hex(d5a79147)
	hex(06ca6351)
	hex(14292967)
	hex(27b70a85)
	hex(2e1b2138)
	hex(4d2c6dfc)
	hex(53380d13)
	hex(650a7354)
	hex(766a0abb)
	hex(81c2c92e)
	hex(92722c85)
	hex(a2bfe8a1)
	hex(a81a664b)
	hex(c24b8b70)
	hex(c76c51a3)
	hex(d192e819)
	hex(d6990624)
	hex(f40e3585)
	hex(106aa070)
	hex(19a4c116)
	hex(1e376c08)
	hex(2748774c)
	hex(34b0bcb5)
	hex(391c0cb3)
	hex(4ed8aa4a)
	hex(5b9cca4f)
	hex(682e6ff3)
	hex(748f82ee)
	hex(78a5636f)
	hex(84c87814)
	hex(8cc70208)
	hex(90befffa)
	hex(a4506ceb)
	hex(bef9a3f7)
	hex(c67178f2);

NullMsg = x: x
	hex(80000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000);

Hash1Padding = x: x
	hex(80000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000100);

WorkPadding = x: x
	hex(80000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000000)
	hex(00000280);

lib.mlc

include(binary.mlc)
include(hex.mlc)dnl

Opt32 = f, n: Optimize f n (Repeat n 32);

BlendS0 = w: Xor3 (Rot32 w 7) (Rot32 w 18) (Shr32 w 3);
BlendS1 = w: Xor3 (Rot32 w 17) (Rot32 w 19) (Shr32 w 10);
BlendS_ = a, b, c, d: Add4 a (BlendS0 b) c (BlendS1 d);
BlendS = Opt32 BlendS_ 4;
Blend = w16, w15, w14, w13, w12, w11, w10, w9,
	w8,  w7,  w6,  w5,  w4,  w3,  w2,  w1, a: Cons
	(Append a w16)
	(x: x w15 w14 w13 w12 w11 w10 w9 w8 w7 w6 w5 w4 w3 w2 w1
		(BlendS w16 w15 w7 w2));

Schedule = 48 (f, l, r: r Blend l f) * I;

RoundK = m: Zip Add32 64 RoundConst (Schedule m);

RoundS1 = e: Xor3 (Rot32 e 6) (Rot32 e 11) (Rot32 e 25);
RoundT1_ = e, f, g, h, w: Add5 h (RoundS1 e) w (Ch32 e f g);
RoundT1 = Opt32 RoundT1_ 6;

RoundS0 = a: Xor3 (Rot32 a 2) (Rot32 a 13) (Rot32 a 22);
RoundT2_ = a, b, c: Add32_ (RoundS0 a) (Maj32 a b c);
RoundT2 = Opt32 RoundT2_ 3;

Round = a, b, c, d, e, f, g, h, w:
	(t1, t2, x: x (t1 t2) a b c (t1 d) e f g)
	(RoundT1 e f g h w) (RoundT2 a b c);

Compress = m, h: Reduce (v: v Round) h 64 (RoundK m);

Hash1Mid_ = m, s: Zip_ Add32 8 s (Compress m s);
Hash1Mid = Optimize Hash1Mid_ 2 (Cons 16 8);
Hash1 = m: Hash1Mid m InitHash;
Hash2Mid = m, s: Hash1 (* (Hash1Mid m s) Hash1Padding);
Hash2 = m: Hash2Mid m InitHash;

RunHash = m, d, n: Hash2Mid (* (Append d n) WorkPadding) m;

Makefile

all:
	node work2mlc.js getwork.json 381353fa >test.mlc
	lambda -pem lib.mlc -f test.mlc

clean:

test.mlc

Mid = x: x
	hex(24e39e50)
	hex(1efebbc8)
	hex(fb545b91)
	hex(db1ff3ca)
	hex(a66f356d)
	hex(7482c0f3)
	hex(acc0caa8)
	hex(00f10dad);

Data = x: x
	hex(a7f5f990)
	hex(fd270c51)
	hex(378a0e1c);

Nonce = hex(381353fa);

Zero32 (Pop 8 (RunHash Mid Data Nonce))

work2mlc.js

"use strict";

const argv = process.argv;
const nonce = `hex(${argv.pop()})`;
const work = require(`./${argv.pop()}`).result;
const re = /(..)(..)(..)(..)/g;
const sub = "\n\thex($4$3$2$1)";
const tohex = str => str.replace(re, sub);
const data = tohex(work.data.slice(128, 152));
const mid = tohex(work.midstate);

console.log(`Mid = x: x${mid};\n`);
console.log(`Data = x: x${data};\n`);
console.log(`Nonce = ${nonce};\n`);

console.log("Zero32 (Pop 8 (RunHash Mid Data Nonce))");