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 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
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.op_LessThan Lib.IntTypes.uint16 Prims.unit FStar.Calc.calc_finish Lib.IntTypes.range_t Lib.IntTypes.U16 Prims.eq2 Lib.IntTypes.v Lib.IntTypes.SEC Prims.op_Modulus Prims.op_Division Prims.op_Addition Prims.pow2 Prims.op_Subtraction Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack Spec.Frodo.Lemmas.modulo_pow2_u16 Prims.squash FStar.Math.Lemmas.pow2_modulo_modulo_lemma_1 FStar.Math.Lemmas.pow2_lt_compat Lib.IntTypes.int_t Lib.IntTypes.op_Amp_Dot Lib.IntTypes.op_Subtraction_Dot Lib.IntTypes.op_Less_Less_Dot Lib.IntTypes.u16 Lib.IntTypes.size Lib.IntTypes.modulus FStar.Math.Lemmas.lemma_mod_plus_distr_r FStar.Math.Lemmas.pow2_modulo_division_lemma_1 FStar.Math.Lemmas.pow2_modulo_modulo_lemma_2 Lib.IntTypes.op_Greater_Greater_Dot Lib.IntTypes.op_Plus_Dot
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)
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)

    logq: Lib.IntTypes.size_pos{logq <= 16} ->
    b: Lib.IntTypes.size_pos{b < logq} ->
    c: Lib.IntTypes.uint16
  -> Prims.Pure Lib.IntTypes.uint16