diff options
Diffstat (limited to 'Test/server/simple-session.transcript')
| -rw-r--r-- | Test/server/simple-session.transcript | 637 |
1 files changed, 637 insertions, 0 deletions
diff --git a/Test/server/simple-session.transcript b/Test/server/simple-session.transcript new file mode 100644 index 00000000..d095f6dd --- /dev/null +++ b/Test/server/simple-session.transcript @@ -0,0 +1,637 @@ +# RUN: "%server" "%s" > "%t"
+# RUN: %diff "%s.expect" "%t"
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG4gfVxuIiwi
+c291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG4iLCJzb3VyY2VJc0ZpbGUiOmZh
+bHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7Iiwic291
+cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gICIs
+InNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG59Iiwi
+c291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG5cbn0i
+LCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIFxu
+fSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHhc
+bn0iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIFxu
+fSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh
+clxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh
+ciB4IDo9IDE7XG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh
+ciB4IDo9IDE7XG4gIFxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh
+ciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDI7XG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh
+ciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDI7XG4gIFxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh
+ciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIFxufSIsInNvdXJjZUlzRmlsZSI6ZmFs
+c2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKCkg
+e1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBcbn0iLCJzb3VyY2VJc0Zp
+bGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKCkg
+e1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBcbn0iLCJzb3VyY2VJc0Zp
+bGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcblxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBcbn0iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcblxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBcbn0iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgXG57XG4gIHZhciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIFxufSIs
+InNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxXG57XG4gIHZhciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIFxu
+fSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxXG57XG4gIHZhciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIFxu
+fSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgXG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzXG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvclxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JyA6OiBcbn0iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JyA6OiBpbnQsIHgnICogeCcgPiAwO1xufSIsInNvdXJj
+ZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JyA6OiBpbnQsIHgnICogeCcgPiAwO1xufSIsInNvdXJj
+ZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4J2ludCwgeCcgKiB4JyA+IDA7XG59Iiwic291cmNlSXNG
+aWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50LCB4JyAqIHgnID4gMDtcbn0iLCJzb3VyY2VJ
+c0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6ICwgeCcgKiB4JyA+IDA7XG59Iiwic291
+cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPiAwO1xufSIsInNvdXJj
+ZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbn0iLCJzb3Vy
+Y2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgXG59Iiwi
+c291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzXG59
+Iiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn0iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn0iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn0iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cbiIs
+InNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNJyh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNJyh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNJyh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG4iLCJzb3VyY2VJc0ZpbGUiOmZhbHNl
+fQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNJyh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTScodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQg
+eCAqIHggPiAwO1xufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0odDogbmF0KVxuICByZXF1aXJlcyB0
+ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBhc3NlcnQgZm9y
+YWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQgeCAqIHggPiAwO1xufVxuXG5z
+dGF0aWMgbWV0aG9kIE0odDogbmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAx
+O1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4
+JyA+PSAwO1xuICBhc3NlcnQgeCAqIHggPiAwO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0odDogbmF0
+KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAz
+O1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQgeCAq
+IHggPiAwO1xufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQg
+eCAqIHggPiAwO1xufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQg
+eCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnID49IDA7XG4gIGFzc2Vy
+dCB4ICogeCA+IDA7XG59XG4iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnICAwO1xuICBhc3NlcnQg
+eCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDwgMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc2Vy
+dCB4ICogeCA+IDA7XG59XG4iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIFxuICBh
+c3NlcnQgeCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc1xu
+ICBhc3NlcnQgeCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc2Vy
+XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG4iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc1xu
+ICBhc3NlcnQgeCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt
+ZSB5IDwgMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt
+ZSB5IDwgMDtcbiAgYXNzZXJ0IDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt
+ZSB5IDwgMDtcbiAgYXNzZXJ0IDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt
+ZSB5IDwgMDtcbiAgYXNzZXJ0IGZhbDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt
+ZSB5IDwgMDtcbiAgYXNzZXJ0IGZhbHNlO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
+verify
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6
+IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g
+MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0
+IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg
+dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv
+cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu
+c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9
+IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq
+IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog
+bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy
+LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt
+ZSB5IDwgMDtcbiAgYXNzZXJ0IGZhbHNlO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0=
+[[DAFNY-CLIENT: EOM]]
|