stp.ml

stp.ml

needs "arm/proofs/base.ml";;

let stp_mc = define_assert_from_elf "stp_mc" "stp.o"
[
  0xa9004c31        (* arm_STP X17 X19 X1 (Immediate_Offset (iword (&0))) *)
];;

let STP_EXEC = ARM_MK_EXEC_RULE stp_mc;;


g `!i a q pc k k4 (z:(64)word) (temp0:(64)word) (temp1:(64)word).

  nonoverlapping_modulo (2 EXP 64)
      (val (word_add z (word (32 * i)):(64)word),32)
      (val (word_add z (word (32 * (i + 1))):(64)word),8 * (k - 4 * i)) /\
  nonoverlapping_modulo (2 EXP 64) (val (word_add z (word (32 * i)):(64)word),16) (pc,4) /\
  k4 < 2 EXP 58 /\
  i < k4 - 1 /\
  2 <= i /\
  4 * i < k /\
  4 * k4 = k
  ==> ensures arm
      (\s. aligned_bytes_loaded s (word pc) stp_mc /\
          read PC s = word pc /\
          read X17 s = temp0 /\
          read X19 s = temp1 /\
          read X1 s = word_add z (word (32 * i)) /\
          read (memory :> bytes (word_add z (word (32 * (i + 1))):(64)word,8 * (k - 4 * i))) s = a /\
          read (memory :> bytes (z:(64)word,32)) s = q)
      (\s. read PC s = word (pc + 4) /\
          read (memory :> bytes (word_add z (word (32 * (i + 1))):(64)word,8 * (k - 4 * i))) s = a /\
          read (memory :> bytes (z:(64)word,32)) s = q)
      (MAYCHANGE [PC] ,, MAYCHANGE [memory :> bytes (word_add z (word (32 * i)),16)])`;;

e(REPEAT STRIP_TAC);;
e(ENSURES_INIT_TAC "s0");;
e(ARM_STEPS_TAC STP_EXEC [1]);;
e(ENSURES_FINAL_STATE_TAC);;
e(ASM_REWRITE_TAC[]);;

(*
  0 [`nonoverlapping_modulo (2 EXP 64) (val (word_add z (word (32 * i))),32)
      (val (word_add z (word (32 * (i + 1)))),8 * (k - 4 * i))`]
  1 [`nonoverlapping_modulo (2 EXP 64) (val (word_add z (word (32 * i))),16)
      (pc,4)`]
  2 [`k4 < 2 EXP 58`]
  3 [`i < k4 - 1`]
  4 [`2 <= i`]
  5 [`4 * i < k`]
  6 [`4 * k4 = k`]
  7 [`aligned_bytes_loaded s1 (word pc) stp_mc`]
  8 [`read (memory :> bytes (z,32)) s1 = q`]
  9 [`read X1 s1 = word_add z (word (32 * i))`]
 10 [`read X19 s1 = temp1`]
 11 [`read X17 s1 = temp0`]
 12 [`(MAYCHANGE [PC] ,,
       MAYCHANGE [memory :> bytes64 (word_add z (word (32 * i)))] ,,
       MAYCHANGE [memory :> bytes64 (word_add z (word (32 * i + 8)))])
      s0
      s1`]
 13 [`read (memory :> bytes64 (word_add z (word (32 * i + 8)))) s1 = temp1`]
 14 [`read PC s1 = word (pc + 4)`]

`eventually arm
 (\s'. (read PC s' = word (pc + 4) /\
        read
        (memory :> bytes (word_add z (word (32 * (i + 1))),8 * (k - 4 * i)))
        s' =
        a /\
        read (memory :> bytes (z,32)) s' = q) /\
       (MAYCHANGE [PC] ,,
        MAYCHANGE [memory :> bytes (word_add z (word (32 * i)),16)])
       s0
       s')
 s1`
*)