val tag_of_der_length32' (x: der_length_t{x < 4294967296}) : Tot (z: U8.t{z == tag_of_der_length x})
let tag_of_der_length32'
  (x: der_length_t { x < 4294967296 } )
: Tot (z: U8.t { z == tag_of_der_length x })
= if x < 128
  then U8.uint_to_t x
  else
    [@inline_let]
    let len_len = log256' x in
    [@inline_let] let _ =
      log256_eq x;
      assert_norm (der_length_max == pow2 (8 * 126) - 1);
      Math.pow2_lt_recip (8 * (len_len - 1)) (8 * 126)
    in
    128uy `U8.add` U8.uint_to_t len_len
val tag_of_der_length32' (x: der_length_t{x < 4294967296}) : Tot (z: U8.t{z == tag_of_der_length x})
let tag_of_der_length32' (x: der_length_t{x < 4294967296}) : Tot (z: U8.t{z == tag_of_der_length x}) =
if x < 128
then U8.uint_to_t x
else
  [@@ inline_let ]let len_len = log256' x in
  [@@ inline_let ]let _ =
    log256_eq x;
    assert_norm (der_length_max == pow2 (8 * 126) - 1);
    Math.pow2_lt_recip (8 * (len_len - 1)) (8 * 126)
  in
  128uy `U8.add` (U8.uint_to_t len_len)
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 Prims.b2t Prims.op_LessThan FStar.UInt8.uint_to_t Prims.bool FStar.UInt8.add FStar.UInt8.__uint_to_t Prims.unit LowParse.Math.pow2_lt_recip FStar.Mul.op_Star Prims.op_Subtraction FStar.Pervasives.assert_norm Prims.eq2 Prims.int LowParse.Spec.DER.der_length_max Prims.pow2 LowParse.Spec.DER.log256_eq LowParse.Spec.BoundedInt.integer_size LowParse.Spec.BoundedInt.log256' FStar.UInt8.t LowParse.Spec.DER.tag_of_der_length
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)
: Tot (y: nat { y <= 126 })
= der_length_payload_size_of_tag (tag_of_der_length x)

val der_length_payload_size_le
  (x1 x2: der_length_t)
: Lemma
  (requires (x1 <= x2))
  (ensures (der_length_payload_size x1 <= der_length_payload_size x2))

let lint (len: nat) : Tot Type = (x: nat { x < pow2 (8 * len) })

module U32 = FStar.UInt32

let tag_of_der_length32
  (x: U32.t)
: GTot U8.t
= let _ = assert_norm (pow2 32 - 1 <= der_length_max) in
  tag_of_der_length (U32.v x)

val parse_der_length_payload32
  (x: U8.t { der_length_payload_size_of_tag x <= 4 } )
: Tot (parser (parse_der_length_payload_kind x) (refine_with_tag tag_of_der_length32 x))

val parse_der_length_payload32_unfold
  (x: U8.t { der_length_payload_size_of_tag x <= 4 } )
  (input: bytes)
: Lemma
  (
    let y = parse (parse_der_length_payload32 x) input in
    (256 < der_length_max) /\ (
    if U8.v x < 128
    then tag_of_der_length (U8.v x) == x /\ y == Some (Cast.uint8_to_uint32 x, 0)
    else if x = 128uy || x = 255uy
    then y == None
    else if x = 129uy
    then
      match parse parse_u8 input with
      | None -> y == None
      | Some (z, consumed) ->
        if U8.v z < 128
        then y == None
        else tag_of_der_length (U8.v z) == x /\ y == Some (Cast.uint8_to_uint32 z, consumed)
    else
      let len : nat = U8.v x - 128 in
      2 <= len /\ len <= 4 /\
      (
      let res : option (bounded_integer len & consumed_length input) = parse (parse_bounded_integer len) input in
      match res with
      | None -> y == None
      | Some (z, consumed) ->
        len > 0 /\ (
        if U32.v z >= pow2 (8 * (len - 1))
        then U32.v z <= der_length_max /\ tag_of_der_length32 z == x /\ y == Some ((z <: refine_with_tag tag_of_der_length32 x), consumed)
        else y == None
  ))))

val log256_eq
  (x: nat)
: Lemma
  (requires (x > 0 /\ x < 4294967296))
  (ensures (log256 x == log256' x))

inline_for_extraction
let tag_of_der_length32'
  (x: der_length_t { x < 4294967296 } )
val tag_of_der_length32' (x: der_length_t{x < 4294967296}) : Tot (z: U8.t{z == tag_of_der_length x})
x: LowParse.Spec.DER.der_length_t{x < 4294967296}
  -> z: FStar.UInt8.t{z == LowParse.Spec.DER.tag_of_der_length x}