diff --git a/examples/riscv/isqrt/isqrt_propScript.sml b/examples/riscv/isqrt/isqrt_propScript.sml index 51138bbcd..8fc0d9c9d 100644 --- 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 index db3821278..f35c8db85 100644 --- 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 *)