val prelude:string
let prelude : string =
"
(set-option :produce-models true)
(declare-datatypes () ((State (mk-state (input-size Int) (choice-index Int)))))
(declare-datatypes () ((Result (mk-result (return-value Int) (after-state State)))))

(define-fun parse-empty ((x State)) Result
  (mk-result 0 x)
)

(declare-fun choose (Int) Int)
(assert (forall ((i Int))
  (and (<= 0 (choose i)) (< (choose i) 256))
))

(define-fun parse-false ((x State)) State
  (mk-state -1 (choice-index x))
)

(define-fun parse-all-bytes ((x State)) State
  (if (<= (input-size x) 0)
    x
    (mk-state 0 (+ (choice-index x) (input-size x)))
  )
)

(define-fun parse-all-zeros ((x State)) State
  (if (<= (input-size x) 0)
    x
    (mk-state
      (if
        (forall ((j Int))
          (if (and (<= 0 j) (< j (input-size x)))
            (= (choose (+ (choice-index x) j)) 0)
            true
          )
        )
        0
        -1
      )
      (+ (choice-index x) (input-size x))
    )
  )
)

(define-fun parse-u8 ((x State)) Result
  (mk-result
    (choose (choice-index x))
    (mk-state (- (input-size x) 1) (+ (choice-index x) 1))
  )
)

(define-fun parse-u16-be ((x State)) Result
  (mk-result
    (+ (choose (+ 1 (choice-index x)))
      (* 256
        (choose (+ 0 (choice-index x)))
      )
    )
    (mk-state (- (input-size x) 2) (+ (choice-index x) 2))
  )
)

(define-fun parse-u16-le ((x State)) Result
  (mk-result
    (+ (choose (+ 0 (choice-index x)))
      (* 256
        (choose (+ 1 (choice-index x)))
      )
    )
    (mk-state (- (input-size x) 2) (+ (choice-index x) 2))
  )
)

(define-fun parse-u32-be ((x State)) Result
  (mk-result
    (+ (choose (+ 3 (choice-index x)))
      (* 256
        (+ (choose (+ 2 (choice-index x)))
          (* 256
            (+ (choose (+ 1 (choice-index x)))
              (* 256
                (choose (+ 0 (choice-index x)))
              )
            )
          )
        )
      )
    )
    (mk-state (- (input-size x) 4) (+ (choice-index x) 4))
  )
)

(define-fun parse-u32-le ((x State)) Result
  (mk-result
    (+ (choose (+ 0 (choice-index x)))
      (* 256
        (+ (choose (+ 1 (choice-index x)))
          (* 256
            (+ (choose (+ 2 (choice-index x)))
              (* 256
                (choose (+ 3 (choice-index x)))
              )
            )
          )
        )
      )
    )
    (mk-state (- (input-size x) 4) (+ (choice-index x) 4))
  )
)

(define-fun parse-u64-be ((x State)) Result
  (mk-result
    (+ (choose (+ 7 (choice-index x)))
      (* 256
        (+ (choose (+ 6 (choice-index x)))
          (* 256
            (+ (choose (+ 5 (choice-index x)))
              (* 256
                (+ (choose (+ 4 (choice-index x)))
                  (* 256
                    (+ (choose (+ 3 (choice-index x)))
                      (* 256
                        (+ (choose (+ 2 (choice-index x)))
                          (* 256
                            (+ (choose (+ 1 (choice-index x)))
                              (* 256
                                (choose (+ 0 (choice-index x)))
                              )
                            )
                          )
                        )
                      )
                    )
                  )
                )
              )
            )
          )
        )
      )
    )
    (mk-state (- (input-size x) 8) (+ (choice-index x) 8))
  )
)

(define-fun parse-u64-le ((x State)) Result
  (mk-result
    (+ (choose (+ 0 (choice-index x)))
      (* 256
        (+ (choose (+ 1 (choice-index x)))
          (* 256
            (+ (choose (+ 2 (choice-index x)))
              (* 256
                (+ (choose (+ 3 (choice-index x)))
                  (* 256
                    (+ (choose (+ 4 (choice-index x)))
                      (* 256
                        (+ (choose (+ 5 (choice-index x)))
                          (* 256
                            (+ (choose (+ 6 (choice-index x)))
                              (* 256
                                (choose (+ 7 (choice-index x)))
                              )
                            )
                          )
                        )
                      )
                    )
                  )
                )
              )
            )
          )
        )
      )
    )
    (mk-state (- (input-size x) 8) (+ (choice-index x) 8))
  )
)

(define-fun-rec pow-2 ((amount Int)) Int
  (if (<= amount 0)
    1
    (* 2 (pow-2 (- amount 1)))
  )
)

;; see LowParse.BitFields.get_bitfield_eq
(define-fun get-bitfield-lsb ((nbBits Int) (value Int) (bitsFrom Int) (bitsTo Int)) Int
  (mod (div value (pow-2 bitsFrom)) (pow-2 (- bitsTo bitsFrom)))
)

;; see EverParse3d.Prelude.StaticHeader
(define-fun get-bitfield-msb ((nbBits Int) (value Int) (bitsFrom Int) (bitsTo Int)) Int
  (get-bitfield-lsb nbBits value (- nbBits bitsTo) (- nbBits bitsFrom))
)

(declare-const initial-input-size Int)
(assert (>= initial-input-size 0))
(define-fun initial-state () State (mk-state initial-input-size 0))

"
val prelude:string
let prelude:string =
"\n(set-option :produce-models true)\n(declare-datatypes () ((State (mk-state (input-size Int) (choice-index Int)))))\n(declare-datatypes () ((Result (mk-result (return-value Int) (after-state State)))))\n\n(define-fun parse-empty ((x State)) Result\n  (mk-result 0 x)\n)\n\n(declare-fun choose (Int) Int)\n(assert (forall ((i Int))\n  (and (<= 0 (choose i)) (< (choose i) 256))\n))\n\n(define-fun parse-false ((x State)) State\n  (mk-state -1 (choice-index x))\n)\n\n(define-fun parse-all-bytes ((x State)) State\n  (if (<= (input-size x) 0)\n    x\n    (mk-state 0 (+ (choice-index x) (input-size x)))\n  )\n)\n\n(define-fun parse-all-zeros ((x State)) State\n  (if (<= (input-size x) 0)\n    x\n    (mk-state\n      (if\n        (forall ((j Int))\n          (if (and (<= 0 j) (< j (input-size x)))\n            (= (choose (+ (choice-index x) j)) 0)\n            true\n          )\n        )\n        0\n        -1\n      )\n      (+ (choice-index x) (input-size x))\n    )\n  )\n)\n\n(define-fun parse-u8 ((x State)) Result\n  (mk-result\n    (choose (choice-index x))\n    (mk-state (- (input-size x) 1) (+ (choice-index x) 1))\n  )\n)\n\n(define-fun parse-u16-be ((x State)) Result\n  (mk-result\n    (+ (choose (+ 1 (choice-index x)))\n      (* 256\n        (choose (+ 0 (choice-index x)))\n      )\n    )\n    (mk-state (- (input-size x) 2) (+ (choice-index x) 2))\n  )\n)\n\n(define-fun parse-u16-le ((x State)) Result\n  (mk-result\n    (+ (choose (+ 0 (choice-index x)))\n      (* 256\n        (choose (+ 1 (choice-index x)))\n      )\n    )\n    (mk-state (- (input-size x) 2) (+ (choice-index x) 2))\n  )\n)\n\n(define-fun parse-u32-be ((x State)) Result\n  (mk-result\n    (+ (choose (+ 3 (choice-index x)))\n      (* 256\n        (+ (choose (+ 2 (choice-index x)))\n          (* 256\n            (+ (choose (+ 1 (choice-index x)))\n              (* 256\n                (choose (+ 0 (choice-index x)))\n              )\n            )\n          )\n        )\n      )\n    )\n    (mk-state (- (input-size x) 4) (+ (choice-index x) 4))\n  )\n)\n\n(define-fun parse-u32-le ((x State)) Result\n  (mk-result\n    (+ (choose (+ 0 (choice-index x)))\n      (* 256\n        (+ (choose (+ 1 (choice-index x)))\n          (* 256\n            (+ (choose (+ 2 (choice-index x)))\n              (* 256\n                (choose (+ 3 (choice-index x)))\n              )\n            )\n          )\n        )\n      )\n    )\n    (mk-state (- (input-size x) 4) (+ (choice-index x) 4))\n  )\n)\n\n(define-fun parse-u64-be ((x State)) Result\n  (mk-result\n    (+ (choose (+ 7 (choice-index x)))\n      (* 256\n        (+ (choose (+ 6 (choice-index x)))\n          (* 256\n            (+ (choose (+ 5 (choice-index x)))\n              (* 256\n                (+ (choose (+ 4 (choice-index x)))\n                  (* 256\n                    (+ (choose (+ 3 (choice-index x)))\n                      (* 256\n                        (+ (choose (+ 2 (choice-index x)))\n                          (* 256\n                            (+ (choose (+ 1 (choice-index x)))\n                              (* 256\n                                (choose (+ 0 (choice-index x)))\n                              )\n                            )\n                          )\n                        )\n                      )\n                    )\n                  )\n                )\n              )\n            )\n          )\n        )\n      )\n    )\n    (mk-state (- (input-size x) 8) (+ (choice-index x) 8))\n  )\n)\n\n(define-fun parse-u64-le ((x State)) Result\n  (mk-result\n    (+ (choose (+ 0 (choice-index x)))\n      (* 256\n        (+ (choose (+ 1 (choice-index x)))\n          (* 256\n            (+ (choose (+ 2 (choice-index x)))\n              (* 256\n                (+ (choose (+ 3 (choice-index x)))\n                  (* 256\n                    (+ (choose (+ 4 (choice-index x)))\n                      (* 256\n                        (+ (choose (+ 5 (choice-index x)))\n                          (* 256\n                            (+ (choose (+ 6 (choice-index x)))\n                              (* 256\n                                (choose (+ 7 (choice-index x)))\n                              )\n                            )\n                          )\n                        )\n                      )\n                    )\n                  )\n                )\n              )\n            )\n          )\n        )\n      )\n    )\n    (mk-state (- (input-size x) 8) (+ (choice-index x) 8))\n  )\n)\n\n(define-fun-rec pow-2 ((amount Int)) Int\n  (if (<= amount 0)\n    1\n    (* 2 (pow-2 (- amount 1)))\n  )\n)\n\n;; see LowParse.BitFields.get_bitfield_eq\n(define-fun get-bitfield-lsb ((nbBits Int) (value Int) (bitsFrom Int) (bitsTo Int)) Int\n  (mod (div value (pow-2 bitsFrom)) (pow-2 (- bitsTo bitsFrom)))\n)\n\n;; see EverParse3d.Prelude.StaticHeader\n(define-fun get-bitfield-msb ((nbBits Int) (value Int) (bitsFrom Int) (bitsTo Int)) Int\n  (get-bitfield-lsb nbBits value (- nbBits bitsTo) (- nbBits bitsFrom))\n)\n\n(declare-const initial-input-size Int)\n(assert (>= initial-input-size 0))\n(define-fun initial-state () State (mk-state initial-input-size 0))\n\n"
Z3TestGen.fst.checked
Z3.fsti.checked Target.fsti.checked prims.fst.checked OS.fsti.checked Lisp.fsti.checked InterpreterTarget.fsti.checked FStar.String.fsti.checked FStar.Seq.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.Char.fsti.checked FStar.All.fst.checked Ast.fst.checked
Z3TestGen.fst
module Z3TestGen
module Printf = FStar.Printf
open FStar.All
open FStar.Mul

module A = Ast
module T = Target
module I = InterpreterTarget
val prelude:string
Prims.string