From ee4aeaf3b0fda61f5ac0da6d38610dcb74d78050 Mon Sep 17 00:00:00 2001
From: Stefan Zetzsche <120379523+stefan-aws@users.noreply.github.com>
Date: Wed, 19 Jul 2023 17:54:37 +0200
Subject: [PATCH] Json fix for nightly (#134)

* deserializer

* serializer
---
 src/JSON/Utils/Str.dfy             |  2 +-
 src/JSON/ZeroCopy/Deserializer.dfy | 27 ++++++++++++++++++++++++---
 src/JSON/ZeroCopy/Serializer.dfy   |  2 +-
 3 files changed, 26 insertions(+), 5 deletions(-)

diff --git a/src/JSON/Utils/Str.dfy b/src/JSON/Utils/Str.dfy
index 9f099419..00cbed19 100644
--- a/src/JSON/Utils/Str.dfy
+++ b/src/JSON/Utils/Str.dfy
@@ -87,7 +87,7 @@ module {:options "-functionSyntax:4"} JSON.Utils.Str {
       else [minus] + OfNat_any(-n, chars)
     }
 
-    function ToNat_any(str: String, base: nat, digits: map<Char, nat>) : (n: nat)
+    function {:vcs_split_on_every_assert} ToNat_any(str: String, base: nat, digits: map<Char, nat>) : (n: nat)
       requires base > 0
       requires forall c | c in str :: c in digits
     {
diff --git a/src/JSON/ZeroCopy/Deserializer.dfy b/src/JSON/ZeroCopy/Deserializer.dfy
index 80c7a9dc..0b7212f9 100644
--- a/src/JSON/ZeroCopy/Deserializer.dfy
+++ b/src/JSON/ZeroCopy/Deserializer.dfy
@@ -57,7 +57,7 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Deserializer {
       return Cursor(cs.s, cs.beg, point', cs.end).Split();
     }
 
-    function {:opaque} Structural<T>(cs: FreshCursor, parser: Parser<T>)
+    function {:opaque} {:vcs_split_on_every_assert} Structural<T>(cs: FreshCursor, parser: Parser<T>)
       : (pr: ParseResult<Structural<T>>)
       requires forall cs :: parser.fn.requires(cs)
       ensures pr.Success? ==> pr.value.StrictlySplitFrom?(cs, st => Spec.Structural(st, parser.spec))
@@ -288,6 +288,11 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Deserializer {
         && ((s0 == CLOSE as opt_byte) ==> var sp: Split<Structural<jclose>> := sp; sp.SplitFrom?(cs, st => Spec.Structural(st, SpecView)))
     {}
 
+    lemma {:vcs_split_on_every_assert} AboutLists<T>(xs: seq<T>, i: uint32)
+      requires 0 <= (i as int) < |xs|
+      ensures xs[(i as int)..(i as int)+1] == [xs[i as int]]
+    {}
+
     // The implementation and proof of this function is more painful than
     // expected due to the tail recursion.
     function {:vcs_split_on_every_assert} {:opaque} {:tailrecursion} Elements(
@@ -311,12 +316,20 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Deserializer {
         AboutTryStructural(elem.cs);
         var sep := Core.TryStructural(elem.cs);
         var s0 := sep.t.t.Peek();
-        if s0 == SEPARATOR as opt_byte then
+        if s0 == SEPARATOR as opt_byte && sep.t.t.Length() == 1 then
           assert sep.t.t.Char?(',') by {
             calc {
               sep.t.t.Char?(',');
               sep.t.t.Byte?(',' as byte);
               sep.t.t.Byte?(SEPARATOR);
+              sep.t.t.Bytes() == [SEPARATOR];
+              sep.t.t.s[(sep.t.t.beg as int)..(sep.t.t.end as int)] == [SEPARATOR];
+              { assert (sep.t.t.beg as int) + 1 == (sep.t.t.end as int) by { assert sep.t.t.Length() == 1; } }
+              sep.t.t.s[(sep.t.t.beg as int)..(sep.t.t.beg as int) + 1] == [SEPARATOR];
+              { assert sep.t.t.s[(sep.t.t.beg as int)..(sep.t.t.beg as int) + 1] == [sep.t.t.s[sep.t.t.beg as int]] by { AboutLists(sep.t.t.s, sep.t.t.beg); } }
+              [sep.t.t.s[sep.t.t.beg as int]] == [SEPARATOR];
+              sep.t.t.s[sep.t.t.beg as int] as opt_byte == SEPARATOR as opt_byte;
+              sep.t.t.At(0) as opt_byte == SEPARATOR as opt_byte;
               (s0 == SEPARATOR as opt_byte);
               true;
             }
@@ -342,10 +355,18 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Deserializer {
           }
           var elems := AppendWithSuffix(open.cs, json, elems, elem, sep);
           Elements(cs0, json, open, elems)
-        else if s0 == CLOSE as opt_byte then
+        else if s0 == CLOSE as opt_byte && sep.t.t.Length() == 1 then
           assert sep.t.t.Byte?(CLOSE) by {
             calc {
               sep.t.t.Byte?(CLOSE);
+              sep.t.t.Bytes() == [CLOSE];
+              sep.t.t.s[(sep.t.t.beg as int)..(sep.t.t.end as int)] == [CLOSE];
+              { assert (sep.t.t.beg as int) + 1 == (sep.t.t.end as int) by { assert sep.t.t.Length() == 1; } }
+              sep.t.t.s[(sep.t.t.beg as int)..(sep.t.t.beg as int) + 1] == [CLOSE];
+              { assert sep.t.t.s[(sep.t.t.beg as int)..(sep.t.t.beg as int) + 1] == [sep.t.t.s[sep.t.t.beg as int]] by { AboutLists(sep.t.t.s, sep.t.t.beg); } }
+              [sep.t.t.s[sep.t.t.beg as int]] == [CLOSE];
+              sep.t.t.s[sep.t.t.beg as int] as opt_byte == CLOSE as opt_byte;
+              sep.t.t.At(0) as opt_byte == CLOSE as opt_byte;
               (s0 == CLOSE as opt_byte);
               true;
             }
diff --git a/src/JSON/ZeroCopy/Serializer.dfy b/src/JSON/ZeroCopy/Serializer.dfy
index 5bd916dd..8746fdb6 100644
--- a/src/JSON/ZeroCopy/Serializer.dfy
+++ b/src/JSON/ZeroCopy/Serializer.dfy
@@ -67,7 +67,7 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Serializer {
     case Bool(b) => var wr := writer.Append(b); wr
     case String(str) => var wr := String(str, writer); wr
     case Number(num) => assert Grammar.Number(num) == v by { Spec.UnfoldValueNumber(v); }  var wr := Number(num, writer); wr
-    case Object(obj) => assert Grammar.Object(obj) == v; assert Spec.Value(v) == Spec.Object(obj); var wr := Object(obj, writer); wr
+    case Object(obj) => assert Grammar.Object(obj) == v; assert Spec.Value(v) == Spec.Value(Grammar.Object(obj)) == Spec.Object(obj); var wr := Object(obj, writer); wr
     case Array(arr) => assert Grammar.Array(arr) == v; assert Spec.Value(v) == Spec.Array(arr); var wr := Array(arr, writer); assert wr.Bytes() == writer.Bytes() + Spec.Value(v); wr
   }