#include "kernel/prelude/kernel_prelude.hats"

#define ATS_DYNLOADFLAG 0

staload "./tss.sats"

staload UN = "prelude/SATS/unsafe.sats"

var tss : tss_t // Task State Segment
var stack1 : stack // Double fault stack

implement tss_init() : void = let
  extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (tss_t@l)
  prval (pf, fpf) = __assert (addr@(tss)) // takeout proof  UNSAFE:
  val sp1 = @{a = ptr_add<uint8>(addr@(stack1),STACK_SIZE)} 
in
  tss.ist.IS1 := sp1;
  let prval () = fpf(pf) in end
end