include "../arch/x64/Vale.X64.InsBasic.vaf"
include "../arch/x64/Vale.X64.InsMem.vaf"
include{:fstar}{:open} "Vale.X64.QuickCode"
include{:fstar}{:open} "Vale.X64.QuickCodes"

module Vale.Test.X64.Memcpy

#verbatim{:interface}{:implementation}
open Vale.Arch.HeapImpl
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsMem
#reset-options "--z3rlimit 20"
#endverbatim

procedure Copy16(inline t:taint, ghost bsrc:buffer64, ghost bdst:buffer64)
    requires/ensures
        locs_disjoint(list(loc_buffer(bsrc), loc_buffer(bdst)));
        validSrcAddrs64(heap0, rsi, bsrc, 2, memLayout, t);
        validDstAddrs64(heap0, rdi, bdst, 2, memLayout, t);
    ensures
        forall(i) 0 <= i && i < 2 ==> buffer64_read(bdst, i, heap0) == buffer64_read(bsrc, i, heap0);
        modifies_mem(loc_buffer(bdst), old(heap0), heap0);
    reads
        rsi; rdi; memLayout;
    modifies
        rax; rcx;
        heap0;
{
    Load64_buffer(heap0, rax, rsi, 0, t, bsrc, 0);
    Load64_buffer(heap0, rcx, rsi, 8, t, bsrc, 1);
    Store64_buffer(heap0, rdi, rax, 0, t, bdst, 0);
    Store64_buffer(heap0, rdi, rcx, 8, t, bdst, 1);
}

/*
procedure Copy64()
    requires/ensures
        rsi + 64 <= rdi;
        forall(i){Map.contains(heap0, i)} rsi <= i < rsi + 64 && (i - rsi) % 8 == 0 ==> Map.contains(heap0, i);
        forall(i){Map.contains(heap0, i)} rdi <= i < rdi + 64 && (i - rdi) % 8 == 0 ==> Map.contains(heap0, i);
    ensures
        forall(i) 0 <= i && i < 64 && i % 8 == 0 ==> heap0[rdi + i] == heap0[rsi + i];
    reads
        rsi; rdi;
    modifies
        rax; rbx; rcx; rdx; rbp;
        heap0;
{
    assert{:fast_block} true;
    Load64(rax, rsi, 0);
    Load64(rbx, rsi, 8);
    Load64(rcx, rsi, 16);
    Load64(rdx, rsi, 24);
    Load64(rbp, rsi, 32);
    Store64(rdi, rax, 0);
    Store64(rdi, rbx, 8);
    Store64(rdi, rcx, 16);
    Store64(rdi, rdx, 24);
    Store64(rdi, rbp, 32);
    Load64(rax, rsi, 40);
    Load64(rbx, rsi, 48);
    Load64(rcx, rsi, 56);
    Store64(rdi, rax, 40);
    Store64(rdi, rbx, 48);
    Store64(rdi, rcx, 56);
}

procedure Copy128()
    requires/ensures
        rsi + 128 <= rdi;
        forall(i){Map.contains(heap0, i)} rsi <= i < rsi + 128 && (i - rsi) % 8 == 0 ==> Map.contains(heap0, i);
        forall(i){Map.contains(heap0, i)} rdi <= i < rdi + 128 && (i - rdi) % 8 == 0 ==> Map.contains(heap0, i);
    ensures
        forall(i) 0 <= i && i < 128 && i % 8 == 0 ==> heap0[rdi + i] == heap0[rsi + i];
    reads
        rsi; rdi;
    modifies
        rax; rbx; rcx; rdx; rbp;
        heap0;
{
    assert{:fast_block} true;
    Load64(rax, rsi, 0);
    Load64(rbx, rsi, 8);
    Load64(rcx, rsi, 16);
    Load64(rdx, rsi, 24);
    Load64(rbp, rsi, 32);
    Store64(rdi, rax, 0);
    Store64(rdi, rbx, 8);
    Store64(rdi, rcx, 16);
    Store64(rdi, rdx, 24);
    Store64(rdi, rbp, 32);
    Load64(rax, rsi, 40);
    Load64(rbx, rsi, 48);
    Load64(rcx, rsi, 56);
    Load64(rdx, rsi, 64);
    Load64(rbp, rsi, 72);
    Store64(rdi, rax, 40);
    Store64(rdi, rbx, 48);
    Store64(rdi, rcx, 56);
    Store64(rdi, rdx, 64);
    Store64(rdi, rbp, 72);
    Load64(rax, rsi, 80);
    Load64(rbx, rsi, 88);
    Load64(rcx, rsi, 96);
    Load64(rdx, rsi, 104);
    Load64(rbp, rsi, 112);
    Store64(rdi, rax, 80);
    Store64(rdi, rbx, 88);
    Store64(rdi, rcx, 96);
    Store64(rdi, rdx, 104);
    Store64(rdi, rbp, 112);
    Load64(rax, rsi, 120);
    Store64(rdi, rax, 120);
}
*/