JSON support #51

cpitclaudel · 2022-09-02T22:13:18Z

The library is documented in JSON/README.md, and there is a tutorial in JSON/Tutorial.dfy.

dafny-lang/dafny#2179

seebees

I'll try and add more.
I really do love the pervasive use of ? :)

src/JSON/Utils/Cursors.dfy

MikaelMayer

This is excellent ! Very well documented an implemented.
My comments are mostly about renaming and comments.

src/BoundedInts.dfy

src/JSON/README.md

MikaelMayer · 2022-09-06T19:24:18Z

src/JSON/API.dfy

+include "Deserializer.dfy"
+include "ZeroCopy/API.dfy"
+
+module {:options "-functionSyntax:4"} JSON.API {


Let's think about names for a moment. Names are the crown of all the hard work you have been putting into this library, and now you have time to step back and think about it ^^.
Everything in library is an API, so using API as a name makes little sense. What about just JSON here?

I cannot use just JSON, unfortunately :( That's because definitions in the JSON module cannot use definitions in submodules of it, like JSON.XYZ.

I considered having two top-level modules JSON and JSONImpl, but that's not great either.

Finally, this respects the link between module names and file names (JSON.API in JSON/Api).

We ought to improve this in the new module system.

Keeping JSON.API, it would be possible to create a file in the folder above JSON.dfy that refines this module, so that users don't need to write JSON.API? Could you do this? I don't see myself writing JSON.API to invoke JSON routines. JavaScript offers JSON.stringify and JSON.parse.

That would introduce a mismatch between the file name and the file path. You can, however, do import JSON.API as JS, which is good, I think?

It is good, but not good enough for what we want to be a default library. I'll take a pass on that later.

Agreed this is good enough given the whole repo reserves the right to rename things for now.

MikaelMayer · 2022-09-06T21:29:07Z

src/JSON/Utils/Views.dfy

+  import opened BoundedInts
+
+  type View = v: View_ | v.Valid? witness View([], 0, 0)
+  datatype View_ = View(s: bytes, beg: uint32, end: uint32) {


You might have preferred "beg" so that it aligns nicely with "end", but aligning is not relevant from the API's interface. "beg" is not a word, and I like that datatype libraries use regular words for identifiers.

I strongly suggest you use "start" here or "beginning"

Could you rename the variable "s" as "bytes" ? If it causes conflict with the type, I would prefer that you rename the type byteSeq so that it's more transparent as a type and bytes can be used as the name.

These fields (and the constructor) are intended to be internal, so keeping them short and (somewhat) opaque isn't necessarily a bad thing, I think. It's important for encapsulation to not peek at the underlying string or at the bounds.

In contrast, renaming s to bytes would be misleading, because there is a public function Bytes that gives you s[beg..end].

That said, I'm OK to rename if you're not convinced.

MikaelMayer · 2022-09-06T21:31:08Z

src/JSON/Utils/Views.dfy

+      else At(0) as opt_byte
+    }
+
+    method Blit(bs: array<byte>, start: uint32 := 0)


Would it make sense to rename Blit to WriteTo?
also, "bs" => "bytes"
"start" => "offset" (so that you can use "start" instead of "beg" as in my comment above)

I agree with you; Blit is a bit opaque. But I think it should be CopyTo, to make it clear that the original object isn't affected.

bs is the convention throughout, but I agree with you that it's not the best. However bytes isn't informative either; it just repeats the type. I think the right name would be target or dest; I chose dest based on https://stackoverflow.com/questions/60532503/whats-different-between-words-target-and-dest

start I would prefer to not change, because other functions have end (here since it's a public API I didn't use beg)

src/JSON/Utils/Views.Writers.dfy

MikaelMayer · 2022-09-13T20:52:49Z

src/JSON/ZeroCopy/API.dfy

+    bs := Serializer.Serialize(js);
+  }
+
+  method SerializeBlit(js: Grammar.JSON, bs: array<byte>) returns (len: SerializationResult<uint32>)


Blit? What does that mean?

https://en.wikipedia.org/wiki/Bit_blit
It means overwriting (or updating) part of an array from another datastructure.

The link is just for information; I renamed it of course :)

MikaelMayer · 2022-09-13T21:13:16Z

src/NonlinearArithmetic/Logarithm.dfy

+include "DivMod.dfy"
+include "Power.dfy"
+
+module Logarithm {


Could you perhaps name this module/file Integers? That way, we would have Integers.Log

This isn't how the rest of this library is structured; I tried to stay consistent with what was already there.
(Also, if you named it Integers, wouldn't you want to have other modules also named Integers in other files?)

Mmmh that makes me think it should just be included in a Math module so that we have Math.log. Let's do that later.

MikaelMayer · 2022-09-13T21:14:24Z

src/JSON/Deserializer.dfy

+    js.At(0) == 't' as byte
+  }
+
+  function Unescape(str: string, start: nat := 0): DeserializationResult<string>


If you did not write a verifier for Escape/Unescape, could you please add a comment in front of each function?

Done, but just in front of Unescape: Escape is the spec :)

MikaelMayer · 2022-09-13T21:15:07Z

src/BoundedInts.dfy

+  const NAT8_MAX:  nat8  := 0x7F
+  const NAT16_MAX: nat16 := 0x7FFF
+  const NAT32_MAX: nat32 := 0x7FFFFFFF
+  const NAT64_MAX: nat64 := 0x7FFFFFFF_FFFFFFFF


There might be some redundancy with the PR with the Heap. Could you synchronize with @prvshah51 to ensure we define these constant in only one place?

I think Parva didn't include these in the end; right? So no conflict.

Co-authored-by: Mikaël Mayer <[email protected]>

dafny-lang/dafny#3951

…ubset types" This reverts commit d2fa10f.

This reverts commit ceed951.

Can’t get it to verify with Dafny 4.0. Will leave getting the code to compile for follow up after merging.

MikaelMayer

I have a few changes to request, but otherwise looks good !

src/Collections/Sequences/Seq.dfy

src/JSON/ConcreteSyntax.SpecProperties.dfy

MikaelMayer · 2023-05-05T15:03:56Z

src/JSON/Deserializer.dfy

  // TODO: Verify this function
-  function Unescape(str: string, start: nat := 0): DeserializationResult<string>
+  function {:tailrecursion} {:vcs_split_on_every_assert} Unescape(str: seq<uint16>, start: nat := 0, prefix: seq<uint16> := []): DeserializationResult<seq<uint16>>


Remove the TODO above?

Done, not because I don't think it would be valuable to add more specification to this function, but because that will be quite a bit of work. I also don't want to imply there's no verification happening in this code.

MikaelMayer · 2023-05-05T15:05:14Z

src/JSON/Deserializer.dfy

  }

  function String(js: Grammar.jstring): DeserializationResult<string> {
-    Transcode8To16Unescaped(js.contents.Bytes())
+    // TODO Optimize with a function by method


Can this TODO be more precise about what can be optimized?

I removed it: since that TODO was left there, I make Unescape tail-recursive to address the worst performance issue. There's definitely more to do here and in the Unicode module, but that's a more widespread challenge to take on in the future.

src/JSON/Utils/Seq.dfy

MikaelMayer · 2023-05-05T15:25:11Z

src/JSON/ZeroCopy/Deserializer.dfy

+      assert cs.Bytes() == Spec.Bracketed(sp.t, SuffixedElementSpec) + close.cs.Bytes() by {
+        assert cs.Bytes() == Spec.Structural(open.t, SpecView) + SuffixedElementsSpec(elems.t) + Spec.Structural(close.t, SpecView) + close.cs.Bytes() by {
+          assert cs.Bytes() == Spec.Structural(open.t, SpecView) + open.cs.Bytes();
+          assert open.cs.Bytes() == SuffixedElementsSpec(elems.t) + elems.cs.Bytes();
+          assert elems.cs.Bytes() == Spec.Structural(close.t, SpecView) + close.cs.Bytes();
+          Seq.Assoc'(Spec.Structural(open.t, SpecView), SuffixedElementsSpec(elems.t), elems.cs.Bytes());
+          Seq.Assoc'(Spec.Structural(open.t, SpecView) + SuffixedElementsSpec(elems.t), Spec.Structural(close.t, SpecView), close.cs.Bytes());
+        }
      }


Suggested change

assert cs.Bytes() == Spec.Bracketed(sp.t, SuffixedElementSpec) + close.cs.Bytes() by {

assert cs.Bytes() == Spec.Structural(open.t, SpecView) + SuffixedElementsSpec(elems.t) + Spec.Structural(close.t, SpecView) + close.cs.Bytes() by {

assert cs.Bytes() == Spec.Structural(open.t, SpecView) + open.cs.Bytes();

assert open.cs.Bytes() == SuffixedElementsSpec(elems.t) + elems.cs.Bytes();

assert elems.cs.Bytes() == Spec.Structural(close.t, SpecView) + close.cs.Bytes();

Seq.Assoc'(Spec.Structural(open.t, SpecView), SuffixedElementsSpec(elems.t), elems.cs.Bytes());

Seq.Assoc'(Spec.Structural(open.t, SpecView) + SuffixedElementsSpec(elems.t), Spec.Structural(close.t, SpecView), close.cs.Bytes());

}

}

calc {

cs.Bytes();

Spec.Structural(open.t, SpecView) + open.cs.Bytes();

{ assert open.cs.Bytes() == SuffixedElementsSpec(elems.t) + elems.cs.Bytes(); }

Spec.Structural(open.t, SpecView) + (SuffixedElementsSpec(elems.t) + elems.cs.Bytes());

{ Seq.Assoc'(Spec.Structural(open.t, SpecView), SuffixedElementsSpec(elems.t), elems.cs.Bytes()); }

Spec.Structural(open.t, SpecView) + SuffixedElementsSpec(elems.t) + elems.cs.Bytes();

{ assert elems.cs.Bytes() == Spec.Structural(close.t, SpecView) + close.cs.Bytes(); }

Spec.Structural(open.t, SpecView) + SuffixedElementsSpec(elems.t) + (Spec.Structural(close.t, SpecView) + close.cs.Bytes());

{ Seq.Assoc'(Spec.Structural(open.t, SpecView) + SuffixedElementsSpec(elems.t), Spec.Structural(close.t, SpecView), close.cs.Bytes()); }

Spec.Structural(open.t, SpecView) + SuffixedElementsSpec(elems.t) + Spec.Structural(close.t, SpecView) + close.cs.Bytes();

Spec.Bracketed(sp.t, SuffixedElementSpec) + close.cs.Bytes();

}

Calc statements are much nicer to reason about and provide the same flexibility as assert ... by, including the ability to provide local proofs. For example, the calls to the two associativity lemmas can be done as a hint.
I verified visually that this proves the same thing as the nested assert by above, but please give it a try in the verifier.
I tested this proof locally, the Resource count drops from 470k to 426k as well.

NICE, thanks! I had that thought too but didn't want to get greedy once we got everything to verify. :)

MikaelMayer · 2023-05-05T19:35:32Z

src/JSON/ZeroCopy/Deserializer.dfy

+      }
+      assert elems'.StrictlySplitFrom?(cs0, SuffixedElementsSpec);
+      assert forall e | e in elems'.t :: e.suffix.NonEmpty? by { assert elems'.t == elems.t + [suffixed]; }
+      assert {:split_here} elems'.cs.Length() < elems.cs.Length();


I tried to apply the same calc technique there but couldn't arrive to something that would verify quickly enough.

Co-authored-by: Mikaël Mayer <[email protected]>

MikaelMayer

Looks good to me ! Great to have.

Tracking under #119 (and https://github.com/dafny-lang/libraries/milestone/1 in general) rather than delaying merging this any longer

MikaelMayer

There is a formatting bug that will fix one issue later
dafny-lang/dafny#3960
but for now it's good enough :-)

MikaelMayer

There is a formatting bug that will fix one issue later
dafny-lang/dafny#3960
but for now it's good enough :-)

MikaelMayer

There is a formatting bug that will fix one issue later
dafny-lang/dafny#3960
but for now it's good enough :-)

cpitclaudel added 16 commits September 1, 2022 22:29

feat: Add a JSON serializer/deserializer

4e43e63

json: Add an efficient serializer

f611179

json: Move away from member functions to reduce the number of lambdas

e3d8e83

dafny-lang/dafny#2179

json: Clean up grammar and put separators after items, not before

c5394f7

json: Complete soundness proof

72708eb

json: Add a clean low-level API

2a0c713

json: Speed things up using by method bodies in a few places

593b32e

json: Small cleanup in types

4c50ce6

json(wip): Start working on high-level API

0198334

json: Clean up encoder and add decoder

a827a77

json: Optimize traversals and add support for unicode escapes

8af0e54

json: Finish unicode encoding and decoding

32068c0

json: Adopt a consistent naming scheme across modules

5ffcf35

json: Clean up API files

6ba1735

json: Merge latest changes to the vectors library

74f9b0b

json: Move IntPow and IntLog to their own utility module

a0a8166

cpitclaudel requested review from jtristan, MikaelMayer and robin-aws September 2, 2022 22:13

cpitclaudel mentioned this pull request Sep 2, 2022

Low-level JSON parsing/serialization library #43

Closed

3 tasks

cpitclaudel added 5 commits September 2, 2022 15:25

json: Add a README

c032f8b

json: Add a useful postcondition to Views.Merge

2de6306

json: Speed up a proof

92a8f8d

json: Move all math code to NonlinearArithmetic/ and use /noNLArith

390e288

json: Add a tutorial

dcd06cc

cpitclaudel force-pushed the json-merge branch from cb0ac78 to dcd06cc Compare September 2, 2022 22:26

jtristan previously approved these changes Sep 9, 2022

View reviewed changes

seebees reviewed Sep 12, 2022

View reviewed changes

src/JSON/Utils/Cursors.dfy Show resolved Hide resolved

src/JSON/Utils/Cursors.dfy Show resolved Hide resolved

src/JSON/Utils/Cursors.dfy Show resolved Hide resolved

MikaelMayer requested changes Sep 13, 2022

View reviewed changes

Update src/JSON/README.md

f23ed82

Co-authored-by: Mikaël Mayer <[email protected]>

Remove unused function that can’t be compiled for Java

8992608

dafny-lang/dafny#3951

robin-aws dismissed their stale review via 8992608 May 4, 2023 17:38

robin-aws added 7 commits May 4, 2023 10:50

Formatting

f277ffe

Double checking ZeroCopy/Deserializer.dfy verifies with the subset types

d2fa10f

Revert "Double checking ZeroCopy/Deserializer.dfy verifies with the s…

acdb6ec

…ubset types" This reverts commit d2fa10f.

Progress on verifying again

ceed951

Revert "Progress on verifying again"

fc2ee8c

This reverts commit ceed951.

Undoing subset type workaround

53b7abf

Can’t get it to verify with Dafny 4.0. Will leave getting the code to compile for follow up after merging.

Formatting

2753e76

robin-aws previously approved these changes May 4, 2023

View reviewed changes

MikaelMayer requested changes May 5, 2023

View reviewed changes

Apply suggestions from code review

35cca47

Co-authored-by: Mikaël Mayer <[email protected]>

robin-aws dismissed their stale review via 35cca47 May 5, 2023 20:36

robin-aws added 3 commits May 5, 2023 13:36

Removing stale TODOs

62d5c89

Mikael’s calc rewrite

da1b5ac

Formatting

45055e1

MikaelMayer previously approved these changes May 5, 2023

View reviewed changes

robin-aws dismissed MikaelMayer’s stale review via 45055e1 May 5, 2023 21:06

robin-aws previously approved these changes May 5, 2023

View reviewed changes

I said, FORMATTING

a58e01d

robin-aws dismissed their stale review via a58e01d May 5, 2023 21:18

robin-aws approved these changes May 5, 2023

View reviewed changes

MikaelMayer approved these changes May 5, 2023

View reviewed changes

robin-aws enabled auto-merge (squash) May 5, 2023 21:22

robin-aws merged commit 3ff49f8 into master May 5, 2023

robin-aws deleted the json-merge branch May 5, 2023 21:42

robin-aws mentioned this pull request May 5, 2023

Request: connecting Unicode logic to the string type #111

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

JSON support #51

JSON support #51

cpitclaudel commented Sep 2, 2022

seebees left a comment

MikaelMayer left a comment

MikaelMayer Sep 6, 2022

cpitclaudel Dec 29, 2022

MikaelMayer Dec 29, 2022

cpitclaudel Dec 30, 2022

MikaelMayer Dec 30, 2022

robin-aws Mar 7, 2023

MikaelMayer Sep 6, 2022

cpitclaudel Dec 29, 2022

MikaelMayer Sep 6, 2022

cpitclaudel Dec 30, 2022

MikaelMayer Sep 13, 2022

cpitclaudel Dec 30, 2022

cpitclaudel Dec 30, 2022

MikaelMayer Sep 13, 2022

cpitclaudel Dec 30, 2022

MikaelMayer Dec 30, 2022

MikaelMayer Sep 13, 2022

cpitclaudel Dec 30, 2022

MikaelMayer Sep 13, 2022

cpitclaudel Dec 30, 2022

MikaelMayer left a comment

MikaelMayer May 5, 2023

robin-aws May 5, 2023

MikaelMayer May 5, 2023

robin-aws May 5, 2023

MikaelMayer May 5, 2023

robin-aws May 5, 2023

MikaelMayer May 5, 2023

MikaelMayer left a comment

MikaelMayer left a comment

MikaelMayer left a comment

MikaelMayer left a comment

JSON support #51

JSON support #51

Conversation

cpitclaudel commented Sep 2, 2022

seebees left a comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment