include{:fstar}{:open} "Vale.Def.Types_s"
include{:fstar}{:open} "Vale.Arch.Types"
include{:fstar}{:open} "Vale.Arch.HeapImpl"
include{:fstar}{:open} "Vale.X64.Machine_s"
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.InsBasic

#verbatim{:interface}
open FStar.Mul
open Vale.Def.Types_s
open Vale.Arch.HeapImpl
open Vale.Arch.Types
open Vale.X64.Machine_s
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.QuickCode
unfold let vale_heap = Vale.X64.Memory.vale_heap
unfold let vale_stack = Vale.X64.Stack_i.vale_stack
open Vale.X64.CPU_Features_s
#endverbatim

#verbatim
open Vale.X64
open Vale.X64.StateLemmas
open Vale.X64.InsLemmas
open Vale.X64.Taint_Semantics
open Vale.X64.CPU_Features_s
open Vale.X64.Memory
open Vale.X64.Stack_i
module I = Vale.X64.Instructions_s
module S = Vale.X64.Machine_Semantics_s
friend Vale.X64.Decls
#reset-options "--initial_fuel 5 --max_fuel 5 --max_ifuel 2 --z3rlimit 20"
#endverbatim

type vale_heap:Type(1) := Vale.X64.Memory.vale_heap;
type vale_stack:Type(1) := Vale.X64.Stack_i.vale_stack;

var ok:bool {:state ok()};
var rax:nat64 {:state reg64(rRax)};
var rbx:nat64 {:state reg64(rRbx)};
var rcx:nat64 {:state reg64(rRcx)};
var rdx:nat64 {:state reg64(rRdx)};
var rsi:nat64 {:state reg64(rRsi)};
var rdi:nat64 {:state reg64(rRdi)};
var rbp:nat64 {:state reg64(rRbp)};
var rsp:nat64 {:state reg64(rRsp)};
var r8:nat64  {:state reg64(rR8)};
var r9:nat64  {:state reg64(rR9)};
var r10:nat64 {:state reg64(rR10)};
var r11:nat64 {:state reg64(rR11)};
var r12:nat64 {:state reg64(rR12)};
var r13:nat64 {:state reg64(rR13)};
var r14:nat64 {:state reg64(rR14)};
var r15:nat64 {:state reg64(rR15)};
var efl:Vale.X64.Flags.t {:state flags()};
var mem_config:int {:state mem_config()};
var mem:vale_heap {:state mem()};
var heap0 :vale_heap {:state mem_heaplet(0 )}{:updates mem};
var heap1 :vale_heap {:state mem_heaplet(1 )}{:updates mem};
var heap2 :vale_heap {:state mem_heaplet(2 )}{:updates mem};
var heap3 :vale_heap {:state mem_heaplet(3 )}{:updates mem};
var heap4 :vale_heap {:state mem_heaplet(4 )}{:updates mem};
var heap5 :vale_heap {:state mem_heaplet(5 )}{:updates mem};
var heap6 :vale_heap {:state mem_heaplet(6 )}{:updates mem};
var heap7 :vale_heap {:state mem_heaplet(7 )}{:updates mem};
var heap8 :vale_heap {:state mem_heaplet(8 )}{:updates mem};
var heap9 :vale_heap {:state mem_heaplet(9 )}{:updates mem};
var heap10:vale_heap {:state mem_heaplet(10)}{:updates mem};
var heap11:vale_heap {:state mem_heaplet(11)}{:updates mem};
var heap12:vale_heap {:state mem_heaplet(12)}{:updates mem};
var heap13:vale_heap {:state mem_heaplet(13)}{:updates mem};
var heap14:vale_heap {:state mem_heaplet(14)}{:updates mem};
var heap15:vale_heap {:state mem_heaplet(15)}{:updates mem};
var stack:vale_stack {:state stack()};
var memLayout:vale_heap_layout {:state mem_layout()};
var stackTaint:memtaint {:state stackTaint()};

operand_type reg64:nat64 :=
| inout rax | inout rbx | inout rcx | inout rdx
| inout rsi | inout rdi | inout rbp | in rsp
| inout r8 | inout r9 | inout r10 | inout r11
| inout r12 | inout r13 | inout r14 | inout r15
;
operand_type shift_amt64:nat64 := in rcx | const;
operand_type reg_opr64:nat64 @ operand64 := reg64;
operand_type Mem64(in h:heaplet, in base:reg64, inline offset:int, ghost b:buffer64, ghost index:int, inline t:taint):int;
operand_type Stack(in base:reg64, inline offset:int, inline t:taint):int;
operand_type dst_opr64:nat64 @ operand64 := reg_opr64 | Mem64 | Stack;
operand_type opr64:nat64 @ operand64 := dst_opr64 | const;

operand_type heaplet:vale_heap @ heaplet_id :=
| inout heap0 | inout heap1 | inout heap2 | inout heap3
| inout heap4 | inout heap5 | inout heap6 | inout heap7
| inout heap8 | inout heap9 | inout heap10 | inout heap11
| inout heap12 | inout heap13 | inout heap14 | inout heap15
;

procedure Mov64(inout dst:dst_opr64, in src:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr_annotate(I.ins_Mov64, S.AnnotateMov64(), dst, src))}
    ensures
        dst == old(src);
{
}

procedure Cmovc64(inout dst:dst_opr64, in src:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Cmovc64, dst, src))}
    reads efl;
    requires
        valid_cf(efl);
    ensures
        if cf(efl) then dst = old(src) else dst = old(dst);
{
}

procedure Add64(inout dst:dst_opr64, in src:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Add64, dst, src))}
    modifies
        efl;
    requires
        src + dst < pow2_64;
    ensures
        dst == old(dst + src);
{
}

procedure Add64Wrap(inout dst:dst_opr64, in src:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Add64, dst, src))}
    modifies
        efl;
    ensures
        dst == old(add_wrap64(dst, src));
        updated_cf(efl, old(dst + src >= pow2_64));
{
}

procedure AddLea64(out dst:dst_opr64, in src1:opr64, in src2:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_AddLea64, dst, src1, src2))}
    requires
        max_one_mem(@src1, @src2);
        src1 + src2 < pow2_64;
    ensures
        dst == old(src1) + old(src2);
{
}

procedure Adc64(inout dst:dst_opr64, in src:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_AddCarry64, dst, src))}
    modifies
        efl;
    requires
        src + dst + 1 < pow2_64;
        valid_cf(efl);
    ensures
        dst == old(dst + src + (if cf(efl) then 1 else 0));
        updated_cf(efl, old(dst + src + (if cf(efl) then 1 else 0)) >= pow2_64);
{
}

procedure Adc64Wrap(inout dst:dst_opr64, in src:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_AddCarry64, dst, src))}
    modifies
        efl;
    requires
        valid_cf(efl);
    ensures
        dst == old(add_wrap64(add_wrap64(dst, src), (if cf(efl) then 1 else 0)));
        updated_cf(efl, old(dst + src + (if cf(efl) then 1 else 0)) >= pow2_64);
{
}

procedure Adcx64Wrap(inout dst:dst_opr64, in src:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Adcx64, dst, src))}
    {:options smtencoding.nl_arith_repr(boxwrap)}
    requires adx_enabled;
    modifies
        efl;
    requires
        valid_cf(efl);
    ensures
        dst == old(add_wrap64(add_wrap64(dst, src), (if cf(efl) then 1 else 0)));
        updated_cf(efl, old(dst + src + (if cf(efl) then 1 else 0)) >= pow2_64);
        maintained_of(efl, old(efl));
{
    assert old(add_wrap64(add_wrap64(dst, src), (if cf(efl) then 1 else 0)) == (dst + src + (if cf(efl) then 1 else 0)) % pow2_64); // REVIEW: shouldn't be necessary
}

procedure Adox64Wrap(inout dst:dst_opr64, in src:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Adox64, dst, src))}
    requires adx_enabled;
    modifies
        efl;
    requires
        valid_of(efl);
    ensures
        dst == old(add_wrap64(add_wrap64(dst, src), (if overflow(efl) then 1 else 0)));
        updated_of(efl, old(dst + src + (if overflow(efl) then 1 else 0)) >= pow2_64);
        maintained_cf(efl, old(efl));
{
}

procedure Sub64(inout dst:dst_opr64, in src:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Sub64, dst, src))}
    requires
        0 <= dst - src;
    modifies
        efl;
    ensures
        dst == old(dst) - old(src);
{
}

procedure Sub64Wrap(inout dst:dst_opr64, in src:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Sub64, dst, src))}
    modifies
        efl;
    ensures
        dst == old(sub_wrap64(dst, src));
        updated_cf(efl, old(dst - src < 0));
{
}

procedure Sbb64(inout dst:dst_opr64, in src:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Sbb64, dst, src))}
    modifies
        efl;
    requires
        valid_cf(efl);
    ensures
        dst == old(sub_wrap64(dst, add_wrap64(src, (if cf(efl) then 1 else 0))));
        updated_cf(efl, old(dst - (src + (if cf(efl) then 1 else 0))) < 0);
{
}

#verbatim
#restart-solver
#push-options "--max_fuel 0 --max_ifuel 0 --using_facts_from 'Prims FStar.UInt'"
let lemma_fundamental_div_mod (a b:nat64) :
  Lemma (pow2_64 * (FStar.UInt.mul_div #64 a b) + (FStar.UInt.mul_mod #64 a b) == a * b)
  =
  FStar.Math.Lemmas.lemma_div_mod (a * b) pow2_64
#pop-options
#endverbatim

ghost procedure lemma_fundamental_div_mod(ghost a:nat64, ghost b:nat64) {:infer_spec} extern;

procedure Mul64Wrap(in src:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Mul64, src))}
    modifies
        efl;
        rax;
        rdx;
    ensures
        pow2_64 * rdx + rax == old(rax * src);
{
    lemma_fundamental_div_mod(old(rax), old(src));
}

procedure Mulx64(out dst_hi:dst_opr64, out dst_lo:dst_opr64, in src:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Mulx64, dst_hi, dst_lo, src))}
    requires bmi2_enabled; @dst_hi != @dst_lo;
    reads
        rdx;
    ensures
        pow2_64 * dst_hi + dst_lo == old(rdx * src);
{
    lemma_fundamental_div_mod(old(rdx), old(src));
}

ghost procedure lemma_mul_nat(ghost x:nat, ghost y:nat) {:infer_spec} extern;
ghost procedure lemma_mul_in_bounds(ghost a:nat64, ghost b:nat64) {:infer_spec} extern;

procedure IMul64(inout dst:dst_opr64, in src:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_IMul64, dst, src))}
    requires
        dst * src < pow2_64;
    modifies
        efl;
    ensures
        dst == old(dst * src);
{
    lemma_mul_nat(old(dst), old(src));
    lemma_mul_in_bounds(old(dst), old(src));
}

procedure Xor64(inout dst:dst_opr64, in src:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr_annotate(I.ins_Xor64, S.AnnotateXor64(), dst, src))}
    modifies
        efl;
    ensures
        dst == old(ixor64(dst, src));
        !overflow(efl);
        !cf(efl);
        valid_cf(efl);
        valid_of(efl);
{
}

procedure And64(inout dst:dst_opr64, in src:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_And64, dst, src))}
    modifies
        efl;
    ensures
        dst == old(iand64(dst, src));
{
}

procedure Shl64(inout dst:dst_opr64, in amt:shift_amt64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Shl64, dst, amt))}
    modifies
        efl;
//    requires
//        0 <= src < 64;
    ensures
        dst == old(ishl64(dst, amt));
{
}

procedure Shr64(inout dst:dst_opr64, in amt:shift_amt64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Shr64, dst, amt))}
    modifies
        efl;
    ensures
        dst == old(ishr64(dst, amt));
{
}

procedure Cpuid_AES()
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Cpuid))}
    requires rax = 1;
    modifies rax; rbx; rcx; rdx;
    ensures
        (iand64(rcx, 0x2000000) > 0) == aesni_enabled;
        (iand64(rcx, 0x2) > 0) == pclmulqdq_enabled;
{
    cpuid_features();
}

procedure Cpuid_Sha()
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Cpuid))}
    requires
        rax = 7;
        rcx = 0;
    modifies rax; rbx; rcx; rdx;
    ensures (iand64(rbx, 0x20000000) > 0) == sha_enabled;
{
    cpuid_features();
}

procedure Cpuid_Adx_Bmi2()
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Cpuid))}
    requires
        rax = 7;
        rcx = 0;
    modifies rax; rbx; rcx; rdx;
    ensures
        (iand64(rbx, 0x100) > 0) == bmi2_enabled;
        (iand64(rbx, 0x80000) > 0) == adx_enabled;
{
    cpuid_features();
}

procedure Cpuid_Avx()
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Cpuid))}
    requires rax = 1;
    modifies rax; rbx; rcx; rdx;
    ensures (iand64(rcx, 0x10000000) > 0) == avx_cpuid_enabled;
{
    cpuid_features();
}

procedure Cpuid_Avx2()
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Cpuid))}
    requires
        rax = 7;
        rcx = 0;
    modifies rax; rbx; rcx; rdx;
    ensures (iand64(rbx, 0x20) > 0) == avx2_cpuid_enabled;
{
    cpuid_features();
}

procedure Cpuid_Sse()
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Cpuid))}
    requires rax = 1;
    modifies rax; rbx; rcx; rdx;
    ensures 
      (iand64(rdx, 0x4000000) > 0) == sse2_enabled;
      (iand64(rcx, 0x80000) > 0) == sse4_1_enabled;
      (iand64(rcx, 0x200) > 0) == ssse3_enabled;
{
    cpuid_features();
}

procedure Cpuid_Movbe()
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Cpuid))}
    requires rax = 1;
    modifies rax; rbx; rcx; rdx;
    ensures (iand64(rcx, 0x400000) > 0) == movbe_enabled;
{
    cpuid_features();
}

procedure Cpuid_Rdrand()
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Cpuid))}
    requires rax = 1;
    modifies rax; rbx; rcx; rdx;
    ensures (iand64(rcx, 0x40000000) > 0) == rdrand_enabled;
{
    cpuid_features();
}

procedure Cpuid_Avx512()
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Cpuid))}
    requires
        rax = 7;
        rcx = 0;
    modifies rax; rbx; rcx; rdx;
    ensures
      (iand64(rbx, 0x10000) > 0) == avx512f_enabled;
      (iand64(rbx, 0x20000) > 0) == avx512dq_enabled;
      (iand64(rbx, 0x40000000) > 0) == avx512bw_enabled;
      (iand64(rbx, 0x80000000) > 0) == avx512vl_enabled;
{
    cpuid_features();
}

procedure Cpuid_Osxsave()
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Cpuid))}
    requires rax = 1;
    modifies rax; rbx; rcx; rdx;
    ensures (iand64(rcx, 0x8000000) > 0) == osxsave_enabled;
{
    cpuid_features();
}

procedure Xgetbv_Avx()
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Xgetbv))}
    requires
        osxsave_enabled;
        rcx = 0;
    modifies rax; rdx;
    ensures
      (iand64(rax, 0x2) > 0) == sse_xcr0_enabled;
      (iand64(rax, 0x4) > 0) == avx_xcr0_enabled;
{
    xgetbv_features();
}

procedure Xgetbv_Avx512()
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr(I.ins_Xgetbv))}
    requires
        osxsave_enabled;
        rcx = 0;
    modifies rax; rdx;
    ensures
      (iand64(rax, 0x20) > 0) == opmask_xcr0_enabled;
      (iand64(rax, 0x40) > 0) == zmm_hi256_xcr0_enabled;
      (iand64(rax, 0x80) > 0) == hi16_zmm_xcr0_enabled;
{
    xgetbv_features();
}

procedure Nat64Equal(out dst:reg_opr64, inout src:reg_opr64)
    {:public}
    {:quick exportOnly}
    modifies efl;
    ensures if old(src = 0xFFFFFFFFFFFFFFFF) then dst = 0 else dst = 1;
{
    Sub64Wrap(src, 0xFFFFFFFFFFFFFFFF);
    Mov64(dst, 0);
    Adc64(dst, 0);
}

procedure Comment(inline c:string)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr_annotate(I.ins_Comment(c), S.AnnotateComment(c)))}
{
    // Do nothing. This is a no-op.
}

procedure LargeComment(inline c:string)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr_annotate(I.ins_LargeComment(c), S.AnnotateLargeComment(c)))}
{
    // Do nothing. This is a no-op.
}

procedure NoNewline()
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr_annotate(I.ins_Space(0), S.AnnotateSpace(0)))}
{
    // Do nothing. This is a no-op.
}

procedure Newline()
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr_annotate(I.ins_Newline, S.AnnotateNewline()))}
{
    // Do nothing. This is a no-op.
}

procedure Space(inline n:nat)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr_annotate(I.ins_Space(n), S.AnnotateSpace(n)))}
{
    // Do nothing. This is a no-op.
}

procedure Prefetchnta(in v:opr64)
    {:public}
    {:quick exportOnly}
    {:instruction mk_ins(make_instr_annotate(I.ins_Prefetchnta, S.AnnotatePrefetchnta(), v))}
{
    // Do nothing. This is (effectively) a no-op.
}