val main: Prims.unit
  -> Stack C.exit_code (requires fun h -> uds_is_enabled h) (ensures fun _ _ _ -> True)
val main: Prims.unit
  -> Stack C.exit_code (requires fun h -> uds_is_enabled h) (ensures fun _ _ _ -> True)
let main ()
  : Stack C.exit_code
      (requires fun h -> uds_is_enabled h)
      (ensures fun _ _ _ -> True)
= let s = HWAbstraction.st () in
  recall_st_liveness s;
  let h0 = get () in
  push_frame ();
  let h1 = get () in
  frame_ghost_state loc_none h0 h1;
  let ret = DICE.Engine.Core.dice_main () in
  pop_frame ();
  C.EXIT_SUCCESS
module DICE.Engine.Test

open LowStar.Buffer
open FStar.HyperStack.ST

open HWAbstraction
/
prims.fst.checked LowStar.Buffer.fst.checked HWAbstraction.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked DICE.Engine.Core.fst.checked C.fst.checked
DICE.Engine.Test.fst
_: Prims.unit -> FStar.HyperStack.ST.Stack C.exit_code
Prims.unit C.EXIT_SUCCESS C.exit_code FStar.HyperStack.ST.pop_frame DICE.Engine.Core.dice_return_code DICE.Engine.Core.dice_main HWAbstraction.frame_ghost_state LowStar.Monotonic.Buffer.loc_none FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get FStar.HyperStack.ST.push_frame HWAbstraction.recall_st_liveness HWState.state HWAbstraction.st HWAbstraction.uds_is_enabled Prims.l_True
let main () : Stack C.exit_code (requires fun h -> uds_is_enabled h) (ensures fun _ _ _ -> True) =
  
let s = HWAbstraction.st () in
recall_st_liveness s;
let h0 = get () in
push_frame ();
let h1 = get () in
frame_ghost_state loc_none h0 h1;
let ret = DICE.Engine.Core.dice_main () in
pop_frame ();
C.EXIT_SUCCESS