
Lifts x86-64 binary loops into closed-form SMT constraints via strided interval analysis, enabling O(1) symbolic execution and crackme key recovery.
High-Performance Algebraic Loop Lifting & Exact Rational Recurrence Engine for Python and C
Traditional compilers, runtimes, and JIT engines (such as GCC, Clang, PyPy, or Numba) treat loops as repetitive control-flow sequences, executing instructions step-by-step:
$$ \text{Runtime Cost} = \mathcal{O}(N) $$
When $N = 10^6$ or $10^9$, sequential execution incurs billions of CPU cycles. Strilight fundamentally re-engineers loop execution through Symbolic Algebraic Lifting:
$$ \vec{\mathbf{X}}(N) = \mathbf{A}^N \cdot \vec{\mathbf{X}}0 + \sum{k=0}^{N-1} \mathbf{A}^{N-1-k} \vec{\mathbf{B}} $$
Strilight does not pretend to introduce esoteric magic; it is fundamentally a developer quality-of-life tool.
In physical modeling, scientific computing, and numerical simulation, engineers frequently face a frustrating dilemma:
Strilight resolves this dilemma. You write the physical or mathematical concept in whatever straightforward, natural syntax you prefer. Strilight inspects your loop structure, derives the exact closed-form recurrence formulas, and accelerates execution behind the scenes—preserving complete readability and simplicity in your codebase.
Floating-point arithmetic introduces cumulative truncation errors ($1/3 \times 3 \approx 0.9999999999999999$). Strilight performs affine induction and stride analysis over the field of rational numbers $\mathbb{Q}$:
Fraction representations in Python, guaranteeing 100% bit-exact mathematical parity.Variables that mutually depend on each other (e.g., physical simulations where position depends on velocity and velocity depends on acceleration) are automatically extracted into a Variable Coupling Matrix ($\mathbf{A}$). Strilight performs binary exponentiation on $\mathbf{A}$, executing millions of iterations in under 2 nanoseconds.
@accelerate Decorator (How It Works)Decorating any standard Python function with @accelerate executes an automated pipeline at function definition time (zero per-call runtime analysis overhead):
for loop constructs, and extracts induction variables.Fraction, math) without polluting module namespaces._loop_summary and _invariant_contract to the compiled function object, enabling downstream compilers and verification tools to inspect the underlying transition matrix $\mathbf{A}$.from strilight import accelerate
@accelerate
def compute_simulation(steps: int) -> int:
acc = 0
for i in range(steps):
acc += (i * 3) + 7
return acc
# Executes in O(1) time (~0.001 ms even if steps = 100,000,000)
result = compute_simulation(100_000_000)
#pragma strilight)Unlike Python's dynamic reflection, C code transformations in Strilight strictly follow an explicit Developer-Contract Model via OpenMP-style pragma directives. The engine never mutates C source code implicitly; transformations occur solely when directed by explicit developer contract clauses (contract, target, include, model):
#pragma strilight accelerate: Explicitly authorizes Strilight to lift the annotated C for loop into an equivalent closed-form mathematical expression.#pragma strilight fuse: Explicit developer directive instructing Strilight to fuse designated adjacent loops sharing identical iteration domains into a unified $\mathcal{O}(\log N)$ binary matrix recurrence kernel.// Example of contract-guided multi-loop fusion via developer directive
int simulate_motion(int n) {
int pos = 0, vel = 10;
#pragma strilight fuse
for (int i = 0; i < n; i++) {
pos += vel;
}
for (int i = 0; i < n; i++) {
vel += 2;
}
return pos;
}
CrossFileResolver)Numerical simulations frequently define parameters in separate header files or configuration modules. Strilight's CrossFileResolver:
#include / #define directives.SOLAR_MASS = 4 * PI * PI) across files via AST evaluation without executing arbitrary runtime code or using unsafe eval.table[i % P]) into precomputed prefix-sum closed formulas in $\mathcal{O}(1)$.memset calls or vector slice assignments (arr[:N] = ...).In mechanical and astrophysical simulations (e.g., $N$-body systems, orbital mechanics, particle kinematics), physical bodies frequently spend extensive periods traversing smooth, unperturbed trajectories without abrupt collisions or directional changes:
@accelerate decorator; in C, it is a standard #pragma. You can add or remove it at any time without altering your algorithm or business logic.Modern AI coding assistants (such as Claude, Gemini, GPT, or Jules) excel when operating over algebraic formulas and closed-form equations. Strilight makes it straightforward for developers and AI agents to inspect the synthesized code and mathematical contracts directly:
from strilight import accelerate
@accelerate
def compute_energy(steps: int) -> int:
total = 0
for i in range(steps):
total += 15
return total
# Execute once to trigger definition-time synthesis
result = compute_energy(100)
# Inspect the underlying mathematical contract:
summary = compute_energy._loop_summary
print("Extracted Induction Formulas:", summary.to_induction_formulas())
print("Invariant Contract:", compute_energy._invariant_contract.to_dict())
You can pass C source code directly to accelerate_c_source to generate inspectable, human-readable accelerated C kernels:
import strilight as sl
c_source = """
long long simulate(void) {
long long total = 0;
#pragma strilight accelerate target(total)
for (int i = 0; i < 1000000; i++) {
total += 42;
}
return total;
}
"""
accelerated_c = sl.accelerate_c_source(c_source)
print(accelerated_c)
# Emits: total += (42LL * 1000000);
We believe in engineering transparency:
target, include, model) provides deterministic transformation guarantees.Evaluated across high-iteration numerical loops, comparing native execution against Strilight acceleration:
| Benchmark Scenario | Iterations ($N$) | Native Baseline | Strilight Accelerated | Measured Speedup | Precision Fidelity |
|---|---|---|---|---|---|
| Coupled 4x4 Linear System (Python) | $1,000,000$ | $75.2\text{ ms}$ | $0.0002\text{ ms}$ | $376,000\times$ | 100% Bit-Exact |
| Coupled 4x4 Linear System (GCC -O2) | $1,000,000$ | $1.1\text{ ms}$ | $0.00002\text{ ms}$ | $55,000\times$ | 100% Bit-Exact |
| Cyclic Array Lookup Summation | $1,000,000$ | $74.8\text{ ms}$ | $0.0044\text{ ms}$ | $17,000\times$ | 100% Bit-Exact |
| Planetary N-Body Celestial Mechanics | $100,000$ | $7.17\text{ ms}$ | $0.051\text{ ms}$ | $140\times$ | Analytical Orbit Parity |
flowchart TD
SRC["Source Code (Python / C)"] --> LIFTER["SourceLifter: AST & Pragma Parser"]
LIFTER --> RESOLV["CrossFileResolver: Static Import Resolution"]
RESOLV --> VSA["Algebraic Induction Engine: models.py"]
VSA --> MATRIX["VariableCouplingMatrix: System Transition Matrix A"]
VSA --> QFIELD["Exact Rational Domain over Q: AffineExpr"]
REDUCE --> CODEGEN["CodeGenerator: C / Python Synthesis"]
VSA --> REDUCE["Schur Reduction & Block-Diagonal Decomposition"]
CODEGEN --> OUT["O(1) / O(log N) Executable Kernel"]Strilight addresses computational bottlenecks across scientific, engineering, and financial domains:
LoopInvariantContract) without memory-intensive loop unrolling.pip install strilight
git clone https://github.com/asama7706r-ui/strilight.git
cd strilight
pip install -e .
Execute the test suite and reproducible benchmarks:
# Run the 60-test unit and induction verification suite:
pytest
# Python recurrence acceleration:
python examples/01_python_recurrence_acceleration.py
# Jovian planetary N-body celestial simulation benchmark:
python examples/02_nbody_simulation_benchmark.py
# Coupled 4x4 linear matrix recurrence benchmark (O(N) -> O(log N) -> O(1)):
python examples/03_coupled_matrix_benchmark.py
# C Developer Contract & pragma acceleration suite:
python examples/c/run_c_acceleration.py
The core mathematical engine of Strilight is 100% open source under the GNU GPLv3 license.
We warmly welcome contributions from the global compiler, scientific computing, and performance engineering communities:
If you are interested in contributing, feel free to open an issue or submit a pull request on GitHub!
Strilight is released under a Dual-Licensing Model:
Contact: [email protected]