examples of relational specifications on riscv states

kth-step · Feb 8, 2024 · 594ed53 · 594ed53
1 parent 90b3406
commit 594ed53
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 5 deletions.
diff --git a/examples/riscv/isqrt/isqrt_propScript.sml b/examples/riscv/isqrt/isqrt_propScript.sml
@@ -39,10 +39,10 @@ Definition wSQRT_def:
 End
 
 Definition isqrt_spec_def:
- isqrt_spec_def ms = 
- let input = ms.c_gpr ms.procID 0w in
- ms with c_gpr := 
-  (\x y. if x = ms.procID /\ y = 0w then (wSQRT input) else ms.c_gpr x y)
+ isqrt_spec_def ms ms' : bool =
+  let input = ms.c_gpr ms.procID 0w in
+  let output = ms'.c_gpr ms'.procID 0w in
+  output = wSQRT input
 End
 
 (* run symbolic execution of BIR to get two symbolic states  *)

diff --git a/examples/riscv/swap/swap_propScript.sml b/examples/riscv/swap/swap_propScript.sml
@@ -22,8 +22,12 @@ Definition swap_mem_spec_def:
     (riscv_mem_load_word ms.MEM8 (ms.c_gpr ms.procID 0w)) ms'_mem8)
 End
 
+Definition swap_spec_output_def:
+ swap_spec_output ms : riscv_state = ms with MEM8 := swap_mem_spec ms
+End
+
 Definition swap_spec_def:
- swap_spec ms = ms with MEM8 := swap_mem_spec ms
+ swap_spec ms ms' : bool = (ms'.MEM8 = swap_mem_spec ms)
 End
 
 (* run symbolic execution of BIR to get two symbolic states  *)