Skip to content

Commit 3b81be6

Browse files
aqjune-awsaqjune-aws
committed
Add tutorial for Arm
This patch adds tutorial for Arm. The examples are copied from my repository (https://github.com/aqjune/hol-light-materials/). :)
1 parent 57953c2 commit 3b81be6

28 files changed

+1265
-5
lines changed

‎README.md

+2
Original file line numberDiff line numberDiff line change
@@ -322,6 +322,8 @@ memory.
322322

323323
To perform the formal proof for a particular function, you will need to install
324324
the latest version of [HOL Light](https://github.com/jrh13/hol-light/).
325+
The OPAM version might not work because it does not contain sufficiently recent
326+
libraries.
325327
To install HOL Light, please follow its
326328
[README](https://github.com/jrh13/hol-light/blob/master/README) instruction.
327329
After installation, set the `HOLDIR` environment variable to the path of

‎arm/Makefile

+19
Original file line numberDiff line numberDiff line change
@@ -389,6 +389,12 @@ UNOPT_OBJ = p256/unopt/p256_montjadd.o \
389389

390390
OBJ = $(POINT_OBJ) $(BIGNUM_OBJ)
391391

392+
# Tutorial assembly files
393+
394+
TUTORIAL_PROOFS = $(wildcard tutorial/*.ml)
395+
396+
TUTORIAL_OBJ = $(TUTORIAL_PROOFS:.ml=.o) tutorial/rel_loop2.o tutorial/rel_simp2.o tutorial/rel_veceq2.o
397+
392398
# According to
393399
# https://developer.apple.com/documentation/xcode/writing-arm64-code-for-apple-platforms,
394400
# x18 should not be used for Apple platforms. Check this using grep.
@@ -419,6 +425,8 @@ HOLLIGHT:=$(HOLDIR)/hol.sh
419425

420426
PROOF_BINS = $(OBJ:.o=.native)
421427
PROOF_LOGS = $(OBJ:.o=.correct)
428+
TUTORIAL_PROOF_BINS = $(TUTORIAL_PROOFS:.ml=.native)
429+
TUTORIAL_PROOF_LOGS = $(TUTORIAL_PROOFS:.ml=.correct)
422430

423431
# Build precompiled native binaries of HOL Light proofs
424432

@@ -477,13 +485,24 @@ p521/p521_jscalarmul_alt.native: p521/bignum_mod_n521_9.native
477485
sm2/sm2_montjscalarmul.native: sm2/sm2_montjadd.native sm2/sm2_montjdouble.native
478486
sm2/sm2_montjscalarmul_alt.native: sm2/sm2_montjadd_alt.native sm2/sm2_montjdouble_alt.native
479487

488+
# Tutorial
489+
490+
.SECONDEXPANSION:
491+
tutorial/%.native: tutorial/%.ml tutorial/%.o ; ../tools/build-proof.sh "$<" "$(HOLLIGHT)" "$@"
492+
# Additional dependencies on .o files
493+
tutorial/rel_loop.native: tutorial/rel_loop2.o
494+
tutorial/rel_simp.native: tutorial/rel_simp2.o
495+
tutorial/rel_veceq.native: tutorial/rel_veceq2.o
496+
480497

481498
unopt: $(UNOPT_OBJ)
482499

483500
build_proofs: $(UNOPT_OBJ) $(PROOF_BINS);
501+
build_tutorial: $(TUTORIAL_OBJ) $(TUTORIAL_PROOF_BINS);
484502
run_proofs: build_proofs $(PROOF_LOGS);
485503

486504
proofs: run_proofs ; ../tools/count-proofs.sh .
505+
tutorial: build_tutorial $(TUTORIAL_PROOF_LOGS);
487506

488507
# Always run sematest regardless of dependency check
489508
FORCE: ;

‎arm/tutorial/README.md

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
# Tutorials for s2n-bignum
2+
3+
This directory includes examples for verifying Arm programs using s2n-bignum
4+
and HOL Light.
5+
6+
### Unary reasoning
7+
8+
1. `simple.ml`: Verifying a simple arithmetic property of a linear program.
9+
2. `sequence.ml`: Verifying a program by splitting into smaller chunks.
10+
3. `branch.ml`: Verifying a program that has a conditional branch.
11+
4. `memory.ml`: Verifying a program that manipulates a memory.
12+
5. `loop.ml`: Verifying a program that has a simple loop.
13+
6. `bignum.ml`: Writing a specification of a program dealing with big numbers & proving it.
14+
15+
### Relational reasoning
16+
17+
1. `rel_simp.ml`: Proving equivalence of two simple programs.
18+
2. `rel_loop.ml`: Proving equivalence of two simple loops.
19+
3. `rel_veceq.ml`: Proving equivalence of scalar vs. vectorized 128x128->256-bit squaring.

‎arm/tutorial/bignum.S

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
ldp x2, x3, [x0]
2+
ldp x4, x5, [x1]
3+
cmp x2, x4
4+
bne bb_false
5+
cmp x3, x5
6+
bne bb_false
7+
mov x0, #1
8+
ret
9+
bb_false:
10+
mov x0, xzr
11+
ret

‎arm/tutorial/bignum.ml

+158
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,158 @@
1+
(*
2+
* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
* SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0
4+
*)
5+
6+
(******************************************************************************
7+
An example that shows how to describe big numbers in a specification.
8+
******************************************************************************)
9+
10+
needs "arm/proofs/base.ml";;
11+
12+
(* Let's prove that the following program
13+
14+
0: a9400c02 ldp x2, x3, [x0]
15+
4: a9401424 ldp x4, x5, [x1]
16+
8: eb04005f cmp x2, x4
17+
c: 540000a1 b.ne 20 <bb_false> // b.any
18+
10: eb05007f cmp x3, x5
19+
14: 54000061 b.ne 20 <bb_false> // b.any
20+
18: d2800020 mov x0, #0x1
21+
1c: d65f03c0 ret
22+
23+
0000000000000020 <bb_false>:
24+
20: aa1f03e0 mov x0, xzr
25+
24: d65f03c0 ret
26+
27+
.. returns 1 to x0 if a pair of 16-byte integers at buffer x0 and x1
28+
are equal, 0 otherwise.
29+
Since this example uses 128 bit integers, we will use 'bignum_from_memory'
30+
which will state that reading a memory buffer of a specified word number will
31+
return some large natural number.
32+
*)
33+
let bignum_mc = define_assert_from_elf "bignum_mc" "arm/tutorial/bignum.o" [
34+
0xa9400c02; (* arm_LDP X2 X3 X0 (Immediate_Offset (iword (&0))) *)
35+
0xa9401424; (* arm_LDP X4 X5 X1 (Immediate_Offset (iword (&0))) *)
36+
0xeb04005f; (* arm_CMP X2 X4 *)
37+
0x540000a1; (* arm_BNE (word 20) *)
38+
0xeb05007f; (* arm_CMP X3 X5 *)
39+
0x54000061; (* arm_BNE (word 12) *)
40+
0xd2800020; (* arm_MOV X0 (rvalue (word 1)) *)
41+
0xd65f03c0; (* arm_RET X30 *)
42+
0xaa1f03e0; (* arm_MOV X0 XZR *)
43+
0xd65f03c0 (* arm_RET X30 *)
44+
];;
45+
46+
(*
47+
You can get the above OCaml list data structure from
48+
`print_literal_from_elf "<.o file>"` or
49+
`save_literal_from_elf "<out.txt>" "<.o file>"`.
50+
*)
51+
52+
(* ARM_MK_EXEC_RULE decodes the byte sequence into conjunction of
53+
equalities between the bytes and instructions. *)
54+
let EXEC = ARM_MK_EXEC_RULE bignum_mc;;
55+
56+
let BIGNUM_SPEC = prove(
57+
`forall pc retpc loc0 loc1 a b.
58+
ensures arm
59+
// Precondition
60+
(\s. aligned_bytes_loaded s (word pc) bignum_mc /\
61+
read PC s = word pc /\
62+
read X30 s = word retpc /\
63+
read X0 s = word loc0 /\
64+
read X1 s = word loc1 /\
65+
// Read 2 words (=128bits) at loc0. It is equivalent to num a.
66+
// Alternatively, this kind of condition can be written using
67+
// bignum_of_wordlist which takes a list of 64-bit words.
68+
bignum_from_memory (word loc0,2) s = a /\
69+
// Read 2 words (=128bits) at loc1. It is equivalent to num b.
70+
bignum_from_memory (word loc1,2) s = b
71+
)
72+
// Postcondition
73+
(\s. read PC s = word retpc /\
74+
read X0 s = word (if a = b then 1 else 0))
75+
// Registers (and memory locations) that may change after execution
76+
(MAYCHANGE [PC;X0;X2;X3;X4;X5] ,, MAYCHANGE SOME_FLAGS)`,
77+
78+
REPEAT STRIP_TAC THEN
79+
(* Convert 'bignum_from_memory' into 'memory :> bytes (..)'.
80+
Also, expand SOME_FLAGS *)
81+
REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES;SOME_FLAGS] THEN
82+
(* Start symbolic execution with state 's0' *)
83+
ENSURES_INIT_TAC "s0" THEN
84+
(* Split the memory :> bytes .. into a pair of memory :> bytes64.
85+
This is necessary to successfully encode the symbolic result of ldps. *)
86+
BIGNUM_DIGITIZE_TAC "a_" `read (memory :> bytes (word loc0,8 * 2)) s0` THEN
87+
BIGNUM_DIGITIZE_TAC "b_" `read (memory :> bytes (word loc1,8 * 2)) s0` THEN
88+
89+
(* Symbolically run two ldp instructions *)
90+
ARM_STEPS_TAC EXEC (1--2) THEN
91+
(* Until first 'bne' *)
92+
ARM_STEPS_TAC EXEC (3--4) THEN
93+
94+
(* Recognize the if condition and create two subgoals . *)
95+
FIRST_X_ASSUM MP_TAC THEN
96+
COND_CASES_TAC THENL [
97+
(* The low 64 bits of a and b are different. *)
98+
STRIP_TAC THEN
99+
ARM_STEPS_TAC EXEC (5--6) THEN
100+
(* Returned; Finalize symbolic execution. *)
101+
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
102+
(* From `~(val (word_sub a_0 b_0) = 0)` and `val a_0 + 2 EXP 64 * val a_1 = a`,
103+
and `val b_0 + 2 EXP 64 * val b_1 = b`,
104+
prove `~(a = b)`. *)
105+
SUBGOAL_THEN `~(a:num = b)` (fun th -> REWRITE_TAC[th]) THEN
106+
MAP_EVERY EXPAND_TAC ["a";"b"] THEN
107+
(* VAL_WORD_SUB_EQ_0: |- !x y. val (word_sub x y) = 0 <=> val x = val y) *)
108+
RULE_ASSUM_TAC (REWRITE_RULE [VAL_WORD_SUB_EQ_0]) THEN
109+
(* EQ_DIVMOD: |- !p m n. m DIV p = n DIV p /\ m MOD p = n MOD p <=> m = n *)
110+
ONCE_REWRITE_TAC[SPEC `2 EXP 64` (GSYM EQ_DIVMOD)] THEN
111+
(* The first '.. DIV .. = .. DIV ..' part is irelevant. *)
112+
MATCH_MP_TAC (TAUT (`~Q ==> ~(P /\ Q)`)) THEN
113+
(* Simplfy! *)
114+
SIMP_TAC[MOD_MULT_ADD;VAL_BOUND_64;ARITH_RULE`~(2 EXP 64 = 0)`] THEN
115+
ASM_SIMP_TAC[MOD_LT;VAL_BOUND_64];
116+
117+
ALL_TAC
118+
] THEN
119+
120+
(* The low 64 bits of a and b are equivalent. *)
121+
(* Until the second 'bne' *)
122+
STRIP_TAC THEN
123+
ARM_STEPS_TAC EXEC (5--6) THEN
124+
125+
(* Recognize the if condition and create two subgoals . *)
126+
FIRST_X_ASSUM MP_TAC THEN
127+
COND_CASES_TAC THENL [
128+
(* The high 64 bits of a and b are different. *)
129+
STRIP_TAC THEN
130+
ARM_STEPS_TAC EXEC (7--8) THEN
131+
(* Returned; Finalize symbolic execution. *)
132+
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
133+
(* Proof pattern is similar to the first branch case *)
134+
SUBGOAL_THEN `~(a:num = b)` (fun th -> REWRITE_TAC[th]) THEN
135+
MAP_EVERY EXPAND_TAC ["a";"b"] THEN
136+
(* VAL_WORD_SUB_EQ_0: |- !x y. val (word_sub x y) = 0 <=> val x = val y) *)
137+
RULE_ASSUM_TAC (REWRITE_RULE [VAL_WORD_SUB_EQ_0]) THEN
138+
(* EQ_DIVMOD: |- !p m n. m DIV p = n DIV p /\ m MOD p = n MOD p <=> m = n *)
139+
ONCE_REWRITE_TAC[SPEC `2 EXP 64` (GSYM EQ_DIVMOD)] THEN
140+
(* The second '.. MOD .. = .. MOD ..' part is irelevant. *)
141+
MATCH_MP_TAC (TAUT (`~P ==> ~(P /\ Q)`)) THEN
142+
(* Simplfy! *)
143+
SIMP_TAC[DIV_MULT_ADD;VAL_BOUND_64;ARITH_RULE`~(2 EXP 64 = 0)`] THEN
144+
ASM_SIMP_TAC[DIV_LT;VAL_BOUND_64;ADD_CLAUSES];
145+
146+
ALL_TAC
147+
] THEN
148+
149+
(* Both limbs are equivalent! *)
150+
STRIP_TAC THEN
151+
ARM_STEPS_TAC EXEC (7--8) THEN
152+
(* Try to prove the postcondition and frame as much as possible *)
153+
ENSURES_FINAL_STATE_TAC THEN
154+
(* Use ASM_REWRITE_TAC[] to rewrite the goal using equalities in assumptions. *)
155+
ASM_REWRITE_TAC[] THEN
156+
SUBGOAL_THEN `(a:num = b)` (fun th -> REWRITE_TAC[th]) THEN
157+
RULE_ASSUM_TAC (REWRITE_RULE [VAL_WORD_SUB_EQ_0]) THEN
158+
ASM_ARITH_TAC);;

‎arm/tutorial/branch.S

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
cmp x1, x2
2+
b.hi BB2
3+
mov x0, x2
4+
ret
5+
BB2:
6+
mov x0, x1
7+
ret

‎arm/tutorial/branch.ml

+117
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,117 @@
1+
(*
2+
* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
* SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0
4+
*)
5+
6+
(******************************************************************************
7+
Prove a property of a simple program that has a conditional branch.
8+
******************************************************************************)
9+
10+
needs "arm/proofs/base.ml";;
11+
12+
(* The following program
13+
0: eb02003f cmp x1, x2
14+
4: 54000068 b.hi 10 <BB2>
15+
8: aa0203e0 mov x0, x2
16+
c: d65f03c0 ret
17+
18+
0000000000000010 <BB2>:
19+
10: aa0103e0 mov x0, x1
20+
14: d65f03c0 ret
21+
22+
.. copies max(x1,x2) to x0 and returns to the caller.
23+
Let's prove this property.
24+
*)
25+
26+
let branch_mc = new_definition `branch_mc = [
27+
word 0x3f; word 0x00; word 0x02; word 0xeb; // cmp x1, x2
28+
word 0x68; word 0x00; word 0x00; word 0x54; // b.hi 10 <BB2>
29+
30+
word 0xe0; word 0x03; word 0x02; word 0xaa; // mov x0, x2
31+
word 0xc0; word 0x03; word 0x5f; word 0xd6; // ret
32+
33+
// BB2:
34+
word 0xe0; word 0x03; word 0x01; word 0xaa; // mov x0, x1
35+
word 0xc0; word 0x03; word 0x5f; word 0xd6 // ret
36+
]:((8)word)list`;;
37+
38+
let EXEC = ARM_MK_EXEC_RULE branch_mc;;
39+
40+
let branch_SPEC = prove(
41+
`forall pc pcret a b.
42+
ensures arm
43+
// Precondition
44+
(\s. aligned_bytes_loaded s (word pc) branch_mc /\
45+
read X30 s = word pcret /\
46+
read PC s = word pc /\
47+
read X1 s = word a /\
48+
read X2 s = word b)
49+
// Postcondition
50+
(\s. read PC s = word pcret /\
51+
read X0 s = word_umax (word a) (word b))
52+
// Registers (and memory locations) that may change after execution.
53+
// ',,' is composition of relations.
54+
(MAYCHANGE [PC;X0] ,, MAYCHANGE SOME_FLAGS)`,
55+
(* Strips the outermost universal quantifier from the conclusion of a goal *)
56+
REPEAT STRIP_TAC THEN
57+
(* ENSURES_FINAL_STATE_TAC does not understand SOME_FLAGS in MAYCHANGE. Let's
58+
unfold this in advance. *)
59+
REWRITE_TAC [SOME_FLAGS] THEN
60+
61+
(* Let's do symbolic execution until it hits the branch instruction. *)
62+
ENSURES_INIT_TAC "s0" THEN
63+
ARM_STEPS_TAC EXEC (1--2) THEN
64+
65+
(* The PC has the following symbolic expression:
66+
`read PC s2 =
67+
(if val (word b) <= val (word a) /\
68+
~(val (word_sub (word a) (word b)) = 0)
69+
then word (pc + 16)
70+
else word (pc + 8))`
71+
Let's do case analysis on the condition of this if expression.
72+
73+
First, move this assumption to the antecendent of the goal so the goal
74+
becomes:
75+
(read PC s2 = ...) ==> eventually arm ...
76+
*)
77+
FIRST_X_ASSUM MP_TAC THEN
78+
79+
(* Recognize the if condition and create two subgoals . *)
80+
COND_CASES_TAC THENL [
81+
(** Case 1: if the branch was taken! **)
82+
(* Let's name the hypothesis first. *)
83+
POP_ASSUM (LABEL_TAC "Hcond") THEN
84+
DISCH_TAC THEN
85+
86+
(* Do symbolic execution on the remaining two insts. *)
87+
ARM_STEPS_TAC EXEC (3--4) THEN
88+
ENSURES_FINAL_STATE_TAC THEN
89+
ASM_REWRITE_TAC[] THEN
90+
91+
(* The remaining goal is `word a = word (MAX a b).` *)
92+
REMOVE_THEN "Hcond" MP_TAC THEN
93+
(* WORD_UMAX: `!x y. word_umax x y = (if val x <= val y then y else x)`
94+
VAL_WORD_SUB_EQ_0: `!x y. val (word_sub x y) = 0 <=> val x = val y` *)
95+
REWRITE_TAC[WORD_UMAX;VAL_WORD_SUB_EQ_0] THEN
96+
(* Let ARITH_TAC deal with reasoning on relational equations. *)
97+
ARITH_TAC;
98+
99+
100+
(** Case 2: if the branch was not taken! **)
101+
(* Let's name the hypothesis first. *)
102+
POP_ASSUM (LABEL_TAC "Hcond") THEN
103+
DISCH_TAC THEN
104+
105+
(* Do symbolic execution on the remaining two insts. *)
106+
ARM_STEPS_TAC EXEC (3--4) THEN
107+
ENSURES_FINAL_STATE_TAC THEN
108+
ASM_REWRITE_TAC[] THEN
109+
110+
(* The remaining goal is `word b = word (MAX a b).` *)
111+
REMOVE_THEN "Hcond" MP_TAC THEN
112+
(* WORD_UMAX: `!x y. word_umax x y = (if val x <= val y then y else x)`
113+
VAL_WORD_SUB_EQ_0: `!x y. val (word_sub x y) = 0 <=> val x = val y` *)
114+
REWRITE_TAC[WORD_UMAX;VAL_WORD_SUB_EQ_0] THEN
115+
(* Let ARITH_TAC deal with reasoning on relational equations. *)
116+
ARITH_TAC;
117+
]);;

‎arm/tutorial/loop.S

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
mov x1, xzr
2+
mov x0, xzr
3+
4+
loop:
5+
add x1, x1, #1
6+
add x0, x0, #2
7+
cmp x1, #10
8+
bne loop
9+
10+
ret

0 commit comments

Comments
 (0)