CompressibleEuler - GitLite

KO | EN

gitlite — search

#chatgpt #java #generative-ai #nextjs #containers #android #artificial-intelligence #react-native #reactjs #shell

CompressibleEuler

(★ 12)

End-to-end formally verified solvers for the isothermal Euler and full compressible Euler equations in 1D, 2D, and 3D.

File Explorer

ZIP Download

- compressible_euler_1d.c
- compressible_euler_2d.c
- compressible_euler_3d.c
- isothermal_euler_1d.c
- isothermal_euler_2d.c
- isothermal_euler_3d.c
- compressible_euler_1d.lean
- compressible_euler_2d.lean
- compressible_euler_3d.lean
- isothermal_euler_1d.lean
- isothermal_euler_2d.lean
- isothermal_euler_3d.lean
- compressible_euler_1d.mov
- compressible_euler_2d.mov
- compressible_euler_3d.mov
- isothermal_euler_1d.mov
- isothermal_euler_2d.mov
- isothermal_euler_3d.mov
- compressible_euler_1d.rkt
- compressible_euler_2d.rkt
- compressible_euler_3d.rkt
- isothermal_euler_1d.rkt
- isothermal_euler_2d.rkt
- isothermal_euler_3d.rkt
.gitattributes
LICENSE
README.md
two-cylinders.png

# Use via CDN

jsDelivr

jsDelivr serves any public GitHub repository as a CDN with zero setup. Pick a version and a file to get a ready-to-paste link and snippet.

Version

File

Link

Example

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

## Highlights

* End-to-end formally verified solvers for the isothermal Euler and full compressible Euler equations (assuming an ideal gas equation of state), in 1D, 2D, and 3D.
* **Took ~179 seconds for Lanyon to generate everything**.
  * ~13 seconds for isothermal Euler in 1D, ~20 seconds for isothermal Euler in 2D, ~35 seconds for isothermal Euler in 3D, ~54 seconds for full compressible Euler in 1D, ~23 seconds for full compressible Euler in 2D, ~34 seconds for full compressible Euler in 3D.
  * Real-time screen captures are shown in `/screencaps`.
* **10,750 lines of Lean 4 code** to prove end-to-end correctness properties.
  * 619 for isothermal Euler in 1D, 1,378 for isothermal Euler in 2D, 2,469 for isothermal Euler in 3D, 872 for full compressible Euler in 1D, 1,954 for full compressible Euler in 2D, 3,458 for full compressible Euler in 3D.
* **270 total definitions** and **156 total theorems**.
* **6,876 lines of formally verified C code**.
  * 504 for isothermal Euler in 1D, 976 for isothermal Euler in 2D, 1,582 for isothermal Euler in 3D, 601 for full compressible Euler in 1D, 1,206 for full compressible Euler in 2D, 2,007 for full compressible Euler in 3D.

## Further Details

The most general form of the compressible Euler equations consists of a conservation law for mass:

$$ \frac{\partial \rho}{\partial t} + \nabla \cdot \left( \rho \mathbf{u} \right) = 0 $$

a conservation law for momentum:

$$ \frac{\partial}{\partial t} \left( \rho \mathbf{u} \right) + \nabla \cdot \left( \rho \mathbf{u} \otimes \mathbf{u} + p \mathbf{I} \right) = 0 $$

and a conservation law for total energy:

$$ \frac{\partial \varepsilon}{\partial t} + \nabla \cdot \left( \mathbf{u} \left( \varepsilon + p \right) \right) = 0 $$

for fluid mass density ${\rho}$, fluid velocity ${\mathbf{u}}$, fluid pressure $p$, rank-2 identity tensor ${\mathbf{I}}$, and total fluid energy ${\varepsilon}$. The total energy ${\varepsilon}$ contains contributions from both the fluid's kinetic energy ${\frac{1}{2} \rho \mathbf{u} \cdot \mathbf{u}}$ and the fluid's specific internal energy; for an ideal gas equation of state, this takes the specific form:

$$ \varepsilon = \frac{1}{2} \rho \mathbf{u} \cdot \mathbf{u} + \frac{p}{\gamma - 1} $$

for adiabatic index ${\gamma}$.

In the isothermal limit, the mass conservation law is left unchanged:

$$ \frac{\partial \rho}{\partial t} + \nabla \cdot \left( \rho \mathbf{u} \right) = 0 $$

and the momentum conservation law reduces to:

$$ \frac{\partial}{\partial t} \left( \rho \mathbf{u} \right) + \nabla \cdot \left( \rho \mathbf{u} \otimes \mathbf{u} + \rho v_{t}^{2} \mathbf{I} \right) = 0 $$

for (constant) fluid thermal velocity ${v_t}$, with the pressure term $p$ and the equation for the total fluid energy ${\varepsilon}$ dropping out entirely. For full details of the equations, the numerical methods used for solving them, and the specific prompts used within Lanyon for running simulations, see [our technical deep dive on the Euler equations](https://lanyon.ai/research/euler-equations/).

![Mach 2 flow over two rigid cylinders](https://raw.githubusercontent.com/lanyonai/CompressibleEuler/main/two-cylinders.png)