val lemma_hash_init (h0 h1:HS.mem) (ctx_b:PS.uint8_p) (is_zero:bool) : Lemma
  (requires
    B.live h0 ctx_b /\
    B.live h1 ctx_b /\
    B.length ctx_b == 192 /\
    (forall (i:int).{:pattern (B.get h0 ctx_b i)} 0 <= i /\ i < 24 ==>
      B.get h0 ctx_b i == B.get h1 ctx_b i) /\
    (is_zero ==> (forall (i:int).{:pattern (B.get h0 ctx_b i)} 0 <= i /\ i < 24 ==>
      B.get h0 ctx_b i == 0uy))
  )
  (ensures (
    let open IT in
    assert (view_n TUInt8 == 1);
    assert (view_n TUInt64 == 8);
    DV.length_eq (get_downview ctx_b);
    let h0_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 0) in
    let h1_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 1) in
    let h2_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 2) in
    let h0_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 0) in
    let h1_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 1) in
    let h2_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 2) in
    h0_in == h0_out /\ h1_in == h1_out /\ h2_in == h2_out /\
    (is_zero ==>
      h0_in == 0 /\ h1_in == 0 /\ h2_in == 0 /\ modp 0 == 0 /\
      PM.lowerUpper192 (PM.lowerUpper128 h0_in h1_in) h2_in == 0)
  ))
let lemma_hash_init h0 h1 ctx_b is_zero =
  let open IT in
  let tag0 = BF.to_bytes (slice (B.as_seq h0 ctx_b) 0 24) in
  let tag1 = BF.to_bytes (slice (B.as_seq h1 ctx_b) 0 24) in
  assert (forall (i:int).{:pattern (index (BF.of_bytes tag0) i)} 0 <= i /\ i < 24 ==> index (BF.of_bytes tag0) i == B.get h0 ctx_b i);
  assert (forall (i:int).{:pattern (index (BF.of_bytes tag1) i)} 0 <= i /\ i < 24 ==> index (BF.of_bytes tag1) i == B.get h1 ctx_b i);
  // REVIEW: triggers F* "Unexpected error": assert (equal (BF.of_bytes tag0) (BF.of_bytes tag1));
  let workaround : squash (equal (BF.of_bytes tag0) (BF.of_bytes tag1)) = () in
  assert (view_n TUInt8 == 1);
  assert (view_n TUInt64 == 8);
  DV.length_eq (get_downview ctx_b);
  let h0_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 0) in
  let h1_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 1) in
  let h2_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 2) in
  let h0_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 0) in
  let h1_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 1) in
  let h2_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 2) in
  let view = Vale.AsLowStar.LowStarSig.view_of_base_typ TUInt64 in
  let ctx_db = get_downview ctx_b in
  let ctx_vb = UV.mk_buffer ctx_db view in
  UV.length_eq ctx_vb;
  let open Vale.Def.Words.Seq_s in
  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag0 0 8);
  calc (==) {
    h0_in;
    == {}
    UInt64.v (UV.sel h0 ctx_vb 0);
    == {UV.get_sel h0 ctx_vb 0; Vale.Interop.Views.get64_reveal ()}
    le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h0 (UV.as_down_buffer ctx_vb)) 0 8));
    == {BF.same_seq_downview8 ctx_b h0}
    nat_from_bytes_le (slice tag0 0 8);
  };
  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag1 0 8);
  calc (==) {
    h0_out;
    == {}
    UInt64.v (UV.sel h1 ctx_vb 0);
    == {UV.get_sel h1 ctx_vb 0; Vale.Interop.Views.get64_reveal ()}
    le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h1 (UV.as_down_buffer ctx_vb)) 0 8));
    == {BF.same_seq_downview8 ctx_b h1}
    nat_from_bytes_le (slice tag1 0 8);
  };
  BF.lemma_le_to_n_is_nat_from_bytes (BF.of_bytes (slice tag0 0 8));
  if is_zero then
    calc (==) {
      nat_from_bytes_le (slice tag0 0 8) <: nat;
      == {}
      FE.le_to_n (BF.of_bytes (slice tag0 0 8));
      == {BF.lemma_le_to_n_indexed (BF.of_bytes (slice tag0 0 8))}
      BF.le_to_n_indexed (BF.of_bytes (slice tag0 0 8));
      == {
        norm_spec [iota; zeta; primops; delta_only [`%BF.le_to_n_indexed_rec; `%pow2]]
          (BF.le_to_n_indexed_rec (BF.of_bytes (slice tag0 0 8)) 8)
      }
      0;
    };
  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag0 8 16);
  calc (==) {
    h1_in;
    == {}
    UInt64.v (UV.sel h0 ctx_vb 1);
    == {UV.get_sel h0 ctx_vb 1; Vale.Interop.Views.get64_reveal ()}
    le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h0 (UV.as_down_buffer ctx_vb)) 8 16));
    == {BF.same_seq_downview8 ctx_b h0}
    nat_from_bytes_le (slice tag0 8 16);
  };
  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag1 8 16);
  calc (==) {
    h1_out;
    == {}
    UInt64.v (UV.sel h1 ctx_vb 1);
    == {UV.get_sel h1 ctx_vb 1; Vale.Interop.Views.get64_reveal ()}
    le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h1 (UV.as_down_buffer ctx_vb)) 8 16));
    == {BF.same_seq_downview8 ctx_b h1}
    nat_from_bytes_le (slice tag1 8 16);
  };
  BF.lemma_le_to_n_is_nat_from_bytes (BF.of_bytes (slice tag0 8 16));
  if is_zero then
    calc (==) {
      nat_from_bytes_le (slice tag0 8 16) <: nat;
      == {}
      FE.le_to_n (BF.of_bytes (slice tag0 8 16));
      == {BF.lemma_le_to_n_indexed (BF.of_bytes (slice tag0 8 16))}
      BF.le_to_n_indexed (BF.of_bytes (slice tag0 8 16));
      == {
        norm_spec [iota; zeta; primops; delta_only [`%BF.le_to_n_indexed_rec; `%pow2]]
          (BF.le_to_n_indexed_rec (BF.of_bytes (slice tag0 8 16)) 8)
      }
      0;
    };
  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag0 16 24);
  calc (==) {
    h2_in;
    == {}
    UInt64.v (UV.sel h0 ctx_vb 2);
    == {UV.get_sel h0 ctx_vb 2; Vale.Interop.Views.get64_reveal ()}
    le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h0 (UV.as_down_buffer ctx_vb)) 16 24));
    == {BF.same_seq_downview8 ctx_b h0}
    nat_from_bytes_le (slice tag0 16 24);
  };
  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag1 16 24);
  calc (==) {
    h2_out;
    == {}
    UInt64.v (UV.sel h1 ctx_vb 2);
    == {UV.get_sel h1 ctx_vb 2; Vale.Interop.Views.get64_reveal ()}
    le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h1 (UV.as_down_buffer ctx_vb)) 16 24));
    == {BF.same_seq_downview8 ctx_b h1}
    nat_from_bytes_le (slice tag1 16 24);
  };
  BF.lemma_le_to_n_is_nat_from_bytes (BF.of_bytes (slice tag0 16 24));
  if is_zero then
    calc (==) {
      nat_from_bytes_le (slice tag0 16 24) <: nat;
      == {}
      FE.le_to_n (BF.of_bytes (slice tag0 16 24));
      == {BF.lemma_le_to_n_indexed (BF.of_bytes (slice tag0 16 24))}
      BF.le_to_n_indexed (BF.of_bytes (slice tag0 16 24));
      == {
        norm_spec [iota; zeta; primops; delta_only [`%BF.le_to_n_indexed_rec; `%pow2]]
          (BF.le_to_n_indexed_rec (BF.of_bytes (slice tag0 16 24)) 8)
      }
      0;
    };
  assert_norm (modp 0 == 0);
  if is_zero then
    calc (==) {
      PM.lowerUpper192 (PM.lowerUpper128 h0_in h1_in) h2_in;
      == {PM.lowerUpper128_reveal (); PM.lowerUpper192_reveal ()}
      0;
    }
val lemma_hash_init (h0 h1:HS.mem) (ctx_b:PS.uint8_p) (is_zero:bool) : Lemma
  (requires
    B.live h0 ctx_b /\
    B.live h1 ctx_b /\
    B.length ctx_b == 192 /\
    (forall (i:int).{:pattern (B.get h0 ctx_b i)} 0 <= i /\ i < 24 ==>
      B.get h0 ctx_b i == B.get h1 ctx_b i) /\
    (is_zero ==> (forall (i:int).{:pattern (B.get h0 ctx_b i)} 0 <= i /\ i < 24 ==>
      B.get h0 ctx_b i == 0uy))
  )
  (ensures (
    let open IT in
    assert (view_n TUInt8 == 1);
    assert (view_n TUInt64 == 8);
    DV.length_eq (get_downview ctx_b);
    let h0_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 0) in
    let h1_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 1) in
    let h2_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 2) in
    let h0_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 0) in
    let h1_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 1) in
    let h2_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 2) in
    h0_in == h0_out /\ h1_in == h1_out /\ h2_in == h2_out /\
    (is_zero ==>
      h0_in == 0 /\ h1_in == 0 /\ h2_in == 0 /\ modp 0 == 0 /\
      PM.lowerUpper192 (PM.lowerUpper128 h0_in h1_in) h2_in == 0)
  ))
let lemma_hash_init h0 h1 ctx_b is_zero =
let open IT in
let tag0 = BF.to_bytes (slice (B.as_seq h0 ctx_b) 0 24) in
let tag1 = BF.to_bytes (slice (B.as_seq h1 ctx_b) 0 24) in
assert (forall (i: int). {:pattern (index (BF.of_bytes tag0) i)}
      0 <= i /\ i < 24 ==> index (BF.of_bytes tag0) i == B.get h0 ctx_b i);
assert (forall (i: int). {:pattern (index (BF.of_bytes tag1) i)}
      0 <= i /\ i < 24 ==> index (BF.of_bytes tag1) i == B.get h1 ctx_b i);
let workaround:squash (equal (BF.of_bytes tag0) (BF.of_bytes tag1)) = () in
assert (view_n TUInt8 == 1);
assert (view_n TUInt64 == 8);
DV.length_eq (get_downview ctx_b);
let h0_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 0) in
let h1_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 1) in
let h2_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 2) in
let h0_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 0) in
let h1_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 1) in
let h2_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 2) in
let view = Vale.AsLowStar.LowStarSig.view_of_base_typ TUInt64 in
let ctx_db = get_downview ctx_b in
let ctx_vb = UV.mk_buffer ctx_db view in
UV.length_eq ctx_vb;
let open Vale.Def.Words.Seq_s in
BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag0 0 8);
calc ( == ) {
  h0_in;
  ( == ) { () }
  UInt64.v (UV.sel h0 ctx_vb 0);
  ( == ) { (UV.get_sel h0 ctx_vb 0;
    Vale.Interop.Views.get64_reveal ()) }
  le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h0 (UV.as_down_buffer ctx_vb)) 0 8));
  ( == ) { BF.same_seq_downview8 ctx_b h0 }
  nat_from_bytes_le (slice tag0 0 8);
};
BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag1 0 8);
calc ( == ) {
  h0_out;
  ( == ) { () }
  UInt64.v (UV.sel h1 ctx_vb 0);
  ( == ) { (UV.get_sel h1 ctx_vb 0;
    Vale.Interop.Views.get64_reveal ()) }
  le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h1 (UV.as_down_buffer ctx_vb)) 0 8));
  ( == ) { BF.same_seq_downview8 ctx_b h1 }
  nat_from_bytes_le (slice tag1 0 8);
};
BF.lemma_le_to_n_is_nat_from_bytes (BF.of_bytes (slice tag0 0 8));
if is_zero
then
  calc ( == ) {
    nat_from_bytes_le (slice tag0 0 8) <: nat;
    ( == ) { () }
    FE.le_to_n (BF.of_bytes (slice tag0 0 8));
    ( == ) { BF.lemma_le_to_n_indexed (BF.of_bytes (slice tag0 0 8)) }
    BF.le_to_n_indexed (BF.of_bytes (slice tag0 0 8));
    ( == ) { norm_spec [iota; zeta; primops; delta_only [`%BF.le_to_n_indexed_rec; `%pow2]]
      (BF.le_to_n_indexed_rec (BF.of_bytes (slice tag0 0 8)) 8) }
    0;
  };
BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag0 8 16);
calc ( == ) {
  h1_in;
  ( == ) { () }
  UInt64.v (UV.sel h0 ctx_vb 1);
  ( == ) { (UV.get_sel h0 ctx_vb 1;
    Vale.Interop.Views.get64_reveal ()) }
  le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h0 (UV.as_down_buffer ctx_vb)) 8 16));
  ( == ) { BF.same_seq_downview8 ctx_b h0 }
  nat_from_bytes_le (slice tag0 8 16);
};
BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag1 8 16);
calc ( == ) {
  h1_out;
  ( == ) { () }
  UInt64.v (UV.sel h1 ctx_vb 1);
  ( == ) { (UV.get_sel h1 ctx_vb 1;
    Vale.Interop.Views.get64_reveal ()) }
  le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h1 (UV.as_down_buffer ctx_vb)) 8 16));
  ( == ) { BF.same_seq_downview8 ctx_b h1 }
  nat_from_bytes_le (slice tag1 8 16);
};
BF.lemma_le_to_n_is_nat_from_bytes (BF.of_bytes (slice tag0 8 16));
if is_zero
then
  calc ( == ) {
    nat_from_bytes_le (slice tag0 8 16) <: nat;
    ( == ) { () }
    FE.le_to_n (BF.of_bytes (slice tag0 8 16));
    ( == ) { BF.lemma_le_to_n_indexed (BF.of_bytes (slice tag0 8 16)) }
    BF.le_to_n_indexed (BF.of_bytes (slice tag0 8 16));
    ( == ) { norm_spec [iota; zeta; primops; delta_only [`%BF.le_to_n_indexed_rec; `%pow2]]
      (BF.le_to_n_indexed_rec (BF.of_bytes (slice tag0 8 16)) 8) }
    0;
  };
BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag0 16 24);
calc ( == ) {
  h2_in;
  ( == ) { () }
  UInt64.v (UV.sel h0 ctx_vb 2);
  ( == ) { (UV.get_sel h0 ctx_vb 2;
    Vale.Interop.Views.get64_reveal ()) }
  le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h0 (UV.as_down_buffer ctx_vb)) 16 24));
  ( == ) { BF.same_seq_downview8 ctx_b h0 }
  nat_from_bytes_le (slice tag0 16 24);
};
BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag1 16 24);
calc ( == ) {
  h2_out;
  ( == ) { () }
  UInt64.v (UV.sel h1 ctx_vb 2);
  ( == ) { (UV.get_sel h1 ctx_vb 2;
    Vale.Interop.Views.get64_reveal ()) }
  le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h1 (UV.as_down_buffer ctx_vb)) 16 24));
  ( == ) { BF.same_seq_downview8 ctx_b h1 }
  nat_from_bytes_le (slice tag1 16 24);
};
BF.lemma_le_to_n_is_nat_from_bytes (BF.of_bytes (slice tag0 16 24));
if is_zero
then
  calc ( == ) {
    nat_from_bytes_le (slice tag0 16 24) <: nat;
    ( == ) { () }
    FE.le_to_n (BF.of_bytes (slice tag0 16 24));
    ( == ) { BF.lemma_le_to_n_indexed (BF.of_bytes (slice tag0 16 24)) }
    BF.le_to_n_indexed (BF.of_bytes (slice tag0 16 24));
    ( == ) { norm_spec [iota; zeta; primops; delta_only [`%BF.le_to_n_indexed_rec; `%pow2]]
      (BF.le_to_n_indexed_rec (BF.of_bytes (slice tag0 16 24)) 8) }
    0;
  };
assert_norm (modp 0 == 0);
if is_zero
then
  calc ( == ) {
    PM.lowerUpper192 (PM.lowerUpper128 h0_in h1_in) h2_in;
    ( == ) { (PM.lowerUpper128_reveal ();
      PM.lowerUpper192_reveal ()) }
    0;
  }
Vale.Poly1305.CallingFromLowStar.fst.checked
Vale.Wrapper.X64.Poly.fsti.checked Vale.Poly1305.Util.fsti.checked Vale.Poly1305.Math.fsti.checked Vale.Interop.Views.fsti.checked Vale.Interop.Types.fst.checked Vale.Def.Words.Seq_s.fsti.checked Vale.AsLowStar.LowStarSig.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Endianness.fsti.checked FStar.Calc.fsti.checked
Vale.Poly1305.CallingFromLowStar.fst
FStar.Monotonic.HyperStack.mem Vale.Wrapper.X64.Poly.uint8_p Prims.bool FStar.Calc.calc_finish Prims.int Prims.eq2 Vale.Poly1305.Math.lowerUpper192 Vale.Poly1305.Math.lowerUpper128 Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack Vale.Poly1305.Math.lowerUpper192_reveal Vale.Poly1305.Math.lowerUpper128_reveal Prims.squash FStar.Pervasives.assert_norm Vale.Poly1305.Spec_s.modp Prims.nat Vale.Poly1305.Equiv.nat_from_bytes_le Lib.IntTypes.SEC FStar.Seq.Base.slice Lib.IntTypes.uint_t Lib.IntTypes.U8 Vale.Arch.BufferFriend.le_to_n_indexed Vale.Arch.BufferFriend.of_bytes FStar.Endianness.le_to_n Vale.Arch.BufferFriend.lemma_le_to_n_indexed FStar.Pervasives.norm_spec FStar.Pervasives.norm_step FStar.Pervasives.iota FStar.Pervasives.zeta FStar.Pervasives.primops FStar.Pervasives.delta_only Prims.string Vale.Arch.BufferFriend.le_to_n_indexed_rec Vale.Arch.BufferFriend.lemma_le_to_n_is_nat_from_bytes FStar.UInt.uint_t FStar.UInt64.n Vale.Def.Types_s.le_bytes_to_nat64 Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 LowStar.BufferView.Up.buffer_src Vale.Interop.Types.base_typ_as_type Vale.Arch.HeapTypes_s.TUInt64 LowStar.BufferView.Down.as_seq LowStar.BufferView.Up.as_down_buffer FStar.UInt64.v LowStar.BufferView.Up.sel Vale.Interop.Views.get64_reveal LowStar.BufferView.Up.get_sel Vale.Arch.BufferFriend.same_seq_downview8 Vale.Arch.BufferFriend.nat_from_bytes_le_is_le_bytes_to_nat64 LowStar.BufferView.Up.length_eq LowStar.BufferView.Up.buffer LowStar.BufferView.Up.mk_buffer FStar.UInt8.t LowStar.BufferView.Down.buffer Vale.Interop.Types.get_downview Vale.Arch.HeapTypes_s.TUInt8 LowStar.Buffer.trivial_preorder LowStar.BufferView.Up.view Vale.AsLowStar.LowStarSig.view_of_base_typ Vale.AsLowStar.MemoryHelpers.low_buffer_read LowStar.BufferView.Down.length_eq Prims._assert Vale.Interop.Types.view_n FStar.Seq.Base.equal Prims.l_Forall Prims.l_imp Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.op_LessThan FStar.Seq.Base.index LowStar.Monotonic.Buffer.get Lib.Sequence.seq Lib.IntTypes.int_t Prims.op_Equals_Equals_Equals FStar.Seq.Base.seq LowStar.Monotonic.Buffer.as_seq FStar.Seq.Base.length Vale.Arch.BufferFriend.to_bytes
module Vale.Poly1305.CallingFromLowStar
open FStar.Mul

module BS = Lib.ByteSequence
module LI = Lib.IntTypes
module FE = FStar.Endianness
module PU = Vale.Poly1305.Util
module PM = Vale.Poly1305.Math
module IT = Vale.Interop.Types
module PS = Vale.Wrapper.X64.Poly

#reset-options "--z3rlimit 100"
val lemma_hash_init (h0 h1:HS.mem) (ctx_b:PS.uint8_p) (is_zero:bool) : Lemma
  (requires
    B.live h0 ctx_b /\
    B.live h1 ctx_b /\
    B.length ctx_b == 192 /\
    (forall (i:int).{:pattern (B.get h0 ctx_b i)} 0 <= i /\ i < 24 ==>
      B.get h0 ctx_b i == B.get h1 ctx_b i) /\
    (is_zero ==> (forall (i:int).{:pattern (B.get h0 ctx_b i)} 0 <= i /\ i < 24 ==>
      B.get h0 ctx_b i == 0uy))
  )
  (ensures (
    let open IT in
    assert (view_n TUInt8 == 1);
    assert (view_n TUInt64 == 8);
    DV.length_eq (get_downview ctx_b);
    let h0_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 0) in
    let h1_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 1) in
    let h2_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 2) in
    let h0_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 0) in
    let h1_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 1) in
    let h2_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 2) in
    h0_in == h0_out /\ h1_in == h1_out /\ h2_in == h2_out /\
    (is_zero ==>
      h0_in == 0 /\ h1_in == 0 /\ h2_in == 0 /\ modp 0 == 0 /\
      PM.lowerUpper192 (PM.lowerUpper128 h0_in h1_in) h2_in == 0)
  ))

    h0: FStar.Monotonic.HyperStack.mem ->
    h1: FStar.Monotonic.HyperStack.mem ->
    ctx_b: Vale.Wrapper.X64.Poly.uint8_p ->
    is_zero: Prims.bool
  -> FStar.Pervasives.Lemma
      (requires
        LowStar.Monotonic.Buffer.live h0 ctx_b /\ LowStar.Monotonic.Buffer.live h1 ctx_b /\
        LowStar.Monotonic.Buffer.length ctx_b == 192 /\
        (forall (i: Prims.int). {:pattern LowStar.Monotonic.Buffer.get h0 ctx_b i}
            0 <= i /\ i < 24 ==>
            LowStar.Monotonic.Buffer.get h0 ctx_b i == LowStar.Monotonic.Buffer.get h1 ctx_b i) /\
        (is_zero ==>
          (forall (i: Prims.int). {:pattern LowStar.Monotonic.Buffer.get h0 ctx_b i}
              0 <= i /\ i < 24 ==> LowStar.Monotonic.Buffer.get h0 ctx_b i == 0uy)))
      (ensures
        ([@@ FStar.Pervasives.inline_let ]let _ =
            assert (Vale.Interop.Types.view_n Vale.Arch.HeapTypes_s.TUInt8 == 1)
          in
          [@@ FStar.Pervasives.inline_let ]let _ =
            assert (Vale.Interop.Types.view_n Vale.Arch.HeapTypes_s.TUInt64 == 8)
          in
          [@@ FStar.Pervasives.inline_let ]let _ =
            LowStar.BufferView.Down.length_eq (Vale.Interop.Types.get_downview ctx_b)
          in
          let h0_in =
            FStar.UInt64.v (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                  Vale.Arch.HeapTypes_s.TUInt64
                  h0
                  ctx_b
                  0)
          in
          let h1_in =
            FStar.UInt64.v (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                  Vale.Arch.HeapTypes_s.TUInt64
                  h0
                  ctx_b
                  1)
          in
          let h2_in =
            FStar.UInt64.v (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                  Vale.Arch.HeapTypes_s.TUInt64
                  h0
                  ctx_b
                  2)
          in
          let h0_out =
            FStar.UInt64.v (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                  Vale.Arch.HeapTypes_s.TUInt64
                  h1
                  ctx_b
                  0)
          in
          let h1_out =
            FStar.UInt64.v (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                  Vale.Arch.HeapTypes_s.TUInt64
                  h1
                  ctx_b
                  1)
          in
          let h2_out =
            FStar.UInt64.v (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                  Vale.Arch.HeapTypes_s.TUInt64
                  h1
                  ctx_b
                  2)
          in
          h0_in == h0_out /\ h1_in == h1_out /\ h2_in == h2_out /\
          (is_zero ==>
            h0_in == 0 /\ h1_in == 0 /\ h2_in == 0 /\ Vale.Poly1305.Spec_s.modp 0 == 0 /\
            Vale.Poly1305.Math.lowerUpper192 (Vale.Poly1305.Math.lowerUpper128 h0_in h1_in) h2_in ==
            0)))