Skip to content

Commit 2f0dd55

Browse files
jakemasUbuntu
jakemas
authored and
Ubuntu
committed
Add HOL Light poly_use_hint_32 and poly_use_hint_88 proofs with functional correctness
Add formal verification proofs for mldsa_poly_use_hint_32 and mldsa_poly_use_hint_88 AArch64 NEON implementations. Both proofs establish full functional correctness: the assembly output equals word(mldsa_use_hint_XX_spec(val(input_a), val(input_h))) for each element, matching the ML-DSA specification. Both proofs work in HOL Light native compilation mode, using: - Barrett reduction equivalence via general interval lemma - Bridge lemmas for real_gt/int_gt type compatibility - BITBLAST_RULE for word comparison bounds - WORD_SUBWORD push-through for SIMD endgame Also adds CI workflow entries, CBMC contracts, header declarations for the use_hint assembly functions, and shared helper lemmas in common/mldsa_specs.ml. Signed-off-by: Jake Massimo <jakemas@amazon.com>
1 parent e47b1c2 commit 2f0dd55

14 files changed

Lines changed: 1647 additions & 4 deletions

File tree

‎.github/workflows/hol_light.yml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -95,6 +95,10 @@ jobs:
9595
needs: ["aarch64_utils.ml"]
9696
- name: mldsa_poly_chknorm
9797
needs: ["aarch64_utils.ml"]
98+
- name: mldsa_poly_use_hint_32
99+
needs: ["mldsa_specs.ml", "subroutine_signatures.ml"]
100+
- name: mldsa_poly_use_hint_88
101+
needs: ["mldsa_specs.ml", "subroutine_signatures.ml"]
98102
- name: keccak_f1600_x1_scalar
99103
needs: ["keccak_spec.ml"]
100104
- name: keccak_f1600_x1_v84a

‎dev/aarch64_opt/src/arith_native_aarch64.h‎

Lines changed: 24 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -117,10 +117,32 @@ __contract__(
117117

118118
#if !defined(MLD_CONFIG_NO_VERIFY_API)
119119
#define mld_poly_use_hint_32_asm MLD_NAMESPACE(poly_use_hint_32_asm)
120-
void mld_poly_use_hint_32_asm(int32_t *b, const int32_t *a, const int32_t *h);
120+
void mld_poly_use_hint_32_asm(int32_t *b, const int32_t *a, const int32_t *h)
121+
/* This must be kept in sync with the HOL-Light specification
122+
* in proofs/hol_light/aarch64/proofs/mldsa_poly_use_hint_32.ml */
123+
__contract__(
124+
requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
125+
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
126+
requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
127+
requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
128+
requires(array_bound(h, 0, MLDSA_N, 0, 2))
129+
assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
130+
ensures(array_bound(b, 0, MLDSA_N, 0, 16))
131+
);
121132

122133
#define mld_poly_use_hint_88_asm MLD_NAMESPACE(poly_use_hint_88_asm)
123-
void mld_poly_use_hint_88_asm(int32_t *b, const int32_t *a, const int32_t *h);
134+
void mld_poly_use_hint_88_asm(int32_t *b, const int32_t *a, const int32_t *h)
135+
/* This must be kept in sync with the HOL-Light specification
136+
* in proofs/hol_light/aarch64/proofs/mldsa_poly_use_hint_88.ml */
137+
__contract__(
138+
requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
139+
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
140+
requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
141+
requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
142+
requires(array_bound(h, 0, MLDSA_N, 0, 2))
143+
assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
144+
ensures(array_bound(b, 0, MLDSA_N, 0, 44))
145+
);
124146
#endif /* !MLD_CONFIG_NO_VERIFY_API */
125147

126148
#define mld_poly_chknorm_asm MLD_NAMESPACE(poly_chknorm_asm)

‎mldsa/src/native/aarch64/src/arith_native_aarch64.h‎

Lines changed: 24 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -117,10 +117,32 @@ __contract__(
117117

118118
#if !defined(MLD_CONFIG_NO_VERIFY_API)
119119
#define mld_poly_use_hint_32_asm MLD_NAMESPACE(poly_use_hint_32_asm)
120-
void mld_poly_use_hint_32_asm(int32_t *b, const int32_t *a, const int32_t *h);
120+
void mld_poly_use_hint_32_asm(int32_t *b, const int32_t *a, const int32_t *h)
121+
/* This must be kept in sync with the HOL-Light specification
122+
* in proofs/hol_light/aarch64/proofs/mldsa_poly_use_hint_32.ml */
123+
__contract__(
124+
requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
125+
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
126+
requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
127+
requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
128+
requires(array_bound(h, 0, MLDSA_N, 0, 2))
129+
assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
130+
ensures(array_bound(b, 0, MLDSA_N, 0, 16))
131+
);
121132

122133
#define mld_poly_use_hint_88_asm MLD_NAMESPACE(poly_use_hint_88_asm)
123-
void mld_poly_use_hint_88_asm(int32_t *b, const int32_t *a, const int32_t *h);
134+
void mld_poly_use_hint_88_asm(int32_t *b, const int32_t *a, const int32_t *h)
135+
/* This must be kept in sync with the HOL-Light specification
136+
* in proofs/hol_light/aarch64/proofs/mldsa_poly_use_hint_88.ml */
137+
__contract__(
138+
requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
139+
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
140+
requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
141+
requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
142+
requires(array_bound(h, 0, MLDSA_N, 0, 2))
143+
assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
144+
ensures(array_bound(b, 0, MLDSA_N, 0, 44))
145+
);
124146
#endif /* !MLD_CONFIG_NO_VERIFY_API */
125147

126148
#define mld_poly_chknorm_asm MLD_NAMESPACE(poly_chknorm_asm)

‎proofs/cbmc/poly_use_hint_native_aarch64/Makefile‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
# Copyright (c) The mldsa-native project authors
2+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
include ../Makefile_params.common
5+
6+
HARNESS_ENTRY = harness
7+
HARNESS_FILE = poly_use_hint_native_aarch64_harness
8+
9+
# This should be a unique identifier for this proof, and will appear on the
10+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
11+
PROOF_UID = poly_use_hint_native_aarch64
12+
13+
# We need to set MLD_CHECK_APIS as otherwise mldsa/src/native/api.h won't be
14+
# included, which contains the CBMC specifications.
15+
DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/aarch64/meta.h\"" -DMLD_CHECK_APIS
16+
INCLUDES +=
17+
18+
REMOVE_FUNCTION_BODY +=
19+
UNWINDSET +=
20+
21+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
22+
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c
23+
24+
ifeq ($(MLD_CONFIG_PARAMETER_SET),44)
25+
CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint_88_native
26+
USE_FUNCTION_CONTRACTS=mld_poly_use_hint_88_asm
27+
else ifeq ($(MLD_CONFIG_PARAMETER_SET),65)
28+
CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint_32_native
29+
USE_FUNCTION_CONTRACTS=mld_poly_use_hint_32_asm
30+
else ifeq ($(MLD_CONFIG_PARAMETER_SET),87)
31+
CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint_32_native
32+
USE_FUNCTION_CONTRACTS=mld_poly_use_hint_32_asm
33+
endif
34+
USE_FUNCTION_CONTRACTS+=mld_sys_check_capability
35+
APPLY_LOOP_CONTRACTS=on
36+
USE_DYNAMIC_FRAMES=1
37+
38+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
39+
EXTERNAL_SAT_SOLVER=
40+
CBMCFLAGS=--smt2
41+
42+
FUNCTION_NAME = poly_use_hint_native_aarch64
43+
44+
# If this proof is found to consume huge amounts of RAM, you can set the
45+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
46+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
47+
# documentation in Makefile.common under the "Job Pools" heading for details.
48+
# EXPENSIVE = true
49+
50+
# This function is large enough to need...
51+
CBMC_OBJECT_BITS = 8
52+
53+
include ../Makefile.common

‎proofs/cbmc/poly_use_hint_native_aarch64/poly_use_hint_native_aarch64_harness.c‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
// Copyright (c) The mldsa-native project authors
2+
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
#include <stdint.h>
5+
#include "cbmc.h"
6+
#include "params.h"
7+
8+
#if MLDSA_GAMMA2 == ((MLDSA_Q - 1) / 88)
9+
int mld_poly_use_hint_88_native(int32_t *b, const int32_t *a, const int32_t *h);
10+
#else
11+
int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a, const int32_t *h);
12+
#endif
13+
14+
void harness(void)
15+
{
16+
int32_t *b, *a, *h;
17+
int t;
18+
19+
#if MLDSA_GAMMA2 == ((MLDSA_Q - 1) / 88)
20+
t = mld_poly_use_hint_88_native(b, a, h);
21+
#else
22+
t = mld_poly_use_hint_32_native(b, a, h);
23+
#endif
24+
}

‎proofs/hol_light/README.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,8 @@ echo '1+1;;' | nc -w 5 127.0.0.1 2012
5454
- ML-DSA Arithmetic:
5555
* AArch64 poly_caddq: [mldsa_poly_caddq.S](aarch64/mldsa/mldsa_poly_caddq.S)
5656
* AArch64 poly_chknorm: [mldsa_poly_chknorm.S](aarch64/mldsa/mldsa_poly_chknorm.S)
57+
* AArch64 poly_use_hint (l=5,7): [mldsa_poly_use_hint_32.S](aarch64/mldsa/mldsa_poly_use_hint_32.S)
58+
* AArch64 poly_use_hint (l=4): [mldsa_poly_use_hint_88.S](aarch64/mldsa/mldsa_poly_use_hint_88.S)
5759
* AArch64 pointwise multiplication: [mldsa_pointwise.S](aarch64/mldsa/mldsa_pointwise.S)
5860
* AArch64 pointwise multiplication-accumulation (l=4): [mldsa_pointwise_acc_l4.S](aarch64/mldsa/mldsa_pointwise_acc_l4.S)
5961
* AArch64 pointwise multiplication-accumulation (l=5): [mldsa_pointwise_acc_l5.S](aarch64/mldsa/mldsa_pointwise_acc_l5.S)

‎proofs/hol_light/aarch64/Makefile‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,8 @@ OBJ = mldsa/mldsa_ntt.o \
5757
mldsa/mldsa_pointwise.o \
5858
mldsa/mldsa_poly_caddq.o \
5959
mldsa/mldsa_poly_chknorm.o \
60+
mldsa/mldsa_poly_use_hint_32.o \
61+
mldsa/mldsa_poly_use_hint_88.o \
6062
mldsa/mldsa_pointwise_acc_l4.o \
6163
mldsa/mldsa_pointwise_acc_l5.o \
6264
mldsa/mldsa_pointwise_acc_l7.o \

‎proofs/hol_light/aarch64/mldsa/mldsa_poly_use_hint_32.S‎

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,98 @@
1+
/*
2+
* Copyright (c) The mldsa-native project authors
3+
* SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
*/
5+
6+
7+
/*
8+
* WARNING: This file is auto-derived from the mldsa-native source file
9+
* dev/aarch64_opt/src/poly_use_hint_32_asm.S using scripts/simpasm. Do not modify it directly.
10+
*/
11+
12+
.text
13+
.balign 4
14+
#ifdef __APPLE__
15+
.global _PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_32_asm
16+
_PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_32_asm:
17+
#else
18+
.global PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_32_asm
19+
PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_32_asm:
20+
#endif
21+
22+
.cfi_startproc
23+
mov w4, #0xe001 // =57345
24+
movk w4, #0x7f, lsl #16
25+
dup v20.4s, w4
26+
mov w5, #0xe100 // =57600
27+
movk w5, #0x7b, lsl #16
28+
dup v21.4s, w5
29+
mov w7, #0xfe00 // =65024
30+
movk w7, #0x7, lsl #16
31+
dup v22.4s, w7
32+
mov w11, #0x401 // =1025
33+
movk w11, #0x4010, lsl #16
34+
dup v23.4s, w11
35+
movi v24.4s, #0xf
36+
mov x3, #0x10 // =16
37+
38+
Lpoly_use_hint_32_loop:
39+
ldr q1, [x1, #0x10]
40+
ldr q2, [x1, #0x20]
41+
ldr q3, [x1, #0x30]
42+
ldr q0, [x1], #0x40
43+
ldr q5, [x2, #0x10]
44+
ldr q6, [x2, #0x20]
45+
ldr q7, [x2, #0x30]
46+
ldr q4, [x2], #0x40
47+
sqdmulh v17.4s, v1.4s, v23.4s
48+
srshr v17.4s, v17.4s, #0x12
49+
cmgt v25.4s, v1.4s, v21.4s
50+
mls v1.4s, v17.4s, v22.4s
51+
bic v17.16b, v17.16b, v25.16b
52+
add v1.4s, v1.4s, v25.4s
53+
cmle v1.4s, v1.4s, #0
54+
orr v1.4s, #0x1
55+
mla v17.4s, v1.4s, v5.4s
56+
and v17.16b, v17.16b, v24.16b
57+
sqdmulh v18.4s, v2.4s, v23.4s
58+
srshr v18.4s, v18.4s, #0x12
59+
cmgt v25.4s, v2.4s, v21.4s
60+
mls v2.4s, v18.4s, v22.4s
61+
bic v18.16b, v18.16b, v25.16b
62+
add v2.4s, v2.4s, v25.4s
63+
cmle v2.4s, v2.4s, #0
64+
orr v2.4s, #0x1
65+
mla v18.4s, v2.4s, v6.4s
66+
and v18.16b, v18.16b, v24.16b
67+
sqdmulh v19.4s, v3.4s, v23.4s
68+
srshr v19.4s, v19.4s, #0x12
69+
cmgt v25.4s, v3.4s, v21.4s
70+
mls v3.4s, v19.4s, v22.4s
71+
bic v19.16b, v19.16b, v25.16b
72+
add v3.4s, v3.4s, v25.4s
73+
cmle v3.4s, v3.4s, #0
74+
orr v3.4s, #0x1
75+
mla v19.4s, v3.4s, v7.4s
76+
and v19.16b, v19.16b, v24.16b
77+
sqdmulh v16.4s, v0.4s, v23.4s
78+
srshr v16.4s, v16.4s, #0x12
79+
cmgt v25.4s, v0.4s, v21.4s
80+
mls v0.4s, v16.4s, v22.4s
81+
bic v16.16b, v16.16b, v25.16b
82+
add v0.4s, v0.4s, v25.4s
83+
cmle v0.4s, v0.4s, #0
84+
orr v0.4s, #0x1
85+
mla v16.4s, v0.4s, v4.4s
86+
and v16.16b, v16.16b, v24.16b
87+
str q17, [x0, #0x10]
88+
str q18, [x0, #0x20]
89+
str q19, [x0, #0x30]
90+
str q16, [x0], #0x40
91+
subs x3, x3, #0x1
92+
b.ne Lpoly_use_hint_32_loop
93+
ret
94+
.cfi_endproc
95+
96+
#if defined(__ELF__)
97+
.section .note.GNU-stack,"",%progbits
98+
#endif

‎proofs/hol_light/aarch64/mldsa/mldsa_poly_use_hint_88.S‎

Lines changed: 106 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,106 @@
1+
/*
2+
* Copyright (c) The mldsa-native project authors
3+
* SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
*/
5+
6+
7+
/*
8+
* WARNING: This file is auto-derived from the mldsa-native source file
9+
* dev/aarch64_opt/src/poly_use_hint_88_asm.S using scripts/simpasm. Do not modify it directly.
10+
*/
11+
12+
.text
13+
.balign 4
14+
#ifdef __APPLE__
15+
.global _PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_88_asm
16+
_PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_88_asm:
17+
#else
18+
.global PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_88_asm
19+
PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_88_asm:
20+
#endif
21+
22+
.cfi_startproc
23+
mov w4, #0xe001 // =57345
24+
movk w4, #0x7f, lsl #16
25+
dup v20.4s, w4
26+
mov w5, #0x6c00 // =27648
27+
movk w5, #0x7e, lsl #16
28+
dup v21.4s, w5
29+
mov w7, #0xe800 // =59392
30+
movk w7, #0x2, lsl #16
31+
dup v22.4s, w7
32+
mov w11, #0x581 // =1409
33+
movk w11, #0x5816, lsl #16
34+
dup v23.4s, w11
35+
movi v24.4s, #0x2b
36+
mov x3, #0x10 // =16
37+
38+
Lpoly_use_hint_88_loop:
39+
ldr q1, [x1, #0x10]
40+
ldr q2, [x1, #0x20]
41+
ldr q3, [x1, #0x30]
42+
ldr q0, [x1], #0x40
43+
ldr q5, [x2, #0x10]
44+
ldr q6, [x2, #0x20]
45+
ldr q7, [x2, #0x30]
46+
ldr q4, [x2], #0x40
47+
sqdmulh v17.4s, v1.4s, v23.4s
48+
srshr v17.4s, v17.4s, #0x11
49+
cmgt v25.4s, v1.4s, v21.4s
50+
mls v1.4s, v17.4s, v22.4s
51+
bic v17.16b, v17.16b, v25.16b
52+
add v1.4s, v1.4s, v25.4s
53+
cmle v1.4s, v1.4s, #0
54+
orr v1.4s, #0x1
55+
mla v17.4s, v1.4s, v5.4s
56+
cmgt v25.4s, v17.4s, v24.4s
57+
bic v17.16b, v17.16b, v25.16b
58+
umin v17.4s, v17.4s, v24.4s
59+
sqdmulh v18.4s, v2.4s, v23.4s
60+
srshr v18.4s, v18.4s, #0x11
61+
cmgt v25.4s, v2.4s, v21.4s
62+
mls v2.4s, v18.4s, v22.4s
63+
bic v18.16b, v18.16b, v25.16b
64+
add v2.4s, v2.4s, v25.4s
65+
cmle v2.4s, v2.4s, #0
66+
orr v2.4s, #0x1
67+
mla v18.4s, v2.4s, v6.4s
68+
cmgt v25.4s, v18.4s, v24.4s
69+
bic v18.16b, v18.16b, v25.16b
70+
umin v18.4s, v18.4s, v24.4s
71+
sqdmulh v19.4s, v3.4s, v23.4s
72+
srshr v19.4s, v19.4s, #0x11
73+
cmgt v25.4s, v3.4s, v21.4s
74+
mls v3.4s, v19.4s, v22.4s
75+
bic v19.16b, v19.16b, v25.16b
76+
add v3.4s, v3.4s, v25.4s
77+
cmle v3.4s, v3.4s, #0
78+
orr v3.4s, #0x1
79+
mla v19.4s, v3.4s, v7.4s
80+
cmgt v25.4s, v19.4s, v24.4s
81+
bic v19.16b, v19.16b, v25.16b
82+
umin v19.4s, v19.4s, v24.4s
83+
sqdmulh v16.4s, v0.4s, v23.4s
84+
srshr v16.4s, v16.4s, #0x11
85+
cmgt v25.4s, v0.4s, v21.4s
86+
mls v0.4s, v16.4s, v22.4s
87+
bic v16.16b, v16.16b, v25.16b
88+
add v0.4s, v0.4s, v25.4s
89+
cmle v0.4s, v0.4s, #0
90+
orr v0.4s, #0x1
91+
mla v16.4s, v0.4s, v4.4s
92+
cmgt v25.4s, v16.4s, v24.4s
93+
bic v16.16b, v16.16b, v25.16b
94+
umin v16.4s, v16.4s, v24.4s
95+
str q17, [x0, #0x10]
96+
str q18, [x0, #0x20]
97+
str q19, [x0, #0x30]
98+
str q16, [x0], #0x40
99+
subs x3, x3, #0x1
100+
b.ne Lpoly_use_hint_88_loop
101+
ret
102+
.cfi_endproc
103+
104+
#if defined(__ELF__)
105+
.section .note.GNU-stack,"",%progbits
106+
#endif

‎proofs/hol_light/aarch64/proofs/dump_bytecode.ml‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,14 @@ print_string "=== bytecode start: aarch64/mldsa/mldsa_poly_caddq.o ===\n";;
3030
print_literal_from_elf "aarch64/mldsa/mldsa_poly_caddq.o";;
3131
print_string "==== bytecode end =====================================\n\n";;
3232

33+
print_string "=== bytecode start: aarch64/mldsa/mldsa_poly_use_hint_32.o ===\n";;
34+
print_literal_from_elf "aarch64/mldsa/mldsa_poly_use_hint_32.o";;
35+
print_string "==== bytecode end =====================================\n\n";;
36+
37+
print_string "=== bytecode start: aarch64/mldsa/mldsa_poly_use_hint_88.o ===\n";;
38+
print_literal_from_elf "aarch64/mldsa/mldsa_poly_use_hint_88.o";;
39+
print_string "==== bytecode end =====================================\n\n";;
40+
3341
print_string "=== bytecode start: aarch64/mldsa/mldsa_poly_chknorm.o ===\n";;
3442
print_literal_from_elf "aarch64/mldsa/mldsa_poly_chknorm.o";;
3543
print_string "==== bytecode end =====================================\n\n";;

0 commit comments

Comments
 (0)