# Solar - ядро

1. "Holes" in Rosette. Розетта предоставляет возможность составить программу из "заглушек", где каждая заглушка - список методов которые можно поставить на это место.
Подробнее здесь: https://docs.racket-lang.org/rosette-guide/sec_rosette-libs.html#%28def._%28%28lib._rosette%2Flib%2Fangelic..rkt%29._choose%2A%29%29
2. Hoisting - вместо генерации "программы из закглушек", мы перебираем все $N^k$ возможных программ, и решаем запрос для каждой из них. Т.к. они независимые, мы можем распараллелить перебор
3. Дополнительная обработка if не требуется - rosette самостоятельно обрабатывает их для символьных выражений
4. Соляру требуется несколько частей:
1) Описание инструкций байткода
2) Машина-интерпретатор инструкций
3) Генератор суммаризации (? не работает)
4) Машина-интерпретатор суммаризаций
5) Солвер
5. Интерпретатор solidity можно заменить на интерпретаторы других языков программирования, для генерации эксплойтов для программ написанных на этих языках