Skip to content

Commit

Permalink
Make symbolic simulation for equiv checking infer output of loads
Browse files Browse the repository at this point in the history 
This patch updates symbolic simulation tactics for equivalence checking
to infer the output of loads from assumptions if there is no directly
matching equality.

For example, if there is an assumption `read (memory :> bytes (ptr,8*n)) = a`
but nothing about `read (memory :> bytes64 (word_add (ptr,8*k)))`, it
tries to construct its output as `bigdigit a k` using `SIMPLE_ARITH_TAC`.
This helps remove boilerplate codes in proofs that manually construct
all equalities between 64-bit and 128-bit memory reads at known
locations.
This also reduces the sizes of assumptions, which may affect
positive results to proof checking times, but in fact caused slowdown to
larger equivalence checking tactics such as p256/p384's point
operations. For these ops, a separate flag disabling this feature is
set.

The main tactics are `MK_MEMORY_READ_EQ_BIGDIGIT_RULE` and
`DIGITIZE_MEMORY_READS`.
They construct equations involving the unseen memory reads and
`bigdigit`. They are passed to `ARM_N_STEP_TAC` (the `ARM_STEP'_TAC` in the
past; this renaming will be explained below), which are called 'auxiliary
memory read equations, and they are either `ASSUME_TAC`ed or passed to
the caller separately from other normal equations describing the actual
outputs of a simulated instruction.

On top of these updates, I also

- Renamed the tactics that are related to equivalence checking so that
  it does not have a punctuation mark but instead `_N` as a
  differentiating string from its original version. For example, the
  equivlaence checking version of `ARM_STEP_TAC` was `ARM_STEP'_TAC`,
  but now it is `ARM_N_STEP_TAC`. `_N` came from `ensures_n`. Some
  tactics are exception from this pattern, however.
- Added `approximate_input_output_regs` which gets the input and output register
  from a basic block. Input registers are registers that are read
  without written, and output registers are those written but not read
  later. This does not consider memory reads and writes. This will be used in my future patches.
- Extended `ENSURES2_WHILE_PAUP_TAC` so that its step counter needed to
  simulate the backedge is not just '1', but parameterically given in
  general.
- And many other minor changes and updates..!
  • Loading branch information
@aqjune-aws
aqjune-aws committed Nov 5, 2024
1 parent 4d00271 commit a79c97e
Show file tree
Hide file tree
Showing 14 changed files with 924 additions and 348 deletions.
40 changes: 16 additions & 24 deletions arm/proofs/bignum_montmul_p256_neon.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -226,15 +226,7 @@ let bignum_montmul_p256_interm1_ops:int list = [
];;

let bignum_montmul_p256_interm1_mc =
let charlist = List.concat_map
(fun op32 ->
[Char.chr (Int.logand op32 255);
Char.chr (Int.logand (Int.shift_right op32 8) 255);
Char.chr (Int.logand (Int.shift_right op32 16) 255);
Char.chr (Int.logand (Int.shift_right op32 24) 255)])
bignum_montmul_p256_interm1_ops in
let byte_list = Bytes.init (List.length charlist) (fun i -> List.nth charlist i) in
define_word_list "bignum_montmul_p256_interm1_mc" (term_of_bytes byte_list);;
define_mc_from_intlist "bignum_montmul_p256_interm1_mc" bignum_montmul_p256_interm1_ops;;

let BIGNUM_MONTMUL_P256_INTERM1_EXEC =
ARM_MK_EXEC_RULE bignum_montmul_p256_interm1_mc;;
Expand Down Expand Up @@ -264,7 +256,9 @@ let montmul_p256_eqout = new_definition
bignum_from_memory (z,4) s1 = a /\
bignum_from_memory (z,4) s1' = a)`;;

(* This diff is generated by tools/gen-actions.py. *)
(* This diff is generated by tools/gen-actions.py.
To get this diff you will need an 'original register name'
version of the bignum_montmul_p256_interm1_mc. *)
let actions = [
("equal", 0, 1, 0, 1);
("insert", 1, 1, 1, 2);
Expand All @@ -279,6 +273,10 @@ let actions = [
("equal", 51, 175, 80, 204)
];;

let actions = break_equal_loads actions
(snd BIGNUM_MONTMUL_P256_CORE_EXEC) 0x0
(snd BIGNUM_MONTMUL_P256_INTERM1_CORE_EXEC) 0x0;;

let equiv_goal1 = mk_equiv_statement_simple
`ALL (nonoverlapping (z:int64,8 * 4))
[(word pc:int64,LENGTH bignum_montmul_p256_core_mc);
Expand Down Expand Up @@ -313,17 +311,14 @@ let BIGNUM_MONTMUL_P256_CORE_EQUIV1 = prove(equiv_goal1,
REPEAT STRIP_TAC THEN
(** Initialize **)
EQUIV_INITIATE_TAC montmul_p256_eqin THEN
REPEAT (FIRST_X_ASSUM BIGNUM_EXPAND_AND_DIGITIZE_TAC) THEN
ASM_PROPAGATE_DIGIT_EQS_FROM_EXPANDED_BIGNUM_TAC THEN
(* necessary to run ldr qs *)
COMBINE_READ_BYTES64_PAIRS_TAC THEN
RULE_ASSUM_TAC (REWRITE_RULE[BIGNUM_FROM_MEMORY_BYTES]) THEN

(* Start *)
EQUIV_STEPS_TAC actions
BIGNUM_MONTMUL_P256_CORE_EXEC
BIGNUM_MONTMUL_P256_INTERM1_CORE_EXEC THEN

REPEAT_N 2 ENSURES_FINAL_STATE'_TAC THEN
REPEAT_N 2 ENSURES_N_FINAL_STATE_TAC THEN
(* Prove remaining clauses from the postcondition *)
ASM_REWRITE_TAC[] THEN
REPEAT CONJ_TAC THENL [
Expand Down Expand Up @@ -407,20 +402,17 @@ let BIGNUM_MONTMUL_P256_CORE_EQUIV2 = prove(
REPEAT STRIP_TAC THEN
(** Initialize **)
EQUIV_INITIATE_TAC montmul_p256_eqin THEN
REPEAT (FIRST_X_ASSUM BIGNUM_EXPAND_AND_DIGITIZE_TAC) THEN
ASM_PROPAGATE_DIGIT_EQS_FROM_EXPANDED_BIGNUM_TAC THEN
(* necessary to run ldr qs *)
COMBINE_READ_BYTES64_PAIRS_TAC THEN
RULE_ASSUM_TAC (REWRITE_RULE[BIGNUM_FROM_MEMORY_BYTES]) THEN

(* Left *)
ARM_STEPS'_AND_ABBREV_TAC BIGNUM_MONTMUL_P256_INTERM1_CORE_EXEC
(1--204) state_to_abbrevs THEN
ARM_N_STEPS_AND_ABBREV_TAC BIGNUM_MONTMUL_P256_INTERM1_CORE_EXEC
(1--(List.length inst_map)) state_to_abbrevs THEN

(* Right *)
ARM_STEPS'_AND_REWRITE_TAC BIGNUM_MONTMUL_P256_NEON_CORE_EXEC
(1--204) inst_map state_to_abbrevs THEN
ARM_N_STEPS_AND_REWRITE_TAC BIGNUM_MONTMUL_P256_NEON_CORE_EXEC
(1--(List.length inst_map)) inst_map state_to_abbrevs THEN

REPEAT_N 2 ENSURES_FINAL_STATE'_TAC THEN
REPEAT_N 2 ENSURES_N_FINAL_STATE_TAC THEN
(* Prove remaining clauses from the postcondition *)
ASM_REWRITE_TAC[] THEN
REPEAT CONJ_TAC THENL [
Expand Down
36 changes: 14 additions & 22 deletions arm/proofs/bignum_montmul_p384_neon.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -434,15 +434,7 @@ let bignum_montmul_p384_interm1_ops:int list = [
];;

let bignum_montmul_p384_interm1_mc =
let charlist = List.concat_map
(fun op32 ->
[Char.chr (Int.logand op32 255);
Char.chr (Int.logand (Int.shift_right op32 8) 255);
Char.chr (Int.logand (Int.shift_right op32 16) 255);
Char.chr (Int.logand (Int.shift_right op32 24) 255)])
bignum_montmul_p384_interm1_ops in
let byte_list = Bytes.init (List.length charlist) (fun i -> List.nth charlist i) in
define_word_list "bignum_montmul_p384_interm1_mc" (term_of_bytes byte_list);;
define_mc_from_intlist "bignum_montmul_p384_interm1_mc" bignum_montmul_p384_interm1_ops;;

let BIGNUM_MONTMUL_P384_INTERM1_EXEC =
ARM_MK_EXEC_RULE bignum_montmul_p384_interm1_mc;;
Expand Down Expand Up @@ -472,7 +464,9 @@ let montmul_p384_eqout = new_definition
bignum_from_memory (z,6) s1 = a /\
bignum_from_memory (z,6) s1' = a)`;;

(* This diff is generated by tools/gen-actions.py. *)
(* This diff is generated by tools/gen-actions.py.
To get this diff you will need an 'original register name'
version of the bignum_montmul_p384_interm1_mc. *)
let actions = [
("equal", 0, 1, 0, 1);
("insert", 1, 1, 1, 2);
Expand All @@ -487,6 +481,10 @@ let actions = [
("equal", 122, 377, 151, 406);
];;

let actions = break_equal_loads actions
(snd BIGNUM_MONTMUL_P384_CORE_EXEC) 0x0
(snd BIGNUM_MONTMUL_P384_INTERM1_CORE_EXEC) 0x0;;

let equiv_goal1 = mk_equiv_statement_simple
`ALL (nonoverlapping (z:int64,8 * 6))
[(word pc:int64,LENGTH bignum_montmul_p384_core_mc);
Expand Down Expand Up @@ -522,17 +520,14 @@ let BIGNUM_MONTMUL_P384_CORE_EQUIV1 = time prove(equiv_goal1,
REPEAT STRIP_TAC THEN
(** Initialize **)
EQUIV_INITIATE_TAC montmul_p384_eqin THEN
REPEAT (FIRST_X_ASSUM BIGNUM_EXPAND_AND_DIGITIZE_TAC) THEN
ASM_PROPAGATE_DIGIT_EQS_FROM_EXPANDED_BIGNUM_TAC THEN
(* necessary to run ldr qs *)
COMBINE_READ_BYTES64_PAIRS_TAC THEN
RULE_ASSUM_TAC (REWRITE_RULE[BIGNUM_FROM_MEMORY_BYTES]) THEN

(* Start *)
EQUIV_STEPS_TAC actions
BIGNUM_MONTMUL_P384_CORE_EXEC
BIGNUM_MONTMUL_P384_INTERM1_CORE_EXEC THEN

REPEAT_N 2 ENSURES_FINAL_STATE'_TAC THEN
REPEAT_N 2 ENSURES_N_FINAL_STATE_TAC THEN
(* Prove remaining clauses from the postcondition *)
ASM_REWRITE_TAC[] THEN
REPEAT CONJ_TAC THENL [
Expand Down Expand Up @@ -619,20 +614,17 @@ let BIGNUM_MONTMUL_P384_CORE_EQUIV2 = time prove(
REPEAT STRIP_TAC THEN
(** Initialize **)
EQUIV_INITIATE_TAC montmul_p384_eqin THEN
REPEAT (FIRST_X_ASSUM BIGNUM_EXPAND_AND_DIGITIZE_TAC) THEN
ASM_PROPAGATE_DIGIT_EQS_FROM_EXPANDED_BIGNUM_TAC THEN
(* necessary to run ldr qs *)
COMBINE_READ_BYTES64_PAIRS_TAC THEN
RULE_ASSUM_TAC(REWRITE_RULE[BIGNUM_FROM_MEMORY_BYTES]) THEN

(* Left *)
ARM_STEPS'_AND_ABBREV_TAC BIGNUM_MONTMUL_P384_INTERM1_CORE_EXEC
ARM_N_STEPS_AND_ABBREV_TAC BIGNUM_MONTMUL_P384_INTERM1_CORE_EXEC
(1--(List.length inst_map)) state_to_abbrevs THEN

(* Right *)
ARM_STEPS'_AND_REWRITE_TAC BIGNUM_MONTMUL_P384_NEON_CORE_EXEC
ARM_N_STEPS_AND_REWRITE_TAC BIGNUM_MONTMUL_P384_NEON_CORE_EXEC
(1--(List.length inst_map)) inst_map state_to_abbrevs THEN

REPEAT_N 2 ENSURES_FINAL_STATE'_TAC THEN
REPEAT_N 2 ENSURES_N_FINAL_STATE_TAC THEN
(* Prove remaining clauses from the postcondition *)
ASM_REWRITE_TAC[] THEN
REPEAT CONJ_TAC THENL [
Expand Down
36 changes: 15 additions & 21 deletions arm/proofs/bignum_montmul_p521_neon.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -688,15 +688,8 @@ let bignum_montmul_p521_interm1_ops:int list = [
];;

let bignum_montmul_p521_interm1_core_mc =
let charlist = List.concat_map
(fun op32 ->
[Char.chr (Int.logand op32 255);
Char.chr (Int.logand (Int.shift_right op32 8) 255);
Char.chr (Int.logand (Int.shift_right op32 16) 255);
Char.chr (Int.logand (Int.shift_right op32 24) 255)])
bignum_montmul_p521_interm1_ops in
let byte_list = Bytes.init (List.length charlist) (fun i -> List.nth charlist i) in
define_word_list "bignum_montmul_p521_interm1_core_mc" (term_of_bytes byte_list);;
define_mc_from_intlist "bignum_montmul_p521_interm1_core_mc"
bignum_montmul_p521_interm1_ops;;

let BIGNUM_MONTMUL_P521_INTERM1_CORE_EXEC =
ARM_MK_EXEC_RULE bignum_montmul_p521_interm1_core_mc;;
Expand Down Expand Up @@ -724,6 +717,9 @@ let montmul_p521_eqout = new_definition
bignum_from_memory (z,9) s1 = a /\
bignum_from_memory (z,9) s1' = a)`;;

(* This diff is generated by tools/gen-actions.py.
To get this diff you will need an 'original register name'
version of the bignum_montmul_p521_interm1_mc. *)
let actions = [
("equal", 0, 3, 0, 3);
("insert", 3, 3, 3, 5);
Expand All @@ -746,6 +742,10 @@ let actions = [
("equal", 148, 619, 197, 668);
];;

let actions = break_equal_loads actions
(snd BIGNUM_MONTMUL_P521_CORE_EXEC) 0x0
(snd BIGNUM_MONTMUL_P521_INTERM1_CORE_EXEC) 0x0;;

let equiv_goal1 = mk_equiv_statement_simple
`aligned 16 stackpointer /\
ALL (nonoverlapping (z:int64,8 * 9))
Expand Down Expand Up @@ -788,17 +788,14 @@ let BIGNUM_MONTMUL_P521_CORE_EQUIV1 = time prove(equiv_goal1,
REPEAT STRIP_TAC THEN
(** Initialize **)
EQUIV_INITIATE_TAC montmul_p521_eqin THEN
REPEAT (FIRST_X_ASSUM BIGNUM_EXPAND_AND_DIGITIZE_TAC) THEN
ASM_PROPAGATE_DIGIT_EQS_FROM_EXPANDED_BIGNUM_TAC THEN
(* necessary to run ldr qs *)
COMBINE_READ_BYTES64_PAIRS_TAC THEN
RULE_ASSUM_TAC (REWRITE_RULE[BIGNUM_FROM_MEMORY_BYTES]) THEN

(* Start *)
EQUIV_STEPS_TAC actions
BIGNUM_MONTMUL_P521_CORE_EXEC
BIGNUM_MONTMUL_P521_INTERM1_CORE_EXEC THEN

REPEAT_N 2 ENSURES_FINAL_STATE'_TAC THEN
REPEAT_N 2 ENSURES_N_FINAL_STATE_TAC THEN
(* Prove remaining clauses from the postcondition *)
ASM_REWRITE_TAC[] THEN
REPEAT CONJ_TAC THENL [
Expand Down Expand Up @@ -889,20 +886,17 @@ let BIGNUM_MONTMUL_P521_CORE_EQUIV2 = time prove(
REPEAT STRIP_TAC THEN
(** Initialize **)
EQUIV_INITIATE_TAC montmul_p521_eqin THEN
REPEAT (FIRST_X_ASSUM BIGNUM_EXPAND_AND_DIGITIZE_TAC) THEN
ASM_PROPAGATE_DIGIT_EQS_FROM_EXPANDED_BIGNUM_TAC THEN
(* necessary to run ldr qs *)
COMBINE_READ_BYTES64_PAIRS_TAC THEN
RULE_ASSUM_TAC (REWRITE_RULE[BIGNUM_FROM_MEMORY_BYTES]) THEN

(* Left *)
ARM_STEPS'_AND_ABBREV_TAC BIGNUM_MONTMUL_P521_INTERM1_CORE_EXEC
ARM_N_STEPS_AND_ABBREV_TAC BIGNUM_MONTMUL_P521_INTERM1_CORE_EXEC
(1--(List.length inst_map)) state_to_abbrevs THEN

(* Right *)
ARM_STEPS'_AND_REWRITE_TAC BIGNUM_MONTMUL_P521_NEON_CORE_EXEC
ARM_N_STEPS_AND_REWRITE_TAC BIGNUM_MONTMUL_P521_NEON_CORE_EXEC
(1--(List.length inst_map)) inst_map state_to_abbrevs THEN

REPEAT_N 2 ENSURES_FINAL_STATE'_TAC THEN
REPEAT_N 2 ENSURES_N_FINAL_STATE_TAC THEN
(* Prove remaining clauses from the postcondition *)
ASM_REWRITE_TAC[] THEN
REPEAT CONJ_TAC THENL [
Expand Down
49 changes: 24 additions & 25 deletions arm/proofs/bignum_montsqr_p256_neon.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -158,15 +158,7 @@ let bignum_montsqr_p256_interm1_ops:int list = [
];;

let bignum_montsqr_p256_interm1_mc =
let charlist = List.concat_map
(fun op32 ->
[Char.chr (Int.logand op32 255);
Char.chr (Int.logand (Int.shift_right op32 8) 255);
Char.chr (Int.logand (Int.shift_right op32 16) 255);
Char.chr (Int.logand (Int.shift_right op32 24) 255)])
bignum_montsqr_p256_interm1_ops in
let byte_list = Bytes.init (List.length charlist) (fun i -> List.nth charlist i) in
define_word_list "bignum_montsqr_p256_interm1_mc" (term_of_bytes byte_list);;
define_mc_from_intlist "bignum_montsqr_p256_interm1_mc" bignum_montsqr_p256_interm1_ops;;

let BIGNUM_MONTSQR_P256_INTERM1_EXEC =
ARM_MK_EXEC_RULE bignum_montsqr_p256_interm1_mc;;
Expand Down Expand Up @@ -196,7 +188,9 @@ let montsqr_p256_eqout = new_definition
bignum_from_memory (z,4) s1' = a)`;;

(* This diff is generated by tools/gen-actions.py, then splitted into two
lists to manually apply necessary equality rules on words. *)
lists to manually apply necessary equality rules on words.
To get this diff you will need an 'original register name'
version of the bignum_montsqr_p256_interm1_mc. *)
let actions = [
("equal", 0, 1, 0, 1);
("insert", 1, 1, 1, 2);
Expand All @@ -210,6 +204,15 @@ let actions2 = [
("equal", 42, 124, 54, 136);
];;


let actions = break_equal_loads actions
(snd BIGNUM_MONTSQR_P256_CORE_EXEC) 0x0
(snd BIGNUM_MONTSQR_P256_INTERM1_CORE_EXEC) 0x0;;

let actions2 = break_equal_loads actions2
(snd BIGNUM_MONTSQR_P256_CORE_EXEC) 0x0
(snd BIGNUM_MONTSQR_P256_INTERM1_CORE_EXEC) 0x0;;

let equiv_goal1 = mk_equiv_statement_simple
`ALL (nonoverlapping (z:int64,8 * 4))
[(word pc:int64,LENGTH bignum_montsqr_p256_core_mc);
Expand Down Expand Up @@ -343,10 +346,7 @@ let BIGNUM_MONTSQR_P256_CORE_EQUIV1 = time prove(equiv_goal1,
REPEAT STRIP_TAC THEN
(** Initialize **)
EQUIV_INITIATE_TAC montsqr_p256_eqin THEN
REPEAT (FIRST_X_ASSUM BIGNUM_EXPAND_AND_DIGITIZE_TAC) THEN
ASM_PROPAGATE_DIGIT_EQS_FROM_EXPANDED_BIGNUM_TAC THEN
(* necessary to run ldr qs *)
COMBINE_READ_BYTES64_PAIRS_TAC THEN
RULE_ASSUM_TAC (REWRITE_RULE[BIGNUM_FROM_MEMORY_BYTES]) THEN

(* Start *)
EQUIV_STEPS_TAC actions
Expand Down Expand Up @@ -376,7 +376,7 @@ let BIGNUM_MONTSQR_P256_CORE_EQUIV1 = time prove(equiv_goal1,
BIGNUM_MONTSQR_P256_CORE_EXEC
BIGNUM_MONTSQR_P256_INTERM1_CORE_EXEC THEN

REPEAT_N 2 ENSURES_FINAL_STATE'_TAC THEN
REPEAT_N 2 ENSURES_N_FINAL_STATE_TAC THEN
(* Prove remaining clauses from the postcondition *)
ASM_REWRITE_TAC[] THEN
REPEAT CONJ_TAC THENL [
Expand Down Expand Up @@ -438,13 +438,13 @@ let equiv_goal2 = mk_equiv_statement_simple
MAYCHANGE [memory :> bytes(z,8 * 4)] ,,
MAYCHANGE SOME_FLAGS`;;

(* Line numbers from bignum_montmul_p256_neon_core_mc (the fully optimized
prog.) to bignum_montmul_p256_interm1_core_mc (the intermediate prog.)
(* Line numbers from bignum_montsqr_p256_neon_core_mc (the fully optimized
prog.) to bignum_montsqr_p256_interm1_core_mc (the intermediate prog.)
The script that prints this map is being privately maintained by aqjune-aws.
This map can be also printed from the instruction map of SLOTHY's output, but
aqjune-aws does not have the converter. *)
let inst_map = [
5;1;4;2;3;9;8;24;47;6;10;49;56;55;12;7;11;46;50;28;23;15;58;57;14;13;59;16;60;63;17;26;18;48;51;19;20;21;30;52;22;25;32;62;27;29;31;33;34;53;61;35;38;68;36;40;37;39;41;42;54;43;116;44;65;45;66;67;69;64;115;70;71;72;73;74;108;75;76;112;77;78;79;80;81;82;83;106;84;90;85;88;109;86;124;87;117;118;127;119;89;91;92;93;97;99;94;95;96;98;100;101;102;103;104;105;107;110;111;113;114;120;121;122;123;125;126;128;129;130;131;133;134;132;136;135;137
5;1;4;2;3;9;8;24;47;6;10;49;56;55;12;7;11;46;50;28;23;15;58;57;14;13;59;16;60;63;17;26;18;48;51;19;20;21;30;52;22;25;32;62;27;29;31;33;34;53;61;35;38;68;36;40;37;39;41;42;54;43;116;44;65;45;66;67;69;64;115;70;71;72;73;74;108;75;76;112;77;78;79;80;81;82;83;106;84;90;85;88;109;86;124;87;117;118;127;119;89;91;92;93;97;99;94;95;96;98;100;101;102;103;104;105;107;110;111;113;114;120;121;122;123;125;126;128;129;130;131;133;134;132;136;135
];;

(* (state number, (equation, fresh var)) *)
Expand All @@ -460,18 +460,17 @@ let BIGNUM_MONTSQR_P256_CORE_EQUIV2 = prove(
REPEAT STRIP_TAC THEN
(** Initialize **)
EQUIV_INITIATE_TAC montsqr_p256_eqin THEN
REPEAT (FIRST_X_ASSUM BIGNUM_EXPAND_AND_DIGITIZE_TAC) THEN
ASM_PROPAGATE_DIGIT_EQS_FROM_EXPANDED_BIGNUM_TAC THEN
(* necessary to run ldr qs *)
COMBINE_READ_BYTES64_PAIRS_TAC THEN
RULE_ASSUM_TAC (REWRITE_RULE[BIGNUM_FROM_MEMORY_BYTES]) THEN

(* Left *)
ARM_STEPS'_AND_ABBREV_TAC BIGNUM_MONTSQR_P256_INTERM1_CORE_EXEC (1--136) state_to_abbrevs THEN
ARM_N_STEPS_AND_ABBREV_TAC BIGNUM_MONTSQR_P256_INTERM1_CORE_EXEC
(1--(List.length inst_map)) state_to_abbrevs THEN

(* Right *)
ARM_STEPS'_AND_REWRITE_TAC BIGNUM_MONTSQR_P256_NEON_CORE_EXEC (1--136) inst_map state_to_abbrevs THEN
ARM_N_STEPS_AND_REWRITE_TAC BIGNUM_MONTSQR_P256_NEON_CORE_EXEC
(1--(List.length inst_map)) inst_map state_to_abbrevs THEN

REPEAT_N 2 ENSURES_FINAL_STATE'_TAC THEN
REPEAT_N 2 ENSURES_N_FINAL_STATE_TAC THEN
(* Prove remaining clauses from the postcondition *)
ASM_REWRITE_TAC[] THEN
REPEAT CONJ_TAC THENL [
Expand Down
Loading

0 comments on commit a79c97e

Please sign in to comment.