TestKeyValueStoreCheckerGenerators.lean

import Test.KeyValueStoreExample.KeyValueStore
import Plausible.Arbitrary
import Plausible.DeriveArbitrary
import Plausible.Chamelean.ArbitrarySizedSuchThat
import Plausible.Chamelean.DeriveChecker
import Plausible.Chamelean.DeriveConstrainedProducer
import Plausible.Chamelean.EnumeratorCombinators
import Plausible.Chamelean.GeneratorCombinators

open Plausible
open KeyValueStore

-- Suppress warnings for unused variables in derived generators/checkers
set_option linter.unusedVariables false

-- Suppress warnings for redundant pattern-match cases in derived generators/checkers
set_option match.ignoreUnusedAlts true

/-- We override the default `Arbitrary` for `String`s so that we only produce strings of length 1
    where the string is a single letter from `A` to `I` -/
instance instKeyValueStoreArbitraryString : Arbitrary String where
  arbitrary := GeneratorCombinators.elementsWithDefault "A" ["A", "B", "C", "D", "E", "F", "G", "H", "I"]

---------------------------------------------------------------------------------------------------------------------------------------
-- Derived Checkers & Generators (everything below in this file is automatically generated by Chamelean)
---------------------------------------------------------------------------------------------------------------------------------------

/--
info: Try this generator: instance : ArbitrarySizedSuchThat (List (String × String)) (fun s1_1 => KeyValueStore.RemoveKV k_1 s1_1 s2_1) where
  arbitrarySizedST :=
    let rec aux_arb (initSize : Nat) (size : Nat) (k_1 : String) (s2_1 : List (String × String)) :
      OptionT Plausible.Gen (List (String × String)) :=
      match size with
      | Nat.zero =>
        OptionTGen.backtrack
          [(1,
              match s2_1 with
              | List.nil => return List.nil
              | _ => OptionT.fail)]
      | Nat.succ size' =>
        OptionTGen.backtrack
          [(1,
              match s2_1 with
              | List.nil => return List.nil
              | _ => OptionT.fail),
            (Nat.succ size', do
              let s1 ← aux_arb initSize size' k_1 s2_1;
              do
                let v ← Plausible.Arbitrary.arbitrary;
                return List.cons (Prod.mk k_1 v) s1),
            (Nat.succ size',
              match s2_1 with
              | List.cons (Prod.mk k2 v2) s2 =>
                match DecOpt.decOpt (Eq (bne k_1 k2) (Bool.true)) initSize with
                | Option.some Bool.true => do
                  let s1 ← aux_arb initSize size' k_1 s2;
                  return List.cons (Prod.mk k2 v2) s1
                | _ => OptionT.fail
              | _ => OptionT.fail)]
    fun size => aux_arb size size k_1 s2_1
-/
#guard_msgs(info, drop warning) in
#derive_generator (fun (s1 : List (String × String)) => KeyValueStore.RemoveKV k s1 s2)

/--
info: Try this generator: instance : ArbitrarySizedSuchThat (List (String × String)) (fun s2_1 => KeyValueStore.RemoveKV k_1 s1_1 s2_1) where
  arbitrarySizedST :=
    let rec aux_arb (initSize : Nat) (size : Nat) (k_1 : String) (s1_1 : List (String × String)) :
      OptionT Plausible.Gen (List (String × String)) :=
      match size with
      | Nat.zero =>
        OptionTGen.backtrack
          [(1,
              match s1_1 with
              | List.nil => return List.nil
              | _ => OptionT.fail)]
      | Nat.succ size' =>
        OptionTGen.backtrack
          [(1,
              match s1_1 with
              | List.nil => return List.nil
              | _ => OptionT.fail),
            (Nat.succ size',
              match s1_1 with
              | List.cons (Prod.mk u_3 v) s1 =>
                match DecOpt.decOpt (BEq.beq u_3 k_1) initSize with
                | Option.some Bool.true => do
                  let s2_1 ← aux_arb initSize size' k_1 s1;
                  return s2_1
                | _ => OptionT.fail
              | _ => OptionT.fail),
            (Nat.succ size',
              match s1_1 with
              | List.cons (Prod.mk k2 v2) s1 =>
                match DecOpt.decOpt (Eq (bne k_1 k2) (Bool.true)) initSize with
                | Option.some Bool.true => do
                  let s2 ← aux_arb initSize size' k_1 s1;
                  return List.cons (Prod.mk k2 v2) s2
                | _ => OptionT.fail
              | _ => OptionT.fail)]
    fun size => aux_arb size size k_1 s1_1
-/
#guard_msgs(info, drop warning) in
#derive_generator (fun (s2 : List (String × String)) => KeyValueStore.RemoveKV k s1 s2)


/--
info: Try this generator: instance : ArbitrarySizedSuchThat (List (String × String)) (fun s1_1 => KeyValueStore.AddKV k_1 v_1 s1_1 s2_1) where
  arbitrarySizedST :=
    let rec aux_arb (initSize : Nat) (size : Nat) (k_1 : String) (v_1 : String) (s2_1 : List (String × String)) :
      OptionT Plausible.Gen (List (String × String)) :=
      match size with
      | Nat.zero =>
        OptionTGen.backtrack
          [(1,
              match s2_1 with
              | List.cons (Prod.mk u_4 u_5) s1_1 =>
                match DecOpt.decOpt (BEq.beq u_4 k_1) initSize with
                | Option.some Bool.true =>
                  match DecOpt.decOpt (BEq.beq u_5 v_1) initSize with
                  | Option.some Bool.true => return s1_1
                  | _ => OptionT.fail
                | _ => OptionT.fail
              | _ => OptionT.fail)]
      | Nat.succ size' =>
        OptionTGen.backtrack
          [(1,
              match s2_1 with
              | List.cons (Prod.mk u_4 u_5) s1_1 =>
                match DecOpt.decOpt (BEq.beq u_4 k_1) initSize with
                | Option.some Bool.true =>
                  match DecOpt.decOpt (BEq.beq u_5 v_1) initSize with
                  | Option.some Bool.true => return s1_1
                  | _ => OptionT.fail
                | _ => OptionT.fail
              | _ => OptionT.fail),
            ]
    fun size => aux_arb size size k_1 v_1 s2_1
-/
#guard_msgs(info, drop warning) in
#derive_generator (fun (s1 : List (String × String)) => KeyValueStore.AddKV k v s1 s2)

/--
info: Try this generator: instance : ArbitrarySizedSuchThat (List (String × String)) (fun s2_1 => KeyValueStore.AddKV k_1 v_1 s1_1 s2_1) where
  arbitrarySizedST :=
    let rec aux_arb (initSize : Nat) (size : Nat) (k_1 : String) (v_1 : String) (s1_1 : List (String × String)) :
      OptionT Plausible.Gen (List (String × String)) :=
      match size with
      | Nat.zero => OptionTGen.backtrack [(1, return List.cons (Prod.mk k_1 v_1) s1_1)]
      | Nat.succ size' => OptionTGen.backtrack [(1, return List.cons (Prod.mk k_1 v_1) s1_1), ]
    fun size => aux_arb size size k_1 v_1 s1_1
-/
#guard_msgs(info, drop warning) in
#derive_generator (fun (s2 : List (String × String)) => KeyValueStore.AddKV k v s1 s2)

/--
info: Try this generator: instance : ArbitrarySizedSuchThat String (fun v_1 => KeyValueStore.AddKV k_1 v_1 x_1_1 s2_1) where
  arbitrarySizedST :=
    let rec aux_arb (initSize : Nat) (size : Nat) (k_1 : String) (x_1_1 : List (String × String))
      (s2_1 : List (String × String)) : OptionT Plausible.Gen String :=
      match size with
      | Nat.zero =>
        OptionTGen.backtrack
          [(1,
              match s2_1 with
              | List.cons (Prod.mk u_4 v_1) u_5 =>
                match DecOpt.decOpt (BEq.beq u_4 k_1) initSize with
                | Option.some Bool.true =>
                  match DecOpt.decOpt (BEq.beq u_5 x_1_1) initSize with
                  | Option.some Bool.true => return v_1
                  | _ => OptionT.fail
                | _ => OptionT.fail
              | _ => OptionT.fail)]
      | Nat.succ size' =>
        OptionTGen.backtrack
          [(1,
              match s2_1 with
              | List.cons (Prod.mk u_4 v_1) u_5 =>
                match DecOpt.decOpt (BEq.beq u_4 k_1) initSize with
                | Option.some Bool.true =>
                  match DecOpt.decOpt (BEq.beq u_5 x_1_1) initSize with
                  | Option.some Bool.true => return v_1
                  | _ => OptionT.fail
                | _ => OptionT.fail
              | _ => OptionT.fail),
            ]
    fun size => aux_arb size size k_1 x_1_1 s2_1
-/
#guard_msgs(info, drop warning) in
#derive_generator (fun (v : String) => KeyValueStore.AddKV k v x_1 s2)

/--
info: Try this checker: instance : DecOpt (KeyValueStore.LookupKV s_1 kv_1) where
  decOpt :=
    let rec aux_dec (initSize : Nat) (size : Nat) (s_1 : List (String × String))
      (kv_1 : StateResult × String × Nat × String) : Option Bool :=
      match size with
      | Nat.zero =>
        DecOpt.checkerBacktrack
          [fun _ =>
            match kv_1 with
            | Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v)) =>
              match s_1 with
              | List.nil => Option.some Bool.true
              | _ => Option.some Bool.false
            | _ => Option.some Bool.false,
            fun _ =>
            match kv_1 with
            | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk u_2 (Prod.mk (Nat.zero) u_3)) =>
              match s_1 with
              | List.cons (Prod.mk k v) s =>
                DecOpt.andOptList [DecOpt.decOpt (BEq.beq u_2 k) initSize, DecOpt.decOpt (BEq.beq u_3 v) initSize]
              | _ => Option.some Bool.false
            | _ => Option.some Bool.false,
            fun _ =>
            match kv_1 with
            | Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) (Prod.mk u_2 (Prod.mk (Nat.succ n) u_3)) =>
              match s_1 with
              | List.cons (Prod.mk k v) (List.nil) =>
                DecOpt.andOptList [DecOpt.decOpt (BEq.beq u_2 k) initSize, DecOpt.decOpt (BEq.beq u_3 v) initSize]
              | _ => Option.some Bool.false
            | _ => Option.some Bool.false]
      | Nat.succ size' =>
        DecOpt.checkerBacktrack
          [fun _ =>
            match kv_1 with
            | Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v)) =>
              match s_1 with
              | List.nil => Option.some Bool.true
              | _ => Option.some Bool.false
            | _ => Option.some Bool.false,
            fun _ =>
            match kv_1 with
            | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk u_2 (Prod.mk (Nat.zero) u_3)) =>
              match s_1 with
              | List.cons (Prod.mk k v) s =>
                DecOpt.andOptList [DecOpt.decOpt (BEq.beq u_2 k) initSize, DecOpt.decOpt (BEq.beq u_3 v) initSize]
              | _ => Option.some Bool.false
            | _ => Option.some Bool.false,
            fun _ =>
            match kv_1 with
            | Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) (Prod.mk u_2 (Prod.mk (Nat.succ n) u_3)) =>
              match s_1 with
              | List.cons (Prod.mk k v) (List.nil) =>
                DecOpt.andOptList [DecOpt.decOpt (BEq.beq u_2 k) initSize, DecOpt.decOpt (BEq.beq u_3 v) initSize]
              | _ => Option.some Bool.false
            | _ => Option.some Bool.false,
            fun _ =>
            match kv_1 with
            | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k1 (Prod.mk n' v1)) =>
              match s_1 with
              | List.cons (Prod.mk k2 v2) s =>
                EnumeratorCombinators.enumerating Enum.enum
                  (fun n =>
                    DecOpt.andOptList
                      [aux_dec initSize size' s (Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k1 (Prod.mk n v1))),
                        DecOpt.decOpt (Eq n' (KeyValueStore.ver k1 k2 n)) initSize])
                  (min 2 initSize)
              | _ => Option.some Bool.false
            | _ => Option.some Bool.false,
            fun _ =>
            match kv_1 with
            | Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) (Prod.mk k1 (Prod.mk n' v1)) =>
              match s_1 with
              | List.cons (Prod.mk k2 v2) s =>
                EnumeratorCombinators.enumerating Enum.enum
                  (fun n =>
                    DecOpt.andOptList
                      [aux_dec initSize size' s
                          (Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) (Prod.mk k1 (Prod.mk n v1))),
                        DecOpt.decOpt (Eq n' (KeyValueStore.ver k1 k2 n)) initSize])
                  (min 2 initSize)
              | _ => Option.some Bool.false
            | _ => Option.some Bool.false]
    fun size => aux_dec size size s_1 kv_1
-/
#guard_msgs(info, drop warning) in
#derive_checker (KeyValueStore.LookupKV s kv)

/--
info: Try this generator: instance : ArbitrarySizedSuchThat (List (String × String)) (fun s1_1 => KeyValueStore.LookupKV s1_1 kv_1) where
  arbitrarySizedST :=
    let rec aux_arb (initSize : Nat) (size : Nat) (kv_1 : StateResult × String × Nat × String) :
      OptionT Plausible.Gen (List (String × String)) :=
      match size with
      | Nat.zero =>
        OptionTGen.backtrack
          [(1,
              match kv_1 with
              | Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v)) =>
                return List.nil
              | _ => OptionT.fail),
            (1,
              match kv_1 with
              | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v)) => do
                let s ← Plausible.Arbitrary.arbitrary;
                return List.cons (Prod.mk k v) s
              | _ => OptionT.fail),
            (1,
              match kv_1 with
              | Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) (Prod.mk k (Prod.mk (Nat.succ n) v)) =>
                return List.cons (Prod.mk k v) (List.nil)
              | _ => OptionT.fail)]
      | Nat.succ size' =>
        OptionTGen.backtrack
          [(1,
              match kv_1 with
              | Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v)) =>
                return List.nil
              | _ => OptionT.fail),
            (1,
              match kv_1 with
              | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v)) => do
                let s ← Plausible.Arbitrary.arbitrary;
                return List.cons (Prod.mk k v) s
              | _ => OptionT.fail),
            (1,
              match kv_1 with
              | Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) (Prod.mk k (Prod.mk (Nat.succ n) v)) =>
                return List.cons (Prod.mk k v) (List.nil)
              | _ => OptionT.fail),
            (Nat.succ size',
              match kv_1 with
              | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k1 (Prod.mk n' v1)) => do
                let k2 ← Plausible.Arbitrary.arbitrary;
                do
                  let n ← Plausible.Arbitrary.arbitrary;
                  do
                    let v2 ← Plausible.Arbitrary.arbitrary;
                    match DecOpt.decOpt (Eq n' (KeyValueStore.ver k1 k2 n)) initSize with
                      | Option.some Bool.true => do
                        let s ←
                          aux_arb initSize size' (Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k1 (Prod.mk n v1)));
                        return List.cons (Prod.mk k2 v2) s
                      | _ => OptionT.fail
              | _ => OptionT.fail),
            (Nat.succ size',
              match kv_1 with
              | Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) (Prod.mk k1 (Prod.mk n' v1)) => do
                let k2 ← Plausible.Arbitrary.arbitrary;
                do
                  let n ← Plausible.Arbitrary.arbitrary;
                  do
                    let v2 ← Plausible.Arbitrary.arbitrary;
                    match DecOpt.decOpt (Eq n' (KeyValueStore.ver k1 k2 n)) initSize with
                      | Option.some Bool.true => do
                        let s ←
                          aux_arb initSize size'
                              (Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) (Prod.mk k1 (Prod.mk n v1)));
                        return List.cons (Prod.mk k2 v2) s
                      | _ => OptionT.fail
              | _ => OptionT.fail)]
    fun size => aux_arb size size kv_1
-/
#guard_msgs(info, drop warning) in
#derive_generator (fun (s1 : List (String × String)) => KeyValueStore.LookupKV s1 kv)

/--
info: Try this checker: instance : DecOpt (KeyValueStore.AddKV k2_1 v_1 s_1_1 s2_1) where
  decOpt :=
    let rec aux_dec (initSize : Nat) (size : Nat) (k2_1 : String) (v_1 : String) (s_1_1 : List (String × String))
      (s2_1 : List (String × String)) : Option Bool :=
      match size with
      | Nat.zero =>
        DecOpt.checkerBacktrack
          [fun _ =>
            match s2_1 with
            | List.cons (Prod.mk u_4 u_5) u_6 =>
              DecOpt.andOptList
                [DecOpt.decOpt (BEq.beq u_6 s_1_1) initSize,
                  DecOpt.andOptList
                    [DecOpt.decOpt (BEq.beq u_5 v_1) initSize, DecOpt.decOpt (BEq.beq u_4 k2_1) initSize]]
            | _ => Option.some Bool.false]
      | Nat.succ size' =>
        DecOpt.checkerBacktrack
          [fun _ =>
            match s2_1 with
            | List.cons (Prod.mk u_4 u_5) u_6 =>
              DecOpt.andOptList
                [DecOpt.decOpt (BEq.beq u_6 s_1_1) initSize,
                  DecOpt.andOptList
                    [DecOpt.decOpt (BEq.beq u_5 v_1) initSize, DecOpt.decOpt (BEq.beq u_4 k2_1) initSize]]
            | _ => Option.some Bool.false,
            ]
    fun size => aux_dec size size k2_1 v_1 s_1_1 s2_1
-/
#guard_msgs(info, drop warning) in
#derive_checker (KeyValueStore.AddKV k2 v s_1 s2)

/--
info: Try this generator: instance : ArbitrarySizedSuchThat (List (String × String)) (fun s_1 => KeyValueStore.EvalStateApiCall s_1 x_1) where
  arbitrarySizedST :=
    let rec aux_arb (initSize : Nat) (size : Nat) (x_1 : StateAPICall × StateResult × List (String × String)) :
      OptionT Plausible.Gen (List (String × String)) :=
      match size with
      | Nat.zero =>
        OptionTGen.backtrack
          [(1,
              match x_1 with
              |
              Prod.mk (KeyValueStore.StateAPICall.Get k (Option.none))
                  (Prod.mk (KeyValueStore.StateResult.Result v) s_1) =>
                match
                  DecOpt.decOpt
                    (KeyValueStore.LookupKV s_1
                      (Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v))))
                    initSize with
                | Option.some Bool.true => return s_1
                | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              |
              Prod.mk (KeyValueStore.StateAPICall.Get k (Option.none))
                  (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) s_1) =>
                do
                let v ← Plausible.Arbitrary.arbitrary;
                match
                    DecOpt.decOpt
                      (KeyValueStore.LookupKV s_1
                        (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v))))
                      initSize with
                  | Option.some Bool.true => return s_1
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              |
              Prod.mk (KeyValueStore.StateAPICall.Get k (Option.some n))
                  (Prod.mk (KeyValueStore.StateResult.Result v) s_1) =>
                match
                  DecOpt.decOpt
                    (KeyValueStore.LookupKV s_1 (Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk n v))))
                    initSize with
                | Option.some Bool.true => return s_1
                | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              |
              Prod.mk (KeyValueStore.StateAPICall.Get k (Option.some n))
                  (Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) s_1) =>
                do
                let v ← Plausible.Arbitrary.arbitrary;
                match
                    DecOpt.decOpt
                      (KeyValueStore.LookupKV s_1
                        (Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) (Prod.mk k (Prod.mk n v))))
                      initSize with
                  | Option.some Bool.true => return s_1
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              | Prod.mk (KeyValueStore.StateAPICall.KeyExists k) (Prod.mk (KeyValueStore.StateResult.Ok) s_1) => do
                let v ← Plausible.Arbitrary.arbitrary;
                match
                    DecOpt.decOpt
                      (KeyValueStore.LookupKV s_1
                        (Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v))))
                      initSize with
                  | Option.some Bool.true => return s_1
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              |
              Prod.mk (KeyValueStore.StateAPICall.KeyExists k)
                  (Prod.mk (KeyValueStore.StateResult.NoSuchKeyResult) s_1) =>
                do
                let v ← Plausible.Arbitrary.arbitrary;
                match
                    DecOpt.decOpt
                      (KeyValueStore.LookupKV s_1
                        (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v))))
                      initSize with
                  | Option.some Bool.true => return s_1
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              | Prod.mk (KeyValueStore.StateAPICall.Set k v) (Prod.mk (KeyValueStore.StateResult.Ok) s2) => do
                let s_1 ← ArbitrarySizedSuchThat.arbitrarySizedST (fun s_1 => KeyValueStore.AddKV k v s_1 s2) initSize;
                return s_1
              | _ => OptionT.fail),
            (1,
              match x_1 with
              | Prod.mk (KeyValueStore.StateAPICall.Copy k k2) (Prod.mk (KeyValueStore.StateResult.Ok) s2) => do
                let v ← Plausible.Arbitrary.arbitrary;
                do
                  let s_1 ←
                    ArbitrarySizedSuchThat.arbitrarySizedST
                        (fun s_1 =>
                          KeyValueStore.LookupKV s_1
                            (Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v))))
                        initSize;
                  match DecOpt.decOpt (KeyValueStore.AddKV k2 v s_1 s2) initSize with
                    | Option.some Bool.true => return s_1
                    | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              |
              Prod.mk (KeyValueStore.StateAPICall.Copy k k2)
                  (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) s_1) =>
                do
                let v ← Plausible.Arbitrary.arbitrary;
                match
                    DecOpt.decOpt
                      (KeyValueStore.LookupKV s_1
                        (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v))))
                      initSize with
                  | Option.some Bool.true => return s_1
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              | Prod.mk (KeyValueStore.StateAPICall.Append k v3) (Prod.mk (KeyValueStore.StateResult.Ok) s2) => do
                let s_1 ← ArbitrarySizedSuchThat.arbitrarySizedST (fun s_1 => KeyValueStore.AddKV k v3 s_1 s2) initSize;
                do
                  let v ← Plausible.Arbitrary.arbitrary;
                  do
                    let v2 ← Plausible.Arbitrary.arbitrary;
                    match
                        DecOpt.decOpt
                          (KeyValueStore.LookupKV s_1
                            (Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v))))
                          initSize with
                      | Option.some Bool.true =>
                        match DecOpt.decOpt (Eq v3 (HAppend.hAppend v v2)) initSize with
                        | Option.some Bool.true => return s_1
                        | _ => OptionT.fail
                      | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              |
              Prod.mk (KeyValueStore.StateAPICall.Append k v2)
                  (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) s_1) =>
                do
                let v ← Plausible.Arbitrary.arbitrary;
                match
                    DecOpt.decOpt
                      (KeyValueStore.LookupKV s_1
                        (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v))))
                      initSize with
                  | Option.some Bool.true => return s_1
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              | Prod.mk (KeyValueStore.StateAPICall.Delete k) (Prod.mk (KeyValueStore.StateResult.Ok) s2) => do
                let s_1 ← ArbitrarySizedSuchThat.arbitrarySizedST (fun s_1 => KeyValueStore.RemoveKV k s_1 s2) initSize;
                do
                  let v ← Plausible.Arbitrary.arbitrary;
                  match
                      DecOpt.decOpt
                        (KeyValueStore.LookupKV s_1
                          (Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v))))
                        initSize with
                    | Option.some Bool.true => return s_1
                    | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              |
              Prod.mk (KeyValueStore.StateAPICall.Delete k)
                  (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) s_1) =>
                do
                let v ← Plausible.Arbitrary.arbitrary;
                match
                    DecOpt.decOpt
                      (KeyValueStore.LookupKV s_1
                        (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v))))
                      initSize with
                  | Option.some Bool.true => return s_1
                  | _ => OptionT.fail
              | _ => OptionT.fail)]
      | Nat.succ size' =>
        OptionTGen.backtrack
          [(1,
              match x_1 with
              |
              Prod.mk (KeyValueStore.StateAPICall.Get k (Option.none))
                  (Prod.mk (KeyValueStore.StateResult.Result v) s_1) =>
                match
                  DecOpt.decOpt
                    (KeyValueStore.LookupKV s_1
                      (Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v))))
                    initSize with
                | Option.some Bool.true => return s_1
                | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              |
              Prod.mk (KeyValueStore.StateAPICall.Get k (Option.none))
                  (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) s_1) =>
                do
                let v ← Plausible.Arbitrary.arbitrary;
                match
                    DecOpt.decOpt
                      (KeyValueStore.LookupKV s_1
                        (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v))))
                      initSize with
                  | Option.some Bool.true => return s_1
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              |
              Prod.mk (KeyValueStore.StateAPICall.Get k (Option.some n))
                  (Prod.mk (KeyValueStore.StateResult.Result v) s_1) =>
                match
                  DecOpt.decOpt
                    (KeyValueStore.LookupKV s_1 (Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk n v))))
                    initSize with
                | Option.some Bool.true => return s_1
                | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              |
              Prod.mk (KeyValueStore.StateAPICall.Get k (Option.some n))
                  (Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) s_1) =>
                do
                let v ← Plausible.Arbitrary.arbitrary;
                match
                    DecOpt.decOpt
                      (KeyValueStore.LookupKV s_1
                        (Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) (Prod.mk k (Prod.mk n v))))
                      initSize with
                  | Option.some Bool.true => return s_1
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              | Prod.mk (KeyValueStore.StateAPICall.KeyExists k) (Prod.mk (KeyValueStore.StateResult.Ok) s_1) => do
                let v ← Plausible.Arbitrary.arbitrary;
                match
                    DecOpt.decOpt
                      (KeyValueStore.LookupKV s_1
                        (Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v))))
                      initSize with
                  | Option.some Bool.true => return s_1
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              |
              Prod.mk (KeyValueStore.StateAPICall.KeyExists k)
                  (Prod.mk (KeyValueStore.StateResult.NoSuchKeyResult) s_1) =>
                do
                let v ← Plausible.Arbitrary.arbitrary;
                match
                    DecOpt.decOpt
                      (KeyValueStore.LookupKV s_1
                        (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v))))
                      initSize with
                  | Option.some Bool.true => return s_1
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              | Prod.mk (KeyValueStore.StateAPICall.Set k v) (Prod.mk (KeyValueStore.StateResult.Ok) s2) => do
                let s_1 ← ArbitrarySizedSuchThat.arbitrarySizedST (fun s_1 => KeyValueStore.AddKV k v s_1 s2) initSize;
                return s_1
              | _ => OptionT.fail),
            (1,
              match x_1 with
              | Prod.mk (KeyValueStore.StateAPICall.Copy k k2) (Prod.mk (KeyValueStore.StateResult.Ok) s2) => do
                let v ← Plausible.Arbitrary.arbitrary;
                do
                  let s_1 ←
                    ArbitrarySizedSuchThat.arbitrarySizedST
                        (fun s_1 =>
                          KeyValueStore.LookupKV s_1
                            (Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v))))
                        initSize;
                  match DecOpt.decOpt (KeyValueStore.AddKV k2 v s_1 s2) initSize with
                    | Option.some Bool.true => return s_1
                    | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              |
              Prod.mk (KeyValueStore.StateAPICall.Copy k k2)
                  (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) s_1) =>
                do
                let v ← Plausible.Arbitrary.arbitrary;
                match
                    DecOpt.decOpt
                      (KeyValueStore.LookupKV s_1
                        (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v))))
                      initSize with
                  | Option.some Bool.true => return s_1
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              | Prod.mk (KeyValueStore.StateAPICall.Append k v3) (Prod.mk (KeyValueStore.StateResult.Ok) s2) => do
                let s_1 ← ArbitrarySizedSuchThat.arbitrarySizedST (fun s_1 => KeyValueStore.AddKV k v3 s_1 s2) initSize;
                do
                  let v ← Plausible.Arbitrary.arbitrary;
                  do
                    let v2 ← Plausible.Arbitrary.arbitrary;
                    match
                        DecOpt.decOpt
                          (KeyValueStore.LookupKV s_1
                            (Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v))))
                          initSize with
                      | Option.some Bool.true =>
                        match DecOpt.decOpt (Eq v3 (HAppend.hAppend v v2)) initSize with
                        | Option.some Bool.true => return s_1
                        | _ => OptionT.fail
                      | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              |
              Prod.mk (KeyValueStore.StateAPICall.Append k v2)
                  (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) s_1) =>
                do
                let v ← Plausible.Arbitrary.arbitrary;
                match
                    DecOpt.decOpt
                      (KeyValueStore.LookupKV s_1
                        (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v))))
                      initSize with
                  | Option.some Bool.true => return s_1
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              | Prod.mk (KeyValueStore.StateAPICall.Delete k) (Prod.mk (KeyValueStore.StateResult.Ok) s2) => do
                let s_1 ← ArbitrarySizedSuchThat.arbitrarySizedST (fun s_1 => KeyValueStore.RemoveKV k s_1 s2) initSize;
                do
                  let v ← Plausible.Arbitrary.arbitrary;
                  match
                      DecOpt.decOpt
                        (KeyValueStore.LookupKV s_1
                          (Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v))))
                        initSize with
                    | Option.some Bool.true => return s_1
                    | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match x_1 with
              |
              Prod.mk (KeyValueStore.StateAPICall.Delete k)
                  (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) s_1) =>
                do
                let v ← Plausible.Arbitrary.arbitrary;
                match
                    DecOpt.decOpt
                      (KeyValueStore.LookupKV s_1
                        (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v))))
                      initSize with
                  | Option.some Bool.true => return s_1
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            ]
    fun size => aux_arb size size x_1
-/
#guard_msgs(info, drop warning) in
#derive_generator (fun (s : List (String × String)) => KeyValueStore.EvalStateApiCall s x)

/--
info: Try this generator: instance : ArbitrarySizedSuchThat (StateResult × String × Nat × String) (fun kv_1 => KeyValueStore.LookupKV s_1 kv_1)
    where
  arbitrarySizedST :=
    let rec aux_arb (initSize : Nat) (size : Nat) (s_1 : List (String × String)) :
      OptionT Plausible.Gen (StateResult × String × Nat × String) :=
      match size with
      | Nat.zero =>
        OptionTGen.backtrack
          [(1,
              match s_1 with
              | List.nil => do
                let k ← Plausible.Arbitrary.arbitrary;
                do
                  let v ← Plausible.Arbitrary.arbitrary;
                  return Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v))
              | _ => OptionT.fail),
            (1,
              match s_1 with
              | List.cons (Prod.mk k v) s =>
                return Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v))
              | _ => OptionT.fail),
            (1,
              match s_1 with
              | List.cons (Prod.mk k v) (List.nil) => do
                let n ← Plausible.Arbitrary.arbitrary;
                return Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) (Prod.mk k (Prod.mk (Nat.succ n) v))
              | _ => OptionT.fail)]
      | Nat.succ size' =>
        OptionTGen.backtrack
          [(1,
              match s_1 with
              | List.nil => do
                let k ← Plausible.Arbitrary.arbitrary;
                do
                  let v ← Plausible.Arbitrary.arbitrary;
                  return Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v))
              | _ => OptionT.fail),
            (1,
              match s_1 with
              | List.cons (Prod.mk k v) s =>
                return Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v))
              | _ => OptionT.fail),
            (1,
              match s_1 with
              | List.cons (Prod.mk k v) (List.nil) => do
                let n ← Plausible.Arbitrary.arbitrary;
                return Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) (Prod.mk k (Prod.mk (Nat.succ n) v))
              | _ => OptionT.fail),
            (Nat.succ size',
              match s_1 with
              | List.cons (Prod.mk k2 v2) s => do
                let vk1_n_v1 ← aux_arb initSize size' s;
                match vk1_n_v1 with
                  | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k1 (Prod.mk n v1)) => do
                    let n' ←
                      ArbitrarySizedSuchThat.arbitrarySizedST (fun n' => Eq n' (KeyValueStore.ver k1 k2 n)) initSize;
                    return Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k1 (Prod.mk n' v1))
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            (Nat.succ size',
              match s_1 with
              | List.cons (Prod.mk k2 v2) s => do
                let vk1_n_v1 ← aux_arb initSize size' s;
                match vk1_n_v1 with
                  | Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) (Prod.mk k1 (Prod.mk n v1)) => do
                    let n' ←
                      ArbitrarySizedSuchThat.arbitrarySizedST (fun n' => Eq n' (KeyValueStore.ver k1 k2 n)) initSize;
                    return Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) (Prod.mk k1 (Prod.mk n' v1))
                  | _ => OptionT.fail
              | _ => OptionT.fail)]
    fun size => aux_arb size size s_1
-/
#guard_msgs(info, drop warning) in
#derive_generator (fun (kv : StateResult × String × Nat × String) => KeyValueStore.LookupKV s kv)

/--
info: Try this generator: instance : ArbitrarySizedSuchThat (Nat × List (String × String)) (fun nb_1 => KeyValueStore.GetBucket s_1 nb_1) where
  arbitrarySizedST :=
    let rec aux_arb (initSize : Nat) (size : Nat) (s_1 : List (Nat × List (String × String))) :
      OptionT Plausible.Gen (Nat × List (String × String)) :=
      match size with
      | Nat.zero =>
        OptionTGen.backtrack
          [(1,
              match s_1 with
              | List.cons (Prod.mk n x) s => return Prod.mk n x
              | _ => OptionT.fail)]
      | Nat.succ size' =>
        OptionTGen.backtrack
          [(1,
              match s_1 with
              | List.cons (Prod.mk n x) s => return Prod.mk n x
              | _ => OptionT.fail),
            (Nat.succ size',
              match s_1 with
              | List.cons (Prod.mk n' x') s => do
                let vn_x ← aux_arb initSize size' s;
                match vn_x with
                  | Prod.mk n x =>
                    match DecOpt.decOpt (Eq (bne n n') (Bool.true)) initSize with
                    | Option.some Bool.true => return Prod.mk n x
                    | _ => OptionT.fail
                  | _ => OptionT.fail
              | _ => OptionT.fail)]
    fun size => aux_arb size size s_1
-/
#guard_msgs(info, drop warning) in
#derive_generator (fun (nb : Nat × List (String × String)) => KeyValueStore.GetBucket s nb)

/--
info: Try this generator: instance :
    ArbitrarySizedSuchThat (StateAPICall × StateResult × List (String × String))
      (fun foo_1 => KeyValueStore.EvalStateApiCall x_1 foo_1)
    where
  arbitrarySizedST :=
    let rec aux_arb (initSize : Nat) (size : Nat) (x_1 : List (String × String)) :
      OptionT Plausible.Gen (StateAPICall × StateResult × List (String × String)) :=
      match size with
      | Nat.zero =>
        OptionTGen.backtrack
          [(1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v)) =>
                  return
                    Prod.mk (KeyValueStore.StateAPICall.Get k (Option.none))
                      (Prod.mk (KeyValueStore.StateResult.Result v) x_1)
                | _ => OptionT.fail),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v)) =>
                  return
                    Prod.mk (KeyValueStore.StateAPICall.Get k (Option.none))
                      (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) x_1)
                | _ => OptionT.fail),
            (1, do
              let vk_n_v ←
                ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_n_v => KeyValueStore.LookupKV x_1 vk_n_v) initSize;
              match vk_n_v with
                | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk n v)) =>
                  return
                    Prod.mk (KeyValueStore.StateAPICall.Get k (Option.some n))
                      (Prod.mk (KeyValueStore.StateResult.Result v) x_1)
                | _ => OptionT.fail),
            (1, do
              let vk_n_v ←
                ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_n_v => KeyValueStore.LookupKV x_1 vk_n_v) initSize;
              match vk_n_v with
                | Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) (Prod.mk k (Prod.mk n v)) =>
                  return
                    Prod.mk (KeyValueStore.StateAPICall.Get k (Option.some n))
                      (Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) x_1)
                | _ => OptionT.fail),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v)) =>
                  return Prod.mk (KeyValueStore.StateAPICall.KeyExists k) (Prod.mk (KeyValueStore.StateResult.Ok) x_1)
                | _ => OptionT.fail),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v)) =>
                  return
                    Prod.mk (KeyValueStore.StateAPICall.KeyExists k)
                      (Prod.mk (KeyValueStore.StateResult.NoSuchKeyResult) x_1)
                | _ => OptionT.fail),
            (1, do
              let k ← Plausible.Arbitrary.arbitrary;
              do
                let s2 ← Plausible.Arbitrary.arbitrary;
                do
                  let v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun v => KeyValueStore.AddKV k v x_1 s2) initSize;
                  return Prod.mk (KeyValueStore.StateAPICall.Set k v) (Prod.mk (KeyValueStore.StateResult.Ok) s2)),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v)) => do
                  let k2 ← Plausible.Arbitrary.arbitrary;
                  do
                    let s2 ←
                      ArbitrarySizedSuchThat.arbitrarySizedST (fun s2 => KeyValueStore.AddKV k2 v x_1 s2) initSize;
                    return Prod.mk (KeyValueStore.StateAPICall.Copy k k2) (Prod.mk (KeyValueStore.StateResult.Ok) s2)
                | _ => OptionT.fail),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v)) => do
                  let k2 ← Plausible.Arbitrary.arbitrary;
                  return
                      Prod.mk (KeyValueStore.StateAPICall.Copy k k2)
                        (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) x_1)
                | _ => OptionT.fail),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v)) => do
                  let v2 ← Plausible.Arbitrary.arbitrary;
                  do
                    let v3 ← ArbitrarySizedSuchThat.arbitrarySizedST (fun v3 => Eq v3 (HAppend.hAppend v v2)) initSize;
                    do
                      let s2 ←
                        ArbitrarySizedSuchThat.arbitrarySizedST (fun s2 => KeyValueStore.AddKV k v3 x_1 s2) initSize;
                      return
                          Prod.mk (KeyValueStore.StateAPICall.Append k v3) (Prod.mk (KeyValueStore.StateResult.Ok) s2)
                | _ => OptionT.fail),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v)) => do
                  let v2 ← Plausible.Arbitrary.arbitrary;
                  return
                      Prod.mk (KeyValueStore.StateAPICall.Append k v2)
                        (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) x_1)
                | _ => OptionT.fail),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v)) => do
                  let s2 ← ArbitrarySizedSuchThat.arbitrarySizedST (fun s2 => KeyValueStore.RemoveKV k x_1 s2) initSize;
                  return Prod.mk (KeyValueStore.StateAPICall.Delete k) (Prod.mk (KeyValueStore.StateResult.Ok) s2)
                | _ => OptionT.fail),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v)) =>
                  return
                    Prod.mk (KeyValueStore.StateAPICall.Delete k)
                      (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) x_1)
                | _ => OptionT.fail)]
      | Nat.succ size' =>
        OptionTGen.backtrack
          [(1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v)) =>
                  return
                    Prod.mk (KeyValueStore.StateAPICall.Get k (Option.none))
                      (Prod.mk (KeyValueStore.StateResult.Result v) x_1)
                | _ => OptionT.fail),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v)) =>
                  return
                    Prod.mk (KeyValueStore.StateAPICall.Get k (Option.none))
                      (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) x_1)
                | _ => OptionT.fail),
            (1, do
              let vk_n_v ←
                ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_n_v => KeyValueStore.LookupKV x_1 vk_n_v) initSize;
              match vk_n_v with
                | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk n v)) =>
                  return
                    Prod.mk (KeyValueStore.StateAPICall.Get k (Option.some n))
                      (Prod.mk (KeyValueStore.StateResult.Result v) x_1)
                | _ => OptionT.fail),
            (1, do
              let vk_n_v ←
                ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_n_v => KeyValueStore.LookupKV x_1 vk_n_v) initSize;
              match vk_n_v with
                | Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) (Prod.mk k (Prod.mk n v)) =>
                  return
                    Prod.mk (KeyValueStore.StateAPICall.Get k (Option.some n))
                      (Prod.mk (KeyValueStore.StateResult.NoSuchVersionFailure) x_1)
                | _ => OptionT.fail),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v)) =>
                  return Prod.mk (KeyValueStore.StateAPICall.KeyExists k) (Prod.mk (KeyValueStore.StateResult.Ok) x_1)
                | _ => OptionT.fail),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v)) =>
                  return
                    Prod.mk (KeyValueStore.StateAPICall.KeyExists k)
                      (Prod.mk (KeyValueStore.StateResult.NoSuchKeyResult) x_1)
                | _ => OptionT.fail),
            (1, do
              let k ← Plausible.Arbitrary.arbitrary;
              do
                let s2 ← Plausible.Arbitrary.arbitrary;
                do
                  let v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun v => KeyValueStore.AddKV k v x_1 s2) initSize;
                  return Prod.mk (KeyValueStore.StateAPICall.Set k v) (Prod.mk (KeyValueStore.StateResult.Ok) s2)),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v)) => do
                  let k2 ← Plausible.Arbitrary.arbitrary;
                  do
                    let s2 ←
                      ArbitrarySizedSuchThat.arbitrarySizedST (fun s2 => KeyValueStore.AddKV k2 v x_1 s2) initSize;
                    return Prod.mk (KeyValueStore.StateAPICall.Copy k k2) (Prod.mk (KeyValueStore.StateResult.Ok) s2)
                | _ => OptionT.fail),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v)) => do
                  let k2 ← Plausible.Arbitrary.arbitrary;
                  return
                      Prod.mk (KeyValueStore.StateAPICall.Copy k k2)
                        (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) x_1)
                | _ => OptionT.fail),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v)) => do
                  let v2 ← Plausible.Arbitrary.arbitrary;
                  do
                    let v3 ← ArbitrarySizedSuchThat.arbitrarySizedST (fun v3 => Eq v3 (HAppend.hAppend v v2)) initSize;
                    do
                      let s2 ←
                        ArbitrarySizedSuchThat.arbitrarySizedST (fun s2 => KeyValueStore.AddKV k v3 x_1 s2) initSize;
                      return
                          Prod.mk (KeyValueStore.StateAPICall.Append k v3) (Prod.mk (KeyValueStore.StateResult.Ok) s2)
                | _ => OptionT.fail),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v)) => do
                  let v2 ← Plausible.Arbitrary.arbitrary;
                  return
                      Prod.mk (KeyValueStore.StateAPICall.Append k v2)
                        (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) x_1)
                | _ => OptionT.fail),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.Ok) (Prod.mk k (Prod.mk (Nat.zero) v)) => do
                  let s2 ← ArbitrarySizedSuchThat.arbitrarySizedST (fun s2 => KeyValueStore.RemoveKV k x_1 s2) initSize;
                  return Prod.mk (KeyValueStore.StateAPICall.Delete k) (Prod.mk (KeyValueStore.StateResult.Ok) s2)
                | _ => OptionT.fail),
            (1, do
              let vk_v ← ArbitrarySizedSuchThat.arbitrarySizedST (fun vk_v => KeyValueStore.LookupKV x_1 vk_v) initSize;
              match vk_v with
                | Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) (Prod.mk k (Prod.mk (Nat.zero) v)) =>
                  return
                    Prod.mk (KeyValueStore.StateAPICall.Delete k)
                      (Prod.mk (KeyValueStore.StateResult.NoSuchKeyFailure) x_1)
                | _ => OptionT.fail),
            ]
    fun size => aux_arb size size x_1
-/
#guard_msgs(info, drop warning) in
#derive_generator (fun (foo : StateAPICall × StateResult × List (String × String)) => KeyValueStore.EvalStateApiCall x foo)

/--
info: Try this generator: instance :
    ArbitrarySizedSuchThat (APICall × Result × (Nat × List (Nat × List (String × String))))
      (fun crns_1 => KeyValueStore.EvalApiCall s_1 crns_1)
    where
  arbitrarySizedST :=
    let rec aux_arb (initSize : Nat) (size : Nat) (s_1 : Nat × List (Nat × List (String × String))) :
      OptionT Plausible.Gen (APICall × Result × (Nat × List (Nat × List (String × String)))) :=
      match size with
      | Nat.zero =>
        OptionTGen.backtrack
          [(1,
              match s_1 with
              | Prod.mk n s => do
                let s' ←
                  ArbitrarySizedSuchThat.arbitrarySizedST (fun s' => Eq s' (KeyValueStore.addBucket n s)) initSize;
                return
                    Prod.mk (KeyValueStore.APICall.CreateBucket)
                      (Prod.mk (KeyValueStore.Result.Created n) (Prod.mk (Nat.succ n) s'))
              | _ => OptionT.fail),
            (1,
              match s_1 with
              | Prod.mk n s => do
                let vn'_x ←
                  ArbitrarySizedSuchThat.arbitrarySizedST (fun vn'_x => KeyValueStore.GetBucket s vn'_x) initSize;
                match vn'_x with
                  | Prod.mk n' x => do
                    let vc_r_x' ←
                      ArbitrarySizedSuchThat.arbitrarySizedST (fun vc_r_x' => KeyValueStore.EvalStateApiCall x vc_r_x')
                          initSize;
                    match vc_r_x' with
                      | Prod.mk c (Prod.mk r x') => do
                        let vs' ←
                          ArbitrarySizedSuchThat.arbitrarySizedST
                              (fun vs' => Eq vs' (KeyValueStore.updateBucket n' s x')) initSize;
                        match vs' with
                          | Option.some s' =>
                            return
                              Prod.mk (KeyValueStore.APICall.OpBucket n' c)
                                (Prod.mk (KeyValueStore.Result.OpResult r) (Prod.mk n s'))
                          | _ => OptionT.fail
                      | _ => OptionT.fail
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match s_1 with
              | Prod.mk n s => do
                let vn'_x ←
                  ArbitrarySizedSuchThat.arbitrarySizedST (fun vn'_x => KeyValueStore.GetBucket s vn'_x) initSize;
                match vn'_x with
                  | Prod.mk n' x => do
                    let vs' ←
                      ArbitrarySizedSuchThat.arbitrarySizedST (fun vs' => Eq vs' (KeyValueStore.removeBucket n' s))
                          initSize;
                    match vs' with
                      | Option.some s' =>
                        return
                          Prod.mk (KeyValueStore.APICall.DeleteBucket n')
                            (Prod.mk (KeyValueStore.Result.Removed) (Prod.mk n s'))
                      | _ => OptionT.fail
                  | _ => OptionT.fail
              | _ => OptionT.fail)]
      | Nat.succ size' =>
        OptionTGen.backtrack
          [(1,
              match s_1 with
              | Prod.mk n s => do
                let s' ←
                  ArbitrarySizedSuchThat.arbitrarySizedST (fun s' => Eq s' (KeyValueStore.addBucket n s)) initSize;
                return
                    Prod.mk (KeyValueStore.APICall.CreateBucket)
                      (Prod.mk (KeyValueStore.Result.Created n) (Prod.mk (Nat.succ n) s'))
              | _ => OptionT.fail),
            (1,
              match s_1 with
              | Prod.mk n s => do
                let vn'_x ←
                  ArbitrarySizedSuchThat.arbitrarySizedST (fun vn'_x => KeyValueStore.GetBucket s vn'_x) initSize;
                match vn'_x with
                  | Prod.mk n' x => do
                    let vc_r_x' ←
                      ArbitrarySizedSuchThat.arbitrarySizedST (fun vc_r_x' => KeyValueStore.EvalStateApiCall x vc_r_x')
                          initSize;
                    match vc_r_x' with
                      | Prod.mk c (Prod.mk r x') => do
                        let vs' ←
                          ArbitrarySizedSuchThat.arbitrarySizedST
                              (fun vs' => Eq vs' (KeyValueStore.updateBucket n' s x')) initSize;
                        match vs' with
                          | Option.some s' =>
                            return
                              Prod.mk (KeyValueStore.APICall.OpBucket n' c)
                                (Prod.mk (KeyValueStore.Result.OpResult r) (Prod.mk n s'))
                          | _ => OptionT.fail
                      | _ => OptionT.fail
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            (1,
              match s_1 with
              | Prod.mk n s => do
                let vn'_x ←
                  ArbitrarySizedSuchThat.arbitrarySizedST (fun vn'_x => KeyValueStore.GetBucket s vn'_x) initSize;
                match vn'_x with
                  | Prod.mk n' x => do
                    let vs' ←
                      ArbitrarySizedSuchThat.arbitrarySizedST (fun vs' => Eq vs' (KeyValueStore.removeBucket n' s))
                          initSize;
                    match vs' with
                      | Option.some s' =>
                        return
                          Prod.mk (KeyValueStore.APICall.DeleteBucket n')
                            (Prod.mk (KeyValueStore.Result.Removed) (Prod.mk n s'))
                      | _ => OptionT.fail
                  | _ => OptionT.fail
              | _ => OptionT.fail),
            ]
    fun size => aux_arb size size s_1
-/
#guard_msgs(info, drop warning) in
#derive_generator (fun (crns : APICall × Result × (Nat × List (Nat × List (String × String)))) => KeyValueStore.EvalApiCall s crns)

/--
info: Try this generator: instance :
    ArbitrarySizedSuchThat (List (APICall × Result) × (Nat × List (Nat × List (String × String))))
      (fun o_1 => KeyValueStore.EvalApiCalls s_1 o_1)
    where
  arbitrarySizedST :=
    let rec aux_arb (initSize : Nat) (size : Nat) (s_1 : Nat × List (Nat × List (String × String))) :
      OptionT Plausible.Gen (List (APICall × Result) × (Nat × List (Nat × List (String × String)))) :=
      match size with
      | Nat.zero => OptionTGen.backtrack [(1, return Prod.mk (List.nil) s_1)]
      | Nat.succ size' =>
        OptionTGen.backtrack
          [(1, return Prod.mk (List.nil) s_1),
            (Nat.succ size', do
              let vc_r_s2 ←
                ArbitrarySizedSuchThat.arbitrarySizedST (fun vc_r_s2 => KeyValueStore.EvalApiCall s_1 vc_r_s2) initSize;
              match vc_r_s2 with
                | Prod.mk c (Prod.mk r s2) => do
                  let vcrs_s3 ← aux_arb initSize size' s2;
                  match vcrs_s3 with
                    | Prod.mk crs s3 => return Prod.mk (List.cons (Prod.mk c r) crs) s3
                    | _ => OptionT.fail
                | _ => OptionT.fail)]
    fun size => aux_arb size size s_1
-/
#guard_msgs(info, drop warning) in
#derive_generator (fun (o : List (APICall × Result) × (Nat × List (Nat × List (String × String)))) => KeyValueStore.EvalApiCalls s o)


/- Uncommenting the following line results in random sequences of API Calls, such as:

```lean
 ([(APICall.CreateBucket, Result.Created 0),
  (APICall.OpBucket 0 (StateAPICall.Delete "B"),
   Result.OpResult (StateResult.NoSuchKeyFailure)),
  (APICall.CreateBucket, Result.Created 1),
  (APICall.DeleteBucket 0, Result.Removed),
  (APICall.CreateBucket, Result.Created 2),
  (APICall.CreateBucket, Result.Created 3),
  (APICall.DeleteBucket 1, Result.Removed),
  (APICall.CreateBucket, Result.Created 4),
  (APICall.DeleteBucket 2, Result.Removed),
  (APICall.OpBucket 3 (StateAPICall.Get "E" none),
   Result.OpResult (StateResult.NoSuchKeyFailure)),
  (APICall.CreateBucket, Result.Created 5),
  (APICall.OpBucket 3 (StateAPICall.Append "B" "D"),
   Result.OpResult (StateResult.NoSuchKeyFailure)),
  (APICall.DeleteBucket 3, Result.Removed),
  (APICall.CreateBucket, Result.Created 6)],
 7,
 [(6, []), (5, []), (4, [])])
```

-/
-- #eval OptionTGen.runSizedGen (ArbitrarySizedSuchThat.arbitrarySizedST (fun crs => KeyValueStore.EvalApiCalls (0, []) crs)) 20