New Challenge 14 - High-Assurance SIMD Intrinsics for Rust #174
Conversation
| these contracts hold when the intrinsics are executed in Rust. | ||
| A secondary goal is to use these contracts as formal specifications | ||
| of the intrinsics API when doing proofs of Rust programs in proof | ||
| assistants like F* and Coq. |
There was a problem hiding this comment.
Why do specific tools matter when you are providing contracts?
There was a problem hiding this comment.
I reduced references to specific tools, but I usually find it better to be concrete.
|
|
||
| Separately, when formally verifying cryptographic libraries, each | ||
| project needs to define its own semantics for SIMD instructions in | ||
| EasyCrypt, F*, or Coq. This work is both time-consuming and |
There was a problem hiding this comment.
Is this necessarily a complete list of tools?
|
|
||
| Consequently, we believe there is a strong need for a consistent, | ||
| formal, testable specification of the SIMD intrinsics that can aid | ||
| Rust crypto developers. Furthermore, we believe that this |
There was a problem hiding this comment.
The motivation comes from crypto, but I rewrote to expand the potential application domain.
| formal, testable specification of the SIMD intrinsics that can aid | ||
| Rust crypto developers. Furthermore, we believe that this | ||
| specification is written in a way that can be used to aid formal | ||
| verification of cryptography in various backend tools, including F*, |
There was a problem hiding this comment.
Is it a necessity that specifications are tailored towards crypto? We seek to do verification for all use cases.
There was a problem hiding this comment.
The specifications are not tailored towards crypto, they are tailored towards verification. Rewrote.
| ``` | ||
|
|
||
| This contract is then used to automatically generate randomized tests | ||
| for the intrinsic, which can be put on CI. |
There was a problem hiding this comment.
| for the intrinsic, which can be put on CI. | |
| for the intrinsic, which can be put in CI. |
| ``` | ||
|
|
||
| We then prove that this contract is consistent with the model of the | ||
| SIMD intrinsic in F* (i.e. our F* implementation of `mm_blen_epi16`) |
There was a problem hiding this comment.
| SIMD intrinsic in F* (i.e. our F* implementation of `mm_blen_epi16`) | |
| SIMD intrinsic in F* (i.e. our F* implementation of `mm_blend_epi16`) |
|
|
||
| ### Assumptions | ||
|
|
||
| Users must trust the semantics of Rust encoded within the `hax` |
There was a problem hiding this comment.
I am not sure that growing the TCB is a good idea, especially in a direction that will be somewhat foreign and inscrutable to Rust developers.
There was a problem hiding this comment.
Rewrote to clarify. Of course, every Rust verification tool has its own TCB.
|
|
||
| The goal is to annotate >= 100 intrinsics in `core::arch::x86_64` and | ||
| `core::arch::aarch64` with contracts, and all these contracts will be | ||
| tested both in Rust and in F*. These functions will include all the |
There was a problem hiding this comment.
I believe the F* part should be a tool proposal and not be intertwined with the challenge. Combining these both limits who can take on the challenge and also restricts us in getting any of this adopted upstream.
There was a problem hiding this comment.
There will be a separate tool proposal for integrating hax (with F*, Coq, and possibly other provers as proof backends). We can remove the F* validation completely from here or offer it as an add-on to the solution.
There was a problem hiding this comment.
After a first pass, my major comment is just to add more clarification on how to pick verification targets, avoid targeting tools to solve the challenge and do not attach the success criteria to any third-party libraries.
We can later send a tool proposal to be integrated into the repository and you can add more discussions on how to solve the challenge, even mentioning specific tools, in the GitHub issue corresponding to the challenge. However, this description should focus on what targets and properties are relevant and why.
- note: I do encourage to use the application of this work in crypto to help prioritize the verification targets.
|
|
||
| - **Status:** Open | ||
| - **Solution:** | ||
| - **Tracking Issue:** https://github.com/model-checking/verify-rust-std/issues/173 |
| This contract is then used to automatically generate randomized tests | ||
| for the intrinsic, which can be put in CI. |
| We can also use the [hax](https://github.com/hacspec/hax) toolchain to | ||
| compile this contract to F* where it can act as an interface to a model | ||
| of the intrinsics library. | ||
|
|
||
| ``` | ||
| val _mm_blend_epi16: __m128i -> __m128i -> i32 -> | ||
| Pure __m128i | ||
| (requires (v IMM8 >= 0 && v IMM8 <= 255))\ | ||
| (ensures(fun result -> | ||
| forall j. j >= 0 && j < 8 ==> | ||
| if get_bit(IMM8,j) then | ||
| get_lane(result, j) == get_lane(b,j) | ||
| else | ||
| get_lane(result, j) == get_lane(a,j))) | ||
| ``` | ||
|
|
||
| We then prove that this contract is consistent with the model of the | ||
| SIMD intrinsic in F* (i.e. our F* implementation of `mm_blend_epi16`) | ||
| and also run the same tests we ran in Rust against this model in F* to | ||
| gain more confidence in our translation from Rust. | ||
|
|
||
| Finally, we will show how to use this contract in F* in proofs like | ||
| the libcrux proof for the ML-KEM post-quantum cryptographic | ||
| contruction. |
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.