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 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
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 Lib.IntTypes.uint16 Prims.op_LessThan Lib.IntTypes.v Lib.IntTypes.U16 Lib.IntTypes.SEC Prims.pow2 Prims.unit Prims._assert Prims.op_Equality Prims.int FStar.Mul.op_Star Prims.op_Subtraction FStar.Math.Lemmas.small_modulo_lemma_2 Lib.IntTypes.modulus FStar.Math.Lemmas.pow2_le_compat FStar.Calc.calc_finish Prims.Cons FStar.Preorder.relation Prims.eq2 Prims.Nil FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Math.Lemmas.lemma_mult_lt_right Prims.squash FStar.Math.Lemmas.pow2_plus Prims.op_Modulus Lib.IntTypes.int_t Lib.IntTypes.op_Less_Less_Dot Lib.IntTypes.size
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))
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))

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