JSON support

.github/workflows/check-examples-in-docs.yml

@@ -15,7 +15,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        version: [ 3.12.0, 3.13.1, 4.0.0 ]
+        version: [ 3.13.1, 4.0.0 ]
         os: [ ubuntu-latest ]
 
     runs-on: ${{ matrix.os }}

.github/workflows/check-format.yml

@@ -13,9 +13,9 @@ jobs:
       - uses: actions/checkout@v3
 
       - name: Install Dafny
-        uses: dafny-lang/setup-dafny-action@v1
+        uses: dafny-lang/setup-dafny-action@v1.6.1
         with:
-          dafny-version: "nightly-2023-02-15-567a5ba"
+          dafny-version: "4.0.0"
 
       - name: Install lit
         run: pip install lit OutputCheck

.github/workflows/nightly.yml

@@ -14,12 +14,7 @@ jobs:
   verification:
     strategy:
       matrix:
-        # nightly-latest to catch anything that breaks these tests in current development
-        # 2/18/2023 version is the first that supports logging, but it is not supported by setup-dafny-action 1.6.1
-        # 3.11.0 supports new CLI but does not support logging
-        # setup-dafny-action does not yet support 3.13.1 or recent nightly-lates
-
-        version: [ nightly-latest, nightly-2023-02-18-ef4f346, 3.11.0, 3.12.0, 3.13.1, 4.0.0 ]
+        version: [ nightly-latest ]
 
     uses: ./.github/workflows/reusable-tests.yml
     with:

.github/workflows/reusable-tests.yml

@@ -39,23 +39,14 @@ jobs:
       - name: Set up JS dependencies
         run: npm install bignumber.js
 
-      - name: Verify Code and Examples without logging
-        id: nolog
-        if: inputs.dafny-version == '3.11.0'
-        run: lit --time-tests -v .
-
       - name: Verify Code and Examples
-        id: withlog
-        if: steps.nolog.conclusion == 'skipped'
         run: |
           lit --time-tests -v --param 'dafny_params=--log-format trx --log-format csv' .
 
       - name: Generate Report
-        if: always() && steps.withlog.conclusion != 'skipped'
-        run: find . -name '*.csv' -print0 | xargs -0 --verbose dafny-reportgenerator summarize-csv-results --max-duration-seconds 10
+        run: find . -name '*.csv' -print0 | xargs -0 --verbose dafny-reportgenerator summarize-csv-results --max-resource-count 40000000
 
       - uses: actions/upload-artifact@v2  # upload test results
-        if: always() && steps.withlog.conclusion != 'skipped'
         with:
           name: verification-results
           path: '**/TestResults/*.trx'

.github/workflows/tests.yml

@@ -13,11 +13,7 @@ jobs:
   verification:
     strategy:
       matrix:
-        # nightly-latest to catch anything that breaks these tests in current development
-        # 2/18/2023 version is the first that supports logging, but it is not supported by dafny-setup-action 1.6.1
-        # 3.11.0 supports new CLI but does not support logging
-        # setup-dafny-action does not yet support 3.13.1 or recent nightly-latest
-        version: [ 3.11.0, 3.12.0, 3.13.1, 4.0.0 ]
+        version: [ 3.13.1, 4.0.0 ]
 
     uses: ./.github/workflows/reusable-tests.yml
     with:

lit.site.cfg

@@ -140,6 +140,7 @@ resolveArgs = ' resolve --use-basename-for-filename ' + standardArguments
 verifyArgs = ' verify --use-basename-for-filename --cores:2 --verification-time-limit:300 ' + standardArguments
 buildArgs = ' build --use-basename-for-filename --cores:2 --verification-time-limit:300 ' + standardArguments
 runArgs = ' run --use-basename-for-filename --cores:2 --verification-time-limit:300 ' + standardArguments
+testArgs = ' test --use-basename-for-filename --cores:2 --verification-time-limit:300 ' + standardArguments
 
 config.substitutions.append( ('%trargs', '--use-basename-for-filename --cores:2 --verification-time-limit:300' ) )
 
@@ -148,6 +149,7 @@ config.substitutions.append( ('%verify', dafnyExecutable + verifyArgs ) )
 config.substitutions.append( ('%translate', dafnyExecutable + ' translate'  ) )
 config.substitutions.append( ('%build', dafnyExecutable + buildArgs ) )
 config.substitutions.append( ('%run', dafnyExecutable + runArgs ) )
+config.substitutions.append( ('%test', dafnyExecutable + runArgs ) )
 
 # config.substitutions.append( ('%repositoryRoot', repositoryRoot) )
 # config.substitutions.append( ('%binaryDir', binaryDir) )

src/BoundedInts.dfy

@@ -2,7 +2,6 @@
 
 module {:options "-functionSyntax:4"} BoundedInts {
   const TWO_TO_THE_0:   int := 1
-
   const TWO_TO_THE_1:   int := 2
   const TWO_TO_THE_2:   int := 4
   const TWO_TO_THE_4:   int := 16
@@ -20,12 +19,12 @@ module {:options "-functionSyntax:4"} BoundedInts {
   const TWO_TO_THE_512: int :=
     0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000;
 
-  newtype uint8 = x: int  | 0 <= x < TWO_TO_THE_8
+  newtype uint8  = x: int | 0 <= x < TWO_TO_THE_8
   newtype uint16 = x: int | 0 <= x < TWO_TO_THE_16
   newtype uint32 = x: int | 0 <= x < TWO_TO_THE_32
   newtype uint64 = x: int | 0 <= x < TWO_TO_THE_64
 
-  newtype int8 = x: int   | -0x80 <= x < 0x80
+  newtype int8  = x: int  | -0x80 <= x < 0x80
   newtype int16 = x: int  | -0x8000 <= x < 0x8000
   newtype int32 = x: int  | -0x8000_0000 <= x < 0x8000_0000
   newtype int64 = x: int  | -0x8000_0000_0000_0000 <= x < 0x8000_0000_0000_0000
@@ -35,4 +34,26 @@ module {:options "-functionSyntax:4"} BoundedInts {
   newtype nat32 = x: int  | 0 <= x < 0x8000_0000
   newtype nat64 = x: int  | 0 <= x < 0x8000_0000_0000_0000
 
+  const UINT8_MAX:  uint8  := 0xFF
+  const UINT16_MAX: uint16 := 0xFFFF
+  const UINT32_MAX: uint32 := 0xFFFF_FFFF
+  const UINT64_MAX: uint64 := 0xFFFF_FFFF_FFFF_FFFF
+
+  const INT8_MIN:  int8  := -0x80
+  const INT8_MAX:  int8  :=  0x7F
+  const INT16_MIN: int16 := -0x8000
+  const INT16_MAX: int16 :=  0x7FFF
+  const INT32_MIN: int32 := -0x8000_0000
+  const INT32_MAX: int32 :=  0x7FFFFFFF
+  const INT64_MIN: int64 := -0x8000_0000_0000_0000
+  const INT64_MAX: int64 :=  0x7FFFFFFF_FFFFFFFF
+
+  const NAT8_MAX:  nat8  := 0x7F
+  const NAT16_MAX: nat16 := 0x7FFF
+  const NAT32_MAX: nat32 := 0x7FFFFFFF
+  const NAT64_MAX: nat64 := 0x7FFFFFFF_FFFFFFFF
+
+  type byte = uint8
+  type bytes = seq<byte>
+  newtype opt_byte = c: int | -1 <= c < TWO_TO_THE_8
 }

src/Collections/Sequences/Seq.dfy

@@ -90,6 +90,26 @@ module {:options "-functionSyntax:4"} Seq {
    *
    ***********************************************************/
 
+  /* If a predicate is true at every index of a sequence,
+     it is true for every member of the sequence as a collection.
+     Useful for converting quantifiers between the two forms
+     to satisfy a precondition in the latter form. */
+  lemma IndexingImpliesMembership<T>(p: T -> bool, xs: seq<T>)
+    requires forall i | 0 <= i < |xs| :: p(xs[i])
+    ensures forall t | t in xs :: p(t)
+  {
+  }
+
+  /* If a predicate is true for every member of a sequence as a collection,
+     it is true at every index of the sequence.
+     Useful for converting quantifiers between the two forms
+     to satisfy a precondition in the latter form. */
+  lemma MembershipImpliesIndexing<T>(p: T -> bool, xs: seq<T>)
+    requires forall t | t in xs :: p(t)
+    ensures forall i | 0 <= i < |xs| :: p(xs[i])
+  {
+  }
+
   /* Is true if the sequence xs is a prefix of the sequence ys. */
   ghost predicate IsPrefix<T>(xs: seq<T>, ys: seq<T>)
     ensures IsPrefix(xs, ys) ==> (|xs| <= |ys| && xs == ys[..|xs|])
@@ -603,8 +623,12 @@ module {:options "-functionSyntax:4"} Seq {
     ensures forall i {:trigger result[i]} :: 0 <= i < |xs| ==> result[i] == f(xs[i]);
     reads set i, o | 0 <= i < |xs| && o in f.reads(xs[i]) :: o
   {
-    if |xs| == 0 then []
-    else [f(xs[0])] + Map(f, xs[1..])
+    // This uses a sequence comprehension because it will usually be
+    // more efficient when compiled, allocating the storage for |xs| elements
+    // once instead of creating a chain of |xs| single element concatenations.
+    seq(|xs|, i requires 0 <= i < |xs| && f.requires(xs[i])
+                reads set i,o | 0 <= i < |xs| && o in f.reads(xs[i]) :: o
+    => f(xs[i]))
   }
 
   /* Applies a function to every element of a sequence, returning a Result value (which is a 
@@ -803,6 +827,25 @@ module {:options "-functionSyntax:4"} Seq {
     }
   }
 
+  /* Optimized implementation of Flatten(Map(f, xs)). */
+  function FlatMap<T,R>(f: (T ~> seq<R>), xs: seq<T>): (result: seq<R>)
+    requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i])
+    reads set i, o | 0 <= i < |xs| && o in f.reads(xs[i]) :: o
+  {
+    Flatten(Map(f, xs))
+  }
+  by method {
+    result := [];
+    ghost var unflattened: seq<seq<R>> := [];
+    for i := |xs| downto 0
+      invariant unflattened == Map(f, xs[i..])
+      invariant result == Flatten(unflattened)
+    {
+      var next := f(xs[i]);
+      unflattened := [next] + unflattened;
+      result := next + result;
+    }
+  }
 
   /**********************************************************
    *

src/JSON/API.dfy

@@ -0,0 +1,40 @@
+// RUN: %verify "%s" --unicode-char:false ../Unicode/UnicodeStringsWithoutUnicodeChar.dfy
+// RUN: %verify "%s" --unicode-char:true ../Unicode/UnicodeStringsWithUnicodeChar.dfy
+
+include "Serializer.dfy"
+include "Deserializer.dfy"
+include "ZeroCopy/API.dfy"
+
+module {:options "-functionSyntax:4"} JSON.API {
+  import opened BoundedInts
+  import opened Errors
+  import Values
+  import Serializer
+  import Deserializer
+  import ZeroCopy = ZeroCopy.API
+
+  function {:opaque} Serialize(js: Values.JSON) : (bs: SerializationResult<seq<byte>>)
+  {
+    var js :- Serializer.JSON(js);
+    ZeroCopy.Serialize(js)
+  }
+
+  method SerializeAlloc(js: Values.JSON) returns (bs: SerializationResult<array<byte>>)
+  {
+    var js :- Serializer.JSON(js);
+    bs := ZeroCopy.SerializeAlloc(js);
+  }
+
+  method SerializeInto(js: Values.JSON, bs: array<byte>) returns (len: SerializationResult<uint32>)
+    modifies bs
+  {
+    var js :- Serializer.JSON(js);
+    len := ZeroCopy.SerializeInto(js, bs);
+  }
+
+  function {:opaque} Deserialize(bs: seq<byte>) : (js: DeserializationResult<Values.JSON>)
+  {
+    var js :- ZeroCopy.Deserialize(bs);
+    Deserializer.JSON(js)
+  }
+}

src/JSON/ConcreteSyntax.Spec.dfy

@@ -0,0 +1,121 @@
+// RUN: %verify "%s"
+
+include "Grammar.dfy"
+
+module {:options "-functionSyntax:4"} JSON.ConcreteSyntax.Spec {
+  import opened BoundedInts
+
+  import Vs = Utils.Views.Core
+  import opened Grammar
+
+  function View(v: Vs.View) : bytes {
+    v.Bytes()
+  }
+
+  function Structural<T>(self: Structural<T>, fT: T -> bytes): bytes {
+    View(self.before) + fT(self.t) + View(self.after)
+  }
+
+  function StructuralView(self: Structural<Vs.View>): bytes {
+    Structural<Vs.View>(self, View)
+  }
+
+  function Maybe<T>(self: Maybe<T>, fT: T -> bytes): (bs: bytes)
+    ensures self.Empty? ==> bs == []
+    ensures self.NonEmpty? ==> bs == fT(self.t)
+  {
+    if self.Empty? then [] else fT(self.t)
+  }
+
+  function ConcatBytes<T>(ts: seq<T>, fT: T --> bytes) : bytes
+    requires forall d | d in ts :: fT.requires(d)
+  {
+    if |ts| == 0 then []
+    else fT(ts[0]) + ConcatBytes(ts[1..], fT)
+  }
+
+  function Bracketed<D, S>(self: Bracketed<Vs.View, D, S, Vs.View>, fDatum: Suffixed<D, S> --> bytes): bytes
+    requires forall d | d < self :: fDatum.requires(d)
+  {
+    StructuralView(self.l) +
+    ConcatBytes(self.data, fDatum) +
+    StructuralView(self.r)
+  }
+
+  function KeyValue(self: jKeyValue): bytes {
+    String(self.k) + StructuralView(self.colon) + Value(self.v)
+  }
+
+  function Frac(self: jfrac): bytes {
+    View(self.period) + View(self.num)
+  }
+
+  function Exp(self: jexp): bytes {
+    View(self.e) + View(self.sign) + View(self.num)
+  }
+
+  function Number(self: jnumber): bytes {
+    View(self.minus) + View(self.num) + Maybe(self.frac, Frac) + Maybe(self.exp, Exp)
+  }
+
+  function String(self: jstring): bytes {
+    View(self.lq) + View(self.contents) + View(self.rq)
+  }
+
+  function CommaSuffix(c: Maybe<Structural<jcomma>>): bytes {
+    // BUG(https://github.com/dafny-lang/dafny/issues/2179)
+    Maybe<Structural<Vs.View>>(c, StructuralView)
+  }
+
+  function Member(self: jmember) : bytes {
+    KeyValue(self.t) + CommaSuffix(self.suffix)
+  }
+
+  function Item(self: jitem) : bytes {
+    Value(self.t) + CommaSuffix(self.suffix)
+  }
+
+  function Object(obj: jobject) : bytes {
+    Bracketed(obj, (d: jmember) requires d < obj => Member(d))
+  }
+
+  function Array(arr: jarray) : bytes {
+    Bracketed(arr, (d: jitem) requires d < arr => Item(d))
+  }
+
+  function Value(self: Value) : bytes {
+    match self {
+      case Null(n) => View(n)
+      case Bool(b) => View(b)
+      case String(str) => String(str)
+      case Number(num) => Number(num)
+      case Object(obj) => Object(obj)
+      case Array(arr) => Array(arr)
+    }
+  }
+
+  lemma UnfoldValueNumber(v: Value)
+    requires v.Number?
+    ensures Value(v) == Number(v.num)
+  {
+    assert Value(v) == match v { case Number(num) => Number(num) case _ => []};
+  }
+
+  lemma UnfoldValueObject(v: Value)
+    requires v.Object?
+    ensures Value(v) == Object(v.obj)
+  {
+    assert Value(v) == match v { case Object(obj) => Object(obj) case _ => []};
+  }
+
+  lemma UnfoldValueArray(v: Value)
+    requires v.Array?
+    ensures Value(v) == Array(v.arr)
+  {
+    assert Value(v) == match v { case Array(arr) => Array(arr) case _ => []};
+  }
+
+  function JSON(js: JSON) : bytes {
+    Structural(js, Value)
+  }
+}