fixing a regression in Interop.fst; bumping an rlimit in fastmul

hacl-star · Dec 1, 2018 · 6e9175e · 6e9175e
1 parent 2220ab8
commit 6e9175e
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 9 deletions.
diff --git a/vale/code/arch/x64/Interop.fst b/vale/code/arch/x64/Interop.fst
@@ -257,8 +257,8 @@ let down_mem mem addrs ptrs =
   let heap = Map.restrict Set.empty heap in
   down_mem_aux ptrs addrs mem ptrs [] heap
 
-private
-let rec frame_down_mem_aux (ptrs:list b8{list_disjoint_or_eq ptrs})
+//private
+val frame_down_mem_aux (ptrs:list b8{list_disjoint_or_eq ptrs})
   (addrs:addr_map)
   (mem:HS.mem)
   (ps:list b8)
@@ -268,8 +268,9 @@ let rec frame_down_mem_aux (ptrs:list b8{list_disjoint_or_eq ptrs})
    forall i. (forall (b:b8{List.memP b ptrs}). 
       let base = addrs b in
       i < base \/ i >= base + B.length b) ==>
-      h.[i] == heap.[i]) =
-  admit(); //NS: 11/30/2018
+      h.[i] == heap.[i])
+
+let rec frame_down_mem_aux ptrs addrs mem ps accu h =
   match ps with
   | [] -> ()
   | a::q ->
@@ -282,14 +283,18 @@ let rec frame_down_mem_aux (ptrs:list b8{list_disjoint_or_eq ptrs})
     correct_down_p_frame mem addrs h a;
     assert (forall p. List.memP p accu ==> disjoint_or_eq p a);
     domain_write_buffer a h mem addrs;
-    addrs_set_concat accu a addrs;    
+    addrs_set_concat accu a addrs;
+    let new_heap' = down_mem_aux ptrs addrs mem q (a::accu) new_heap in
     frame_down_mem_aux ptrs addrs mem q (a::accu) new_heap;
     frame_write_vale_mem contents length addr 0 h;
-    ()
-
+    assert_norm (down_mem_aux ptrs addrs mem (a::q) accu h ==
+                 new_heap') //NS: 11/30, unfolding a recursive function via smt
+                            //requires non-trivial proofs of typing;
+                            //do it via normalization instead
+
 let same_unspecified_down mem1 mem2 addrs ptrs =
   let heap = Map.const 0 in
-  let heap = Map.restrict Set.empty heap in
+  let heap = Map.restrict Set.empty heap in 
   let heapf1 = down_mem_aux ptrs addrs mem1 ptrs [] heap in
   let heapf2 = down_mem_aux ptrs addrs mem2 ptrs [] heap in
   frame_down_mem_aux ptrs addrs mem1 ptrs [] heap;

diff --git a/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/X64.FastMul.vaf b/vale/code/thirdPartyPorts/rfc7748/curve25519/x64/X64.FastMul.vaf
@@ -46,7 +46,7 @@ const int_canon:tactic extern;
 ghost procedure assert_by_tactic(ghost p:prop, ghost t:tactic) extern;
 
 
-#reset-options "--z3rlimit 20"
+#reset-options "--z3rlimit 100"
 procedure{:quick} fast_multiply_a0b(
     ghost dst_b:buffer64,
     ghost inA_b:buffer64,