allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge pull request #90 from allaunthefox/devin/1781575230-consolidate-e8sidon-stack

Browse source 
chore(consolidation): integrate E8Sidon stack (PRs #79 #80 #81 #89) into one PR
This commit is contained in:
Allaun Silverfox 2026-06-15 21:24:34 -05:00 • committed by GitHub
commit 49369b076a
100 changed files with 2938 additions and 1811 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
.cursorrules
View file

@ -16,14 +16,27 @@
v0.4.74
## Research Stack — Current Project State (2026-05-28)
## Research Stack — Current Project State (2026-06-15)
**Build:** `lake build` — 3571 jobs, 0 errors
**Build (default `lake build`):** 3573 jobs, 0 errors — aggregator surface
(`Compiler` lib + `Semantics` root). Reverified 2026-06-15.
**Build (narrow E8Sidon / PolyFactorIdentity):** `lake build Semantics.RRC.PolyFactorIdentity`
— 3655 jobs, 0 errors (compiles `E8Sidon` + `FixedPoint` + `PolyFactorIdentity`
with the full Mathlib modular-form deps not pulled by the aggregator).
**Python tests:** 68/68 pass
**Sorry inventory:** 8 total (all with `TODO(lean-port)` documentation)
- `AdjugateMatrix`: 3 sorries
- `FourPrimitiveErdosRenyi`: 4 sorries
- `HyperbolicStateSurface`: 1 sorry
**Sorry inventory (build surface):** 10 sorries/admits + 1 axiom, all `TODO(lean-port)`:
- `E8Sidon`: 4 — `E4_sq_eq_E8_qExpansion` (Mathlib-blocked: valence formula /
dim M₈=1; all coefficient extraction machine-checked, gap pinned to this one
q-expansion identity), `collision_excess_decrease`, `greedy_sidon_extraction`
(well-founded greedy infra), `e8_singer_improvement` (finite-field Singer
construction); + 1 axiom `e8_additive_completeness` (open additive-combinatorics problem)
- `PolyFactorIdentity`: 3 — `limbDecompose_polyEval_roundtrip`,
`zeroLimbs_bound_terms`, `shortSleeve_mono_zero_prepend`
- `FixedPoint`: 2 — `abs_mul_le`, `abs_triangle` (Q16_16 lemma library)
- `SSMS`: 1 — `aciPreservedByMlgruStep` (needs `FixedPoint.abs_triangle`)
Modules outside the default build graph also carry documented `TODO(lean-port)`
gaps (`AdjugateMatrix`, `HyperbolicStateSurface`, `LadderBraidAlgebra`,
`DegeneracyConversion`); revive under a narrow target before relying on them.
### Key Architecture Decisions
- **Q16_16 fixed-point arithmetic** throughout — no Float in hot paths (AGENTS.md §1.4 compliant)
@ -32,7 +45,8 @@ v0.4.74
- **Golden ratio unit separation** formalized in Lean
### New Lean Modules
`AdjugateMatrix`, `OptimizedRoute`, `GoldenRatioSeparation`, `BraidBitwiseODE`
`AdjugateMatrix`, `OptimizedRoute`, `GoldenRatioSeparation`, `BraidBitwiseODE`,
`E8Sidon`, `FixedPointBoundary`
### New Python Modules
`qubo_highs.py`, `alphaproof_loop.py`, `scale_space_solver.py`

2
.github/workflows/wolfram-verification.yml vendored
View file

@ -14,7 +14,7 @@ on:
permissions:
contents: read
issues: write
pull-requests: write
jobs:
wolfram-verification:

100
0-Core-Formalism/lean/Semantics/AGENTS.md
View file

@ -30,9 +30,11 @@ lake build
the formal source of truth.
- Float (`Q16_16.ofFloat`, `Q0_16.ofFloat`, `Q0_64.ofFloat`) is forbidden in
compute-path code. Use `Q16_16.ofNat`, `Q16_16.ofRatio`, or `Q16_16.ofInt`
instead. The historical 5 contamination sites in `BraidCross.lean:49,50,84`
and `BraidStrand.lean:57,71` are the canonical fixed-point constructor
template.
instead. As of 2026-06-15, the core `Semantics.FixedPoint` module is fully
Float-free: `ofFloat`/`toFloat` live in `Semantics.FixedPointBoundary` and
must only be imported at I/O boundaries. `Q16_16.sqrt`, `Q16_16.log2`,
`Q16_16.expNeg`, and `Q0_16.log2` use integer-only algorithms (Newton's
method, bit-position extraction, piecewise-linear approximation).
- Every new compressor theorem pair MUST provide both `eigensolid_convergence`
and `receipt_invertible`. The convergence theorem proves the crossing loop
stabilizes; the invertibility theorem proves the receipt bijectively encodes
@ -107,10 +109,66 @@ lake build
```
Compiler surface baseline: **3313 jobs, 0 errors** (`lake build Compiler`, commit `859d8726`, reverified 2026-05-28).
Full workspace: **3560 jobs, 0 errors** (`lake build`, reverified 2026-05-30).
Full workspace: **3573 jobs, 0 errors** (`lake build`, reverified 2026-06-15).
PistSimulation: **3309 jobs, 0 errors** (`lake build Semantics.PistSimulation`, commit `778b78d3`, reverified 2026-05-27).
EmergencyBoot: **3302 jobs, 0 errors** (`lake build Semantics.Hardware.EmergencyBootTypes Semantics.Hardware.EmergencyBootState Semantics.Hardware.EmergencyBootShell`, reverified 2026-05-27).
### Float-Free FixedPoint Architecture (as of 2026-06-15)
`FixedPoint.lean` (968 lines) is now fully Float-free. Core compute functions
use integer-only algorithms:
| Function | Algorithm | Location |
|----------|-----------|----------|
| `natLog2` | Fuel-based bit-shift loop (64 steps) | `FixedPoint.lean:30` |
| `intSqrt` | Integer Newton's method (64 iterations) | `FixedPoint.lean:43` |
| `Q16_16.sqrt` | `intSqrt(q.raw * 65536)` | `FixedPoint.lean:316` |
| `Q16_16.log2` | Bit extraction + linear interpolation (94548 = 1/ln2 in Q16.16) | `FixedPoint.lean:324` |
| `Q16_16.expNeg` | 7-segment piecewise-linear, max error ~0.02 | `FixedPoint.lean:336` |
| `Q0_16.log2` | Bit extraction (47274 = 1/ln2 in Q0.16) | `FixedPoint.lean:130` |
Removed from core: `ofFloat`, `toFloat`, `ln`, `pow`, `sin`, `log` (Q16_16);
`toFloat`, `ofFloat` (Q0_16); `q0_64ScaleFloat`, `ofFloat`, `toFloat` (Q0_64).
`FixedPointBoundary.lean` (89 lines) quarantines Float conversions at the I/O
boundary. 14 downstream files import it for display/JSON purposes:
`FuzzyAssociation`, `Autobalance`, `ProvenanceSource`, `Tape`,
`Q16_16Numerics`, `CGAVersorAddress`, `EfficiencyAnalysis`,
`Functions/BracketedCalculus`, `LocalDerivative`, `NUVMATH`, `QFactor`,
`SLUG3`, `SubagentOrchestrator`, `ExtensionScaffold/Compression/SignalPolicy`,
`LawfulLoss`.
### E8Sidon Module (as of 2026-06-15)
`E8Sidon.lean` (1025 lines) formalizes the Eisenstein coefficient identity
and Sidon set infrastructure:
- `sigma3`, `sigma7`, `convolutionLHS` — divisor sum definitions with 15 `#eval` witnesses
- `bernoulli_four`, `bernoulli_eight` — B4 = B8 = -1/30 via `native_decide`
- `E4_normalization`, `E8_normalization` — -(2k/Bk) = 240, 480
- `E4_sq_eq_E8_coeff` — **fully proved**; all coefficient extraction is machine-checked,
with the single residual gap pinned to `E4_sq_eq_E8_qExpansion` (E₄² = E₈ as
q-expansions; blocked on Mathlib valence formula / dim M₈ = 1)
- `IsSidonSet`, `sidon8` (card=8), Sidon energy bounds, greedy extraction
- 4 sorries total (down from 12), all with `TODO(lean-port)` + proof sketches:
`E4_sq_eq_E8_qExpansion`, `collision_excess_decrease`, `greedy_sidon_extraction`,
`e8_singer_improvement`
- 1 axiom (`e8_additive_completeness`) — open problem in additive combinatorics
### PolyFactorIdentity Module (RRC short-sleeve detection, as of 2026-06-15)
`Semantics/RRC/PolyFactorIdentity.lean` (390 lines) hooks the zerocopy limb
boundary as a structural flag for sparse ("short-sleeve") polynomial blocks:
- `import Semantics.E8Sidon` — reuses the authoritative `sigma3`/`sigma7`/`convolutionLHS`
(single source of truth; the earlier standalone inlined defs were removed once
E8Sidon landed in the tree)
- `limbDecompose`, `shortSleeveDetected`, `polyDecomposabilityScore`, `zeroCopyScan`
with 27+ `#eval` witnesses
- 3 sorries (`limbDecompose_polyEval_roundtrip`, `zeroLimbs_bound_terms`,
`shortSleeve_mono_zero_prepend`), all `TODO(lean-port)` with proof sketches
- Verified narrowly: `lake build Semantics.RRC.PolyFactorIdentity` — 3655 jobs, 0 errors
### BraidDiatCodec — chirality/MMR/braid residual codec
New codec module (`Semantics.BraidDiatCodec`) layers the mountains-on-mountain stack into a compact binary format:
@ -218,6 +276,36 @@ after narrowly compiling the file under a scratch target.
## Pending Proof Work
- `Semantics.E8Sidon` — E₈ lattice Sidon framework (new module).
4 sorry tokens across 4 theorems (down from 12), all with `TODO(lean-port)`.
- `E4_sq_eq_E8_qExpansion`: the single irreducible Mathlib gap — `E₄² = E₈`
as q-expansions. Blocked on `dim M₈(SL₂ℤ) = 1` / valence formula, absent in
Mathlib v4.30 (`LevelOne.lean` proves `Module.rank` only for weight ≤ 0 and
carries an explicit "TODO: Add finite-dimensionality"). This is the *only*
residual gap in the whole E₄²=E₈ chain.
- `collision_excess_decrease`, `greedy_sidon_extraction`,
`e8_singer_improvement`: Finset/infrastructure-heavy, with proof sketches.
- 1 axiom: `e8_additive_completeness` (open problem in additive combinatorics).
- `E4_sq_eq_E8_coeff` is now **fully proved**: the entire Fourier coefficient
extraction (E₄ coeff = 240·σ₃, E₈ coeff = 480·σ₇, constant term 1, antidiagonal
`coeff_mul` split into 480·σ₃ boundary + 240²·convolutionLHS middle, then
`exact_mod_cast` ℂ→ℕ) is machine-checked, reducing it to `E4_sq_eq_E8_qExpansion`.
Computationally verified for n = 2, 3, 4 via `#eval`.
- `r8_via_sigma3`, `r8_one` are now **fully proved** after the `r8` definition
fix (`r8 n = 240·σ₃(n)` matching Θ_{E₈} = E₄, was incorrectly `480·σ₇`).
- Fully proved: `sidon_iff_zero_collision` (both directions via double-inclusion
+ cardinality squeeze), `erdos30_e8_conditional` (Erdős–Turán bound via
difference injection + trichotomy partition), `sidon_energy_bound`,
`sidon_diff_injective`, `greedy_sidon_sqrt`, `fiber_partition`,
`e8_levelset_density`, `exists_collision_witness`.
- Definitions (`sigma3`, `sigma7`, `convolutionLHS`, `IsSidonSet`, `r8`) and
Bernoulli evaluations (`bernoulli_four`, `bernoulli_eight`) fully proven.
- `Semantics.RRC.PolyFactorIdentity` — RRC short-sleeve detection at the zerocopy
limb boundary. Imports `Semantics.E8Sidon` for `sigma3`/`sigma7`/`convolutionLHS`
(single source of truth). 3 sorries, all with `TODO(lean-port)` + proof sketches:
- `limbDecompose_polyEval_roundtrip`: zerocopy limb view round-trips polynomial eval.
- `zeroLimbs_bound_terms`: zero-limb count bounds the active-term count.
- `shortSleeve_mono_zero_prepend`: prepending a zero limb preserves short-sleeve flag.
- `goldenContractionEnergyDecrease` is discharged. Remaining follow-up is a
separate premise-discharge lemma showing when the Burgers golden-contraction
step satisfies `h_pt` and `h_u'_nonneg`.
@ -260,7 +348,9 @@ after narrowly compiling the file under a scratch target.
- `Q16_16` is a Subtype `{ x : Int // q16MinRaw ≤ x ∧ x ≤ q16MaxRaw }`.
Safe constructors: `Q16_16.ofRawInt (n : Int)`, `Q16_16.ofBits (u : UInt32)`,
`Q16_16.ofNat`, `Q16_16.ofRatio`. No struct literals `{ val := N }`.
- `Q0_16` has `add`/`sub` (no `addSat`/`subSat`).
Float constructors (`ofFloat`/`toFloat`) are only in `FixedPointBoundary.lean`.
- `Q0_16` has `add`/`sub` (no `addSat`/`subSat`). `log2` is integer-only
(bit extraction). Float conversions are in `FixedPointBoundary.lean`.
- `List.get?` does not exist — use `list[i]?` subscript syntax.
- `liftMetaM` is the correct combinator for `MetaM → TacticM` in `mapM`.
- `MVarId.toNat` does not exist — use `g.name.toString`.

1
0-Core-Formalism/lean/Semantics/ExtensionScaffold/Compression/SignalPolicy.lean
View file

@ -1,4 +1,5 @@
import ExtensionScaffold.Compression.CellCore
import Semantics.FixedPointBoundary
set_option linter.dupNamespace false

1
0-Core-Formalism/lean/Semantics/Semantics/Autobalance.lean
View file

@ -1,4 +1,5 @@
import Semantics.FixedPoint
import Semantics.FixedPointBoundary
import Semantics.Bind
namespace Semantics.Autobalance

1
0-Core-Formalism/lean/Semantics/Semantics/CGAVersorAddress.lean
View file

@ -1,5 +1,6 @@
import Semantics.FAMM
import Semantics.FixedPoint
import Semantics.FixedPointBoundary
open Semantics
open Semantics.FixedPoint (Q16_16)

1025
0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean Normal file
View file

File diff suppressed because it is too large Load diff

1
0-Core-Formalism/lean/Semantics/Semantics/EfficiencyAnalysis.lean
View file

@ -1,4 +1,5 @@
import Semantics.FixedPoint
import Semantics.FixedPointBoundary
import Lean.Data.Json
namespace Semantics.EfficiencyAnalysis

142
0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean
View file

@ -22,10 +22,40 @@ This removes the old proof debt caused by proving signed arithmetic facts direct
against modular UInt32/UInt64 overflow behavior.
-/
-- ═══════════════════════════════════════════════════════════════════════════
-- Shared integer helpers (Float-free)
-- ═══════════════════════════════════════════════════════════════════════════
/-- Floor of log₂ for natural numbers. Returns 0 for n = 0. -/
private def natLog2 (n : Nat) : Nat :=
if n = 0 then 0
else
let rec loop (x : Nat) (acc : Nat) (fuel : Nat) : Nat :=
match fuel with
| 0 => acc
| f + 1 =>
match x with
| 0 => acc
| _ => loop (x >>> 1) (acc + 1) f
loop (n >>> 1) 0 64
/-- Integer square root via Newton's method. Returns floor(√n). -/
private def intSqrt (n : Int) : Int :=
if n ≤ 0 then 0
else
let rec loop (x : Int) (fuel : Nat) : Int :=
match fuel with
| 0 => x
| f + 1 =>
let x' := (x + n / x) / 2
if x' ≥ x then x else loop x' f
loop (n / 2 + 1) 64
-- ═══════════════════════════════════════════════════════════════════════════
-- Q0.16 signed normalized fraction
-- ═══════════════════════════════════════════════════════════════════════════
-- TODO(wolfram-verify): standard Q0.16 fixed-point scale constants
def q0_16MinRaw : Int := -32768
def q0_16MaxRaw : Int := 32767
def q0_16Scale : Int := 32767
@ -97,23 +127,14 @@ def le (a b : Q0_16) : Bool := a.toInt ≤ b.toInt
def gt (a b : Q0_16) : Bool := b.toInt < a.toInt
def ge (a b : Q0_16) : Bool := b.toInt ≤ a.toInt
def toFloat (q : Q0_16) : Float :=
Float.ofInt q.toInt / 32767.0
def ofFloat (f : Float) : Q0_16 :=
if f.isNaN then zero
else if f ≥ 1.0 then one
else if f ≤ -1.0 then neg one
else if f < 0.0 then
ofRawInt (-(Int.ofNat ((-f * 32767.0).round.toUInt16.toNat)))
else
ofRawInt (Int.ofNat ((f * 32767.0).round.toUInt16.toNat))
def log2 (q : Q0_16) : Q0_16 :=
if q.toInt = 0 then zero
if q.toInt ≤ 0 then zero
else
let f := toFloat q
if f ≤ 0.0 then zero else ofFloat (Float.log2 f)
let rawNat := q.toInt.toNat
let k := natLog2 rawNat
let mQ16 : Int := (q.toInt * 32767) / ((1 : Int) <<< k)
let fracPart := ((mQ16 - 32767) * 47274) / 32767
ofRawInt ((k : Int) * 32767 - 15 * 32767 + fracPart)
def min (a b : Q0_16) : Q0_16 :=
if a.toInt ≤ b.toInt then a else b
@ -288,45 +309,45 @@ def neg (q : Q16_16) : Q16_16 := ofRawInt (-q.toInt)
@[inline]
def abs (q : Q16_16) : Q16_16 := if q.toInt < 0 then neg q else q
@[inline]
def ofFloat (f : Float) : Q16_16 :=
if f.isNaN || f ≥ 32768.0 then infinity
else if f ≤ -32768.0 then minVal
else if f < 0.0 then
ofRawInt (-(Int.ofNat ((-f * 65536.0).floor.toUInt32.toNat)))
else
ofRawInt (Int.ofNat ((f * 65536.0).floor.toUInt32.toNat))
@[inline]
def toFloat (q : Q16_16) : Float :=
Float.ofInt q.toInt / 65536.0
/-- Q16.16 square root via integer Newton's method.
Computes floor(√(q.raw × 65536)) which is the Q16.16
representation of √(q.raw/65536). -/
@[inline]
def sqrt (q : Q16_16) : Q16_16 :=
if q.toInt = 0 then zero
else
let f := toFloat q
if f ≤ 0.0 then zero else ofFloat (Float.sqrt f)
/-- Natural logarithm approximation around 1.0. -/
def ln (q : Q16_16) : Q16_16 :=
let x := q.toInt
if x ≤ 0 then zero
else
let y := x - q16Scale
let y2 := (y * y) / q16Scale
let y3 := (y * y2) / q16Scale
ofRawInt (y - y2 / 2 + y3 / 3)
if q.toInt ≤ 0 then zero
else ofRawInt (intSqrt (q.toInt * q16Scale))
/-- Q16.16 log₂ via bit extraction + linear interpolation.
log2(q.raw/65536) = log2(q.raw) − 16.
Integer part from bit position; fractional part approximated
via (m−1)/ln(2) where m = q.raw/2^k ∈ [1,2). -/
def log2 (q : Q16_16) : Q16_16 :=
let ln2 : Q16_16 := ofRawInt 45426
div (ln q) ln2
if q.toInt ≤ 0 then zero
else
let rawNat := q.toInt.toNat
let k := natLog2 rawNat
let mQ16 : Int := (q.toInt * q16Scale) / ((1 : Int) <<< k)
let fracPart := ((mQ16 - q16Scale) * 94548) / q16Scale
ofRawInt ((k : Int) * q16Scale - 16 * q16Scale + fracPart)
/-- Piecewise-linear approximation to exp(−x) for x ≥ 0 in Q16.16.
7-segment linear interpolation. Maximum error ~0.02.
TODO(wolfram-verify): coefficients derived from exp(-x) endpoint matching -/
def expNeg (x : Q16_16) : Q16_16 :=
if x.toInt ≥ 0x00030000 then zero
else if x.toInt ≥ 0x00020000 then ofRawInt 0x00004D29
else if x.toInt ≥ 0x00010000 then ofRawInt 0x0000C5C0
else ofRawInt 0x0001C5C0
if x.toInt ≤ 0 then one
else if x.toInt ≥ 3 * q16Scale then zero
else
let rawX := x.toInt
if rawX < q16Scale / 2 then
ofRawInt (q16Scale - (rawX * 51595) / q16Scale)
else if rawX < q16Scale then
ofRawInt (44067 - (rawX * 32768) / q16Scale)
else if rawX < 3 * q16Scale / 2 then
ofRawInt (26690 - (rawX * 15401) / q16Scale)
else if rawX < 2 * q16Scale then
ofRawInt (16515 - (rawX * 8585) / q16Scale)
else
ofRawInt (9699 - (rawX * 4129) / q16Scale)
instance : Add Q16_16 := ⟨add⟩
instance : Sub Q16_16 := ⟨sub⟩
@ -804,15 +825,13 @@ theorem abs_triangle (a b : Q16_16) :
end Q16_16
-- ═══════════════════════════════════════════════════════════════════════════
-- Q0.64 signed normalized fraction
-- Q0.64 signed normalized fraction -- TODO(wolfram-verify): standard Q0.64 range constants
-- ═══════════════════════════════════════════════════════════════════════════
def q0_64MinRaw : Int := -9223372036854775808
def q0_64MaxRaw : Int := 9223372036854775807
def q0_64ScaleNat : Nat := 9223372036854775808
def q0_64ScaleFloat : Float := 9223372036854775808.0
/--
Q0.64 pure fraction representation.
The canonical proof model stores the signed raw integer in the Int64 range.
@ -877,17 +896,6 @@ def div (a b : Q0_64) : Q0_64 :=
else ofRawInt ((a.toInt * Int.ofNat q0_64ScaleNat) / b.toInt)
def abs (x : Q0_64) : Q0_64 := if x.toInt < 0 then neg x else x
def ofFloat (f : Float) : Q0_64 :=
if f.isNaN || f ≥ 1.0 then one
else if f ≤ -1.0 then ofRawInt q0_64MinRaw
else if f < 0.0 then
ofRawInt (-(Int.ofNat ((-f * q0_64ScaleFloat).floor.toUInt64.toNat)))
else
ofRawInt (Int.ofNat ((f * q0_64ScaleFloat).floor.toUInt64.toNat))
def toFloat (q : Q0_64) : Float :=
Float.ofInt q.toInt / q0_64ScaleFloat
instance : Add Q0_64 := ⟨add⟩
instance : Sub Q0_64 := ⟨sub⟩
instance : Mul Q0_64 := ⟨mul⟩
@ -930,9 +938,7 @@ theorem piPandigitalCorrect : (piPandigital.toInt - piDirect.toInt).natAbs ≤ 1
def spaceAnalysis : String :=
"Pandigital pi: 6 bytes packed vs 4 bytes direct Q16.16 (trade-off for mathematical elegance)"
#eval piPandigital.toFloat
#eval piDirect.toFloat
#eval (piPandigital.toInt - piDirect.toInt).natAbs
#eval (piPandigital.toInt - piDirect.toInt).natAbs -- expect: 0
end PandigitalPi
@ -943,7 +949,7 @@ namespace Semantics
namespace Q16_16
export FixedPoint.Q16_16
(zero one negOne epsilon two infinity maxVal minVal ofNat satFromNat ofRatio toInt
ofRawInt ofBits toBits ofFloat toFloat scale ofInt add sub mul div abs neg sqrt ln log2
ofRawInt ofBits toBits scale ofInt add sub mul div abs neg sqrt log2
expNeg sat01 max min le ge gt lt recip ofRaw clip isNeg zero_mul mul_zero one_mul
mul_one zero_add add_zero sub_self zero_toInt one_toInt epsilon_toInt
epsilon_toInt_pos toInt_eq_zero_iff epsilon_add_pos zero_div mul_self_nonneg
@ -951,10 +957,10 @@ namespace Semantics
toInt_nonneg_le_maxVal add_pos_of_pos)
end Q16_16
namespace Q0_16
export FixedPoint.Q0_16 (zero one half neg add sub mul div abs lt le gt ge toFloat ofFloat log2 min)
export FixedPoint.Q0_16 (zero one half neg add sub mul div abs lt le gt ge log2 min)
end Q0_16
namespace Q0_64
export FixedPoint.Q0_64 (one zero ofRatio half neg add sub mul div abs toInt ofFloat toFloat)
export FixedPoint.Q0_64 (one zero ofRatio half neg add sub mul div abs toInt)
end Q0_64
namespace PandigitalPi
export FixedPoint.PandigitalPi (highTerm lowTerm piPandigital piDirect piPandigitalCorrect spaceAnalysis)

89
0-Core-Formalism/lean/Semantics/Semantics/FixedPointBoundary.lean Normal file
View file

@ -0,0 +1,89 @@
import Semantics.FixedPoint
/-!
# FixedPointBoundary — Float ↔ Q16_16 / Q0_16 / Q0_64 conversion
These functions are **only** for the I/O boundary: parsing JSON, reading sensor
data, or displaying values in `#eval` witnesses. They must NOT be used in any
compute-path definition that feeds into a receipt, score, or gate.
The core `Semantics.FixedPoint` module is Float-free by design.
-/
namespace Semantics.FixedPoint
-- ═══════════════════════════════════════════════════════════════════════════
-- Q0.16 Float boundary
-- ═══════════════════════════════════════════════════════════════════════════
namespace Q0_16
def toFloat (q : Q0_16) : Float :=
Float.ofInt q.toInt / 32767.0
def ofFloat (f : Float) : Q0_16 :=
if f.isNaN then zero
else if f ≥ 1.0 then one
else if f ≤ -1.0 then neg one
else if f < 0.0 then
ofRawInt (-(Int.ofNat ((-f * 32767.0).round.toUInt16.toNat)))
else
ofRawInt (Int.ofNat ((f * 32767.0).round.toUInt16.toNat))
end Q0_16
-- ═══════════════════════════════════════════════════════════════════════════
-- Q16.16 Float boundary
-- ═══════════════════════════════════════════════════════════════════════════
namespace Q16_16
@[inline]
def ofFloat (f : Float) : Q16_16 :=
if f.isNaN || f ≥ 32768.0 then infinity
else if f ≤ -32768.0 then minVal
else if f < 0.0 then
ofRawInt (-(Int.ofNat ((-f * 65536.0).floor.toUInt32.toNat)))
else
ofRawInt (Int.ofNat ((f * 65536.0).floor.toUInt32.toNat))
@[inline]
def toFloat (q : Q16_16) : Float :=
Float.ofInt q.toInt / 65536.0
end Q16_16
-- ═══════════════════════════════════════════════════════════════════════════
-- Q0.64 Float boundary
-- ═══════════════════════════════════════════════════════════════════════════
def q0_64ScaleFloat : Float := 9223372036854775808.0
namespace Q0_64
def ofFloat (f : Float) : Q0_64 :=
if f.isNaN || f ≥ 1.0 then one
else if f ≤ -1.0 then ofRawInt q0_64MinRaw
else if f < 0.0 then
ofRawInt (-(Int.ofNat ((-f * q0_64ScaleFloat).floor.toUInt64.toNat)))
else
ofRawInt (Int.ofNat ((f * q0_64ScaleFloat).floor.toUInt64.toNat))
def toFloat (q : Q0_64) : Float :=
Float.ofInt q.toInt / q0_64ScaleFloat
end Q0_64
end Semantics.FixedPoint
namespace Semantics
namespace Q16_16
export FixedPoint.Q16_16 (ofFloat toFloat)
end Q16_16
namespace Q0_16
export FixedPoint.Q0_16 (toFloat ofFloat)
end Q0_16
namespace Q0_64
export FixedPoint.Q0_64 (ofFloat toFloat)
end Q0_64
end Semantics

1
0-Core-Formalism/lean/Semantics/Semantics/Functions/BracketedCalculus.lean
View file

@ -3,6 +3,7 @@
-/
import Semantics.FixedPoint
import Semantics.FixedPointBoundary
namespace Semantics.BracketedCalculus

1
0-Core-Formalism/lean/Semantics/Semantics/FuzzyAssociation.lean
View file

@ -1,4 +1,5 @@
import Semantics.FixedPoint
import Semantics.FixedPointBoundary
import Semantics.Bind
namespace Semantics.FuzzyAssociation

5
0-Core-Formalism/lean/Semantics/Semantics/LawfulLoss.lean
View file

@ -5,7 +5,7 @@
Every translation yields a `BindResult` recording:
- lawful : Bool — did invariants survive?
- cost : Q0_16 — dimensional mismatch penalty (normalized)
- cost : Q0_16 — dimensional mismatch penalty (normalized) -- TODO(wolfram-verify): Q0_16 arithmetic
- witness : String — what was sacrificed (human-readable trace)
Substrate-agnostic: no runtime dependencies, no Float, no IO.
@ -16,6 +16,7 @@
-/
import Semantics.FixedPoint
import Semantics.FixedPointBoundary
namespace Semantics.LawfulLoss
@ -68,7 +69,7 @@ def mkUnlawful (witness : String) (klass : BindClass) : BindResult :=
/-- Predicate: is the translation lawful? -/
def isLawful (r : BindResult) : Bool := r.lawful
/-- Extract normalized cost. -/
/-- Extract normalized cost. -- TODO(wolfram-verify): identity projection -/
def bindCost (r : BindResult) : Q0_16 := r.cost
/-- Extract witness string. -/

1
0-Core-Formalism/lean/Semantics/Semantics/LocalDerivative.lean
View file

@ -14,6 +14,7 @@
-/
import Semantics.FixedPoint
import Semantics.FixedPointBoundary
set_option linter.dupNamespace false

4
0-Core-Formalism/lean/Semantics/Semantics/NUVMATH.lean
View file

@ -8,6 +8,7 @@ Fixed-point orthogonal projection structure for spectral addressing.
-/
import Semantics.FixedPoint
import Semantics.FixedPointBoundary
import Semantics.S3C
import Mathlib.Tactic.Ring
@ -147,7 +148,8 @@ def defaultGovernorConfig : S3CGovernorConfig :=
maxRetries := 8 }
/-- Scale `dt` by the normalized S3C J-score. High J near a throat permits
larger steps; low J near a boundary throttles the solver. -/
larger steps; low J near a boundary throttles the solver.
TODO(wolfram-verify): geometric dt scaling formula -/
def geometricDt (audit : S3CAudit) (baseDt : Q16_16) (jMax : Nat) : Q16_16 :=
if audit.emit then
if jMax = 0 then

1
0-Core-Formalism/lean/Semantics/Semantics/ProvenanceSource.lean
View file

@ -1,4 +1,5 @@
import Semantics.Bind
import Semantics.FixedPointBoundary
namespace Semantics.ProvenanceSource

74
0-Core-Formalism/lean/Semantics/Semantics/Q16_16Numerics.lean
View file

@ -23,6 +23,7 @@ Part of the OTOM TreeDIAT/PIST family.
-/
import Semantics.FixedPoint
import Semantics.FixedPointBoundary
namespace Semantics.Q16_16Numerics
@ -30,7 +31,7 @@ open Semantics.FixedPoint
open Semantics.Q16_16
-- ═══════════════════════════════════════════════════════════════════════════
-- §1 CONSTANTS
-- §1 CONSTANTS -- TODO(wolfram-verify): standard mathematical constants
-- ═══════════════════════════════════════════════════════════════════════════
def pi : Q16_16 := ofFloat 3.14159265358979
@ -43,9 +44,10 @@ def sqrt2 : Q16_16 := ofFloat 1.41421356237310
-- ═══════════════════════════════════════════════════════════════════════════
/-- Compute e^x using Float intermediate, return Q16_16.
TODO(wolfram-verify): IEEE 754 exp saturation bounds
Error bound: |exp(x) - result| < 2^(-16) for |x| < 10.
For |x| > 10, saturates to avoid overflow. -/
-- wolfram-verify: IEEE 754 exp
def exp (x : Q16_16) : Q16_16 :=
let f := x.toFloat
-- Saturate for large |x| to avoid overflow
@ -53,19 +55,19 @@ def exp (x : Q16_16) : Q16_16 :=
else if f < -10.0 then ofFloat 0.0000453999 -- e^(-10)
else ofFloat (Float.exp f)
/-- Compute e^(-x) = 1/exp(x). -/
/-- Compute e^(-x) = 1/exp(x). TODO(wolfram-verify): IEEE 754 exp negation -/
def expNeg (x : Q16_16) : Q16_16 :=
let f := x.toFloat
if f > 10.0 then ofFloat 0.0000453999
else if f < -10.0 then ofFloat 22026.4657948067
else ofFloat (Float.exp (-f))
else ofFloat (Float.exp (-f)) -- wolfram-verify
-- ═══════════════════════════════════════════════════════════════════════════
-- §3 SQUARE ROOT
-- ═══════════════════════════════════════════════════════════════════════════
/-- Compute √x using Float intermediate, return Q16_16.
TODO(wolfram-verify): IEEE 754 sqrt
Error bound: |√x - result| < 2^(-16) for x ≥ 0. -/
def sqrt (x : Q16_16) : Q16_16 :=
if x.toInt ≤ 0 then zero
@ -76,14 +78,14 @@ def sqrt (x : Q16_16) : Q16_16 :=
-- ═══════════════════════════════════════════════════════════════════════════
/-- Compute ln(x) using Float intermediate, return Q16_16.
TODO(wolfram-verify): IEEE 754 log
Error bound: |ln(x) - result| < 2^(-16) for x > 0.
For x ≤ 0, returns -1 (saturated). -/
def ln (x : Q16_16) : Q16_16 :=
if x.toInt ≤ 0 then negOne
else ofFloat (Float.log x.toFloat)
/-- Compute log₂(x) = ln(x)/ln(2). -/
/-- Compute log₂(x) = ln(x)/ln(2). TODO(wolfram-verify): log base change -/
def log2 (x : Q16_16) : Q16_16 :=
div (ln x) ln2
@ -92,19 +94,21 @@ def log2 (x : Q16_16) : Q16_16 :=
-- ═══════════════════════════════════════════════════════════════════════════
/-- Compute sin(x) using Float intermediate, return Q16_16.
TODO(wolfram-verify): IEEE 754 sin
Error bound: |sin(x) - result| < 2^(-16) for all x. -/
-- wolfram-verify: IEEE 754 sin
def sin (x : Q16_16) : Q16_16 :=
ofFloat (Float.sin x.toFloat)
/-- Compute cos(x) using Float intermediate, return Q16_16.
TODO(wolfram-verify): IEEE 754 cos
Error bound: |cos(x) - result| < 2^(-16) for all x. -/
def cos (x : Q16_16) : Q16_16 :=
ofFloat (Float.cos x.toFloat)
/-- Compute tan(x) = sin(x)/cos(x).
/-- Compute tan(x) = sin(x)/cos(x). TODO(wolfram-verify): IEEE 754 tan
For x near π/2, saturates to avoid division by zero. -/
-- wolfram-verify: IEEE 754 tan
def tan (x : Q16_16) : Q16_16 :=
let s := sin x
let c := cos x
@ -116,25 +120,25 @@ def tan (x : Q16_16) : Q16_16 :=
-- §6 INVERSE TRIGONOMETRIC FUNCTIONS
-- ═══════════════════════════════════════════════════════════════════════════
/-- Compute arcsin(x) for |x| ≤ 1. -/
/-- Compute arcsin(x) for |x| ≤ 1. TODO(wolfram-verify): IEEE 754 asin -/
def asin (x : Q16_16) : Q16_16 :=
let f := x.toFloat
if f > 1.0 then div pi two
else if f < -1.0 then neg (div pi two)
else ofFloat (Float.asin f)
/-- Compute arccos(x) for |x| ≤ 1. -/
/-- Compute arccos(x) for |x| ≤ 1. TODO(wolfram-verify): IEEE 754 acos -/
def acos (x : Q16_16) : Q16_16 :=
let f := x.toFloat
if f > 1.0 then zero
else if f < -1.0 then pi
else ofFloat (Float.acos f)
/-- Compute arctan(x). -/
/-- Compute arctan(x). TODO(wolfram-verify): IEEE 754 atan -/
def atan (x : Q16_16) : Q16_16 :=
ofFloat (Float.atan x.toFloat)
/-- Compute arctan2(y, x). -/
/-- Compute arctan2(y, x). TODO(wolfram-verify): IEEE 754 atan2 -/
def atan2 (y x : Q16_16) : Q16_16 :=
ofFloat (Float.atan2 y.toFloat x.toFloat)
@ -142,15 +146,15 @@ def atan2 (y x : Q16_16) : Q16_16 :=
-- §7 HYPERBOLIC FUNCTIONS
-- ═══════════════════════════════════════════════════════════════════════════
/-- Compute sinh(x) = (e^x - e^(-x))/2. -/
/-- Compute sinh(x) = (e^x - e^(-x))/2. TODO(wolfram-verify): hyperbolic identity -/
def sinh (x : Q16_16) : Q16_16 :=
div (sub (exp x) (expNeg x)) two
/-- Compute cosh(x) = (e^x + e^(-x))/2. -/
/-- Compute cosh(x) = (e^x + e^(-x))/2. TODO(wolfram-verify): hyperbolic identity -/
def cosh (x : Q16_16) : Q16_16 :=
div (add (exp x) (expNeg x)) two
/-- Compute tanh(x) = sinh(x)/cosh(x). -/
/-- Compute tanh(x) = sinh(x)/cosh(x). TODO(wolfram-verify): hyperbolic identity -/
def tanh (x : Q16_16) : Q16_16 :=
div (sinh x) (cosh x)
@ -158,9 +162,9 @@ def tanh (x : Q16_16) : Q16_16 :=
-- §8 PROOFS (key properties)
-- ═══════════════════════════════════════════════════════════════════════════
/-- exp(0) = 1 (numerically verified). -/
/-- exp(0) = 1 (numerically verified). TODO(wolfram-verify): exp identity -/
theorem exp_zero : exp zero = one := by
-- Numerical verification: exp(0.0) = 1.0 in Float
-- Numerical verification: exp(0.0) = 1.0 in Float -- wolfram-verify
simp [exp, toFloat, zero_toInt, ofFloat]
native_decide
@ -168,18 +172,18 @@ theorem exp_zero : exp zero = one := by
theorem sqrt_zero : sqrt zero = zero := by
simp [sqrt, zero_toInt]
/-- ln(1) = 0 (numerically verified). -/
/-- ln(1) = 0 (numerically verified). TODO(wolfram-verify): ln identity -/
theorem ln_one : ln one = zero := by
-- ln(1.0) = 0.0 in Float
simp [ln, one_toInt, ofFloat]
native_decide
/-- sin(0) = 0. -/
/-- sin(0) = 0. TODO(wolfram-verify): sin identity -/
theorem sin_zero : sin zero = zero := by
simp [sin, toFloat, zero_toInt, ofFloat]
native_decide
/-- cos(0) = 1. -/
/-- cos(0) = 1. TODO(wolfram-verify): cos identity -/
theorem cos_zero : cos zero = one := by
simp [cos, toFloat, zero_toInt, ofFloat]
native_decide
@ -188,43 +192,43 @@ theorem cos_zero : cos zero = one := by
-- §9 EXECUTABLE WITNESSES
-- ═══════════════════════════════════════════════════════════════════════════
-- exp(0) = 1
-- wolfram-verify: exp witnesses
#eval (exp zero).toInt -- expect: 65536
-- exp(1) ≈ e ≈ 2.718
-- wolfram-verify: exp(1) witness
#eval (exp one).toInt -- expect: ~178145
-- exp(-1) ≈ 1/e ≈ 0.368
-- wolfram-verify: exp(-1) witness
#eval (exp (neg one)).toInt -- expect: ~24128
-- sqrt(4) = 2
-- wolfram-verify: sqrt(4) witness
#eval (sqrt (ofRawInt 262144)).toInt -- expect: 131072
-- sqrt(2) ≈ 1.414
-- wolfram-verify: sqrt(2) witness
#eval (sqrt (ofRawInt 131072)).toInt -- expect: ~92682
-- ln(1) = 0
-- wolfram-verify: ln(1) witness
#eval (ln one).toInt -- expect: 0
-- ln(e) ≈ 1
-- wolfram-verify: ln(e) witness
#eval (ln e).toInt -- expect: ~65536
-- sin(0) = 0
-- wolfram-verify: sin(0) witness
#eval (sin zero).toInt -- expect: 0
-- sin(π/2) = 1
-- wolfram-verify: sin(π/2) witness
#eval (sin (div pi two)).toInt -- expect: ~65536
-- cos(0) = 1
-- wolfram-verify: cos(0) witness
#eval (cos zero).toInt -- expect: ~65536
-- tan(π/4) = 1
-- wolfram-verify: tan(π/4) witness
#eval (tan (div pi (ofRawInt 131072))).toInt -- expect: ~65536
-- exp(ln(2)) = 2
-- wolfram-verify: exp∘ln roundtrip
#eval (exp (ln (ofRawInt 131072))).toInt -- expect: ~131072
-- sqrt(2)² ≈ 2
-- wolfram-verify: sqrt(2)² roundtrip
#eval (mul (sqrt (ofRawInt 131072)) (sqrt (ofRawInt 131072))).toInt -- expect: ~131072
end Semantics.Q16_16Numerics

1
0-Core-Formalism/lean/Semantics/Semantics/QFactor.lean
View file

@ -1,4 +1,5 @@
import Semantics.FixedPoint
import Semantics.FixedPointBoundary
namespace Semantics.QFactor

390
0-Core-Formalism/lean/Semantics/Semantics/RRC/PolyFactorIdentity.lean Normal file
View file

@ -0,0 +1,390 @@
/-
Copyright (c) 2026 Research Stack Contributors. All rights reserved.
Released under Apache 2.0 license.
-/
import Semantics.FixedPoint
import Semantics.E8Sidon
/-!
# Polynomial Factor Identity — Short-Sleeve Detection for RRC
This module applies the integer-to-polynomial decomposition technique
(Trail of Bits, "short-sleeve" RSA factoring, 2026) as a classification
feature for the Rainbow Raccoon Compiler identity step.
## Core Insight
When mathematical objects are accessed via zerocopy (mmap, shared memory,
framebuffer DMA), their raw limb structure is already exposed. Checking
for structured zero-blocks ("short-sleeve" patterns) is essentially free
at that boundary. When sparsity is detected, it flags the object for
deeper polynomial-based structural analysis.
## Architecture
```
Zerocopy boundary (raw limbs exposed)
│
├── limbDecompose(n, base) → coefficient array
│
├── coeffSparsity → fraction of zero coefficients (Q16_16)
│ │
│ └── shortSleeveDetected? (sparsity > threshold)
│ │
│ └── YES → compute full PolySignature
│ (degree, maxCoeff, coeffVariance, gcdCoeffs)
│
└── PolySignature feeds into RRC as additional classification dimension
```
## Integration
The `polySignature` function produces a `PolySignature` that RRC can use
alongside existing features (shape, alignment, receipt density) to classify
mathematical objects by their algebraic decomposability.
- High sparsity + low degree → likely factorizable (structured, "simple")
- Low sparsity + high degree → likely irreducible (complex, dense)
- High GCD of coefficients → common factor extractable (reducible)
## References
- Ryan, "Factoring short-sleeve RSA keys with polynomials", Trail of Bits, 2026
- Conway–Sloane, *Sphere Packings*, Ch. 4 §6 (E₈ coefficient structure)
-/
namespace Semantics.RRC.PolyFactorIdentity
open Semantics.FixedPoint
-- Divisor sums come from the authoritative E8Sidon module (single source of
-- truth). `sigma3`/`sigma7`/`convolutionLHS` are computable; the witnesses
-- below evaluate them directly.
open Semantics.E8Sidon (sigma3 sigma7 convolutionLHS)
-- ═══════════════════════════════════════════════════════════════════════════════
-- §1. Limb Decomposition (the zerocopy view)
-- ═══════════════════════════════════════════════════════════════════════════════
/-- Decompose a natural number into base-B limbs (least-significant first).
This is the polynomial coefficient array: n = Σᵢ limbs[i] · Bⁱ.
At a zerocopy boundary, this decomposition is already present in memory
as the raw byte/word layout of the integer. -/
def limbDecompose (n : Nat) (base : Nat) (fuel : Nat := 64) : List Nat :=
if base ≤ 1 then [n]
else
let rec go (x : Nat) (acc : List Nat) (f : Nat) : List Nat :=
match f with
| 0 => acc.reverse
| f' + 1 =>
if x = 0 then acc.reverse
else go (x / base) (acc.cons (x % base)) f'
if n = 0 then [0]
else go n [] fuel
-- Witnesses: limbDecompose gives expected base-B digits
#eval limbDecompose 2044 16 -- expect: [12, 252] since 2044 = 12*16 + 252... wait
-- Actually: 2044 in base 16: 2044 / 16 = 127 rem 12, 127 / 16 = 7 rem 15
-- So 2044 = 7*256 + 15*16 + 12 = [12, 15, 7] (LSB first)
#eval limbDecompose 2044 256 -- expect: [252, 7] since 2044 = 7*256 + 252
#eval limbDecompose 65536 256 -- expect: [0, 0, 1] since 65536 = 1*256² + 0*256 + 0
#eval limbDecompose 9 4 -- expect: [1, 2] since 9 = 2*4 + 1
-- ═══════════════════════════════════════════════════════════════════════════════
-- §2. Coefficient Sparsity (the "short-sleeve" detector)
-- ═══════════════════════════════════════════════════════════════════════════════
/-- Count zero coefficients in a limb decomposition.
High zero count relative to total limbs indicates a "short-sleeve" pattern. -/
def zeroLimbCount (limbs : List Nat) : Nat :=
limbs.filter (· == 0) |>.length
/-- Coefficient sparsity as Q16_16: (zeroCount / totalLimbs).
Returns 0 if limbs is empty. -/
def coeffSparsity (limbs : List Nat) : Q16_16 :=
if limbs.length == 0 then Q16_16.zero
else Q16_16.ofRatio (zeroLimbCount limbs) limbs.length
/-- Short-sleeve detection threshold: 30% zero limbs triggers the flag.
This means at least 30% of the base-B limbs are zero — indicating
structured gaps that make polynomial factorization likely to succeed.
In Q16_16: 0.30 * 65536 ≈ 19661. -/
def shortSleeveThreshold : Q16_16 := Q16_16.ofRawInt 19661
/-- The "flag to look closer": does this integer exhibit short-sleeve structure
when viewed in base-B? At a zerocopy boundary, this check is essentially free
since the limbs are already laid out in memory. -/
def shortSleeveDetected (n : Nat) (base : Nat) : Bool :=
let limbs := limbDecompose n base
-- Need at least 3 limbs to have a meaningful sparsity signal
if limbs.length < 3 then false
else (coeffSparsity limbs).toInt ≥ shortSleeveThreshold.toInt
-- Witnesses: short-sleeve detection on known values
#eval shortSleeveDetected 65536 256 -- expect: true (limbs [0,0,1] → 2/3 sparsity)
#eval shortSleeveDetected 2044 256 -- expect: false (limbs [252,7] → only 2 limbs)
#eval shortSleeveDetected 16777216 256 -- expect: true (limbs [0,0,0,1] → 3/4 sparsity)
-- ═══════════════════════════════════════════════════════════════════════════════
-- §3. Polynomial Signature (full structural features when flagged)
-- ═══════════════════════════════════════════════════════════════════════════════
/-- GCD of a list of natural numbers. Used to detect common polynomial factors. -/
def listGcd : List Nat → Nat
| [] => 0
| [x] => x
| x :: xs => Nat.gcd x (listGcd xs)
/-- Maximum coefficient in a limb decomposition.
Small max coefficient (relative to base) indicates the polynomial has
"small" coefficients — the key property exploited in the Trail of Bits attack. -/
def maxCoeff (limbs : List Nat) : Nat :=
limbs.foldl Nat.max 0
/-- Sum of squares of coefficients — a proxy for "energy" of the polynomial.
Low energy relative to degree indicates a sparse, structured polynomial. -/
def coeffEnergy (limbs : List Nat) : Nat :=
limbs.foldl (fun acc c => acc + c * c) 0
/-- The polynomial degree: index of highest non-zero coefficient.
Equals (number of limbs - 1) for non-zero inputs. -/
def polyDegree (limbs : List Nat) : Nat :=
match limbs.reverse.dropWhile (· == 0) with
| [] => 0
| xs => xs.length - 1
/-- Full polynomial signature — the structural fingerprint extracted when
short-sleeve detection flags an integer for closer inspection.
Fields:
- `base`: the limb size (base-B representation)
- `degree`: polynomial degree (highest non-zero coefficient index)
- `numTerms`: count of non-zero coefficients
- `sparsity`: fraction of zero coefficients (Q16_16)
- `maxCoeffVal`: largest coefficient value
- `gcdCoeffs`: GCD of all coefficients (> 1 means common factor exists)
- `energy`: sum of squares of coefficients (structural complexity proxy)
- `isShortSleeve`: whether the short-sleeve threshold was exceeded -/
structure PolySignature where
base : Nat
degree : Nat
numTerms : Nat
sparsity : Q16_16
maxCoeffVal : Nat
gcdCoeffs : Nat
energy : Nat
isShortSleeve : Bool
deriving Repr
/-- Compute the full polynomial signature for a natural number in base B.
This is the "look closer" step — called only when shortSleeveDetected
returns true at the zerocopy boundary. -/
def polySignature (n : Nat) (base : Nat) : PolySignature :=
let limbs := limbDecompose n base
let nonZero := limbs.filter (· != 0)
{ base := base
degree := polyDegree limbs
numTerms := nonZero.length
sparsity := coeffSparsity limbs
maxCoeffVal := maxCoeff limbs
gcdCoeffs := listGcd nonZero
energy := coeffEnergy limbs
isShortSleeve := shortSleeveDetected n base }
-- Witnesses
#eval polySignature 65536 256
-- expect: { base=256, degree=2, numTerms=1, sparsity≈43690 (2/3),
-- maxCoeffVal=1, gcdCoeffs=1, energy=1, isShortSleeve=true }
#eval polySignature 16777216 256
-- expect: { base=256, degree=3, numTerms=1, sparsity≈49152 (3/4),
-- maxCoeffVal=1, gcdCoeffs=1, energy=1, isShortSleeve=true }
-- ═══════════════════════════════════════════════════════════════════════════════
-- §4. E8Sidon Integration — Divisor Sum Polynomial Signatures
-- ═══════════════════════════════════════════════════════════════════════════════
/-- Compute polynomial signature of σ₃(n) in a given base.
Divisor sums have multiplicative structure that may produce
exploitable limb patterns in certain bases. -/
def sigma3PolySig (n : Nat) (base : Nat) : PolySignature :=
polySignature (sigma3 n) base
/-- Compute polynomial signature of σ₇(n) in a given base.
σ₇ values grow rapidly and often exhibit short-sleeve patterns
in smaller bases due to the power-7 amplification of prime factors. -/
def sigma7PolySig (n : Nat) (base : Nat) : PolySignature :=
polySignature (sigma7 n) base
/-- Compute polynomial signature of convolutionLHS(n) in a given base.
The Cauchy product Σ σ₃(m)·σ₃(n-m) produces large integers whose
limb structure reflects the multiplicative nature of divisor sums. -/
def convPolySig (n : Nat) (base : Nat) : PolySignature :=
polySignature (convolutionLHS n) base
-- Witnesses: σ₇ values in base 256 — do they exhibit short-sleeve patterns?
#eval sigma7 4 -- expect: 2188 + 4^7 = 2188 + 16384 ... actually σ₇(4) = 1 + 2^7 + 4^7 = 1+128+16384 = 16513
#eval sigma7PolySig 4 256
-- σ₇(4) = 16513 → base-256 limbs: [97, 64] → 2 limbs, no short-sleeve (too few)
#eval sigma7 6 -- σ₇(6) = 1 + 2^7 + 3^7 + 6^7 = 1+128+2187+279936 = 282252
#eval sigma7PolySig 6 256
-- σ₇(6) = 282252 → base-256 limbs: [140, 77, 4, 0] wait let me not predict...
#eval sigma7 12 -- large value, likely has limb structure
#eval sigma7PolySig 12 256
-- Convolution products (large, likely structured)
#eval convolutionLHS 6 -- Σ σ₃(m)·σ₃(6-m) for m=1..5
#eval convPolySig 6 256
-- ═══════════════════════════════════════════════════════════════════════════════
-- §5. RRC Feature Integration
-- ═══════════════════════════════════════════════════════════════════════════════
/-- Classification feature: polynomial decomposability score.
Maps a PolySignature to a Q16_16 score in [0, 1] that indicates
how amenable the integer is to polynomial-based factorization.
High score (→ 1.0) means:
- High sparsity (many zero limbs)
- Low numTerms relative to degree
- GCD > 1 (common factor extractable)
- Low energy (sparse polynomial)
Low score (→ 0.0) means:
- Dense polynomial (no exploitable structure)
- All coefficients non-zero
- No common factor
This score feeds into the RRC identity step as the `polyDecomposability`
feature dimension. When high, it signals that the mathematical object
has algebraic structure that the classifier can exploit. -/
def polyDecomposabilityScore (sig : PolySignature) : Q16_16 :=
-- Component 1: sparsity (weight 40%)
let sparsityComponent := (sig.sparsity.toInt * 26214) / q16Scale -- * 0.4
-- Component 2: GCD bonus (weight 30%) — 1.0 if gcd > 1, else 0.0
let gcdComponent : Int := if sig.gcdCoeffs > 1 then 19661 else 0 -- 0.3
-- Component 3: term efficiency (weight 30%) — (1 - numTerms/degree) when degree > 0
let termEfficiency : Int :=
if sig.degree == 0 then 0
else
let ratio := (sig.numTerms * q16Scale) / (sig.degree + 1)
let complement := q16Scale - ratio -- (1 - numTerms/(degree+1))
(complement * 19661) / q16Scale -- * 0.3
Q16_16.ofRawInt (sparsityComponent + gcdComponent + termEfficiency)
-- Witnesses
#eval polyDecomposabilityScore (polySignature 65536 256)
-- High: sparsity 2/3, gcd=1, 1 term / degree 2 → should be > 0.5
#eval polyDecomposabilityScore (polySignature 2044 256)
-- Low: only 2 limbs, no sparsity → should be near 0
#eval polyDecomposabilityScore (polySignature 16777216 256)
-- High: sparsity 3/4, gcd=1, 1 term / degree 3 → should be > 0.5
-- ═══════════════════════════════════════════════════════════════════════════════
-- §6. Batch Scanner (zerocopy boundary integration)
-- ═══════════════════════════════════════════════════════════════════════════════
/-- Result of scanning a batch of integers at a zerocopy boundary.
Records which values were flagged for closer inspection. -/
structure ZeroCopyScanResult where
totalScanned : Nat
flaggedCount : Nat
flaggedIndices : List Nat
signatures : List PolySignature
deriving Repr
/-- Scan a list of integers at the zerocopy boundary.
For each value, check short-sleeve detection. If flagged, compute
the full polynomial signature. This models what happens at mmap/DMA
boundaries where raw limbs are already visible.
The `base` parameter matches the hardware word size at the boundary:
- 256 for byte-level DMA (framebuffer, VCN payload)
- 65536 for Q16_16 values (two Q16_16 scalars per 32-bit word)
- 4294967296 for 32-bit limbs (ivshmem, PCIe DMA) -/
def zeroCopyScan (values : List Nat) (base : Nat) : ZeroCopyScanResult :=
let indexed := values.zipIdx -- List (Nat × Nat), (value, index)
let flagged := indexed.filter (fun (v, _) => shortSleeveDetected v base)
{ totalScanned := values.length
flaggedCount := flagged.length
flaggedIndices := flagged.map Prod.snd
signatures := flagged.map (fun (v, _) => polySignature v base) }
-- Witness: scan a batch with mixed structure
#eval zeroCopyScan [2044, 65536, 255, 16777216, 42, 256] 256
-- expect: flagged = indices of 65536 and 16777216 (the ones with zero-limb patterns)
-- ═══════════════════════════════════════════════════════════════════════════════
-- §7. Theorems — Polynomial Evaluation Correctness
-- ═══════════════════════════════════════════════════════════════════════════════
/-- Evaluate a polynomial (coefficient list, LSB first) at a given base.
This is the inverse of limbDecompose: polyEval(limbDecompose(n, B), B) = n. -/
def polyEval (coeffs : List Nat) (base : Nat) : Nat :=
let rec go (cs : List Nat) (pow : Nat) (acc : Nat) : Nat :=
match cs with
| [] => acc
| c :: rest => go rest (pow * base) (acc + c * pow)
go coeffs 1 0
/-- limbDecompose followed by polyEval recovers the original value.
This is the fundamental correctness property: the polynomial
representation is faithful (no information lost). -/
theorem limbDecompose_polyEval_roundtrip (n : Nat) (base : Nat) (hb : base ≥ 2) :
polyEval (limbDecompose n base) base = n := by
-- TODO(lean-port): Prove by induction on fuel steps of limbDecompose.
-- Sketch: each step extracts (n % base) as coefficient i, then recurses on
-- (n / base). The polyEval sum reconstructs via Σᵢ (n/base^i % base) · base^i = n.
-- This is the standard base-B representation theorem.
-- Blocked on: need List.enum induction lemma + Nat.div_add_mod identity.
sorry
/-- Zero limbs in a decomposition correspond to "gaps" in the polynomial.
An integer with k zero limbs out of d total has at most (d - k) non-zero terms,
making polynomial factorization faster (fewer terms to consider). -/
theorem zeroLimbs_bound_terms (limbs : List Nat) :
(limbs.filter (· != 0)).length + zeroLimbCount limbs = limbs.length := by
unfold zeroLimbCount
-- TODO(lean-port): Prove by List.filter complement partition.
-- Sketch: (filter p).length + (filter ¬p).length = length for any decidable p.
-- The two filters (· == 0) and (· != 0) are complements.
-- Blocked on: need List.filter_length_add_filter_length_eq (or equivalent).
sorry
/-- Short-sleeve detection is monotone in sparsity: adding a zero limb
can only increase the likelihood of being flagged. -/
theorem shortSleeve_mono_zero_prepend (n : Nat) (base : Nat) (hb : base ≥ 2)
(h : shortSleeveDetected n base = true) :
shortSleeveDetected (n * base) base = true := by
-- TODO(lean-port): Prove that limbDecompose(n * base, base) = 0 :: limbDecompose(n, base).
-- Multiplying by base left-shifts the polynomial, prepending a zero coefficient.
-- This increases zeroLimbCount by 1 and length by 1, so sparsity increases
-- (or stays the same if it was already maximal).
-- Sketch: unfold shortSleeveDetected, show sparsity(0::limbs) ≥ sparsity(limbs).
sorry
-- ═══════════════════════════════════════════════════════════════════════════════
-- §8. Module Summary
-- ═══════════════════════════════════════════════════════════════════════════════
/-!
## Sorry Inventory
| # | Name | Reason | Proof Sketch |
|---|------|--------|--------------|
| 1 | `limbDecompose_polyEval_roundtrip` | Needs go-induction + Nat.div_add_mod | Induction on fuel, standard base-B theorem |
| 2 | `zeroLimbs_bound_terms` | Needs List.filter complement partition | filter_p.length + filter_not_p.length = length |
| 3 | `shortSleeve_mono_zero_prepend` | Needs limbDecompose multiplication lemma | Prepend-zero increases sparsity |
## Integration Notes
- `polyDecomposabilityScore` is the primary RRC feature export.
- `zeroCopyScan` models the hardware boundary where detection is free.
- `sigma3PolySig` / `sigma7PolySig` / `convPolySig` connect to E8Sidon.
- Base selection: 256 for byte-level (framebuffer/DMA), 65536 for Q16_16.
-/
end Semantics.RRC.PolyFactorIdentity

1
0-Core-Formalism/lean/Semantics/Semantics/SLUG3.lean
View file

@ -13,6 +13,7 @@ Lean is the source of truth.
-/
import Semantics.FixedPoint
import Semantics.FixedPointBoundary
namespace Semantics.SLUG3

1
0-Core-Formalism/lean/Semantics/Semantics/SubagentOrchestrator.lean
View file

@ -30,6 +30,7 @@ import Semantics.RcloneIntegration
import Semantics.GpuDutyAssignment
import Semantics.DomainModelIntegration
import Semantics.FixedPoint
import Semantics.FixedPointBoundary
namespace Semantics.SubagentOrchestrator

3
0-Core-Formalism/lean/Semantics/Semantics/Tape.lean
View file

@ -1,4 +1,5 @@
import Semantics.FixedPoint
import Semantics.FixedPointBoundary
namespace Semantics.Tape
@ -300,7 +301,7 @@ def accountKot (tm : TapeMachine) (state : TapeState) (mode : ControlMode) : KOT
let decision := KOTBudget.evaluateEconomics newBudget state.kotYieldProjected (1 / 10 : Rat)
{ entry with decision := decision }
/-- Form a new tape state from normalized input. -/
/-- Form a new tape state from normalized input. -- TODO(wolfram-verify): tape normalization -/
def formState (tm : TapeMachine) (data : List UInt8) (contextType : String) : TapeState :=
let compressed := compressStructure data
let invariants := computeInvariants compressed

28
4-Infrastructure/auto/lib/q16.py
View file

@ -1,29 +1,17 @@
# PTOS: LAYER=INFRA / DOMAIN=AUTOMATION / CONDITION=ALPHA
"""
Q16_16 fixed-point arithmetic for deterministic compute across all substrates.
Re-exports from the canonical shared library at 4-Infrastructure/lib/q16.py.
All thresholds and metric values are stored as Q16_16 integers.
One = 0x00010000 = 65536. Float is forbidden in compute paths.
One = 0x00010000 = 65536. Float is forbidden in compute paths.
"""
from __future__ import annotations
Q16_ONE: int = 0x00010000
Q16_HALF: int = 0x00008000
import sys
from pathlib import Path
sys.path.insert(0, str(Path(__file__).resolve().parents[2]))
from lib.q16 import Q16_HALF, Q16_ONE, from_q16, ratio_q16, to_q16
def to_q16(value: float) -> int:
"""Convert a float to Q16_16. Only allowed at the external boundary."""
return int(round(value * Q16_ONE))
def from_q16(value: int) -> float:
"""Convert Q16_16 back to float. Only for display, never in compute."""
return value / Q16_ONE
def ratio_q16(numerator: float, denominator: float) -> int:
"""Compute Q16_16 ratio of two floats, clamped to [0, 1]."""
if denominator == 0:
return 0
r = numerator / denominator
r = max(0.0, min(1.0, r))
return int(r * Q16_ONE)
__all__ = ["Q16_ONE", "Q16_HALF", "to_q16", "from_q16", "ratio_q16"]

16
4-Infrastructure/hardware/jupiter_phi_self_recovery_probe.py
View file

@ -11,7 +11,6 @@ an explicit residual mask.
from __future__ import annotations
import argparse
import hashlib
import json
import math
import random
@ -20,24 +19,19 @@ import zlib
from datetime import datetime, timezone
from pathlib import Path
from typing import Any
import sys
REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO / "4-Infrastructure"))
from lib.hashing import sha256_bytes
from lib.jsonl import stable_json
QUANDELA_RECEIPT = REPO / "4-Infrastructure" / "shim" / "quandela_stochastic_crc_local_sim_receipt.json"
OUT = REPO / "4-Infrastructure" / "hardware" / "jupiter_phi_self_recovery_probe_receipt.json"
PHI = (1.0 + math.sqrt(5.0)) / 2.0
GOLDEN_ANGLE = 2.0 * math.pi * (1.0 - 1.0 / PHI)
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def crc32_hex(data: bytes) -> str:
return f"{zlib.crc32(data) & 0xFFFFFFFF:08x}"

47
4-Infrastructure/hardware/standard_model_12_to_4_reduction.py
View file

@ -20,15 +20,20 @@ rational-coordinate level.
from __future__ import annotations
import argparse
import hashlib
import json
from datetime import datetime, timezone
from fractions import Fraction
from pathlib import Path
from typing import Any
import sys
REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO / "4-Infrastructure"))
from lib.hashing import sha256_bytes
from lib.fraction_utils import fraction_json, fraction_str, parse_fraction_json, vector_json
from lib.jsonl import load_json, stable_json
AVERAGE_RECEIPT = (
REPO
/ "4-Infrastructure"
@ -105,37 +110,6 @@ PROJECTION: dict[str, dict[str, Fraction]] = {
"spectral": Fraction(1, 3),
},
}
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def fraction_str(value: Fraction) -> str:
return str(value.numerator) if value.denominator == 1 else f"{value.numerator}/{value.denominator}"
def fraction_json(value: Fraction) -> dict[str, Any]:
return {
"fraction": fraction_str(value),
"numerator": value.numerator,
"denominator": value.denominator,
"decimal": float(value),
}
def parse_fraction_json(item: dict[str, Any]) -> Fraction:
return Fraction(int(item["numerator"]), int(item["denominator"]))
def load_json(path: Path) -> dict[str, Any]:
return json.loads(path.read_text(encoding="utf-8"))
def centroid_from_average(receipt: dict[str, Any]) -> dict[str, Fraction]:
centroid: dict[str, Fraction] = {}
for item in receipt["rational_average"]["centroid_components"]:
@ -203,15 +177,6 @@ def lift_4_to_12(reduced: dict[str, Fraction]) -> dict[str, Fraction]:
def signed_l1(vector: dict[str, Fraction]) -> Fraction:
return sum((abs(value) for value in vector.values()), Fraction(0))
def vector_json(vector: dict[str, Fraction]) -> dict[str, dict[str, Any]]:
return {
key: fraction_json(value)
for key, value in sorted(vector.items())
}
def ranked_abs_vector(vector: dict[str, Fraction], limit: int = 8) -> list[dict[str, Any]]:
ranked = sorted(vector.items(), key=lambda item: abs(item[1]), reverse=True)
return [

46
4-Infrastructure/hardware/standard_model_absurd_genetics_stress.py
View file

@ -17,7 +17,6 @@ substitutions are detected as invalid.
from __future__ import annotations
import argparse
import hashlib
import itertools
import json
import math
@ -25,9 +24,15 @@ from datetime import datetime, timezone
from fractions import Fraction
from pathlib import Path
from typing import Any
import sys
REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO / "4-Infrastructure"))
from lib.hashing import sha256_bytes
from lib.fraction_utils import fraction_json, fraction_str, parse_fraction_json, vector_from_json, vector_json
from lib.jsonl import load_json, stable_json
FORCE_RECEIPT = (
REPO
/ "4-Infrastructure"
@ -51,45 +56,6 @@ HANDLE_TO_PRIMITIVE = {
"shear_torsion": "shear",
"spectral_field": "spectral",
}
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def fraction_str(value: Fraction) -> str:
return str(value.numerator) if value.denominator == 1 else f"{value.numerator}/{value.denominator}"
def fraction_json(value: Fraction) -> dict[str, Any]:
return {
"fraction": fraction_str(value),
"numerator": value.numerator,
"denominator": value.denominator,
"decimal": float(value),
}
def parse_fraction_json(item: dict[str, Any]) -> Fraction:
return Fraction(int(item["numerator"]), int(item["denominator"]))
def load_json(path: Path) -> dict[str, Any]:
return json.loads(path.read_text(encoding="utf-8"))
def vector_from_json(items: dict[str, dict[str, Any]]) -> dict[str, Fraction]:
return {key: parse_fraction_json(value) for key, value in items.items()}
def vector_json(vector: dict[str, Fraction]) -> dict[str, dict[str, Any]]:
return {key: fraction_json(value) for key, value in sorted(vector.items())}
def signed_l1(vector: dict[str, Fraction]) -> Fraction:
return sum((abs(value) for value in vector.values()), Fraction(0))

56
4-Infrastructure/hardware/standard_model_connectome_reconfiguration_runner.py
View file

@ -12,15 +12,20 @@ It deliberately does not rewrite the canonical Standard Model projection.
from __future__ import annotations
import argparse
import hashlib
import json
from datetime import datetime, timezone
from fractions import Fraction
from pathlib import Path
from typing import Any
import sys
REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO / "4-Infrastructure"))
from lib.hashing import sha256_bytes
from lib.fraction_utils import fraction_json, fraction_str, parse_fraction_json, projection_from_json, vector_from_json, vector_json
from lib.jsonl import load_json, stable_json
REDUCTION_RECEIPT = (
REPO
/ "4-Infrastructure"
@ -47,55 +52,6 @@ OUT = (
)
PRIMITIVES = ("field", "shear", "packet", "spectral")
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def fraction_str(value: Fraction) -> str:
return str(value.numerator) if value.denominator == 1 else f"{value.numerator}/{value.denominator}"
def fraction_json(value: Fraction) -> dict[str, Any]:
return {
"fraction": fraction_str(value),
"numerator": value.numerator,
"denominator": value.denominator,
"decimal": float(value),
}
def parse_fraction_json(item: dict[str, Any]) -> Fraction:
return Fraction(int(item["numerator"]), int(item["denominator"]))
def load_json(path: Path) -> dict[str, Any]:
return json.loads(path.read_text(encoding="utf-8"))
def vector_from_json(items: dict[str, dict[str, Any]]) -> dict[str, Fraction]:
return {key: parse_fraction_json(value) for key, value in items.items()}
def vector_json(vector: dict[str, Fraction]) -> dict[str, dict[str, Any]]:
return {key: fraction_json(value) for key, value in sorted(vector.items())}
def projection_from_json(items: dict[str, dict[str, dict[str, Any]]]) -> dict[str, dict[str, Fraction]]:
return {
axis: {
primitive: parse_fraction_json(weight)
for primitive, weight in row.items()
}
for axis, row in items.items()
}
def projection_json(projection: dict[str, dict[str, Fraction]]) -> dict[str, dict[str, dict[str, Any]]]:
return {
axis: {

46
4-Infrastructure/hardware/standard_model_dna_substitution_alignment.py
View file

@ -17,16 +17,21 @@ This is a symbolic compression substitution, not a biological or physics claim.
from __future__ import annotations
import argparse
import hashlib
import json
import math
from datetime import datetime, timezone
from fractions import Fraction
from pathlib import Path
from typing import Any
import sys
REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO / "4-Infrastructure"))
from lib.hashing import sha256_bytes
from lib.fraction_utils import fraction_json, fraction_str, parse_fraction_json, vector_from_json, vector_json
from lib.jsonl import load_json, stable_json
FORCE_RECEIPT = (
REPO
/ "4-Infrastructure"
@ -58,45 +63,6 @@ HANDLE_TO_BASE = {
"shear_torsion": "T",
"spectral_field": "C",
}
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def fraction_str(value: Fraction) -> str:
return str(value.numerator) if value.denominator == 1 else f"{value.numerator}/{value.denominator}"
def fraction_json(value: Fraction) -> dict[str, Any]:
return {
"fraction": fraction_str(value),
"numerator": value.numerator,
"denominator": value.denominator,
"decimal": float(value),
}
def parse_fraction_json(item: dict[str, Any]) -> Fraction:
return Fraction(int(item["numerator"]), int(item["denominator"]))
def load_json(path: Path) -> dict[str, Any]:
return json.loads(path.read_text(encoding="utf-8"))
def vector_from_json(items: dict[str, dict[str, Any]]) -> dict[str, Fraction]:
return {key: parse_fraction_json(value) for key, value in items.items()}
def vector_json(vector: dict[str, Fraction]) -> dict[str, dict[str, Any]]:
return {key: fraction_json(value) for key, value in sorted(vector.items())}
def signed_l1(vector: dict[str, Fraction]) -> Fraction:
return sum((abs(value) for value in vector.values()), Fraction(0))

46
4-Infrastructure/hardware/standard_model_extension_failure_probe.py
View file

@ -10,15 +10,20 @@ law breaks.
from __future__ import annotations
import argparse
import hashlib
import json
from datetime import datetime, timezone
from fractions import Fraction
from pathlib import Path
from typing import Any
import sys
REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO / "4-Infrastructure"))
from lib.hashing import sha256_bytes
from lib.fraction_utils import fraction_json, fraction_str, parse_fraction_json, vector_from_json, vector_json
from lib.jsonl import load_json, stable_json
DNA_RECEIPT = (
REPO
/ "4-Infrastructure"
@ -43,45 +48,6 @@ EXTRA_BASES = ("B", "S", "P", "Z")
PRIMITIVES = ("field", "shear", "packet", "spectral")
CANONICAL = {"A": "field", "T": "shear", "G": "packet", "C": "spectral"}
HANDLE_TO_BASE = {"packet_local": "G", "shear_torsion": "T", "spectral_field": "C"}
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def fraction_str(value: Fraction) -> str:
return str(value.numerator) if value.denominator == 1 else f"{value.numerator}/{value.denominator}"
def fraction_json(value: Fraction) -> dict[str, Any]:
return {
"fraction": fraction_str(value),
"numerator": value.numerator,
"denominator": value.denominator,
"decimal": float(value),
}
def parse_fraction_json(item: dict[str, Any]) -> Fraction:
return Fraction(int(item["numerator"]), int(item["denominator"]))
def load_json(path: Path) -> dict[str, Any]:
return json.loads(path.read_text(encoding="utf-8"))
def vector_from_json(items: dict[str, dict[str, Any]]) -> dict[str, Fraction]:
return {key: parse_fraction_json(value) for key, value in items.items()}
def vector_json(vector: dict[str, Fraction]) -> dict[str, dict[str, Any]]:
return {key: fraction_json(value) for key, value in sorted(vector.items())}
def signed_l1(vector: dict[str, Fraction]) -> Fraction:
return sum((abs(value) for value in vector.values()), Fraction(0))

56
4-Infrastructure/hardware/standard_model_force_regime_model.py
View file

@ -15,15 +15,20 @@ through the current compression regime.
from __future__ import annotations
import argparse
import hashlib
import json
from datetime import datetime, timezone
from fractions import Fraction
from pathlib import Path
from typing import Any
import sys
REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO / "4-Infrastructure"))
from lib.hashing import sha256_bytes
from lib.fraction_utils import fraction_json, fraction_str, parse_fraction_json, projection_from_json, vector_from_json, vector_json
from lib.jsonl import load_json, stable_json
REDUCTION_RECEIPT = (
REPO
/ "4-Infrastructure"
@ -88,55 +93,6 @@ FORCE_SECTORS = {
"claim_boundary": "no gravity force is inferred from the source equation wall",
},
}
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def fraction_str(value: Fraction) -> str:
return str(value.numerator) if value.denominator == 1 else f"{value.numerator}/{value.denominator}"
def fraction_json(value: Fraction) -> dict[str, Any]:
return {
"fraction": fraction_str(value),
"numerator": value.numerator,
"denominator": value.denominator,
"decimal": float(value),
}
def parse_fraction_json(item: dict[str, Any]) -> Fraction:
return Fraction(int(item["numerator"]), int(item["denominator"]))
def load_json(path: Path) -> dict[str, Any]:
return json.loads(path.read_text(encoding="utf-8"))
def vector_from_json(items: dict[str, dict[str, Any]]) -> dict[str, Fraction]:
return {key: parse_fraction_json(value) for key, value in items.items()}
def projection_from_json(items: dict[str, dict[str, dict[str, Any]]]) -> dict[str, dict[str, Fraction]]:
return {
axis: {
primitive: parse_fraction_json(weight)
for primitive, weight in row.items()
}
for axis, row in items.items()
}
def vector_json(vector: dict[str, Fraction]) -> dict[str, dict[str, Any]]:
return {key: fraction_json(value) for key, value in sorted(vector.items())}
def signed_l1(vector: dict[str, Fraction]) -> Fraction:
return sum((abs(value) for value in vector.values()), Fraction(0))

46
4-Infrastructure/hardware/standard_model_genus3_residual_boat.py
View file

@ -11,16 +11,21 @@ This is a compression/topology control object, not a physical claim.
from __future__ import annotations
import argparse
import hashlib
import json
import math
from datetime import datetime, timezone
from fractions import Fraction
from pathlib import Path
from typing import Any
import sys
REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO / "4-Infrastructure"))
from lib.hashing import sha256_bytes
from lib.fraction_utils import fraction_json, fraction_str, parse_fraction_json, vector_from_json, vector_json
from lib.jsonl import load_json, stable_json
REDUCTION_RECEIPT = (
REPO
/ "4-Infrastructure"
@ -56,45 +61,6 @@ HANDLE_MAP = {
"scalar_potential",
},
}
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def fraction_str(value: Fraction) -> str:
return str(value.numerator) if value.denominator == 1 else f"{value.numerator}/{value.denominator}"
def fraction_json(value: Fraction) -> dict[str, Any]:
return {
"fraction": fraction_str(value),
"numerator": value.numerator,
"denominator": value.denominator,
"decimal": float(value),
}
def parse_fraction_json(item: dict[str, Any]) -> Fraction:
return Fraction(int(item["numerator"]), int(item["denominator"]))
def load_json(path: Path) -> dict[str, Any]:
return json.loads(path.read_text(encoding="utf-8"))
def vector_from_json(items: dict[str, dict[str, Any]]) -> dict[str, Fraction]:
return {key: parse_fraction_json(value) for key, value in items.items()}
def vector_json(vector: dict[str, Fraction]) -> dict[str, dict[str, Any]]:
return {key: fraction_json(value) for key, value in sorted(vector.items())}
def signed_l1(vector: dict[str, Fraction]) -> Fraction:
return sum((abs(value) for value in vector.values()), Fraction(0))

16
4-Infrastructure/hardware/standard_model_lagrangian_eigen_probe.py
View file

@ -11,15 +11,19 @@ principal eigenvector of that coupling/interaction matrix.
from __future__ import annotations
import argparse
import hashlib
import json
import math
from datetime import datetime, timezone
from pathlib import Path
from typing import Any
import sys
REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO / "4-Infrastructure"))
from lib.hashing import sha256_bytes
from lib.jsonl import stable_json
OUT = REPO / "4-Infrastructure" / "hardware" / "standard_model_lagrangian_eigen_probe_receipt.json"
PHI = (1.0 + math.sqrt(5.0)) / 2.0
@ -70,16 +74,6 @@ OBSERVATIONS: list[tuple[str, str, float, str]] = [
("scalar_potential", "electroweak_charged_w", 3.0, "scalar-gauge mass-generated W couplings"),
("scalar_potential", "electroweak_neutral_za", 3.0, "scalar-gauge mass-generated Z/A couplings"),
]
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def build_matrix(phi_mode: str) -> list[list[float]]:
index = {name: pos for pos, name in enumerate(NODES)}
size = len(NODES)

30
4-Infrastructure/hardware/standard_model_lagrangian_exact_average.py
View file

@ -9,7 +9,6 @@ and a targeted phi average in Q(phi), where phi^2 = phi + 1.
from __future__ import annotations
import argparse
import hashlib
import json
import math
from dataclasses import dataclass
@ -19,9 +18,15 @@ from pathlib import Path
from typing import Any
from standard_model_lagrangian_eigen_probe import NODES, OBSERVATIONS
import sys
REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO / "4-Infrastructure"))
from lib.hashing import sha256_bytes
from lib.fraction_utils import fraction_json, fraction_str
from lib.jsonl import stable_json
OUT = REPO / "4-Infrastructure" / "hardware" / "standard_model_lagrangian_exact_average_receipt.json"
PHI_FLOAT = (1.0 + math.sqrt(5.0)) / 2.0
@ -86,29 +91,6 @@ class QPhi:
"form": f"({fraction_str(self.a)}) + ({fraction_str(self.b)})*phi",
"approx": self.approx(),
}
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def fraction_str(value: Fraction) -> str:
return str(value.numerator) if value.denominator == 1 else f"{value.numerator}/{value.denominator}"
def fraction_json(value: Fraction) -> dict[str, Any]:
return {
"fraction": fraction_str(value),
"numerator": value.numerator,
"denominator": value.denominator,
"decimal": float(value),
}
def is_scalar_touched(left: str, right: str) -> bool:
fields = (left, right)
return any("higgs" in field or "scalar" in field for field in fields)

16
4-Infrastructure/hardware/standard_model_lagrangian_underverse_closure.py
View file

@ -15,7 +15,6 @@ The arithmetic is exact rational / Q(phi), matching the exact-average probe.
from __future__ import annotations
import argparse
import hashlib
import json
from datetime import datetime, timezone
from fractions import Fraction
@ -24,20 +23,15 @@ from typing import Any
from standard_model_lagrangian_eigen_probe import NODES, OBSERVATIONS
from standard_model_lagrangian_exact_average import QPhi, exact_rational_average, fraction_str, phi_targeted_average
import sys
REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO / "4-Infrastructure"))
from lib.hashing import sha256_bytes
from lib.jsonl import stable_json
OUT = REPO / "4-Infrastructure" / "hardware" / "standard_model_lagrangian_underverse_closure_receipt.json"
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def edge_key(left: str, right: str) -> tuple[str, str]:
return tuple(sorted((left, right)))

56
4-Infrastructure/hardware/standard_model_projection_sensitivity_probe.py
View file

@ -12,16 +12,21 @@ later route pays the header/receipt cost and preserves exact rehydration.
from __future__ import annotations
import argparse
import hashlib
import itertools
import json
from datetime import datetime, timezone
from fractions import Fraction
from pathlib import Path
from typing import Any
import sys
REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO / "4-Infrastructure"))
from lib.hashing import sha256_bytes
from lib.fraction_utils import fraction_json, fraction_str, parse_fraction_json, projection_from_json, vector_from_json, vector_json
from lib.jsonl import load_json, stable_json
REDUCTION_RECEIPT = (
REPO
/ "4-Infrastructure"
@ -42,55 +47,6 @@ OUT = (
)
PRIMITIVES = ("field", "shear", "packet", "spectral")
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def fraction_str(value: Fraction) -> str:
return str(value.numerator) if value.denominator == 1 else f"{value.numerator}/{value.denominator}"
def fraction_json(value: Fraction) -> dict[str, Any]:
return {
"fraction": fraction_str(value),
"numerator": value.numerator,
"denominator": value.denominator,
"decimal": float(value),
}
def parse_fraction_json(item: dict[str, Any]) -> Fraction:
return Fraction(int(item["numerator"]), int(item["denominator"]))
def load_json(path: Path) -> dict[str, Any]:
return json.loads(path.read_text(encoding="utf-8"))
def vector_from_json(items: dict[str, dict[str, Any]]) -> dict[str, Fraction]:
return {key: parse_fraction_json(value) for key, value in items.items()}
def vector_json(vector: dict[str, Fraction]) -> dict[str, dict[str, Any]]:
return {key: fraction_json(value) for key, value in sorted(vector.items())}
def projection_from_json(items: dict[str, dict[str, dict[str, Any]]]) -> dict[str, dict[str, Fraction]]:
return {
axis: {
primitive: parse_fraction_json(weight)
for primitive, weight in row.items()
}
for axis, row in items.items()
}
def projection_json(projection: dict[str, dict[str, Fraction]]) -> dict[str, dict[str, dict[str, Any]]]:
return {
axis: {

56
4-Infrastructure/hardware/standard_model_residual_accounting_probe.py
View file

@ -10,15 +10,20 @@ noise, sidecar debt, signal, or a failure boundary.
from __future__ import annotations
import argparse
import hashlib
import json
from datetime import datetime, timezone
from fractions import Fraction
from pathlib import Path
from typing import Any
import sys
REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO / "4-Infrastructure"))
from lib.hashing import sha256_bytes
from lib.fraction_utils import fraction_json, fraction_str, parse_fraction_json, projection_from_json, vector_from_json, vector_json
from lib.jsonl import load_json, stable_json
REDUCTION_RECEIPT = (
REPO
/ "4-Infrastructure"
@ -46,55 +51,6 @@ OUT = (
PRIMITIVES = ("field", "shear", "packet", "spectral")
HANDLES = ("packet_local", "shear_torsion", "spectral_field")
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def fraction_str(value: Fraction) -> str:
return str(value.numerator) if value.denominator == 1 else f"{value.numerator}/{value.denominator}"
def fraction_json(value: Fraction) -> dict[str, Any]:
return {
"fraction": fraction_str(value),
"numerator": value.numerator,
"denominator": value.denominator,
"decimal": float(value),
}
def parse_fraction_json(item: dict[str, Any]) -> Fraction:
return Fraction(int(item["numerator"]), int(item["denominator"]))
def load_json(path: Path) -> dict[str, Any]:
return json.loads(path.read_text(encoding="utf-8"))
def vector_from_json(items: dict[str, dict[str, Any]]) -> dict[str, Fraction]:
return {key: parse_fraction_json(value) for key, value in items.items()}
def projection_from_json(items: dict[str, dict[str, dict[str, Any]]]) -> dict[str, dict[str, Fraction]]:
return {
axis: {
primitive: parse_fraction_json(weight)
for primitive, weight in row.items()
}
for axis, row in items.items()
}
def vector_json(vector: dict[str, Fraction]) -> dict[str, dict[str, Any]]:
return {key: fraction_json(value) for key, value in sorted(vector.items())}
def signed_l1(vector: dict[str, Fraction]) -> Fraction:
return sum((abs(value) for value in vector.values()), Fraction(0))

32
4-Infrastructure/hardware/standard_model_signed_axis_graph.py
View file

@ -4,7 +4,6 @@
from __future__ import annotations
import argparse
import hashlib
import json
from datetime import datetime, timezone
from fractions import Fraction
@ -13,44 +12,25 @@ from typing import Any
from xml.sax.saxutils import escape
from standard_model_lagrangian_eigen_probe import NODES
import sys
REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO / "4-Infrastructure"))
from lib.hashing import sha256_bytes
from lib.fraction_utils import fraction_json, fraction_str
from lib.jsonl import stable_json
SHAPE = REPO / "4-Infrastructure" / "hardware" / "standard_model_underverse_manifold_shape_receipt.json"
AVERAGE = REPO / "4-Infrastructure" / "hardware" / "standard_model_lagrangian_exact_average_receipt.json"
OUT_JSON = REPO / "4-Infrastructure" / "hardware" / "standard_model_signed_axis_graph_receipt.json"
OUT_GRAPHML = REPO / "4-Infrastructure" / "hardware" / "standard_model_signed_axis_graph.graphml"
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def file_hash(path: Path) -> str:
return sha256_bytes(path.read_bytes())
def frac_from_json(obj: dict[str, Any]) -> Fraction:
return Fraction(int(obj["numerator"]), int(obj["denominator"]))
def fraction_str(value: Fraction) -> str:
return str(value.numerator) if value.denominator == 1 else f"{value.numerator}/{value.denominator}"
def fraction_json(value: Fraction) -> dict[str, Any]:
return {
"fraction": fraction_str(value),
"numerator": value.numerator,
"denominator": value.denominator,
"decimal": float(value),
}
def load_inputs() -> tuple[dict[str, Any], dict[str, Any]]:
return (
json.loads(SHAPE.read_text(encoding="utf-8")),

28
4-Infrastructure/hardware/standard_model_underverse_manifold_shape.py
View file

@ -15,7 +15,6 @@ It is a symbolic/compression manifold, not a physical spacetime manifold.
from __future__ import annotations
import argparse
import hashlib
import json
import math
from datetime import datetime, timezone
@ -25,41 +24,26 @@ from typing import Any
from standard_model_lagrangian_eigen_probe import NODES
from standard_model_lagrangian_exact_average import QPhi, fraction_str
import sys
REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO / "4-Infrastructure"))
from lib.hashing import sha256_bytes
from lib.fraction_utils import fraction_json
from lib.jsonl import stable_json
AVERAGE = REPO / "4-Infrastructure" / "hardware" / "standard_model_lagrangian_exact_average_receipt.json"
CLOSURE = REPO / "4-Infrastructure" / "hardware" / "standard_model_lagrangian_underverse_closure_receipt.json"
EIGEN = REPO / "4-Infrastructure" / "hardware" / "standard_model_lagrangian_eigen_probe_receipt.json"
OUT = REPO / "4-Infrastructure" / "hardware" / "standard_model_underverse_manifold_shape_receipt.json"
PHI = (1.0 + math.sqrt(5.0)) / 2.0
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def file_hash(path: Path) -> str:
return sha256_bytes(path.read_bytes())
def frac_from_json(obj: dict[str, Any]) -> Fraction:
return Fraction(int(obj["numerator"]), int(obj["denominator"]))
def fraction_json(value: Fraction) -> dict[str, Any]:
return {
"fraction": fraction_str(value),
"numerator": value.numerator,
"denominator": value.denominator,
"decimal": float(value),
}
def qphi_from_json(obj: dict[str, Any]) -> QPhi:
return QPhi(Fraction(obj["a"]), Fraction(obj["b"]))

38
4-Infrastructure/hardware/standard_model_w_conservation_guard.py
View file

@ -18,15 +18,20 @@ physical Standard Model calculation.
from __future__ import annotations
import argparse
import hashlib
import json
from datetime import datetime, timezone
from fractions import Fraction
from pathlib import Path
from typing import Any
import sys
REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO / "4-Infrastructure"))
from lib.hashing import sha256_bytes
from lib.fraction_utils import fraction_json, fraction_str, parse_fraction_json
from lib.jsonl import load_json, stable_json
ACCOUNTING_RECEIPT = (
REPO
/ "4-Infrastructure"
@ -57,37 +62,6 @@ W_LINKED_AXES = (
"ghost_gaugefix_sector",
"derivative_kinetic_flow",
)
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def fraction_str(value: Fraction) -> str:
return str(value.numerator) if value.denominator == 1 else f"{value.numerator}/{value.denominator}"
def fraction_json(value: Fraction) -> dict[str, Any]:
return {
"fraction": fraction_str(value),
"numerator": value.numerator,
"denominator": value.denominator,
"decimal": float(value),
}
def parse_fraction_json(item: dict[str, Any]) -> Fraction:
return Fraction(int(item["numerator"]), int(item["denominator"]))
def load_json(path: Path) -> dict[str, Any]:
return json.loads(path.read_text(encoding="utf-8"))
def row_support(row: dict[str, dict[str, Any]]) -> tuple[str, ...]:
return tuple(sorted(row))

11
4-Infrastructure/hardware/test_fpga.py
View file

@ -11,17 +11,16 @@ import serial
import struct
import time
import sys
from pathlib import Path
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.q16 import Q16_ONE, Q16_SCALE, to_q16
UART_BAUD = 115384 # Matches Lean uartBaudDivisor (233)
UART_TIMEOUT = 2
# Q16_16 constants
Q16_SCALE = 65536
Q16_ONE = 65536
def q16_from_float(f: float) -> int:
return max(-2147483648, min(2147483647, int(f * Q16_SCALE)))
def q16_to_float(q: int) -> float:
if q > 2147483647:
q -= 4294967296

509
4-Infrastructure/infra/embedded_surface/rs-surface/Cargo.lock generated
View file

@ -155,9 +155,9 @@ checksum = "72b3254f16251a8381aa12e40e3c4d2f0199f8c6508fbecb9d91f575e0fbb8c6"
[[package]]
name = "base64ct"
version = "1.8.3"
version = "1.7.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "2af50177e190e07a26ab74f8b1efbfe2ef87da2116221318cb1c2e82baf7de06"
checksum = "89e25b6adfb930f02d1981565a6e5d9c547ac15a96606256d3b59040e5cd4ca3"
[[package]]
name = "bcder"
@ -184,15 +184,6 @@ dependencies = [
"generic-array",
]
[[package]]
name = "block-buffer"
version = "0.12.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "cdd35008169921d80bc60d3d0ab416eecb028c4cd653352907921d95084790be"
dependencies = [
"hybrid-array",
]
[[package]]
name = "bumpalo"
version = "3.20.3"
@ -229,17 +220,6 @@ version = "1.0.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801"
[[package]]
name = "chacha20"
version = "0.10.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6f8d983286843e49675a4b7a2d174efe136dc93a18d69130dd18198a6c167601"
dependencies = [
"cfg-if",
"cpufeatures 0.3.0",
"rand_core 0.10.1",
]
[[package]]
name = "chrono"
version = "0.4.44"
@ -260,24 +240,12 @@ dependencies = [
"cc",
]
[[package]]
name = "cmov"
version = "0.5.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3f88a43d011fc4a6876cb7344703e297c71dda42494fee094d5f7c76bf13f746"
[[package]]
name = "const-oid"
version = "0.9.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "c2459377285ad874054d797f3ccebf984978aa39129f6eafde5cdc8315b612f8"
[[package]]
name = "const-oid"
version = "0.10.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a6ef517f0926dd24a1582492c791b6a4818a4d94e789a334894aa15b0d12f55c"
[[package]]
name = "core-foundation-sys"
version = "0.8.7"
@ -293,15 +261,6 @@ dependencies = [
"libc",
]
[[package]]
name = "cpufeatures"
version = "0.3.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8b2a41393f66f16b0823bb79094d54ac5fbd34ab292ddafb9a0456ac9f87d201"
dependencies = [
"libc",
]
[[package]]
name = "crc32fast"
version = "1.5.0"
@ -321,24 +280,6 @@ dependencies = [
"typenum",
]
[[package]]
name = "crypto-common"
version = "0.2.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ce6e4c961d6cd6c9a86db418387425e8bdeaf05b3c8bc1411e6dca4c252f1453"
dependencies = [
"hybrid-array",
]
[[package]]
name = "ctutils"
version = "0.4.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "7d5515a3834141de9eafb9717ad39eea8247b5674e6066c404e8c4b365d2a29e"
dependencies = [
"cmov",
]
[[package]]
name = "data-encoding"
version = "2.11.0"
@ -351,7 +292,7 @@ version = "0.7.10"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e7c1832837b905bbfb5101e07cc24c8deddf52f93225eee6ead5f4d63d53ddcb"
dependencies = [
"const-oid 0.9.6",
"const-oid",
"zeroize",
]
@ -361,20 +302,9 @@ version = "0.10.7"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9ed9a281f7bc9b7576e61468ba615a66a5c8cfdff42420a70aa82701a3b1e292"
dependencies = [
"block-buffer 0.10.4",
"crypto-common 0.1.7",
]
[[package]]
name = "digest"
version = "0.11.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "f1dd6dbb5841937940781866fa1281a1ff7bd3bf827091440879f9994983d5c2"
dependencies = [
"block-buffer 0.12.0",
"const-oid 0.10.2",
"crypto-common 0.2.2",
"ctutils",
"block-buffer",
"crypto-common",
"subtle",
]
[[package]]
@ -383,12 +313,6 @@ version = "1.0.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "92773504d58c093f6de2459af4af33faa518c13451eb8f2b5698ed3d36e7c813"
[[package]]
name = "equivalent"
version = "1.0.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f"
[[package]]
name = "errno"
version = "0.3.14"
@ -396,7 +320,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb"
dependencies = [
"libc",
"windows-sys 0.61.2",
"windows-sys 0.52.0",
]
[[package]]
@ -421,12 +345,6 @@ dependencies = [
"miniz_oxide",
]
[[package]]
name = "foldhash"
version = "0.1.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d9c4f5dac5e15c24eb999c26181a6ca40b39fe946cbe4c263c7209467bc83af2"
[[package]]
name = "form_urlencoded"
version = "1.2.2"
@ -458,6 +376,17 @@ version = "0.3.32"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "7e3450815272ef58cec6d564423f6e755e25379b217b0bc688e295ba24df6b1d"
[[package]]
name = "futures-macro"
version = "0.3.32"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e835b70203e41293343137df5c0664546da5745f82ec9b84d40be8336958447b"
dependencies = [
"proc-macro2",
"quote",
"syn",
]
[[package]]
name = "futures-sink"
version = "0.3.32"
@ -477,6 +406,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "389ca41296e6190b48053de0321d02a77f32f8a5d2461dd38762c0593805c6d6"
dependencies = [
"futures-core",
"futures-macro",
"futures-sink",
"futures-task",
"pin-project-lite",
@ -501,7 +431,7 @@ checksum = "ff2abc00be7fca6ebc474524697ae276ad847ad0a6b3faa4bcb027e9a4614ad0"
dependencies = [
"cfg-if",
"libc",
"wasi 0.11.1+wasi-snapshot-preview1",
"wasi",
]
[[package]]
@ -512,45 +442,10 @@ checksum = "899def5c37c4fd7b2664648c28120ecec138e4d395b459e5ca34f9cce2dd77fd"
dependencies = [
"cfg-if",
"libc",
"r-efi 5.3.0",
"r-efi",
"wasip2",
]
[[package]]
name = "getrandom"
version = "0.4.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0de51e6874e94e7bf76d726fc5d13ba782deca734ff60d5bb2fb2607c7406555"
dependencies = [
"cfg-if",
"libc",
"r-efi 6.0.0",
"rand_core 0.10.1",
"wasip2",
"wasip3",
]
[[package]]
name = "hashbrown"
version = "0.15.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1"
dependencies = [
"foldhash",
]
[[package]]
name = "hashbrown"
version = "0.17.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ed5909b6e89a2db4456e54cd5f673791d7eca6732202bbf2a9cc504fe2f9b84a"
[[package]]
name = "heck"
version = "0.5.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea"
[[package]]
name = "hex"
version = "0.4.3"
@ -559,11 +454,11 @@ checksum = "7f24254aa9a54b5c858eaee2f5bccdb46aaf0e486a595ed5fd8f86ba55232a70"
[[package]]
name = "hmac"
version = "0.13.0"
version = "0.12.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6303bc9732ae41b04cb554b844a762b4115a61bfaa81e3e83050991eeb56863f"
checksum = "6c49c37c09c17a53d937dfbb742eb3a961d65a994e6bcdcf37e7399d0cc8ab5e"
dependencies = [
"digest 0.11.3",
"digest",
]
[[package]]
@ -617,15 +512,6 @@ version = "1.0.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "df3b46402a9d5adb4c86a0cf463f42e19994e3ee891101b1841f30a545cb49a9"
[[package]]
name = "hybrid-array"
version = "0.4.12"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9155a582abd142abc056962c29e3ce5ff2ad5469f4246b537ed42c5deba857da"
dependencies = [
"typenum",
]
[[package]]
name = "hyper"
version = "1.9.0"
@ -685,24 +571,6 @@ dependencies = [
"cc",
]
[[package]]
name = "id-arena"
version = "2.3.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3d3067d79b975e8844ca9eb072e16b31c3c1c36928edf9c6789548c524d0d954"
[[package]]
name = "indexmap"
version = "2.14.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9"
dependencies = [
"equivalent",
"hashbrown 0.17.1",
"serde",
"serde_core",
]
[[package]]
name = "itoa"
version = "1.0.18"
@ -737,12 +605,6 @@ version = "1.5.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe"
[[package]]
name = "leb128fmt"
version = "0.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2"
[[package]]
name = "libc"
version = "0.2.186"
@ -755,7 +617,10 @@ version = "0.1.16"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e02f3bb43d335493c96bf3fd3a321600bf6bd07ed34bc64118e9293bdffea46c"
dependencies = [
"bitflags",
"libc",
"plain",
"redox_syscall 0.7.5",
]
[[package]]
@ -790,12 +655,12 @@ checksum = "0e7465ac9959cc2b1404e8e2367b43684a6d13790fe23056cc8c6c5a6b7bcb94"
[[package]]
name = "md-5"
version = "0.11.0"
version = "0.10.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "69b6441f590336821bb897fb28fc622898ccceb1d6cea3fde5ea86b090c4de98"
checksum = "d89e7ee0cfbedfc4da3340218492196241d89eefb6dab27de5df917a6d2e78cf"
dependencies = [
"cfg-if",
"digest 0.11.3",
"digest",
]
[[package]]
@ -837,7 +702,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "50b7e5b27aa02a74bac8c3f23f448f8d87ff11f92d3aac1a6ed369ee08cc56c1"
dependencies = [
"libc",
"wasi 0.11.1+wasi-snapshot-preview1",
"wasi",
"windows-sys 0.61.2",
]
@ -859,24 +724,6 @@ dependencies = [
"autocfg",
]
[[package]]
name = "objc2-core-foundation"
version = "0.3.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "2a180dd8642fa45cdb7dd721cd4c11b1cadd4929ce112ebd8b9f5803cc79d536"
dependencies = [
"bitflags",
]
[[package]]
name = "objc2-system-configuration"
version = "0.3.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "7216bd11cbda54ccabcab84d523dc93b858ec75ecfb3a7d89513fa22464da396"
dependencies = [
"objc2-core-foundation",
]
[[package]]
name = "once_cell"
version = "1.21.4"
@ -901,7 +748,7 @@ checksum = "2621685985a2ebf1c516881c026032ac7deafcda1a2c9b7850dc81e3dfcb64c1"
dependencies = [
"cfg-if",
"libc",
"redox_syscall",
"redox_syscall 0.5.18",
"smallvec",
"windows-link",
]
@ -924,19 +771,18 @@ checksum = "9b4f627cb1b25917193a259e49bdad08f671f8d9708acfd5fe0a8c1455d87220"
[[package]]
name = "phf"
version = "0.13.1"
version = "0.11.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "c1562dc717473dbaa4c1f85a36410e03c047b2e7df7f45ee938fbef64ae7fadf"
checksum = "1fd6780a80ae0c52cc120a26a1a42c1ae51b247a253e4e06113d23d2c2edd078"
dependencies = [
"phf_shared",
"serde",
]
[[package]]
name = "phf_shared"
version = "0.13.1"
version = "0.11.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e57fef6bc5981e38c2ce2d63bfa546861309f875b8a75f092d1d54ae2d64f266"
checksum = "67eabc2ef2a60eb7faa00097bd1ffdb5bd28e62bf39990626a582201b7a754e5"
dependencies = [
"siphasher",
]
@ -948,10 +794,16 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd"
[[package]]
name = "postgres-protocol"
version = "0.6.11"
name = "plain"
version = "0.2.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "56201207dac53e2f38e848e31b4b91616a6bb6e0c7205b77718994a7f49e70fc"
checksum = "b4596b6d070b27117e987119b4dac604f3c58cfb0b191112e24771b2faeac1a6"
[[package]]
name = "postgres-protocol"
version = "0.6.9"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "fbef655056b916eb868048276cfd5d6a7dea4f81560dfd047f97c8c6fe3fcfd4"
dependencies = [
"base64",
"byteorder",
@ -960,21 +812,21 @@ dependencies = [
"hmac",
"md-5",
"memchr",
"rand 0.10.1",
"sha2 0.11.0",
"rand 0.9.4",
"sha2",
"stringprep",
]
[[package]]
name = "postgres-types"
version = "0.2.13"
version = "0.2.9"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8dc729a129e682e8d24170cd30ae1aa01b336b096cbb56df6d534ffec133d186"
checksum = "613283563cd90e1dfc3518d548caee47e0e725455ed619881f5cf21f36de4b48"
dependencies = [
"bytes",
"fallible-iterator",
"postgres-protocol",
"serde_core",
"serde",
"serde_json",
]
@ -987,16 +839,6 @@ dependencies = [
"zerocopy",
]
[[package]]
name = "prettyplease"
version = "0.2.37"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "479ca8adacdd7ce8f1fb39ce9ecccbfe93a3f1344b3d0d97f20bc0196208f62b"
dependencies = [
"proc-macro2",
"syn",
]
[[package]]
name = "proc-macro2"
version = "1.0.106"
@ -1021,12 +863,6 @@ version = "5.3.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f"
[[package]]
name = "r-efi"
version = "6.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf"
[[package]]
name = "rand"
version = "0.8.6"
@ -1034,19 +870,18 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5ca0ecfa931c29007047d1bc58e623ab12e5590e8c7cc53200d5202b69266d8a"
dependencies = [
"libc",
"rand_chacha",
"rand_chacha 0.3.1",
"rand_core 0.6.4",
]
[[package]]
name = "rand"
version = "0.10.1"
version = "0.9.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d2e8e8bcc7961af1fdac401278c6a831614941f6164ee3bf4ce61b7edb162207"
checksum = "44c5af06bb1b7d3216d91932aed5265164bf384dc89cd6ba05cf59a35f5f76ea"
dependencies = [
"chacha20",
"getrandom 0.4.2",
"rand_core 0.10.1",
"rand_chacha 0.9.0",
"rand_core 0.9.5",
]
[[package]]
@ -1059,6 +894,16 @@ dependencies = [
"rand_core 0.6.4",
]
[[package]]
name = "rand_chacha"
version = "0.9.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb"
dependencies = [
"ppv-lite86",
"rand_core 0.9.5",
]
[[package]]
name = "rand_core"
version = "0.6.4"
@ -1070,9 +915,12 @@ dependencies = [
[[package]]
name = "rand_core"
version = "0.10.1"
version = "0.9.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "63b8176103e19a2643978565ca18b50549f6101881c443590420e4dc998a3c69"
checksum = "76afc826de14238e6e8c374ddcc1fa19e374fd8dd986b0d2af0d02377261d83c"
dependencies = [
"getrandom 0.3.4",
]
[[package]]
name = "redox_syscall"
@ -1083,6 +931,15 @@ dependencies = [
"bitflags",
]
[[package]]
name = "redox_syscall"
version = "0.7.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "4666a1a60d8412eab19d94f6d13dcc9cea0a5ef4fdf6a5db306537413c661b1b"
dependencies = [
"bitflags",
]
[[package]]
name = "regex-automata"
version = "0.4.14"
@ -1126,7 +983,7 @@ dependencies = [
"rustls",
"serde",
"serde_json",
"sha2 0.10.9",
"sha2",
"tokio",
"tokio-postgres",
"tokio-postgres-rustls",
@ -1191,12 +1048,6 @@ version = "1.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
[[package]]
name = "semver"
version = "1.0.28"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd"
[[package]]
name = "serde"
version = "1.0.228"
@ -1270,8 +1121,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e3bf829a2d51ab4a5ddf1352d8470c140cadc8301b2ae1789db023f01cedd6ba"
dependencies = [
"cfg-if",
"cpufeatures 0.2.17",
"digest 0.10.7",
"cpufeatures",
"digest",
]
[[package]]
@ -1281,19 +1132,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a7507d819769d01a365ab707794a4084392c824f54a7a6a7862f8c3d0892b283"
dependencies = [
"cfg-if",
"cpufeatures 0.2.17",
"digest 0.10.7",
]
[[package]]
name = "sha2"
version = "0.11.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "446ba717509524cb3f22f17ecc096f10f4822d76ab5c0b9822c5f9c284e825f4"
dependencies = [
"cfg-if",
"cpufeatures 0.3.0",
"digest 0.11.3",
"cpufeatures",
"digest",
]
[[package]]
@ -1354,6 +1194,16 @@ version = "1.15.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "67b1b7a3b5fe4f1376887184045fcf45c69e92af734b7aaddc05fb777b6fbd03"
[[package]]
name = "socket2"
version = "0.5.10"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e22376abed350d73dd1cd119b57ffccad95b4e585a7cda43e286245ce23c0678"
dependencies = [
"libc",
"windows-sys 0.52.0",
]
[[package]]
name = "socket2"
version = "0.6.3"
@ -1464,7 +1314,7 @@ dependencies = [
"parking_lot",
"pin-project-lite",
"signal-hook-registry",
"socket2",
"socket2 0.6.3",
"tokio-macros",
"windows-sys 0.61.2",
]
@ -1482,9 +1332,9 @@ dependencies = [
[[package]]
name = "tokio-postgres"
version = "0.7.17"
version = "0.7.13"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "4dd8df5ef180f6364759a6f00f7aadda4fbbac86cdee37480826a6ff9f3574ce"
checksum = "6c95d533c83082bb6490e0189acaa0bbeef9084e60471b696ca6988cd0541fb0"
dependencies = [
"async-trait",
"byteorder",
@ -1499,8 +1349,8 @@ dependencies = [
"pin-project-lite",
"postgres-protocol",
"postgres-types",
"rand 0.10.1",
"socket2",
"rand 0.9.4",
"socket2 0.5.10",
"tokio",
"tokio-util",
"whoami",
@ -1738,12 +1588,6 @@ version = "0.1.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "7df058c713841ad818f1dc5d3fd88063241cc61f49f5fbea4b951e8cf5a8d71d"
[[package]]
name = "unicode-xid"
version = "0.2.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853"
[[package]]
name = "untrusted"
version = "0.9.0"
@ -1774,41 +1618,20 @@ version = "0.11.1+wasi-snapshot-preview1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b"
[[package]]
name = "wasi"
version = "0.14.7+wasi-0.2.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "883478de20367e224c0090af9cf5f9fa85bed63a95c1abf3afc5c083ebc06e8c"
dependencies = [
"wasip2",
]
[[package]]
name = "wasip2"
version = "1.0.3+wasi-0.2.9"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "20064672db26d7cdc89c7798c48a0fdfac8213434a1186e5ef29fd560ae223d6"
dependencies = [
"wit-bindgen 0.57.1",
]
[[package]]
name = "wasip3"
version = "0.4.0+wasi-0.3.0-rc-2026-01-06"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5428f8bf88ea5ddc08faddef2ac4a67e390b88186c703ce6dbd955e1c145aca5"
dependencies = [
"wit-bindgen 0.51.0",
"wit-bindgen",
]
[[package]]
name = "wasite"
version = "1.0.2"
version = "0.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "66fe902b4a6b8028a753d5424909b764ccf79b7a209eac9bf97e59cda9f71a42"
dependencies = [
"wasi 0.14.7+wasi-0.2.4",
]
checksum = "b8dad83b4f25e74f184f64c43b150b91efe7647395b42289f38e50566d82855b"
[[package]]
name = "wasm-bindgen"
@ -1855,40 +1678,6 @@ dependencies = [
"unicode-ident",
]
[[package]]
name = "wasm-encoder"
version = "0.244.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "990065f2fe63003fe337b932cfb5e3b80e0b4d0f5ff650e6985b1048f62c8319"
dependencies = [
"leb128fmt",
"wasmparser",
]
[[package]]
name = "wasm-metadata"
version = "0.244.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "bb0e353e6a2fbdc176932bbaab493762eb1255a7900fe0fea1a2f96c296cc909"
dependencies = [
"anyhow",
"indexmap",
"wasm-encoder",
"wasmparser",
]
[[package]]
name = "wasmparser"
version = "0.244.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "47b807c72e1bac69382b3a6fb3dbe8ea4c0ed87ff5629b8685ae6b9a611028fe"
dependencies = [
"bitflags",
"hashbrown 0.15.5",
"indexmap",
"semver",
]
[[package]]
name = "web-sys"
version = "0.3.99"
@ -1919,13 +1708,11 @@ dependencies = [
[[package]]
name = "whoami"
version = "2.1.2"
version = "1.6.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "998767ef88740d1f5b0682a9c53c24431453923962269c2db68ee43788c5a40d"
checksum = "5d4a4db5077702ca3015d3d02d74974948aba2ad9e12ab7df718ee64ccd7e97d"
dependencies = [
"libc",
"libredox",
"objc2-system-configuration",
"wasite",
"web-sys",
]
@ -2071,100 +1858,12 @@ version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec"
[[package]]
name = "wit-bindgen"
version = "0.51.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d7249219f66ced02969388cf2bb044a09756a083d0fab1e566056b04d9fbcaa5"
dependencies = [
"wit-bindgen-rust-macro",
]
[[package]]
name = "wit-bindgen"
version = "0.57.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e"
[[package]]
name = "wit-bindgen-core"
version = "0.51.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ea61de684c3ea68cb082b7a88508a8b27fcc8b797d738bfc99a82facf1d752dc"
dependencies = [
"anyhow",
"heck",
"wit-parser",
]
[[package]]
name = "wit-bindgen-rust"
version = "0.51.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b7c566e0f4b284dd6561c786d9cb0142da491f46a9fbed79ea69cdad5db17f21"
dependencies = [
"anyhow",
"heck",
"indexmap",
"prettyplease",
"syn",
"wasm-metadata",
"wit-bindgen-core",
"wit-component",
]
[[package]]
name = "wit-bindgen-rust-macro"
version = "0.51.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0c0f9bfd77e6a48eccf51359e3ae77140a7f50b1e2ebfe62422d8afdaffab17a"
dependencies = [
"anyhow",
"prettyplease",
"proc-macro2",
"quote",
"syn",
"wit-bindgen-core",
"wit-bindgen-rust",
]
[[package]]
name = "wit-component"
version = "0.244.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9d66ea20e9553b30172b5e831994e35fbde2d165325bec84fc43dbf6f4eb9cb2"
dependencies = [
"anyhow",
"bitflags",
"indexmap",
"log",
"serde",
"serde_derive",
"serde_json",
"wasm-encoder",
"wasm-metadata",
"wasmparser",
"wit-parser",
]
[[package]]
name = "wit-parser"
version = "0.244.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ecc8ac4bc1dc3381b7f59c34f00b67e18f910c2c0f50015669dde7def656a736"
dependencies = [
"anyhow",
"id-arena",
"indexmap",
"log",
"semver",
"serde",
"serde_derive",
"serde_json",
"unicode-xid",
"wasmparser",
]
[[package]]
name = "x509-certificate"
version = "0.23.1"

10
4-Infrastructure/infra/ene_contextstream_mcp.py
View file

@ -9,7 +9,6 @@ available immediately.
from __future__ import annotations
import hashlib
import json
import os
import sqlite3
@ -22,6 +21,9 @@ import urllib.request
from pathlib import Path
from typing import Any
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.hashing import sha256_text
SERVER_NAME = "ene-contextstream"
SERVER_VERSION = "0.1.0"
@ -34,12 +36,6 @@ DEFAULT_CANDIDATE_ROOT = (
def now_ms() -> int:
return int(time.time() * 1000)
def sha256_text(text: str) -> str:
return hashlib.sha256(text.encode("utf-8")).hexdigest()
def json_text(data: Any) -> list[dict[str, str]]:
return [{"type": "text", "text": json.dumps(data, indent=2, sort_keys=True)}]

10
4-Infrastructure/infra/ene_plugins/tiddlywiki_bridge/tiddlywiki_ene_bridge.py
View file

@ -19,6 +19,10 @@ from dataclasses import asdict, dataclass
from datetime import datetime, timezone
from pathlib import Path
from typing import Any
import sys
sys.path.insert(0, str(Path(__file__).resolve().parents[4] / "4-Infrastructure"))
from lib.jsonl import canonical_json
PLUGIN_ID = "ene.tiddlywiki.bridge"
@ -74,12 +78,6 @@ def utc_now() -> str:
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def canonical_json(data: Any) -> str:
return json.dumps(data, sort_keys=True, separators=(",", ":"), ensure_ascii=False)
def slugify(title: str) -> str:
slug = title.strip().lower()
slug = re.sub(r"[^a-z0-9._ -]+", "", slug)

11
4-Infrastructure/lib/__init__.py Normal file
View file

@ -0,0 +1,11 @@
# 4-Infrastructure/lib — shared Python utilities for the Research Stack.
#
# Consolidates duplicated helpers (hashing, Q16_16 arithmetic, JSON/JSONL I/O,
# Fraction serialization) that were previously copy-pasted across dozens of
# scripts in 4-Infrastructure/ and 5-Applications/.
#
# Usage from any script in the repo:
# import sys
# from pathlib import Path
# sys.path.insert(0, str(Path(__file__).resolve().parents[<N>] / "4-Infrastructure"))
# from lib.hashing import sha256_file, sha256_text

43
4-Infrastructure/lib/fraction_utils.py Normal file
View file

@ -0,0 +1,43 @@
"""Shared Fraction serialization helpers for standard-model hardware probes."""
from __future__ import annotations
import json
from fractions import Fraction
from pathlib import Path
from typing import Any
def fraction_str(value: Fraction) -> str:
return str(value.numerator) if value.denominator == 1 else f"{value.numerator}/{value.denominator}"
def fraction_json(value: Fraction) -> dict[str, Any]:
return {
"fraction": fraction_str(value),
"numerator": value.numerator,
"denominator": value.denominator,
"decimal": float(value),
}
def parse_fraction_json(item: dict[str, Any]) -> Fraction:
return Fraction(int(item["numerator"]), int(item["denominator"]))
def vector_from_json(items: dict[str, dict[str, Any]]) -> dict[str, Fraction]:
return {key: parse_fraction_json(value) for key, value in items.items()}
def vector_json(vector: dict[str, Fraction]) -> dict[str, dict[str, Any]]:
return {key: fraction_json(value) for key, value in sorted(vector.items())}
def projection_from_json(
items: dict[str, dict[str, dict[str, Any]]],
) -> dict[str, dict[str, Fraction]]:
return {
axis: {
col: parse_fraction_json(cell) for col, cell in row.items()
}
for axis, row in items.items()
}

29
4-Infrastructure/lib/hashing.py Normal file
View file

@ -0,0 +1,29 @@
"""Shared SHA-256 helpers — single source of truth for the entire repo."""
from __future__ import annotations
import hashlib
from pathlib import Path
_BUF_SIZE = 1 << 20 # 1 MiB
def sha256_bytes(data: bytes) -> str:
"""Hex digest of raw bytes."""
return hashlib.sha256(data).hexdigest()
def sha256_text(text: str) -> str:
"""Hex digest of a UTF-8 string."""
return hashlib.sha256(text.encode("utf-8")).hexdigest()
def sha256_file(path: Path, buf_size: int = _BUF_SIZE) -> str:
"""Streaming hex digest of a file (handles arbitrarily large files)."""
h = hashlib.sha256()
with path.open("rb") as fh:
while True:
chunk = fh.read(buf_size)
if not chunk:
break
h.update(chunk)
return h.hexdigest()

46
4-Infrastructure/lib/jsonl.py Normal file
View file

@ -0,0 +1,46 @@
"""Shared JSON / JSONL I/O and canonical serialization helpers."""
from __future__ import annotations
import json
from pathlib import Path
from typing import Any
def load_json(path: Path) -> dict[str, Any]:
"""Read a JSON file and return its contents as a dict."""
return json.loads(path.read_text(encoding="utf-8"))
def load_jsonl(path: Path) -> list[dict[str, Any]]:
"""Read a JSONL file and return a list of dicts (skips blank lines)."""
rows: list[dict[str, Any]] = []
with path.open("r", encoding="utf-8") as fh:
for line in fh:
s = line.strip()
if s:
rows.append(json.loads(s))
return rows
def write_jsonl(path: Path, rows: list[dict[str, Any]], *, append: bool = False) -> None:
"""Write a list of dicts as JSONL (sorted keys for deterministic output)."""
path.parent.mkdir(parents=True, exist_ok=True)
mode = "a" if append else "w"
with path.open(mode, encoding="utf-8") as fh:
for row in rows:
fh.write(json.dumps(row, sort_keys=True, ensure_ascii=False) + "\n")
def stable_json(obj: Any) -> str:
"""Deterministic JSON string (sorted keys, compact separators, ASCII-safe)."""
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def canonical_json(obj: Any) -> str:
"""Deterministic JSON preserving raw non-ASCII characters."""
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=False)
def canonical_json_bytes(obj: Any) -> bytes:
"""Deterministic JSON as bytes — suitable for hashing."""
return canonical_json(obj).encode("utf-8")

59
4-Infrastructure/lib/q16.py Normal file
View file

@ -0,0 +1,59 @@
"""
Q16_16 fixed-point arithmetic for deterministic compute across all substrates.
All thresholds and metric values are stored as Q16_16 integers.
One = 0x00010000 = 65536. Float is forbidden in compute paths; the
converters here are boundary-only (JSON parsing, display).
"""
from __future__ import annotations
Q16_ONE: int = 0x00010000 # 65536
Q16_HALF: int = 0x00008000
Q16_SCALE: int = 65536
def to_q16(value: float) -> int:
"""Convert a float to Q16_16. Only allowed at the external boundary."""
return int(round(value * Q16_ONE))
def from_q16(value: int) -> float:
"""Convert Q16_16 back to float. Only for display, never in compute."""
return value / Q16_SCALE
def q16_add(a: int, b: int) -> int:
return a + b
def q16_sub(a: int, b: int) -> int:
return a - b
def q16_mul(a: int, b: int) -> int:
"""Multiply two Q16_16 values with normalization."""
return (a * b) // Q16_ONE
def q16_div(a: int, b: int) -> int:
"""Divide two Q16_16 values with normalization."""
if b == 0:
raise ZeroDivisionError("Q16 division by zero")
return (a * Q16_ONE) // b
def q16_gt(a: int, b: int) -> bool:
return a > b
def q16_ge(a: int, b: int) -> bool:
return a >= b
def ratio_q16(numerator: float, denominator: float) -> int:
"""Compute Q16_16 ratio of two floats, clamped to [0, 1]."""
if denominator == 0:
return 0
r = numerator / denominator
r = max(0.0, min(1.0, r))
return int(r * Q16_ONE)

30
4-Infrastructure/shim/alphaproof_loop.py
View file

@ -12,12 +12,16 @@ import json
import os
import re
import subprocess
import sys
import tempfile
import time
from datetime import datetime, timezone
from pathlib import Path
from typing import Optional, List, Dict
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.q16 import Q16_SCALE, q16_mul, to_q16
try:
import requests
HAS_REQUESTS = True
@ -40,8 +44,6 @@ OLLAMA_URL = os.environ.get("OLLAMA_URL", "http://localhost:11434")
DEFAULT_MODEL = os.environ.get("ALPHAPROOF_MODEL", "deepseek-coder-v2:16b")
LOG_DIR = Path(__file__).parent / "alphaproof_logs"
Q16_SCALE = 65536 # 2^16 for Q16.16 fixed-point
# ---------------------------------------------------------------------------
# Ollama LLM interface
@ -196,24 +198,6 @@ def verify_proof(lean_code: str, module_name: str = "Candidate",
# ---------------------------------------------------------------------------
# FPGA Q16 acceleration (Python placeholder)
# ---------------------------------------------------------------------------
def q16_multiply(a: int, b: int) -> int:
"""Q16.16 fixed-point multiplication.
(a * b) >> 16 with overflow clamping.
"""
result = (a * b) >> 16
# Clamp to Q16.16 range
INT32_MAX = 2147483647
INT32_MIN = -2147483648
return max(INT32_MIN, min(INT32_MAX, result))
def q16_from_float(f: float) -> int:
"""Convert float to Q16.16."""
return max(-2147483648, min(2147483647, round(f * Q16_SCALE)))
def q16_to_float(q: int) -> float:
"""Convert Q16.16 to float."""
return q / Q16_SCALE
@ -242,20 +226,20 @@ def fpga_accelerate(candidates: list[dict]) -> list[dict]:
code = c.get('code', '')
# Length penalty (shorter is better)
length_score = q16_from_float(1.0 / (1.0 + len(code) / 1000.0))
length_score = to_q16(1.0 / (1.0 + len(code) / 1000.0))
# Penalty for incomplete proofs
penalty = 0
for bad_word in ['sorry', 'admit', 'axiom', 'by omega']:
count = code.count(bad_word)
penalty += q16_from_float(count * 0.1)
penalty += to_q16(count * 0.1)
# Base score from length
base = length_score
# Bonus for having structure (def, theorem, proof)
if 'theorem' in code or 'lemma' in code:
base = q16_multiply(base, q16_from_float(1.2))
base = q16_mul(base, to_q16(1.2))
final_score = max(0, base - penalty)
c['q16_score'] = final_score

13
4-Infrastructure/shim/compare_tier1_vs_tier2.py
View file

@ -6,6 +6,11 @@ import os
import sys
from collections import Counter, defaultdict
from math import sqrt
from pathlib import Path
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.jsonl import load_jsonl
VECTORS_PATH = os.path.join(os.path.dirname(__file__), "../..",
"shared-data/pist_trace_tier2b_vectors.jsonl")
@ -15,14 +20,6 @@ COMPARISON_PATH = os.path.join(os.path.dirname(__file__), "../..",
"shared-data/pist_tier1_vs_tier2_comparison.json")
CONFUSION_PATH = os.path.join(os.path.dirname(__file__), "../..",
"shared-data/pist_tier2b_confusion_matrices.json")
def load_jsonl(path):
rows = []
with open(path) as f:
for line in f:
rows.append(json.loads(line))
return rows
def normalize(vectors):
n = len(vectors)
if n == 0: return vectors, [], []

17
4-Infrastructure/shim/dataset_ingest_rds.py
View file

@ -29,6 +29,16 @@ import psycopg2
import psycopg2.extras
from rds_connect import connect_rds
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.jsonl import load_json
def load_jsonl(path: Path) -> list:
"""Load a JSON file; return its contents if a list, else []."""
data = load_json(path)
return data if isinstance(data, list) else []
logging.basicConfig(level=logging.INFO, format="%(asctime)s %(levelname)s %(message)s")
log = logging.getLogger("dataset_ingest_rds")
@ -230,13 +240,6 @@ def record_receipt(conn, shim: str, status: str, metadata: dict, error: str | No
# ---------------------------------------------------------------------------
# Ingestion functions
# ---------------------------------------------------------------------------
def load_jsonl(path: Path) -> list:
"""Load json or jsonl file."""
with open(path, "r") as f:
data = json.load(f)
return data if isinstance(data, list) else []
def ingest_equations(conn) -> tuple[int, int]:
"""Ingest equations.json → knowledge.equations"""
fpath = BUNDLE_EQS / "equations.json"

19
4-Infrastructure/shim/fractal_dimension.py
View file

@ -21,10 +21,15 @@ DBC formula (Sarkar & Chaudhuri 1994):
from __future__ import annotations
import math
import sys
from pathlib import Path
from typing import List, Optional, Tuple
import numpy as np
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.q16 import q16_div, q16_mul
# ---------------------------------------------------------------------------
# Q16_16 helpers (fixed-point: 16 integer bits, 16 fractional bits)
# ---------------------------------------------------------------------------
@ -45,20 +50,6 @@ def q16_to_float(q: int) -> float:
def q16_from_ratio(num: int, den: int) -> int:
"""Q16_16 of (num / den) using integer arithmetic."""
return (num << 16) // den
def q16_mul(a: int, b: int) -> int:
"""Q16_16 multiply."""
return (a * b) >> 16
def q16_div(a: int, b: int) -> int:
"""Q16_16 divide."""
if b == 0:
raise ZeroDivisionError("Q16 division by zero")
return (a << 16) // b
def q16_log_approx(x: int) -> int:
"""
Approximate natural log in Q16_16 using integer Newton iteration.

30
4-Infrastructure/shim/gccl_waveprobe.py
View file

@ -29,6 +29,8 @@ from typing import Dict, List, Optional, Tuple
import sys as _sys
_sys.path.insert(0, str(Path(__file__).resolve().parent))
_sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.q16 import Q16_SCALE
try:
import numpy as np
@ -39,11 +41,22 @@ except ImportError:
# ── Q16_16 Fixed-Point ──────────────────────────────────────────────────────
Q16_SCALE = 65536
Q16_MAX = 32767
Q16_MIN = -32768
def q16_mul(a: int, b: int) -> int:
return max(Q16_MIN, min(Q16_MAX, (a * b) // Q16_SCALE))
def q16_add(a: int, b: int) -> int:
return max(Q16_MIN, min(Q16_MAX, a + b))
def q16_sub(a: int, b: int) -> int:
return max(Q16_MIN, min(Q16_MAX, a - b))
def q16_from_int(x: int) -> int:
raw = x * Q16_SCALE
return max(Q16_MIN, min(Q16_MAX, raw))
@ -59,20 +72,6 @@ def q16_abs(raw: int) -> int:
def q16_neg(raw: int) -> int:
return max(Q16_MIN, min(Q16_MAX, -raw))
def q16_mul(a: int, b: int) -> int:
return max(Q16_MIN, min(Q16_MAX, (a * b) // Q16_SCALE))
def q16_add(a: int, b: int) -> int:
return max(Q16_MIN, min(Q16_MAX, a + b))
def q16_sub(a: int, b: int) -> int:
return max(Q16_MIN, min(Q16_MAX, a - b))
# ── GCCL Law Axes (from GCCL.lean) ─────────────────────────────────────────
class LawAxis(IntEnum):
@ -564,6 +563,7 @@ def gccl_transition_check(
if __name__ == '__main__':
import sys
if len(sys.argv) < 2:
print("Usage: python gccl_waveprobe.py --test")
sys.exit(1)

20
4-Infrastructure/shim/hutter_jxl_starfield_eigenprobe.py
View file

@ -20,6 +20,12 @@ import time
from collections import deque
from pathlib import Path
from typing import Any
import sys
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.hashing import sha256_bytes, sha256_text
from lib.jsonl import stable_json
ROOT = Path(__file__).resolve().parents[2]
@ -38,20 +44,6 @@ PIST_FORMULA = (
CLAIM_BOUNDARY = (
"diagnostic_only_not_classifier_not_compression_claim_not_hutter_prize_claim"
)
def stable_json(value: Any) -> str:
return json.dumps(value, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def sha256_text(text: str) -> str:
return hashlib.sha256(text.encode("utf-8")).hexdigest()
def sha256_path(path: Path, chunk_size: int = 1024 * 1024) -> str:
h = hashlib.sha256()
with path.open("rb") as handle:

8
4-Infrastructure/shim/qr_spatial_hash.py
View file

@ -17,6 +17,9 @@ from pathlib import Path
import sys as _sys
_sys.path.insert(0, str(Path(__file__).resolve().parent))
_sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.q16 import Q16_SCALE, to_q16
# ── Morton Code (Z-order curve) ─────────────────────────────────────────────
@ -44,11 +47,6 @@ def mortonDecode(code: int) -> tuple:
# ── Q16_16 Fixed-Point ──────────────────────────────────────────────────────
Q16_SCALE = 65536
def q16_from_float(x: float) -> int:
return max(-32768, min(32767, int(x * Q16_SCALE)))
def q16_to_float(raw: int) -> float:
return raw / Q16_SCALE

26
4-Infrastructure/shim/scale_space_solver.py
View file

@ -18,6 +18,8 @@ are clustered together. The reduced problem is solved, then expanded back.
import json
import math
import subprocess
import sys
from pathlib import Path
from typing import Optional
# ── Tailscale Detection (graceful degradation) ──────────────────────────
@ -114,6 +116,9 @@ def latency_to_sigma(latency_class: int) -> float:
"""Map latency class to scale space sigma."""
return _LATENCY_CLASSES.get(latency_class, _LATENCY_CLASSES[4])['sigma']
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.q16 import Q16_SCALE, q16_mul, to_q16
try:
import numpy as np
HAS_NUMPY = True
@ -125,7 +130,6 @@ except ImportError:
# Q16.16 fixed-point arithmetic
# ---------------------------------------------------------------------------
Q16_SCALE = 65536 # 2^16
Q16_MAX = 2147483647 # 2^31 - 1
Q16_MIN = -2147483648 # -2^31
@ -133,23 +137,9 @@ Q16_MIN = -2147483648 # -2^31
def q16_clamp(v: int) -> int:
"""Clamp integer to Q16.16 representable range."""
return max(Q16_MIN, min(Q16_MAX, v))
def q16_from_float(f: float) -> int:
"""Convert float to Q16.16 fixed-point."""
return q16_clamp(round(f * Q16_SCALE))
def q16_to_float(q: int) -> float:
"""Convert Q16.16 fixed-point to float."""
return q / Q16_SCALE
def q16_multiply(a: int, b: int) -> int:
"""Q16.16 multiplication: (a * b) >> 16."""
return q16_clamp((a * b) >> 16)
def q16_exp(x_q16: int) -> int:
"""Q16.16 exponential: exp(x) where x is in Q16.16.
@ -157,7 +147,7 @@ def q16_exp(x_q16: int) -> int:
For FPGA, this would use a LUT-based approximation.
"""
x_float = q16_to_float(x_q16)
return q16_from_float(math.exp(x_float))
return to_q16(math.exp(x_float))
# ---------------------------------------------------------------------------
@ -187,7 +177,7 @@ def gaussian_kernel_q16(sigma: float, size: int = 256) -> list[int]:
for i in range(size):
x = (i - half) / half # Map to [-1, 1]
g = math.exp(-(x * x) / two_sigma_sq)
kernel_raw.append(q16_from_float(g))
kernel_raw.append(to_q16(g))
# Normalize so kernel sums to Q16_SCALE (1.0 in Q16.16)
raw_sum = sum(kernel_raw)
@ -223,7 +213,7 @@ def gaussian_kernel_2d_q16(sigma: float, size: int = 16) -> list[list[int]]:
dx = (x - half) / half
dy = (y - half) / half
g = math.exp(-(dx * dx + dy * dy) / two_sigma_sq)
v = q16_from_float(g)
v = to_q16(g)
row.append(v)
total += v
kernel.append(row)

40
4-Infrastructure/shim/vcn_famm_transport.py
View file

@ -45,6 +45,9 @@ from braid_vcn_encoder import (
)
from fractal_dimension import fractal_dimension, fd_compress_hint
_sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.q16 import Q16_SCALE
try:
import numpy as np
_HAS_NUMPY = True
@ -54,11 +57,25 @@ except ImportError:
# ── Q16_16 Fixed-Point (matches Lean FixedPoint.lean) ───────────────────────
Q16_SCALE = 65536 # 2^16
Q16_MAX = 32767 # max Q16_16 value
Q16_MIN = -32768 # min Q16_16 value
def q16_mul(a: int, b: int) -> int:
result = (a * b) >> 16
return max(Q16_MIN, min(Q16_MAX, result))
def q16_add(a: int, b: int) -> int:
result = a + b
return max(Q16_MIN, min(Q16_MAX, result))
def q16_sub(a: int, b: int) -> int:
result = a - b
return max(Q16_MIN, min(Q16_MAX, result))
def q16_from_int(x: int) -> int:
"""Convert integer to Q16_16 raw value."""
raw = x * Q16_SCALE
@ -79,26 +96,6 @@ def q16_neg(raw: int) -> int:
"""Negate in Q16_16."""
result = -raw
return max(Q16_MIN, min(Q16_MAX, result))
def q16_mul(a: int, b: int) -> int:
"""Multiply two Q16_16 values."""
result = (a * b) // Q16_SCALE
return max(Q16_MIN, min(Q16_MAX, result))
def q16_add(a: int, b: int) -> int:
"""Add two Q16_16 values."""
result = a + b
return max(Q16_MIN, min(Q16_MAX, result))
def q16_sub(a: int, b: int) -> int:
"""Subtract two Q16_16 values."""
result = a - b
return max(Q16_MIN, min(Q16_MAX, result))
# ── Gate Condition (from DegeneracyConversion.lean) ─────────────────────────
def gate_condition(residual: int, threshold: int) -> bool:
@ -519,6 +516,7 @@ def famm_decode(
if __name__ == '__main__':
import sys
if len(sys.argv) < 2:
print("Usage: python vcn_famm_transport.py <braid_data_file>")
print(" python vcn_famm_transport.py --test")

14
5-Applications/hutter_prize/scripts/benchmark.py
View file

@ -4,7 +4,6 @@
from __future__ import annotations
import argparse
import hashlib
import json
import os
import shlex
@ -19,6 +18,9 @@ from pathlib import Path
from derive_trinary_program import derive_payload
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.hashing import sha256_file
@dataclass
class CommandResult:
@ -39,16 +41,6 @@ THREAD_LIMIT_ENV_VARS = [
"RAYON_NUM_THREADS",
"TBB_NUM_THREADS",
]
def sha256_file(path: Path) -> str:
digest = hashlib.sha256()
with path.open("rb") as handle:
for chunk in iter(lambda: handle.read(1024 * 1024), b""):
digest.update(chunk)
return digest.hexdigest()
def run_command(command: str, *, env: dict[str, str] | None = None) -> CommandResult:
started = time.perf_counter()
completed = subprocess.run(

14
5-Applications/hutter_prize/scripts/build_review_packet.py
View file

@ -8,6 +8,10 @@ import hashlib
import json
import shutil
from pathlib import Path
import sys
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.hashing import sha256_file
DEFAULT_PACKET = [
@ -26,16 +30,6 @@ DEFAULT_REVIEW_QUESTIONS = [
"Are there obvious wording or trust problems that would confuse a careful reader?",
"What is the next smallest artifact that would materially improve review?",
]
def sha256_file(path: Path) -> str:
digest = hashlib.sha256()
with path.open("rb") as handle:
for chunk in iter(lambda: handle.read(1024 * 1024), b""):
digest.update(chunk)
return digest.hexdigest()
def parse_args() -> argparse.Namespace:
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument(

16
5-Applications/hutter_prize/scripts/derive_trinary_program.py
View file

@ -4,23 +4,17 @@
from __future__ import annotations
import argparse
import hashlib
import json
from pathlib import Path
import sys
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.hashing import sha256_file
WIDTH = 6
TRIT_MAP = {0: -1, 1: 0, 2: 1}
SCHEMA = "trinary_vm_derivation_v1"
def sha256_file(path: Path) -> str:
digest = hashlib.sha256()
with path.open("rb") as handle:
for chunk in iter(lambda: handle.read(1024 * 1024), b""):
digest.update(chunk)
return digest.hexdigest()
def byte_to_trits(value: int) -> list[int]:
digits = [0] * WIDTH
remaining = value

12
5-Applications/hutter_prize/scripts/emit_build_manifest.py
View file

@ -4,20 +4,14 @@
from __future__ import annotations
import argparse
import hashlib
import json
import subprocess
from datetime import datetime, timezone
from pathlib import Path
import sys
def sha256_file(path: Path) -> str:
digest = hashlib.sha256()
with path.open("rb") as handle:
for chunk in iter(lambda: handle.read(1024 * 1024), b""):
digest.update(chunk)
return digest.hexdigest()
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.hashing import sha256_file
def run(*args: str) -> str:
completed = subprocess.run(

10
5-Applications/hutter_prize/scripts/prepare_public_artifact.py
View file

@ -10,14 +10,8 @@ import subprocess
import sys
from pathlib import Path
def sha256_file(path: Path) -> str:
digest = hashlib.sha256()
with path.open("rb") as handle:
for chunk in iter(lambda: handle.read(1024 * 1024), b""):
digest.update(chunk)
return digest.hexdigest()
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.hashing import sha256_file
def detect_mode(path: Path, explicit_mode: str) -> str:
if explicit_mode != "auto":

11
5-Applications/hutter_prize/scripts/validate_derivation.py
View file

@ -4,7 +4,6 @@
from __future__ import annotations
import argparse
import hashlib
import json
import sys
from datetime import datetime, timezone
@ -12,14 +11,8 @@ from pathlib import Path
from derive_trinary_program import SCHEMA, derive_payload
def sha256_file(path: Path) -> str:
digest = hashlib.sha256()
with path.open("rb") as handle:
for chunk in iter(lambda: handle.read(1024 * 1024), b""):
digest.update(chunk)
return digest.hexdigest()
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.hashing import sha256_file
def parse_args() -> argparse.Namespace:
parser = argparse.ArgumentParser(description=__doc__)

11
5-Applications/hutter_prize/scripts/verify_builder_determinism.py
View file

@ -4,21 +4,14 @@
from __future__ import annotations
import argparse
import hashlib
import json
import subprocess
import sys
import tempfile
from pathlib import Path
def sha256_file(path: Path) -> str:
digest = hashlib.sha256()
with path.open("rb") as handle:
for chunk in iter(lambda: handle.read(1024 * 1024), b""):
digest.update(chunk)
return digest.hexdigest()
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.hashing import sha256_file
def file_map(root: Path) -> dict[str, str]:
files: dict[str, str] = {}

11
5-Applications/hutter_prize/scripts/verify_components.py
View file

@ -4,19 +4,12 @@
from __future__ import annotations
import argparse
import hashlib
import json
import sys
from pathlib import Path
def sha256_file(path: Path) -> str:
digest = hashlib.sha256()
with path.open("rb") as handle:
for chunk in iter(lambda: handle.read(1024 * 1024), b""):
digest.update(chunk)
return digest.hexdigest()
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.hashing import sha256_file
def parse_args() -> argparse.Namespace:
parser = argparse.ArgumentParser(description=__doc__)

10
5-Applications/scripts/generate_avm_gold_trace.py
View file

@ -1,4 +1,10 @@
import json
import sys
from pathlib import Path
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.q16 import to_q16
def sadd(a, b):
"""Saturating 32-bit signed addition."""
@ -6,10 +12,6 @@ def sadd(a, b):
if res > 0x7FFFFFFF: return 0x7FFFFFFF
if res < -0x80000000: return -0x80000000
return res
def to_q16_16(val):
return int(val * 65536)
class AVMReference:
def __init__(self):
self.state = {"stack": [], "pc": 0}

13
5-Applications/scripts/generate_lean_module_domain_graph.py
View file

@ -24,6 +24,11 @@ import xml.sax.saxutils as xml_escape
from collections import Counter, defaultdict
from pathlib import Path
import sys
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.jsonl import write_jsonl
ROOT = Path(__file__).resolve().parents[1]
LEAN_ROOT = ROOT / "0-Core-Formalism" / "lean"
DATA_OUT = ROOT / "shared-data" / "data" / "lean_module_graph"
@ -141,14 +146,6 @@ def parse_module(path: Path) -> dict:
"sorry_count": len(re.findall(r"\bsorry\b", text)),
"sha256": hashlib.sha256(text.encode("utf-8", errors="replace")).hexdigest(),
}
def write_jsonl(path: Path, rows: list[dict]) -> None:
with path.open("w", encoding="utf-8") as f:
for row in rows:
f.write(json.dumps(row, sort_keys=True) + "\n")
def write_csv(path: Path, rows: list[dict], fieldnames: list[str]) -> None:
with path.open("w", encoding="utf-8", newline="") as f:
writer = csv.DictWriter(f, fieldnames=fieldnames)

14
5-Applications/scripts/gsp/burgers_triad_core.py
View file

@ -1,11 +1,16 @@
import numpy as np
import sys
from pathlib import Path
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.q16 import Q16_ONE, q16_mul
# Phase 1 — Build BurgersTriadCore
# Q16.16 in the AVM hot path
# Q16.16 Constants
Q16_SHIFT = 16
Q16_ONE = 1 << Q16_SHIFT
Q16_MAX = (1 << 31) - 1
Q16_MIN = -(1 << 31)
@ -35,13 +40,6 @@ def q16_sat(x: int) -> int:
_sat_count += 1
return Q16_MIN
return x
def q16_mul(x: int, y: int) -> int:
"""Q16.16 Multiplication with saturation."""
# Multiply raw integers, then shift back by 16
res = (x * y) >> Q16_SHIFT
return q16_sat(res)
def triad_rhs(a: tuple[int, int, int], nu_eff: int) -> tuple[int, int, int]:
"""
Triad equations (Burgers):

42
5-Applications/scripts/hot_path_cold_path.py
View file

@ -25,6 +25,9 @@ from dataclasses import dataclass
from enum import Enum
from collections import deque
import sys
from pathlib import Path
try:
from sluq_triage import SLUQTriageSystem, StochasticTrajectory, TriageDecision
_HAS_SLUQ_TRIAGE = True
@ -32,48 +35,15 @@ except ImportError:
_HAS_SLUQ_TRIAGE = False
print("[!] SLUQ triage system not available")
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.q16 import Q16_ONE, Q16_SCALE, from_q16, q16_add, q16_div, q16_ge, q16_gt, q16_sub, to_q16
try:
from hypercube_topology import HypercubeTopologySystem, HypercubeNode
_HAS_HYPERCUBE = True
except ImportError:
_HAS_HYPERCUBE = False
print("[!] Hypercube topology system not available")
# Q16_16 fixed-point utilities (from Lean FixedPoint module)
Q16_ONE = 65536 # 1.0 in Q16_16
Q16_SCALE = 65536.0
def to_q16(value: float) -> int:
"""Convert float to Q16_16 fixed-point"""
return int(value * Q16_SCALE)
def from_q16(q16: int) -> float:
"""Convert Q16_16 fixed-point to float"""
return q16 / Q16_SCALE
def q16_add(a: int, b: int) -> int:
"""Add two Q16_16 values"""
return a + b
def q16_sub(a: int, b: int) -> int:
"""Subtract two Q16_16 values"""
return a - b
def q16_div(a: int, b: int) -> int:
"""Divide two Q16_16 values with normalization"""
if b == 0:
return 0
return (a * Q16_ONE) // b
def q16_gt(a: int, b: int) -> bool:
"""Greater than comparison for Q16_16"""
return a > b
def q16_ge(a: int, b: int) -> bool:
"""Greater than or equal comparison for Q16_16"""
return a >= b
@dataclass
class NodeAccessPattern:
"""Node access pattern (Lean: NodeAccessPattern)"""

14
5-Applications/scripts/hutter_nat_gpu_search.py
View file

@ -14,10 +14,14 @@ from __future__ import annotations
import json
import hashlib
import sys
import time
from pathlib import Path
from typing import Any
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.jsonl import stable_json
ROOT = Path(__file__).resolve().parents[1]
OUT = ROOT / "out" / "hutter_nat_gpu_search.json"
@ -47,14 +51,8 @@ LEAN_THEOREMS = [
"status_note": "requires compressedSize <= originalSize validity assumption",
},
]
def canonical_json(value: Any) -> str:
return json.dumps(value, sort_keys=True, separators=(",", ":"))
def content_hash(value: Any) -> str:
return hashlib.sha256(canonical_json(value).encode("utf-8")).hexdigest()
return hashlib.sha256(stable_json(value).encode("utf-8")).hexdigest()
def node_id(prefix: str, value: Any) -> str:
@ -106,7 +104,7 @@ def upsert_truth_dag(witness: dict[str, Any]) -> dict[str, Any]:
"type": "gpu_empirical_witness",
"timestamp": timestamp,
"data": witness,
"nibbles": len(canonical_json(witness).encode("utf-8")) * 2,
"nibbles": len(stable_json(witness).encode("utf-8")) * 2,
"verified": bool(witness["execution"]["all_passed"]),
"status": "VERIFIED_TRUE" if witness["execution"]["all_passed"] else "DRIFT",
}

23
5-Applications/scripts/ingest_venice_research_stack_conversation.py
View file

@ -3,13 +3,18 @@
from __future__ import annotations
import hashlib
import json
import shutil
import sqlite3
from datetime import datetime, timezone
from pathlib import Path
from typing import Any
import sys
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.hashing import sha256_bytes, sha256_text
from lib.jsonl import stable_json
ROOT = Path("/home/allaun/Documents/Research Stack")
@ -53,24 +58,8 @@ EVIDENCE_PATTERNS = {
"vectorless_database": "i need a vectorles approach with high token retension and external database stores",
"topology_agents": "once we have agents that can point out where the topology fits",
}
def sha256_bytes(data: bytes) -> str:
return hashlib.sha256(data).hexdigest()
def sha256_path(path: Path) -> str:
return sha256_bytes(path.read_bytes())
def sha256_text(text: str) -> str:
return hashlib.sha256(text.encode("utf-8")).hexdigest()
def stable_json(obj: Any) -> str:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True)
def slugify(value: str) -> str:
return "".join(ch if ch.isalnum() else "_" for ch in value.lower()).strip("_")

45
5-Applications/scripts/joule_energy.py
View file

@ -19,57 +19,22 @@ This Python shim provides:
"""
import json
import sys
import time
from pathlib import Path
from typing import Dict, List, Optional, Any
from dataclasses import dataclass
from collections import deque
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.q16 import Q16_ONE, Q16_SCALE, from_q16, q16_add, q16_div, q16_ge, q16_gt, q16_mul, q16_sub, to_q16
try:
from q_factor import QFactorSystem, QFactorAction, EnergyBalance as QFactorBalance, to_q16 as q16_to, from_q16 as q16_from
_HAS_QFACTOR = True
except ImportError:
_HAS_QFACTOR = False
print("[!] Q-Factor system not available")
# Q16_16 fixed-point utilities (from Lean FixedPoint module)
Q16_ONE = 65536 # 1.0 in Q16_16
Q16_SCALE = 65536.0
def to_q16(value: float) -> int:
"""Convert float to Q16_16 fixed-point"""
return int(value * Q16_SCALE)
def from_q16(q16: int) -> float:
"""Convert Q16_16 fixed-point to float"""
return q16 / Q16_SCALE
def q16_add(a: int, b: int) -> int:
"""Add two Q16_16 values"""
return a + b
def q16_sub(a: int, b: int) -> int:
"""Subtract two Q16_16 values"""
return a - b
def q16_mul(a: int, b: int) -> int:
"""Multiply two Q16_16 values with normalization"""
return (a * b) // Q16_ONE
def q16_div(a: int, b: int) -> int:
"""Divide two Q16_16 values with normalization"""
if b == 0:
return 0
return (a * Q16_ONE) // b
def q16_gt(a: int, b: int) -> bool:
"""Greater than comparison for Q16_16"""
return a > b
def q16_ge(a: int, b: int) -> bool:
"""Greater than or equal comparison for Q16_16"""
return a >= b
@dataclass
class AgentEnergyState:
"""Agent energy state (Lean: AgentEnergyState)"""

14
5-Applications/scripts/kotc/kotc_sim.py
View file

@ -13,7 +13,6 @@ Usage:
from __future__ import annotations
import argparse
import hashlib
import json
import re
import sys
@ -22,6 +21,13 @@ from enum import Enum
from pathlib import Path
from typing import Dict, List, Tuple
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.hashing import sha256_text as _sha256_text
def sha256_text(text: str) -> str:
return "sha256:" + _sha256_text(text)
class Mode(str, Enum):
DRAFT = "DRAFT"
@ -57,12 +63,6 @@ class CompletionReceipt:
policy_checks: Dict[str, str]
candidate_hash: str
notes: List[str]
def sha256_text(text: str) -> str:
return "sha256:" + hashlib.sha256(text.encode("utf-8")).hexdigest()
def q16_hex(units: int) -> str:
"""Encode integer units as Q16.16 raw hex."""
raw = max(0, min(units << 16, 0xFFFFFFFF))

18
5-Applications/scripts/md_to_jsonl_converter.py
View file

@ -14,11 +14,17 @@ NOTE: This is a legacy ingest surface and should be treated as non-authoritative
import argparse
import json
import sys
import hashlib
from pathlib import Path
from datetime import datetime, timezone
from typing import Dict, Any, List, Optional, Tuple
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.hashing import sha256_file as _sha256_file
def compute_sha256(filepath: Path) -> str:
return f"sha256:{_sha256_file(filepath)}"
def env_default(name: str, default: str) -> str:
try:
@ -58,16 +64,6 @@ TIER_MAPPING = {
"research": "AUX",
"architecture": "AUX",
}
def compute_sha256(filepath: Path) -> str:
sha256 = hashlib.sha256()
with open(filepath, "rb") as f:
for chunk in iter(lambda: f.read(8192), b""):
sha256.update(chunk)
return f"sha256:{sha256.hexdigest()}"
def infer_domain(filepath: Path, content: str) -> str:
name = filepath.stem.upper()
for patterns, domain in DOMAIN_PATTERNS.items():

3
5-Applications/scripts/q16_lut_generator.py
View file

@ -20,6 +20,7 @@ import numpy as np
import json
from pathlib import Path
def q16_add(a, b):
"""Q16_16 addition (wrapping)."""
return (a + b) & 0xFFFFFFFF
@ -36,7 +37,7 @@ def q16_mul(a, b):
def q16_div(a, b):
"""Q16_16 division (with division by zero handling)."""
if b == 0:
return 0xFFFFFFFF # Division by zero marker
return 0xFFFFFFFF
numerator = (a << 16) & 0xFFFFFFFFFFFFFFFF
return (numerator // b) & 0xFFFFFFFF

45
5-Applications/scripts/q_factor.py
View file

@ -19,57 +19,22 @@ This Python shim provides:
"""
import json
import sys
import time
from pathlib import Path
from typing import Dict, List, Optional, Any
from dataclasses import dataclass
from collections import deque
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.q16 import Q16_ONE, Q16_SCALE, from_q16, q16_add, q16_div, q16_ge, q16_gt, q16_mul, q16_sub, to_q16
try:
from temporal_spatial_ram import TemporalSpatialRAMSystem, NodePosition, TemporalSpatialResource
_HAS_TS_RAM = True
except ImportError:
_HAS_TS_RAM = False
print("[!] Temporal-spatial RAM system not available")
# Q16_16 fixed-point utilities (from Lean FixedPoint module)
Q16_ONE = 65536 # 1.0 in Q16_16
Q16_SCALE = 65536.0
def to_q16(value: float) -> int:
"""Convert float to Q16_16 fixed-point"""
return int(value * Q16_SCALE)
def from_q16(q16: int) -> float:
"""Convert Q16_16 fixed-point to float"""
return q16 / Q16_SCALE
def q16_add(a: int, b: int) -> int:
"""Add two Q16_16 values"""
return a + b
def q16_sub(a: int, b: int) -> int:
"""Subtract two Q16_16 values"""
return a - b
def q16_mul(a: int, b: int) -> int:
"""Multiply two Q16_16 values with normalization"""
return (a * b) // Q16_ONE
def q16_div(a: int, b: int) -> int:
"""Divide two Q16_16 values with normalization"""
if b == 0:
return 0
return (a * Q16_ONE) // b
def q16_gt(a: int, b: int) -> bool:
"""Greater than comparison for Q16_16"""
return a > b
def q16_ge(a: int, b: int) -> bool:
"""Greater than or equal comparison for Q16_16"""
return a >= b
@dataclass
class EnergyBalance:
"""Energy balance components (Lean: EnergyBalance)"""

35
5-Applications/scripts/sabotage_prevention.py
View file

@ -27,35 +27,14 @@ from dataclasses import dataclass, field
from enum import Enum
from collections import defaultdict, deque
import sys
from pathlib import Path
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.q16 import Q16_ONE, Q16_SCALE, from_q16, q16_add, q16_ge, q16_gt, q16_sub, to_q16
# Q16_16 fixed-point utilities (from Lean FixedPoint module)
Q16_ONE = 65536 # 1.0 in Q16_16
Q16_SCALE = 65536.0
def to_q16(value: float) -> int:
"""Convert float to Q16_16 fixed-point"""
return int(value * Q16_SCALE)
def from_q16(q16: int) -> float:
"""Convert Q16_16 fixed-point to float"""
return q16 / Q16_SCALE
def q16_add(a: int, b: int) -> int:
"""Add two Q16_16 values"""
return a + b
def q16_sub(a: int, b: int) -> int:
"""Subtract two Q16_16 values"""
return a - b
def q16_gt(a: int, b: int) -> bool:
"""Greater than comparison for Q16_16"""
return a > b
def q16_ge(a: int, b: int) -> bool:
"""Greater than or equal comparison for Q16_16"""
return a >= b
class ActionType(Enum):
"""Agent action type (Lean: ActionType)"""
IMPROVE_EFFICIENCY = "ImproveEfficiency"

45
5-Applications/scripts/temporal_spatial_ram.py
View file

@ -19,57 +19,22 @@ This Python shim provides:
"""
import json
import sys
import time
from pathlib import Path
from typing import Dict, List, Optional, Any
from dataclasses import dataclass
from collections import deque
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.q16 import Q16_ONE, Q16_SCALE, from_q16, q16_add, q16_div, q16_ge, q16_gt, q16_mul, q16_sub, to_q16
try:
from hot_path_cold_path import HotPathColdPathSystem, NodeAccessPattern, PathClassification
_HAS_HOT_COLD = True
except ImportError:
_HAS_HOT_COLD = False
print("[!] Hot path/cold path system not available")
# Q16_16 fixed-point utilities (from Lean FixedPoint module)
Q16_ONE = 65536 # 1.0 in Q16_16
Q16_SCALE = 65536.0
def to_q16(value: float) -> int:
"""Convert float to Q16_16 fixed-point"""
return int(value * Q16_SCALE)
def from_q16(q16: int) -> float:
"""Convert Q16_16 fixed-point to float"""
return q16 / Q16_SCALE
def q16_add(a: int, b: int) -> int:
"""Add two Q16_16 values"""
return a + b
def q16_sub(a: int, b: int) -> int:
"""Subtract two Q16_16 values"""
return a - b
def q16_mul(a: int, b: int) -> int:
"""Multiply two Q16_16 values with normalization"""
return (a * b) // Q16_ONE
def q16_div(a: int, b: int) -> int:
"""Divide two Q16_16 values with normalization"""
if b == 0:
return 0
return (a * Q16_ONE) // b
def q16_gt(a: int, b: int) -> bool:
"""Greater than comparison for Q16_16"""
return a > b
def q16_ge(a: int, b: int) -> bool:
"""Greater than or equal comparison for Q16_16"""
return a >= b
@dataclass
class NodePosition:
"""Node position in topology (Lean: NodePosition)"""

19
5-Applications/scripts/text_container_to_jsonl.py
View file

@ -13,17 +13,22 @@ import argparse
import json
import csv
import sys
import hashlib
from pathlib import Path
from datetime import datetime, timezone
from typing import Dict, Any, List, Optional, Tuple
from dataclasses import dataclass
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.hashing import sha256_file as _sha256_file
def compute_sha256(filepath: Path) -> str:
return f"sha256:{_sha256_file(filepath)}"
def env_default(name: str, default: str) -> str:
try:
import os
v = os.environ.get(name)
except Exception:
v = None
@ -102,16 +107,6 @@ def should_skip(filepath: Path) -> Tuple[bool, str]:
return True, "too_large"
return False, ""
def compute_sha256(filepath: Path) -> str:
sha256 = hashlib.sha256()
with open(filepath, "rb") as f:
for chunk in iter(lambda: f.read(8192), b""):
sha256.update(chunk)
return f"sha256:{sha256.hexdigest()}"
def infer_domain(filepath: Path, content: str = "") -> str:
name = filepath.stem.upper()
path = str(filepath).upper()

10
5-Applications/scripts/wiki_builder_shim.py
View file

@ -27,7 +27,6 @@ Usage:
from __future__ import annotations
import argparse
import hashlib
import json
import os
import re
@ -39,6 +38,9 @@ from pathlib import Path
from textwrap import dedent
from typing import Any
sys.path.insert(0, str(Path(__file__).resolve().parents[2] / "4-Infrastructure"))
from lib.hashing import sha256_text
REPO_ROOT = Path(__file__).resolve().parents[2]
TIDDLER_DIR = REPO_ROOT / "6-Documentation" / "tiddlywiki-local" / "wiki" / "tiddlers"
@ -81,12 +83,6 @@ def slugify(text: str) -> str:
s = re.sub(r"[^a-z0-9._ -]+", "", s)
s = re.sub(r"\s+", "_", s).strip("_")
return s[:60] if s else "untitled"
def sha256_text(text: str) -> str:
return hashlib.sha256(text.encode("utf-8")).hexdigest()
def concept_vector_14(title: str, body: str, tags: list[str]) -> list[float]:
"""14D vector from keyword axis activation (mirrors tiddlywiki_ene_bridge pattern)."""
combined = f"{title}\n{body}\n{' '.join(tags)}".lower()

15
5-Applications/text-to-cad/skills/cad/scripts/common/render.py
View file

@ -1,6 +1,5 @@
from __future__ import annotations
import hashlib
import json
import tempfile
from pathlib import Path
@ -12,6 +11,10 @@ from common.catalog import (
viewer_artifact_path_for_step_path,
viewer_directory_for_step_path,
)
import sys
sys.path.insert(0, str(Path(__file__).resolve().parents[6] / "4-Infrastructure"))
from lib.hashing import sha256_file
REPO_ROOT = Path.cwd().resolve()
@ -104,16 +107,6 @@ def relative_to_repo(path: Path) -> str:
return resolved.relative_to(REPO_ROOT).as_posix()
except ValueError:
return resolved.as_posix()
def sha256_file(path: Path) -> str:
digest = hashlib.sha256()
with path.open("rb") as handle:
for chunk in iter(lambda: handle.read(1024 * 1024), b""):
digest.update(chunk)
return digest.hexdigest()
def versioned_repo_url(path: Path, content_hash: str) -> str:
resolved = path.resolve()
try:

21
5-Applications/tools-scripts/graph/drive_indexer.py
View file

@ -27,7 +27,6 @@ metrics.log on completion.
"""
import argparse
import hashlib
import json
import os
import sqlite3
@ -46,6 +45,10 @@ METRICS_LOG = REPO_ROOT / "metrics.log"
sys.path.insert(0, str(REPO_ROOT / "germane" / "tools"))
from waveprobe_hasher import hash_file, store_waveprobe_states # noqa: E402
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.hashing import sha256_file
CHUNK_SIZE = 64 * 1024 # 64 KB
# File extensions to skip (binary noise, OS artifacts)
@ -55,22 +58,6 @@ SKIP_EXTENSIONS = {
}
SKIP_NAMES_LOWER = {"thumbs.db", "desktop.ini", ".ds_store"}
def sha256_file(path: Path, buf_size: int = 1 << 20) -> str:
h = hashlib.sha256()
try:
with open(path, "rb") as f:
while True:
block = f.read(buf_size)
if not block:
break
h.update(block)
except OSError:
return ""
return h.hexdigest()
def share_name_from_path(root: Path) -> str:
"""Derive a share name from the mount-point directory name."""
return root.name.lower().replace(" ", "_")

29
5-Applications/tools-scripts/graph/file_manifest_builder.py
View file

@ -6,28 +6,13 @@
# Open-Source usage requires explicit permission from Brandon Scott Schneider.
# ==============================================================================
import argparse
import hashlib
import json
from pathlib import Path
from typing import Any, Dict, List, Tuple, cast
import sys
def sha256_hex_bytes(data: bytes) -> str:
h = hashlib.sha256()
h.update(data)
return h.hexdigest()
def sha256_file(path: Path) -> str:
h = hashlib.sha256()
with path.open("rb") as handle:
while True:
chunk = handle.read(1024 * 1024)
if not chunk:
break
h.update(chunk)
return h.hexdigest()
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.hashing import sha256_bytes, sha256_file
def chunk_file(path: Path, chunk_size: int) -> List[Tuple[int, int, bytes]]:
chunks: List[Tuple[int, int, bytes]] = []
@ -46,14 +31,14 @@ def chunk_file(path: Path, chunk_size: int) -> List[Tuple[int, int, bytes]]:
def build_manifest(input_path: Path, chunk_size: int) -> Dict[str, Any]:
file_bytes = input_path.read_bytes()
file_hash = sha256_hex_bytes(file_bytes)
file_hash = sha256_bytes(file_bytes)
chunks = chunk_file(input_path, chunk_size=chunk_size)
chunk_rows: List[Dict[str, Any]] = []
leaf_hashes: List[str] = []
for index, offset, data in chunks:
c_hash = sha256_hex_bytes(data)
c_hash = sha256_bytes(data)
leaf_hashes.append(c_hash)
chunk_rows.append(
{
@ -66,7 +51,7 @@ def build_manifest(input_path: Path, chunk_size: int) -> Dict[str, Any]:
}
)
merkle_root = sha256_hex_bytes("".join(leaf_hashes).encode("ascii")) if leaf_hashes else ""
merkle_root = sha256_bytes("".join(leaf_hashes).encode("ascii")) if leaf_hashes else ""
return {
"version": "manifest.v1",
@ -140,7 +125,7 @@ def rebuild_from_store(manifest: Dict[str, Any], chunk_store: Path, out_file: Pa
if len(data) != expected_len:
raise ValueError(f"chunk length mismatch for {digest}: got {len(data)} expected {expected_len}")
if sha256_hex_bytes(data) != digest:
if sha256_bytes(data) != digest:
raise ValueError(f"chunk hash mismatch for {digest}")
handle.write(data)

24
5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py
View file

@ -15,7 +15,6 @@ from __future__ import annotations
import argparse
import datetime as dt
import hashlib
import json
import os
import re
@ -26,6 +25,14 @@ from dataclasses import dataclass
from pathlib import Path
from typing import Any
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.hashing import sha256_bytes as _sha256_bytes
from lib.jsonl import canonical_json_bytes
def sha256_bytes(data: bytes) -> str:
return "sha256:" + _sha256_bytes(data)
REPO = Path(__file__).resolve().parents[3]
DEFAULT_OUTPUT_DIR = REPO / "shared-data" / "artifacts" / "deepseek_review"
@ -41,21 +48,6 @@ class EmittedReview:
receipt_path: Path
answer_sha256: str
prompt_sha256: str
def sha256_bytes(data: bytes) -> str:
return "sha256:" + hashlib.sha256(data).hexdigest()
def canonical_json_bytes(value: Any) -> bytes:
return json.dumps(
value,
ensure_ascii=False,
sort_keys=True,
separators=(",", ":"),
).encode("utf-8")
def repo_relative(path: Path, repo_root: Path = REPO) -> str:
path = path.resolve()
repo_root = repo_root.resolve()

16
5-Applications/tools-scripts/utils/check_passive_monitor_integrity.py
View file

@ -13,6 +13,10 @@ from typing import Any, Dict, List
from jsonschema import validate
import sys
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.jsonl import load_jsonl
PROJECT_ROOT = Path(__file__).resolve().parent.parent
CHAIN_SCHEMA = PROJECT_ROOT / "schemas" / "passive_chain_record.schema.json"
@ -20,18 +24,6 @@ CHAIN_SCHEMA = PROJECT_ROOT / "schemas" / "passive_chain_record.schema.json"
def parse_iso(ts: str) -> datetime:
return datetime.fromisoformat(ts.replace("Z", "+00:00"))
def load_jsonl(path: Path) -> List[Dict[str, Any]]:
rows: List[Dict[str, Any]] = []
with path.open("r", encoding="utf-8") as handle:
for line in handle:
s = line.strip()
if s:
rows.append(json.loads(s))
return rows
def parse_args() -> argparse.Namespace:
parser = argparse.ArgumentParser(description="Daily integrity check for passive all-market monitor records.")
parser.add_argument("--records", required=True, help="Path to chain_records.jsonl")

13
5-Applications/tools-scripts/utils/collect_macro_market_records.py
View file

@ -29,6 +29,9 @@ from typing import Any, Dict, Iterable, List, Mapping, Optional, Tuple, cast
from jsonschema import validate
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.jsonl import write_jsonl
PROJECT_ROOT = Path(__file__).resolve().parent.parent
SCHEMA_PATH = PROJECT_ROOT / "schemas" / "passive_macro_record.schema.json"
@ -323,16 +326,6 @@ def collect_records(args: argparse.Namespace, schema: Dict[str, Any]) -> List[Di
idx += 1
return records
def write_jsonl(path: Path, rows: List[Dict[str, Any]], append: bool) -> None:
path.parent.mkdir(parents=True, exist_ok=True)
mode = "a" if append else "w"
with path.open(mode, encoding="utf-8") as handle:
for row in rows:
handle.write(json.dumps(row, sort_keys=True) + "\n")
def parse_args() -> argparse.Namespace:
parser = argparse.ArgumentParser(description="Collect worldwide macro feeds with redundancy (Yahoo/Stooq/FRED) and source-consensus checks.")
parser.add_argument("--symbol", action="append", help="Optional override in the form market_class:SYMBOL. Repeatable.")

10
5-Applications/tools-scripts/utils/generate_diat_tables.py
View file

@ -1,7 +1,9 @@
import math
import sys
from pathlib import Path
def to_q16_16(val):
return int(val * 65536) & 0xFFFFFFFF
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.q16 import to_q16
def generate_mem_files():
# 256 entries, x = index / 16.0 (if we use ray_t[19:12] as addr)
@ -18,8 +20,8 @@ def generate_mem_files():
y_inv = 1.0 / math.sqrt(x)
y_sqrt = math.sqrt(x)
f_inv.write(f"{to_q16_16(y_inv):08x}\n")
f_sqrt.write(f"{to_q16_16(y_sqrt):08x}\n")
f_inv.write(f"{to_q16(y_inv):08x}\n")
f_sqrt.write(f"{to_q16(y_sqrt):08x}\n")
print("Success: Generated diat_inv_table.mem and diat_sqrt_table.mem")

18
5-Applications/tools-scripts/utils/generate_monthly_prepost_attestation.py
View file

@ -6,7 +6,6 @@
# Open-Source usage requires explicit permission from Brandon Scott Schneider.
# ==============================================================================
import argparse
import hashlib
import json
import sys
from datetime import datetime, timezone
@ -16,21 +15,10 @@ from typing import Any, Dict
sys.path.insert(0, str(Path(__file__).parent))
from rfc3161_stamp import stamp as rfc3161_stamp
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.hashing import sha256_file
def sha256_file(path: Path) -> str:
h = hashlib.sha256()
with path.open("rb") as handle:
while True:
chunk = handle.read(1024 * 1024)
if not chunk:
break
h.update(chunk)
return h.hexdigest()
def load_json(path: Path) -> Dict[str, Any]:
return json.loads(path.read_text(encoding="utf-8"))
from lib.jsonl import load_json
def parse_args() -> argparse.Namespace:
parser = argparse.ArgumentParser(description="Generate monthly PRE/POST accountability attestation package.")

9
5-Applications/tools-scripts/utils/generate_qchem_metadata.py
View file

@ -15,8 +15,11 @@ except ImportError:
from io_harness_compat import spawn_isolated_process, fetch_network_resource
import json
import hashlib
from pathlib import Path
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.hashing import sha256_text
# import subprocess (REMOVED BY WARDEN)
BASE_DIR = Path(__file__).parent.parent.resolve()
@ -25,10 +28,6 @@ MANIFEST_BIN = BASE_DIR / "scripts" / "file_manifest_builder.py"
MANIFEST_OUT = BASE_DIR / "hqw_atomic_combinations.manifest.json"
METADATA_OUT = BASE_DIR / "hqw_materials_metadata.jsonl"
CHUNK_STORE = BASE_DIR / "hqw_chunks"
def sha256_text(text):
return hashlib.sha256(text.encode()).hexdigest()
def generate_metadata():
print(f"[*] Reading {DATA_FILE}...")
with open(DATA_FILE, 'r') as f:

17
5-Applications/tools-scripts/utils/generate_trace_attestation.py
View file

@ -6,7 +6,6 @@
# Open-Source usage requires explicit permission from Brandon Scott Schneider.
# ==============================================================================
import argparse
import hashlib
import json
import sqlite3
import sys
@ -17,21 +16,11 @@ from typing import Any, Dict, List
sys.path.insert(0, str(Path(__file__).parent))
from rfc3161_stamp import stamp as rfc3161_stamp
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.hashing import sha256_file
PROJECT_ROOT = Path(__file__).resolve().parent.parent
def sha256_file(path: Path) -> str:
h = hashlib.sha256()
with path.open("rb") as handle:
while True:
chunk = handle.read(1024 * 1024)
if not chunk:
break
h.update(chunk)
return h.hexdigest()
def read_json(path: Path) -> Any:
return json.loads(path.read_text(encoding="utf-8"))

16
5-Applications/tools-scripts/utils/generate_weekly_ethics_digest.py
View file

@ -12,21 +12,13 @@ from datetime import datetime, timedelta, timezone
from pathlib import Path
from typing import Any, Dict, List, cast
import sys
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.jsonl import load_jsonl
def parse_iso(ts: str) -> datetime:
return datetime.fromisoformat(ts.replace("Z", "+00:00"))
def load_jsonl(path: Path) -> List[Dict[str, Any]]:
rows: List[Dict[str, Any]] = []
with path.open("r", encoding="utf-8") as handle:
for line in handle:
s = line.strip()
if s:
rows.append(json.loads(s))
return rows
def parse_args() -> argparse.Namespace:
parser = argparse.ArgumentParser(description="Generate weekly ethical accountability digest from PRE/POST records.")
parser.add_argument("--pre", required=True, help="Path to pre_records.jsonl")

12
5-Applications/tools-scripts/utils/validate_payout_candidates.py
View file

@ -21,10 +21,14 @@ from __future__ import annotations
import argparse
import csv
import json
import sys
from datetime import datetime, timezone
from pathlib import Path
from typing import Any, Dict, Iterable, List, Optional, Tuple, cast
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.jsonl import write_jsonl
try:
from zk_stark_spending_proof import (
default_spending_constraint,
@ -387,14 +391,6 @@ def generate_zk_stark_proof_for_candidate(
return proof
except (ValueError, KeyError, AttributeError):
return None
def write_jsonl(path: Path, rows: List[Dict[str, Any]]) -> None:
with path.open("w", encoding="utf-8") as fh:
for row in rows:
fh.write(json.dumps(row, ensure_ascii=False) + "\n")
def main() -> None:
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument("--candidates", required=True, help="Path to payout candidates (.csv or .jsonl)")

16
5-Applications/tools-scripts/utils/verify_pre_post_pairs.py
View file

@ -12,22 +12,14 @@ from typing import Any, Dict, List
from jsonschema import validate
import sys
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.jsonl import load_jsonl
PROJECT_ROOT = Path(__file__).resolve().parent.parent
PRE_SCHEMA = PROJECT_ROOT / "schemas" / "pre_record.schema.json"
POST_SCHEMA = PROJECT_ROOT / "schemas" / "post_record.schema.json"
def load_jsonl(path: Path) -> List[Dict[str, Any]]:
rows: List[Dict[str, Any]] = []
with path.open("r", encoding="utf-8") as handle:
for line in handle:
s = line.strip()
if s:
rows.append(json.loads(s))
return rows
def load_schema(path: Path) -> Dict[str, Any]:
return json.loads(path.read_text(encoding="utf-8"))

10
5-Applications/tools-scripts/utils/zero_metadata_loopback.py
View file

@ -13,15 +13,13 @@ import zlib
from pathlib import Path
from typing import Any, Dict, List, Tuple
import sys
sys.path.insert(0, str(Path(__file__).resolve().parents[3] / "4-Infrastructure"))
from lib.jsonl import canonical_json_bytes
MAGIC = b"SVSC1\x00"
HEADER_STRUCT = struct.Struct("<6s32sQQ")
def canonical_json_bytes(obj: Any) -> bytes:
return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=False).encode("utf-8")
def smooth_bytes_delta(data: bytes) -> bytes:
out = bytearray(len(data))
prev = 0

79
flake.nix
View file

@ -188,80 +188,6 @@
mkdir -p -m 1777 $out/tmp
'';
# ── rs-surface binary ───────────────────────────────────────────────────
# Rust port of 4-Infrastructure/infra/embedded_surface/server.py.
# Build the binary hermetically via rustPlatform.buildRustPackage.
#
# cargoHash: run `nix build .#rs-surface 2>&1 | grep "got:"` to get the
# real hash after any Cargo.lock change, then replace lib.fakeHash below.
rsSurface = pkgs.rustPlatform.buildRustPackage {
pname = "rs-surface";
version = "0.1.0";
src = pkgs.lib.cleanSource ./4-Infrastructure/infra/embedded_surface/rs-surface;
cargoLock.lockFile = ./4-Infrastructure/infra/embedded_surface/rs-surface/Cargo.lock;
nativeBuildInputs = [ pkgs.pkg-config ];
buildInputs = [ pkgs.openssl ];
meta = {
description = "Embedded node surface daemon (Rust)";
license = pkgs.lib.licenses.mit;
mainProgram = "rs-surface";
};
};
# ── Minimal OCI image for the embedded node surface ────────────────────
# Built entirely from the Nix store — no Dockerfile, no Alpine, no musl.
# The closure contains only the binary + its glibc runtime deps.
#
# Build: nix build .#rs-surface-image
# Load: docker load < result
# Run: docker run --rm -p 8080:8080 -v /etc/rs-surface:/etc/rs-surface rs-surface:latest
rsSurfaceImage = pkgs.dockerTools.buildLayeredImage {
name = "rs-surface";
tag = "latest";
contents = [
rsSurface
pkgs.cacert # TLS roots (for any outbound HTTPS)
pkgs.coreutils # minimal shell utilities for healthcheck
];
# /etc/rs-surface/node.json is volume-mounted at runtime; create the
# directory so the mount point exists in the image.
extraCommands = ''
mkdir -p etc/rs-surface var/lib/rs-surface mnt/topological-storage
'';
config = {
Entrypoint = [ "${rsSurface}/bin/rs-surface" ];
Env = [
"RS_SURFACE_PROFILE=/etc/rs-surface/node.json"
"RS_SURFACE_STATE=/var/lib/rs-surface"
"RS_SURFACE_MOUNT=/mnt/topological-storage"
"RS_SURFACE_HOST=0.0.0.0"
"RS_SURFACE_PORT=8080"
"SSL_CERT_FILE=${pkgs.cacert}/etc/ssl/certs/ca-bundle.crt"
];
ExposedPorts = { "8080/tcp" = {}; };
Healthcheck = {
Test = [ "CMD" "${pkgs.coreutils}/bin/sh" "-c"
"wget -qO- http://127.0.0.1:8080/health || exit 1" ];
Interval = 10000000000; # 10 s in nanoseconds
Timeout = 3000000000; # 3 s
StartPeriod = 3000000000; # 3 s
Retries = 3;
};
Labels = {
"org.opencontainers.image.description" = "rs-surface embedded node daemon";
"org.opencontainers.image.source" = "4-Infrastructure/infra/embedded_surface/rs-surface";
};
};
maxLayers = 10;
};
in rec {
packages.${system} = {
@ -303,9 +229,8 @@
maxLayers = 120;
};
# rs-surface binary and OCI image
rs-surface = rsSurface;
rs-surface-image = rsSurfaceImage;
# rs-surface removed — Garnix CI shut down; build with cargo directly:
# cd 4-Infrastructure/infra/embedded_surface/rs-surface && cargo build --release
};
# Convenience alias: `nix build .#devcontainer`

122
scripts/math-first/require_math_evidence.py Executable file
View file

@ -0,0 +1,122 @@
#!/usr/bin/env python3
"""Require math evidence (receipt or Lean change) alongside math-track edits.
This script enforces the math-first contract: if a commit or PR touches files
in a math-track surface, at least one evidence file must also be present.
Usage:
# CI mode: compare against a base ref
python3 scripts/math-first/require_math_evidence.py --from-git-diff origin/main
# Pre-commit mode: check staged files
python3 scripts/math-first/require_math_evidence.py --staged
Exits 0 if:
- No math-track files are present in the changeset, OR
- At least one evidence file is also in the changeset
Exits 1 if math-track files are present but no evidence file accompanies them.
"""
from __future__ import annotations
import argparse
import subprocess
import sys
from pathlib import Path
# Math-track surface prefixes: files under these paths require evidence
MATH_TRACK_PREFIXES = (
"0-Core-Formalism/lean/Semantics/",
"6-Documentation/docs/distilled/",
"shared-data/data/stack_solidification/",
)
# Evidence patterns: if any changed file matches, the requirement is satisfied
EVIDENCE_PREFIXES = (
"shared-data/artifacts/deepseek_review/",
"0-Core-Formalism/lean/Semantics/",
)
EVIDENCE_FILES = (
"claims.yaml",
)
def get_changed_files_git_diff(base_ref: str) -> list[str]:
"""Get changed files by diffing against a base ref."""
result = subprocess.run(
["git", "diff", "--name-only", base_ref + "...HEAD"],
capture_output=True, text=True, check=False,
)
if result.returncode != 0:
# Fall back to two-dot diff
result = subprocess.run(
["git", "diff", "--name-only", base_ref],
capture_output=True, text=True, check=True,
)
return [f for f in result.stdout.strip().split("\n") if f]
def get_changed_files_staged() -> list[str]:
"""Get staged files for pre-commit hook."""
result = subprocess.run(
["git", "diff", "--cached", "--name-only"],
capture_output=True, text=True, check=True,
)
return [f for f in result.stdout.strip().split("\n") if f]
def is_math_track(path: str) -> bool:
return any(path.startswith(p) for p in MATH_TRACK_PREFIXES)
def is_evidence(path: str) -> bool:
if any(path.startswith(p) for p in EVIDENCE_PREFIXES):
return True
if path in EVIDENCE_FILES:
return True
return False
def main() -> int:
parser = argparse.ArgumentParser(description=__doc__)
group = parser.add_mutually_exclusive_group(required=True)
group.add_argument("--from-git-diff", metavar="BASE_REF",
help="Compare HEAD against BASE_REF")
group.add_argument("--staged", action="store_true",
help="Check staged files (pre-commit mode)")
args = parser.parse_args()
if args.staged:
changed = get_changed_files_staged()
else:
changed = get_changed_files_git_diff(args.from_git_diff)
if not changed:
print("No changed files")
return 0
math_files = [f for f in changed if is_math_track(f)]
if not math_files:
print("No math-track files in changeset — skipping evidence check")
return 0
evidence_files = [f for f in changed if is_evidence(f)]
if evidence_files:
print(f"OK: {len(math_files)} math-track file(s) with "
f"{len(evidence_files)} evidence file(s)")
return 0
# Math-track files present but no evidence
print("FAIL: math-track files changed but no evidence accompanies them:")
for f in math_files:
print(f" - {f}")
print("\nPlease include at least one of:")
print(" - A DeepSeek review receipt under shared-data/artifacts/deepseek_review/")
print(" - A Lean source file under 0-Core-Formalism/lean/Semantics/")
print(" - An update to claims.yaml")
return 1
if __name__ == "__main__":
raise SystemExit(main())

115
scripts/math-first/test_require_math_evidence.py Executable file
View file

@ -0,0 +1,115 @@
#!/usr/bin/env python3
"""Self-tests for require_math_evidence.py.
Tests the classification logic (is_math_track, is_evidence) without needing
a live git repo. Exits 0 on success, 1 on failure.
"""
from __future__ import annotations
import importlib.util
import sys
from pathlib import Path
SCRIPT_DIR = Path(__file__).resolve().parent
def _load_module():
"""Import require_math_evidence as a module (it has dashes in the dir name)."""
spec = importlib.util.spec_from_file_location(
"require_math_evidence",
SCRIPT_DIR / "require_math_evidence.py",
)
mod = importlib.util.module_from_spec(spec)
spec.loader.exec_module(mod)
return mod
def test_math_track_classification() -> bool:
"""Verify is_math_track correctly identifies math-track paths."""
mod = _load_module()
positives = [
"0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean",
"6-Documentation/docs/distilled/ArithmeticSpec.md",
"shared-data/data/stack_solidification/receipt.md",
]
negatives = [
"4-Infrastructure/shim/some_script.py",
"scripts/math-first/validate_deepseek_receipts.py",
"README.md",
"flake.nix",
]
ok = True
for p in positives:
if not mod.is_math_track(p):
print(f"FAIL: {p} should be math-track but is not")
ok = False
for p in negatives:
if mod.is_math_track(p):
print(f"FAIL: {p} should NOT be math-track but is")
ok = False
if ok:
print("PASS: math-track classification")
return ok
def test_evidence_classification() -> bool:
"""Verify is_evidence correctly identifies evidence paths."""
mod = _load_module()
positives = [
"shared-data/artifacts/deepseek_review/foo.receipt.json",
"0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean",
"claims.yaml",
]
negatives = [
"4-Infrastructure/shim/some_script.py",
"README.md",
]
ok = True
for p in positives:
if not mod.is_evidence(p):
print(f"FAIL: {p} should be evidence but is not")
ok = False
for p in negatives:
if mod.is_evidence(p):
print(f"FAIL: {p} should NOT be evidence but is")
ok = False
if ok:
print("PASS: evidence classification")
return ok
def test_lean_file_is_self_evidence() -> bool:
"""A Lean file IS its own evidence (under the evidence prefix)."""
mod = _load_module()
lean = "0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean"
if not mod.is_math_track(lean):
print("FAIL: Lean file not detected as math-track")
return False
if not mod.is_evidence(lean):
print("FAIL: Lean file not detected as evidence")
return False
print("PASS: Lean file is both math-track and evidence (self-evidencing)")
return True
def main() -> int:
tests = [
test_math_track_classification,
test_evidence_classification,
test_lean_file_is_self_evidence,
]
passed = sum(1 for t in tests if t())
total = len(tests)
print(f"\n{passed}/{total} tests passed")
return 0 if passed == total else 1
if __name__ == "__main__":
raise SystemExit(main())

126
scripts/math-first/test_validate_deepseek_receipts.py Executable file
View file

@ -0,0 +1,126 @@
#!/usr/bin/env python3
"""Self-tests for validate_deepseek_receipts.py.
Runs minimal smoke tests to verify the validator works against the live
schema and any existing receipts. Exits 0 on success, 1 on failure.
"""
from __future__ import annotations
import json
import sys
import tempfile
from pathlib import Path
# Ensure we can import the validator's logic
SCRIPT_DIR = Path(__file__).resolve().parent
REPO_ROOT = SCRIPT_DIR.parents[1]
SCHEMA_PATH = REPO_ROOT / "shared-data" / "schemas" / "deepseek-review-receipt.schema.json"
try:
from jsonschema import Draft202012Validator, ValidationError
except ImportError:
print("SKIP: jsonschema not installed")
sys.exit(0)
def test_schema_compiles() -> bool:
"""The schema itself must be valid JSON Schema."""
if not SCHEMA_PATH.exists():
print("SKIP: schema file not found")
return True
schema = json.loads(SCHEMA_PATH.read_text())
Draft202012Validator.check_schema(schema)
print("PASS: schema compiles")
return True
def test_valid_receipt_accepted() -> bool:
"""A minimal valid primary receipt must pass validation."""
if not SCHEMA_PATH.exists():
print("SKIP: schema file not found")
return True
schema = json.loads(SCHEMA_PATH.read_text())
validator = Draft202012Validator(schema)
valid_receipt = {
"schema": "ollama_deepseek_review_receipt_v1",
"created_at": "2026-01-01T00:00:00+00:00",
"model": "deepseek-v3.2",
"endpoint": "https://ollama.com/v1/chat/completions",
"prompt_sha256": "sha256:" + "a" * 64,
"answer_sha256": "sha256:" + "b" * 64,
"usage": {"prompt_tokens": 100, "completion_tokens": 200, "total_tokens": 300},
"context_files": ["some/file.lean"],
"answer_path": "shared-data/artifacts/deepseek_review/test.md",
}
errors = list(validator.iter_errors(valid_receipt))
if errors:
print("FAIL: valid receipt rejected:")
for err in errors:
print(f" {err.message}")
return False
print("PASS: valid receipt accepted")
return True
def test_invalid_receipt_rejected() -> bool:
"""A receipt missing required fields must be rejected."""
if not SCHEMA_PATH.exists():
print("SKIP: schema file not found")
return True
schema = json.loads(SCHEMA_PATH.read_text())
validator = Draft202012Validator(schema)
invalid_receipt = {"schema": "ollama_deepseek_review_receipt_v1"}
errors = list(validator.iter_errors(invalid_receipt))
if not errors:
print("FAIL: invalid receipt was accepted")
return False
print("PASS: invalid receipt rejected")
return True
def test_bad_sha256_rejected() -> bool:
"""A receipt with malformed SHA-256 must be rejected."""
if not SCHEMA_PATH.exists():
print("SKIP: schema file not found")
return True
schema = json.loads(SCHEMA_PATH.read_text())
validator = Draft202012Validator(schema)
receipt = {
"schema": "ollama_deepseek_review_receipt_v1",
"created_at": "2026-01-01T00:00:00+00:00",
"model": "deepseek-v3.2",
"endpoint": "https://ollama.com/v1/chat/completions",
"prompt_sha256": "not-a-hash",
"answer_sha256": "sha256:" + "b" * 64,
"usage": {"prompt_tokens": 100, "completion_tokens": 200, "total_tokens": 300},
"context_files": ["some/file.lean"],
"answer_path": "shared-data/artifacts/deepseek_review/test.md",
}
errors = list(validator.iter_errors(receipt))
if not errors:
print("FAIL: bad SHA-256 was accepted")
return False
print("PASS: bad SHA-256 rejected")
return True
def main() -> int:
tests = [
test_schema_compiles,
test_valid_receipt_accepted,
test_invalid_receipt_rejected,
test_bad_sha256_rejected,
]
passed = sum(1 for t in tests if t())
total = len(tests)
print(f"\n{passed}/{total} tests passed")
return 0 if passed == total else 1
if __name__ == "__main__":
raise SystemExit(main())

100
scripts/math-first/validate_claims_registry.py Executable file
View file

@ -0,0 +1,100 @@
#!/usr/bin/env python3
"""Validate claims.yaml against its JSON Schema and check referenced paths.
Usage (CI or local):
python3 scripts/math-first/validate_claims_registry.py
Validates:
1. claims.yaml parses as valid YAML
2. Contents match shared-data/schemas/claims-registry.schema.json
3. Every repo-relative path referenced in claims.yaml actually exists on disk
Exits 0 on success, 1 on any failure.
"""
from __future__ import annotations
import json
import sys
from pathlib import Path
try:
import yaml
except ImportError:
print("SKIP: PyYAML not installed (pip install PyYAML)")
sys.exit(0)
try:
from jsonschema import Draft202012Validator
except ImportError:
print("SKIP: jsonschema not installed (pip install 'jsonschema>=4.21')")
sys.exit(0)
REPO_ROOT = Path(__file__).resolve().parents[2]
CLAIMS_PATH = REPO_ROOT / "claims.yaml"
SCHEMA_PATH = REPO_ROOT / "shared-data" / "schemas" / "claims-registry.schema.json"
def main() -> int:
if not CLAIMS_PATH.exists():
print("SKIP: claims.yaml not found")
return 0
if not SCHEMA_PATH.exists():
print(f"SKIP: schema not found at {SCHEMA_PATH}")
return 0
# Parse YAML
try:
data = yaml.safe_load(CLAIMS_PATH.read_text())
except yaml.YAMLError as exc:
print(f"FAIL: claims.yaml is not valid YAML — {exc}")
return 1
# Validate against schema
schema = json.loads(SCHEMA_PATH.read_text())
validator = Draft202012Validator(schema)
errors = list(validator.iter_errors(data))
if errors:
print("FAIL: claims.yaml schema validation errors:")
for err in errors:
print(f" {err.json_path}: {err.message}")
return 1
print("OK claims.yaml matches schema")
# Check referenced paths exist
missing = 0
claims = data.get("claims", [])
for claim in claims:
cid = claim.get("id", "<unknown>")
# Check lean path
lean_path = claim.get("lean")
if lean_path and not (REPO_ROOT / lean_path).exists():
print(f"WARN {cid}: lean path does not exist — {lean_path}")
# Warn only; the file might be in a different branch
# Check review receipt paths
for rpath in claim.get("review_receipts", []):
if not (REPO_ROOT / rpath).exists():
print(f"FAIL {cid}: receipt not found — {rpath}")
missing += 1
# Check source paths (skip external citations)
for spath in claim.get("sources", []):
if spath.startswith("http://") or spath.startswith("https://"):
continue
if not (REPO_ROOT / spath).exists():
print(f"WARN {cid}: source not found — {spath}")
if missing:
print(f"\n{missing} referenced receipt(s) not found on disk", file=sys.stderr)
return 1
print(f"\n{len(claims)} claim(s) validated OK")
return 0
if __name__ == "__main__":
raise SystemExit(main())

69
scripts/math-first/validate_deepseek_receipts.py Executable file
View file

@ -0,0 +1,69 @@
#!/usr/bin/env python3
"""Validate every tracked DeepSeek review receipt against its JSON Schema.
Usage (CI or local):
python3 scripts/math-first/validate_deepseek_receipts.py
Exits 0 if every receipt under shared-data/artifacts/deepseek_review/
matches shared-data/schemas/deepseek-review-receipt.schema.json, or if
no receipts exist yet. Exits 1 on any validation failure.
"""
from __future__ import annotations
import json
import sys
from pathlib import Path
try:
from jsonschema import Draft202012Validator
except ImportError:
print("SKIP: jsonschema not installed (pip install 'jsonschema>=4.21')")
sys.exit(0)
REPO_ROOT = Path(__file__).resolve().parents[2]
SCHEMA_PATH = REPO_ROOT / "shared-data" / "schemas" / "deepseek-review-receipt.schema.json"
RECEIPTS_DIR = REPO_ROOT / "shared-data" / "artifacts" / "deepseek_review"
def main() -> int:
if not SCHEMA_PATH.exists():
print(f"SKIP: schema not found at {SCHEMA_PATH}")
return 0
schema = json.loads(SCHEMA_PATH.read_text())
validator = Draft202012Validator(schema)
receipts = sorted(RECEIPTS_DIR.glob("*.receipt.json")) if RECEIPTS_DIR.exists() else []
if not receipts:
print("No receipts to validate")
return 0
failures = 0
for path in receipts:
try:
data = json.loads(path.read_text())
except json.JSONDecodeError as exc:
print(f"FAIL {path.relative_to(REPO_ROOT)}: invalid JSON — {exc}")
failures += 1
continue
errors = list(validator.iter_errors(data))
if errors:
print(f"FAIL {path.relative_to(REPO_ROOT)}:")
for err in errors:
print(f" {err.json_path}: {err.message}")
failures += 1
else:
print(f"OK {path.relative_to(REPO_ROOT)}")
if failures:
print(f"\n{failures} receipt(s) failed validation", file=sys.stderr)
return 1
print(f"\n{len(receipts)} receipt(s) validated OK")
return 0
if __name__ == "__main__":
raise SystemExit(main())