mlkem-native/dev/fips202/aarch64/src/fips202_native_aarch64.h at main · pq-code-package/mlkem-native · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
/*
 * Copyright (c) The mlkem-native project authors
 * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 */
#ifndef MLK_DEV_FIPS202_AARCH64_SRC_FIPS202_NATIVE_AARCH64_H
#define MLK_DEV_FIPS202_AARCH64_SRC_FIPS202_NATIVE_AARCH64_H

#include "../../../../cbmc.h"
#include "../../../../common.h"

#define mlk_keccakf1600_round_constants \
  MLK_NAMESPACE(keccakf1600_round_constants)
MLK_INTERNAL_DATA_DECLARATION const uint64_t
    mlk_keccakf1600_round_constants[24];

#define mlk_keccak_f1600_x1_scalar_aarch64_asm \
  MLK_NAMESPACE(keccak_f1600_x1_scalar_aarch64_asm)
void mlk_keccak_f1600_x1_scalar_aarch64_asm(uint64_t state[25],
                                            const uint64_t rc[24])
/* This must be kept in sync with the HOL-Light specification
 * in proofs/hol_light/aarch64/proofs/keccak_f1600_x1_scalar_aarch64_asm.ml */
__contract__(
  requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1))
  requires(rc == mlk_keccakf1600_round_constants)
  assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1))
);

#define mlk_keccak_f1600_x1_v84a_aarch64_asm \
  MLK_NAMESPACE(keccak_f1600_x1_v84a_aarch64_asm)
void mlk_keccak_f1600_x1_v84a_aarch64_asm(uint64_t state[25],
                                          const uint64_t rc[24])
/* This must be kept in sync with the HOL-Light specification
 * in proofs/hol_light/aarch64/proofs/keccak_f1600_x1_v84a_aarch64_asm.ml */
__contract__(
  requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1))
  requires(rc == mlk_keccakf1600_round_constants)
  assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1))
);

#define mlk_keccak_f1600_x2_v84a_aarch64_asm \
  MLK_NAMESPACE(keccak_f1600_x2_v84a_aarch64_asm)
void mlk_keccak_f1600_x2_v84a_aarch64_asm(uint64_t state[50],
                                          const uint64_t rc[24])
/* This must be kept in sync with the HOL-Light specification
 * in proofs/hol_light/aarch64/proofs/keccak_f1600_x2_v84a_aarch64_asm.ml */
__contract__(
  requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 2))
  requires(rc == mlk_keccakf1600_round_constants)
  assigns(memory_slice(state, sizeof(uint64_t) * 25 * 2))
);

#define mlk_keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm \
  MLK_NAMESPACE(keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm)
void mlk_keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm(uint64_t state[100],
                                                       const uint64_t rc[24])
/* This must be kept in sync with the HOL-Light specification
 * in
 * proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml
 */
__contract__(
  requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4))
  requires(rc == mlk_keccakf1600_round_constants)
  assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4))
);

#define mlk_keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm \
  MLK_NAMESPACE(keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm)
void mlk_keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm(
    uint64_t state[100], const uint64_t rc[24])
/* This must be kept in sync with the HOL-Light specification
 * in
 * proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.ml
 */
__contract__(
  requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4))
  requires(rc == mlk_keccakf1600_round_constants)
  assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4))
);

#endif /* !MLK_DEV_FIPS202_AARCH64_SRC_FIPS202_NATIVE_AARCH64_H */