Lightweight, Modular Verification for WebAssembly-to-Native Instruction Selection

The paper "Lightweight, Modular Verification for WebAssembly-to-Native Instruction Selection" addresses the problem of verifying the correctness of the compilation phase in which high-level intermediate representation (IR) instructions are transformed into a set of instructions that specific hardware can execute. This stage—known as instruction selection—is one of the most complex and error-prone parts of a compiler because it must bridge the significant gap between the abstract logic of a program and the details of a processor’s instruction set.

The main contribution of the work is the development of a system called Crocus. The key features and achievements of Crocus can be summarized as follows:

- Modularity and Ease of Integration. Crocus is designed so that compiler developers only need to add special annotations next to the lowering rules written in the domain-specific language (DSL) ISLE. These annotations describe the semantics of individual constructs at a high level, making it easier to maintain and update the rules as the compiler evolves.

- Automated Verification Using SMT Solvers. The system translates the annotated rules into logical formulas that are then verified using an SMT (Satisfiability Modulo Theories) solver. This process guarantees that each transformation from IR to machine code preserves the original semantics—meaning that the final machine code accurately reflects the intended behavior of the source program.

- Enhanced Reliability and Security. Since WebAssembly is frequently used to execute code from untrusted sources (for example, in web browsers or distributed cloud services), errors during instruction selection can lead to serious vulnerabilities, such as sandbox escapes. Crocus helps detect both previously known and new errors in the lowering rules, thereby reducing the risk of security breaches.

- Practical Application in Production Compilers. Crocus has been tested on the real-world compiler Cranelift, which is used in engines like Wasmtime, a popular WebAssembly runtime. The system not only reproduced previously discovered bugs but also identified new issues that had gone unnoticed, demonstrating its practical value in a production setting.

In summary, the paper demonstrates how modern formal verification methods based on SMT solvers can be effectively integrated into existing compilers to automatically check complex code transformations. This approach not only improves the reliability of the generated machine code but also significantly lowers the risk of vulnerabilities in systems running WebAssembly.

🔗dl.acm.org/doi/10.1145/3617232.3624862 #wasm

The Topology and Combinatorics of Soccer Balls
by Dieter Kotschick

When mathematicians think about soccer balls, the number of possible designs quickly multiplies

🔗 arxiv.org/pdf/math/0606193

🔗 americanscientist.org/article/the-topology-and-combinatorics-of-soccer-balls #math

3️⃣ Еженедельный войс каждую Пятницу
Пройдёт в Web3 Voice 4 Апреля в 17:00 CET

👤 Специальный гость:
Skuli Dropek — Software Engineer

📌 Воркшоп по Cursor:
• Знакомство с Cursor — что это, и как меняет подход к разработке
• Практика — ключевые функции, настройка под задачи
• Ответы на вопросы — разбор ошибок, советы по использованию

#cursor #ai #w3voice

JamLearn — 3D Game Engine — Day 2

В основе этого JamLearn совместная практика написания 3D Game Engine на C++ с нуля изучив курс линейной алгебры и матриц

🎓 На прошлой сессии мы разобрались с C++ & CMake, настройка среды CLion/VS Code, изучили C++ за 20 минут 😼 (типы данных и функции, стандартные контейнеры, ООП, перегрузка операторов), познакомились с вектором, линейные комбинации и базис, линейные преобразования, масштабирование, повороты, векторное произведение, еще был бонусный воркшоп по Cursor

Что же нас ждет сегодня 🤔

#math #jamlearn #day2

JamLearn — 3D Game Engine — Day 3

В основе этого JamLearn совместная практика написания 3D Game Engine на C++ с нуля изучив курс линейной алгебры и матриц

🎓 На прошлой сессии мы разобрались с определением матрицы, операциями с матрицами, 📝 порешали матрицы и рассмотрели матрицу как линейное преобразование

⭐️План рассмотреть и понять что успеем и сможем и этого набора тем: Как устроен 3D движок, Реализация классов Вектор и Матрица, Как устроена 3D графика, Проекция 3D фигур на плоскости, Матрица проекции, Матрица экранного пространства, Мировая система координат, Матрицы вращения, перемещения, масштабирования, Реализация 3D графики

🔔17 апреля 18:00 CET

#math #jamlearn #day3

JamLearn — 3D Game Engine — Day 4

В основе этого JamLearn совместная практика написания 3D Game Engine на C++ с нуля изучив курс линейной алгебры и матриц

🎓 На прошлой сессии мы рассмотрели как устроен 3D движок и реализовали классы Вектор и Матрица

⭐️План рассмотреть и понять что успеем и сможем и этого набора тем: Решить задачи с матрицами, Визуализация кватернионов (четырехмерных чисел), Как устроена 3D графика, Проекция 3D фигур на плоскости, Матрица проекции, Матрица экранного пространства, Мировая система координат, Матрицы вращения, перемещения, масштабирования, Реализация 3D графики

🔔18 апреля 18:00 CET уже началось

#math #jamlearn #day4

JamLearn — Tact Smart Battle

В основе этого JamLearn совместная практика прохождения курсов, CTF, etc

🎓 На прошлой сессии мы решали матрицы, познакомились с визуализацией кватернионов (четырехмерных чисел), рассмотрели устройство 3D графики, проекцию 3D фигур на плоскости, различные виды матриц (проекции, экранного пространства, вращения, перемещения, масштабирования), мировую систему координат, домашние задание: Реализация 3D графики

⭐️Продолжить разбираться в понедельник с вектором, матрицей, линейными преобразованиями и реализацией 3D графики в понедельник, также надеюсь, что будет что обсудить после проделанной самостоятельной работы с домашним заданием будем смотреть 🧠 Tact Smart Battle

#ctf #jamlearn

Криптография 101 с Альфредом Менезесом
🎓 Kyber (ML-KEM) и Dilithium (ML-DSA) — квантово-безопасные схемы инкапсуляции и подписи ключей на основе решеток, которые недавно были стандартизированы Национальным институтом стандартов и технологий (NIST)

📁 Квантово-устойчивая схема пороговой подписи на решётках, которая поддерживает до 1024 участников и не требует тяжёлых криптографических инструментов
🐱 Скрипты оценки безопасности для Kyber и Dilithium

#cryptography #dilithium #kyber #quantum

JamLearn — 3D Game Engine — Day 5

В основе этого JamLearn совместная практика написания 3D Game Engine на C++ с нуля изучив курс линейной алгебры и матриц

🎓 На прошлой сессии мы решали задачи с матрицами, Визуализация кватернионов (четырехмерных чисел), разбирались как устроена 3D графика, проекция 3D фигур на плоскости, матрица проекции, матрица экранного пространства, мировая система координат, матрицы вращения, перемещения, масштабирования, домашние задание: реализация 3D графики

🗓 25 мая 18:00 CET добавить в календарь 🔔 videochat

⭐️План продолжить разбираться с вектором, матрицей, линейными преобразованиями и реализацией 3D графики, также надеюсь, что будет что обсудить после проделанной самостоятельной работы с домашним заданием

💼 Домашние задание
jam-game-engine/lesson2.cpp

int main() {
    /*
     * TODO: реализуйте преобразования объектов и проекции треугольников на экран
     * На этом уроке вам необходимо работать со следующими файлами:
     *
     * engine/Object.cpp
     * engine/linalg/Matrix4x4.cpp
     * engine/Camera.cpp
     *
     * Если вы всё сделали правильно, то на экране появится вращающийся куб
     */
    Lesson2 l;
    l.create();
}

🏠 Backlog
- https://github.com/BoringStudio/tron
- https://github.com/bwasty/learn-opengl-rs

#math #jamlearn #gamedev #day5

Day 5 — 3D Game Engine — JamLearn

В основе этого JamLearn совместная практика написания 3D Game Engine на C++ с нуля изучив курс линейной алгебры и матриц

🎓 В этой сессии мы разбирались применением векторов и реализацией 3D графики, также обсудили проделанную самостоятельно работы с домашним заданием

💼 Домашние задание
jam-game-engine/lesson3.cpp

int main() {
  /*
  * TODO: реализуйте загрузку .obj файлов, простое освещение и алгоритм художника
  * На этом уроке вам необходимо работать со следующими файлами:
  *
  * engine/utils/ResourceManager.cpp
  * engine/Camera.cpp
  *
  * Если вы всё сделали правильно, то на экране должна появится вращающаяся обезьянка
  */

  Lesson3 l;
  l.create();
}

расписание может меняться, добавьте событие в календарь, чтобы быть в курсе 🔔
🗓 3D Game Engine — JamLearn

#math #jamlearn #day5 #gamedev

Карьера в arXiv

Cornell Tech: Мы ищем разработчика программного обеспечения с опытом работы в Cloud DevOps, который возглавит процесс модернизации нашей системы DevOps, чтобы мы могли эффективно, надежно и безопасно развертывать новый код, используя принципы Infrastructure as Code, эта задача, скорее всего, будет включать в себя значительную часть автоматизации с помощью gitops, а также инструментов Google Cloud Platform, руководитель DevOps также развернет надежный конвейер CI/CD

- Вы уже должны иметь законное право работать в США
- arXiv находится в кампусе Cornell Tech на острове Рузвельта в Нью-Йорке, при найме предпочтение отдается кандидатам, которые могут работать в этом месте, но гибридная и/или удаленная работа может быть вариантом

🔗 info.arxiv.org/hiring/

#career #arXiv #cornell

Day 7 — 3D Game Engine — JamLearn

В основе этого JamLearn совместная практика написания 3D Game Engine на C++ с нуля изучив курс линейной алгебры и матриц и не только, а еще магию разработки

🎓 В этой сессии мы отвечали на вопросы по пройденному материалу, обсуждали возможности 3D-движка, применимость тестов в разработке и частности Property testing, а также сериализацию данных с использованием TL-B

💼 Домашние задания
- jam-game-engine/lesson3.cpp
- jam-game-engine/lesson4.cpp

расписание может меняться, добавьте событие в календарь, чтобы быть в курсе 🔔
🗓 3D Game Engine — JamLearn 🎓

#math #jamlearn #day7 #gamedev #ton #tlb

📁 Tutorial collect contract gas metric #ton #sandbox