val lemma_preserve_valid64 (m m': S.machine_heap)
    : Lemma (requires Set.equal (Map.domain m) (Map.domain m'))
      (ensures
        (forall (i: int). {:pattern (S.valid_addr64 i m')}
            S.valid_addr64 i m ==> S.valid_addr64 i m'))
let lemma_preserve_valid64 (m m':S.machine_heap) : Lemma
  (requires Set.equal (Map.domain m) (Map.domain m'))
  (ensures (forall (i:int).{:pattern (S.valid_addr64 i m')}
    S.valid_addr64 i m ==> S.valid_addr64 i m'))
  =
  reveal_opaque (`%S.valid_addr64) S.valid_addr64
val lemma_preserve_valid64 (m m': S.machine_heap)
    : Lemma (requires Set.equal (Map.domain m) (Map.domain m'))
      (ensures
        (forall (i: int). {:pattern (S.valid_addr64 i m')}
            S.valid_addr64 i m ==> S.valid_addr64 i m'))
let lemma_preserve_valid64 (m m': S.machine_heap)
    : Lemma (requires Set.equal (Map.domain m) (Map.domain m'))
      (ensures
        (forall (i: int). {:pattern (S.valid_addr64 i m')}
            S.valid_addr64 i m ==> S.valid_addr64 i m')) =
reveal_opaque (`%S.valid_addr64) S.valid_addr64
Vale.X64.Leakage_Ins.fst.checked
Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Leakage_s.fst.checked Vale.X64.Leakage_Helpers.fst.checked Vale.X64.Instruction_s.fsti.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Lib.Set.fsti.checked Vale.Lib.MapTree.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.Types.fsti.checked Vale.Arch.MachineHeap_s.fst.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.Classical.fsti.checked
Vale.X64.Leakage_Ins.fst
Vale.Arch.MachineHeap_s.machine_heap FStar.Pervasives.reveal_opaque Prims.int Prims.bool Vale.Arch.MachineHeap_s.valid_addr64 Prims.unit FStar.Set.equal FStar.Map.domain Vale.Def.Types_s.nat8 Prims.squash Prims.l_Forall Prims.l_imp Prims.b2t Prims.Nil FStar.Pervasives.pattern
module Vale.X64.Leakage_Ins
open FStar.Mul
open Vale.Arch.MachineHeap_s
open Vale.Arch.Heap
open Vale.X64.Machine_s
open Vale.X64.Instruction_s
module BC = Vale.X64.Bytes_Code_s
module S = Vale.X64.Machine_Semantics_s
open Vale.X64.Leakage_s
open Vale.X64.Leakage_Helpers

unfold let (.[]) = Map.sel
unfold let (.[]<-) = Map.upd

unfold let obs_args = S.obs_args
unfold let obs_inouts = S.obs_inouts
unfold let machine_eval_code = S.machine_eval_code

let reveal_machine_eval_code_ins (i:S.ins) (s:S.machine_state) : Lemma
  (requires True)
  (ensures S.machine_eval_code_ins i s == S.machine_eval_code_ins_def i s)
  [SMTPat (S.machine_eval_code_ins i s)]
  =
  reveal_opaque (`%S.machine_eval_code_ins) S.machine_eval_code_ins

let rec check_if_consumes_fixed_time_args
    (args:list instr_operand) (oprs:instr_operands_t_args args) (ts:analysis_taints)
  : Pure bool
    (requires True)
    (ensures fun b -> b ==> (forall (s1 s2:S.machine_state).{:pattern (constTimeInvariant ts.lts s1 s2)}
      constTimeInvariant ts.lts s1 s2 ==> obs_args args oprs s1 == obs_args args oprs s2))
  =
  allow_inversion maddr;
  allow_inversion tmaddr;
  match args with
  | [] -> true
  | (IOpEx i)::args ->
    let ((o:instr_operand_t i), (oprs:instr_operands_t_args args)) = coerce oprs in
    let b' =
      match i with
      | IOp64 -> operand_does_not_use_secrets #nat64 #reg_64 o ts
      | IOpXmm -> operand_does_not_use_secrets #quad32 #reg_xmm o ts
      in
    let b'' = check_if_consumes_fixed_time_args args oprs ts in
    b' && b''
  | (IOpIm i)::args ->
    let b' =
      match i with
      | IOp64One o -> operand_does_not_use_secrets o ts
      | IOpXmmOne o -> operand_does_not_use_secrets o ts
      | IOpFlagsCf -> true
      | IOpFlagsOf -> true
      in
    let b'' = check_if_consumes_fixed_time_args args (coerce oprs) ts in
    b' && b''

let check_if_consumes_fixed_time_outs_explicit
    (i:instr_operand_explicit) (o:instr_operand_t i)
    (ts:analysis_taints) (t_out:taint)
  : bool
  =
  match i with
  | IOp64 -> operand_does_not_use_secrets #nat64 #reg_64 o ts && operand_taint_allowed #nat64 #reg_64 o t_out
  | IOpXmm -> operand_does_not_use_secrets #quad32 #reg_xmm o ts && operand_taint_allowed #quad32 #reg_xmm o t_out

let check_if_consumes_fixed_time_outs_implicit
    (i:instr_operand_implicit) (ts:analysis_taints) (t_out:taint)
  : bool
  =
  match i with
  | IOp64One o -> operand_does_not_use_secrets o ts && operand_taint_allowed o t_out
  | IOpXmmOne o -> operand_does_not_use_secrets o ts && operand_taint_allowed o t_out
  | IOpFlagsCf -> true
  | IOpFlagsOf -> true

let rec check_if_consumes_fixed_time_outs
    (outs:list instr_out) (args:list instr_operand) (oprs:instr_operands_t outs args)
    (ts:analysis_taints) (t_out:taint)
  : Pure bool
    (requires True)
    (ensures fun b -> b ==> (forall (s1 s2:S.machine_state).{:pattern (constTimeInvariant ts.lts s1 s2)}
      constTimeInvariant ts.lts s1 s2 ==> obs_inouts outs args oprs s1 == obs_inouts outs args oprs s2))
  =
  allow_inversion maddr;
  allow_inversion tmaddr;
  allow_inversion operand64;
  allow_inversion operand128;
  match outs with
  | [] -> check_if_consumes_fixed_time_args args oprs ts
  | (_, IOpEx i)::outs ->
    let ((o:instr_operand_t i), (oprs:instr_operands_t outs args)) = coerce oprs in
    let b' = check_if_consumes_fixed_time_outs_explicit i o ts t_out in
    let b'' = check_if_consumes_fixed_time_outs outs args oprs ts t_out in
    b' && b''
  | (_, IOpIm i)::outs ->
    let b' = check_if_consumes_fixed_time_outs_implicit i ts t_out in
    let b'' = check_if_consumes_fixed_time_outs outs args (coerce oprs) ts t_out in
    b' && b''

#restart-solver
#reset-options "--z3rlimit 300"
let rec lemma_args_taint
    (outs:list instr_out) (args:list instr_operand)
    (f:instr_args_t outs args) (oprs:instr_operands_t_args args)
    (ts:analysis_taints) (s1 s2:S.machine_state)
  : Lemma
    (requires
      constTimeInvariant ts.lts s1 s2 /\
      Some? (S.instr_apply_eval_args outs args f oprs s1) /\
      Some? (S.instr_apply_eval_args outs args f oprs s2) /\
      check_if_consumes_fixed_time_args args oprs ts /\
      args_taint args oprs ts == Public)
    (ensures
      S.instr_apply_eval_args outs args f oprs s1 ==
      S.instr_apply_eval_args outs args f oprs s2)
  =
  allow_inversion maddr;
  allow_inversion tmaddr;
  allow_inversion operand64;
  allow_inversion operand128;
  match args with
  | [] -> ()
  | i::args ->
    let (v1, v2, oprs) : option (instr_val_t i) & option (instr_val_t i) & instr_operands_t_args args =
      match i with
      | IOpEx i ->
        let (o, (oprs:instr_operands_t_args args)) = coerce oprs in
        (
          S.instr_eval_operand_explicit i o s1,
          S.instr_eval_operand_explicit i o s2,
          oprs)
      | IOpIm i ->
        let oprs = coerce oprs in (
          S.instr_eval_operand_implicit i s1,
          S.instr_eval_operand_implicit i s2,
          oprs)
      in
    let f:arrow (instr_val_t i) (instr_args_t outs args) = coerce f in
    S.get_heap_val32_reveal ();
    S.get_heap_val64_reveal ();
    S.get_heap_val128_reveal ();
    assert (v1 == v2);
    let Some v = v1 in
    lemma_args_taint outs args (f v) oprs ts s1 s2

#restart-solver
let rec lemma_inouts_taint
    (outs inouts:list instr_out) (args:list instr_operand)
    (f:instr_inouts_t outs inouts args) (oprs:instr_operands_t inouts args)
    (ts:analysis_taints) (s1 s2:S.machine_state)
  : Lemma
    (requires
      constTimeInvariant ts.lts s1 s2 /\
      Some? (S.instr_apply_eval_inouts outs inouts args f oprs s1) /\
      Some? (S.instr_apply_eval_inouts outs inouts args f oprs s2) /\
      check_if_consumes_fixed_time_outs inouts args oprs ts Public /\
      inouts_taint inouts args oprs ts == Public)
    (ensures
      S.instr_apply_eval_inouts outs inouts args f oprs s1 ==
      S.instr_apply_eval_inouts outs inouts args f oprs s2)
  =
  allow_inversion maddr;
  allow_inversion tmaddr;
  allow_inversion operand64;
  allow_inversion operand128;
  match inouts with
  | [] -> lemma_args_taint outs args f oprs ts s1 s2
  | (Out, i)::inouts ->
    let oprs =
      match i with
      | IOpEx i -> snd #(instr_operand_t i) (coerce oprs)
      | IOpIm i -> coerce oprs
      in
    lemma_inouts_taint outs inouts args (coerce f) oprs ts s1 s2
  | (InOut, i)::inouts ->
    let (v1, v2, oprs) : option (instr_val_t i) & option (instr_val_t i) & instr_operands_t inouts args =
      match i with
      | IOpEx i ->
        let (o, (oprs:instr_operands_t inouts args)) = coerce oprs in
        let oprs = coerce oprs in (
          S.instr_eval_operand_explicit i o s1,
          S.instr_eval_operand_explicit i o s2,
          oprs)
      | IOpIm i ->
        let oprs = coerce oprs in (
          S.instr_eval_operand_implicit i s1,
          S.instr_eval_operand_implicit i s2,
          oprs)
      in
    let f:arrow (instr_val_t i) (instr_inouts_t outs inouts args) = coerce f in
    S.get_heap_val32_reveal ();
    S.get_heap_val64_reveal ();
    S.get_heap_val128_reveal ();
    assert (v1 == v2);
    let Some v = v1 in
    lemma_inouts_taint outs inouts args (f v) oprs ts s1 s2

let instr_set_taint_explicit
    (i:instr_operand_explicit) (o:instr_operand_t i) (ts:analysis_taints) (t:taint)
  : analysis_taints =
  match i with
  | IOp64 -> set_taint 0 (o <: operand64) ts t
  | IOpXmm -> set_taint 1 (o <: operand128) ts t

[@instr_attr]
let instr_set_taint_implicit (i:instr_operand_implicit) (ts:analysis_taints) (t:taint) : analysis_taints =
  match i with
  | IOp64One o -> set_taint 0 o ts t
  | IOpXmmOne o -> set_taint 1 o ts t
  | IOpFlagsCf -> set_taint_cf_and_flags ts t
  | IOpFlagsOf -> set_taint_of_and_flags ts t

let rec instr_set_taints
    (outs:list instr_out) (args:list instr_operand)
    (oprs:instr_operands_t outs args) (ts:analysis_taints) (t:taint)
  : analysis_taints =
  match outs with
  | [] -> ts
  | (_, i)::outs ->
    (
      match i with
      | IOpEx i ->
        let oprs:instr_operand_t i & instr_operands_t outs args = coerce oprs in
        instr_set_taints outs args (snd oprs) (instr_set_taint_explicit i (fst oprs) ts t) t
      | IOpIm i -> instr_set_taints outs args (coerce oprs) (instr_set_taint_implicit i ts t) t
    )

let rec lemma_instr_write_outputs_ok
    (outs:list instr_out) (args:list instr_operand)
    (vs:instr_ret_t outs) (oprs:instr_operands_t outs args) (s_orig s:S.machine_state)
  : Lemma
    (requires (S.instr_write_outputs outs args vs oprs s_orig s).S.ms_ok)
    (ensures s.S.ms_ok)
  =
  match outs with
  | [] -> ()
  | (_, i)::outs ->
    (
      let ((v:instr_val_t i), (vs:instr_ret_t outs)) =
        match outs with
        | [] -> (vs, ())
        | _::_ -> let vs = coerce vs in (fst vs, snd vs)
        in
      match i with
      | IOpEx i ->
          let oprs:instr_operand_t i & instr_operands_t outs args = coerce oprs in
          let s' = S.instr_write_output_explicit i v (fst oprs) s_orig s in
          lemma_instr_write_outputs_ok outs args vs (snd oprs) s_orig s'
      | IOpIm i ->
          let s' = S.instr_write_output_implicit i v s_orig s in
          lemma_instr_write_outputs_ok outs args vs (coerce oprs) s_orig s'
    )

[@"opaque_to_smt"]
let update_heap32_val (ptr:int) (v:Vale.Def.Types_s.nat32) (i:int) : Vale.Def.Types_s.nat8 =
  let open Vale.Def.Words_s in
  let open Vale.Def.Words.Four_s in
  let v = nat_to_four 8 v in
  match (i - ptr) with
  | 0 -> v.lo0
  | 1 -> v.lo1
  | 2 -> v.hi2
  | 3 -> v.hi3
  | _ -> 0

let valid_addr32 (ptr:int) (mem:S.machine_heap) : bool =
  S.valid_addr (ptr + 0) mem &&
  S.valid_addr (ptr + 1) mem &&
  S.valid_addr (ptr + 2) mem &&
  S.valid_addr (ptr + 3) mem

let lemma_update_heap32_val (ptr:int) (v:Vale.Def.Types_s.nat32) (mem:S.machine_heap) (i:int) : Lemma
  (requires True)
  (ensures (S.update_heap32 ptr v mem).[i] ==
    (if ptr <= i && i < ptr + 4 then update_heap32_val ptr v i else mem.[i]))
  [SMTPat ((S.update_heap32 ptr v mem).[i])]
  =
  S.update_heap32_reveal ();
  reveal_opaque (`%update_heap32_val) update_heap32_val

let lemma_update_heap32_domain (ptr:int) (v:Vale.Def.Types_s.nat32) (mem:S.machine_heap) : Lemma
  (requires valid_addr32 ptr mem)
  (ensures Map.domain (S.update_heap32 ptr v mem) == Map.domain mem)
  [SMTPat (Map.domain (S.update_heap32 ptr v mem))]
  =
  S.update_heap32_reveal ();
  assert (Set.equal (Map.domain (S.update_heap32 ptr v mem)) (Map.domain mem))

[@"opaque_to_smt"]
let update_heap64_val (ptr:int) (v:nat64) (i:int) : Vale.Def.Types_s.nat8 =
  let open Vale.Def.Words_s in
  let open Vale.Def.Words.Two_s in
  let open Vale.Def.Words.Four_s in
  let v = nat_to_two 32 v in
  let lo = nat_to_four 8 v.lo in
  let hi = nat_to_four 8 v.hi in
  match (i - ptr) with
  | 0 -> lo.lo0
  | 1 -> lo.lo1
  | 2 -> lo.hi2
  | 3 -> lo.hi3
  | 4 -> hi.lo0
  | 5 -> hi.lo1
  | 6 -> hi.hi2
  | 7 -> hi.hi3
  | _ -> 0

let lemma_update_heap64_val (ptr:int) (v:nat64) (mem:S.machine_heap) (i:int) : Lemma
  (requires True)
  (ensures
    (S.update_heap64 ptr v mem).[i] ==
    (if ptr <= i && i < ptr + 8 then update_heap64_val ptr v i else mem.[i])
  )
  [SMTPat ((S.update_heap64 ptr v mem).[i])]
  =
  S.update_heap64_reveal ();
  reveal_opaque (`%update_heap64_val) update_heap64_val

let lemma_update_heap64_domain (ptr:int) (v:nat64) (mem:S.machine_heap) : Lemma
  (requires S.valid_addr64 ptr mem)
  (ensures Map.domain (S.update_heap64 ptr v mem) == Map.domain mem)
  [SMTPat (Map.domain (S.update_heap64 ptr v mem))]
  =
  reveal_opaque (`%S.valid_addr64) S.valid_addr64;
  S.update_heap64_reveal ();
  assert (Set.equal (Map.domain (S.update_heap64 ptr v mem)) (Map.domain mem))

[@"opaque_to_smt"]
let update_heap128_val (ptr:int) (v:Vale.Def.Types_s.quad32) (i:int) : Vale.Def.Types_s.nat8 =
  let open Vale.Def.Words_s in
  let j = i - ptr in
  if  0 <= j && j <  4 then update_heap32_val (ptr + 0 ) v.lo0 i else
  if  4 <= j && j <  8 then update_heap32_val (ptr + 4 ) v.lo1 i else
  if  8 <= j && j < 12 then update_heap32_val (ptr + 8 ) v.hi2 i else
  if 12 <= j && j < 16 then update_heap32_val (ptr + 12) v.hi3 i else
  0

let valid_addr128 (ptr:int) (mem:S.machine_heap) : bool =
  valid_addr32 (ptr + 0) mem &&
  valid_addr32 (ptr + 4) mem &&
  valid_addr32 (ptr + 8) mem &&
  valid_addr32 (ptr + 12) mem

let lemma_update_heap128_val (ptr:int) (v:Vale.Def.Types_s.quad32) (mem:S.machine_heap) (i:int) : Lemma
  (requires True)
  (ensures
    (S.update_heap128 ptr v mem).[i] ==
    (if ptr <= i && i < ptr + 16 then update_heap128_val ptr v i else mem.[i])
  )
  [SMTPat ((S.update_heap128 ptr v mem).[i])]
  =
  S.update_heap128_reveal ();
  reveal_opaque (`%update_heap128_val) update_heap128_val

let lemma_update_heap128_domain (ptr:int) (v:Vale.Def.Types_s.quad32) (mem:S.machine_heap) : Lemma
  (requires valid_addr128 ptr mem)
  (ensures Map.domain (S.update_heap128 ptr v mem) == Map.domain mem)
  [SMTPat (S.update_heap128 ptr v mem)]
  =
  S.update_heap128_reveal ();
  assert (Set.equal (Map.domain (S.update_heap128 ptr v mem)) (Map.domain mem))

let lemma_preserve_valid64 (m m':S.machine_heap) : Lemma
  (requires Set.equal (Map.domain m) (Map.domain m'))
  (ensures (forall (i:int).{:pattern (S.valid_addr64 i m')}
    S.valid_addr64 i m ==> S.valid_addr64 i m'))
val lemma_preserve_valid64 (m m': S.machine_heap)
    : Lemma (requires Set.equal (Map.domain m) (Map.domain m'))
      (ensures
        (forall (i: int). {:pattern (S.valid_addr64 i m')}
            S.valid_addr64 i m ==> S.valid_addr64 i m'))
m: Vale.Arch.MachineHeap_s.machine_heap -> m': Vale.Arch.MachineHeap_s.machine_heap
  -> FStar.Pervasives.Lemma (requires FStar.Set.equal (FStar.Map.domain m) (FStar.Map.domain m'))
      (ensures
        forall (i: Prims.int). {:pattern Vale.Arch.MachineHeap_s.valid_addr64 i m'}
          Vale.Arch.MachineHeap_s.valid_addr64 i m ==> Vale.Arch.MachineHeap_s.valid_addr64 i m')