aqjune

version = "3.0.0"
description = "The HOL Light interactive theorem prover"
requires = "camlp5 zarith"
archive(byte) = "hol_lib.cma"
archive(native) = "hol_lib.cmxa"

aqjune

(****** A simple specification about program 'simple_arm.S' *******)

(* If you are using HOL Light Online, this line is not necessary. *)
(* needs "arm/proofs/base.ml";; *)

let simple_arm_mc = new_definition `simple_arm_mc = [
    word 0xe0; word 0x03; word 0x1f; word 0xaa; // arm_MOV X0 XZR
    word 0x00; word 0x04; word 0x00; word 0x91; // arm_ADD X0 X0 (rvalue (word 1))
    word 0x1f; word 0x0c; word 0x00; word 0xf1; // arm_CMP X0 (rvalue (word 3))
    word 0xc1; word 0xff; word 0xff; word 0x54  // arm_BNE (word 2097144)

aqjune

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;;

aqjune

dev-dsk-lebjuney-1d-d3fc5ff7 % make sematest
../tools/run-sematest.sh . 32 "/home/lebjuney/hol-light-ocaml4.14/hollight "
- Child 1 (pid 8752) has started (log path: /tmp/tmp.qeBbXPDRRr)
- Child 2 (pid 8756) has started (log path: /tmp/tmp.I0ALk9exvX)
- Child 3 (pid 8761) has started (log path: /tmp/tmp.DGJxWS09ar)
- Child 4 (pid 8767) has started (log path: /tmp/tmp.uCaV3R0nnS)
- Child 5 (pid 8771) has started (log path: /tmp/tmp.uzG2Tnfrgw)
- Child 6 (pid 8778) has started (log path: /tmp/tmp.TuTNQssTIo)
- Child 7 (pid 8784) has started (log path: /tmp/tmp.hKGajyyESl)

aqjune

dev-dsk-lebjuney-1d-d3fc5ff7 % make sematest
../tools/run-sematest.sh . 32 "/home/lebjuney/hol-light-ocaml4.14/hollight "
- Child 1 (pid 3178) has started (log path: /tmp/tmp.muukON4ZUi)
- Child 2 (pid 3183) has started (log path: /tmp/tmp.sQ1LEwAzA5)
- Child 3 (pid 3187) has started (log path: /tmp/tmp.d6SAmJ6Hfz)
- Child 4 (pid 3193) has started (log path: /tmp/tmp.tUY6sTyOYR)
- Child 5 (pid 3198) has started (log path: /tmp/tmp.q5XSylRFhq)
- Child 6 (pid 3205) has started (log path: /tmp/tmp.MtloMm7gT3)
- Child 7 (pid 3211) has started (log path: /tmp/tmp.cdFrUjdqn6)

aqjune

(* sli     v3.2d, v4.2d, #32 *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x6f605483)`;;

(*   output: - : thm = |- decode (word 1868584067) = SOME (arm_SLI_VEC Q3 Q4 32 64) *)

(* 2. Check that the symbolic output looks ok *)
let code_6f605483 = define `code_6f605483:byte list = [word 0x83; word 0x54; word 0x60; word 0x6f]`;;
let execth = ARM_MK_EXEC_RULE code_6f605483;;
g `ensures arm

aqjune

(* usra v1.2d, v3.2d, #30 *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x6f621461)`;;
(*   output: - : thm = |- decode (word 1868698721) = SOME (arm_USRA_VEC Q1 Q3 30 64 128) *)
(* 2. Check that the symbolic output looks ok *)
let code_6f621461 = define `code_6f621461:byte list = [word 0x61; word 0x14; word 0x62; word 0x6f]`;;
let execth = ARM_MK_EXEC_RULE code_6f621461;;
g `ensures arm
      (\s. aligned_bytes_loaded s (word pc) code_6f621461 /\
           read PC s = word pc)

aqjune

let test_mc =
  define_assert_from_elf "test_mc" "test.o"
[
  0x3dc00000;       (* arm_LDR Q0 X0 (Immediate_Offset (word 0)) *)
  0xa9000c22        (* arm_STP X2 X3 X1 (Immediate_Offset (iword (&0))) *)
];;

let TEST_EXEC = ARM_MK_EXEC_RULE test_mc;;

let STORE_DOES_NOT_TOUCH_LDR_Q = prove(

aqjune

(* ============= *)
(* 1. dup: https://developer.arm.com/documentation/ddi0602/2022-06/SIMD-FP-Instructions/DUP--general---Duplicate-general-purpose-register-to-vector- *)

(* dup v2.2d, x4 (0x4e080c82, 0100 1110 0000 1000 0000 1100 1000 0010) *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x4e080c82)`;;
(*   output: - : thm = |- decode (word 1309150338) = SOME (arm_DUP Q2 X4) *)

(* 2. Check that the symbolic output looks ok *)
let code_4e080c82 = define `code_4e080c82:byte list = [word 0x82; word 0x0c; word 0x08; word 0x4e]`;;

aqjune

#map0 = affine_map<(d0, d1) -> (d0, d1)>
#map1 = affine_map<(d0) -> (d0)>
#map2 = affine_map<(d0, d1) -> (d0)>
module  {
  func @encrypt(%arg0: tensor<18x131072xi64>, %arg1: tensor<18x131072xi64>) -> tensor<18x131072xi64> {
    %cst = arith.constant dense<[1, 131072]> : tensor<2xi64>
    %cst_0 = arith.constant dense<1> : tensor<1xi64>
    %cst_1 = arith.constant dense<131072> : tensor<1xi64>
    %cst_2 = arith.constant dense<[30, 1]> : tensor<2xi64>
    %c18 = arith.constant 18 : index