val frodo_key_encode1:
    logq:size_pos{logq <= 16}
  -> b:size_pos{b <= logq /\ b <= 8}
  -> n:size_pos{n == 8}
  -> a:lbytes (n * n * b / 8)
  -> i:size_nat{i < n}
  -> uint64
let frodo_key_encode1 logq b n a i =
  let v8 = LSeq.create 8 (u8 0) in
  let v8 = update_sub v8 0 b (LSeq.sub a (i * b) b) in
  uint_from_bytes_le #U64 v8
val frodo_key_encode1:
    logq:size_pos{logq <= 16}
  -> b:size_pos{b <= logq /\ b <= 8}
  -> n:size_pos{n == 8}
  -> a:lbytes (n * n * b / 8)
  -> i:size_nat{i < n}
  -> uint64
let frodo_key_encode1 logq b n a i =
let v8 = LSeq.create 8 (u8 0) in
let v8 = update_sub v8 0 b (LSeq.sub a (i * b) b) in
uint_from_bytes_le #U64 v8
Spec.Frodo.Encode.fst.checked
Spec.Matrix.fst.checked Spec.Frodo.Lemmas.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Spec.Frodo.Encode.fst
Lib.IntTypes.size_pos Prims.b2t Prims.op_LessThanOrEqual Prims.l_and Prims.eq2 Prims.int Lib.ByteSequence.lbytes Prims.op_Division FStar.Mul.op_Star Lib.IntTypes.size_nat Prims.op_LessThan Lib.ByteSequence.uint_from_bytes_le Lib.IntTypes.U64 Lib.IntTypes.SEC Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.Sequence.sub Prims.op_Multiply Prims.l_Forall Prims.nat Prims.l_or Prims.op_Addition FStar.Seq.Base.index Lib.Sequence.to_seq Lib.Sequence.index Lib.Sequence.update_sub Lib.IntTypes.uint_t FStar.Seq.Base.seq FStar.Seq.Base.create Lib.IntTypes.mk_int Prims.l_imp Lib.Sequence.create Lib.IntTypes.u8 Lib.IntTypes.uint64
module Spec.Frodo.Encode

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

open Spec.Matrix
open Spec.Frodo.Lemmas

module LSeq = Lib.Sequence
module Loops = Lib.LoopCombinators

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

(** The simplified version of the encode and decode functions when n = params_nbar = 8 *)

val ec:
    logq:size_pos{logq <= 16}
  -> b:size_pos{b <= logq}
  -> k:uint16{v k < pow2 b}
  -> Pure uint16
    (requires True)
    (ensures fun r ->
      v r < pow2 logq /\ v r == v k * pow2 (logq - b))

let ec logq b k =
  let res = k <<. size (logq - b) in
  assert (v res = v k * pow2 (logq - b) % modulus U16);

  calc (<) {
    v k * pow2 (logq - b);
    (<) { Math.Lemmas.lemma_mult_lt_right (pow2 (logq - b)) (v k) (pow2 b) }
    pow2 b * pow2 (logq - b);
    (==) { Math.Lemmas.pow2_plus b (logq - b) }
    pow2 logq;
    };

  Math.Lemmas.pow2_le_compat 16 logq;
  Math.Lemmas.small_modulo_lemma_2 (v k * pow2 (logq - b)) (modulus U16);
  assert (v res = v k * pow2 (logq - b));
  res


val dc:
    logq:size_pos{logq <= 16}
  -> b:size_pos{b < logq}
  -> c:uint16
  -> Pure uint16
    (requires True)
    (ensures  fun r ->
      v r < pow2 b /\ v r = (v c + pow2 (logq - b - 1)) / pow2 (logq - b) % pow2 b)

let dc logq b c =
  let res1 = (c +. (u16 1 <<. size (logq - b - 1))) >>. size (logq - b) in
  Math.Lemmas.pow2_lt_compat 16 (16 - logq + b);

  calc (==) {
    v res1;
    (==) { }
    (((v c + pow2 (logq - b - 1) % modulus U16) % modulus U16) / pow2 (logq - b)) % modulus U16;
    (==) { Math.Lemmas.lemma_mod_plus_distr_r (v c) (pow2 (logq - b - 1)) (modulus U16) }
    (((v c + pow2 (logq - b - 1)) % modulus U16) / pow2 (logq - b)) % modulus U16;
    (==) { Math.Lemmas.pow2_modulo_division_lemma_1 (v c + pow2 (logq - b - 1)) (logq - b) 16 }
    (((v c + pow2 (logq - b - 1)) / pow2 (logq - b)) % pow2 (16 - logq + b)) % modulus U16;
    (==) { Math.Lemmas.pow2_modulo_modulo_lemma_2 ((v c + pow2 (logq - b - 1)) / pow2 (logq - b)) 16 (16 - logq + b) }
    ((v c + pow2 (logq - b - 1)) / pow2 (logq - b)) % pow2 (16 - logq + b);
    };

  let res = res1 &. ((u16 1 <<. size b) -. u16 1) in
  Math.Lemmas.pow2_lt_compat 16 b;

  calc (==) {
    v res;
    (==) { modulo_pow2_u16 res1 b }
    v res1 % pow2 b;
    (==) { Math.Lemmas.pow2_modulo_modulo_lemma_1 ((v c + pow2 (logq - b - 1)) / pow2 (logq - b)) b (16 - logq + b) }
    ((v c + pow2 (logq - b - 1)) / pow2 (logq - b)) % pow2 b;
    };
  res


val ec1:
    logq:size_pos{logq <= 16}
  -> b:size_pos{b <= logq /\ b <= 8}
  -> x:uint64
  -> k:size_nat{k < 8}
  -> Pure uint16
    (requires True)
    (ensures  fun res ->
      let rk = v x / pow2 (b * k) % pow2 b in
      Math.Lemmas.pow2_lt_compat 16 b;
      res == ec logq b (u16 rk))

let ec1 logq b x k =
  let rk = (x >>. size (b * k)) &. ((u64 1 <<. size b) -. u64 1) in
  Math.Lemmas.pow2_lt_compat 16 b;

  calc (==) {
    v rk;
    (==) { modulo_pow2_u64 (x >>. size (b * k)) b }
    v (x >>. size (b * k)) % pow2 b;
    (==) { }
    v x / pow2 (b * k) % pow2 b;
    };

  ec logq b (to_u16 rk)


val frodo_key_encode0:
    logq:size_pos{logq <= 16}
  -> b:size_pos{b <= logq /\ b <= 8}
  -> n:size_pos{n == 8}
  -> a:lbytes (n * n * b / 8)
  -> x:uint64
  -> i:size_nat{i < n}
  -> k:size_nat{k < 8}
  -> res:matrix n n
  -> matrix n n

let frodo_key_encode0 logq b n a x i k res =
  res.(i, k) <- ec1 logq b x k


val frodo_key_encode1:
    logq:size_pos{logq <= 16}
  -> b:size_pos{b <= logq /\ b <= 8}
  -> n:size_pos{n == 8}
  -> a:lbytes (n * n * b / 8)
  -> i:size_nat{i < n}
  -> uint64
val frodo_key_encode1:
    logq:size_pos{logq <= 16}
  -> b:size_pos{b <= logq /\ b <= 8}
  -> n:size_pos{n == 8}
  -> a:lbytes (n * n * b / 8)
  -> i:size_nat{i < n}
  -> uint64

    logq: Lib.IntTypes.size_pos{logq <= 16} ->
    b: Lib.IntTypes.size_pos{b <= logq /\ b <= 8} ->
    n: Lib.IntTypes.size_pos{n == 8} ->
    a: Lib.ByteSequence.lbytes ((n * n) * b / 8) ->
    i: Lib.IntTypes.size_nat{i < n}
  -> Lib.IntTypes.uint64