val frodo_key_encode1:
    logq:size_t{0 < v logq /\ v logq <= 16}
  -> b:size_t{0 < v b /\ v b <= 8 /\ v b <= v logq}
  -> n:size_t{v n == 8}
  -> a:lbytes (n *! n *! b /. size 8)
  -> i:size_t{v i < v n}
  -> Stack uint64
    (requires fun h -> live h a)
    (ensures fun h0 r h1 -> modifies0 h0 h1 /\
      r == S.frodo_key_encode1 (v logq) (v b) (v n) (as_seq h0 a) (v i))
let frodo_key_encode1 logq b n a i =
  let h0 = ST.get() in
  push_frame();
  let v8 = create (size 8) (u8 0) in
  let chunk = sub a (i *! b) b in
  let h1 = ST.get() in
  assert (as_seq h1 chunk == LSeq.sub (as_seq h0 a) (v (i *! b)) (v b));
  update_sub v8 (size 0) b chunk;
  let x = uint_from_bytes_le #U64 v8 in
  pop_frame();
  x
val frodo_key_encode1:
    logq:size_t{0 < v logq /\ v logq <= 16}
  -> b:size_t{0 < v b /\ v b <= 8 /\ v b <= v logq}
  -> n:size_t{v n == 8}
  -> a:lbytes (n *! n *! b /. size 8)
  -> i:size_t{v i < v n}
  -> Stack uint64
    (requires fun h -> live h a)
    (ensures fun h0 r h1 -> modifies0 h0 h1 /\
      r == S.frodo_key_encode1 (v logq) (v b) (v n) (as_seq h0 a) (v i))
let frodo_key_encode1 logq b n a i =
let h0 = ST.get () in
push_frame ();
let v8 = create (size 8) (u8 0) in
let chunk = sub a (i *! b) b in
let h1 = ST.get () in
assert (as_seq h1 chunk == LSeq.sub (as_seq h0 a) (v (i *! b)) (v b));
update_sub v8 (size 0) b chunk;
let x = uint_from_bytes_le #U64 v8 in
pop_frame ();
x
Hacl.Impl.Frodo.Encode.fst.checked
Spec.Matrix.fst.checked Spec.Frodo.Lemmas.fst.checked Spec.Frodo.Encode.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.Matrix.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Impl.Frodo.Encode.fst
Lib.IntTypes.size_t Prims.l_and Prims.b2t Prims.op_LessThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Prims.op_LessThanOrEqual Prims.eq2 Prims.int Hacl.Impl.Matrix.lbytes Lib.IntTypes.op_Slash_Dot Lib.IntTypes.op_Star_Bang Lib.IntTypes.size Lib.IntTypes.uint64 Prims.unit FStar.HyperStack.ST.pop_frame Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC Lib.ByteBuffer.uint_from_bytes_le Lib.IntTypes.uint_t Lib.Buffer.update_sub Lib.Buffer.MUT Lib.IntTypes.uint8 Prims._assert Lib.Sequence.lseq Lib.Buffer.as_seq Lib.Sequence.sub FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Lib.Buffer.lbuffer_t Lib.IntTypes.U8 Lib.Buffer.sub Lib.IntTypes.mk_int Lib.Buffer.create Lib.IntTypes.u8 Lib.Buffer.lbuffer FStar.HyperStack.ST.push_frame
module Hacl.Impl.Frodo.Encode

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open LowStar.Buffer

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer

open Hacl.Impl.Matrix

module ST = FStar.HyperStack.ST
module Loops = Lib.LoopCombinators
module LSeq = Lib.Sequence
module S    = Spec.Frodo.Encode

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

inline_for_extraction noextract private
val ec:
    logq:size_t{0 < v logq /\ v logq <= 16}
  -> b:size_t{0 < v b /\ v b <= v logq}
  -> k:uint16{v k < pow2 (v b)}
  -> r:uint16{r == S.ec (v logq) (v b) k}

let ec logq b a =
  a <<. (logq -. b)


inline_for_extraction noextract private
val dc:
    logq:size_t{0 < v logq /\ v logq <= 16}
  -> b:size_t{0 < v b /\ v b < v logq}
  -> c:uint16
  -> r:uint16{r == S.dc (v logq) (v b) c}

let dc logq b c =
  let res1 = (c +. (u16 1 <<. (logq -. b -. size 1))) >>. (logq -. b) in
  res1 &. ((u16 1 <<. b) -. u16 1)


inline_for_extraction noextract private
val ec1:
    logq:size_t{0 < v logq /\ v logq <= 16}
  -> b:size_t{0 < v b /\ v b <= 8 /\ v b <= v logq}
  -> x:uint64
  -> k:size_t{v k < 8}
  -> res:uint16{res == S.ec1 (v logq) (v b) x (v k)}

let ec1 logq b x k =
  Spec.Frodo.Lemmas.modulo_pow2_u64 (x >>. (b *! k)) (v b);
  let rk = (x >>. (b *! k)) &. ((u64 1 <<. b) -. u64 1) in
  ec logq b (to_u16 rk)


inline_for_extraction noextract private
val frodo_key_encode1:
    logq:size_t{0 < v logq /\ v logq <= 16}
  -> b:size_t{0 < v b /\ v b <= 8 /\ v b <= v logq}
  -> n:size_t{v n == 8}
  -> a:lbytes (n *! n *! b /. size 8)
  -> i:size_t{v i < v n}
  -> Stack uint64
    (requires fun h -> live h a)
    (ensures fun h0 r h1 -> modifies0 h0 h1 /\
      r == S.frodo_key_encode1 (v logq) (v b) (v n) (as_seq h0 a) (v i))
val frodo_key_encode1:
    logq:size_t{0 < v logq /\ v logq <= 16}
  -> b:size_t{0 < v b /\ v b <= 8 /\ v b <= v logq}
  -> n:size_t{v n == 8}
  -> a:lbytes (n *! n *! b /. size 8)
  -> i:size_t{v i < v n}
  -> Stack uint64
    (requires fun h -> live h a)
    (ensures fun h0 r h1 -> modifies0 h0 h1 /\
      r == S.frodo_key_encode1 (v logq) (v b) (v n) (as_seq h0 a) (v i))

    logq: Lib.IntTypes.size_t{0 < Lib.IntTypes.v logq /\ Lib.IntTypes.v logq <= 16} ->
    b:
      Lib.IntTypes.size_t
        {0 < Lib.IntTypes.v b /\ Lib.IntTypes.v b <= 8 /\ Lib.IntTypes.v b <= Lib.IntTypes.v logq} ->
    n: Lib.IntTypes.size_t{Lib.IntTypes.v n == 8} ->
    a: Hacl.Impl.Matrix.lbytes (n *! n *! b /. Lib.IntTypes.size 8) ->
    i: Lib.IntTypes.size_t{Lib.IntTypes.v i < Lib.IntTypes.v n}
  -> FStar.HyperStack.ST.Stack Lib.IntTypes.uint64