Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add microarchitectural events for Arm, bump HOL Light version #195

Open
wants to merge 5 commits into
base: main
Choose a base branch
from
+1,160 −887
Open

Add microarchitectural events for Arm, bump HOL Light version #195

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
9edb727
Add an observable microarchitectural event for Arm
aqjune-aws Feb 16, 2025
51024f7
use sed to systematically attach MAYCHANGE [event] after MAYCHANGE SO…
aqjune-aws Feb 21, 2025
c67e415
Manually edit the remaining failures
aqjune-aws Feb 21, 2025
df2e60f
Bump HOL Light commit hash, use the upstreamed check_axioms
aqjune-aws Feb 16, 2025
2d24553
Resolve possible slowdowns in ARM decoder
aqjune-aws Feb 28, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
5 changes: 4 additions & 1 deletion arm/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -498,7 +498,10 @@ tutorial/rel_reordertac.native: tutorial/rel_reordertac2.o

unopt: $(UNOPT_OBJ)

build_proofs: $(UNOPT_OBJ) $(PROOF_BINS);
build_proofs: $(UNOPT_OBJ) $(PROOF_BINS)
# Conservatively check that there is no redefinition of "check_axioms"
# '-I' excludes binary files (*.native).
! grep -RI "check_axioms" . ../common/ --exclude="Makefile"
build_tutorial: $(TUTORIAL_OBJ) $(TUTORIAL_PROOF_BINS);
run_proofs: build_proofs $(PROOF_LOGS);

Expand Down
6 changes: 6 additions & 0 deletions arm/proofs/arm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -410,6 +410,12 @@ let is_read_pc t =
| Comb (Comb (Const ("read", _), Const ("PC", _)), _) -> true
| _ -> false;;

(* returns true if t is `read events <state>`. *)
let is_read_events t =
match t with
| Comb (Comb (Const ("read", _), Const ("events", _)), _) -> true
| _ -> false;;

(*** decode_ths is an array from int offset i to
*** Some `|- !s pc. aligned_bytes_loaded s pc *_mc
*** ==> arm_decode s (word (pc+i)) (..inst..)`
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_add.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ let BIGNUM_ADD_CORRECT = prove
bignum_from_memory (z,val p) s =
lowdigits a (val p) + lowdigits b (val p))
(MAYCHANGE [PC; X0; X2; X4; X6; X7; X8] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,val p)])`,
W64_GEN_TAC `p:num` THEN X_GEN_TAC `z:int64` THEN
W64_GEN_TAC `m:num` THEN MAP_EVERY X_GEN_TAC [`x:int64`; `a:num`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_add_p25519.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ let BIGNUM_ADD_P25519_CORRECT = time prove
(m < p_25519 /\ n < p_25519
==> bignum_from_memory (z,4) s = (m + n) MOD p_25519))
(MAYCHANGE [PC; X3; X4; X5; X6; X7; X8; X9; X10] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,4)])`,
MAP_EVERY X_GEN_TAC
[`z:int64`; `x:int64`; `y:int64`; `m:num`; `n:num`; `pc:num`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_add_p256.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ let BIGNUM_ADD_P256_CORRECT = time prove
(m < p_256 /\ n < p_256
==> bignum_from_memory (z,4) s = (m + n) MOD p_256))
(MAYCHANGE [PC; X3; X4; X5; X6; X7; X8; X9; X10; X11] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,4)])`,
MAP_EVERY X_GEN_TAC
[`z:int64`; `x:int64`; `y:int64`; `m:num`; `n:num`; `pc:num`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_add_p256k1.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ let BIGNUM_ADD_P256K1_CORRECT = time prove
(m < p_256k1 /\ n < p_256k1
==> bignum_from_memory (z,4) s = (m + n) MOD p_256k1))
(MAYCHANGE [PC; X3; X4; X5; X6; X7; X8; X9] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,4)])`,
MAP_EVERY X_GEN_TAC
[`z:int64`; `x:int64`; `y:int64`; `m:num`; `n:num`; `pc:num`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_add_p384.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ let BIGNUM_ADD_P384_CORRECT = time prove
(m < p_384 /\ n < p_384
==> bignum_from_memory (z,6) s = (m + n) MOD p_384))
(MAYCHANGE [PC; X3; X4; X5; X6; X7; X8; X9; X10] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,6)])`,
MAP_EVERY X_GEN_TAC
[`z:int64`; `x:int64`; `y:int64`; `m:num`; `n:num`; `pc:num`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_add_p521.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ let BIGNUM_ADD_P521_CORRECT = time prove
(m < p_521 /\ n < p_521
==> bignum_from_memory (z,9) s = (m + n) MOD p_521))
(MAYCHANGE [PC; X3; X4; X5; X6; X7; X8; X9; X10; X11; X12; X13] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,9)])`,
MAP_EVERY X_GEN_TAC
[`z:int64`; `x:int64`; `y:int64`; `m:num`; `n:num`; `pc:num`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_add_sm2.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ let BIGNUM_ADD_SM2_CORRECT = time prove
(m < p_sm2 /\ n < p_sm2
==> bignum_from_memory (z,4) s = (m + n) MOD p_sm2))
(MAYCHANGE [PC; X3; X4; X5; X6; X7; X8; X9; X10; X11] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,4)])`,
MAP_EVERY X_GEN_TAC
[`z:int64`; `x:int64`; `y:int64`; `m:num`; `n:num`; `pc:num`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_amontifier.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -301,7 +301,7 @@ let BIGNUM_AMONTIFIER_CORRECT = time prove
(MAYCHANGE [PC; X4; X5; X6; X7; X8; X9; X10; X11] ,,
MAYCHANGE [memory :> bytes(z,8 * val k);
memory :> bytes(t,8 * val k)] ,,
MAYCHANGE SOME_FLAGS)`,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events])`,
W64_GEN_TAC `k:num` THEN
MAP_EVERY X_GEN_TAC
[`z:int64`; `mm:int64`; `t:int64`; `m:num`; `pc:num`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_amontmul.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ let BIGNUM_AMONTMUL_CORRECT = time prove
inverse_mod n (2 EXP (64 * val k)) * a * b) (mod n)))
(MAYCHANGE [PC; X5; X6; X7; X8; X9; X10; X11; X12; X13; X14] ,,
MAYCHANGE [memory :> bytes(z,8 * val k)] ,,
MAYCHANGE SOME_FLAGS)`,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events])`,
W64_GEN_TAC `k:num` THEN
MAP_EVERY X_GEN_TAC [`z:int64`; `x:int64`; `y:int64`; `m:int64`] THEN
MAP_EVERY X_GEN_TAC [`a:num`; `b:num`; `n:num`; `pc:num`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_amontredc.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -142,7 +142,7 @@ let BIGNUM_AMONTREDC_CORRECT = time prove
lowdigits a (val k + val p)) (mod n)))
(MAYCHANGE [PC; X6; X7; X8; X9; X10; X11; X12; X13; X14] ,,
MAYCHANGE [memory :> bytes(z,8 * val k)] ,,
MAYCHANGE SOME_FLAGS)`,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events])`,
W64_GEN_TAC `k:num` THEN X_GEN_TAC `z:int64` THEN
W64_GEN_TAC `nx:num` THEN X_GEN_TAC `x:int64` THEN
X_GEN_TAC `m:int64` THEN W64_GEN_TAC `p:num` THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_amontsqr.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,7 +138,7 @@ let BIGNUM_AMONTSQR_CORRECT = time prove
inverse_mod n (2 EXP (64 * val k)) * a EXP 2) (mod n)))
(MAYCHANGE [PC; X4; X5; X6; X7; X8; X9; X10; X11; X12; X13] ,,
MAYCHANGE [memory :> bytes(z,8 * val k)] ,,
MAYCHANGE SOME_FLAGS)`,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events])`,
W64_GEN_TAC `k:num` THEN
MAP_EVERY X_GEN_TAC [`z:int64`; `x:int64`; `m:int64`] THEN
MAP_EVERY X_GEN_TAC [`a:num`; `n:num`; `pc:num`] THEN
Expand Down
6 changes: 3 additions & 3 deletions arm/proofs/bignum_bigendian_4.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ let BIGNUM_FROMBEBYTES_4_CORRECT = time prove
read (memory :> bytelist(x,32)) s = l)
(\s. read PC s = word (pc + 0x110) /\
bignum_from_memory(z,4) s = num_of_bytelist (REVERSE l))
(MAYCHANGE [PC; X2; X3; X4] ,,
(MAYCHANGE [PC; X2; X3; X4] ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,4)])`,
MAP_EVERY X_GEN_TAC [`z:int64`; `x:int64`; `l:byte list`; `pc:num`] THEN
REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS; NONOVERLAPPING_CLAUSES] THEN
Expand Down Expand Up @@ -152,7 +152,7 @@ let BIGNUM_TOBEBYTES_4_CORRECT = time prove
(\s. read PC s = word (pc + 0x110) /\
read (memory :> bytelist(z,32)) s =
REVERSE(bytelist_of_num 32 n))
(MAYCHANGE [PC; X2; X3; X4] ,,
(MAYCHANGE [PC; X2; X3; X4] ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,4)])`,
REPEAT GEN_TAC THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN
Expand Down Expand Up @@ -199,7 +199,7 @@ let BIGNUM_BIGENDIAN_4_CORRECT = time prove
(\s. read PC s = word (pc + 0x110) /\
bignum_from_memory(z,4) s =
num_of_bytelist(REVERSE(bytelist_of_num 32 n)))
(MAYCHANGE [PC; X2; X3; X4] ,,
(MAYCHANGE [PC; X2; X3; X4] ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,4)])`,
REPEAT GEN_TAC THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
GEN_REWRITE_TAC (RATOR_CONV o LAND_CONV o ONCE_DEPTH_CONV)
Expand Down
6 changes: 3 additions & 3 deletions arm/proofs/bignum_bigendian_6.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ let BIGNUM_FROMBEBYTES_6_CORRECT = time prove
read (memory :> bytelist(x,48)) s = l)
(\s. read PC s = word (pc + 0x198) /\
bignum_from_memory(z,6) s = num_of_bytelist (REVERSE l))
(MAYCHANGE [PC; X2; X3; X4] ,,
(MAYCHANGE [PC; X2; X3; X4] ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,6)])`,
MAP_EVERY X_GEN_TAC [`z:int64`; `x:int64`; `l:byte list`; `pc:num`] THEN
REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS; NONOVERLAPPING_CLAUSES] THEN
Expand Down Expand Up @@ -186,7 +186,7 @@ let BIGNUM_TOBEBYTES_6_CORRECT = time prove
(\s. read PC s = word (pc + 0x198) /\
read (memory :> bytelist(z,48)) s =
REVERSE(bytelist_of_num 48 n))
(MAYCHANGE [PC; X2; X3; X4] ,,
(MAYCHANGE [PC; X2; X3; X4] ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,6)])`,
REPEAT GEN_TAC THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN
Expand Down Expand Up @@ -233,7 +233,7 @@ let BIGNUM_BIGENDIAN_6_CORRECT = time prove
(\s. read PC s = word (pc + 0x198) /\
bignum_from_memory(z,6) s =
num_of_bytelist(REVERSE(bytelist_of_num 48 n)))
(MAYCHANGE [PC; X2; X3; X4] ,,
(MAYCHANGE [PC; X2; X3; X4] ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,6)])`,
REPEAT GEN_TAC THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
GEN_REWRITE_TAC (RATOR_CONV o LAND_CONV o ONCE_DEPTH_CONV)
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_bitfield.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ let BIGNUM_BITFIELD_CORRECT = prove
(\s. read PC s = word(pc + 0x68) /\
C_RETURN s = word((a DIV (2 EXP val n)) MOD (2 EXP val l)))
(MAYCHANGE [PC; X0; X2; X4; X5; X6; X7; X8] ,,
MAYCHANGE SOME_FLAGS)`,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events])`,
W64_GEN_TAC `k:num` THEN X_GEN_TAC `x:int64` THEN
MAP_EVERY W64_GEN_TAC [`n:num`; `l:num`] THEN
MAP_EVERY X_GEN_TAC [`a:num`; `pc:num`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_bitsize.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ let BIGNUM_BITSIZE_CORRECT = prove
(\s'. read PC s' = word (pc + 0x38) /\
C_RETURN s' = word(bitsize x))
(MAYCHANGE [PC; X0; X2; X3; X4; X5] ,,
MAYCHANGE SOME_FLAGS)`,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events])`,
W64_GEN_TAC `k:num` THEN
MAP_EVERY X_GEN_TAC [`a:int64`; `x:num`; `pc:num`] THEN
REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS] THEN
Expand Down
8 changes: 5 additions & 3 deletions arm/proofs/bignum_cdiv.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -193,7 +193,7 @@ let BIGNUM_CDIV_CORRECT = prove
C_RETURN s = word(a MOD val m)))
(MAYCHANGE [PC; X0; X2; X3; X4; X5; X6; X7; X8; X9;
X10; X11; X12; X13; X14] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,val k)])`,
W64_GEN_TAC `k:num` THEN X_GEN_TAC `z:int64` THEN W64_GEN_TAC `n:num` THEN
X_GEN_TAC `x:int64` THEN W64_GEN_TAC `m:num` THEN
Expand Down Expand Up @@ -228,7 +228,8 @@ let BIGNUM_CDIV_CORRECT = prove
(~(m = 0) ==> read X14 s = word (a MOD m)))
(MAYCHANGE [PC; X5; X6; X7; X8; X9; X10;
X11; X12; X13; X14] ,,
MAYCHANGE [NF; ZF; CF; VF])`
MAYCHANGE [NF; ZF; CF; VF] ,,
MAYCHANGE [events])`
MP_TAC THENL
[ALL_TAC;
REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN DISCH_THEN(fun th ->
Expand Down Expand Up @@ -315,7 +316,8 @@ let BIGNUM_CDIV_CORRECT = prove
&2 pow 64 + &(val (read X5 s)) < &2 pow 128 / &n /\
&2 pow 128 / &n <= &2 pow 64 + &(val (read X5 s)) + &1)
(MAYCHANGE [PC; X5; X7; X9; X14] ,,
MAYCHANGE [NF; ZF; CF; VF])`
MAYCHANGE [NF; ZF; CF; VF] ,,
MAYCHANGE [events])`
MP_TAC THENL
[ALL_TAC;
REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN DISCH_THEN(fun th ->
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_cdiv_exact.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ let BIGNUM_CDIV_EXACT_CORRECT = prove
lowdigits (a DIV val m) (val k)))
(MAYCHANGE [PC; X2; X3; X4; X5; X6; X7; X8; X9;
X10; X11; X12; X13] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,val k)])`,
W64_GEN_TAC `k:num` THEN X_GEN_TAC `z:int64` THEN W64_GEN_TAC `n:num` THEN
X_GEN_TAC `x:int64` THEN W64_GEN_TAC `m:num` THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_cld.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ let BIGNUM_CLD_CORRECT = prove
(\s'. read PC s' = word (pc + 0x28) /\
C_RETURN s' = word((64 * val k - bitsize x) DIV 64))
(MAYCHANGE [PC; X0; X2; X3; X4] ,,
MAYCHANGE SOME_FLAGS)`,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events])`,
W64_GEN_TAC `k:num` THEN
MAP_EVERY X_GEN_TAC [`a:int64`; `x:num`; `pc:num`] THEN
REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_clz.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ let BIGNUM_CLZ_CORRECT = prove
(\s'. read PC s' = word (pc + 0x3c) /\
C_RETURN s' = word(64 * val k - bitsize x))
(MAYCHANGE [PC; X0; X2; X3; X4; X5] ,,
MAYCHANGE SOME_FLAGS)`,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events])`,
W64_GEN_TAC `k:num` THEN
MAP_EVERY X_GEN_TAC [`a:int64`; `x:num`; `pc:num`] THEN
REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_cmadd.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ let BIGNUM_CMADD_CORRECT = prove
(val n <= val p
==> C_RETURN s = word(highdigits (d + val c * a) (val p))))
(MAYCHANGE [PC; X0; X3; X5; X6; X7; X8; X9] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,val p)])`,
W64_GEN_TAC `p:num` THEN MAP_EVERY X_GEN_TAC [`z:int64`; `d:num`] THEN
W64_GEN_TAC `c:num` THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_cmnegadd.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ let BIGNUM_CMNEGADD_CORRECT = prove
&2 pow (64 * val p) * &(val(C_RETURN s)):int =
&d - &(val c) * &a))
(MAYCHANGE [PC; X0; X3; X5; X6; X7; X8; X9] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,val p)])`,
W64_GEN_TAC `p:num` THEN MAP_EVERY X_GEN_TAC [`z:int64`; `d:num`] THEN
W64_GEN_TAC `c:num` THEN
Expand Down
5 changes: 3 additions & 2 deletions arm/proofs/bignum_cmod.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,7 @@ let BIGNUM_CMOD_CORRECT = prove
(\s. read PC s = word(pc + 0x140) /\
(~(val m = 0) ==> C_RETURN s = word(a MOD val m)))
(MAYCHANGE [PC; X0; X3; X4; X5; X6; X7; X8; X9; X10] ,,
MAYCHANGE SOME_FLAGS)`,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events])`,
W64_GEN_TAC `k:num` THEN X_GEN_TAC `x:int64` THEN W64_GEN_TAC `m:num` THEN
MAP_EVERY X_GEN_TAC [`a:num`; `pc:num`] THEN
REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS] THEN
Expand Down Expand Up @@ -191,7 +191,8 @@ let BIGNUM_CMOD_CORRECT = prove
&2 pow 64 + &(val (read X5 s)) < &2 pow 128 / &n /\
&2 pow 128 / &n <= &2 pow 64 + &(val (read X5 s)) + &1)
(MAYCHANGE [PC; X5; X6; X9; X10] ,,
MAYCHANGE [NF; ZF; CF; VF])`
MAYCHANGE [NF; ZF; CF; VF] ,,
MAYCHANGE [events])`
MP_TAC THENL
[ALL_TAC;
REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN DISCH_THEN(fun th ->
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_cmul.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ let BIGNUM_CMUL_CORRECT = prove
(p = n
==> C_RETURN s = word(highdigits (val c * a) (val p))))
(MAYCHANGE [PC; X0; X3; X5; X6; X7; X8] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,val p)])`,
W64_GEN_TAC `p:num` THEN X_GEN_TAC `z:int64` THEN W64_GEN_TAC `c:num` THEN
W64_GEN_TAC `n:num` THEN MAP_EVERY X_GEN_TAC [`x:int64`; `a:num`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_cmul_p25519.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ let BIGNUM_CMUL_P25519_CORRECT = time prove
(a < p_25519
==> bignum_from_memory (z,4) s = (val c * a) MOD p_25519))
(MAYCHANGE [PC; X3; X4; X5; X6; X7; X8; X9; X10] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,4)])`,
MAP_EVERY X_GEN_TAC
[`z:int64`; `c:int64`; `x:int64`; `a:num`; `pc:num`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_cmul_p256.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ let BIGNUM_CMUL_P256_CORRECT = time prove
(a < p_256
==> bignum_from_memory (z,4) s = (val c * a) MOD p_256))
(MAYCHANGE [PC; X3; X4; X5; X6; X7; X8; X9; X10; X11; X12] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,4)])`,
MAP_EVERY X_GEN_TAC
[`z:int64`; `c:int64`; `x:int64`; `a:num`; `pc:num`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_cmul_p256k1.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ let BIGNUM_CMUL_P256K1_CORRECT = time prove
(a < p_256k1
==> bignum_from_memory (z,4) s = (val c * a) MOD p_256k1))
(MAYCHANGE [PC; X3; X4; X5; X6; X7; X8; X9; X10] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,4)])`,
MAP_EVERY X_GEN_TAC
[`z:int64`; `c:int64`; `x:int64`; `a:num`; `pc:num`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_cmul_p384.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,7 @@ let BIGNUM_CMUL_P384_CORRECT = time prove
==> bignum_from_memory (z,6) s = (val c * a) MOD p_384))
(MAYCHANGE [PC; X1; X2; X3; X4; X5; X6; X7; X8;
X9; X10; X11; X12; X13] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,6)])`,
MAP_EVERY X_GEN_TAC
[`z:int64`; `c:int64`; `x:int64`; `a:num`; `pc:num`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_cmul_p521.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,7 @@ let BIGNUM_CMUL_P521_CORRECT = time prove
==> bignum_from_memory (z,9) s = (val c * a) MOD p_521))
(MAYCHANGE [PC; X3; X4; X5; X6; X7; X8;
X9; X10; X11; X12; X13; X14; X15] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,9)])`,
MAP_EVERY X_GEN_TAC
[`z:int64`; `c:int64`; `x:int64`; `a:num`; `pc:num`] THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_cmul_sm2.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ let BIGNUM_CMUL_SM2_CORRECT = time prove
(a < p_sm2
==> bignum_from_memory (z,4) s = (val c * a) MOD p_sm2))
(MAYCHANGE [PC; X3; X4; X5; X6; X7; X8; X9; X10; X11; X12] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,4)])`,
MAP_EVERY X_GEN_TAC
[`z:int64`; `c:int64`; `x:int64`; `a:num`; `pc:num`] THEN
Expand Down
4 changes: 2 additions & 2 deletions arm/proofs/bignum_coprime.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -258,7 +258,7 @@ let BIGNUM_COPRIME_CORRECT = prove
C_RETURN s = if coprime(a,b) then word 1 else word 0)
(MAYCHANGE [PC; X0; X1; X2; X3; X5; X6; X7; X8; X9; X10; X11;
X12; X13; X14; X15; X16; X17; X19; X20] ,,
MAYCHANGE SOME_FLAGS ,,
MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(w,2 * MAX (val m) (val n))])`,
W64_GEN_TAC `m:num` THEN MAP_EVERY X_GEN_TAC [`x:int64`; `a:num`] THEN
W64_GEN_TAC `n:num` THEN MAP_EVERY X_GEN_TAC [`y:int64`; `b:num`] THEN
Expand Down Expand Up @@ -319,7 +319,7 @@ let BIGNUM_COPRIME_CORRECT = prove
MATCH_MP_TAC ENSURES_FRAME_SUBSUMED THEN EXISTS_TAC
`MAYCHANGE [PC; X0; X1; X2; X3; X5; X6; X7; X8; X9; X10; X11;
X12; X13; X14; X15; X16; X17; X19; X20] ,,
MAYCHANGE [NF; ZF; CF; VF] ,,
MAYCHANGE [NF; ZF; CF; VF] ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(mm,k); memory :> bignum(nn,k)]` THEN
CONJ_TAC THENL
[REPEAT(MATCH_MP_TAC SUBSUMED_SEQ THEN REWRITE_TAC[SUBSUMED_REFL]) THEN
Expand Down
2 changes: 1 addition & 1 deletion arm/proofs/bignum_copy.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ let BIGNUM_COPY_CORRECT = prove
bignum_from_memory (x,val n) s = a)
(\s. read PC s = word (pc + 0x3c) /\
bignum_from_memory (z,val k) s = lowdigits a (val k))
(MAYCHANGE [PC; X2; X4; X5] ,, MAYCHANGE SOME_FLAGS ,,
(MAYCHANGE [PC; X2; X4; X5] ,, MAYCHANGE SOME_FLAGS ,, MAYCHANGE [events] ,,
MAYCHANGE [memory :> bignum(z,val k)])`,
REWRITE_TAC[NONOVERLAPPING_CLAUSES] THEN
REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS; fst BIGNUM_COPY_EXEC] THEN
Expand Down
Loading