Refine ARM ABI specifications for Q8-Q15

The ABI only requires preservation of the low 64-bit parts of
Q8,...,Q15, and MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI now
reflects that with new entries Q8 :> tophalf; ...; Q15 :> tophalf.
The subroutine boilerplate tactic ARM_ADD_RETURN_STACK_TAC is now
updated (somewhat crudely) to accept save/restore of D8,...,D15
in the prologue and epilogue of functions.

arm/proofs/arm.ml

@@ -231,7 +231,7 @@ let ARM_EXEC_CONV =
     ONCE_DEPTH_CONV(EQT_INTRO o ORTHOGONAL_COMPONENTS_CONV) THENC
     REWRITE_CONV[] THENC
     ONCE_DEPTH_CONV(LAND_CONV DIMINDEX_CONV THENC NUM_DIV_CONV) THENC
-    GEN_REWRITE_CONV ONCE_DEPTH_CONV [GSYM BYTES64_WBYTES;
+    GEN_REWRITE_CONV ONCE_DEPTH_CONV [GSYM BYTES32_WBYTES; GSYM BYTES64_WBYTES;
                                       GSYM BYTES128_WBYTES] THENC
     GEN_REWRITE_CONV ONCE_DEPTH_CONV [qth] THENC
     GEN_REWRITE_CONV ONCE_DEPTH_CONV [rth] THENC
@@ -713,6 +713,52 @@ let ARM_MACRO_SIM_ABBREV_TAC =
         let n = int_of_string(implode(tl(explode(fst(dest_var sv))))) in
         (ARM_STEPS_TAC execth ((n+1)--(n+prep)) THEN main_tac) (asl,w);;
 
+(* ------------------------------------------------------------------------- *)
+(* Refinment of ENSURES_PRESERVED_TAC for special D register handling.       *)
+(* ------------------------------------------------------------------------- *)
+
+let ENSURES_PRESERVED_DREG_TAC =
+  let pth = prove
+   (`read (Q8 :> bottomhalf) s = word_zx(read Q8 s) /\
+     read (Q9 :> bottomhalf) s = word_zx (read Q9 s) /\
+     read (Q10 :> bottomhalf) s = word_zx (read Q10 s) /\
+     read (Q11 :> bottomhalf) s = word_zx (read Q11 s) /\
+     read (Q12 :> bottomhalf) s = word_zx (read Q12 s) /\
+     read (Q13 :> bottomhalf) s = word_zx (read Q13 s) /\
+     read (Q14 :> bottomhalf) s = word_zx (read Q14 s) /\
+     read (Q15 :> bottomhalf) s = word_zx (read Q15 s)`,
+    CONV_TAC(ONCE_DEPTH_CONV COMPONENT_CANON_CONV) THEN
+    REWRITE_TAC[READ_COMPONENT_COMPOSE; READ_ZEROTOP_64;
+                bottomhalf; subword; read; FUN_EQ_THM] THEN
+    REWRITE_TAC[word_zx; DIV_1; EXP; WORD_MOD_SIZE])
+  and sth = prove
+   (`valid_component c /\
+     R ,, R = R /\
+     MAYCHANGE [c :> tophalf] subsumed R /\
+     ensures step P Q (R ,, MAYCHANGE [c])
+     ==> ensures step P Q (R ,, MAYCHANGE [c :> bottomhalf])`,
+    REWRITE_TAC[MAYCHANGE_SING] THEN
+    REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
+    MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] ENSURES_FRAME_SUBSUMED) THEN
+    FIRST_ASSUM(fun th ->
+      GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [SYM th]) THEN
+    REWRITE_TAC[GSYM SEQ_ASSOC] THEN MATCH_MP_TAC SUBSUMED_SEQ THEN
+    REWRITE_TAC[SUBSUMED_REFL] THEN
+    FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP ASSIGNS_TOPHALF_BOTTOMHALF) THEN
+    MATCH_MP_TAC SUBSUMED_SEQ THEN ASM_REWRITE_TAC[SUBSUMED_REFL]) in
+  let alist = zip [`D8`; `D9`; `D10`; `D11`; `D12`; `D13`; `D14`; `D15`]
+                  (map (lhand o lhand o concl) (CONJUNCTS pth)) in
+  let dregs = map fst alist in
+  fun pname ctm ->
+    if not (mem ctm dregs) then ENSURES_PRESERVED_TAC pname ctm else
+    let ctm' = assoc ctm alist in
+    ENSURES_PRESERVED_TAC pname ctm' THEN REWRITE_TAC[pth] THEN
+    TRY(REWRITE_TAC[SEQ_ASSOC] THEN MATCH_MP_TAC sth THEN
+        CONJ_TAC THENL [CONV_TAC VALID_COMPONENT_CONV; ALL_TAC] THEN
+        CONJ_TAC THENL [MAYCHANGE_IDEMPOT_TAC; ALL_TAC] THEN
+        CONJ_TAC THENL [SUBSUMED_MAYCHANGE_TAC THEN NO_TAC; ALL_TAC] THEN
+        REWRITE_TAC[GSYM SEQ_ASSOC]);;
+
 (* ------------------------------------------------------------------------- *)
 (* Fix up call/return boilerplate given core correctness.                    *)
 (* ------------------------------------------------------------------------- *)
@@ -797,7 +843,8 @@ let ARM_ADD_RETURN_NOSTACK_TAC =
 let ARM_ADD_RETURN_STACK_TAC =
   let mono2lemma = MESON[]
    `(!x. (!y. P x y) ==> (!y. Q x y)) ==> (!x y. P x y) ==> (!x y. Q x y)`
-  and sp_tm = `SP` and x30_tm = `X30` in
+  and sp_tm = `SP` and x30_tm = `X30`
+  and dqd_thm = WORD_BLAST `(word_zx:int128->int64)(word_zx(x:int64)) = x` in
   fun execth coreth reglist stackoff ->
     let regs = dest_list reglist in
     let n = let n0 = length regs / 2 in
@@ -827,15 +874,17 @@ let ARM_ADD_RETURN_STACK_TAC =
       ENSURES_EXISTING_PRESERVED_TAC sp_tm THEN
       (if mem x30_tm regs then ENSURES_EXISTING_PRESERVED_TAC x30_tm
        else ALL_TAC) THEN
-      MAP_EVERY (fun c -> ENSURES_PRESERVED_TAC ("init_"^fst(dest_const c)) c)
+      MAP_EVERY (fun c -> ENSURES_PRESERVED_DREG_TAC
+                            ("init_"^fst(dest_const c)) c)
                 (subtract regs [x30_tm]) THEN
       REWRITE_TAC(!simulation_precanon_thms) THEN ENSURES_INIT_TAC "s0" THEN
       ARM_STEPS_TAC execth (1--n) THEN
       MP_TAC th) THEN
     ARM_BIGSTEP_TAC execth ("s"^string_of_int(n+1)) THEN
     REWRITE_TAC(!simulation_precanon_thms) THEN
     ARM_STEPS_TAC execth ((n+2)--(2*n+2)) THEN
-    ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[];;
+    ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
+    REWRITE_TAC[dqd_thm];;
 
 (* ------------------------------------------------------------------------- *)
 (* Handling more general branch targets                                      *)

arm/proofs/instruction.ml

@@ -727,19 +727,25 @@ let MODIFIABLE_GPRS = define
     subroutine calls; the remaining registers (v0-v7, v16-v31) do not need to
     be preserved (or should be preserved by the caller). Additionally, only
     the bottom 64 bits of each value stored in v8-v15 need to be preserved"
-    - 2023. Jun. 2: there is no implementation that utilizes the high 64-bit
-      parts of v8-v15. If they are used, this definition need to be expanded to
-      include them. *)
+ *)
+
 let MODIFIABLE_SIMD_REGS = define
  `MODIFIABLE_SIMD_REGS =
     [Q0; Q1; Q2; Q3; Q4; Q5; Q6; Q7; Q16; Q17; Q18; Q19; Q20; Q21;
       Q22; Q23; Q24; Q25; Q26; Q27; Q28; Q29; Q30; Q31]`;;
 
+let MODIFIABLE_UPPER_SIMD_REGS = define
+ `MODIFIABLE_UPPER_SIMD_REGS =
+   [Q8 :> tophalf; Q9 :> tophalf; Q10 :> tophalf; Q11 :> tophalf;
+    Q12 :> tophalf; Q13 :> tophalf; Q14 :> tophalf; Q15 :> tophalf]`;;
+
 let MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI = REWRITE_RULE
-    [SOME_FLAGS; MODIFIABLE_GPRS; MODIFIABLE_SIMD_REGS]
+    [SOME_FLAGS; MODIFIABLE_GPRS; MODIFIABLE_SIMD_REGS;
+     MODIFIABLE_UPPER_SIMD_REGS]
  (new_definition `MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI =
     MAYCHANGE [PC] ,, MAYCHANGE MODIFIABLE_GPRS ,,
-    MAYCHANGE MODIFIABLE_SIMD_REGS ,, MAYCHANGE SOME_FLAGS`);;
+    MAYCHANGE MODIFIABLE_SIMD_REGS ,,
+    MAYCHANGE MODIFIABLE_UPPER_SIMD_REGS ,, MAYCHANGE SOME_FLAGS`);;
 
 (* ------------------------------------------------------------------------- *)
 (* General register-register instructions.                                   *)

common/components.ml

@@ -1151,6 +1151,22 @@ let READ_WRITE_LOWER_SUBWORD = prove
   REWRITE_TAC[MOD_MULT_ADD] THEN
   SIMP_TAC[MOD_MOD; MULT_EQ_0; EXP_EQ_0; ARITH_EQ]);;
 
+let READ_TOPHALF_BOTTOMHALF_EQ = prove
+ (`!x y:(N tybit0)word.
+        read tophalf x = read tophalf y /\
+        read bottomhalf x = read bottomhalf y <=>
+        x = y`,
+  REPEAT GEN_TAC THEN
+  REWRITE_TAC[bottomhalf; tophalf; subword; read; GSYM word_subword] THEN
+  REWRITE_TAC[WORD_EQ_BITS_ALT; DIMINDEX_TYBIT0; BIT_WORD_SUBWORD] THEN
+  SIMP_TAC[ARITH_RULE `MIN n n = n`; ADD_CLAUSES] THEN
+  REWRITE_TAC[ARITH_RULE `i < 2 * n <=> n <= i /\ i - n < n \/ i < n`] THEN
+  REWRITE_TAC[FORALL_AND_THM; TAUT
+   `p \/ q ==> r <=> (p ==> r) /\ (q ==> r)`] THEN
+  AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[LE_EXISTS] THEN
+  REWRITE_TAC[LEFT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
+  MESON_TAC[ADD_SYM; ADD_SUB]);;
+
 let STRONGLY_VALID_COMPONENT_BOTTOMHALF = prove
  (`strongly_valid_component(bottomhalf:((N tybit0)word,N word)component)`,
   REWRITE_TAC[bottomhalf] THEN

common/relational.ml

@@ -2081,6 +2081,75 @@ let ENSURES_EXISTING_PRESERVED_TAC ctm =
    [REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN NO_TAC;
     REWRITE_TAC[GSYM CONJ_ASSOC; GSYM SEQ_ASSOC]];;
 
+(* ------------------------------------------------------------------------- *)
+(* A more refined version where we are allowed to modify a high part.        *)
+(* ------------------------------------------------------------------------- *)
+
+let ASSIGNS_TOPHALF_BOTTOMHALF = prove
+ (`!c:(A,(N tybit0)word)component.
+        valid_component c
+        ==> ASSIGNS (c :> tophalf) ,, ASSIGNS (c :> bottomhalf) = ASSIGNS c`,
+  REPEAT STRIP_TAC THEN REWRITE_TAC[ASSIGNS; ASSIGNS_SEQ; FUN_EQ_THM] THEN
+  MAP_EVERY X_GEN_TAC [`s:A`; `s':A`] THEN
+  REWRITE_TAC[assign; WRITE_COMPONENT_COMPOSE] THEN
+  RULE_ASSUM_TAC(REWRITE_RULE[valid_component]) THEN
+  ASM_REWRITE_TAC[READ_WRITE_TOPHALF_BOTTOMHALF] THEN
+  EQ_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM; RIGHT_IMP_EXISTS_THM] THENL
+   [MAP_EVERY X_GEN_TAC [`x:N word`; `y:N word`] THEN
+    EXISTS_TAC `(word_join:N word->N word->(N tybit0)word) x y`;
+    X_GEN_TAC `z:(N tybit0)word` THEN MAP_EVERY EXISTS_TAC
+     [`word_subword (z:(N tybit0)word) (dimindex(:N),dimindex(:N)):N word`;
+      `word_subword (z:(N tybit0)word) (0,dimindex(:N)):N word`]] THEN
+  DISCH_THEN(SUBST1_TAC o SYM) THEN AP_THM_TAC THEN AP_TERM_TAC THEN
+  SPEC_TAC(`read (c:(A,(N tybit0)word)component) s`,`w:(N tybit0) word`) THEN
+  POP_ASSUM_LIST(K ALL_TAC) THEN GEN_TAC THEN
+  GEN_REWRITE_TAC I [GSYM READ_TOPHALF_BOTTOMHALF_EQ] THEN
+  REWRITE_TAC[READ_WRITE_TOPHALF_BOTTOMHALF] THEN
+  REWRITE_TAC[bottomhalf; tophalf; subword; read] THEN
+  SIMP_TAC[VAL_WORD_JOIN; word_subword; EXP; DIV_1] THEN
+  REWRITE_TAC[DIMINDEX_TYBIT0; DIV_MOD; GSYM EXP_ADD; GSYM MULT_2] THEN
+  REWRITE_TAC[MOD_MOD_EXP_MIN; ARITH_RULE `MIN (2 * n) n = n`] THEN
+  REWRITE_TAC[MOD_MULT_ADD; WORD_VAL; ARITH_RULE `MIN n n = n`;
+              VAL_MOD_REFL] THEN
+  REWRITE_TAC[MULT_2; EXP_ADD; GSYM DIV_MOD] THEN
+  SIMP_TAC[DIV_MULT_ADD; EXP_EQ_0; ARITH_EQ; DIV_LT; VAL_BOUND] THEN
+  REWRITE_TAC[ADD_CLAUSES; VAL_MOD_REFL; WORD_VAL]);;
+
+let ENSURES_MAYCHANGE_TOPHALF_PRESERVED = prove
+ (`!(c:(A,((N)tybit0)word)component) t P Q R.
+        valid_component c /\
+        (!s s'. R s s' ==> read c s' = read c s) /\
+        (!d. ensures t (\s. P s /\ read (c :> bottomhalf) s = d)
+                       (\s. Q s /\ read (c :> bottomhalf) s = d)
+                       (R ,, MAYCHANGE [c]))
+        ==> ensures t P Q (R ,, MAYCHANGE [c :> tophalf])`,
+  REPEAT GEN_TAC THEN REWRITE_TAC[ensures; valid_component] THEN
+  STRIP_TAC THEN X_GEN_TAC `s0:A` THEN DISCH_TAC THEN
+  ABBREV_TAC `d = read (c:(A,((N)tybit0)word)component) s0` THEN
+  FIRST_X_ASSUM(MP_TAC o SPECL
+   [`word_subword (d:((N)tybit0)word) (0,dimindex(:N)):N word`; `s0:A`]) THEN
+  ASM_REWRITE_TAC[MAYCHANGE; SEQ_ID] THEN ANTS_TAC THENL
+   [REWRITE_TAC[READ_COMPONENT_COMPOSE; SEQ_ID] THEN
+    ASM_REWRITE_TAC[bottomhalf; READ_SUBWORD];
+    ALL_TAC] THEN
+  REWRITE_TAC[ASSIGNS_THM; seq] THEN
+  FIRST_X_ASSUM(MP_TAC o SPEC `s0:A`) THEN
+  ABBREV_TAC `fr = (R:A->A->bool) s0` THEN DISCH_TAC THEN
+  SPEC_TAC(`s0:A`,`s0:A`) THEN MATCH_MP_TAC EVENTUALLY_MONO THEN
+  X_GEN_TAC `s2:A` THEN ASM_REWRITE_TAC[READ_COMPONENT_COMPOSE] THEN
+  DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
+  ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
+  X_GEN_TAC `s1:A` THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
+  DISCH_THEN(X_CHOOSE_TAC `y:((N)tybit0)word`) THEN
+  EXISTS_TAC `s1:A` THEN ASM_REWRITE_TAC[WRITE_COMPONENT_COMPOSE] THEN
+  FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN
+  FIRST_X_ASSUM(MP_TAC o SYM o SYM) THEN ASM_REWRITE_TAC[] THEN
+  DISCH_TAC THEN EXISTS_TAC `read tophalf (y:(N tybit0)word)` THEN
+  ASM_SIMP_TAC[] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
+  GEN_REWRITE_TAC I [GSYM READ_TOPHALF_BOTTOMHALF_EQ] THEN
+  ASM_REWRITE_TAC[READ_WRITE_TOPHALF_BOTTOMHALF] THEN
+  REWRITE_TAC[bottomhalf; read; subword; GSYM word_subword]);;
+
 (* ------------------------------------------------------------------------- *)
 (* A kind of dual of ignoring things about unchanged components.             *)
 (* ------------------------------------------------------------------------- *)

x86/proofs/x86.ml

@@ -730,7 +730,7 @@ let x86_MOV = new_definition
  *** A bit bizarrely there are same-size versions of MOVSXD.
  *** These are really just freaks of decoding, with semantics
  *** equivalent to MOV, and use is actively discouraged in
- *** the Intel manuals ("The use of MOVSXD without REX.W in 
+ *** the Intel manuals ("The use of MOVSXD without REX.W in
  *** 64-bit mode is discouraged".) However, we do handle
  *** the 32->32 case anyway, though not the 16->16 case, in
  *** line with the general policy of rejecting operand size