include "Vale.X64.InsBasic.vaf"
include "Vale.X64.InsVector.vaf"
include{:fstar}{:open} "Vale.Def.Words.Seq_s"
include{:fstar}{:open} "Vale.Def.Words.Two_s"
include{:fstar}{:open} "Vale.Def.Words.Four_s"
include{:fstar}{:open} "Vale.Def.Types_s"
include{:fstar}{:open} "Vale.Arch.Types"
include{:fstar}{:open} "Vale.X64.Machine_s"
include{:fstar}{:open} "Vale.X64.Memory"
include{:fstar}{:open} "Vale.X64.Stack_i"
include{:fstar}{:open} "Vale.X64.Memory_Sems"
include{:fstar}{:open} "Vale.X64.Stack_Sems"
include{:fstar}{:open} "Vale.X64.State"
include{:fstar}{:open} "Vale.X64.Decls"
include{:fstar}{:open} "Vale.X64.QuickCode"
include{:fstar}{:open} "Vale.X64.CPU_Features_s"

module Vale.X64.InsStack

#verbatim{:interface}
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open Vale.Def.Words.Two_s
open Vale.Def.Words.Four_s
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.Stack_i
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.QuickCode
open Vale.X64.InsBasic
open Vale.X64.InsVector
open Vale.X64.CPU_Features_s
#endverbatim

#verbatim
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.Stack_i
open Vale.X64
open Vale.X64.State
open Vale.X64.StateLemmas
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsVector
open Vale.X64.InsLemmas
module I = Vale.X64.Instructions_s
module BC = Vale.X64.Bytes_Code_s
module S = Vale.X64.Machine_Semantics_s
module P = Vale.X64.Print_s
open Vale.X64.Taint_Semantics

friend Vale.X64.Decls
friend Vale.X64.Stack_i
#reset-options "--initial_fuel 2 --max_fuel 4 --max_ifuel 2 --z3rlimit 50"
#endverbatim

//function operator([]) #[a:Type(0), b:Type(0)](m:FStar.Map.t(a, b), key:a):b extern;
//function operator([]) (m:heap0, b:Vale.X64.Memory.buffer64):fun(int) -> nat64 extern;

procedure Stack_in(in base:reg64, inline offset:int, inline t:taint) returns(o:opr)
    {:operand}
    reads
        stack;
    extern;

procedure Stack_lemma(ghost base:operand64, ghost offset:int, ghost t:taint)
    {:public}
    {:quick exportOnly}
{
}

procedure Pop(out dst:dst_opr64)
    {:public}
    {:quick exportOnly}
    {:instruction Ins(BC.Pop(dst, Public))}
    reads stackTaint;
    modifies rsp; stack;
    requires
        valid_src_stack64(rsp, stack);
        valid_taint_stack64(rsp, Public, stackTaint);
        rsp >= init_rsp(stack) - 4096;
        rsp + 8 <= init_rsp(stack);
    ensures
        dst == load_stack64(old(rsp), old(stack));
        rsp == old(rsp) + 8;
        stack == free_stack64(rsp-8, rsp, old(stack));
{
    lemma_valid_taint_stack64(old(rsp), Public, old(stackTaint));
}

procedure Push(in src:reg_opr64)
    {:public}
    {:quick exportOnly}
    {:instruction Ins(BC.Push(src, Public))}
    modifies
        rsp; stack; stackTaint;
    requires
        rsp <= init_rsp(stack);
        init_rsp(stack) - 4096 <= rsp - 8;
    ensures
        rsp == old(rsp) - 8;
        stack == store_stack64(rsp, old(src), old(stack));
        stackTaint == store_taint_stack64(rsp, Public, old(stackTaint));
{
    equiv_store_stack64(rsp, old(src), old(stack));
}

procedure Pop_Secret(out dst:dst_opr64)
    {:public}
    {:quick exportOnly}
    {:instruction Ins(BC.Pop(dst, Secret))}
    reads stackTaint;
    modifies rsp; stack;
    requires
        valid_src_stack64(rsp, stack);
        valid_taint_stack64(rsp, Secret, stackTaint);
        rsp >= init_rsp(stack) - 4096;
        rsp + 8 <= init_rsp(stack);
    ensures
        dst == load_stack64(old(rsp), old(stack));
        rsp == old(rsp) + 8;
        stack == free_stack64(rsp-8, rsp, old(stack));
{
    lemma_valid_taint_stack64(old(rsp), Secret, old(stackTaint));
}

procedure Push_Secret(in src:reg_opr64)
    {:public}
    {:quick exportOnly}
    {:instruction Ins(BC.Push(src, Secret))}
    modifies
        rsp; stack; stackTaint;
    requires
        rsp <= init_rsp(stack);
        init_rsp(stack) - 4096 <= rsp - 8;
    ensures
        rsp == old(rsp) - 8;
        stack == store_stack64(rsp, old(src), old(stack));
        stackTaint == store_taint_stack64(rsp, Secret, old(stackTaint));
{
    equiv_store_stack64(rsp, old(src), old(stack));
}


procedure Load64_stack(out dst:dst_opr64, in src:reg_opr64, inline offset:int)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr_annotate(I.ins_Mov64, S.AnnotateMov64(), dst, OStack(tuple(MReg(get_reg(src), offset), Public))))}
    reads
        stack; stackTaint;
    requires
        valid_src_stack64(src + offset, stack);
        valid_taint_stack64(src + offset, Public, stackTaint);
    ensures
        dst == old(load_stack64(src + offset, stack));
{
    lemma_valid_taint_stack64(old(src + offset), Public, old(stackTaint));
}

procedure PushXmm(in src:xmm, out tmp:reg_opr64)
    {:public}
    {:quick exportOnly}
    modifies
        rsp; stack; stackTaint;
    requires
        sse_enabled;
        rsp <= init_rsp(stack);
        init_rsp(stack) - 4096 <= rsp - 16;
    ensures
        let src_lo := lo64(src);
        let src_hi := hi64(src);
        stack == old(store_stack64(rsp - 16, src_hi, store_stack64(rsp - 8, src_lo, stack)));
        stackTaint == old(store_taint_stack64(rsp - 16, Public, store_taint_stack64(rsp - 8, Public, stackTaint)));
        rsp == old(rsp) - 16;
{
    Pextrq(tmp, src, 0);
    Push(tmp);
    Pextrq(tmp, src, 1);
    Push(tmp);
}

procedure PopXmm(out dst:xmm, out tmp:reg_opr64, ghost expected_xmm:quad32)
    {:public}
    {:quick exportOnly}
    reads stackTaint;
    modifies rsp; stack;
    requires
        sse_enabled;
        valid_src_stack64(rsp, stack);
        valid_src_stack64(rsp + 8, stack);
        valid_taint_stack64(rsp, Public, stackTaint);
        valid_taint_stack64(rsp + 8, Public, stackTaint);
        hi64(expected_xmm) == load_stack64(rsp, stack);
        lo64(expected_xmm) == load_stack64(rsp+8, stack);
        rsp >= init_rsp(stack) - 4096;
        rsp + 16 <= init_rsp(stack);
    ensures
        dst == expected_xmm;
        rsp == old(rsp) + 16;
        stack == free_stack64(rsp-16, rsp, old(stack));
{
    Pop(tmp);
    Pinsrq(dst, tmp, 1);
    Pop(tmp);
    Pinsrq(dst, tmp, 0);
    push_pop_xmm(expected_xmm, old(dst));
}

procedure PushXmm_Secret(in src:xmm, out tmp:reg_opr64)
    {:public}
    {:quick exportOnly}
    modifies
        rsp; stack; stackTaint;
    requires
        sse_enabled;
        rsp <= init_rsp(stack);
        init_rsp(stack) - 4096 <= rsp - 16;
    ensures
        let src_lo := lo64(src);
        let src_hi := hi64(src);
        stack == old(store_stack64(rsp - 16, src_hi, store_stack64(rsp - 8, src_lo, stack)));
        stackTaint == old(store_taint_stack64(rsp - 16, Secret, store_taint_stack64(rsp - 8, Secret, stackTaint)));
        rsp == old(rsp) - 16;
{
    Pextrq(tmp, src, 0);
    Push_Secret(tmp);
    Pextrq(tmp, src, 1);
    Push_Secret(tmp);
}

procedure PopXmm_Secret(out dst:xmm, out tmp:reg_opr64, ghost expected_xmm:quad32)
    {:public}
    {:quick exportOnly}
    reads stackTaint;
    modifies rsp; stack;
    requires
        sse_enabled;
        valid_src_stack64(rsp, stack);
        valid_src_stack64(rsp + 8, stack);
        valid_taint_stack64(rsp, Secret, stackTaint);
        valid_taint_stack64(rsp + 8, Secret, stackTaint);
        hi64(expected_xmm) == load_stack64(rsp, stack);
        lo64(expected_xmm) == load_stack64(rsp+8, stack);
        rsp >= init_rsp(stack) - 4096;
        rsp + 16 <= init_rsp(stack);
    ensures
        dst == expected_xmm;
        rsp == old(rsp) + 16;
        stack == free_stack64(rsp-16, rsp, old(stack));
{
    Pop_Secret(tmp);
    Pinsrq(dst, tmp, 1);
    Pop_Secret(tmp);
    Pinsrq(dst, tmp, 0);
    push_pop_xmm(expected_xmm, old(dst));
}