mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-08-13 13:40:34 +00:00
feat(lean): add PolyFactorIdentity — short-sleeve polynomial detection for RRC
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. Architecture: - limbDecompose: convert integers to base-B polynomial coefficients (models the zerocopy boundary where raw limbs are already exposed) - shortSleeveDetected: cheap sparsity check flags structured integers - polySignature: full structural features when flagged (degree, GCD, energy, sparsity, term count) - polyDecomposabilityScore: Q16_16 score for RRC feature integration - zeroCopyScan: batch scanner for hardware DMA boundaries - E8Sidon integration: sigma3/sigma7/convolution polynomial signatures 3 sorries (all with TODO(lean-port) + proof sketches): - limbDecompose_polyEval_roundtrip (base-B representation theorem) - zeroLimbs_bound_terms (filter complement partition) - shortSleeve_mono_zero_prepend (sparsity monotonicity) Build: passes (Semantics.RRC.PolyFactorIdentity target, 0 errors) Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
This commit is contained in:
Devin AI
parent
5371c70229
commit
b5319c7d98
1 changed files with 387 additions and 0 deletions
|
|
@ -0,0 +1,387 @@
|
|||
/-
|
||||
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
|
||||
open Semantics.E8Sidon
|
||||
|
||||
-- ═══════════════════════════════════════════════════════════════════════════════
|
||||
-- §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
|
||||
Loading…
Add table
Reference in a new issue