Languages Features Creators Calendar CSV Resources Blog About Pricing Add Language
GitHub icon

Vale

Vale - Assembly language

< >

Vale, aka Verified Assembly Language for Everest, is an assembly language created in 2017 by Chris Hawblitzel.

#1105on PLDB 6Years Old 272Users
0Books 0Papers

Vale is a tool for constructing formally verified high-performance assembly language code, with an emphasis on cryptographic code. It uses existing verification frameworks, such as Dafny and F*, for formal verification. It supports multiple architectures, such as x86, x64, and ARM, and multiple platforms, such as Windows, Mac, and Linux. Additional architectures and platforms can be supported with no changes to the Vale tool.


Example from the web:
procedure ReadA(ghost a:seq(uint32),inline b:bool) reads r0; mem; modifies r1; requires length(a) >= 3; a[0] <= 100; a[1] <= 100; forall i :: 0 <= i < length(a) ==> InMem(r0 + 4 * i, mem) && mem[r0 + 4 * i] == a[i]; ensures b ==> r1 == a[0] + 1; !b ==> r1 == a[1] + 1; { inline if (b) { LDR(r1, r0, 0); //load memory [r0+0] into r1 AddOne(r1); } else { LDR(r1, r0, 4); //load memory [r0+4] into r1 AddOne(r1); } } procedure{:recursive} AddNToR7(inline n:nat) modifies r7; requires r7 + n <= 0xffffffff; ensures r7 == old(r7) + n; { inline if (n > 0) { AddOne(r7); AddNToR7(n - 1); }

Language features

Feature Supported Token Example
Comments
// A comment
Line Comments //
// A comment
Semantic Indentation X
gentoo-ebuild.html · vale-assembly.html · mirc.html

View source

- Build the next great programming language · Search · v2023 · Day 205 · Docs · Acknowledgements · Traffic · Traffic Today · Mirrors · GitHub · feedback@pldb.com