{ parameter (or (unit %snapshot)

                (or (pair %insert (bytes %key) (bytes %value))

                    (list %configure (or (address %update_administrator)

                                        (or (nat %update_max_state_size)

                                            (nat %update_snapshot_duration)))))) ;

  storage (pair

            (pair %config (address %administrator)

                          (pair (nat %max_state_size) (nat %snapshot_duration)))

            (pair

              (pair %merkle_tree

                (map %nodes bytes

                            (map int

                                 (pair (pair %label (nat %data) (nat %length))

                                       (bytes %node))))

                (pair (bytes %root)

                      (pair

                        (pair %root_edge (pair %label (nat %data) (nat %length))

                                         (bytes %node))

                        (map %states bytes bytes))))

              (pair (nat %snapshot_counter)

                    (pair (big_map %snapshot_level nat nat) (nat %snapshot_start_level))))) ;

  code { LAMBDA

           (pair bool

                 (pair (list operation)

                       (pair (pair address (pair nat nat))

                             (pair

                               (pair (map bytes (map int (pair (pair nat nat) bytes)))

                                     (pair bytes

                                           (pair (pair (pair nat nat) bytes)

                                                 (map bytes bytes))))

                               (pair nat (pair (big_map nat nat) nat))))))

           (pair unit

                 (pair (list operation)

                       (pair (pair address (pair nat nat))

                             (pair

                               (pair (map bytes (map int (pair (pair nat nat) bytes)))

                                     (pair bytes

                                           (pair (pair (pair nat nat) bytes)

                                                 (map bytes bytes))))

                               (pair nat (pair (big_map nat nat) nat))))))

           { UNPAIR 3 ;

             SWAP ;

             PUSH nat 0 ;

             DUP 4 ;

             GET 8 ;

             COMPARE ;

             EQ ;

             IF

               { DIG 2 ;

                 LEVEL ;

                 UPDATE 8 ;

                 EMPTY_MAP bytes bytes ;

                 PUSH (pair (pair nat nat) bytes) (Pair (Pair 0 0) 0x) ;

                 PUSH bytes 0x ;

                 EMPTY_MAP bytes (map int (pair (pair nat nat) bytes)) ;

                 PAIR 4 ;

                 UPDATE 3 ;

                 DUG 2 }

               {} ;

             LEVEL ;

             DIG 3 ;

             DUP ;

             CAR ;

             GET 4 ;

             SWAP ;

             DUP ;

             DUG 5 ;

             GET 8 ;

             ADD ;

             COMPARE ;

             LT ;

             IF

               { DIG 2 ;

                 DUP ;

                 GET 5 ;

                 PUSH nat 1 ;

                 ADD ;

                 UPDATE 5 ;

                 DUG 2 ;

                 PUSH nat 1 ;

                 LEVEL ;

                 SUB ;

                 ISNAT ;

                 IF_NONE { PUSH int 324 ; FAILWITH } {} ;

                 DUP 4 ;

                 DUP ;

                 GET 7 ;

                 DUP 3 ;

                 SOME ;

                 DIG 6 ;

                 GET 5 ;

                 UPDATE ;

                 UPDATE 7 ;

                 LEVEL ;

                 UPDATE 8 ;

                 EMPTY_MAP bytes bytes ;

                 PUSH (pair (pair nat nat) bytes) (Pair (Pair 0 0) 0x) ;

                 PUSH bytes 0x ;

                 EMPTY_MAP bytes (map int (pair (pair nat nat) bytes)) ;

                 PAIR 4 ;

                 DIG 4 ;

                 DROP ;

                 UPDATE 3 ;

                 DUG 2 ;

                 SWAP ;

                 DUP 3 ;

                 GET 5 ;

                 DIG 2 ;

                 PAIR ;

                 EMIT %SNAPSHOT_FINALIZED (pair (nat %level) (nat %snapshot)) ;

                 CONS }

               { SWAP ; IF { PUSH string "CANNOT_SNAPSHOT" ; FAILWITH } {} } ;

             UNIT ;

             PAIR 3 } ;

         SWAP ;

         LAMBDA_REC

           (pair (pair (pair (pair nat nat) bytes) (pair nat nat))

                 (pair

                   (pair (map bytes (map int (pair (pair nat nat) bytes)))

                         (pair bytes

                               (pair (pair (pair nat nat) bytes) (map bytes bytes))))

                   bytes))

           (pair

             (pair (map bytes (map int (pair (pair nat nat) bytes)))

                   (pair bytes (pair (pair (pair nat nat) bytes) (map bytes bytes))))

             (pair (pair nat nat) bytes))

           { DUP ;

             UNPAIR ;

             UNPAIR ;

             DIG 2 ;

             UNPAIR ;

             DUP ;

             LAMBDA

               (pair nat nat)

               (pair int (pair nat nat))

               { DUP ;

                 CDR ;

                 PUSH nat 0 ;

                 COMPARE ;

                 LT ;

                 IF {} { PUSH string "EMPTY_KEY" ; FAILWITH } ;

                 DUP ;

                 CDR ;

                 PUSH nat 1 ;

                 SWAP ;

                 SUB ;

                 ISNAT ;

                 IF_NONE { PUSH int 0 ; FAILWITH } {} ;

                 PUSH nat 1 ;

                 DUP ;

                 DUP 4 ;

                 CDR ;

                 SUB ;

                 ISNAT ;

                 IF_NONE { PUSH int 0 ; FAILWITH } {} ;

                 PUSH nat 1 ;

                 LSL ;

                 SUB ;

                 ISNAT ;

                 IF_NONE { PUSH int 21 ; FAILWITH } {} ;

                 DUP 3 ;

                 CAR ;

                 AND ;

                 PAIR ;

                 PUSH nat 1 ;

                 DUP 3 ;

                 CDR ;

                 SUB ;

                 ISNAT ;

                 IF_NONE { PUSH int 0 ; FAILWITH } {} ;

                 DIG 2 ;

                 CAR ;

                 LSR ;

                 INT ;

                 PAIR } ;

             LAMBDA

               (pair (pair nat nat) nat)

               (pair nat nat)

               { UNPAIR ;

                 DUP ;

                 DUG 2 ;

                 CDR ;

                 SUB ;

                 ISNAT ;

                 IF_NONE { PUSH string "PREFIX_TOO_LONG" ; FAILWITH } {} ;

                 DUP ;

                 PUSH nat 0 ;

                 COMPARE ;

                 EQ ;

                 IF

                   { DROP 2 ; PUSH (pair nat nat) (Pair 0 0) }

                   { DUP ;

                     PUSH nat 1 ;

                     DIG 2 ;

                     PUSH nat 1 ;

                     LSL ;

                     SUB ;

                     ISNAT ;

                     IF_NONE { PUSH int 21 ; FAILWITH } {} ;

                     DIG 2 ;

                     CAR ;

                     AND ;

                     PAIR } } ;

             LAMBDA

               (pair (pair nat nat) (pair nat nat))

               (pair (pair nat nat) (pair nat nat))

               { DUP ;

                 UNPAIR ;

                 SWAP ;

                 DUP ;

                 DUG 2 ;

                 CDR ;

                 SWAP ;

                 DUP ;

                 DUG 2 ;

                 CDR ;

                 COMPARE ;

                 LT ;

                 IF { DUP ; CDR } { SWAP ; DUP ; DUG 2 ; CDR } ;

                 PUSH nat 0 ;

                 PUSH bool False ;

                 DUP 3 ;

                 DUP 3 ;

                 COMPARE ;

                 LT ;

                 LOOP { PUSH nat 1 ;

                        DUP 3 ;

                        ADD ;

                        DUP 6 ;

                        CDR ;

                        SUB ;

                        ISNAT ;

                        IF_NONE { PUSH int 25 ; FAILWITH } {} ;

                        DUP 6 ;

                        CAR ;

                        LSR ;

                        PUSH nat 1 ;

                        DUP 4 ;

                        ADD ;

                        DUP 6 ;

                        CDR ;

                        SUB ;

                        ISNAT ;

                        IF_NONE { PUSH int 25 ; FAILWITH } {} ;

                        DUP 6 ;

                        CAR ;

                        LSR ;

                        COMPARE ;

                        EQ ;

                        IF

                          { PUSH nat 1 ; DIG 2 ; ADD ; SWAP }

                          { DROP ; PUSH bool True } ;

                        DUP ;

                        IF { PUSH bool False } { DUP 3 ; DUP 3 ; COMPARE ; LT } } ;

                 DROP ;

                 SWAP ;

                 DROP ;

                 DIG 2 ;

                 DROP ;

                 DIG 2 ;

                 DROP ;

                 SWAP ;

                 DUP ;

                 CDR ;

                 DUP 3 ;

                 COMPARE ;

                 LE ;

                 IF { PUSH nat 256 ; DUP 3 ; COMPARE ; LE } { PUSH bool False } ;

                 IF {} { PUSH string "BAD_POS" ; FAILWITH } ;

                 SWAP ;

                 DUP ;

                 DUG 2 ;

                 PUSH nat 0 ;

                 PAIR ;

                 PUSH nat 0 ;

                 DUP 4 ;

                 COMPARE ;

                 NEQ ;

                 IF

                   { DUP 3 ;

                     DUP 3 ;

                     CDR ;

                     SUB ;

                     ISNAT ;

                     IF_NONE { PUSH int 25 ; FAILWITH } {} ;

                     DUP 3 ;

                     CAR ;

                     LSR ;

                     UPDATE 1 }

                   {} ;

                 DUP 3 ;

                 DUP 3 ;

                 CDR ;

                 SUB ;

                 ISNAT ;

                 IF_NONE { PUSH int 0 ; FAILWITH } {} ;

                 PUSH nat 1 ;

                 DIG 4 ;

                 DUP 5 ;

                 CDR ;

                 SUB ;

                 ISNAT ;

                 IF_NONE { PUSH int 0 ; FAILWITH } {} ;

                 PUSH nat 1 ;

                 LSL ;

                 SUB ;

                 ISNAT ;

                 IF_NONE { PUSH int 21 ; FAILWITH } {} ;

                 DIG 3 ;

                 CAR ;

                 AND ;

                 PAIR ;

                 SWAP ;

                 PAIR } ;

             DUP 7 ;

             CAR ;

             CDR ;

             DUP 9 ;

             CDR ;

             COMPARE ;

             GE ;

             IF {} { PUSH string "KEY_LENGTH_MISMATCH" ; FAILWITH } ;

             DUP ;

             DUP 8 ;

             CAR ;

             DUP 10 ;

             PAIR ;

             EXEC ;

             UNPAIR ;

             PUSH nat 0 ;

             DUP 3 ;

             CDR ;

             COMPARE ;

             EQ ;

             IF

               { SWAP ;

                 DROP ;

                 SWAP ;

                 DROP ;

                 SWAP ;

                 DROP ;

                 SWAP ;

                 DROP ;

                 DIG 2 ;

                 DROP ;

                 DIG 3 ;

                 DROP ;

                 DIG 3 ;

                 DROP ;

                 DIG 3 ;

                 DROP ;

                 DIG 3 ;

                 DROP ;

                 DUG 2 ;

                 PAIR }

               { DUP 5 ;

                 DUP 3 ;

                 EXEC ;

                 UNPAIR ;

                 DUP 11 ;

                 CAR ;

                 CDR ;

                 DUP 4 ;

                 CDR ;

                 COMPARE ;

                 GE ;

                 IF

                   { DIG 4 ;

                     DROP ;

                     DIG 4 ;

                     DROP ;

                     DIG 4 ;

                     DROP ;

                     DIG 5 ;

                     DROP ;

                     DIG 7 ;

                     DROP ;

                     DIG 7 ;

                     DROP ;

                     PUSH nat 1 ;

                     DIG 4 ;

                     CDR ;

                     COMPARE ;

                     GT ;

                     IF {} { PUSH string "BAD_KEY" ; FAILWITH } ;

                     DUP 4 ;

                     CAR ;

                     DUP 7 ;

                     CDR ;

                     GET ;

                     IF_NONE { PUSH int 398 ; FAILWITH } {} ;

                     DIG 7 ;

                     DIG 6 ;

                     DIG 6 ;

                     PAIR ;

                     DIG 4 ;

                     DUP 4 ;

                     DUP 6 ;

                     GET ;

                     IF_NONE { PUSH int 402 ; FAILWITH } {} ;

                     PAIR ;

                     PAIR ;

                     EXEC ;

                     UNPAIR ;

                     DUG 4 ;

                     SOME ;

                     DIG 2 ;

                     UPDATE ;

                     DIG 2 ;

                     DUP ;

                     CAR ;

                     NONE (map int (pair (pair nat nat) bytes)) ;

                     DIG 5 ;

                     CDR ;

                     UPDATE ;

                     UPDATE 1 ;

                     DUG 2 ;

                     DUP ;

                     PUSH int 1 ;

                     GET ;

                     IF_NONE { PUSH int 53 ; FAILWITH } {} ;

                     CDR ;

                     SWAP ;

                     DUP ;

                     DUG 2 ;

                     PUSH int 0 ;

                     GET ;

                     IF_NONE { PUSH int 52 ; FAILWITH } {} ;

                     CDR ;

                     CONCAT ;

                     KECCAK ;

                     DIG 3 ;

                     DUP ;

                     CAR ;

                     DIG 3 ;

                     SOME ;

                     DUP 4 ;

                     UPDATE ;

                     UPDATE 1 ;

                     PAIR }

                   { DIG 3 ;

                     DROP ;

                     DIG 3 ;

                     DROP ;

                     DIG 4 ;

                     DROP ;

                     DIG 5 ;

                     DROP ;

                     DIG 7 ;

                     DROP ;

                     DIG 7 ;

                     DROP ;

                     DIG 7 ;

                     DROP ;

                     EMPTY_MAP int (pair (pair nat nat) bytes) ;

                     DIG 6 ;

                     DIG 3 ;

                     PAIR ;

                     SOME ;

                     DUP 3 ;

                     UPDATE ;

                     DUP 6 ;

                     CDR ;

                     DIG 4 ;

                     PUSH nat 1 ;

                     DUP 6 ;

                     CDR ;

                     ADD ;

                     DIG 7 ;

                     CAR ;

                     PAIR ;

                     EXEC ;

                     PAIR ;

                     SOME ;

                     DIG 2 ;

                     PUSH int 1 ;

                     SUB ;

                     UPDATE ;

                     DUP ;

                     PUSH int 1 ;

                     GET ;

                     IF_NONE { PUSH int 53 ; FAILWITH } {} ;

                     CDR ;

                     SWAP ;

                     DUP ;

                     DUG 2 ;

                     PUSH int 0 ;

                     GET ;

                     IF_NONE { PUSH int 52 ; FAILWITH } {} ;

                     CDR ;

                     CONCAT ;

                     KECCAK ;

                     DIG 3 ;

                     DUP ;

                     CAR ;

                     DIG 3 ;

                     SOME ;

                     DUP 4 ;

                     UPDATE ;

                     UPDATE 1 ;

                     PAIR } } ;

             UNPAIR ;

             SWAP ;

             DIG 2 ;

             PAIR ;

             SWAP ;

             PAIR } ;

         SWAP ;

         UNPAIR ;

         IF_LEFT

           { DROP ; SWAP ; DROP ; NIL operation ; DIG 2 ; PUSH bool True ; SWAP ; DUG 3 ; PAIR 3 ; EXEC ; CDR ; UNPAIR }

           { IF_LEFT

               { LAMBDA

                   bytes

                   nat

                   { DUP ;

                     SIZE ;

                     DUP ;

                     PUSH nat 0 ;

                     SWAP ;

                     PUSH nat 0 ;

                     DUP ;

                     DUP 3 ;

                     COMPARE ;

                     GT ;

                     LOOP { DUP 5 ;

                            PUSH nat 1 ;

                            DUP 3 ;

                            SLICE ;

                            IF_NONE { PUSH int 126 ; FAILWITH } {} ;

                            PUSH nat 2 ;

                            PUSH nat 1 ;

                            DUP 4 ;

                            ADD ;

                            DUP 7 ;

                            SUB ;

                            ISNAT ;

                            IF_NONE { PUSH int 127 ; FAILWITH } {} ;

                            MUL ;

                            PUSH nat 1 ;

                            PUSH nat 16 ;

                            DUP 3 ;

                            DUP ;

                            PUSH nat 0 ;

                            COMPARE ;

                            NEQ ;

                            LOOP { PUSH nat 0 ;

                                   PUSH nat 2 ;

                                   DUP 3 ;

                                   EDIV ;

                                   IF_NONE { PUSH int 28 ; FAILWITH } { CDR } ;

                                   COMPARE ;

                                   NEQ ;

                                   IF { SWAP ; DUP ; DUG 2 ; DIG 3 ; MUL ; DUG 2 } {} ;

                                   PUSH nat 1 ;

                                   SWAP ;

                                   LSR ;

                                   SWAP ;

                                   DUP ;

                                   MUL ;

                                   SWAP ;

                                   DUP ;

                                   PUSH nat 0 ;

                                   COMPARE ;

                                   NEQ } ;

                            DROP 2 ;

                            SWAP ;

                            DROP ;

                            PUSH bytes 0x00000000000000000000000000000000000000000000000000000000000000 ;

                            DIG 2 ;

                            PUSH bytes 0x050a00000020 ;

                            CONCAT ;

                            CONCAT ;

                            UNPACK bls12_381_fr ;

                            IF_NONE { PUSH int 134 ; FAILWITH } {} ;

                            INT ;

                            ISNAT ;

                            IF_NONE { PUSH int 133 ; FAILWITH } {} ;

                            MUL ;

                            DIG 3 ;

                            ADD ;

                            DUG 2 ;

                            PUSH nat 1 ;

                            ADD ;

                            DUP ;

                            DUP 3 ;

                            COMPARE ;

                            GT } ;

                     DROP 2 ;

                     SWAP ;

                     DROP ;

                     SWAP ;

                     DROP } ;

                 NIL operation ;

                 DUP 6 ;

                 PUSH bool False ;

                 SWAP ;

                 DIG 5 ;

                 DIG 3 ;

                 DIG 3 ;

                 PAIR 3 ;

                 EXEC ;

                 CDR ;

                 UNPAIR ;

                 DIG 5 ;

                 DIG 5 ;

                 DIG 3 ;

                 DIG 5 ;

                 DIG 5 ;

                 DIG 5 ;

                 DUP 4 ;

                 CAR ;

                 GET 3 ;

                 DUP 4 ;

                 CDR ;

                 SIZE ;

                 COMPARE ;

                 LE ;

                 IF {} { PUSH string "STATE_TOO_LARGE" ; FAILWITH } ;

                 DUP 3 ;

                 CAR ;

                 SENDER ;

                 PACK ;

                 CONCAT ;

                 KECCAK ;

                 PUSH nat 256 ;

                 DIG 3 ;

                 DIG 2 ;

                 EXEC ;

                 PAIR ;

                 NIL bytes ;

                 DUP 4 ;

                 CDR ;

                 CONS ;

                 DUP 4 ;

                 CAR ;

                 CONS ;

                 SENDER ;

                 PACK ;

                 CONS ;

                 CONCAT ;

                 KECCAK ;

                 DIG 4 ;

                 DUP ;

                 GET 3 ;

                 DUP ;

                 GET 6 ;

                 DIG 6 ;

                 CDR ;

                 SOME ;

                 DUP 5 ;

                 UPDATE ;

                 UPDATE 6 ;

                 UPDATE 3 ;

                 DUG 3 ;

                 PUSH bytes 0x ;

                 DUP 5 ;

                 GET 3 ;

                 GET 3 ;

                 COMPARE ;

                 EQ ;

                 IF

                   { DIG 4 ;

                     DROP ;

                     DIG 4 ;

                     DROP ;

                     SWAP ;

                     PAIR ;

                     DIG 2 ;

                     DUP ;

                     GET 3 ;

                     DUP 3 ;

                     CDR ;

                     UPDATE 3 ;

                     UPDATE 3 ;

                     DUP ;

                     GET 3 ;

                     DIG 2 ;

                     UPDATE 5 ;

                     UPDATE 3 ;

                     SWAP }

                   { DIG 5 ;

                     DROP ;

                     DIG 4 ;

                     SWAP ;

                     DUP 5 ;

                     GET 3 ;

                     PAIR ;

                     DIG 2 ;

                     DUP 5 ;

                     GET 3 ;

                     GET 5 ;

                     PAIR ;

                     PAIR ;

                     EXEC ;

                     UNPAIR ;

                     DIG 3 ;

                     SWAP ;

                     UPDATE 3 ;

                     DUP ;

                     GET 3 ;

                     DUP 3 ;

                     CDR ;

                     UPDATE 3 ;

                     UPDATE 3 ;

                     DUP ;

                     GET 3 ;

                     DIG 2 ;

                     UPDATE 5 ;

                     UPDATE 3 ;

                     SWAP } }

               { SENDER ;

                 DUP 3 ;

                 CAR ;

                 CAR ;

                 COMPARE ;

                 EQ ;

                 IF {} { PUSH string "NOT_ADMINISTRATOR" ; FAILWITH } ;

                 DUP ;

                 ITER { IF_LEFT

                          { DIG 2 ; DUP ; CAR ; DIG 2 ; UPDATE 1 ; UPDATE 1 ; SWAP }

                          { IF_LEFT

                              { DIG 2 ; DUP ; CAR ; DIG 2 ; UPDATE 3 ; UPDATE 1 ; SWAP }

                              { DIG 2 ; DUP ; CAR ; DIG 2 ; UPDATE 4 ; UPDATE 1 ; SWAP } } } ;

                 DROP ;

                 SWAP ;

                 DROP ;

                 SWAP ;

                 DROP ;

                 NIL operation } } ;

         NIL operation ;

         SWAP ;

         ITER { CONS } ;

         PAIR } ;

  view "get_proof" (pair (bytes %key) (address %owner))

        (pair (bytes %key)

              (pair (bytes %merkle_root)

                    (pair (list %path (or (bytes %Left) (bytes %Right)))

                          (pair (nat %snapshot) (bytes %value)))))

        { UNPAIR ;

          LAMBDA

            (pair nat nat)

            (pair int (pair nat nat))

            { DUP ;

              CDR ;

              PUSH nat 0 ;

              COMPARE ;

              LT ;

              IF {} { PUSH string "EMPTY_KEY" ; FAILWITH } ;

              DUP ;

              CDR ;

              PUSH nat 1 ;

              SWAP ;

              SUB ;

              ISNAT ;

              IF_NONE { PUSH int 0 ; FAILWITH } {} ;

              PUSH nat 1 ;

              DUP ;

              DUP 4 ;

              CDR ;

              SUB ;

              ISNAT ;

              IF_NONE { PUSH int 0 ; FAILWITH } {} ;

              PUSH nat 1 ;

              LSL ;

              SUB ;

              ISNAT ;

              IF_NONE { PUSH int 21 ; FAILWITH } {} ;

              DUP 3 ;

              CAR ;

              AND ;

              PAIR ;

              PUSH nat 1 ;

              DUP 3 ;

              CDR ;

              SUB ;

              ISNAT ;