diff --git a/docs/_source/merkle-agi-dag-v7.rst b/docs/_source/merkle-agi-dag-v7.rst index b945b17..8762fb5 100644 --- a/docs/_source/merkle-agi-dag-v7.rst +++ b/docs/_source/merkle-agi-dag-v7.rst @@ -78,18 +78,20 @@ The outputs (\mathcal O\subseteq V) define the model outputs. The overall model ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We fix a public quantization step (\Delta>0). For any real tensor (T), -[ -Q(T) ;=; \mathrm{round}(T/\Delta)\in \mathbb Z^{\text{shape}(T)},\quad -q^{-1}(Z)=Z\cdot \Delta,\quad -|T - q^{-1}(Q(T))|_{\infty}\le \Delta/2. -] + +:: + + Q(T) ;=; \mathrm{round}(T/\Delta)\in \mathbb Z^{\text{shape}(T)},\quad + q^{-1}(Z)=Z\cdot \Delta,\quad + |T - q^{-1}(Q(T))|_{\infty}\le \Delta/2. + All hashed numerics (parameters and any activations that appear in proofs) are expressed as integers via Q. Part 2 supplies deterministic fixed-point kernels used for verification. § 2.3 Canonical encoding (A1) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We define an injective type-length-value (TLV) encoding: -- Each field is tag (1 byte) | len (4 bytes LE) | payload. +- Each field is tag (1 byte) \| len (4 bytes LE) \| payload. - Composite objects are the concatenation of TLVs in a prescribed order. - Domain separation tags disambiguate: "base", "node", "leaf", "forest-root", "op", "params", "attrs", "arity", "child", etc. - Length-prefix every child commitment to avoid ambiguity under concatenation. @@ -120,17 +122,19 @@ Let - op(v), version(v), attrs(v) be canonicalized, - Q(Θ_v) be the integer tensor of params. Define: -[ -h^{\text{base}}_v -= H!\big(\mathrm{Enc}( -\text{"base"}, -\text{id}=id(v), -\text{"op"},op(v), -\text{"ver"},version(v), -\text{"attrs"},attrs(v), -\text{"params"},Q(\Theta_v) -)\big). -] + +:: + + h^{\text{base}}_v + = H!\big(\mathrm{Enc}( + \text{"base"}, + \text{id}=id(v), + \text{"op"},op(v), + \text{"ver"},version(v), + \text{"attrs"},attrs(v), + \text{"params"},Q(\Theta_v) + )\big). + § 3.2 Parent order & commutativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -140,27 +144,33 @@ Each operator declares whether its inputs are commutative (e.g., add) or ordered § 3.3 Node commitment ~~~~~~~~~~~~~~~~~~~~~~ -Let (k=|\mathrm{pred}(v)|), and (C(u_i)) denote each parent’s commitment. Then +Let (k=\|\mathrm{pred}(v)\|), and (C(u_i)) denote each parent’s commitment. Then - Leaf (k=0): - [ - C(v) = H!\big(\mathrm{Enc}(\text{"leaf"}, \text{id}=id(v), \text{"base"},h^{\text{base}}_v)\big). - ] + + :: + + C(v) = H!\big(\mathrm{Enc}(\text{"leaf"}, \text{id}=id(v), \text{"base"},h^{\text{base}}_v)\big). + - Internal (k>0): - [ - \begin{aligned} - C(v) = H!\big(&\mathrm{Enc}(\text{"node"},\text{id}=id(v),\text{"arity"},k,\text{"base"},h^{\text{base}}v) ;|; \ - &\underbrace{\mathrm{LP}(C(u_1)) ;|; \cdots ;|; \mathrm{LP}(C(u_k))}{\text{each child length-prefixed}}\big), - \end{aligned} - ] - where (\mathrm{LP}(y)=\text{len}(y),|,y). + + :: + + \begin{aligned} + C(v) = H!\big(&\mathrm{Enc}(\text{"node"},\text{id}=id(v),\text{"arity"},k,\text{"base"},h^{\text{base}}v) ;|; \ + &\underbrace{\mathrm{LP}(C(u_1)) ;|; \cdots ;|; \mathrm{LP}(C(u_k))}{\text{each child length-prefixed}}\big), + \end{aligned} + + where (\mathrm{LP}(y)=\text{len}(y),\|,y). § 3.4 Model root ~~~~~~~~~~~~~~~~~ For outputs (\mathcal O=(o_1,\dots,o_m)) in canonical order: -[ -C(M) ;=; H!\big(\mathrm{Enc}(\text{"forest-root"},\text{"nout"},m),|,\mathrm{LP}(C(o_1)),|,\cdots,|,\mathrm{LP}(C(o_m))\big). -] + +:: + + C(M) ;=; H!\big(\mathrm{Enc}(\text{"forest-root"},\text{"nout"},m),|,\mathrm{LP}(C(o_1)),|,\cdots,|,\mathrm{LP}(C(o_m))\big). + Remark (block hashing). Large parameter tensors are partitioned into fixed-size blocks; each block is a leaf with its own base hash. The node’s params field then references block leaves, preserving completeness while enabling sparse proofs. § 4 Security Core — Long-Form Proofs @@ -173,7 +183,7 @@ Proof (long-form, induction on height). Define the height of a node as the length of the longest path from any leaf to the node. Proceed by induction on height. - Base (height 0). Leaves differ if any of op, version, attrs, or Q(Θ_v) differ. By A1, the Enc("base", …) bitstring differs, so (h^{\text{base}}_v) differs unless (H) collides. Since a leaf commitment is (H(\mathrm{Enc}("leaf", id, h^{\text{base}}_v))), the commitment also differs absent collision. - Inductive step. Assume the claim holds for all nodes of height ( bytes: - assert len(tag) == 1 - return tag + len(payload).to_bytes(4, "little") + payload -def enc_str(s: str) -> bytes: - b = s.encode("utf-8") - return tlv(b"\x01", b) # tag 0x01 = utf8 string -def enc_int(i: int) -> bytes: - b = i.to_bytes(8, "little", signed=True) - return tlv(b"\x02", b) # tag 0x02 = int64 -def enc_bytes(b: bytes) -> bytes: - return tlv(b"\x03", b) # tag 0x03 = raw bytes -def enc_tensor_q(Z: "IntTensor") -> bytes: - # deterministic row-major, little-endian 64-bit ints - b = Z.astype(" bytes: + assert len(tag) == 1 + return tag + len(payload).to_bytes(4, "little") + payload + def enc_str(s: str) -> bytes: + b = s.encode("utf-8") + return tlv(b"\x01", b) # tag 0x01 = utf8 string + def enc_int(i: int) -> bytes: + b = i.to_bytes(8, "little", signed=True) + return tlv(b"\x02", b) # tag 0x02 = int64 + def enc_bytes(b: bytes) -> bytes: + return tlv(b"\x03", b) # tag 0x03 = raw bytes + def enc_tensor_q(Z: "IntTensor") -> bytes: + # deterministic row-major, little-endian 64-bit ints + b = Z.astype(" bytes: # SHA-256 wrapper - import hashlib - return hashlib.sha256(data).digest() -def commit_leaf(node) -> bytes: - base = H(Enc_base(node)) - preimage = tlv(b"\x30", # "leaf" - tlv(b"\x10", enc_str(node.id)) + - tlv(b"\x21", enc_bytes(base))) - return H(preimage) -def commit_node(node, child_commits: list[bytes]) -> bytes: - base = H(Enc_base(node)) - # commutativity: optionally sort child_commits lexicographically - if node.is_commutative: - child_commits = sorted(child_commits) - children_lp = b"".join(tlv(b"\x40", c) for c in child_commits) # "\x40" = "child" - preimage = tlv(b"\x31", # "node" - tlv(b"\x10", enc_str(node.id)) + - tlv(b"\x22", enc_int(len(child_commits))) + - tlv(b"\x21", enc_bytes(base)) + - children_lp) - return H(preimage) -def commit_model(outputs: list[bytes]) -> bytes: - roots_lp = b"".join(tlv(b"\x41", c) for c in outputs) # "\x41" = "root-child" - preimage = tlv(b"\x32", tlv(b"\x23", enc_int(len(outputs))) + roots_lp) # "forest-root" - return H(preimage) -``` + +.. code-block:: python + + def H(data: bytes) -> bytes: # SHA-256 wrapper + import hashlib + return hashlib.sha256(data).digest() + def commit_leaf(node) -> bytes: + base = H(Enc_base(node)) + preimage = tlv(b"\x30", # "leaf" + tlv(b"\x10", enc_str(node.id)) + + tlv(b"\x21", enc_bytes(base))) + return H(preimage) + def commit_node(node, child_commits: list[bytes]) -> bytes: + base = H(Enc_base(node)) + # commutativity: optionally sort child_commits lexicographically + if node.is_commutative: + child_commits = sorted(child_commits) + children_lp = b"".join(tlv(b"\x40", c) for c in child_commits) # "\x40" = "child" + preimage = tlv(b"\x31", # "node" + tlv(b"\x10", enc_str(node.id)) + + tlv(b"\x22", enc_int(len(child_commits))) + + tlv(b"\x21", enc_bytes(base)) + + children_lp) + return H(preimage) + def commit_model(outputs: list[bytes]) -> bytes: + roots_lp = b"".join(tlv(b"\x41", c) for c in outputs) # "\x41" = "root-child" + preimage = tlv(b"\x32", tlv(b"\x23", enc_int(len(outputs))) + roots_lp) # "forest-root" + return H(preimage) + A3. Path proof verification (subset) -```python -def verify_path(CM_root: bytes, proof) -> bool: - # proof contains: outputs commitments, and for a chosen output o: - # a bottom-up list of nodes with their encoded base fields, - # their arity k, commutativity flag, and sibling commitments - # sufficient to reconstruct each ancestor commitment. - C = {} - for node in proof.bottom_up_nodes: - base = H(Enc_base(node)) - child_commits = [C[ch.id] for ch in node.children_in_proof] - # plus sibling commitments provided as raw bytes - child_commits += node.sibling_commits - if node.is_commutative: - child_commits = sorted(child_commits) - if node.arity != len(child_commits): - return False - preimage = tlv(b"\x31", tlv(b"\x10", enc_str(node.id)) + - tlv(b"\x22", enc_int(len(child_commits))) + - tlv(b"\x21", enc_bytes(base)) + - b"".join(tlv(b"\x40", c) for c in child_commits)) - C[node.id] = H(preimage) - # reached output commitment: - Co = C[proof.output_id] - # authenticate forest root - forest = commit_model(proof.all_output_commitments) - return forest == CM_root and Co in proof.all_output_commitments -``` + +.. code-block:: python + + def verify_path(CM_root: bytes, proof) -> bool: + # proof contains: outputs commitments, and for a chosen output o: + # a bottom-up list of nodes with their encoded base fields, + # their arity k, commutativity flag, and sibling commitments + # sufficient to reconstruct each ancestor commitment. + C = {} + for node in proof.bottom_up_nodes: + base = H(Enc_base(node)) + child_commits = [C[ch.id] for ch in node.children_in_proof] + # plus sibling commitments provided as raw bytes + child_commits += node.sibling_commits + if node.is_commutative: + child_commits = sorted(child_commits) + if node.arity != len(child_commits): + return False + preimage = tlv(b"\x31", tlv(b"\x10", enc_str(node.id)) + + tlv(b"\x22", enc_int(len(child_commits))) + + tlv(b"\x21", enc_bytes(base)) + + b"".join(tlv(b"\x40", c) for c in child_commits)) + C[node.id] = H(preimage) + # reached output commitment: + Co = C[proof.output_id] + # authenticate forest root + forest = commit_model(proof.all_output_commitments) + return forest == CM_root and Co in proof.all_output_commitments + Determinism note. All encodings and child order rules are explicit; integer tensors and byte orders are fixed; hence recomputation is platform-independent. § 4.2 What Part 1 establishes (and what follows next) @@ -319,11 +335,13 @@ Purpose. This section fixes the exact arithmetic the verifier uses when checking - Global public step (\Delta>0) (chosen and published with the model). - Quantize any real tensor (T) elementwise: - [ - Q(T)=\operatorname{round}(T/\Delta)\in \mathbb Z^{\text{shape}(T)} \quad\text{(round to nearest, ties to even).} - ] + + :: + + Q(T)=\operatorname{round}(T/\Delta)\in \mathbb Z^{\text{shape}(T)} \quad\text{(round to nearest, ties to even).} + - Dequantize: (q^{-1}(Z)=Z\cdot \Delta). -- Uniform bound: (|T - q^{-1}(Q(T))|_\infty \le \Delta/2). +- Uniform bound: (\|T - q^{-1}(Q(T))\|_\infty \le \Delta/2). Determinism note. “Ties to even” removes platform ambiguity at .5 steps. The rounding rule is part of A2 and is encoded in the reproducibility manifest (Appendix schema). § 5.2 Integer arithmetic model @@ -342,17 +360,20 @@ We define the exact integer kernels used by the verifier. Let (Z,W,B) denote int § 5.3.1 Bias add (elementwise) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -[ -\text{bias_add}_q(Z,B) ;=; Z + B \quad(\text{integer add}) -] +:: + + \text{bias_add}_q(Z,B) ;=; Z + B \quad(\text{integer add}) + § 5.3.2 Matrix multiply (affine core) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Given (W\in \mathbb Z^{m\times n},, A\in \mathbb Z^{n}) (vector) or (\mathbb Z^{n\times b}) (batch): -[ -\mathrm{gemm_q}(W,A) = W\cdot A \quad\text{over }\mathbb Z, -] + +:: + + \mathrm{gemm_q}(W,A) = W\cdot A \quad\text{over }\mathbb Z, + i.e., ((\mathrm{gemm_q})i = \sum{j=1}^n W_{ij},A_j). Scaling semantics (for real comparison only): If (w= q^{-1}(W), a=q^{-1}(A)), then (w\cdot a = \Delta^2 \cdot (W\cdot A)). We postpone the (\Delta^2) factor until a bound requires it. @@ -404,7 +425,7 @@ Non-polynomial functions (exp, erf/GELU, rsqrt) use byte-committed lookup tables Example recipe (exp LUT). Domain ([-K,K]) at step (h). For each grid point (x_k = k,h), store (\lfloor \exp(x_k)/\Delta_e \rceil) as int64. Interpolation rule is fixed (nearest or linear with even-tie). The tuple ((K,h,\Delta_e,\text{interp})) is committed. Lemma (LUT reproducibility). Given the recipe (R) and its parameters in attrs, any conforming implementation reconstructs exactly the same LUT byte string (B_L). Proof. All steps are deterministic over rationals with a fixed rounding policy. A1 injectivity binds the parameters; T1 then binds the bytes. ∎ -Lemma (LUT error bound). If (R) guarantees (|f(x) - q^{-1}(L(x))| \le \varepsilon_{\text{LUT}}) on its domain, then the integer-space kernel using (L) yields at most (\varepsilon_{\text{LUT}}) local real-space discrepancy per evaluation (before downstream scaling). +Lemma (LUT error bound). If (R) guarantees (\|f(x) - q^{-1}(L(x))\| \le \varepsilon_{\text{LUT}}) on its domain, then the integer-space kernel using (L) yields at most (\varepsilon_{\text{LUT}}) local real-space discrepancy per evaluation (before downstream scaling). Proof. Immediate from definition of (L) and the fixed interpolation rule. ∎ § 5.5 Reproducibility contract (numeric) @@ -425,7 +446,7 @@ Proof. 1. Binding of bytes to semantics. By A1, the node’s attrs and Q(Θ_v) are encoded injectively within (h_v^{\text{base}}). By T1, any change to these bytes (including LUT tables and rounding policy flags) yields a different base hash and hence a different node commitment. Therefore the node commitment (C(v)) fixes the exact integer kernel semantics. 2. Determinism of integer kernels. Each kernel in §5.3 is a finite composition of (\mathbb Z) addition/multiplication, max, and table lookups with declared tie-breaking and scaling rules (e.g., shift-right with “ties-to-even”). These operations are deterministic over integers. If engineering mode (int64-sat) is used, the saturation behavior is byte-committed; in the sound verifier (big-int) there is no overflow. Hence, given the same integer inputs and the same attributes, every conforming implementation produces the same integer output tensor. 3. Byte-exact reproducibility. Because the proof carries the exact integer inputs/parameters (or references them via the committed model), and the verifier recomputes the same deterministic kernel on those integers, the output integer tensor (Z_v^*) equals the claimed (Z_v) if and only if the claimed computation is honest. There is no dependency on floating-point hardware or library versions. -4. Mapping to reals for inequalities. Whenever an inequality is to be checked in real space (e.g., (|z_{\text{full}} - z_S|p \le \varepsilon |z{\text{full}}|p) in Part 3), both sides are computed from the same integers using the public (\Delta) (and any LUT residual bounds (\varepsilon{\text{LUT}}) explicitly added where relevant). Triangle inequality yields a bound that is explicitly the sum of local quantization/LUT errors dictated in the manifest; there is no hidden platform jitter. +4. Mapping to reals for inequalities. Whenever an inequality is to be checked in real space (e.g., (\|z_{\text{full}} - z_S\|p \le \varepsilon \|z{\text{full}}\|p) in Part 3), both sides are computed from the same integers using the public (\Delta) (and any LUT residual bounds (\varepsilon{\text{LUT}}) explicitly added where relevant). Triangle inequality yields a bound that is explicitly the sum of local quantization/LUT errors dictated in the manifest; there is no hidden platform jitter. Therefore, local numeric verification is bit-exact in (\mathbb Z), and any real-space statement derived from it is reproducible with declared error envelopes only. ∎ § 5.6 Practical catalog: where ε-proofs will apply later @@ -440,24 +461,26 @@ We pre-classify ops by whether they expose affine preactivation frontiers (eligi ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We will ship a Python 3.12 reference that implements these kernels and exposes a small surface area the proofs can call. Function signatures (types elided for brevity): -```python -# Quantization and encoding (A1, A2) -Q(tensor) -> IntTensor -dequant(IntTensor) -> FloatTensor # only for display/inequalities -enc_tensor_q(IntTensor) -> bytes -enc_attrs(dict) -> bytes -# Integer kernels (reference big-int, with optional int64-sat mode) -gemm_q(W_q, A_q) -> IntTensor -conv2d_q(W_q, A_q, stride, pad, dil) -> IntTensor -bias_add_q(Z_q, B_q) -> IntTensor -add_q(X_q, Y_q) -> IntTensor -concat_q(tensors, axis) -> IntTensor -layernorm_q(A_q, gamma_q, beta_q, eps_bytes, luts) -> IntTensor -gelu_q(A_q, luts) -> IntTensor -softmax_q(A_q, luts, div_policy_bytes) -> IntTensor -# Proof helpers -recompute_node_q(node_spec, parent_acts_q) -> IntTensor -``` + +.. code-block:: python + + # Quantization and encoding (A1, A2) + Q(tensor) -> IntTensor + dequant(IntTensor) -> FloatTensor # only for display/inequalities + enc_tensor_q(IntTensor) -> bytes + enc_attrs(dict) -> bytes + # Integer kernels (reference big-int, with optional int64-sat mode) + gemm_q(W_q, A_q) -> IntTensor + conv2d_q(W_q, A_q, stride, pad, dil) -> IntTensor + bias_add_q(Z_q, B_q) -> IntTensor + add_q(X_q, Y_q) -> IntTensor + concat_q(tensors, axis) -> IntTensor + layernorm_q(A_q, gamma_q, beta_q, eps_bytes, luts) -> IntTensor + gelu_q(A_q, luts) -> IntTensor + softmax_q(A_q, luts, div_policy_bytes) -> IntTensor + # Proof helpers + recompute_node_q(node_spec, parent_acts_q) -> IntTensor + All LUTs and policy bytes are passed explicitly and are also present in the node’s committed attrs (A1), ensuring T1 applies. § 5.8 Corner-case policies (fully specified) @@ -496,22 +519,28 @@ Let (M=(G,\Theta,\mathcal O)) be the committed model (Part 1). For node (v) with - (Q(\Theta_v)) are v’s quantized parameters (integers) committed via A1/A3. - (A_u = Q(a_u(x)) \in \mathbb Z^{d_u}) are quantized activations at parents (u) on the specific input (x). - Affine preactivation node (v) means its committed op semantics produce an integer preactivation vector (Z_v) as: - [ - Z_v ;=; \Big(\sum_{i=1}^{k} \mathrm{lin}i\big(W{i\to v}, A_{u_i}\big)\Big) ;+; B_v, - ] + + :: + + Z_v ;=; \Big(\sum_{i=1}^{k} \mathrm{lin}i\big(W{i\to v}, A_{u_i}\big)\Big) ;+; B_v, + where each (\mathrm{lin}_i) is a declared integer-linear kernel (e.g., gemm_q, conv2d_q, elementwise mul+add), and (B_v) is an integer bias term. Shapes and broadcasting rules are fully specified in attrs (A1). Non-affine ops (softmax, GELU, LN, etc.) are outside v7-Local’s quantitative scope; anchor proofs one step upstream at their affine inputs (Part 2 §5.6). Define the per-parent integer contribution tensor: -[ -C_i ;=; \mathrm{lin}i!\big(W{i\to v}, A_{u_i}\big)\quad\in\mathbb Z^{d_v}, -\quad Z_v = \Big(\sum_{i=1}^k C_i\Big) + B_v . -] + +:: + + C_i ;=; \mathrm{lin}i!\big(W{i\to v}, A_{u_i}\big)\quad\in\mathbb Z^{d_v}, + \quad Z_v = \Big(\sum_{i=1}^k C_i\Big) + B_v . + Let (S\subseteq{1,\dots,k}) be the set of parents the explainer claims suffice up to tolerance (\varepsilon). Let (C_S=\sum_{i\in S}C_i) and (Z^{\mathrm{partial}}_v = C_S+B_v). We will certify an ε-complete local explanation if -[ -|,Z_v - Z^{\mathrm{partial}}_v,|_p ;\le; \varepsilon,|,Z_v,|_p, -\tag{6.1} -] -where (|\cdot|_p) is an integer-induced norm (see §6.5), all computed exactly in integer space using the Part 2 kernels (Theorem T4). + +:: + + |,Z_v - Z^{\mathrm{partial}}_v,|_p ;\le; \varepsilon,|,Z_v,|_p, + \tag{6.1} + +where (\|\cdot\|_p) is an integer-induced norm (see §6.5), all computed exactly in integer space using the Part 2 kernels (Theorem T4). § 6.2 What must be revealed (and why) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -535,19 +564,19 @@ Verifier computation (integer space, see Part 2): 2. For each (i), recompute (C_i=\mathrm{lin}i(W{i\to v}, A_{u_i})) using integer kernels. 3. Compute (Z_v = (\sum_i C_i)+B_v) and (Z^{\mathrm{partial}}v = (\sum{i\in S} C_i)+B_v). 4. Compute integer residual (R_v = Z_v - Z^{\mathrm{partial}}v = \sum{i\notin S} C_i). -5. Evaluate (|R_v|_p) and (|Z_v|_p) in integer-induced norm; accept iff (6.1) holds. +5. Evaluate (\|R_v\|_p) and (\|Z_v\|_p) in integer-induced norm; accept iff (6.1) holds. 6. (Only if a real-space statement must be displayed): dequantize both sides with (\Delta) (and add any LUT envelopes if any existed upstream of this preact; typically none at pure linear preacts). Security intuition: The prover cannot shrink (R_v) without lying about some (A_{u_i}) or (W_{i\to v}); but those are either disclosed integers checked by deterministic kernels (A2/T4) or committed parameters bound by T1/T2. There is no place to inject a trusted scalar/vector. § 6.4 Theorem T5 (v7-Local) — Sound ε-Completeness at Affine Preactivations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Statement. For an affine preactivation node (v) on input (x), the protocol in §6.3 is sound under A1–A3: if the verifier accepts, then the omitted integer contribution (R_v) computed from the committed (W_{i\to v}) and the disclosed parent integers (A_{u_i}) satisfies (6.1). Any prover that causes acceptance while (|R_v|_p > \varepsilon |Z_v|_p) must either (i) falsify the Merkle structure (hash collision) or (ii) falsify the integer recomputation (contradicting T4) or (iii) alter committed parameters (second-preimage on H). +Statement. For an affine preactivation node (v) on input (x), the protocol in §6.3 is sound under A1–A3: if the verifier accepts, then the omitted integer contribution (R_v) computed from the committed (W_{i\to v}) and the disclosed parent integers (A_{u_i}) satisfies (6.1). Any prover that causes acceptance while (\|R_v\|_p > \varepsilon \|Z_v\|_p) must either (i) falsify the Merkle structure (hash collision) or (ii) falsify the integer recomputation (contradicting T4) or (iii) alter committed parameters (second-preimage on H). Proof (long-form). 1. Binding of structure and parameters. By T2 (completeness-binding), the arity (k) and the ordered parent list for (v) are fixed by the node commitment (C(v)). By T1, the base hash (h_v^{\text{base}}) binds the op type/version, attrs (including kernel policies), and the quantized parameters (Q(\Theta_v)). Hence any deviation in parent set/order, kernel semantics, or weight bytes requires breaking H. 2. Determinism of numeric recomputation. Given the disclosed integer parent activations ({A_{u_i}}) and the committed integer parameters, the verifier computes each (C_i) via the declared integer kernels (Part 2 §5.3). By T4, these kernels are deterministic over (\mathbb Z); thus the resulting (C_i), (Z_v), and (Z^{\mathrm{partial}}_v) are bit-exact integers. The prover cannot influence these outputs except by changing disclosed inputs/weights or structure, which are all checked. -3. Residual exactness. The omitted residual (R_v = Z_v - Z^{\mathrm{partial}}v) equals (\sum{i\notin S} C_i) by construction; no hidden terms exist because all parents are revealed and all contributions are recomputed. Therefore (|R_v|_p) and (|Z_v|_p) are integer-induced norms of exact integers. -4. Acceptance implies inequality. The verifier explicitly checks (6.1) on these integers. Acceptance means (6.1) held numerically. If in reality (|R_v|_p > \varepsilon |Z_v|_p), acceptance would contradict step (2)’s bit-exact recomputation unless H is broken. Hence a cheating prover must break the hash or the integer recomputation lemmas—both assumed infeasible. +3. Residual exactness. The omitted residual (R_v = Z_v - Z^{\mathrm{partial}}v) equals (\sum{i\notin S} C_i) by construction; no hidden terms exist because all parents are revealed and all contributions are recomputed. Therefore (\|R_v\|_p) and (\|Z_v\|_p) are integer-induced norms of exact integers. +4. Acceptance implies inequality. The verifier explicitly checks (6.1) on these integers. Acceptance means (6.1) held numerically. If in reality (\|R_v\|_p > \varepsilon \|Z_v\|_p), acceptance would contradict step (2)’s bit-exact recomputation unless H is broken. Hence a cheating prover must break the hash or the integer recomputation lemmas—both assumed infeasible. 5. Mapping to reals (if displayed). If the statement is presented in real space, the verifier applies (q^{-1}) to both sides (and adds any LUT error envelopes if applicable; at pure preactivation none are needed). Since both sides scale by the same (\Delta) and any LUT residuals are explicit and bounded, the inequality remains valid (up to the declared envelopes), preserving soundness. ∎ Corollary (No trusted values). Unlike v6/v6.6, v7-Local relies on no prover-supplied scalar or output vector for omitted mass. Every quantity is re-derived from committed parameters and disclosed integer parent activations via deterministic kernels. ∎ @@ -556,7 +585,7 @@ Corollary (No trusted values). Unlike v6/v6.6, v7-Local relies on no prover-supp ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Norms supported. Any integer-induced norm definable over (\mathbb Z^{d_v}): (L_1), (L_2) (via exact integer square-sum; compare (L_2^2) to avoid sqrt), (L_\infty). Default: (L_1), because it composes most transparently across dimensions and avoids square-root rationalities. -Attribution granularity. The “parent contribution” (C_i) is a tensor. The protocol does not require per-feature scalars (which vary across ops); it only requires recomputing (C_i) via the node’s linear kernel. If desired, a manuscript can present per-feature magnitudes (|C_i|_p), but the acceptance check is on the residual (R_v) vs (Z_v). +Attribution granularity. The “parent contribution” (C_i) is a tensor. The protocol does not require per-feature scalars (which vary across ops); it only requires recomputing (C_i) via the node’s linear kernel. If desired, a manuscript can present per-feature magnitudes (\|C_i\|_p), but the acceptance check is on the residual (R_v) vs (Z_v). Signed vs magnitude. The core inequality uses magnitudes (norms). If signed influence is needed for exposition, it can be derived post-verification from the same integers. § 6.6 Neutral-element masking & baseline policy (for partial recompute) @@ -602,56 +631,57 @@ Steps: 2. Load op attrs and parameter blocks; validate against committed hashes (T1). 3. For each (i) in (1..k): compute (C_i = \mathrm{lin}i(W{i\to v}, A_{u_i})) in (\mathbb Z) (T4). 4. Aggregate: (Z_v = (\sum_i C_i)+B_v); (Z^{\mathrm{partial}}v = (\sum{i\in S}C_i)+B_v). -5. Compute (R_v = Z_v - Z^{\mathrm{partial}}_v); evaluate (|R_v|_p), (|Z_v|_p) (integer (L_p)). -6. Accept iff (|R_v|_p \le \varepsilon |Z_v|_p). Else reject with a precise reason ("epsilon_violation", "structure_mismatch", "param_mismatch", "numeric_mismatch"). +5. Compute (R_v = Z_v - Z^{\mathrm{partial}}_v); evaluate (\|R_v\|_p), (\|Z_v\|_p) (integer (L_p)). +6. Accept iff (\|R_v\|_p \le \varepsilon \|Z_v\|_p). Else reject with a precise reason ("epsilon_violation", "structure_mismatch", "param_mismatch", "numeric_mismatch"). § 6.9.2 Reference pseudo-code (integer-exact) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -```python -def verify_eps_affine(M_root, node_v_id, π): - # 1) Structure - if not verify_merkle_paths(M_root, π.structure, node_v_id): - return False, "structure_mismatch" - parents = π.structure.ordered_parents(node_v_id) # [u1,...,uk] - # 2) Params & attrs (bind to committed bytes) - attrs, B_v, W_blocks = π.params.attrs, π.params.bias_q, π.params.W_blocks - if not attrs_hash_matches_commit(node_v_id, attrs): - return False, "param_mismatch" - if not weights_blocks_match_commit(node_v_id, W_blocks): - return False, "param_mismatch" - # 3) Disclosed integer parent activations (all parents) - A = {} - for i, u in enumerate(parents, start=1): - if u not in π.activations: - return False, "missing_parent_activation" - A[i] = π.activations[u] # IntTensor; exact integers - # 4) Recompute integer contributions C_i - C = [] - for i, u in enumerate(parents, start=1): - W_i = materialize_kernel_weights(W_blocks, i, attrs) - C_i = apply_linear_kernel_q(W_i, A[i], attrs) # big-int exact - C.append(C_i) - # 5) Aggregate Z_full and Z_partial - Z_full = sum_tensors_q(C) + B_v - S = set(π.statement.S) - Z_part = sum_tensors_q([C[i-1] for i in S]) + B_v - # 6) Residual and inequality - R = Z_full - Z_part - p = π.statement.p or 1 - eps = π.statement.eps - num = norm_q(R, p) # integer-induced Lp - den = norm_q(Z_full, p) - # Both integers; compare as rationals to avoid float - if den == 0: - # define policy: zero-output nodes accept only if num==0 - return (num == 0, "zero_output_ok" if num == 0 else "epsilon_violation") - # Check num <= eps * den in rationals - if rational_leq(num, eps, den): # i.e., num/den <= eps - return True, "ok" - else: - return False, "epsilon_violation" -``` +.. code-block:: python + + def verify_eps_affine(M_root, node_v_id, π): + # 1) Structure + if not verify_merkle_paths(M_root, π.structure, node_v_id): + return False, "structure_mismatch" + parents = π.structure.ordered_parents(node_v_id) # [u1,...,uk] + # 2) Params & attrs (bind to committed bytes) + attrs, B_v, W_blocks = π.params.attrs, π.params.bias_q, π.params.W_blocks + if not attrs_hash_matches_commit(node_v_id, attrs): + return False, "param_mismatch" + if not weights_blocks_match_commit(node_v_id, W_blocks): + return False, "param_mismatch" + # 3) Disclosed integer parent activations (all parents) + A = {} + for i, u in enumerate(parents, start=1): + if u not in π.activations: + return False, "missing_parent_activation" + A[i] = π.activations[u] # IntTensor; exact integers + # 4) Recompute integer contributions C_i + C = [] + for i, u in enumerate(parents, start=1): + W_i = materialize_kernel_weights(W_blocks, i, attrs) + C_i = apply_linear_kernel_q(W_i, A[i], attrs) # big-int exact + C.append(C_i) + # 5) Aggregate Z_full and Z_partial + Z_full = sum_tensors_q(C) + B_v + S = set(π.statement.S) + Z_part = sum_tensors_q([C[i-1] for i in S]) + B_v + # 6) Residual and inequality + R = Z_full - Z_part + p = π.statement.p or 1 + eps = π.statement.eps + num = norm_q(R, p) # integer-induced Lp + den = norm_q(Z_full, p) + # Both integers; compare as rationals to avoid float + if den == 0: + # define policy: zero-output nodes accept only if num==0 + return (num == 0, "zero_output_ok" if num == 0 else "epsilon_violation") + # Check num <= eps * den in rationals + if rational_leq(num, eps, den): # i.e., num/den <= eps + return True, "ok" + else: + return False, "epsilon_violation" + Implementation notes. - apply_linear_kernel_q dispatches to gemm_q, conv2d_q, etc., based on attrs (Part 2). - rational_leq(num, eps, den) compares exact integers with a rational eps represented in canonical TLV (avoid floats). @@ -696,7 +726,7 @@ Disclosure: RCA is non-normative. v7-Local’s sound claims rely only on full lo ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - Prefer (L_1) for clarity; use (L_\infty) to guard worst-case channels; use (L_2) when energy-style arguments are desired. -- If epsilon_violation, report: (|R_v|_p), (|Z_v|_p), (\varepsilon) threshold, list of largest omitted contributors (by (|C_i|_p)) to guide next S selection. +- If epsilon_violation, report: (\|R_v\|_p), (\|Z_v\|_p), (\varepsilon) threshold, list of largest omitted contributors (by (\|C_i\|_p)) to guide next S selection. - If param_mismatch, display the first diverging byte range and the expected committed hash. - If structure_mismatch, show the expected ordered parent commitments vs the proof’s paths. @@ -739,66 +769,68 @@ Determinism: All verifier-critical math runs in Python big-int or Torch integer § 7.2 Public API surface ~~~~~~~~~~~~~~~~~~~~~~~~~ -```python -# merkleagi/__init__.py (public facade) -# Build & commit -def build_merkle_dag(model_spec: dict, delta: float, kernels: dict) -> dict: - """Return {'root': bytes32, 'nodes': {...}, 'manifest': {...}}""" -# Path proofs (structure) -def prove_path(repo: dict, node_id: str) -> dict: - """Return Merkle authentication for node_id with ordered parents.""" -# ε-proofs at affine preactivations (v7-Local) -def prove_eps_affine(repo: dict, node_id: str, x_binding: dict, - subset_S: list[int], p: str, eps: str) -> dict: - """Return full local revelation proof for node_id on input binding x.""" -# Verifiers -def verify_root(root: bytes, manifest: dict) -> tuple[bool, str]: - """Check manifest consistency & root commitment.""" -def verify_path(root: bytes, proof: dict) -> tuple[bool, str]: - """Completeness-binding and membership checks.""" -def verify_eps_affine(root: bytes, node_id: str, proof: dict) -> tuple[bool, str]: - """Integer-exact ε-check per Part 3.""" -# Utilities -def block_hash_matrix(W: "torch.Tensor|np.ndarray", block: int = 4096) -> dict: ... -def dedup_sibling_hashes(proof: dict) -> dict: ... -def write_manifest(manifest: dict, path: str) -> None: ... -def load_manifest(path: str) -> dict: ... -``` +.. code-block:: python + + # merkleagi/__init__.py (public facade) + # Build & commit + def build_merkle_dag(model_spec: dict, delta: float, kernels: dict) -> dict: + """Return {'root': bytes32, 'nodes': {...}, 'manifest': {...}}""" + # Path proofs (structure) + def prove_path(repo: dict, node_id: str) -> dict: + """Return Merkle authentication for node_id with ordered parents.""" + # ε-proofs at affine preactivations (v7-Local) + def prove_eps_affine(repo: dict, node_id: str, x_binding: dict, + subset_S: list[int], p: str, eps: str) -> dict: + """Return full local revelation proof for node_id on input binding x.""" + # Verifiers + def verify_root(root: bytes, manifest: dict) -> tuple[bool, str]: + """Check manifest consistency & root commitment.""" + def verify_path(root: bytes, proof: dict) -> tuple[bool, str]: + """Completeness-binding and membership checks.""" + def verify_eps_affine(root: bytes, node_id: str, proof: dict) -> tuple[bool, str]: + """Integer-exact ε-check per Part 3.""" + # Utilities + def block_hash_matrix(W: "torch.Tensor|np.ndarray", block: int = 4096) -> dict: ... + def dedup_sibling_hashes(proof: dict) -> dict: ... + def write_manifest(manifest: dict, path: str) -> None: ... + def load_manifest(path: str) -> dict: ... + § 7.3 Canonical encoding (A1) — TLV, length-prefix, domain separation ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -```python -# merkleagi/encoding.py -from struct import pack -from typing import Iterable -def tlv(tag: int, payload: bytes) -> bytes: - # 1 byte tag, 4 bytes LE length, then payload - return bytes([tag]) + pack(" bytes: - return int(n).to_bytes(bytelen, "little", signed=False) -def enc_bytes(tag: int, b: bytes) -> bytes: - return tlv(tag, b) -def enc_str(tag: int, s: str) -> bytes: - return tlv(tag, s.encode("utf-8")) -def enc_seq(tag: int, seq: Iterable[bytes]) -> bytes: - body = b"".join([tlv(0xEE, e) for e in seq]) # 0xEE = element - return tlv(tag, body) -# Domain tags -T_BASE = 0x10 # node base: op/version/attrs/params -T_NODE = 0x11 # node commit with children -T_LEAF = 0x12 -T_ROOT = 0x13 -T_CHILD = 0x14 # length-prefix child hash -T_ATTRS = 0x21 -T_PARAMS = 0x22 -T_BIAS = 0x23 -T_ID = 0x24 -T_ARITY = 0x25 -T_ORDER = 0x26 -T_ACT = 0x30 # activation record (optional, RCA only) -T_LUT = 0x31 # deterministic LUT ID bytes -``` +.. code-block:: python + + # merkleagi/encoding.py + from struct import pack + from typing import Iterable + def tlv(tag: int, payload: bytes) -> bytes: + # 1 byte tag, 4 bytes LE length, then payload + return bytes([tag]) + pack(" bytes: + return int(n).to_bytes(bytelen, "little", signed=False) + def enc_bytes(tag: int, b: bytes) -> bytes: + return tlv(tag, b) + def enc_str(tag: int, s: str) -> bytes: + return tlv(tag, s.encode("utf-8")) + def enc_seq(tag: int, seq: Iterable[bytes]) -> bytes: + body = b"".join([tlv(0xEE, e) for e in seq]) # 0xEE = element + return tlv(tag, body) + # Domain tags + T_BASE = 0x10 # node base: op/version/attrs/params + T_NODE = 0x11 # node commit with children + T_LEAF = 0x12 + T_ROOT = 0x13 + T_CHILD = 0x14 # length-prefix child hash + T_ATTRS = 0x21 + T_PARAMS = 0x22 + T_BIAS = 0x23 + T_ID = 0x24 + T_ARITY = 0x25 + T_ORDER = 0x26 + T_ACT = 0x30 # activation record (optional, RCA only) + T_LUT = 0x31 # deterministic LUT ID bytes + Notes. - Every complex record is a TLV of other TLVs (enc_seq). - Length-prefix: children are prepended by a 4-byte length inside T_CHILD to block concatenation ambiguity. @@ -807,129 +839,132 @@ Notes. § 7.4 Hashing (A3) — SHA-256 wrapper and commit builders ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -```python -# merkleagi/hash.py -import hashlib -from .encoding import * -HASH_LEN = 32 -def sha256(b: bytes) -> bytes: - return hashlib.sha256(b).digest() -def commit_base(node_id: bytes, attrs_tlv: bytes, params_tlv: bytes) -> bytes: - pre = enc_seq(T_BASE, [tlv(0x01, node_id), attrs_tlv, params_tlv]) - return sha256(pre) -def commit_leaf(node_id: bytes, h_base: bytes) -> bytes: - pre = enc_seq(T_LEAF, [tlv(0x01, node_id), tlv(0x02, h_base)]) - return sha256(pre) -def commit_node(node_id: bytes, k: int, h_base: bytes, child_hashes: list[bytes]) -> bytes: - children = [tlv(T_CHILD, enc_uint_le(HASH_LEN,4) + h) for h in child_hashes] - pre = enc_seq(T_NODE, [tlv(0x01, node_id), tlv(0x02, enc_uint_le(k,4)), tlv(0x03, h_base)] + children) - return sha256(pre) -def commit_root(outputs: list[bytes]) -> bytes: - pre = enc_seq(T_ROOT, [tlv(0x01, enc_uint_le(len(outputs),4))] + - [tlv(T_CHILD, enc_uint_le(HASH_LEN,4) + h) for h in outputs]) - return sha256(pre) -``` +.. code-block:: python + + # merkleagi/hash.py + import hashlib + from .encoding import * + HASH_LEN = 32 + def sha256(b: bytes) -> bytes: + return hashlib.sha256(b).digest() + def commit_base(node_id: bytes, attrs_tlv: bytes, params_tlv: bytes) -> bytes: + pre = enc_seq(T_BASE, [tlv(0x01, node_id), attrs_tlv, params_tlv]) + return sha256(pre) + def commit_leaf(node_id: bytes, h_base: bytes) -> bytes: + pre = enc_seq(T_LEAF, [tlv(0x01, node_id), tlv(0x02, h_base)]) + return sha256(pre) + def commit_node(node_id: bytes, k: int, h_base: bytes, child_hashes: list[bytes]) -> bytes: + children = [tlv(T_CHILD, enc_uint_le(HASH_LEN,4) + h) for h in child_hashes] + pre = enc_seq(T_NODE, [tlv(0x01, node_id), tlv(0x02, enc_uint_le(k,4)), tlv(0x03, h_base)] + children) + return sha256(pre) + def commit_root(outputs: list[bytes]) -> bytes: + pre = enc_seq(T_ROOT, [tlv(0x01, enc_uint_le(len(outputs),4))] + + [tlv(T_CHILD, enc_uint_le(HASH_LEN,4) + h) for h in outputs]) + return sha256(pre) + § 7.5 Quantization & kernels (A2) — integer exactness and LUT IDs ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -```python -# merkleagi/quant.py -import math -import torch -from .encoding import tlv, T_LUT -class QuantConfig: - def __init__(self, delta: float): - self.delta = float(delta) -def q_round(x: torch.Tensor, Δ: float) -> torch.Tensor: - # Round-to-nearest, ties-to-even via torch.round; store as integers by dividing by Δ - return torch.round(x / Δ).to(torch.int64) -def q_deq(q: torch.Tensor, Δ: float) -> torch.Tensor: - return (q.to(torch.float64) * Δ) -def canonical_bytes_from_int_tensor(q: torch.Tensor) -> bytes: - # C order, little-endian int64 - return q.contiguous().cpu().numpy().tobytes(order="C") -# Deterministic LUT registry (for non-linear ops outside ε scope; used in Part 2) -LUT_REGISTRY = { - # 'gelu_v1': bytes_id, 'rsqrt_v1': bytes_id, ... -} -def lut_id_tlv(name: str) -> bytes: - return tlv(T_LUT, name.encode("utf-8")) -# Integer linear kernels (affine preactivation frontiers) -def gemm_q(W_q: torch.Tensor, A_q: torch.Tensor, attrs: dict) -> torch.Tensor: - # W_q: [m,k] int64; A_q: [k] or [k,b]; returns int64 [m] or [m,b] - # Use big-int semantics: promote to 128-bit accumulation via Python int if needed - return (W_q @ A_q) # Torch int64 matmul is exact mod 2^64; to avoid wrap, enforce range checks upstream or use chunking. -def conv2d_q(W_q, A_q, attrs: dict) -> torch.Tensor: - # Minimal spec: use unfold + gemm_q chunks; exactness relies on range checks/tiling to avoid overflow. - # Reference implementation can tile to guarantee no wrap within int64; verifier MUST range-check or fallback to Python big-int loops if needed. - raise NotImplementedError("Reference conv2d_q provided in Appendix B (tiling big-int safe)") -``` +.. code-block:: python + + # merkleagi/quant.py + import math + import torch + from .encoding import tlv, T_LUT + class QuantConfig: + def __init__(self, delta: float): + self.delta = float(delta) + def q_round(x: torch.Tensor, Δ: float) -> torch.Tensor: + # Round-to-nearest, ties-to-even via torch.round; store as integers by dividing by Δ + return torch.round(x / Δ).to(torch.int64) + def q_deq(q: torch.Tensor, Δ: float) -> torch.Tensor: + return (q.to(torch.float64) * Δ) + def canonical_bytes_from_int_tensor(q: torch.Tensor) -> bytes: + # C order, little-endian int64 + return q.contiguous().cpu().numpy().tobytes(order="C") + # Deterministic LUT registry (for non-linear ops outside ε scope; used in Part 2) + LUT_REGISTRY = { + # 'gelu_v1': bytes_id, 'rsqrt_v1': bytes_id, ... + } + def lut_id_tlv(name: str) -> bytes: + return tlv(T_LUT, name.encode("utf-8")) + # Integer linear kernels (affine preactivation frontiers) + def gemm_q(W_q: torch.Tensor, A_q: torch.Tensor, attrs: dict) -> torch.Tensor: + # W_q: [m,k] int64; A_q: [k] or [k,b]; returns int64 [m] or [m,b] + # Use big-int semantics: promote to 128-bit accumulation via Python int if needed + return (W_q @ A_q) # Torch int64 matmul is exact mod 2^64; to avoid wrap, enforce range checks upstream or use chunking. + def conv2d_q(W_q, A_q, attrs: dict) -> torch.Tensor: + # Minimal spec: use unfold + gemm_q chunks; exactness relies on range checks/tiling to avoid overflow. + # Reference implementation can tile to guarantee no wrap within int64; verifier MUST range-check or fallback to Python big-int loops if needed. + raise NotImplementedError("Reference conv2d_q provided in Appendix B (tiling big-int safe)") + Engineering note (exactness): - The reference verifier MUST avoid silent int64 wrap. For GEMM, either range-check or process in tiles with Python int accumulation (slower but exact). The optimized path is permitted only with a no-saturation certificate in the proof (a TLV that upper-bounds intermediate sums given shapes and max magnitudes). The spec includes the safe fallback; Appendix B ships both versions. § 7.6 DAG & commitments — node model, parents, block hashing, dedup ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -```python -# merkleagi/dag.py -from dataclasses import dataclass, field -from typing import Optional -from .hash import commit_base, commit_leaf, commit_node, commit_root -from .encoding import * -@dataclass -class NodeSpec: - nid: str - op: str # e.g., "linear_preact" - version: str # kernel version - attrs: dict # shapes, broadcasting, kernel policy - params_q: dict # {'W_blocks': [bytes32...], 'B': bytes of int tensor} - parents: list[str] # ordered parent node ids - is_commutative: bool = False -@dataclass -class Repo: - nodes: dict[str, NodeSpec] = field(default_factory=dict) - outputs: list[str] = field(default_factory=list) - commitments: dict[str, bytes] = field(default_factory=dict) - base_hash: dict[str, bytes] = field(default_factory=dict) - root: Optional[bytes] = None -def encode_attrs(attrs: dict) -> bytes: - # Serialize attrs under T_ATTRS: deterministic key order - items = [] - for k in sorted(attrs.keys()): - v = attrs[k] - items.append(tlv(0xA0, tlv(0xA1, k.encode()) + tlv(0xA2, str(v).encode()))) - return enc_seq(T_ATTRS, items) -def encode_params(params_q: dict) -> bytes: - # W_blocks as sequence of child hashes; B as raw integer bytes - seq = [] - if "W_blocks" in params_q: - seq.append(enc_seq(0xB0, [tlv(0xB1, b) for b in params_q["W_blocks"]])) - if "B" in params_q: - seq.append(tlv(T_BIAS, params_q["B"])) - return enc_seq(T_PARAMS, seq) -def compute_commits(repo: Repo) -> None: - # post-order over DAG (assume acyclic and topo-sorted elsewhere) - for nid, ns in repo.nodes.items(): - node_id_bytes = ns.nid.encode("utf-8") - h_base = commit_base(node_id_bytes, encode_attrs(ns.attrs), encode_params(ns.params_q)) - repo.base_hash[nid] = h_base - # now parent/child composition - for nid, ns in repo.nodes.items(): - node_id_bytes = ns.nid.encode("utf-8") - if len(ns.parents) == 0: - h = commit_leaf(node_id_bytes, repo.base_hash[nid]) - else: - child_hashes = [repo.commitments[p] for p in ordered_parents(repo, ns)] - h = commit_node(node_id_bytes, len(ns.parents), repo.base_hash[nid], child_hashes) - repo.commitments[nid] = h - repo.root = commit_root([repo.commitments[o] for o in repo.outputs]) -def ordered_parents(repo: Repo, ns: NodeSpec) -> list[str]: - if ns.is_commutative: - # sort by child commitment bytes (lexicographic) - return sorted(ns.parents, key=lambda p: repo.commitments[p]) - return ns.parents -``` +.. code-block:: python + + # merkleagi/dag.py + from dataclasses import dataclass, field + from typing import Optional + from .hash import commit_base, commit_leaf, commit_node, commit_root + from .encoding import * + @dataclass + class NodeSpec: + nid: str + op: str # e.g., "linear_preact" + version: str # kernel version + attrs: dict # shapes, broadcasting, kernel policy + params_q: dict # {'W_blocks': [bytes32...], 'B': bytes of int tensor} + parents: list[str] # ordered parent node ids + is_commutative: bool = False + @dataclass + class Repo: + nodes: dict[str, NodeSpec] = field(default_factory=dict) + outputs: list[str] = field(default_factory=list) + commitments: dict[str, bytes] = field(default_factory=dict) + base_hash: dict[str, bytes] = field(default_factory=dict) + root: Optional[bytes] = None + def encode_attrs(attrs: dict) -> bytes: + # Serialize attrs under T_ATTRS: deterministic key order + items = [] + for k in sorted(attrs.keys()): + v = attrs[k] + items.append(tlv(0xA0, tlv(0xA1, k.encode()) + tlv(0xA2, str(v).encode()))) + return enc_seq(T_ATTRS, items) + def encode_params(params_q: dict) -> bytes: + # W_blocks as sequence of child hashes; B as raw integer bytes + seq = [] + if "W_blocks" in params_q: + seq.append(enc_seq(0xB0, [tlv(0xB1, b) for b in params_q["W_blocks"]])) + if "B" in params_q: + seq.append(tlv(T_BIAS, params_q["B"])) + return enc_seq(T_PARAMS, seq) + def compute_commits(repo: Repo) -> None: + # post-order over DAG (assume acyclic and topo-sorted elsewhere) + for nid, ns in repo.nodes.items(): + node_id_bytes = ns.nid.encode("utf-8") + h_base = commit_base(node_id_bytes, encode_attrs(ns.attrs), encode_params(ns.params_q)) + repo.base_hash[nid] = h_base + # now parent/child composition + for nid, ns in repo.nodes.items(): + node_id_bytes = ns.nid.encode("utf-8") + if len(ns.parents) == 0: + h = commit_leaf(node_id_bytes, repo.base_hash[nid]) + else: + child_hashes = [repo.commitments[p] for p in ordered_parents(repo, ns)] + h = commit_node(node_id_bytes, len(ns.parents), repo.base_hash[nid], child_hashes) + repo.commitments[nid] = h + repo.root = commit_root([repo.commitments[o] for o in repo.outputs]) + def ordered_parents(repo: Repo, ns: NodeSpec) -> list[str]: + if ns.is_commutative: + # sort by child commitment bytes (lexicographic) + return sorted(ns.parents, key=lambda p: repo.commitments[p]) + return ns.parents + Block hashing. Large matrices are split into fixed-size blocks; each block is a leaf with its own commitment. The node’s params_q['W_blocks'] stores the hash list (order matters). Proofs reveal only relevant blocks. Appendix B contains the matrix tiling APIs and a no-wrap certificate generator. Deduplication. Proof objects carry sibling lists; dedup_sibling_hashes() prunes repeated siblings when the same sub-DAG appears multiple times along different paths. @@ -940,60 +975,62 @@ Deduplication. Proof objects carry sibling lists; dedup_sibling_hashes() prunes § 7.7.1 Path proof (structure only) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -```json -{ - "type": "path_proof/v1", - "node_id": "v", - "root": "", - "auth_chain": [ - { - "node_id": "v", - "base_hash": "", - "arity": 3, - "ordered_children": [ - {"hash":"", "position": 0}, - {"hash":"", "position": 1}, - {"hash":"", "position": 2} - ], - "siblings": [ - {"parent_id":"p1","side":"left","hashes":["", "..."]}, - {"parent_id":"p2","side":"right","hashes":["", "..."]} - ] - } - // ... up to root - ] -} -``` +.. code-block:: text + + { + "type": "path_proof/v1", + "node_id": "v", + "root": "", + "auth_chain": [ + { + "node_id": "v", + "base_hash": "", + "arity": 3, + "ordered_children": [ + {"hash":"", "position": 0}, + {"hash":"", "position": 1}, + {"hash":"", "position": 2} + ], + "siblings": [ + {"parent_id":"p1","side":"left","hashes":["", "..."]}, + {"parent_id":"p2","side":"right","hashes":["", "..."]} + ] + } + // ... up to root + ] + } + § 7.7.2 ε-proof at affine preactivation (v7-Local) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -```json -{ - "type": "eps_affine/v1", - "node_id": "v", - "root": "", - "statement": {"S":[1,5,9], "norm":"L1", "eps":"0.05"}, - "structure": { /* same shape as path_proof for v and each parent u_i */ }, - "attrs": { "op":"linear_preact", "version":"1.0", "shape":{"m":1024,"k":4096}, "policy":"gemm_q" }, - "params": { - "W_blocks": ["", "..."], // block hash list (order matters) - "B": "" // bias int tensor bytes - }, - "activations": { - "u1": "", // int tensor bytes for A_{u1} - "u2": "", - "...": "..." - }, - "block_payloads": { // disclosed blocks (subset) - "idx->bytes": { "0":"", "1":"", "...": "..." } - }, - "range_cert": { // optional no-saturation certificate - "max_abs_W": "12345", "max_abs_A": "8192", - "acc_limit": "9223372036854775807" - } -} -``` +.. code-block:: text + + { + "type": "eps_affine/v1", + "node_id": "v", + "root": "", + "statement": {"S":[1,5,9], "norm":"L1", "eps":"0.05"}, + "structure": { /* same shape as path_proof for v and each parent u_i */ }, + "attrs": { "op":"linear_preact", "version":"1.0", "shape":{"m":1024,"k":4096}, "policy":"gemm_q" }, + "params": { + "W_blocks": ["", "..."], // block hash list (order matters) + "B": "" // bias int tensor bytes + }, + "activations": { + "u1": "", // int tensor bytes for A_{u1} + "u2": "", + "...": "..." + }, + "block_payloads": { // disclosed blocks (subset) + "idx->bytes": { "0":"", "1":"", "...": "..." } + }, + "range_cert": { // optional no-saturation certificate + "max_abs_W": "12345", "max_abs_A": "8192", + "acc_limit": "9223372036854775807" + } + } + All byte arrays are little-endian int64-encoded tensor bytes with shape derivable from attrs. The verifier must check sizes and shapes. § 7.8 Prover algorithms @@ -1073,7 +1110,7 @@ No simulated metrics are asserted in this text; this is a procedural template. T - kernel_policy_mismatch: attrs.policy not in eligible catalog for v7-Local ε. - numeric_mismatch: kernel recompute inconsistency (append index + block id). - overflow_risk: int64 path selected without valid range_cert; retry big-int mode. -- epsilon_violation: include exact integers for (|R_v|_p), (|Z_v|_p), p, ε, and top omitted contributors. +- epsilon_violation: include exact integers for (\|R_v\|_p), (\|Z_v\|_p), p, ε, and top omitted contributors. § 7.12 Security & correctness checks integrated by default ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1087,26 +1124,27 @@ No simulated metrics are asserted in this text; this is a procedural template. T § 7.13 Reproducibility manifest (schema excerpt) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -```json -{ - "type": "manifest/v1", - "root": "", - "delta": "1e-6", - "env": {"python":"3.12.3","torch":"2.4.0","device":"cpu"}, - "lut_digests": {"gelu_v1":"","rsqrt_v1":""}, - "nodes": { - "v": { - "op":"linear_preact","version":"1.0", - "attrs": {"m":1024,"k":4096,"policy":"gemm_q"}, - "params":{"W_blocks":["", "..."], "B":""}, - "parents":["u1","u2"], "is_commutative": false, - "base_hash":"", "commit":"" - } - // ... - }, - "outputs": ["o1","o2"] -} -``` +.. code-block:: text + + { + "type": "manifest/v1", + "root": "", + "delta": "1e-6", + "env": {"python":"3.12.3","torch":"2.4.0","device":"cpu"}, + "lut_digests": {"gelu_v1":"","rsqrt_v1":""}, + "nodes": { + "v": { + "op":"linear_preact","version":"1.0", + "attrs": {"m":1024,"k":4096,"policy":"gemm_q"}, + "params":{"W_blocks":["", "..."], "B":""}, + "parents":["u1","u2"], "is_commutative": false, + "base_hash":"", "commit":"" + } + // ... + }, + "outputs": ["o1","o2"] + } + CLI helpers (scripts/reproduce.py): - --strict (default): v7-Local only; big-int kernels if no range cert. - --hybrid --rca K: adds RCA(K) spot-check (non-normative). @@ -1115,85 +1153,88 @@ CLI helpers (scripts/reproduce.py): § 7.14 CLI usage (contract) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -```bash -# Build and write manifest -python -m merkleagi.cli build --spec model.json --delta 1e-6 --out manifest.json -# Prove path -python -m merkleagi.cli prove-path --manifest manifest.json --node v > path_v.json -# Prove epsilon at affine preactivation v -python -m merkleagi.cli prove-eps --manifest manifest.json --node v - --input-hash deadbeef... --subset 1,5,9 --norm L1 --eps 0.05 - > eps_v.json -# Verify -python -m merkleagi.cli verify-root --manifest manifest.json -python -m merkleagi.cli verify-eps --manifest manifest.json --node v --proof eps_v.json --strict -``` +.. code-block:: bash + + # Build and write manifest + python -m merkleagi.cli build --spec model.json --delta 1e-6 --out manifest.json + # Prove path + python -m merkleagi.cli prove-path --manifest manifest.json --node v > path_v.json + # Prove epsilon at affine preactivation v + python -m merkleagi.cli prove-eps --manifest manifest.json --node v + --input-hash deadbeef... --subset 1,5,9 --norm L1 --eps 0.05 + > eps_v.json + # Verify + python -m merkleagi.cli verify-root --manifest manifest.json + python -m merkleagi.cli verify-eps --manifest manifest.json --node v --proof eps_v.json --strict + § 7.15 Reference code (concise core) — end-to-end wiring ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Note: Full, production-ready listings (including conv tiling, big-int GEMM, RCA, and CLI) are provided in Appendix B. Below is the concise core wiring the Parts 2–3 specifications into callable functions. -```python -# merkleagi/proofs.py (concise core) -from typing import Tuple -from .dag import Repo, compute_commits, ordered_parents -from .hash import sha256 -from .quant import gemm_q -from .encoding import * -def verify_path(root: bytes, proof: dict) -> Tuple[bool,str]: - # Replay Merkle chain; check ordered children and siblings up to 'root' - # (Full implementation in Appendix B) - ... -def attrs_hash_matches_commit(repo: Repo, nid: str, attrs_tlv: bytes, params_tlv: bytes) -> bool: - hb = repo.base_hash[nid] - return hb == sha256(enc_seq(T_BASE, [tlv(0x01, nid.encode()), attrs_tlv, params_tlv])) -def materialize_kernel_weights(repo: Repo, nid: str, params: dict, block_payloads: dict) -> "torch.Tensor": - # Resolve W from block hashes + provided payloads; check each payload digest - ... - return W_q -def apply_linear_kernel_q(W_q, A_q, attrs): - if attrs["policy"] == "gemm_q": - return gemm_q(W_q, A_q, attrs) - raise ValueError("Unsupported policy for affine preactivation") -def norm_q(q_tensor, p: str) -> int: - # Exact integer norms; return Python int (no float) - # L1: sum(abs), L2: sum(x^2) (compare squared values), Linf: max(abs) - ... - return int_val -def rational_leq(num: int, eps_str: str, den: int) -> bool: - # Compare num/den <= eps as integers (avoid float) - # eps_str is decimal; parse to (num_eps, den_eps) and compare num*den_eps <= den*num_eps - ... - return bool -def verify_eps_affine(root: bytes, node_id: str, proof: dict, repo: Repo) -> Tuple[bool,str]: - ok, msg = verify_path(root, proof.get("structure_v", proof.get("structure"))) - if not ok: return False, "structure_mismatch" - parents = proof["structure"]["ordered_parents"] # or rebuild from repo - attrs = proof["attrs"]; params = proof["params"] - attrs_tlv = encode_attrs(attrs) - params_tlv = encode_params(params) - if not attrs_hash_matches_commit(repo, node_id, attrs_tlv, params_tlv): - return False, "param_mismatch" - # Load activations (all parents) - A = { pid: decode_int_tensor_bytes(proof["activations"][pid], attrs) for pid in parents } - # Materialize W and B - W_q = materialize_kernel_weights(repo, node_id, params, proof.get("block_payloads", {})) - B_v = decode_int_tensor_bytes(params["B"], attrs) - # Compute C_i for each parent in order - C = [] - for pid in parents: - C_i = apply_linear_kernel_q(select_W_for_parent(W_q, pid, attrs), A[pid], attrs) - C.append(C_i) - Z_full = tensor_sum(C) + B_v - S_idx = set(proof["statement"]["S"]) - Z_part = tensor_sum([C[i] for i,_ in enumerate(parents) if (i+1) in S_idx]) + B_v - R = Z_full - Z_part - p = proof["statement"]["norm"]; eps = proof["statement"]["eps"] - num = norm_q(R, p); den = norm_q(Z_full, p) - if den == 0: - return (num == 0, "zero_output_ok" if num == 0 else "epsilon_violation") - return (rational_leq(num, eps, den), "ok" if rational_leq(num, eps, den) else "epsilon_violation") -``` + +.. code-block:: python + + # merkleagi/proofs.py (concise core) + from typing import Tuple + from .dag import Repo, compute_commits, ordered_parents + from .hash import sha256 + from .quant import gemm_q + from .encoding import * + def verify_path(root: bytes, proof: dict) -> Tuple[bool,str]: + # Replay Merkle chain; check ordered children and siblings up to 'root' + # (Full implementation in Appendix B) + ... + def attrs_hash_matches_commit(repo: Repo, nid: str, attrs_tlv: bytes, params_tlv: bytes) -> bool: + hb = repo.base_hash[nid] + return hb == sha256(enc_seq(T_BASE, [tlv(0x01, nid.encode()), attrs_tlv, params_tlv])) + def materialize_kernel_weights(repo: Repo, nid: str, params: dict, block_payloads: dict) -> "torch.Tensor": + # Resolve W from block hashes + provided payloads; check each payload digest + ... + return W_q + def apply_linear_kernel_q(W_q, A_q, attrs): + if attrs["policy"] == "gemm_q": + return gemm_q(W_q, A_q, attrs) + raise ValueError("Unsupported policy for affine preactivation") + def norm_q(q_tensor, p: str) -> int: + # Exact integer norms; return Python int (no float) + # L1: sum(abs), L2: sum(x^2) (compare squared values), Linf: max(abs) + ... + return int_val + def rational_leq(num: int, eps_str: str, den: int) -> bool: + # Compare num/den <= eps as integers (avoid float) + # eps_str is decimal; parse to (num_eps, den_eps) and compare num*den_eps <= den*num_eps + ... + return bool + def verify_eps_affine(root: bytes, node_id: str, proof: dict, repo: Repo) -> Tuple[bool,str]: + ok, msg = verify_path(root, proof.get("structure_v", proof.get("structure"))) + if not ok: return False, "structure_mismatch" + parents = proof["structure"]["ordered_parents"] # or rebuild from repo + attrs = proof["attrs"]; params = proof["params"] + attrs_tlv = encode_attrs(attrs) + params_tlv = encode_params(params) + if not attrs_hash_matches_commit(repo, node_id, attrs_tlv, params_tlv): + return False, "param_mismatch" + # Load activations (all parents) + A = { pid: decode_int_tensor_bytes(proof["activations"][pid], attrs) for pid in parents } + # Materialize W and B + W_q = materialize_kernel_weights(repo, node_id, params, proof.get("block_payloads", {})) + B_v = decode_int_tensor_bytes(params["B"], attrs) + # Compute C_i for each parent in order + C = [] + for pid in parents: + C_i = apply_linear_kernel_q(select_W_for_parent(W_q, pid, attrs), A[pid], attrs) + C.append(C_i) + Z_full = tensor_sum(C) + B_v + S_idx = set(proof["statement"]["S"]) + Z_part = tensor_sum([C[i] for i,_ in enumerate(parents) if (i+1) in S_idx]) + B_v + R = Z_full - Z_part + p = proof["statement"]["norm"]; eps = proof["statement"]["eps"] + num = norm_q(R, p); den = norm_q(Z_full, p) + if den == 0: + return (num == 0, "zero_output_ok" if num == 0 else "epsilon_violation") + return (rational_leq(num, eps, den), "ok" if rational_leq(num, eps, den) else "epsilon_violation") + § 7.16 What auditors, engineers, and reviewers can rely on ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1238,20 +1279,26 @@ All sizes below are exact or worst-case tight up to small constant TLV overheads Theorem 8.1 (Path proof size and time). A canonical Merkle authentication from node (v) to the root requires at most -[ -S_{\text{path}} \le D\cdot (1 + s_\text{sib})\cdot h -] + +:: + + S_{\text{path}} \le D\cdot (1 + s_\text{sib})\cdot h + bytes of hash material, where (s_\text{sib}) is the average number of sibling hashes per level (≤ outdegree−1), and verification time -[ -T_{\text{path}}=O(D\cdot (1+s_\text{sib})) -] + +:: + + T_{\text{path}}=O(D\cdot (1+s_\text{sib})) + hash computations. With parent-order enforcement and length-prefixing (Part 3), the bound is tight. Proof (sketch). Standard Merkle authentication: each level contributes the current node hash plus sibling hashes needed to recompute the parent commitment; length-prefixing prevents ambiguity; ordered parents are verified by comparing ordered child digests inside the committed preimage. □ Corollary 8.1.1 (Dedup). If a proof references the same sibling set multiple times along the chain (shared sub-DAGs), deduplication reduces the transferable hashes to the set of unique siblings per level without affecting soundness. Size becomes -[ -S_{\text{path}}^{\text{dedup}} \le D\cdot (1+\tilde s_\text{sib})\cdot h,\quad \tilde s_\text{sib}\le s_\text{sib}. -] + +:: + + S_{\text{path}}^{\text{dedup}} \le D\cdot (1+\tilde s_\text{sib})\cdot h,\quad \tilde s_\text{sib}\le s_\text{sib}. + § 8.3 ε-proofs at affine preactivation frontiers (v7-Local) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1261,20 +1308,24 @@ Recall (Part 3): for (v) affine preactivation, we reveal all parent activations § 8.3.1 Weight disclosure ^^^^^^^^^^^^^^^^^^^^^^^^^^ -Let (W_v) be block-hashed into (\lceil |W_v| / B \rceil) blocks. For a column-selective computation (typical for parent (u)’s slice), the prover discloses only the blocks intersecting the addressed columns/rows. -- Worst case (arbitrary layout): all blocks may be required ⇒ (|W_v|) entries disclosed. +Let (W_v) be block-hashed into (\lceil \|W_v\| / B \rceil) blocks. For a column-selective computation (typical for parent (u)’s slice), the prover discloses only the blocks intersecting the addressed columns/rows. +- Worst case (arbitrary layout): all blocks may be required ⇒ (\|W_v\|) entries disclosed. - Structured case (contiguous columns per parent, standard in MLP/attention projections): only the blocks for the selected columns are disclosed. If parent (u) contributes a slice of width (k_{u\to v}), blocks disclosed are - [ - \left\lceil\frac{m_v\cdot k_{u\to v}}{B}\right\rceil. - ] + + :: + + \left\lceil\frac{m_v\cdot k_{u\to v}}{B}\right\rceil. + § 8.3.2 Activation disclosure ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ All parents’ integer activations (A_{u\to v}) are disclosed. Size: -[ -S_{\text{acts}} = \sum_{u\in \text{pred}(v)} |A_{u\to v}|\cdot s_{\text{int}} -] + +:: + + S_{\text{acts}} = \sum_{u\in \text{pred}(v)} |A_{u\to v}|\cdot s_{\text{int}} + where (s_{\text{int}}) is the integer byte width (8 bytes for int64; exact by spec). § 8.3.3 Total ε-proof size @@ -1282,23 +1333,29 @@ where (s_{\text{int}}) is the integer byte width (8 bytes for int64; exact by sp Theorem 8.2 (ε-proof size bound). For affine preactivation node (v) with indegree (d_v), block size (B), int64 tensors, the ε-proof needs: -[ -S_{\varepsilon}(v)\ \le\ S_{\text{path}}^{\text{dedup}}(v)\ +\ \underbrace{\sum_{u\in\text{pred}(v)} |A_{u\to v}|\cdot 8}{\text{parent activations}}\ +\ \underbrace{#\text{Wblocks}\cdot (B\cdot 8 + h)}{\text{block payloads + their hashes}}\ +\ \underbrace{|B_v|\cdot 8}_{\text{bias}} \ +\ O(1). -] + +:: + + S_{\varepsilon}(v)\ \le\ S_{\text{path}}^{\text{dedup}}(v)\ +\ \underbrace{\sum_{u\in\text{pred}(v)} |A_{u\to v}|\cdot 8}{\text{parent activations}}\ +\ \underbrace{#\text{Wblocks}\cdot (B\cdot 8 + h)}{\text{block payloads + their hashes}}\ +\ \underbrace{|B_v|\cdot 8}_{\text{bias}} \ +\ O(1). + Verification time is: -[ -T_{\varepsilon}(v)\ =\ O\big(#\text{Wblocks} + D\cdot(1+\tilde s_\text{sib})\big)\ \text{hash ops}\ +\ T_{\text{gemm}}^{\text{int}}(m_v,k_v)\ +\ T_{\text{norm}}(m_v), -] + +:: + + T_{\varepsilon}(v)\ =\ O\big(#\text{Wblocks} + D\cdot(1+\tilde s_\text{sib})\big)\ \text{hash ops}\ +\ T_{\text{gemm}}^{\text{int}}(m_v,k_v)\ +\ T_{\text{norm}}(m_v), + where (T_{\text{gemm}}^{\text{int}}) is the integer-exact matrix-vector cost (big-int safe fallback allowed). Bounds are tight up to constant TLVs. Proof. The proof object contains (i) structure authentication (Theorem 8.1), (ii) all parents’ activations (integer bytes), (iii) the set of disclosed weight blocks (each with payload + its 32-byte hash to check against the committed list), and (iv) bias. The verifier recomputes (Z_v) with integer kernels and checks the ε-inequality (Part 3). No other data are required. □ § 8.4 Integer exactness without overflow: tile policies and certificates ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Let (k) be the inner dimension of the GEMM (Z = W A). Suppose (|W_{ij}| \le M_W), (|A_j| \le M_A) (integer magnitudes). A naive int64 accumulation risks overflow if: -[ -k\cdot M_W\cdot M_A \ge 2^{63}. -] +Let (k) be the inner dimension of the GEMM (Z = W A). Suppose (\|W_{ij}\| \le M_W), (\|A_j\| \le M_A) (integer magnitudes). A naive int64 accumulation risks overflow if: + +:: + + k\cdot M_W\cdot M_A \ge 2^{63}. + Two solutions are specified in the v7 contract: § 8.4.1 Big-int safe kernel (reference path) @@ -1311,9 +1368,11 @@ Accumulate in Python big-ints (or chunk and carry in 128-bit software) ⇒ exact Lemma 8.3 (Safe tile length). If accumulation is tiled with inner tile length (t) such that -[ -t \cdot M_W \cdot M_A < 2^{62}, -] + +:: + + t \cdot M_W \cdot M_A < 2^{62}, + and partial sums are flushed to 128-bit or big-int before next tile, then int64 accumulation within each tile is overflow-free. Proof. Max per-tile sum magnitude (< 2^{62}) ⇒ two’s-complement int64 headroom is respected (one bit for sign, one safety bit). □ Certificate generation. The prover computes conservative (M_W,M_A) (max absolute entries) and discloses them in range_cert, together with the chosen (t). The verifier checks the inequality; if it fails or is absent, it must run the big-int path. @@ -1326,9 +1385,11 @@ Proof. Integer arithmetic is associative; within each tile, no wrap occurs; tile Theorem 8.5 (Streaming working-set bound). A verifier can process an ε-proof for node (v) with peak memory -[ -M_{\text{peak}}=O\big(h\cdot D + B\cdot 8 + d\cdot 8\big), -] + +:: + + M_{\text{peak}}=O\big(h\cdot D + B\cdot 8 + d\cdot 8\big), + i.e., proportional to one level of authentication hashes, one weight block, and one activation vector, by streaming blocks and parents sequentially. Proof. Structure hashes are verified level-by-level (keep only current frontier). Weight blocks are hashed and consumed incrementally; activations per parent are streamed; partial sums for (Z_v) can be accumulated in place. No other state is required. □ Corollary (Parallelization). @@ -1340,13 +1401,17 @@ Parents can be processed in parallel; blocks within a parent slice can be tiled Under A1–A3, a verifier must (i) authenticate membership (at least one hash per level) and (ii) compute an ε-inequality that depends on the actual integers of (Z_v) and subset (S). Therefore: Theorem 8.6 (Information-theoretic lower bound). Any ε-proof at an affine preactivation frontier requires -[ -\Omega(D\cdot h)\ \text{bits for structure} \quad\text{and}\quad \Omega(m_v + \text{nnz}(W_{v,S}))\ \text{integer symbols for the numeric check}. -] + +:: + + \Omega(D\cdot h)\ \text{bits for structure} \quad\text{and}\quad \Omega(m_v + \text{nnz}(W_{v,S}))\ \text{integer symbols for the numeric check}. + Consequently, -[ -S_{\varepsilon}(v)=\Omega(D\cdot h + m_v + \text{nnz}(W_{v,S})), -] + +:: + + S_{\varepsilon}(v)=\Omega(D\cdot h + m_v + \text{nnz}(W_{v,S})), + up to logarithmic factors for TLVs. Proof (sketch). Without the (D\cdot h) hashes, the verifier cannot bind the node to the root (any collision would be undetectable); without the integers underlying (Z_v) and (Z_v^{\text{partial}}), no ε-comparison can be executed. Any compression that hides integer content would contradict ε-soundness unless replaced by a zero-knowledge argument—outside v7 core. □ Thus the O(D·d_max + D·d) style bounds in Parts 3–4 are essentially tight. @@ -1395,7 +1460,7 @@ Rationale. Non-affine transitions (e.g., pooling, softmax, LN) are verified stru ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - Block hashing: choose block size (B) (entries) so each block payload remains comfortably cache-resident (e.g., 16–64 Ki entries ⇒ 128–512 KiB per int64 block). -- Root build: (O(|\Theta|/B)) leaf commits + (O(|V|)) internal commits (linear passes). +- Root build: (O(\|\Theta\|/B)) leaf commits + (O(\|V\|)) internal commits (linear passes). - ε-proofs: local to touched layers only; disclosure cost is proportional to needed blocks, independent of total parameter count except via the selected layer shapes. - Streaming verification: workable on commodity hardware; parallelizable across blocks and parents. Theorem 8.8 (Asymptotic independence from total params). @@ -1413,11 +1478,11 @@ Proof. All numeric checks depend only on (W_v,B_v) and parents’ activations; u ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Let (Z\in\mathbb{Z}^m). Define: -- ( |Z|_{1} = \sum_i |Z_i| ) — linear time, integer-exact. -- ( |Z|_{2}^2 = \sum_i Z_i^2 ) — integer-exact; comparisons can be done on squares to avoid roots. -- ( |Z|_{\infty} = \max_i |Z_i| ) — linear time. +- ( \|Z\|_{1} = \sum_i \|Z_i\| ) — linear time, integer-exact. +- ( \|Z\|_{2}^2 = \sum_i Z_i^2 ) — integer-exact; comparisons can be done on squares to avoid roots. +- ( \|Z\|_{\infty} = \max_i \|Z_i\| ) — linear time. Theorem 8.9 (ε comparison without floating point). -For any rational (ε=\frac{p}{q}) in lowest terms (parsed from a decimal string), the check (|R| \le ε |Z|) is equivalent to ( q\cdot |R| \le p\cdot |Z| ), computable with exact integer arithmetic. +For any rational (ε=\frac{p}{q}) in lowest terms (parsed from a decimal string), the check (\|R\| \le ε \|Z\|) is equivalent to ( q\cdot \|R\| \le p\cdot \|Z\| ), computable with exact integer arithmetic. Proof. Cross-multiply over integers; no rounding or float required. □ § 8.12 Complexity summary (layer-wise) @@ -1425,19 +1490,25 @@ Proof. Cross-multiply over integers; no rounding or float required. □ For an affine preactivation node (v) with shape (m\times k), block size (B), and indegree (d_v): - Proof size - [ - S_{\varepsilon}(v) = O\big(D\cdot h\big)\ +\ O\big(m + \min(|W_v|,\lceil m k_S/B\rceil\cdot B)\big)\cdot 8, - ] + + :: + + S_{\varepsilon}(v) = O\big(D\cdot h\big)\ +\ O\big(m + \min(|W_v|,\lceil m k_S/B\rceil\cdot B)\big)\cdot 8, + plus (O(#\text{Wblocks}\cdot h)) for per-block digests. - Verification time - [ - T_{\varepsilon}(v) = O\big(D\cdot (1+\tilde s_\text{sib})\big)\ \text{hashes}\ +\ O(mk)\ \text{int ops}\ +\ O(m) - ] + + :: + + T_{\varepsilon}(v) = O\big(D\cdot (1+\tilde s_\text{sib})\big)\ \text{hashes}\ +\ O(mk)\ \text{int ops}\ +\ O(m) + (big-int exact or range-certified tiled int64). - Memory (peak) - [ - M_{\text{peak}} = O(D\cdot h + B\cdot 8 + d\cdot 8). - ] + + :: + + M_{\text{peak}} = O(D\cdot h + B\cdot 8 + d\cdot 8). + Each bound is achievable with the streaming implementation in Part 4 and optimal up to constants by Theorem 8.6. § 8.13 Practical parameter choices (engineering playbook) @@ -1492,18 +1563,22 @@ Let (v) have quantized parameters (Q(\Theta_v)), ordered parents (\mathrm{pred}( - Hard base: (h_v^{\text{base}} = H\big(\mathrm{Enc}(\texttt{"base"},\mathrm{id}(v),d_v)\big)). - Hard commit (leaf): (C(v)=H\big(\mathrm{Enc}(\texttt{"leaf"},\mathrm{id}(v),h_v^{\text{base}})\big)). - Hard commit (internal): - [ - C(v)=H!\Big(\mathrm{Enc}(\texttt{"node"},\mathrm{id}(v),k,h_v^{\text{base}})\ \Vert\ \big\Vert_{i=1}^{k}\mathrm{len}\big(C(u_i)\big)\ \Vert\ C(u_i)\Big), - ] + + :: + + C(v)=H!\Big(\mathrm{Enc}(\texttt{"node"},\mathrm{id}(v),k,h_v^{\text{base}})\ \Vert\ \big\Vert_{i=1}^{k}\mathrm{len}\big(C(u_i)\big)\ \Vert\ C(u_i)\Big), + with canonical parent order and length-prefixing (Part 3). - Soft hash (train-time): - [ - h_v=\sigma!\left(W_v^{(h)},[,\mathrm{vec}\big(Q(\Theta_v)\big)\ ;\ \overline{h}{\mathrm{pred}(v)},]\right),\quad - \overline{h}{\mathrm{pred}(v)}=\begin{cases} - \frac{1}{k}\sum_{u\in\mathrm{pred}(v)} h_u,& k>0\[3pt] - 0,& k=0 - \end{cases} - ] + + :: + + h_v=\sigma!\left(W_v^{(h)},[,\mathrm{vec}\big(Q(\Theta_v)\big)\ ;\ \overline{h}{\mathrm{pred}(v)},]\right),\quad + \overline{h}{\mathrm{pred}(v)}=\begin{cases} + \frac{1}{k}\sum_{u\in\mathrm{pred}(v)} h_u,& k>0\[3pt] + 0,& k=0 + \end{cases} + with (\sigma=\tanh) and (W_v^{(h)}) a learned projector. - Hard-to-soft anchor: fixed embedding (\widehat h_v^{\text{hard}}=\phi\big(C(v)\big)) that maps the 32-byte digest to a (d_h)-vector (e.g., interpret as 64×uint32, normalize to ([-1,1])). @@ -1511,12 +1586,14 @@ Let (v) have quantized parameters (Q(\Theta_v)), ordered parents (\mathrm{pred}( ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Let (L_{\text{task}}) be the primary task loss (e.g., cross-entropy, MSE). Define: -[ -\mathcal{L}{\text{plastic}} -= \lambda_1 \sum{v}\big|h_v - \widehat h_v^{\text{hard}}\big|_2^2 -- \lambda_2 \sum_{v}\big|h_v^{(t)} - h_v^{(t-1)}\big|_2^2 -- \lambda_3 \operatorname{Tr}!\big(\mathrm{Cov}({h_v})\big), - ] + +:: + + \mathcal{L}{\text{plastic}} + = \lambda_1 \sum{v}\big|h_v - \widehat h_v^{\text{hard}}\big|_2^2 + - \lambda_2 \sum_{v}\big|h_v^{(t)} - h_v^{(t-1)}\big|_2^2 + - \lambda_3 \operatorname{Tr}!\big(\mathrm{Cov}({h_v})\big), + where the third term discourages collapse by maximizing dispersion (negative trace of covariance). Total loss: ( \mathcal{L} = L_{\text{task}} + \mathcal{L}{\text{plastic}} + \mathcal{L}{\text{sparsity}} ) (the last is optional L1/Top-k gating to induce interpretable, low-fan-in circuits). Schedules (robust defaults): @@ -1553,57 +1630,58 @@ With (\lambda_2>0), the family ({h_v^{(t)}}) forms a Lipschitz trajectory across We recommend shipping a stability head that monitors: - Commit drift: Hamming distance between (\widehat h_v^{\text{hard}}(t)) and (\widehat h_v^{\text{hard}}(t-1)) (post-embedding). -- Jacobian SNR: ratio (| \partial h_v/\partial \Theta_v |_F / | h_v |_2) to detect vanishing/exploding plastic signals. +- Jacobian SNR: ratio (\| \partial h_v/\partial \Theta_v \|_F / \| h_v \|_2) to detect vanishing/exploding plastic signals. - Entropy of fan-in: (H_{\text{fan-in}}(v)=-\sum p_u\log p_u) where (p_u) is normalized contribution from parent (u) (in integer space). A drop signals hard specialization; a spike signals diffusion. These diagnostics do not affect proofs; they guide training. § 9.7 Plasticity code (reference, deterministic & minimal) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -```python -# merkleagi/plastic.py -import torch, struct, hashlib -from typing import List, Optional -INT32_MAX = 4294967295 -def sha256(b: bytes) -> bytes: - return hashlib.sha256(b).digest() -def embed_hard_to_vec(digest: bytes, dim: int = 256) -> torch.Tensor: - """Map 32B digest -> dim vector in [-1,1] deterministically.""" - padded = digest.ljust(256, b"\x00") - ints = struct.unpack("<64I", padded) - v = torch.tensor(ints, dtype=torch.float32) - v = 2.0 * (v / INT32_MAX) - 1.0 - if dim != 256: - # Fixed linear down/up-projection with frozen seed - torch.manual_seed(0) - P = torch.randn(dim, 256) - v = P @ v - v = torch.tanh(v) - return v -class SoftHashProjector(torch.nn.Module): - def __init__(self, in_dim: int, out_dim: int = 256): - super().__init__() - self.proj = torch.nn.Linear(in_dim, out_dim, bias=True) - def forward(self, qparams: torch.Tensor, parent_soft: Optional[List[torch.Tensor]]): - if parent_soft: - parent_mean = torch.stack(parent_soft, dim=0).mean(dim=0) - else: - parent_mean = torch.zeros(self.proj.in_features - qparams.numel(), dtype=torch.float32, device=qparams.device) - x = torch.cat([qparams.flatten(), parent_mean]) - return torch.tanh(self.proj(x)) -def plasticity_loss(h_soft: List[torch.Tensor], - h_soft_prev: List[Optional[torch.Tensor]], - h_hard_embed: List[torch.Tensor], - lam_cons: float, lam_smooth: float, lam_div: float) -> torch.Tensor: - Lc = sum((hs - hh).pow(2).sum() for hs, hh in zip(h_soft, h_hard_embed)) - Ls = sum((hs - hp).pow(2).sum() for hs, hp in zip(h_soft, h_soft_prev) if hp is not None) - # Diversity via negative covariance trace - H = torch.stack(h_soft, dim=0) # [V, dh] - Hc = H - H.mean(dim=0, keepdim=True) - cov_trace = (Hc.T @ Hc).trace() / (H.shape[0] - 1 + 1e-12) - Ld = -cov_trace - return lam_cons * Lc + lam_smooth * Ls + lam_div * Ld -``` +.. code-block:: python + + # merkleagi/plastic.py + import torch, struct, hashlib + from typing import List, Optional + INT32_MAX = 4294967295 + def sha256(b: bytes) -> bytes: + return hashlib.sha256(b).digest() + def embed_hard_to_vec(digest: bytes, dim: int = 256) -> torch.Tensor: + """Map 32B digest -> dim vector in [-1,1] deterministically.""" + padded = digest.ljust(256, b"\x00") + ints = struct.unpack("<64I", padded) + v = torch.tensor(ints, dtype=torch.float32) + v = 2.0 * (v / INT32_MAX) - 1.0 + if dim != 256: + # Fixed linear down/up-projection with frozen seed + torch.manual_seed(0) + P = torch.randn(dim, 256) + v = P @ v + v = torch.tanh(v) + return v + class SoftHashProjector(torch.nn.Module): + def __init__(self, in_dim: int, out_dim: int = 256): + super().__init__() + self.proj = torch.nn.Linear(in_dim, out_dim, bias=True) + def forward(self, qparams: torch.Tensor, parent_soft: Optional[List[torch.Tensor]]): + if parent_soft: + parent_mean = torch.stack(parent_soft, dim=0).mean(dim=0) + else: + parent_mean = torch.zeros(self.proj.in_features - qparams.numel(), dtype=torch.float32, device=qparams.device) + x = torch.cat([qparams.flatten(), parent_mean]) + return torch.tanh(self.proj(x)) + def plasticity_loss(h_soft: List[torch.Tensor], + h_soft_prev: List[Optional[torch.Tensor]], + h_hard_embed: List[torch.Tensor], + lam_cons: float, lam_smooth: float, lam_div: float) -> torch.Tensor: + Lc = sum((hs - hh).pow(2).sum() for hs, hh in zip(h_soft, h_hard_embed)) + Ls = sum((hs - hp).pow(2).sum() for hs, hp in zip(h_soft, h_soft_prev) if hp is not None) + # Diversity via negative covariance trace + H = torch.stack(h_soft, dim=0) # [V, dh] + Hc = H - H.mean(dim=0, keepdim=True) + cov_trace = (Hc.T @ Hc).trace() / (H.shape[0] - 1 + 1e-12) + Ld = -cov_trace + return lam_cons * Lc + lam_smooth * Ls + lam_div * Ld + Notes. - embed_hard_to_vec is fixed and stateless; it never touches commitments. - No randomness is used at verify time; seeds are fixed for reproducibility. @@ -1611,22 +1689,23 @@ Notes. § 9.8 Checkpoint API (minimal contract) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -```python -# merkleagi/checkpoint.py -from merkleagi.dag import recompute_commits, root_commit -from merkleagi.quant import quantize_params -from merkleagi.manifest import write_manifest -def checkpoint_commit(model, delta, kernels_digest, dataset_digest, step, outdir): - """ - 1) Freeze params; 2) Quantize (A2); 3) Recompute node commits; 4) Write root and manifest. - Returns root digest bytes. - """ - qparams = quantize_params(model.parameters(), delta) - recompute_commits(model, qparams) # traverses DAG; sets C(v) - root = root_commit(model) # C(M_t) - write_manifest(outdir, step, root, delta, kernels_digest, dataset_digest) - return root -``` +.. code-block:: python + + # merkleagi/checkpoint.py + from merkleagi.dag import recompute_commits, root_commit + from merkleagi.quant import quantize_params + from merkleagi.manifest import write_manifest + def checkpoint_commit(model, delta, kernels_digest, dataset_digest, step, outdir): + """ + 1) Freeze params; 2) Quantize (A2); 3) Recompute node commits; 4) Write root and manifest. + Returns root digest bytes. + """ + qparams = quantize_params(model.parameters(), delta) + recompute_commits(model, qparams) # traverses DAG; sets C(v) + root = root_commit(model) # C(M_t) + write_manifest(outdir, step, root, delta, kernels_digest, dataset_digest) + return root + § 9.9 Security review (plasticity) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1731,114 +1810,126 @@ We support two proof families: Claim: “Feature (f_i) is part of the explanation on input (x) with non-zero quantized activation (Q\big(s_i(x)\big)).” Proof object must include: 1. Path proof for (f_i) into (C(M)) (structural). -2. The integer (Q\big(s_i(x)\big)) and a statement that (|Q(s_i)|\ge \tau) (threshold). +2. The integer (Q\big(s_i(x)\big)) and a statement that (\|Q(s_i)\|\ge \tau) (threshold). 3. If tying to outputs, an ε-proof at the affine reconstruction preactivation: disclose needed columns of (D) and the code entries (Q(s_j(x))) that are in the claimed subset (S). (B) Integer reconstruction check. For a selected set (J\subseteq{1,\ldots,k}), we verify that -[ -Q!\big(a^{(L)}(x)\big) \approx \sum_{j\in J} Q!\big(D_{:,j}\big),Q!\big(s_j(x)\big) -] + +:: + + Q!\big(a^{(L)}(x)\big) \approx \sum_{j\in J} Q!\big(D_{:,j}\big),Q!\big(s_j(x)\big) + in integer space. Exact equality can be enforced or a tolerance (\delta) stated explicitly as a bound due solely to A2 rounding (no simulations). Tolerance computation (axiomatic). Let (r_D=D-Q(D)) and (r_s=s-Q(s)). Then the integer-space reconstruction error vector is -[ -E = Q(a) - \sum_{j\in J} Q(D_{:,j}),Q(s_j). -] + +:: + + E = Q(a) - \sum_{j\in J} Q(D_{:,j}),Q(s_j). + If the original real reconstruction satisfied (a \approx D s), then -[ -|E|1 \le |Q(a)-a|1 + \sum{j\in J}|r_D^{(:,j)},Q(s_j)|1 + \sum{j\in J}|Q(D{:,j}),r_{s_j}|_1 + \text{modeling error}. -] + +:: + + |E|1 \le |Q(a)-a|1 + \sum{j\in J}|r_D^{(:,j)},Q(s_j)|1 + \sum{j\in J}|Q(D{:,j}),r_{s_j}|_1 + \text{modeling error}. + Each term is bounded by (\Delta) and the entrywise magnitudes (all are integers or Δ-scaled integers). The proof states numeric, verifier-checkable caps, not measurements. § 10.4 Theorem 7 (Verifiable monosemanticity under sparsity & separation) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Statement. -Assume: (i) integer codes (Q(s(x))) are (k_s)-sparse with threshold (\tau>0) (i.e., at most (k_s) non-zeros ≥ (\tau)), (ii) decoder columns ({Q(D_{:,j})}) are pairwise (\ell_2)-separated by margin (\gamma>0) after normalization to unit integer norm. Then, for any input (x), if a proof (B) certifies that a single feature (f_i) with (|Q(s_i)|\ge\tau) explains at least ((1-\varepsilon)) of the integer reconstruction norm at the affine preactivation, the feature is monosemantic for this input in the sense that no other feature (f_{j\ne i}) with (|Q(s_j)|\ge\tau) can exceed the same contribution unless (\varepsilon \ge \frac{\tau}{\tau+\gamma}). +Assume: (i) integer codes (Q(s(x))) are (k_s)-sparse with threshold (\tau>0) (i.e., at most (k_s) non-zeros ≥ (\tau)), (ii) decoder columns ({Q(D_{:,j})}) are pairwise (\ell_2)-separated by margin (\gamma>0) after normalization to unit integer norm. Then, for any input (x), if a proof (B) certifies that a single feature (f_i) with (\|Q(s_i)\|\ge\tau) explains at least ((1-\varepsilon)) of the integer reconstruction norm at the affine preactivation, the feature is monosemantic for this input in the sense that no other feature (f_{j\ne i}) with (\|Q(s_j)\|\ge\tau) can exceed the same contribution unless (\varepsilon \ge \frac{\tau}{\tau+\gamma}). Proof (sketch, integer domain). -Normalize columns to integer unit norm; contribution of (f_i) is (|Q(s_i)|). If a competitor (f_j) carried equal or larger contribution, the integer inner product (\langle Q(D_{:,i}), Q(D_{:,j})\rangle) would have to be large; separation margin (\gamma) bounds this inner product, yielding a contradiction unless the residual allowance (\varepsilon) is at least (\tau/(\tau+\gamma)). All operations are on integers; the bound is deterministic given ((\tau,\gamma)). □ +Normalize columns to integer unit norm; contribution of (f_i) is (\|Q(s_i)\|). If a competitor (f_j) carried equal or larger contribution, the integer inner product (\langle Q(D_{:,i}), Q(D_{:,j})\rangle) would have to be large; separation margin (\gamma) bounds this inner product, yielding a contradiction unless the residual allowance (\varepsilon) is at least (\tau/(\tau+\gamma)). All operations are on integers; the bound is deterministic given ((\tau,\gamma)). □ Interpretation. With sparse, separated decoders, a large integer activation for (f_i) implies exclusive explanatory weight within the certified tolerance. This is a verifiable analogue of monosemanticity. § 10.5 Dictionary integration algorithms ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Commit dictionary features -```python -# merkleagi/dictionary.py -from merkleagi.encoding import enc_tlv -from merkleagi.hash import sha256_h -from merkleagi.quant import quantize_tensor -def commit_dictionary(layer_id: str, D_cols: dict, dag): - """ - D_cols: mapping {i: torch.Tensor shape [d]} for decoder columns. - Produces committed feature nodes f_i and attaches to DAG. - """ - for i, col in D_cols.items(): - qcol = quantize_tensor(col) # A2 - nid = f"dict_feat::{i}::layer::{layer_id}" - base = sha256_h(enc_tlv("base", nid, {"op":"dictionary_feature", - "ver":1, - "attrs":{}, - "qparams": qcol.cpu().numpy().tobytes(order="C")})) - leaf = sha256_h(enc_tlv("leaf", nid, base)) - dag.add_feature_node(nid=nid, qparams=qcol, base_hash=base, commit=leaf) -``` + +.. code-block:: python + + # merkleagi/dictionary.py + from merkleagi.encoding import enc_tlv + from merkleagi.hash import sha256_h + from merkleagi.quant import quantize_tensor + def commit_dictionary(layer_id: str, D_cols: dict, dag): + """ + D_cols: mapping {i: torch.Tensor shape [d]} for decoder columns. + Produces committed feature nodes f_i and attaches to DAG. + """ + for i, col in D_cols.items(): + qcol = quantize_tensor(col) # A2 + nid = f"dict_feat::{i}::layer::{layer_id}" + base = sha256_h(enc_tlv("base", nid, {"op":"dictionary_feature", + "ver":1, + "attrs":{}, + "qparams": qcol.cpu().numpy().tobytes(order="C")})) + leaf = sha256_h(enc_tlv("leaf", nid, base)) + dag.add_feature_node(nid=nid, qparams=qcol, base_hash=base, commit=leaf) + Prove feature use (presence + reconstruction fragment) -```python -def prove_feature_use(model_root, layer_id, i, q_s_i, J_subset, q_s_subset, tol_bound, path_proof_fi, D_blocks_payload): - """ - Returns a proof dict containing: - - path_proof_fi (Merkle path for f_i) - - q_s_i >= tau - - (optional) reconstruction fragment over J_subset with disclosed D blocks and q_s_subset - - declared integer tolerance 'tol_bound' (verifier-checkable) - """ - assert abs(q_s_i) > 0, "feature inactive" - proof = { - "type": "feature_use", - "layer_id": layer_id, - "feature_id": i, - "q_s_i": int(q_s_i), - "path": path_proof_fi, - "recon": { - "J": list(J_subset), - "q_s_subset": [int(q_s_subset[j]) for j in J_subset], - "D_blocks": D_blocks_payload, # block-hashed, each with (payload, hash) - "tol_bound": tol_bound, - } - } - return proof -``` + +.. code-block:: python + + def prove_feature_use(model_root, layer_id, i, q_s_i, J_subset, q_s_subset, tol_bound, path_proof_fi, D_blocks_payload): + """ + Returns a proof dict containing: + - path_proof_fi (Merkle path for f_i) + - q_s_i >= tau + - (optional) reconstruction fragment over J_subset with disclosed D blocks and q_s_subset + - declared integer tolerance 'tol_bound' (verifier-checkable) + """ + assert abs(q_s_i) > 0, "feature inactive" + proof = { + "type": "feature_use", + "layer_id": layer_id, + "feature_id": i, + "q_s_i": int(q_s_i), + "path": path_proof_fi, + "recon": { + "J": list(J_subset), + "q_s_subset": [int(q_s_subset[j]) for j in J_subset], + "D_blocks": D_blocks_payload, # block-hashed, each with (payload, hash) + "tol_bound": tol_bound, + } + } + return proof + Verify feature use -```python -def verify_feature_use(model_root, proof, q_a_L, block_hash_index): - """ - model_root: trusted C(M); q_a_L: integer preactivation at layer L; block_hash_index: mapping hash->payload - Steps: - 1) verify path proof binds feature_id to model_root; - 2) check |q_s_i| >= tau (tau is policy); - 3) (optional) reconstruct sum_j Q(D_j) * Q(s_j) from disclosed blocks; compare to q_a_L within tol_bound (integer L1 or L2^2); - """ - ok, reason = verify_path(model_root, proof["path"]) - if not ok: return False, f"path invalid: {reason}" - if abs(proof["q_s_i"]) < 1: # example tau=1 in integer units - return False, "feature below threshold" - # Reconstruction: - recon = proof.get("recon", None) - if recon: - # Resolve blocks by hash - D = assemble_matrix_from_blocks(recon["D_blocks"], block_hash_index) - J = recon["J"]; q_s = recon["q_s_subset"] - recon_vec = sum(D[:, j] * q_s[k] for k, j in enumerate(J)) - if not integer_within_tolerance(q_a_L, recon_vec, recon["tol_bound"]): - return False, "reconstruction outside declared integer tolerance" - return True, "feature use verified" -``` + +.. code-block:: python + + def verify_feature_use(model_root, proof, q_a_L, block_hash_index): + """ + model_root: trusted C(M); q_a_L: integer preactivation at layer L; block_hash_index: mapping hash->payload + Steps: + 1) verify path proof binds feature_id to model_root; + 2) check |q_s_i| >= tau (tau is policy); + 3) (optional) reconstruct sum_j Q(D_j) * Q(s_j) from disclosed blocks; compare to q_a_L within tol_bound (integer L1 or L2^2); + """ + ok, reason = verify_path(model_root, proof["path"]) + if not ok: return False, f"path invalid: {reason}" + if abs(proof["q_s_i"]) < 1: # example tau=1 in integer units + return False, "feature below threshold" + # Reconstruction: + recon = proof.get("recon", None) + if recon: + # Resolve blocks by hash + D = assemble_matrix_from_blocks(recon["D_blocks"], block_hash_index) + J = recon["J"]; q_s = recon["q_s_subset"] + recon_vec = sum(D[:, j] * q_s[k] for k, j in enumerate(J)) + if not integer_within_tolerance(q_a_L, recon_vec, recon["tol_bound"]): + return False, "reconstruction outside declared integer tolerance" + return True, "feature use verified" + All arithmetic operates on integers per A2; tolerances are declared as exact integer bounds computed from (\Delta) and shapes—no empirical fudge factors. § 10.6 Training SAEs in a commitment-friendly way ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- Quantization-aware decoder: include (\mathcal{L}_{Q} = | D - Q(D)|_F^2) or straight-through estimator so that eventual (Q(D)) is high-fidelity. +- Quantization-aware decoder: include (\mathcal{L}_{Q} = \| D - Q(D)\|_F^2) or straight-through estimator so that eventual (Q(D)) is high-fidelity. - Code sparsity: enforce (k_s)-sparsity (top-k) or L1 with deterministic tie-breaking (lexicographic on indices) to avoid non-deterministic supports. - Column normalization (integer): maintain near-unit integer norms using periodic re-scaling compatible with A2 (e.g., project to nearest quantized unit). - Feature IDs: fix column order or ship a stable permutation proof (appendix) so that semantic names persist across checkpoints. @@ -1848,7 +1939,7 @@ All arithmetic operates on integers per A2; tolerances are declared as exact int - Zero vector columns: forbidden by schema; encoder refuses to commit zero-norm (Q(D_{:,i})). - Highly correlated bases: separation margin (\gamma) becomes small; monosemanticity bound weakens accordingly—proof remains honest. -- Negative codes: allowed; integer sign handled natively; thresholds apply to (|Q(s_i)|). +- Negative codes: allowed; integer sign handled natively; thresholds apply to (\|Q(s_i)\|). - Batch reconstructions: verify per-sample; batch aggregation is a convenience only. § 10.8 Interoperation with ε-proofs (v7-Local) @@ -1857,7 +1948,7 @@ All arithmetic operates on integers per A2; tolerances are declared as exact int When a dictionary feature feeds a subsequent affine preactivation, ε-proofs apply there: - Disclose the relevant decoder columns (Q(D_{:,j})) and code entries (Q(s_j(x))). - Recompute the affine preactivation (Z) exactly in integer space with big-int or range-certified tiles. -- Check (|Z - Z_S| \le \varepsilon |Z|) with the integer cross-multiplication rule (Part 5, §8.11). +- Check (\|Z - Z_S\| \le \varepsilon \|Z\|) with the integer cross-multiplication rule (Part 5, §8.11). Dictionary proofs and ε-proofs thus compose cleanly: the former certifies feature identity and activity; the latter certifies quantitative coverage at the downstream affine frontier. § 10.9 Security & governance notes (dictionary) @@ -1907,11 +1998,13 @@ Composition rule (locality of ε): If (v) is non-affine (e.g., softmax_q, gelu_l ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider a typical VL pipeline: -[ -\text{image} \xrightarrow{\text{CNN}} e_{\mathrm{img}} -\ \xrightarrow{\text{bridge_linear}} z -\ \xrightarrow{\text{Transformer}} y_{\text{text}}. -] + +:: + + \text{image} \xrightarrow{\text{CNN}} e_{\mathrm{img}} + \ \xrightarrow{\text{bridge_linear}} z + \ \xrightarrow{\text{Transformer}} y_{\text{text}}. + - The CNN exposes affine preactivations before non-linearities; ε-proofs can be placed at selected conv/linear preacts. - The bridge is linear—prime location for ε-proofs to quantify the image subspace that influences text tokens. - The Transformer exposes affine preactivations at Q/K/V projections and MLP linears. ε-proofs go there; attention softmax gets structural only plus quantized top-k proofs (Part 4). @@ -1925,9 +2018,11 @@ Let a multimodal DAG (M) be partitioned into (L) stages by (possibly multiple) a (|z_\ell - z_{\ell,S_\ell}|p \le \varepsilon\ell |z_\ell|_p) (notation as in Sec. 6), independent of other stages. 2. (Global control under monotone positives) If, between (F_\ell) and (F_{\ell+1}), the subgraph is monotone positive with respect to the norm (e.g., non-negative linear mixing and ReLU-like non-expansive maps), then the downstream relative error accumulates at most additively: - [ - \frac{|y - \tilde y|p}{|y|p} \ \le\ \sum{\ell\in S} \alpha\ell \varepsilon_\ell, - ] + + :: + + \frac{|y - \tilde y|p}{|y|p} \ \le\ \sum{\ell\in S} \alpha\ell \varepsilon_\ell, + where (\alpha_\ell\ge 1) are verifier-known stability constants derived from deterministic Lipschitz/LUT bounds (Sec. 5). 3. (Soundness without monotonicity) Without monotone-positive structure, only local guarantees hold. Global claims are withheld; structural membership remains verifiable end-to-end. Proof (long-form, axiomatic). @@ -1951,40 +2046,42 @@ Implication. Multimodal pipelines are handled modularly: you certify what portio - Optional ε-proofs at Q/K/V linears for specific token positions. - Softmax is structural only + topk_q proof (quantized scores). Proof object (schema excerpt): -```json -{ - "type": "multimodal_eps_bundle", - "frontiers": [ - { - "id": "vision.block3.conv2.preact", - "eps": 0.10, - "parents": "... integer tensors ...", - "weights": "... integer tensors ...", - "norm": "L1" - }, - { - "id": "bridge.linear.preact", - "eps": 0.05, - "parents": "...", - "weights": "...", - "norm": "L2" - }, - { - "id": "decoder.block2.attn.Q.preact", - "eps": 0.08, - "parents": "...", - "weights": "...", - "norm": "L1" - } - ], - "structural_paths": [ - "vision.root→...→decoder.logits", - "decoder.block2.attn.softmax (structural only)" - ], - "kernel_manifest_digest": "…", - "delta": "Δ=1e-x" -} -``` + +.. code-block:: text + + { + "type": "multimodal_eps_bundle", + "frontiers": [ + { + "id": "vision.block3.conv2.preact", + "eps": 0.10, + "parents": "... integer tensors ...", + "weights": "... integer tensors ...", + "norm": "L1" + }, + { + "id": "bridge.linear.preact", + "eps": 0.05, + "parents": "...", + "weights": "...", + "norm": "L2" + }, + { + "id": "decoder.block2.attn.Q.preact", + "eps": 0.08, + "parents": "...", + "weights": "...", + "norm": "L1" + } + ], + "structural_paths": [ + "vision.root→...→decoder.logits", + "decoder.block2.attn.softmax (structural only)" + ], + "kernel_manifest_digest": "…", + "delta": "Δ=1e-x" + } + The verifier checks each frontier ε-proof exactly (integer arithmetic), validates structural paths, and—if the intermediate slice is monotone positive—computes a global bound with published (\alpha_\ell). § 11.5.2 Audio → Language (ASR or audio-QA) @@ -2013,26 +2110,27 @@ The verifier checks each frontier ε-proof exactly (integer arithmetic), validat § 11.7 Minimal API for multimodal proofs ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -```python -# merkleagi/multimodal.py -def prove_eps_bundle(model, x, frontier_specs, norm="L1"): - """ - frontier_specs: list of {"id": , "eps": float} - Returns a proof bundle containing independent v7-Local ε-proofs at each frontier. - """ - proofs = [] - for spec in frontier_specs: - v = locate_frontier(model, spec["id"]) - proofs.append(prove_eps_affine(model, v, x, p=norm, eps=spec["eps"])) # from Part 4 - return {"type":"multimodal_eps_bundle", - "frontiers": proofs, - "kernel_manifest_digest": manifest_digest(model)} -def verify_eps_bundle(root_commit, bundle): - for p in bundle["frontiers"]: - ok, reason = verify_eps_affine(root_commit, p) - if not ok: return False, f"frontier failed: {reason}" - return True, "all frontiers verified" -``` +.. code-block:: python + + # merkleagi/multimodal.py + def prove_eps_bundle(model, x, frontier_specs, norm="L1"): + """ + frontier_specs: list of {"id": , "eps": float} + Returns a proof bundle containing independent v7-Local ε-proofs at each frontier. + """ + proofs = [] + for spec in frontier_specs: + v = locate_frontier(model, spec["id"]) + proofs.append(prove_eps_affine(model, v, x, p=norm, eps=spec["eps"])) # from Part 4 + return {"type":"multimodal_eps_bundle", + "frontiers": proofs, + "kernel_manifest_digest": manifest_digest(model)} + def verify_eps_bundle(root_commit, bundle): + for p in bundle["frontiers"]: + ok, reason = verify_eps_affine(root_commit, p) + if not ok: return False, f"frontier failed: {reason}" + return True, "all frontiers verified" + § 12 Benchmark Plan & Reproducibility (No simulated results) ------------------------------------------------------------- @@ -2045,7 +2143,7 @@ We intentionally provide only procedures, scripts, and schemas. No numbers are c - Build time (s): wall-clock to compute all (C(v)) and root (C(M)). - Proof size (bytes): serialized ε-proof object; dedup on shared sub-DAGs. - Verify time (ms): wall-clock for verify_* on CPU. -- ε-coverage (%): (100\cdot \left(1-\frac{|z - z_S|_p}{|z|_p}\right)) (computed by verifier algebraically from integers). +- ε-coverage (%): (100\cdot \left(1-\frac{\|z - z_S\|_p}{\|z\|_p}\right)) (computed by verifier algebraically from integers). - Plastic overhead (%): (\frac{\text{step time with plasticity} - \text{baseline}}{\text{baseline}}\times 100). - Dictionary proof size (bytes): feature-use proof with integer reconstruction for J features. - Determinism checks: digest equality of manifests and kernel tables across runs. @@ -2078,76 +2176,78 @@ The bench harness will iterate over (frontier, ε, p) tuples and produce JSON lo § 12.5 Reproducibility manifest (JSON schema) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -```json -{ - "merkleagi_version": "7.0", - "root_commit": "32-byte-hex", - "delta": 1e-6, - "kernel_manifest": "32-byte-hex", - "hardware": { - "cpu": "...", - "gpu": "...", - "ram_gb": 64, - "os": "..." - }, - "software": { - "python": "3.12.3", - "torch": "2.4.0+cu121" - }, - "dataset_digest": "32-byte-hex", - "audit_mode": "STRICT|HYBRID|VISUAL", - "frontiers_tested": ["..."], - "random_seed": 0 -} -``` +.. code-block:: text + + { + "merkleagi_version": "7.0", + "root_commit": "32-byte-hex", + "delta": 1e-6, + "kernel_manifest": "32-byte-hex", + "hardware": { + "cpu": "...", + "gpu": "...", + "ram_gb": 64, + "os": "..." + }, + "software": { + "python": "3.12.3", + "torch": "2.4.0+cu121" + }, + "dataset_digest": "32-byte-hex", + "audit_mode": "STRICT|HYBRID|VISUAL", + "frontiers_tested": ["..."], + "random_seed": 0 + } + This manifest is written by the runner before benchmarks and attached to each result file. § 12.6 Benchmark runner (reference) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -```python -# bench/runner.py -import json, time -from merkleagi.manifest import new_manifest, write_manifest -from merkleagi.dag import root_commit, build_dag_from_model -from merkleagi.proofs import prove_eps_affine, verify_eps_affine -from merkleagi.multimodal import prove_eps_bundle, verify_eps_bundle -def run_bench(model, dataset, frontier_specs, delta, manifest_meta, outdir): - manifest = new_manifest(model, dataset, delta, manifest_meta) - write_manifest(outdir, **manifest) - # Build DAG & root - t0 = time.time() - dag = build_dag_from_model(model, delta) # quantizes & commits nodes - build_sec = time.time() - t0 - root = root_commit(dag) - results = [] - for i, x in enumerate(dataset): - # Proofs - t1 = time.time() - bundle = prove_eps_bundle(dag, x, frontier_specs, norm="L1") - prove_ms = (time.time() - t1) * 1000.0 - payload = json.dumps(bundle).encode("utf-8") - proof_bytes = len(payload) - # Verify - t2 = time.time() - ok, reason = verify_eps_bundle(root, bundle) - verify_ms = (time.time() - t2) * 1000.0 - results.append({ - "sample": i, - "root_commit_hex": root.hex(), - "prove_ms": round(prove_ms, 3), - "verify_ms": round(verify_ms, 3), - "proof_bytes": proof_bytes, - "ok": ok, - "reason": reason - }) - with open(f"{outdir}/bench_results.json", "w") as f: - json.dump({ - "manifest": manifest, - "build_time_s": round(build_sec, 3), - "results": results - }, f, indent=2) -``` +.. code-block:: python + + # bench/runner.py + import json, time + from merkleagi.manifest import new_manifest, write_manifest + from merkleagi.dag import root_commit, build_dag_from_model + from merkleagi.proofs import prove_eps_affine, verify_eps_affine + from merkleagi.multimodal import prove_eps_bundle, verify_eps_bundle + def run_bench(model, dataset, frontier_specs, delta, manifest_meta, outdir): + manifest = new_manifest(model, dataset, delta, manifest_meta) + write_manifest(outdir, **manifest) + # Build DAG & root + t0 = time.time() + dag = build_dag_from_model(model, delta) # quantizes & commits nodes + build_sec = time.time() - t0 + root = root_commit(dag) + results = [] + for i, x in enumerate(dataset): + # Proofs + t1 = time.time() + bundle = prove_eps_bundle(dag, x, frontier_specs, norm="L1") + prove_ms = (time.time() - t1) * 1000.0 + payload = json.dumps(bundle).encode("utf-8") + proof_bytes = len(payload) + # Verify + t2 = time.time() + ok, reason = verify_eps_bundle(root, bundle) + verify_ms = (time.time() - t2) * 1000.0 + results.append({ + "sample": i, + "root_commit_hex": root.hex(), + "prove_ms": round(prove_ms, 3), + "verify_ms": round(verify_ms, 3), + "proof_bytes": proof_bytes, + "ok": ok, + "reason": reason + }) + with open(f"{outdir}/bench_results.json", "w") as f: + json.dump({ + "manifest": manifest, + "build_time_s": round(build_sec, 3), + "results": results + }, f, indent=2) + Notes. - All timings use wall-clock and are environment-dependent. - No results are printed here; the file is the single source of truth. @@ -2156,43 +2256,47 @@ Notes. ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ scripts/reproduce.sh -```bash -#!/usr/bin/env bash -set -euo pipefail -# 1) Environment print -python -c "import sys, torch, platform; -print({'python':sys.version, 'torch':torch.__version__, 'platform':platform.platform()})" -# 2) Set deterministic seeds -export PYTHONHASHSEED=0 -export CUBLAS_WORKSPACE_CONFIG=:4096:8 -export CUDA_LAUNCH_BLOCKING=1 -# 3) Build kernels manifest (hash LUTs) -python -m merkleagi.quant --emit-kernel-manifest out/kernel_manifest.json -# 4) Prepare dataset digest (you provide the dataset) -python -m merkleagi.datasets --digest data/ | tee out/dataset_digest.txt -# 5) Run VL-small benchmark -python -m bench.runner - --model configs/vl_small.json - --data data/vl_samples.jsonl - --frontiers configs/frontiers_vl.json - --delta 1e-6 - --out out/vl_small_run -# 6) Run AT-small benchmark -python -m bench.runner - --model configs/at_small.json - --data data/at_samples.jsonl - --frontiers configs/frontiers_at.json - --delta 1e-6 - --out out/at_small_run -``` + +.. code-block:: bash + + #!/usr/bin/env bash + set -euo pipefail + # 1) Environment print + python -c "import sys, torch, platform; + print({'python':sys.version, 'torch':torch.__version__, 'platform':platform.platform()})" + # 2) Set deterministic seeds + export PYTHONHASHSEED=0 + export CUBLAS_WORKSPACE_CONFIG=:4096:8 + export CUDA_LAUNCH_BLOCKING=1 + # 3) Build kernels manifest (hash LUTs) + python -m merkleagi.quant --emit-kernel-manifest out/kernel_manifest.json + # 4) Prepare dataset digest (you provide the dataset) + python -m merkleagi.datasets --digest data/ | tee out/dataset_digest.txt + # 5) Run VL-small benchmark + python -m bench.runner + --model configs/vl_small.json + --data data/vl_samples.jsonl + --frontiers configs/frontiers_vl.json + --delta 1e-6 + --out out/vl_small_run + # 6) Run AT-small benchmark + python -m bench.runner + --model configs/at_small.json + --data data/at_samples.jsonl + --frontiers configs/frontiers_at.json + --delta 1e-6 + --out out/at_small_run + configs/frontiers_vl.json (example) -```json -[ - {"id": "vision.b3.conv2.preact", "eps": 0.10}, - {"id": "bridge.linear.preact", "eps": 0.05}, - {"id": "dec.b2.attn.Q.preact", "eps": 0.08} -] -``` + +.. code-block:: text + + [ + {"id": "vision.b3.conv2.preact", "eps": 0.10}, + {"id": "bridge.linear.preact", "eps": 0.05}, + {"id": "dec.b2.attn.Q.preact", "eps": 0.08} + ] + § 12.8 Acceptance criteria (what the auditor should check) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2447,13 +2551,15 @@ Canonical numeric forms: - Fixed-point tensors (A2) → 64-bit signed integers (see A.3) in row-major order with shape header (see below). Composite records: concatenate TLVs in semantic order (never sorted unless specified). Minimal tensor header TLV: -``` - payload: - shape_rank: uint8 - shape_dims: shape_rank × uint32 LE - dtype_tag: uint8 # 0=int64_q, 1=uint8, etc. (here we use int64_q) - data: |shape| × int64 BE # Q-values (see A.3) -``` + +.. code-block:: text + + payload: + shape_rank: uint8 + shape_dims: shape_rank × uint32 LE + dtype_tag: uint8 # 0=int64_q, 1=uint8, etc. (here we use int64_q) + data: |shape| × int64 BE # Q-values (see A.3) + A.2 Domain Separation for Hash Preimages ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2469,10 +2575,12 @@ A.3 Quantized Integer Representation (A2) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Let public step Δ > 0. Quantization Q: ℝ → ℤ is round-to-nearest, ties-to-even: -``` -q = nearest_even(r / Δ), r̂ = q * Δ -|r − r̂| ≤ Δ / 2 -``` + +.. code-block:: text + + q = nearest_even(r / Δ), r̂ = q * Δ + |r − r̂| ≤ Δ / 2 + Vectors/matrices quantize elementwise. Integers are stored as signed 64-bit in big-endian order inside TLVs. Shapes and ranks are stored in LE in the header to keep shape parsing fast; data itself is BE for math portability across toolchains. A.4 Node Preimages & Commitments @@ -2480,31 +2588,41 @@ A.4 Node Preimages & Commitments For node v with id id(v) (32 bytes), parent commitments C(u1..uk), operator metadata meta(v): Base hash (bind operator & params): -``` -preimage_base = DS("NODEBASE") || TLV(op_name) || TLV(op_version) || - TLV(attrs_bytes) || TLV(Q(params_tensor)) -h_base = SHA-256(preimage_base) -``` + +.. code-block:: text + + preimage_base = DS("NODEBASE") || TLV(op_name) || TLV(op_version) || + TLV(attrs_bytes) || TLV(Q(params_tensor)) + h_base = SHA-256(preimage_base) + Leaf commitment (k=0): -``` -preimage_leaf = DS("LEAF") || id(v) || TLV(h_base) -C(v) = SHA-256(preimage_leaf) -``` + +.. code-block:: text + + preimage_leaf = DS("LEAF") || id(v) || TLV(h_base) + C(v) = SHA-256(preimage_leaf) + Internal commitment (k>0), with length-prefix and semantic parent order: -``` -preimage_node = DS("NODE") || id(v) || uint32LE(k) || TLV(h_base) || - Σ_i (uint32LE(32) || C(ui)) # child length fixed at 32 -C(v) = SHA-256(preimage_node) -``` + +.. code-block:: text + + preimage_node = DS("NODE") || id(v) || uint32LE(k) || TLV(h_base) || + Σ_i (uint32LE(32) || C(ui)) # child length fixed at 32 + C(v) = SHA-256(preimage_node) + Model root: -``` -preimage_forest = DS("FOREST") || uint32LE(|O|) || Σ_o (uint32LE(32) || C(o)) -C(M) = SHA-256(preimage_forest) -``` + +.. code-block:: text + + preimage_forest = DS("FOREST") || uint32LE(|O|) || Σ_o (uint32LE(32) || C(o)) + C(M) = SHA-256(preimage_forest) + Activation bind (per-inference): -``` -A(v,x) = SHA-256( DS("ACT") || id(v) || SHA-256(x_preproc_bytes) || TLV(Q(a_v(x))) ) -``` + +.. code-block:: text + + A(v,x) = SHA-256( DS("ACT") || id(v) || SHA-256(x_preproc_bytes) || TLV(Q(a_v(x))) ) + A.5 Canonical Byte Order Sanity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2517,25 +2635,26 @@ A.5 Canonical Byte Order Sanity A.6 Reference Python (encoding & hashing) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -```python -# merkleagi/encoding.py -import struct, hashlib -from typing import Iterable -def le_u32(n: int) -> bytes: return struct.pack(' bytes: return struct.pack('>q', n) -def tlv(tag: int, payload: bytes) -> bytes: - assert 0 <= tag <= 255 - return bytes([tag]) + le_u32(len(payload)) + payload -def ds(label: str) -> bytes: - return (f"MERKLEAGI/V7/{label}\0").encode('ascii') + b'\x01' -def tensor_tlv_int64_q(shape: Iterable[int], data_q: Iterable[int]) -> bytes: - shape = list(shape) - rank = len(shape) - hdr = bytes([rank]) + b''.join(struct.pack(' bytes: return hashlib.sha256(b).digest() -``` +.. code-block:: python + + # merkleagi/encoding.py + import struct, hashlib + from typing import Iterable + def le_u32(n: int) -> bytes: return struct.pack(' bytes: return struct.pack('>q', n) + def tlv(tag: int, payload: bytes) -> bytes: + assert 0 <= tag <= 255 + return bytes([tag]) + le_u32(len(payload)) + payload + def ds(label: str) -> bytes: + return (f"MERKLEAGI/V7/{label}\0").encode('ascii') + b'\x01' + def tensor_tlv_int64_q(shape: Iterable[int], data_q: Iterable[int]) -> bytes: + shape = list(shape) + rank = len(shape) + hdr = bytes([rank]) + b''.join(struct.pack(' bytes: return hashlib.sha256(b).digest() + Appendix B — Deterministic Kernels & LUTs (A2) ---------------------------------------------- @@ -2548,37 +2667,41 @@ B.1 Fixed-Point Convention We use a single global Δ for tensors that participate in proofs. For efficiency, internal kernels may use integer math with scale multipliers: - z = (x * y) / S where S corresponds to Δ scaling (exact integer division with round-to-nearest ties-to-even). RNE function: -```python -def div_rne(num: int, den: int) -> int: - q, r = divmod(num, den) - twice = r * 2 - if twice > den: return q + 1 - if twice < den: return q - # exactly half: ties-to-even - return q + (q & 1) -``` + +.. code-block:: python + + def div_rne(num: int, den: int) -> int: + q, r = divmod(num, den) + twice = r * 2 + if twice > den: return q + 1 + if twice < den: return q + # exactly half: ties-to-even + return q + (q & 1) + B.2 GEMM (int64) with global Δ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Let input A (m×k) and B (k×n) be in Q-space (int64). True real value is A*Δ, B*Δ. Their product real is (AΔ)·(BΔ) = (A·B) Δ². To remain in Q-space we divide by scale=S=1/Δ twice → divide by S² in integer domain. -```python -# merkleagi/quant.py -import numpy as np -from .encoding import le_u32 -def gemm_q(A_q: np.ndarray, B_q: np.ndarray, S: int) -> np.ndarray: - # A_q: (m,k) int64, B_q: (k,n) int64, S = 1/Δ as positive integer - m, k = A_q.shape; k2, n = B_q.shape - assert k == k2 - C = np.zeros((m, n), dtype=np.int64) - for i in range(m): - for j in range(n): - acc = 0 - for t in range(k): - acc += int(A_q[i,t]) * int(B_q[t,j]) # 128-bit accumulator in Python int - C[i,j] = div_rne(acc, S*S) - return C -``` + +.. code-block:: python + + # merkleagi/quant.py + import numpy as np + from .encoding import le_u32 + def gemm_q(A_q: np.ndarray, B_q: np.ndarray, S: int) -> np.ndarray: + # A_q: (m,k) int64, B_q: (k,n) int64, S = 1/Δ as positive integer + m, k = A_q.shape; k2, n = B_q.shape + assert k == k2 + C = np.zeros((m, n), dtype=np.int64) + for i in range(m): + for j in range(n): + acc = 0 + for t in range(k): + acc += int(A_q[i,t]) * int(B_q[t,j]) # 128-bit accumulator in Python int + C[i,j] = div_rne(acc, S*S) + return C + Note: In practice, use 128-bit accumulators in C/LLVM reference kernel; Python int is unbounded and deterministic. B.3 Conv2D (NCHW) as im2col+GEMM @@ -2590,25 +2713,27 @@ B.4 LayerNorm (integer, LUT-backed variance inverse) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ LayerNorm requires 1/sqrt(var + eps). We ship an LUT over a bounded range of (var_q) mapped to inv_sqrt_q. The LUT is deterministically generated: -```python -# merkleagi/lut.py -import math, numpy as np -from .encoding import tlv, ds -def build_inv_sqrt_lut(S: int, max_var_real: float, step_real: float, Δ: float): - # Map var_real ∈ [0, max_var_real] in steps to inv_sqrt quantized - xs = [] - vals = [] - var = 0.0 - while var <= max_var_real + 1e-15: - inv = 1.0 / math.sqrt(var + 1e-12) - xs.append(int(round(var / Δ))) # quantized var bucket (int) - vals.append(int(round(inv / Δ))) # quantized inverse sqrt - var += step_real - # Emit TLV; verifier rebuilds same table - payload = b''.join(int(x).to_bytes(8, 'big', signed=True) for x in xs) + - b''.join(int(v).to_bytes(8, 'big', signed=True) for v in vals) - return tlv(0x07, payload) # lut_table -``` + +.. code-block:: python + + # merkleagi/lut.py + import math, numpy as np + from .encoding import tlv, ds + def build_inv_sqrt_lut(S: int, max_var_real: float, step_real: float, Δ: float): + # Map var_real ∈ [0, max_var_real] in steps to inv_sqrt quantized + xs = [] + vals = [] + var = 0.0 + while var <= max_var_real + 1e-15: + inv = 1.0 / math.sqrt(var + 1e-12) + xs.append(int(round(var / Δ))) # quantized var bucket (int) + vals.append(int(round(inv / Δ))) # quantized inverse sqrt + var += step_real + # Emit TLV; verifier rebuilds same table + payload = b''.join(int(x).to_bytes(8, 'big', signed=True) for x in xs) + + b''.join(int(v).to_bytes(8, 'big', signed=True) for v in vals) + return tlv(0x07, payload) # lut_table + LayerNorm kernel computes mean & variance in int64, looks up inverse sqrt via LUT (nearest bucket), and rescales. B.5 GELU & Softmax (LUT-backed) @@ -2621,11 +2746,13 @@ B.6 Top-k Attention (quantized scores only) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Sort and select on quantized scores (score_q), never floats: -```python -def topk_q(scores_q: np.ndarray, k: int): - idx = np.argsort(scores_q)[::-1][:k] - return idx -``` + +.. code-block:: python + + def topk_q(scores_q: np.ndarray, k: int): + idx = np.argsort(scores_q)[::-1][:k] + return idx + B.7 Kernel Manifest (hash-bound) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2640,89 +2767,94 @@ All proofs are pure data (no code) with strict schemas. C.1 Path Proof ~~~~~~~~~~~~~~~ -```json -{ - "schema_version": "v7.0", - "type": "proof_path", - "root_commit": "<32-byte hex>", - "node_id": "<32-byte hex>", - "path": [ - { - "parent_commit": "<32-byte hex>", - "sibling_hashes": ["<32-byte hex>", "..."], - "position": "left" - } - ], - "node_base": { - "op": "linear", - "op_version": 1, - "attrs": "base64-bytes", - "params_q": { "shape": [m, n], "data_be_i64": "base64" } - } -} -``` +.. code-block:: text + + { + "schema_version": "v7.0", + "type": "proof_path", + "root_commit": "<32-byte hex>", + "node_id": "<32-byte hex>", + "path": [ + { + "parent_commit": "<32-byte hex>", + "sibling_hashes": ["<32-byte hex>", "..."], + "position": "left" + } + ], + "node_base": { + "op": "linear", + "op_version": 1, + "attrs": "base64-bytes", + "params_q": { "shape": [m, n], "data_be_i64": "base64" } + } + } + C.2 ε-Proof at Affine Preactivation (v7-Local) -```json -{ - "schema_version": "v7.0", - "type": "proof_eps_affine", - "root_commit": "<32-byte hex>", - "frontier_id": "enc_string", - "input_hash": "<32-byte hex>", - "p_norm": 1, - "epsilon": 0.05, - "node": { - "id": "<32-byte hex>", - "op": "linear_preact", - "parents": [ - { - "id": "<32-byte hex>", - "activation_q": { "shape": [d], "data_be_i64": "base64" } - } - ], - "weights_q": { "shape": [d, o], "data_be_i64": "base64" }, - "bias_q": { "shape": [o], "data_be_i64": "base64" } - }, - "subset_S_parent_ids": ["<32b hex>", "..."], - "kernel_manifest_digest": "<32-byte hex>", - "delta_check": { "norm_omitted_q": "int64-decimal-string", "norm_total_q": "int64-decimal-string" } -} -``` -Verifier contract: recompute integer z_full_q and z_S_q, check ||z_full_q - z_S_q||_p ≤ ε · ||z_full_q||_p, using kernels whose digest matches kernel_manifest_digest. + +.. code-block:: text + + { + "schema_version": "v7.0", + "type": "proof_eps_affine", + "root_commit": "<32-byte hex>", + "frontier_id": "enc_string", + "input_hash": "<32-byte hex>", + "p_norm": 1, + "epsilon": 0.05, + "node": { + "id": "<32-byte hex>", + "op": "linear_preact", + "parents": [ + { + "id": "<32-byte hex>", + "activation_q": { "shape": [d], "data_be_i64": "base64" } + } + ], + "weights_q": { "shape": [d, o], "data_be_i64": "base64" }, + "bias_q": { "shape": [o], "data_be_i64": "base64" } + }, + "subset_S_parent_ids": ["<32b hex>", "..."], + "kernel_manifest_digest": "<32-byte hex>", + "delta_check": { "norm_omitted_q": "int64-decimal-string", "norm_total_q": "int64-decimal-string" } + } + +Verifier contract: recompute integer z_full_q and z_S_q, check \|\|z_full_q - z_S_q\|\|_p ≤ ε · \|\|z_full_q\|\|_p, using kernels whose digest matches kernel_manifest_digest. C.3 Frontier Declaration ~~~~~~~~~~~~~~~~~~~~~~~~~ -```json -{ - "schema_version": "v7.0", - "type": "frontier_decl", - "frontier_id": "enc_string", - "node_selector": "module:encoder.block.6.mlp.pre_linear", - "op": "linear_preact", - "p_norm": 1 -} -``` +.. code-block:: text + + { + "schema_version": "v7.0", + "type": "frontier_decl", + "frontier_id": "enc_string", + "node_selector": "module:encoder.block.6.mlp.pre_linear", + "op": "linear_preact", + "p_norm": 1 + } + C.4 Reproducibility Manifest ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -```json -{ - "schema_version": "v7.0", - "root_commit": "<32-byte hex>", - "delta": "1e-6", - "kernel_manifest_digest": "<32-byte hex>", - "dataset_digest": "<32-byte hex>", - "code_digest": "<32-byte hex>", - "env": { - "python": "3.12.3", - "torch": "2.4.0", - "platform": "Darwin-25.1 / Linux-6.8" - }, - "audit_mode": "STRICT" -} -``` +.. code-block:: text + + { + "schema_version": "v7.0", + "root_commit": "<32-byte hex>", + "delta": "1e-6", + "kernel_manifest_digest": "<32-byte hex>", + "dataset_digest": "<32-byte hex>", + "code_digest": "<32-byte hex>", + "env": { + "python": "3.12.3", + "torch": "2.4.0", + "platform": "Darwin-25.1 / Linux-6.8" + }, + "audit_mode": "STRICT" + } + Appendix D — Plasticity (Dual Hash) & Separation ------------------------------------------------ @@ -2731,48 +2863,49 @@ Appendix D — Plasticity (Dual Hash) & Separation D.1 Plastic Node (reference) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -```python -# merkleagi/plastic.py -import torch, torch.nn as nn -from .encoding import sha256 -class PlasticNode(nn.Module): - def __init__(self, nid_bytes: bytes, op_bytes: bytes, params_init: torch.Tensor, parents: list['PlasticNode'], hash_dim=256): - super().__init__() - assert len(nid_bytes) == 32 and len(op_bytes) == 32 - self.nid = nid_bytes; self.op = op_bytes - self.params = nn.Parameter(params_init.clone().detach()) - self.parents = parents - self.proj = nn.Linear(self.params.numel() + hash_dim, hash_dim, bias=True) - self._hard: bytes | None = None - self._soft: torch.Tensor | None = None - self.prev_soft: torch.Tensor | None = None - self.is_commutative = False - def compute_soft(self) -> torch.Tensor: - if self._soft is not None: return self._soft - if self.parents: - parent_soft = torch.stack([p.compute_soft() for p in self.parents]).mean(0) - else: - parent_soft = torch.zeros(self.proj.in_features - self.params.numel(), dtype=torch.float32, device=self.params.device) - x = torch.cat([self.params.flatten(), parent_soft]) - self._soft = torch.tanh(self.proj(x)) - return self._soft - def _embed_hard(self) -> torch.Tensor: - h = self.compute_hard() - v = torch.tensor(list(h) + [0]*(256-len(h)), dtype=torch.float32, device=self.params.device) # 32→256 pad - v = v / 255.0 * 2.0 - 1.0 - return v - def plasticity_loss(self, λ1=1.0, λ2=0.1, λ3=0.0) -> torch.Tensor: - s = self.compute_soft() - l_cons = (s - self._embed_hard()).pow(2).sum() - l_smooth = (s - self.prev_soft).pow(2).sum() if self.prev_soft is not None else torch.tensor(0.0, device=s.device) - self.prev_soft = s.detach() - return λ1*l_cons + λ2*l_smooth + λ3*0.0 - def compute_hard(self) -> bytes: - if self._hard is not None: return self._hard - # Quantize params externally and build canonical node preimage (A1+A2), - # then hash. Omitted here for brevity; use dag.commit_node() - raise RuntimeError("Use dag.commit_node() to compute hard hash for PlasticNode") -``` +.. code-block:: python + + # merkleagi/plastic.py + import torch, torch.nn as nn + from .encoding import sha256 + class PlasticNode(nn.Module): + def __init__(self, nid_bytes: bytes, op_bytes: bytes, params_init: torch.Tensor, parents: list['PlasticNode'], hash_dim=256): + super().__init__() + assert len(nid_bytes) == 32 and len(op_bytes) == 32 + self.nid = nid_bytes; self.op = op_bytes + self.params = nn.Parameter(params_init.clone().detach()) + self.parents = parents + self.proj = nn.Linear(self.params.numel() + hash_dim, hash_dim, bias=True) + self._hard: bytes | None = None + self._soft: torch.Tensor | None = None + self.prev_soft: torch.Tensor | None = None + self.is_commutative = False + def compute_soft(self) -> torch.Tensor: + if self._soft is not None: return self._soft + if self.parents: + parent_soft = torch.stack([p.compute_soft() for p in self.parents]).mean(0) + else: + parent_soft = torch.zeros(self.proj.in_features - self.params.numel(), dtype=torch.float32, device=self.params.device) + x = torch.cat([self.params.flatten(), parent_soft]) + self._soft = torch.tanh(self.proj(x)) + return self._soft + def _embed_hard(self) -> torch.Tensor: + h = self.compute_hard() + v = torch.tensor(list(h) + [0]*(256-len(h)), dtype=torch.float32, device=self.params.device) # 32→256 pad + v = v / 255.0 * 2.0 - 1.0 + return v + def plasticity_loss(self, λ1=1.0, λ2=0.1, λ3=0.0) -> torch.Tensor: + s = self.compute_soft() + l_cons = (s - self._embed_hard()).pow(2).sum() + l_smooth = (s - self.prev_soft).pow(2).sum() if self.prev_soft is not None else torch.tensor(0.0, device=s.device) + self.prev_soft = s.detach() + return λ1*l_cons + λ2*l_smooth + λ3*0.0 + def compute_hard(self) -> bytes: + if self._hard is not None: return self._hard + # Quantize params externally and build canonical node preimage (A1+A2), + # then hash. Omitted here for brevity; use dag.commit_node() + raise RuntimeError("Use dag.commit_node() to compute hard hash for PlasticNode") + D.2 Separation Theorem (sketch recap) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2795,20 +2928,22 @@ E.1 Committing Dictionary Columns ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ For dictionary D ∈ ℝ^{d×k}, quantize columns Q(D[:,i]) and create feature nodes: -```python -# merkleagi/dictionary.py -def commit_dictionary_columns(D_q: np.ndarray, parent_id: bytes) -> list[bytes]: - # Returns list of feature node commits C(f_i) - commits = [] - for i in range(D_q.shape[1]): - nid = hashlib.sha256(b'DICTFEAT'+i.to_bytes(4,'big')).digest() - pre_base = ds('NODEBASE') + tlv(0x01, b'dictionary_feature') + tlv(0x01, b'\x00\x00\x00\x01') + - tlv(0x01, b'') + tensor_tlv_int64_q((D_q.shape[0],), D_q[:,i].tolist()) - h_base = sha256(pre_base) - pre_node = ds('NODE') + nid + struct.pack(' list[bytes]: + # Returns list of feature node commits C(f_i) + commits = [] + for i in range(D_q.shape[1]): + nid = hashlib.sha256(b'DICTFEAT'+i.to_bytes(4,'big')).digest() + pre_base = ds('NODEBASE') + tlv(0x01, b'dictionary_feature') + tlv(0x01, b'\x00\x00\x00\x01') + + tlv(0x01, b'') + tensor_tlv_int64_q((D_q.shape[0],), D_q[:,i].tolist()) + h_base = sha256(pre_base) + pre_node = ds('NODE') + nid + struct.pack(' out/env.json -# === 1) Build kernel manifest digest === -python3 - <<'PY' -import hashlib, json, glob -paths = sorted(glob.glob('merkleagi/*.py')) -h = hashlib.sha256() -for p in paths: - with open(p,'rb') as f: h.update(f.read()) -print(json.dumps({"kernel_manifest_digest": h.hexdigest()}, indent=2)) -PY -# === 2) Run bench harness (no fabricated outputs) === -python3 -m bench.runner | tee out/bench_linear.json -# === 3) Build toy DAG and proof === -python3 -m examples.affine_proof_demo | tee out/proof_demo.json -echo "Artifacts in ./out" -``` + +.. code-block:: bash + + #!/usr/bin/env bash + set -euo pipefail + # === 0) Env capture === + python3 -c 'import sys,platform,hashlib,torch,json; + print(json.dumps({ + "python": sys.version, + "platform": platform.platform(), + "torch": torch.__version__ + }, indent=2))' > out/env.json + # === 1) Build kernel manifest digest === + python3 - <<'PY' + import hashlib, json, glob + paths = sorted(glob.glob('merkleagi/*.py')) + h = hashlib.sha256() + for p in paths: + with open(p,'rb') as f: h.update(f.read()) + print(json.dumps({"kernel_manifest_digest": h.hexdigest()}, indent=2)) + PY + # === 2) Run bench harness (no fabricated outputs) === + python3 -m bench.runner | tee out/bench_linear.json + # === 3) Build toy DAG and proof === + python3 -m examples.affine_proof_demo | tee out/proof_demo.json + echo "Artifacts in ./out" + H.2 Manifest Builder ~~~~~~~~~~~~~~~~~~~~~ -```python -# scripts/build_manifest.py -import json, hashlib, glob -from merkleagi.encoding import sha256 -def file_sha256(path): - import hashlib - h=hashlib.sha256() - with open(path,'rb') as f: h.update(f.read()) - return h.hexdigest() -def main(): - code_digest = file_sha256('merkleagi/encoding.py') # extend as needed - dataset_digest = "00"*32 # user to fill - manifest = { - "schema_version":"v7.0", - "root_commit":"00"*32, - "delta":"1e-6", - "kernel_manifest_digest": file_sha256('merkleagi/quant.py'), - "dataset_digest": dataset_digest, - "code_digest": code_digest, - "env": {}, - "audit_mode":"STRICT" - } - print(json.dumps(manifest, indent=2)) -if __name__=='__main__': main() -``` +.. code-block:: python + + # scripts/build_manifest.py + import json, hashlib, glob + from merkleagi.encoding import sha256 + def file_sha256(path): + import hashlib + h=hashlib.sha256() + with open(path,'rb') as f: h.update(f.read()) + return h.hexdigest() + def main(): + code_digest = file_sha256('merkleagi/encoding.py') # extend as needed + dataset_digest = "00"*32 # user to fill + manifest = { + "schema_version":"v7.0", + "root_commit":"00"*32, + "delta":"1e-6", + "kernel_manifest_digest": file_sha256('merkleagi/quant.py'), + "dataset_digest": dataset_digest, + "code_digest": code_digest, + "env": {}, + "audit_mode":"STRICT" + } + print(json.dumps(manifest, indent=2)) + if __name__=='__main__': main() + Implementation Notes (Ground-Truth Practicalities) - All code here is runnable with Python 3.12 + NumPy/PyTorch; it avoids undefined behavior and non-deterministic reductions. - We do not include any measured numbers, checksums, or logs. Run the scripts to generate them on your hardware. @@ -3006,7 +3146,7 @@ B.3 Accumulator width ~~~~~~~~~~~~~~~~~~~~~~ - Integer GEMM/Conv must use accumulators wide enough to avoid overflow: with int64 inputs representing q=⟂r/Δ⟂, the product sum can exceed 64-bit at large k. - Bound: Let max |A_q| ≤ Q_max, max |B_q| ≤ Q_max, k ≤ k_max. Acc bound ≈ k_max * Q_max^2. Require 128-bit accumulators (e.g., __int128 in C/LLVM). + Bound: Let max \|A_q\| ≤ Q_max, max \|B_q\| ≤ Q_max, k ≤ k_max. Acc bound ≈ k_max * Q_max^2. Require 128-bit accumulators (e.g., __int128 in C/LLVM). Action: Our Python reference is safe (bigint). In a native reference, mandate 128-bit accumulation and test overflow guards. Document as MUST in kernel manifest. B.4 Δ and scale S = 1/Δ - Using a single global Δ across proofs is simplest. If teams prefer per-layer Δ, they must commit Δ per node in attrs(v) and propagate scaling in verifier math. @@ -3107,7 +3247,7 @@ E.2 Overflow bounds ~~~~~~~~~~~~~~~~~~~~ For GEMM C = A·B / S²: -- If |A_q| ≤ A_max, |B_q| ≤ B_max, k ≤ k_max, then accumulator bound is k_max·A_max·B_max. Require acc_width ≥ ⌈log2(k_max·A_max·B_max)⌉ + 2 for headroom. +- If \|A_q\| ≤ A_max, \|B_q\| ≤ B_max, k ≤ k_max, then accumulator bound is k_max·A_max·B_max. Require acc_width ≥ ⌈log2(k_max·A_max·B_max)⌉ + 2 for headroom. - Mandate 128-bit accumulators in native kernels; add a manifest flag acc128=true. E.3 LUT error @@ -3187,7 +3327,7 @@ L Minimal Mathematical Additions (tighten the paper) ----------------------------------------------------- Lemma (Monotone L1 composition at a layer). -If w ≥ 0 and a ≥ 0 elementwise at an affine preactivation frontier, then ||z||₁ = ||Σ_u w_u⊙a_u||₁ = Σ_u ||w_u⊙a_u||₁ and local ε-coverage C_S ≥ (1−ε)C_total implies ||z − z_S||₁ ≤ ε·||z||₁. +If w ≥ 0 and a ≥ 0 elementwise at an affine preactivation frontier, then \|\|z\|\|₁ = \|\|Σ_u w_u⊙a_u\|\|₁ = Σ_u \|\|w_u⊙a_u\|\|₁ and local ε-coverage C_S ≥ (1−ε)C_total implies \|\|z − z_S\|\|₁ ≤ ε·\|\|z\|\|₁. Proof: Nonnegativity removes cancellations; triangle inequality is tight. Lemma (RNE determinism). Let den>0. The integer function div_rne(num, den) is deterministic across platforms and equal to nearest-even rounding of the real quotient when numerator/denominator are exact integers.