Upgrade to latest F* master

project-everest · Dec 5, 2018 · c6e4545 · c6e4545
1 parent 2cf0717
commit c6e4545
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/.fstar_version b/.fstar_version
@@ -1 +1 @@
-a762dc29d47dc4c803225af65311a58b1769246e
+d12198861e796fe1fe4adb7aac84fb581d0145f3
diff --git a/fstar/code/arch/x64/X64.Vale.QuickCodes.fst b/fstar/code/arch/x64/X64.Vale.QuickCodes.fst
@@ -189,6 +189,7 @@ let rec wp_compute #a cs qcs mods s0 =
       wp_compute cs qcs' mods s0
 
 let rec wp_sound #a cs qcs mods k s0 =
+  let qcs0 = qcs in
   match qcs with
   | QEmpty g ->
       update_state_mods_refl mods s0;
@@ -206,6 +207,7 @@ let rec wp_sound #a cs qcs mods k s0 =
       let fN' = va_lemma_merge_total (c::cs) s0 fM sM fN sN in
       update_state_mods_weaken qc.mods mods sM s0;
       update_state_mods_trans mods s0 sM sN;
+      wp_monotone (c::cs) qcs0 mods k k_true s0;
       ()
   | QBind _ _ qc qcs ->
       let QProc c' _ wp1' monotone compute proof = qc in
@@ -220,6 +222,7 @@ let rec wp_sound #a cs qcs mods k s0 =
       let fN' = va_lemma_merge_total (c::cs) s0 fM sM fN sN in
       update_state_mods_weaken qc.mods mods sM s0;
       update_state_mods_trans mods s0 sM sN;
+      wp_monotone (c::cs) qcs0 mods k k_true s0;
       ()
   | QGetState f ->
       let c::cs = cs in