specification for isqrt

examples/riscv/isqrt/isqrt_propScript.sml

@@ -1,5 +1,9 @@
 open HolKernel boolLib Parse bossLib;
 
+open BasicProvers simpLib metisLib;
+
+open logrootTheory arithmeticTheory pairTheory combinTheory wordsTheory;
+
 open bir_programSyntax bir_program_labelsTheory bir_immTheory;
 
 open isqrtTheory;
@@ -13,20 +17,33 @@ val blocks = (fst o listSyntax.dest_list o dest_BirProgram o snd o dest_eq o con
 
 bir_isqrt_riscv_lift_THM;
 
-(*
-Definition swap_mem_spec_def:
- swap_mem_spec ms =
- let ms'_mem8 = (riscv_mem_store_word (ms.c_gpr ms.procID 0w)
-   (riscv_mem_load_word ms.MEM8 (ms.c_gpr ms.procID 1w)) ms.MEM8)
- in
-   (riscv_mem_store_word (ms.c_gpr ms.procID 1w)
-    (riscv_mem_load_word ms.MEM8 (ms.c_gpr ms.procID 0w)) ms'_mem8)
+Definition SQRT_def:
+ SQRT x = ROOT 2 x
+End
+
+val arith_ss = srw_ss() ++ numSimps.old_ARITH_ss;
+
+Theorem sqrt_thm:
+!x p. SQRT x = let q = p * p in
+      if (q <= x /\ x < q + 2 * p + 1) then p else SQRT x
+Proof
+RW_TAC (arith_ss ++ boolSimps.LET_ss) [SQRT_def] THEN
+  MATCH_MP_TAC ROOT_UNIQUE THEN
+  RW_TAC bool_ss [ADD1,EXP_ADD,EXP_1,DECIDE ``2 = SUC 1``,
+    LEFT_ADD_DISTRIB,RIGHT_ADD_DISTRIB] THEN
+  DECIDE_TAC
+QED
+
+Definition wSQRT_def:
+ wSQRT w = n2w (SQRT (w2n w))
 End
 
-Definition swap_spec_def:
- swap_spec ms = ms with MEM8 := swap_mem_spec ms
+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)
 End
-*)
 
 (* run symbolic execution of BIR to get two symbolic states  *)
 (* connect this back to the riscv state via the lifting theorem *)