Roots share their ~ constants, so a template goes to the kernel once instead of once per root that uses it

[chelokot]

Problem

--verdict checks a template like def pair(~a: Nat, ~b: Nat) at made-up constants pair~a, pair~b. Every root gets its own made-up constants, and every template it calls is copied at them. So in

def pair(~a: Nat, ~b: Nat) -> Nat: Nat.add(a, b)
def other(~x: Nat, ~y: Nat) -> Nat: pair(~x, ~y)

pair goes to the kernel twice: once at pair~a, pair~b, once at other~x, other~y. A template used by 18 roots goes 18 times, with everything it calls.

Fix

A root reuses the constant an earlier root made for the same place and type. Above, other checks at pair~a, pair~b, and pair(~x, ~y) is the copy that is already there.

This is safe because:

• the kernel knows nothing about a made-up constant, so a proof at it holds for every value, whichever root made it;
• two parameters of one root are at different places, so they still get different constants ({a == b} still does not check).

Numbers

Our book (generated square-packing proofs, 2.4 MB), on main (d052d4f), same machine:

	main	this PR
text sent to the kernel	237 MB	23.5 MB
memory to write it (-o)	14.7 GB	4.5 GB
kernel memory	8.6 GB	0.85 GB
kernel time (two runs, busy)	24 to 63 min	57 s
our CI job	27 min	7.6 min

gates/safe_node.ts on all 1580 files in tests/ prints exactly the same output as main.

Note on #1263

#1263 lets a root change the models of its constants after the fact. With shared constants, that change would also affect other roots, so a root that needs such a change should get its own constants again. If #1263 lands first, I will add that to this PR.

🤖 Generated with Claude Code