Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Adopt the Arm SIMD-optimized p384 fields to point operations
This patch updates the p384 point operations to use the field operations optimized using NEON and the SLOTHY optimizer. The performance improvement is around 9%. ``` p384_montjdouble : 591.7 ns each (var 0.1%, corr -0.02) = 1690105 ops/sec p384_montjadd : 1143.6 ns each (var 0.1%, corr 0.04) = 874447 ops/sec p384_montjscalarmul : 329982.3 ns each (var 0.0%, corr 0.09) = 3030 ops/sec => p384_montjdouble : 543.2 ns each (var 0.1%, corr 0.02) = 1840798 ops/sec p384_montjadd : 1044.5 ns each (var 0.1%, corr -0.09) = 957396 ops/sec p384_montjscalarmul : 303017.8 ns each (var 0.0%, corr 0.04) = 3300 ops/sec ``` This patch also includes the following updates: - Add `arm/proofs/utils` and factor out the OCaml codes that are parameters to the equivalence checking tactics as files in the directory. - Update EQUIV_STEP_TAC to take additional arguments that describe dead value information of the registers in the programs. The information describes which registers contain dead values after each program location. EQUIV_STEP_TAC uses this information to clean assumptions that will not be used later during simulation. - A few tactics for equivalence checking to shorten repeatedly appearing proof patterns and a few updates in arm.ml for better error messages - Bug fixes in actions_merger.ml - Add a user-defined custom cache to ORTHOGONAL_COMPONENTS_CONV. This is useful for equiv checking because the memory invariants that appear in assumptions have a typical form (the byte64). - And many other improvements for speed
- Loading branch information
1 parent
d85c6b5
commit 0af76bc