AVX2 enabling

arm/proofs/bignum_copy_row_from_table_16_neon.ml

@@ -80,7 +80,7 @@ let LT_WORD_64 = prove(`!x (y:int64). x < val y ==> x < 2 EXP 64`,
 let READ_MEMORY_BYTES_BYTES128 = prove(`!z s.
     read (memory :> bytes (z,16)) s = val (read (memory :> bytes128 z) s)`,
   REPEAT GEN_TAC THEN
-  REWRITE_TAC[fst (CONJ_PAIR READ_MEMORY_BYTESIZED_SPLIT)] THEN
+  REWRITE_TAC[el 1 (CONJUNCTS READ_MEMORY_BYTESIZED_SPLIT)] THEN
   REWRITE_TAC[VAL_WORD_JOIN;DIMINDEX_64;DIMINDEX_128] THEN
   IMP_REWRITE_TAC[MOD_LT] THEN
   REWRITE_TAC[ARITH_RULE`2 EXP 128 = 2 EXP 64 * 2 EXP 64`] THEN

arm/proofs/bignum_copy_row_from_table_32_neon.ml

@@ -103,7 +103,7 @@ let LT_WORD_64 = prove(`!x (y:int64). x < val y ==> x < 2 EXP 64`,
 let READ_MEMORY_BYTES_BYTES128 = prove(`!z s.
     read (memory :> bytes (z,16)) s = val (read (memory :> bytes128 z) s)`,
   REPEAT GEN_TAC THEN
-  REWRITE_TAC[fst (CONJ_PAIR READ_MEMORY_BYTESIZED_SPLIT)] THEN
+  REWRITE_TAC[el 1 (CONJUNCTS READ_MEMORY_BYTESIZED_SPLIT)] THEN
   REWRITE_TAC[VAL_WORD_JOIN;DIMINDEX_64;DIMINDEX_128] THEN
   IMP_REWRITE_TAC[MOD_LT] THEN
   REWRITE_TAC[ARITH_RULE`2 EXP 128 = 2 EXP 64 * 2 EXP 64`] THEN
@@ -112,7 +112,6 @@ let READ_MEMORY_BYTES_BYTES128 = prove(`!z s.
   REWRITE_TAC[ARITH_RULE`16 = 8*(1+1)`;GSYM BIGNUM_FROM_MEMORY_BYTES;BIGNUM_FROM_MEMORY_STEP;BIGNUM_FROM_MEMORY_SING] THEN
   REWRITE_TAC[ARITH_RULE`8*1=8`;ARITH_RULE`64*1=64`] THEN ARITH_TAC);;
 
-
 let ABBREV_TABLE_READ_128BITS_TAC name st ofs =
   let v = mk_var (name, `:int128`) in
   let templ =

arm/proofs/bignum_copy_row_from_table_8n_neon.ml

@@ -140,7 +140,7 @@ let READ_MEMORY_BYTES_BYTES64 = prove(`!z s.
 let READ_MEMORY_BYTES_BYTES128 = prove(`!z s.
     read (memory :> bytes (z,16)) s = val (read (memory :> bytes128 z) s)`,
   REPEAT GEN_TAC THEN
-  REWRITE_TAC[fst (CONJ_PAIR READ_MEMORY_BYTESIZED_SPLIT)] THEN
+  REWRITE_TAC[el 1 (CONJUNCTS READ_MEMORY_BYTESIZED_SPLIT)] THEN
   REWRITE_TAC[VAL_WORD_JOIN;DIMINDEX_64;DIMINDEX_128] THEN
   IMP_REWRITE_TAC[MOD_LT] THEN
   REWRITE_TAC[ARITH_RULE`2 EXP 128 = 2 EXP 64 * 2 EXP 64`] THEN

arm/proofs/p256_montjadd.ml

@@ -1165,7 +1165,7 @@ let equiv_goal = mk_equiv_statement
 
 
 extra_early_rewrite_rules :=
-  (hd (CONJUNCTS READ_MEMORY_BYTESIZED_SPLIT))::
+  (el 1 (CONJUNCTS READ_MEMORY_BYTESIZED_SPLIT))::
   !extra_early_rewrite_rules;;
 
 let occ_cache_left:(term * ((term * thm) list ref)) list ref = ref []

arm/proofs/p256_montjdouble.ml

@@ -1896,7 +1896,7 @@ let equiv_goal = mk_equiv_statement
         `\(s:armstate). (x:num)`);;
 
 extra_early_rewrite_rules :=
-  (hd (CONJUNCTS READ_MEMORY_BYTESIZED_SPLIT))::
+  (el 1 (CONJUNCTS READ_MEMORY_BYTESIZED_SPLIT))::
   !extra_early_rewrite_rules;;
 
 let occ_cache_left:(term * ((term * thm) list ref)) list ref = ref []
@@ -2097,4 +2097,4 @@ let P256_MONTJDOUBLE_SUBROUTINE_CORRECT = time prove
   REWRITE_TAC[fst P256_MONTJDOUBLE_OPT_EXEC] THEN
   ARM_ADD_RETURN_STACK_TAC P256_MONTJDOUBLE_OPT_EXEC
     (REWRITE_RULE[fst P256_MONTJDOUBLE_OPT_EXEC]P256_MONTJDOUBLE_CORRECT)
-    `[X19;X20;X21;X22;X23;X24;X25;X26;X27]` 272);;
+    `[X19;X20;X21;X22;X23;X24;X25;X26;X27]` 272);;

arm/proofs/p384_montjadd.ml

@@ -1564,7 +1564,7 @@ let equiv_goal = mk_equiv_statement
         `\(s:armstate). (x:num)`);;
 
 extra_early_rewrite_rules :=
-  (hd (CONJUNCTS READ_MEMORY_BYTESIZED_SPLIT))::
+  (el 1 (CONJUNCTS READ_MEMORY_BYTESIZED_SPLIT))::
   !extra_early_rewrite_rules;;
 
 let occ_cache_left:(term * ((term * thm) list ref)) list ref = ref []

arm/proofs/p384_montjdouble.ml

@@ -2589,7 +2589,7 @@ let equiv_goal = mk_equiv_statement
         `\(s:armstate). (x:num)`);;
 
 extra_early_rewrite_rules :=
-  (hd (CONJUNCTS READ_MEMORY_BYTESIZED_SPLIT))::
+  (el 1 (CONJUNCTS READ_MEMORY_BYTESIZED_SPLIT))::
   !extra_early_rewrite_rules;;
 
 let occ_cache_left:(term * ((term * thm) list ref)) list ref = ref []
@@ -2847,4 +2847,4 @@ let P384_MONTJDOUBLE_SUBROUTINE_CORRECT = time prove
                       memory :> bytes(word_sub stackpointer (word 464),464)])`,
   ARM_ADD_RETURN_STACK_TAC P384_MONTJDOUBLE_OPT_EXEC
    P384_MONTJDOUBLE_CORRECT
-    `[X19; X20; X21; X22; X23; X24; X25; X26; X27]` 464);;
+    `[X19; X20; X21; X22; X23; X24; X25; X26; X27]` 464);;

arm/tutorial/branch.ml

@@ -82,7 +82,7 @@ let branch_SPEC = prove(
     (* Let's name the hypothesis first. *)
     POP_ASSUM (LABEL_TAC "Hcond") THEN
     DISCH_TAC THEN
-    
+
     (* Do symbolic execution on the remaining two insts. *)
     ARM_STEPS_TAC EXEC (3--4) THEN
     ENSURES_FINAL_STATE_TAC THEN

common/components.ml

@@ -1585,6 +1585,57 @@ add_valid_component_thms [VALID_COMPONENT_ZEROTOP_8];;
 add_component_read_write_thms
  [CONJUNCT1(GEN_REWRITE_RULE I [valid_component] VALID_COMPONENT_ZEROTOP_8)];;
 
+(* ------------------------------------------------------------------------- *)
+(* Dually, larger versions that are used to encode the x86 treatment of      *)
+(* writes (but WHEN VEX-ENCODED ONLY!) to XMMs within YMMs within ZMMs.      *)
+(* ------------------------------------------------------------------------- *)
+
+let zerotop_128 = new_definition
+  `zerotop_128:(256 word,128 word)component =
+      through(word_zx,word_zx)`;;
+
+let READ_ZEROTOP_128 = prove
+ (`!s:A. read (c :> zerotop_128) s = word_zx(read c s)`,
+  REWRITE_TAC[READ_COMPONENT_COMPOSE; zerotop_128; through; read]);;
+
+let WRITE_ZEROTOP_128 = prove
+ (`!(s:A) y. write (c :> zerotop_128) y s = write c (word_zx y) s`,
+  REWRITE_TAC[WRITE_COMPONENT_COMPOSE; zerotop_128; through; write]);;
+
+let VALID_COMPONENT_ZEROTOP_128 = prove
+ (`valid_component zerotop_128`,
+  REWRITE_TAC[valid_component; read; write; zerotop_128; through] THEN
+  GEN_TAC THEN MATCH_MP_TAC WORD_ZX_ZX THEN
+  REWRITE_TAC[DIMINDEX_128; DIMINDEX_256] THEN CONV_TAC NUM_REDUCE_CONV);;
+
+add_valid_component_thms [VALID_COMPONENT_ZEROTOP_128];;
+
+add_component_read_write_thms
+ [CONJUNCT1(GEN_REWRITE_RULE I [valid_component] VALID_COMPONENT_ZEROTOP_128)];;
+
+let zerotop_256 = new_definition
+  `zerotop_256:(512 word,256 word)component =
+      through(word_zx,word_zx)`;;
+
+let READ_ZEROTOP_256 = prove
+ (`!s:A. read (c :> zerotop_256) s = word_zx(read c s)`,
+  REWRITE_TAC[READ_COMPONENT_COMPOSE; zerotop_256; through; read]);;
+
+let WRITE_ZEROTOP_256 = prove
+ (`!(s:A) y. write (c :> zerotop_256) y s = write c (word_zx y) s`,
+  REWRITE_TAC[WRITE_COMPONENT_COMPOSE; zerotop_256; through; write]);;
+
+let VALID_COMPONENT_ZEROTOP_256 = prove
+ (`valid_component zerotop_256`,
+  REWRITE_TAC[valid_component; read; write; zerotop_256; through] THEN
+  GEN_TAC THEN MATCH_MP_TAC WORD_ZX_ZX THEN
+  REWRITE_TAC[DIMINDEX_256; DIMINDEX_512] THEN CONV_TAC NUM_REDUCE_CONV);;
+
+add_valid_component_thms [VALID_COMPONENT_ZEROTOP_256];;
+
+add_component_read_write_thms
+ [CONJUNCT1(GEN_REWRITE_RULE I [valid_component] VALID_COMPONENT_ZEROTOP_256)];;
+
 (* ------------------------------------------------------------------------- *)
 (* State component for a multi-byte chunk of memory treated as a number.     *)
 (* NB: This is assuming a *little-endian* encoding.                          *)
@@ -1934,6 +1985,9 @@ let bytes64 = define
 let bytes128 = define
  `bytes128 addr :((int64->byte),int128)component = bytes(addr,16) :> asword`;;
 
+let bytes256 = define
+ `bytes256 addr :((int64->byte),256 word)component = bytes(addr,32) :> asword`;;
+
 let BYTES8_WBYTES = prove
  (`bytes8 = wbytes`,
   REWRITE_TAC[FUN_EQ_THM; wbytes; bytes8] THEN
@@ -1964,6 +2018,12 @@ let BYTES128_WBYTES = prove
   CONV_TAC(ONCE_DEPTH_CONV DIMINDEX_CONV) THEN
   CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[]);;
 
+let BYTES256_WBYTES = prove
+ (`bytes256 = wbytes`,
+  REWRITE_TAC[FUN_EQ_THM; wbytes; bytes256] THEN
+  CONV_TAC(ONCE_DEPTH_CONV DIMINDEX_CONV) THEN
+  CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[]);;
+
 let STRONGLY_VALID_COMPONENT_BYTES8 = prove
  (`!a:int64. strongly_valid_component (bytes8 a)`,
   GEN_TAC THEN
@@ -2095,8 +2155,8 @@ let STRONGLY_VALID_COMPONENT_BYTES128 = prove
   MP_TAC(ISPECL [`a:int64`; `16`] READ_WRITE_BYTES) THEN
   REWRITE_TAC[DIMINDEX_64] THEN CONV_TAC NUM_REDUCE_CONV THEN
   REWRITE_TAC[strongly_valid_component; EXTENSIONALLY_VALID_COMPONENT] THEN
-  STRIP_TAC THEN STRIP_TAC THEN
-  ASM_REWRITE_TAC[bytes128; READ_COMPONENT_COMPOSE; WRITE_COMPONENT_COMPOSE] THEN
+  STRIP_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC
+   [bytes128; READ_COMPONENT_COMPOSE; WRITE_COMPONENT_COMPOSE] THEN
   ASM_REWRITE_TAC[read; write; asword; through; VAL_WORD] THEN
   REWRITE_TAC[DIMINDEX_128] THEN CONV_TAC NUM_REDUCE_CONV THEN
   SUBST1_TAC(
@@ -2120,29 +2180,62 @@ let WEAKLY_VALID_COMPONENT_BYTES128 = prove
   SIMP_TAC[VALID_IMP_WEAKLY_VALID_COMPONENT;
            VALID_COMPONENT_BYTES128]);;
 
+let STRONGLY_VALID_COMPONENT_BYTES256 = prove
+ (`!a:int64. strongly_valid_component (bytes256 a)`,
+  GEN_TAC THEN
+  MP_TAC(ISPECL [`a:int64`; `32`] EXTENSIONALLY_VALID_COMPONENT_BYTES) THEN
+  MP_TAC(ISPECL [`a:int64`; `32`] READ_WRITE_BYTES) THEN
+  REWRITE_TAC[DIMINDEX_64] THEN CONV_TAC NUM_REDUCE_CONV THEN
+  REWRITE_TAC[strongly_valid_component; EXTENSIONALLY_VALID_COMPONENT] THEN
+  STRIP_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC
+   [bytes256; READ_COMPONENT_COMPOSE; WRITE_COMPONENT_COMPOSE] THEN
+  ASM_REWRITE_TAC[read; write; asword; through; VAL_WORD] THEN
+  REWRITE_TAC[DIMINDEX_256] THEN CONV_TAC NUM_REDUCE_CONV THEN
+  SUBST1_TAC(GSYM(NUM_REDUCE_CONV `2 EXP (8 * 32)`)) THEN
+  ASM_REWRITE_TAC[READ_BYTES_MOD_LEN] THEN
+  CONV_TAC(ONCE_DEPTH_CONV NUM_MULT_CONV) THEN
+  REWRITE_TAC[GSYM DIMINDEX_256; VAL_MOD_REFL; WORD_VAL]);;
+
+let EXTENSIONALLY_VALID_COMPONENT_BYTES256 = prove
+ (`!a:int64. extensionally_valid_component (bytes256 a)`,
+  SIMP_TAC[STRONGLY_VALID_IMP_EXTENSIONALLY_VALID_COMPONENT;
+           STRONGLY_VALID_COMPONENT_BYTES256]);;
+
+let VALID_COMPONENT_BYTES256 = prove
+ (`!a:int64. valid_component (bytes256 a)`,
+  SIMP_TAC[STRONGLY_VALID_IMP_VALID_COMPONENT;
+           STRONGLY_VALID_COMPONENT_BYTES256]);;
+
+let WEAKLY_VALID_COMPONENT_BYTES256 = prove
+ (`!a:int64. weakly_valid_component (bytes128 a)`,
+  SIMP_TAC[VALID_IMP_WEAKLY_VALID_COMPONENT;
+           VALID_COMPONENT_BYTES128]);;
+
 add_valid_component_thms
   [VALID_COMPONENT_BYTES8; VALID_COMPONENT_BYTES16;
    VALID_COMPONENT_BYTES32; VALID_COMPONENT_BYTES64;
-   VALID_COMPONENT_BYTES128];;
+   VALID_COMPONENT_BYTES128; VALID_COMPONENT_BYTES256];;
 
 add_strongly_valid_component_thms
   [STRONGLY_VALID_COMPONENT_BYTES8; STRONGLY_VALID_COMPONENT_BYTES16;
    STRONGLY_VALID_COMPONENT_BYTES32; STRONGLY_VALID_COMPONENT_BYTES64;
-   STRONGLY_VALID_COMPONENT_BYTES128];;
+   STRONGLY_VALID_COMPONENT_BYTES128; STRONGLY_VALID_COMPONENT_BYTES256];;
 
 add_extensionally_valid_component_thms
   [EXTENSIONALLY_VALID_COMPONENT_BYTES8;
    EXTENSIONALLY_VALID_COMPONENT_BYTES16;
    EXTENSIONALLY_VALID_COMPONENT_BYTES32;
    EXTENSIONALLY_VALID_COMPONENT_BYTES64;
-   EXTENSIONALLY_VALID_COMPONENT_BYTES128];;
+   EXTENSIONALLY_VALID_COMPONENT_BYTES128;
+   EXTENSIONALLY_VALID_COMPONENT_BYTES256];;
 
 add_weakly_valid_component_thms
   [WEAKLY_VALID_COMPONENT_BYTES8;
    WEAKLY_VALID_COMPONENT_BYTES16;
    WEAKLY_VALID_COMPONENT_BYTES32;
    WEAKLY_VALID_COMPONENT_BYTES64;
-   WEAKLY_VALID_COMPONENT_BYTES128];;
+   WEAKLY_VALID_COMPONENT_BYTES128;
+   WEAKLY_VALID_COMPONENT_BYTES256];;
 
 (*** NB: the composites are better-behaved than plain "bytes".
  *** So when proving "valid_component" theorems by chaining, it
@@ -2155,7 +2248,10 @@ add_weakly_valid_component_thms
  ***)
 
 let READ_MEMORY_BYTESIZED_SPLIT = prove
- (`(!m x s. read (m :> bytes128 x) s =
+ (`(!m x s. read (m :> bytes256 x) s =
+            word_join (read (m :> bytes128 (word_add x (word 16))) s)
+                      (read (m :> bytes128 x) s)) /\
+   (!m x s. read (m :> bytes128 x) s =
             word_join (read (m :> bytes64 (word_add x (word 8))) s)
                       (read (m :> bytes64 x) s)) /\
    (!m x s. read (m :> bytes64 x) s =
@@ -2168,23 +2264,29 @@ let READ_MEMORY_BYTESIZED_SPLIT = prove
             word_join (read (m :> bytes8 (word_add x (word 1))) s)
                       (read (m :> bytes8 x) s))`,
   REWRITE_TAC[GSYM VAL_EQ] THEN
-  SIMP_TAC[VAL_WORD_JOIN_SIMPLE; DIMINDEX_128; DIMINDEX_64; DIMINDEX_32;
-           DIMINDEX_16; DIMINDEX_8; ARITH] THEN
-  REWRITE_TAC[bytes128; bytes64; bytes32; bytes16; bytes8] THEN
+  SIMP_TAC[VAL_WORD_JOIN_SIMPLE; DIMINDEX_256; DIMINDEX_128; DIMINDEX_64;
+           DIMINDEX_32; DIMINDEX_16; DIMINDEX_8; ARITH] THEN
+  REWRITE_TAC[bytes256; bytes128; bytes64; bytes32; bytes16; bytes8] THEN
   REWRITE_TAC[asword; through; read; READ_COMPONENT_COMPOSE] THEN
-  REWRITE_TAC[VAL_WORD; DIMINDEX_128; DIMINDEX_64; DIMINDEX_32; DIMINDEX_16;
-              DIMINDEX_8] THEN
+  REWRITE_TAC[VAL_WORD; DIMINDEX_256; DIMINDEX_128; DIMINDEX_64; DIMINDEX_32;
+              DIMINDEX_16; DIMINDEX_8] THEN
   REWRITE_TAC[ARITH_RULE
    `2 EXP 8 = 2 EXP (8 * 1) /\ 2 EXP 16 = 2 EXP (8 * 2) /\
     2 EXP 32 = 2 EXP (8 * 4) /\ 2 EXP 64 = 2 EXP (8 * 8) /\
-    2 EXP 128 = 2 EXP (8 * 16)`] THEN
+    2 EXP 128 = 2 EXP (8 * 16) /\ 2 EXP 256 = 2 EXP (8 * 32)`] THEN
   SIMP_TAC[READ_BYTES_BOUND; MOD_LT] THEN
   REPEAT STRIP_TAC THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
-   [ARITH_RULE `16 = 8 + 8 /\ 8 = 4 + 4 /\ 4 = 2 + 2 /\ 2 = 1 + 1`] THEN
+   [ARITH_RULE `32 = 16 + 16 /\ 16 = 8 + 8 /\ 8 = 4 + 4 /\
+                4 = 2 + 2 /\ 2 = 1 + 1`] THEN
   REWRITE_TAC[READ_BYTES_COMBINE] THEN ARITH_TAC);;
 
 let READ_MEMORY_BYTESIZED_UNSPLIT = prove
  (`(!m x s d.
+      read (m :> bytes256 x) s = d <=>
+      read (m :> bytes128 x) s = word_subword d (0,128) /\
+      read (m :> bytes128 (word_add x (word 16))) s =
+      word_subword d (128,128)) /\
+   (!m x s d.
       read (m :> bytes128 x) s = d <=>
       read (m :> bytes64 x) s = word_subword d (0,64) /\
       read (m :> bytes64 (word_add x (word 8))) s = word_subword d (64,64)) /\
@@ -3183,7 +3285,11 @@ let (NONOVERLAPPING_TAC:tactic) =
 
 let ORTHOGONAL_COMPONENTS_TAC =
   let pth = prove
-   (`((orthogonal_components (bytes(a,16)) c
+   (`((orthogonal_components (bytes(a,32)) c
+       ==> orthogonal_components (bytes256 a) c) /\
+      (orthogonal_components d (bytes(a,32))
+       ==> orthogonal_components d (bytes256 a)) /\
+      (orthogonal_components (bytes(a,16)) c
        ==> orthogonal_components (bytes128 a) c) /\
       (orthogonal_components d (bytes(a,16))
        ==> orthogonal_components d (bytes128 a)) /\
@@ -3211,8 +3317,8 @@ let ORTHOGONAL_COMPONENTS_TAC =
       ==> orthogonal_components
            (bytes(a1:int64,l1)) (bytes (a2:int64,l2)))`,
     CONJ_TAC THENL
-     [REWRITE_TAC[bytes128; bytes64; bytes32; bytes16; bytes8; bytelist;
-                  COMPONENT_COMPOSE_ASSOC] THEN
+     [REWRITE_TAC[bytes256; bytes128; bytes64; bytes32; bytes16; bytes8;
+                  bytelist; COMPONENT_COMPOSE_ASSOC] THEN
       REWRITE_TAC[ORTHOGONAL_COMPONENTS_SUB_LEFT;
                   ORTHOGONAL_COMPONENTS_SUB_RIGHT];
       DISCH_TAC THEN

common/relational.ml

@@ -106,6 +106,14 @@ let ASSIGN_ZEROTOP_64 = prove
  (`!c y. ((c :> zerotop_64) := y) = (c := word_zx y)`,
   REWRITE_TAC[assign; WRITE_ZEROTOP_64]);;
 
+let ASSIGN_ZEROTOP_128 = prove
+ (`!c y. ((c :> zerotop_128) := y) = (c := word_zx y)`,
+  REWRITE_TAC[assign; WRITE_ZEROTOP_128]);;
+
+let ASSIGN_ZEROTOP_256 = prove
+ (`!c y. ((c :> zerotop_256) := y) = (c := word_zx y)`,
+  REWRITE_TAC[assign; WRITE_ZEROTOP_256]);;
+
 (* ------------------------------------------------------------------------- *)
 (* A nondeterministic assignment of a state component.                       *)
 (* ------------------------------------------------------------------------- *)

x86/proofs/bignum_bigendian_4.ml

@@ -59,7 +59,7 @@ let BIGNUM_FROMBEBYTES_4_CORRECT = time prove
   BIGNUM_DIGITIZE_TAC "d_" `bignum_from_memory(x,4) s0` THEN
   EVERY_ASSUM(fun th ->
    try MP_TAC(GEN_REWRITE_RULE LAND_CONV
-        [CONJUNCT2 READ_MEMORY_BYTESIZED_SPLIT] th)
+        [CONJUNCT2(CONJUNCT2 READ_MEMORY_BYTESIZED_SPLIT)] th)
    with Failure _ -> ALL_TAC) THEN
   REWRITE_TAC[IMP_IMP] THEN
   GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV)

x86/proofs/bignum_bigendian_6.ml

@@ -65,7 +65,7 @@ let BIGNUM_FROMBEBYTES_6_CORRECT = time prove
   BIGNUM_DIGITIZE_TAC "d_" `bignum_from_memory(x,6) s0` THEN
   EVERY_ASSUM(fun th ->
    try MP_TAC(GEN_REWRITE_RULE LAND_CONV
-        [CONJUNCT2 READ_MEMORY_BYTESIZED_SPLIT] th)
+        [CONJUNCT2(CONJUNCT2 READ_MEMORY_BYTESIZED_SPLIT)] th)
    with Failure _ -> ALL_TAC) THEN
   REWRITE_TAC[IMP_IMP] THEN
   GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV)