-
Notifications
You must be signed in to change notification settings - Fork 25
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Co-authored-by: Mikaël Mayer <[email protected]> Co-authored-by: Alex Chew <[email protected]> Co-authored-by: Robin Salkeld <[email protected]> Co-authored-by: Fabio Madge <[email protected]>
- Loading branch information
5 people
authored
May 5, 2023
1 parent
7c386fa
commit 3ff49f8
Showing
40 changed files
with
4,213 additions
and
29 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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) | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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) | ||
| } | ||
| } |
Oops, something went wrong.