val der_length_payload_size (x: der_length_t) : Tot (y: nat{y <= 126})
let der_length_payload_size
  (x: der_length_t)
: Tot (y: nat { y <= 126 })
= der_length_payload_size_of_tag (tag_of_der_length x)
val der_length_payload_size (x: der_length_t) : Tot (y: nat{y <= 126})
let der_length_payload_size (x: der_length_t) : Tot (y: nat{y <= 126}) =
der_length_payload_size_of_tag (tag_of_der_length x)
LowParse.Spec.DER.fsti.checked
prims.fst.checked LowParse.Spec.Int.fsti.checked LowParse.Spec.BoundedInt.fsti.checked LowParse.Math.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Int.Cast.fst.checked
LowParse.Spec.DER.fsti
LowParse.Spec.DER.der_length_t LowParse.Spec.DER.der_length_payload_size_of_tag LowParse.Spec.DER.tag_of_der_length Prims.nat Prims.b2t Prims.op_LessThanOrEqual
module LowParse.Spec.DER
include LowParse.Spec.Int
include LowParse.Spec.BoundedInt

open FStar.Mul

module U8 = FStar.UInt8
module UInt = FStar.UInt
module Seq = FStar.Seq
module Math = LowParse.Math
module Cast = FStar.Int.Cast

#reset-options "--z3cliopt smt.arith.nl=false --max_fuel 0 --max_ifuel 0"

let der_length_max : nat = 2743062034396844341627968125593604635037196317966166035056000994228098690879836473582587849768181396806642362668936055872479091931372323951612051859122835149807249350355003132267795098895967012320756270631179897595796976964454084495146379250195728106130226298287754794921070036903071843030324651025760255

// _ by (FStar.Tactics.(exact (norm_term [delta; iota; zeta; primops] (`(pow2 (8 * 126) - 1)))))

val der_length_max_eq : squash (der_length_max == pow2 (8 * 126) - 1)

// let _ = intro_ambient der_length_max

let der_length_t = (x: nat { x <= der_length_max })

[@@(noextract_to "krml")]
val log256
  (x: nat { x > 0 })
: Tot (y: nat { y > 0 /\ pow2 (8 * (y - 1)) <= x /\ x < pow2 (8 * y)})

val log256_unique
  (x: nat)
  (y: nat)
: Lemma
  (requires (
    x > 0 /\
    y > 0 /\
    pow2 (8 * (y - 1)) <= x /\
    x < pow2 (8 * y)
  ))
  (ensures (y == log256 x))

val log256_le
  (x1 x2: nat)
: Lemma
  (requires (0 < x1 /\ x1 <= x2))
  (ensures (log256 x1 <= log256 x2))

inline_for_extraction // for parser_kind
let der_length_payload_size_of_tag
  (x: U8.t)
: Tot (y: nat { y <= 126 })
= assert_norm (der_length_max == pow2 (8 * 126) - 1);
  assert_norm (pow2 7 == 128);
  assert_norm (pow2 8 == 256);
  assert_norm (256 < der_length_max);
  assert (U8.v x <= der_length_max);
  [@inline_let]
  let x' = U8.v x in
  if x' <= 128 || x' = 255
  then
    0
  else
    x' - 128

inline_for_extraction
let parse_der_length_payload_kind (x: U8.t) : Tot parser_kind =
  let len = der_length_payload_size_of_tag x in
  strong_parser_kind len len None

[@@(noextract_to "krml")]
let tag_of_der_length
  (x: der_length_t)
: Tot U8.t
= if x < 128
  then U8.uint_to_t x
  else
    let len_len = log256 x in
    assert_norm (der_length_max == pow2 (8 * 126) - 1);
    Math.pow2_lt_recip (8 * (len_len - 1)) (8 * 126);
    128uy `U8.add` U8.uint_to_t len_len

[@@(noextract_to "krml")]
let der_length_payload_size
  (x: der_length_t)
val der_length_payload_size (x: der_length_t) : Tot (y: nat{y <= 126})
x: LowParse.Spec.DER.der_length_t -> y: Prims.nat{y <= 126}