GitHub - bollu/fpsan-verification: The one where bollu vibes the correctness of Triton's FPSan · GitHub
/" data-turbo-transient="true" />
Skip to content
Search or jump to...
Search code, repositories, users, issues, pull requests...
-->
Search
Clear
Search syntax tips
Provide feedback
--><br>We read every piece of feedback, and take your input very seriously.
Include my email address so I can be contacted
Cancel
Submit feedback
Saved searches
Use saved searches to filter your results more quickly
-->
Name
Query
To see all available qualifiers, see our documentation.
Cancel
Create saved search
Sign in
/;ref_cta:Sign up;ref_loc:header logged out"}"<br>Sign up
Appearance settings
Resetting focus
You signed in with another tab or window. Reload to refresh your session.<br>You signed out in another tab or window. Reload to refresh your session.<br>You switched accounts on another tab or window. Reload to refresh your session.
Dismiss alert
{{ message }}
bollu
fpsan-verification
Public
Notifications<br>You must be signed in to change notification settings
Fork
Star
master
BranchesTags
Go to file
CodeOpen more actions menu
Folders and files<br>NameNameLast commit message<br>Last commit date<br>Latest commit
History<br>1 Commit<br>1 Commit
RequestProject
RequestProject
.gitignore
.gitignore
ARISTOTLE_SUMMARY.md
ARISTOTLE_SUMMARY.md
README.md
README.md
fpsan.txt
fpsan.txt
lake-manifest.json
lake-manifest.json
lakefile.toml
lakefile.toml
lean-toolchain
lean-toolchain
View all files
Repository files navigation
Verification of Triton's FPSan
We use the FPSan.cpp from triton to lift definitions into Lean,<br>along with definitions from opencompl/fp-lean of floating point numbers,<br>to give a formally verified implementation of the FPSan sanitizer in Lean.<br>Then, the bulk of the work was performed by Aristotle,<br>with high-level guidance from me on proof strategies, due to my experience with<br>floating point and bitvector verification in Lean, as well as experience thinking<br>about decision procedures for exponential rings (thanks Ben!).
Axioms
We take as axiom the fact that if two circuits agree on the free exponential ring,<br>which we just take to be the reals, then they agree on agree exponential ring.<br>This is the essential content of Macintyre'91.
Proofs
We prove the following properties of the embedding:
Homomorphism theorems (φ commutes with every operation)
phi_fpsanAdd: φ(fpsanAdd(a, b)) = φ(a) + φ(b)
phi_fpsanSub: φ(fpsanSub(a, b)) = φ(a) - φ(b)
phi_fpsanMul: φ(fpsanMul(a, b)) = φ(a) * φ(b)
phi_fpsanNeg: φ(fpsanNeg(a)) = -φ(a)
phi_fpsanZero: φ(fpsanZero) = 0
phi_fpsanOne: φ(fpsanOne) = 1
phi_fpsanExp: φ(fpsanExp(a)) = exp(φ(a))
phi_fpsanSin: φ(fpsanSin(a)) = sin(φ(a))
phi_fpsanCos: φ(fpsanCos(a)) = cos(φ(a))
Ring axioms (FPSan operations form a commutative ring)
fpsanAdd_comm, fpsanAdd_assoc — addition is commutative and associative
fpsanZero_add, fpsanAdd_zero — zero is the additive identity
fpsanNeg_add — negation is the additive inverse
fpsanSub_eq_add_neg — subtraction equals adding the negation
fpsanMul_comm, fpsanMul_assoc — multiplication is commutative and associative
fpsanOne_mul, fpsanMul_one — one is the multiplicative identity
fpsanMul_add, fpsanAdd_mul — distributivity
Exponential ring axioms
fpsanExp_zero: fpsanExp(0) = 1
fpsanExp_add: fpsanExp(a + b) = fpsanExp(a) * fpsanExp(b)
Trigonometric identities
fpsanSin_zero, fpsanCos_zero — sin(0) = 0, cos(0) = 1
fpsanCos_add — cosine angle-sum formula
fpsanSin_add — sine angle-sum formula
fpsanSin_sq_add_cos_sq — Pythagorean identity: sin²(a) + cos²(a) = 1
About
The one where bollu vibes the correctness of Triton's FPSan
Resources
Readme
Uh oh!
There was an error while loading. Please reload this page.
Activity
Stars
stars
Watchers
watching
Forks
forks
Report repository
Releases
No releases published
Packages
Uh oh!
There was an error while loading. Please reload this page.
Contributors
Uh oh!
There was an error while loading. Please reload this page.
Languages
Lean<br>100.0%
You can’t perform that action at this time.