Strilight (v0.2.0)

Высокопроизводительный движок алгебраического подъёма циклов и точных рациональных рекуррентных вычислений для Python и C

---

Обзор: зачем перебирать, если можно решить?

Традиционные компиляторы, среды выполнения и JIT-движки (такие как GCC, Clang, PyPy или Numba) рассматривают циклы как повторяющиеся последовательности управляющего потока, выполняя инструкции шаг за шагом:

$$ \text{Runtime Cost} = \mathcal{O}(N) $$

Когда $N = 10^6$ или $10^9$, последовательное выполнение требует миллиардов циклов процессора. Strilight принципиально перестраивает выполнение циклов с помощью символического алгебраического подъёма:

1. Формулировка перехода состояний: он статически анализирует тело цикла и формулирует его матрицу математического перехода состояний:

$$ \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}} $$

2. Решение в замкнутой форме: он решает рекуррентную систему в замкнутой форме, сокращая время выполнения с $\mathcal{O}(N)$ до $\mathcal{O}(1)$ (для скалярных/периодических/телескопических рядов) или $\mathcal{O}(\log N)$ (посредством быстрого бинарного возведения матрицы в степень).

---

Философия дизайна: удобство разработчика прежде всего

Strilight не претендует на внедрение эзотерической магии; по сути это инструмент для удобства разработчика.

В физическом моделировании, научных вычислениях и численном моделировании инженеры часто сталкиваются с досадной дилеммой:

• Читаемый код: естественные, выразительные уравнения, отражающие физику из учебника, но выполняющиеся медленно при миллионах итераций.
• Вручную оптимизированный код: запутанные, вручную развёрнутые циклы и неочевидные арифметические трюки, которые работают быстро, но хрупки, трудны в отладке и скрывают лежащую в основе физику.

Strilight разрешает эту дилемму. Вы записываете физическую или математическую концепцию в любом удобном для вас простом, естественном синтаксисе. Strilight анализирует структуру вашего цикла, выводит точные рекуррентные формулы в замкнутой форме и ускоряет выполнение за кулисами — сохраняя полную читаемость и простоту вашей кодовой базы.

---

Архитектурные основы

1. Точная рациональная арифметика над $\mathbb{Q}$ (нулевая потеря точности)

Арифметика с плавающей запятой вносит накапливающиеся ошибки усечения ($1/3 \times 3 \approx 0.9999999999999999$). Strilight выполняет аффинную индукцию и анализ шага над полем рациональных чисел $\mathbb{Q}$:

• Множители и смещения моделируются как канонические дроби ($\frac{p}{q}$).
• Генерирует ядра двойной точности на C и точные представления Fraction в Python, гарантируя 100% побитово точное математическое соответствие.

2. Многопеременные связанные рекуррентные системы ($\mathcal{O}(\log N)$)

Переменные, взаимно зависящие друг от друга (например, физические симуляции, где положение зависит от скорости, а скорость зависит от ускорения), автоматически извлекаются в матрицу связей переменных ($\mathbf{A}$). Strilight выполняет бинарное возведение в степень над $\mathbf{A}$, выполняя миллионы итераций менее чем за 2 наносекунды.

3. Прозрачный декоратор @accelerate (как это работает)

Декорирование любой стандартной функции Python с помощью @accelerate запускает автоматизированный конвейер во время определения функции (без накладных расходов на анализ при каждом вызове):

1. Извлечение AST: анализирует AST функции, выявляет конструкции циклов for и извлекает индукционные переменные.
2. Синтез в замкнутой форме: преобразует цикл в эквивалентные рекуррентные модели в замкнутой форме или ядра бинарного матричного возведения в степень.
3. Встраивание на месте: заменяет узлы AST цикла на месте, компилирует вызываемый объект в память и внедряет глобальные переменные времени выполнения (Fraction, math), не загрязняя пространства имён модуля.
4. Отражение контракта: прикрепляет _loop_summary и _invariant_contract к скомпилированному объекту функции, позволяя последующим компиляторам и инструментам верификации исследовать базовую матрицу переходов $\mathbf{A}$.
5. Корректный откат: при обнаружении нелинейной индексации или неподдерживаемых динамических вызовов Strilight выдаёт диагностическое предупреждение и корректно возвращается к нативному выполнению без сбоев.

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)

4. Управляемые контрактом директивы исходного кода C (#pragma strilight)

В отличие от динамической рефлексии Python, преобразования кода C в Strilight строго следуют явной модели разработчика-контракта через прагма-директивы в стиле OpenMP. Движок никогда не изменяет исходный код C неявно; преобразования происходят исключительно при наличии явных контрактных клауз разработчика (contract, target, include, model):

• #pragma strilight accelerate: Явно разрешает Strilight поднять аннотированный цикл for на C в эквивалентное математическое выражение в замкнутой форме.
• #pragma strilight fuse: Явная директива разработчика, предписывающая Strilight объединить указанные смежные циклы с идентичными доменами итерации в единое ядро бинарной матричной рекуррентности $\mathcal{O}(\log N)$.

// 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;
}

5. Разрешение символов и констант между файлами (CrossFileResolver)

Численные симуляции часто определяют параметры в отдельных заголовочных файлах или конфигурационных модулях. CrossFileResolver в Strilight:

• Статически отслеживает импорты локальных модулей и директивы C #include / #define.
• Вычисляет литеральные константные выражения (например, SOLAR_MASS = 4 * PI * PI) между файлами посредством вычисления AST без выполнения произвольного кода во время выполнения и без использования небезопасного eval.

6. Индукция срезов массивов и циклические табличные поиски

• Циклический табличный поиск: Преобразует циклические табличные поиски (table[i % P]) в предвычисленные замкнутые формулы префиксных сумм за $\mathcal{O}(1)$.
• Мутация срезов массивов на месте: Классифицирует константные заполнения и арифметические прогрессии, синтезируя оптимальные аппаратные вызовы memset или векторные присваивания срезов (arr[:N] = ...).