clean up

dafny-lang · Jul 12, 2023 · 47e38d6 · 47e38d6
1 parent fead347
commit 47e38d6
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 5 deletions.
diff --git a/src/JSON/Utils/Cursors.dfy b/src/JSON/Utils/Cursors.dfy
@@ -305,7 +305,7 @@ module {:options "-functionSyntax:4"} JSON.Utils.Cursors {
       : (pr: CursorResult<R>)
       requires Valid?
       decreases SuffixLength()
-      ensures pr.Success? ==> (pr.value.AdvancedFrom?(this))
+      ensures pr.Success? ==> pr.value.AdvancedFrom?(this)
     {
       match step(st, Peek())
       case Accept => Success(this)

diff --git a/src/JSON/ZeroCopy/Deserializer.dfy b/src/JSON/ZeroCopy/Deserializer.dfy
@@ -39,9 +39,7 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Deserializer {
 
     function {:opaque} WS(cs: FreshCursor): (sp: Split<jblanks>)
       ensures sp.SplitFrom?(cs, SpecView)
-      ensures sp.cs.beg >= cs.beg
-      ensures sp.cs.end == cs.end
-      ensures sp.cs.s == cs.s
+      ensures sp.cs.SuffixOf?(cs)
     {
       cs.SkipWhile(Blank?).Split()
     } by method {
@@ -426,7 +424,7 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Deserializer {
 
     import ConcreteSyntax.SpecProperties
 
-    function {:rlimit 1000} {:vcs_split_on_every_assert} {:opaque} Value(cs: FreshCursor) : (pr: ParseResult<Value>)
+    function {:opaque} Value(cs: FreshCursor) : (pr: ParseResult<Value>)
       decreases cs.Length(), 1
       ensures pr.Success? ==> pr.value.StrictlySplitFrom?(cs, Spec.Value)
     {