Improved models for SIMD intrinsics - #1481

Open

karthikbhargavan wants to merge 19 commits into

mainfrom

pr2-intrinsics

Commits on Jul 23, 2026

core-models: unify intrinsics reference models across proof branches

karthikbhargavan
authored and
abentkamp
committed
cf8dff6
core-models: intrinsics differential-test + audit tooling

karthikbhargavan
authored and
abentkamp
committed
23fb712
intrinsics: unify arm64/avx2 F* trust axioms across proof branches

karthikbhargavan
authored and
abentkamp
committed
7272e46
intrinsics: prove the ARM64 NEON SHA3 fallback implementations (veor3q/vbcaxq/vrax1q/vxarq)

karthikbhargavan
authored and
abentkamp
committed
f946d2b
intrinsics/core-models: cargo fmt

karthikbhargavan
authored and
abentkamp
committed
f316b18
intrinsics: mark get_lane_u64 opaque to hax (raw-pointer helper)

karthikbhargavan
authored and
abentkamp
committed
495050b
changelog: add #1481 (improved models for SIMD intrinsics)

karthikbhargavan
authored and
abentkamp
committed
0ada4bb
changelog: trim #1481 entry to title

karthikbhargavan
authored and
abentkamp
committed
2c09416
changelog: tag #1481 with affected crates

karthikbhargavan
authored and
abentkamp
committed
0d27e25
ml-dsa/intrinsics: F* spec lemmas for AVX2 compute_hint/use_hint + rejection_sample

karthikbhargavan
authored and
abentkamp
committed
bb7dc08
ml-dsa Spec.Intrinsics: add 3 D6.3 rejection_sample bit-model axioms (parity with ml-dsa-proofs)

authored and
abentkamp
committed
580b396
pr2-intrinsics: strengthen NEON _vld1q_bytes/_vst1q_bytes + add vec128_as_i16x8 bit-decomp axiom

authored and
abentkamp
committed
b61aa2d
pr2-intrinsics: add validated mm256_srai_epi32 arithmetic-shift axiom

authored and
abentkamp
committed
c787e3b
pr2-intrinsics: add validated arm64 s32<->u32 lane reinterpret bridge axiom

authored and
abentkamp
committed
66711be
agent-mlkem: pr2-intrinsics e_vst1q_u8 per-byte store axiom (A2)

authored and
abentkamp
committed
f39d601
sha3: split simd/{arm64,avx2}.rs into load/store/wrappers submodules

karthikbhargavan
authored and
abentkamp
committed
9ac2afa
pr2-intrinsics: fix vqdmulh overflow + unify shift-immediate masking in core-models

karthikbhargavan
authored and
abentkamp
committed
00b33ad
pr2-intrinsics: resolve Error 233 and prove AVX2 lane-view axioms

karthikbhargavan
authored and
abentkamp
committed
64100fe
pr2-intrinsics: trust-base tooling, CI gate, and trust plan

karthikbhargavan
authored and
abentkamp
committed
726b450

Navigation Menu

Uh oh!

Improved models for SIMD intrinsics - #1481

Improved models for SIMD intrinsics#1481
karthikbhargavan wants to merge 19 commits into
mainfrom
pr2-intrinsics

Commits on Jul 23, 2026

core-models: unify intrinsics reference models across proof branches

core-models: intrinsics differential-test + audit tooling

intrinsics: unify arm64/avx2 F* trust axioms across proof branches

intrinsics: prove the ARM64 NEON SHA3 fallback implementations (veor3q/vbcaxq/vrax1q/vxarq)

intrinsics/core-models: cargo fmt

intrinsics: mark get_lane_u64 opaque to hax (raw-pointer helper)

changelog: add #1481 (improved models for SIMD intrinsics)

changelog: trim #1481 entry to title

changelog: tag #1481 with affected crates

ml-dsa/intrinsics: F* spec lemmas for AVX2 compute_hint/use_hint + rejection_sample

ml-dsa Spec.Intrinsics: add 3 D6.3 rejection_sample bit-model axioms (parity with ml-dsa-proofs)

pr2-intrinsics: strengthen NEON _vld1q_bytes/_vst1q_bytes + add vec128_as_i16x8 bit-decomp axiom

pr2-intrinsics: add validated mm256_srai_epi32 arithmetic-shift axiom

pr2-intrinsics: add validated arm64 s32<->u32 lane reinterpret bridge axiom

agent-mlkem: pr2-intrinsics e_vst1q_u8 per-byte store axiom (A2)

sha3: split simd/{arm64,avx2}.rs into load/store/wrappers submodules

pr2-intrinsics: fix vqdmulh overflow + unify shift-immediate masking in core-models

pr2-intrinsics: resolve Error 233 and prove AVX2 lane-view axioms

pr2-intrinsics: trust-base tooling, CI gate, and trust plan