val der_length_max:nat
let der_length_max : nat = 2743062034396844341627968125593604635037196317966166035056000994228098690879836473582587849768181396806642362668936055872479091931372323951612051859122835149807249350355003132267795098895967012320756270631179897595796976964454084495146379250195728106130226298287754794921070036903071843030324651025760255
val der_length_max:nat
let der_length_max:nat =
2743062034396844341627968125593604635037196317966166035056000994228098690879836473582587849768181396806642362668936055872479091931372323951612051859122835149807249350355003132267795098895967012320756270631179897595796976964454084495146379250195728106130226298287754794921070036903071843030324651025760255
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
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"
val der_length_max:nat
Prims.nat