FYI: Support raw-pointer casts to non-literal pointee types (SHA-NI extraction)#976
Open
fournet wants to merge 3 commits into
Open
FYI: Support raw-pointer casts to non-literal pointee types (SHA-NI extraction)#976fournet wants to merge 3 commits into
fournet wants to merge 3 commits into
Conversation
The new Aeneas translation generates destructuring binds: let (s, back) ← lift (Array.to_slice_mut a) The old @[step_pure_def] left an opaque pair that couldn't be reduced. The new @[step] theorem introduces s and back as separate variables. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Changed tuple postconditions ⦃ (s, back) => ... ⦄ to curried ⦃ (s : Slice α) (back : Slice α → ...) => ... ⦄ in: - Slice.lean: SliceIndexRangeUsizeSlice.index_mut - Slice.lean: SliceIndexRangeToUsizeSlice.index_mut - Slice.lean: SliceIndexRangeFromUsizeSlice.index_mut - Vec.lean: Vec.index_mut_RangeTo/RangeFrom/Range_spec - ArraySlice.lean: Array.index_mut_SliceIndexRangeTo/From This handles the new Aeneas translation pattern where let (s, back) ← f destructures the result pair. With curried postconditions, step introduces s and back as separate variables matching the destructuring. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Generalize CastRawPtr's source/target pointee from literal_type to ty, so that casts whose pointee is an opaque builtin (e.g. *const __m128i, *const __m256i) or any other non-scalar type are translated rather than raising a fatal error. On the Lean backend this is emitted as a generic RawPtr.cast that leaves the source and target pointee types implicit (Lean infers them from the surrounding context, e.g. the argument type of _mm_loadu_si128). On other backends we still restrict to literal scalar pointees as before. Fixes the OOM observed when extracting SymCrypt's SHA-NI fast path (sha2::sha2_impl::append_blocks_256_shani), which contains many *const u8 -> *const __m128i casts.
Contributor
|
Hi! Heads-up that our work likely overlaps. I've formally verified RustCrypto's SHA-256, see my fork, against a literate translation of the FIPS-180-4 spec. Happy to collaborate. Contact: remix7531@mailbox.org. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
FYI — sharing for visibility / discussion. Not requesting merge.
Three small commits surfaced while preparing the SymCrypt SHA-2 SHA-NI
verification target.
1.
Add @[step] theorem for Array.to_slice_mut with curried postconditionAdds a
@[step]theorem so thatstepcan decomposeArray.to_slice_mut. Uses the curried⦃ s lib => ... ⦄postconditionform so callers don't need to destructure a tuple.
2.
Curried postconditions for all index_mut/to_slice_mut step specsSweep across
Array/ArraySlice.lean,Slice.lean,Vec.leanto convertthe existing
index_mut/to_slice_mutstep theorems to the curriedform. One Bst test updated.
3.
Support raw-pointer casts to non-literal pointee typesGeneralize
CastRawPtr's source/target pointee fromliteral_typetoty, so casts whose pointee is an opaque builtin (e.g.*const __m128i,*const __m256i) or any other non-scalar type are translated rather thanraising a fatal error.
On the Lean backend this is emitted as a generic
RawPtr.castthatleaves the source and target pointee types implicit (Lean infers them
from the surrounding context, e.g. the argument type of
_mm_loadu_si128). On other backends we still restrict to literalscalar pointees as before.
This fixes the OOM observed when extracting SymCrypt's SHA-NI fast path
(
sha2::sha2_impl::append_blocks_256_shani), which contains many*const u8 as *const __m128icasts via primitives like:Validated end-to-end: extraction of the full SymCrypt SHA-2 module
including the SHA-NI fast path now produces clean Lean (
defs for theload/store primitives, axiomatised intrinsics for
_mm_sha256rnds2_epu32etc.).
Conflict resolution
The cherry-pick of #3 onto current
origin/mainproduced a singletrivial conflict against the recent Charon update (
d9d473d0 Update Charon): both branches independently renamedCharon.Print.cast_kind_to_string→Charon.PrintExpressions.cast_kind_to_stringin the same error site. Resolution: kept this PR's version, which also
updates the surrounding code path.