remove straggling admits

project-everest · Feb 8, 2024 · ebe6941 · ebe6941
1 parent 318604e
commit ebe6941
Showing 1 changed file with 5 additions and 29 deletions.
diff --git a/steel/apps/kvstore/Zeta.Steel.Application.fst b/steel/apps/kvstore/Zeta.Steel.Application.fst
@@ -173,32 +173,6 @@ let vget_impl (#tsm:TSM.thread_state_model)
       return b
     end
 
-
-let intro_verify_runapp_success
-    (tsm:M.thread_state_model)
-    (t:V.thread_state_t)
-    (pl: runApp_payload)
-    (out_bytes:Ghost.erased bytes)
-    (out_offset:U32.t)
-    (out:A.array U8.t)
-    (out_bytes':Ghost.erased bytes)
-    (wrote:_)
- : STT verify_runapp_result
-    (V.thread_state_inv t (M.verify_step_model tsm (RunApp pl)) `star` //tsm' is the new state of the thread
-     A.pts_to out full_perm out_bytes' `star`
-     pure (n_out_bytes tsm (M.verify_step_model tsm (RunApp pl)) out_offset wrote out_bytes out_bytes'))
-    (fun res ->
-      verify_runapp_entry_post tsm t pl out_bytes out_offset out res)
-= rewrite (A.pts_to out full_perm out_bytes')
-          (array_pts_to out out_bytes');
-  intro_exists (Ghost.reveal out_bytes') (fun (out_bytes':Seq.seq U8.t) ->
-        (let tsm' = M.verify_step_model tsm (RunApp pl) in
-         V.thread_state_inv t tsm' `star` //tsm' is the new state of the thread
-         array_pts_to out out_bytes' `star`
-         pure (n_out_bytes tsm tsm' out_offset wrote out_bytes out_bytes')));
-  return (Run_app_success wrote)
-
-
 //
 // The main vget function
 //
@@ -298,9 +272,10 @@ let run_vget
                             wrote
                             out_bytes
                             out_bytes);
-              admit_();  //without this, the steel tactic loops for a very long time consuming lots of memory
+              rewrite (V.thread_state_inv t _)
+                      (V.thread_state_inv t (M.verify_step_model tsm (RunApp pl)));
+
               return (Run_app_success wrote)
-              // intro_verify_runapp_success tsm t pl out_bytes out_offset out out_bytes wrote
 
             end
             else begin
@@ -504,7 +479,8 @@ let run_vput
                             wrote
                             out_bytes
                             out_bytes);
-              admit_(); //without this, the steel tactic loops for a very long time consuming lots of memory
+              rewrite (V.thread_state_inv t _)
+                      (V.thread_state_inv t (M.verify_step_model tsm (RunApp pl)));
               return (Run_app_success wrote)
             end
             else begin