- Adapted islaris to the new trace syntax for the enumerate types and…

… values produced by the new isla-footprint

- Changed Makefile instructions for coq-bbv for `make deps`: use coq-bbv.1.4 instead of 1.3 and install via opam

deps/Makefile

@@ -1,22 +1,13 @@
 SAIL_COMMIT=605cd3cffe4b18fb5d0a99beef5d6ee33e1a7dcb
-BBV_COMMIT=6144e214583b72182a4ed89e4328ea62ba766e2e
 
 all: sail-riscv-coq
 .PHONY: all
 
 sail-%.tar.gz:
 	wget "https://github.com/rems-project/sail/archive/$*.tar.gz" -O $@
 
-bbv-%.tar.gz:
-	wget "https://github.com/mit-plv/bbv/archive/$*.tar.gz" -O $@
-
-# TODO: maybe add opam install z3?
-bbv: bbv-$(BBV_COMMIT).tar.gz
-	rm -rf coq-bbv
-	tar xf bbv-$(BBV_COMMIT).tar.gz
-	mv "bbv-${BBV_COMMIT}" coq-bbv
-	cp coq-bbv-1.3.opam coq-bbv/opam
-	opam pin add ./coq-bbv -n
+bbv: 
+	opam pin --yes coq-bbv 1.4
 .PHONY: bbv
 
 # TODO: maybe add opam install z3?

etc/aarch64_isla_coq.toml

@@ -14,6 +14,7 @@ write_exclusives = ["Write_exclusive", "Write_exclusive_release"]
 assembler = "aarch64-linux-gnu-as -march=armv8.1-a"
 objdump = "aarch64-linux-gnu-objdump"
 linker = "aarch64-linux-gnu-ld"
+nm = "aarch64-linux-gnu-nm"
 
 [mmu]
 page_table_base = "0x300000"

etc/aarch64_isla_coq_el1.toml

@@ -14,6 +14,7 @@ write_exclusives = ["Write_exclusive", "Write_exclusive_release"]
 assembler = "aarch64-linux-gnu-as -march=armv8.1-a"
 objdump = "aarch64-linux-gnu-objdump"
 linker = "aarch64-linux-gnu-ld"
+nm = "aarch64-linux-gnu-nm"
 
 [mmu]
 page_table_base = "0x300000"

etc/aarch64_isla_coq_pkvm.toml

@@ -14,6 +14,7 @@ write_exclusives = ["Write_exclusive", "Write_exclusive_release"]
 assembler = "aarch64-linux-gnu-as -march=armv8.1-a"
 objdump = "aarch64-linux-gnu-objdump"
 linker = "aarch64-linux-gnu-ld"
+nm = "aarch64-linux-gnu-nm"
 
 [mmu]
 page_table_base = "0x300000"

etc/riscv64_isla_coq.toml

@@ -11,6 +11,10 @@ write_exclusives = ["Write_RISCV_conditional", "Write_RISCV_conditional_release"
 assembler = "riscv64-linux-gnu-as -march=rv64imac"
 objdump = "riscv64-linux-gnu-objdump"
 linker = "riscv64-linux-gnu-ld"
+nm = "riscv64-linux-gnu-nm"
+
+[const_primops]
+platform_write_mem_ea = false
 
 # Currently not used for RISC-V
 [mmu]

frontend/coq_pp.ml

@@ -88,7 +88,7 @@ let pp_lrng ff _ =
 let pp_var_name ff i =
   Format.fprintf ff "%a" pp_Z i
 
-let pp_register_name ff r =
+let pp_sail_name ff r =
   Format.fprintf ff "%S" r
 
 let remove_zeroes digits =
@@ -127,13 +127,13 @@ let pp_bv ff s =
 let pp_accessor ff a =
   let pp fmt = Format.fprintf ff fmt in
   match a with
-  | Ast.Field(r) -> pp "Field %a" pp_register_name r
+  | Ast.Field(r) -> pp "Field %a" pp_sail_name r
 
 let pp_accessor_list ff l =
   pp_list pp_accessor ff (match l with Ast.Nil -> [] | Ast.Cons(l) -> l)
 
 let pp_enum_id ff i =
-  Format.fprintf ff "(Mk_enum_id %i%%nat)" i
+  Format.fprintf ff "\"%s\"" i  
 
 let rec pp_ty ff ty =
   let pp fmt = Format.fprintf ff fmt in
@@ -214,11 +214,11 @@ let pp_manyop ff o =
   | Ast.Concat         -> pp "Concat"
 
 let pp_enum_ctor ff n =
-  Format.fprintf ff "Mk_enum_ctor %i%%nat" n
+  Format.fprintf ff "\"%s\"" n
 
 let pp_enum ff e =
   let pp fmt = Format.fprintf ff fmt in
-  pp "(%a, %a)" pp_enum_id (fst e) pp_enum_ctor (snd e)
+  pp "%a" pp_enum_ctor e
 
 let pp_base_val ff v =
   let pp fmt = Format.fprintf ff fmt in
@@ -236,7 +236,7 @@ let pp_assume_val ff v =
   let pp fmt = Format.fprintf ff fmt in
   match v with
   | Ast.AVal_Var(r,l)  ->
-      pp "AVal_Var %a %a" pp_register_name r pp_accessor_list l
+      pp "AVal_Var %a %a" pp_sail_name r pp_accessor_list l
   | Ast.AVal_Bool(b)      ->
       pp "AVal_Bool %b" b
   | Ast.AVal_Bits(s)      ->
@@ -261,11 +261,11 @@ let rec pp_valu ff v =
       pp "RegVal_List %a" (pp_list pp_valu) l
   | Ast.RegVal_Struct(l)         ->
       let pp_elt ff (r, v) =
-        Format.fprintf ff "(%a, %a)" pp_register_name r pp_valu v
+        Format.fprintf ff "(%a, %a)" pp_sail_name r pp_valu v
       in
       pp "RegVal_Struct %a" (pp_list pp_elt) l
   | Ast.RegVal_Constructor(r, v) ->
-      pp "RegVal_Constructor %a (%a)" pp_register_name r pp_valu v
+      pp "RegVal_Constructor %a (%a)" pp_sail_name r pp_valu v
   | Ast.RegVal_Poison            ->
       pp "RegVal_Poison"
 
@@ -311,8 +311,8 @@ let pp_smt ff e =
       pp "DefineConst %a (%a)" pp_var_name i pp_exp e
   | Ast.Assert(e)          ->
       pp "Assert (%a)" pp_exp e
-  | Ast.DefineEnum(i)      ->
-      pp "DefineEnum %a" pp_Z i
+  | Ast.DefineEnum(name,len,l)      ->
+      pp "DefineEnum %a %a %a" pp_sail_name name pp_Z len (pp_list pp_sail_name) l   
 
 let pp_event ff e =
   let pp fmt = Format.fprintf ff fmt in
@@ -322,10 +322,10 @@ let pp_event ff e =
   | Ast.Branch(i,s,a)              ->
       pp "Branch %a %a %a" pp_Z i pp_str s pp_lrng a
   | Ast.ReadReg(r,l,v,a)           ->
-      pp "ReadReg %a %a (%a) %a" pp_register_name r pp_accessor_list l
+      pp "ReadReg %a %a (%a) %a" pp_sail_name r pp_accessor_list l
         pp_valu v pp_lrng a
   | Ast.WriteReg(r,l,v,a)          ->
-      pp "WriteReg %a %a (%a) %a" pp_register_name r pp_accessor_list l
+      pp "WriteReg %a %a (%a) %a" pp_sail_name r pp_accessor_list l
         pp_valu v pp_lrng a
   | Ast.ReadMem(v1,v2,v3,i,v,a)    ->
       (* TODO: We remove the kind information since it is quite big and not used.
@@ -362,18 +362,20 @@ let pp_event ff e =
   | Ast.SleepRequest(a)            ->
       pp "SleepRequest %a" pp_lrng a
   | Ast.AssumeReg(r,l,v,a)         ->
-      pp "AssumeReg %a %a (%a) %a" pp_register_name r pp_accessor_list l
+      pp "AssumeReg %a %a (%a) %a" pp_sail_name r pp_accessor_list l
         pp_valu v pp_lrng a
   | Ast.Assume(e,a)                ->
       pp "Assume (%a) %a" pp_a_exp e pp_lrng a
   | Ast.FunAssume(r,v,args,a)      ->
-      pp "FunAssume %a %a %a %a" pp_register_name r pp_valu v pp_arg_list args pp_lrng a
+      pp "FunAssume %a %a %a %a" pp_sail_name r pp_valu v pp_arg_list args pp_lrng a
   | Ast.UseFunAssume(r,v,args,a)   ->
-      pp "UseFunAssume %a %a %a %a" pp_register_name r pp_valu v pp_arg_list args pp_lrng a
+      pp "UseFunAssume %a %a %a %a" pp_sail_name r pp_valu v pp_arg_list args pp_lrng a
   | Ast.AbstractCall(r,v,args,a)   ->
-      pp "AbstractCall %a %a %a %a" pp_register_name r pp_valu v pp_arg_list args pp_lrng a
-  | Ast.AbstractPrimop(r,v,args,a)   ->
-      pp "AbstractPrimop %a %a %a %a" pp_register_name r pp_valu v pp_arg_list args pp_lrng a
+      pp "AbstractCall %a %a %a %a" pp_sail_name r pp_valu v pp_arg_list args pp_lrng a
+  | Ast.AbstractPrimop(r,v,args,a) ->
+      pp "AbstractPrimop %a %a %a %a" pp_sail_name r pp_valu v pp_arg_list args pp_lrng a
+  | Call (_, _)                    -> () (* TODO: fill in here? *)
+  | Return (_, _)                  -> () (* TODO: fill in here? *)
 
 (** [pp_trace_def name] is a pretty-printer for the Coq definition of a trace,
 with given definition name [name]. *)

frontend/decomp.ml

@@ -84,7 +84,7 @@ let event_filter : Arch.t -> int -> event -> bool = fun arch i e ->
   | Smt(Assert(_), _)                                    -> i = 0
   | Cycle(_)
   | MarkReg(_, _, _)
-  | Smt(DefineEnum(_), _)                                -> false
+  | Smt(DefineEnum(_,_,_), _)                                -> false
   | _                                                    -> true
 
 (** [gen_coq arch name isla_f coq_f] processes Isla file [isla_f] and produces

instructions/binary_search_riscv64/a0.v

@@ -4,10 +4,10 @@ Definition a0 : isla_trace :=
   Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
   Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
-  Smt (DefineConst 14%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 13%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xffffffffffffffc0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  WriteReg "x2" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DefineConst 3%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xffffffffffffffc0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  WriteReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
   WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
   tnil
 .

instructions/binary_search_riscv64/a10.v

@@ -14,27 +14,27 @@ Definition a10 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 21%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 35%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 35%Z)) Mk_annot :t:
-  Smt (DeclareConst 53%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x18" [] (RegVal_Base (Val_Symbolic 53%Z)) Mk_annot :t:
-  Smt (DefineConst 61%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 67%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 71%Z Ty_Bool) Mk_annot :t:
-  WriteMem (RegVal_Base (Val_Symbolic 71%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 21%Z)) (RegVal_Base (Val_Symbolic 53%Z)) 8%N None Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x18" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t:
+  Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t:
+  WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .

instructions/binary_search_riscv64/a10_spec.v

@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.binary_search_riscv64.a10.
 
 Lemma a10_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some a10) ⊢
-  instr_body pc (sd_spec pc "x18" "x2" (32)).
+  instr pc (Some a10)
+  ⊢ instr_body pc (sd_spec pc "x18" "x2" (32)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.

instructions/binary_search_riscv64/a14.v

@@ -14,27 +14,27 @@ Definition a14 : isla_trace :=
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
+  Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
   Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
   Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
-  Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
-  Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
-  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
-  Smt (DefineConst 21%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
+  Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
+  ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
   ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t:
-  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 6%Z)) Mk_annot :t:
-  Smt (DeclareConst 35%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 35%Z)) Mk_annot :t:
-  Smt (DeclareConst 53%Z (Ty_BitVec 64%N)) Mk_annot :t:
-  ReadReg "x19" [] (RegVal_Base (Val_Symbolic 53%Z)) Mk_annot :t:
-  Smt (DefineConst 61%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DefineConst 67%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
-  Smt (DeclareConst 71%Z Ty_Bool) Mk_annot :t:
-  WriteMem (RegVal_Base (Val_Symbolic 71%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 21%Z)) (RegVal_Base (Val_Symbolic 53%Z)) 8%N None Mk_annot :t:
-  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%Z)) Mk_annot :t:
+  ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
+  Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t:
+  Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t:
+  ReadReg "x19" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t:
+  Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t:
+  WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t:
+  WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
   tnil
 .

instructions/binary_search_riscv64/a14_spec.v

@@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
 Require Export isla.instructions.binary_search_riscv64.a14.
 
 Lemma a14_spec `{!islaG Σ} `{!threadG} pc:
-  instr pc (Some a14) ⊢
-  instr_body pc (sd_spec pc "x19" "x2" (24)).
+  instr pc (Some a14)
+  ⊢ instr_body pc (sd_spec pc "x19" "x2" (24)).
 Proof.
   iStartProof.
   repeat liAStep; liShow.