Standalone computational specification

def retire_capacity(g, region, frame, occupancy=None): owned(("cap", region), frame) occ = dict(occupancy or {}) caps = g.capacity() if region not in caps or caps[region] <= occ.get(region, 0): raise GuardFailure("no unoccupied capacity unit") caps[region] -= 1 g2 = replace(g, cap=tuple(sorted(caps.items()))) return finish(g, g2, -1)

def delete_active(g, tid, frame): owned(("link", tid), frame) found = [edge for edge in g.active if edge[0] == tid] if not found: raise GuardFailure("active identifier absent") g2 = replace(g, active=tuple(edge for edge in g.active if edge[0] != tid)) return finish(g, g2, -1)

def delete_latent(g, tid, frame): owned(("link", tid), frame) found = [link for link in g.latent if link[0] == tid] if not found: raise GuardFailure("latent identifier absent") g2 = replace(g, latent=tuple(link for link in g.latent if link[0] != tid)) return finish(g, g2, -1)

def activate(g, tid, source, frame): # The frame represents the single activation authority. # Production term typing must issue that authority linearly. owned(("link", tid), frame) found = [link for link in g.latent if link[0] == tid] if not found: raise GuardFailure("latent identifier absent or spent") _, ends = found[0] if source not in ends: raise GuardFailure("source is not an endpoint") target = next(iter(ends - source)) if g.has_path(target, source): raise GuardFailure("activation would create a cycle") g2 = replace( g, latent=tuple(link for link in g.latent if link[0] != tid), active=g.active + ((tid, source, target),), ) return finish(g, g2, 0)

def expect_guard_failure(fn): try: fn() except GuardFailure: return raise InvariantError("expected guard refusal did not occur")

def ceil_log2(n): require(isinstance(n, int) and n >= 1, "ceil_log2 requires a positive integer") return (n - 1).bit_length()

def primitive_multiplicities(m): m = tuple(m) require(bool(m), "empty multiplicity list") require(all(isinstance(x, int) and x >= 0 for x in m), "multiplicities must be nonnegative integers") positive = [x for x in m if x] require(bool(positive), "all multiplicities vanish") d = reduce(gcd, positive) return tuple(x // d for x in m)

def finegrain_cost(m, s=1): require(isinstance(s, int) and s >= 0, "invalid register size") m = primitive_multiplicities(m) require(len(m) <= 2 ** s, "too many outcome labels") M = sum(m) return s + ceil_log2(M) + ceil_log2(max(m))