adding a couple of calls to monotonicity in the proof of wp_sound

hacl-star · Nov 30, 2018 · 2220ab8 · 2220ab8
1 parent 39a7b31
commit 2220ab8
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/vale/code/arch/x64/X64.Vale.QuickCodes.fst b/vale/code/arch/x64/X64.Vale.QuickCodes.fst
@@ -191,6 +191,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;
@@ -208,6 +209,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
@@ -222,6 +224,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