chore: Improve proofs

dafny-lang · Dec 25, 2024 · 8cf5e3a · 8cf5e3a
1 parent 2a0e013
commit 8cf5e3a
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 7 deletions.
diff --git a/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy b/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy
@@ -56,6 +56,12 @@ module Std.Collections.Seq {
     xs[..|xs|-1]
   }
 
+  lemma TakeLess<T>(s: seq<T>, m: nat, n: nat)
+    requires m <= n <= |s|
+    ensures s[..n][..m] == s[..m]
+  {
+  }
+
   /* The concatenation of two subsequences of a non-empty sequence, the first obtained
      from dropping the last element, the second consisting only of the last
      element, is the original sequence. */

diff --git a/Source/DafnyStandardLibraries/src/Std/JSON/Utils/Views.Writers.dfy b/Source/DafnyStandardLibraries/src/Std/JSON/Utils/Views.Writers.dfy
@@ -8,7 +8,6 @@
  */
 module Std.JSON.Utils.Views.Writers {
   import opened BoundedInts
-  import opened Wrappers
   import opened Core
 
   datatype Chain =
@@ -121,4 +120,4 @@ module Std.JSON.Utils.Views.Writers {
       CopyTo(bs);
     }
   }
-}
+}
diff --git a/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Deserializer.dfy b/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Deserializer.dfy
@@ -291,11 +291,17 @@ module Std.JSON.ZeroCopy.Deserializer {
       ensures
         var sp := Core.TryStructural(cs);
         var s0 := sp.t.t.Peek();
-        && ((!cs.BOF? || !cs.EOF?) && (s0 == SEPARATOR as opt_byte) ==> (var sp: Split<Structural<jcomma>> := sp; sp.cs.StrictSuffixOf?(cs)))
-        && ((s0 == SEPARATOR as opt_byte) ==> var sp: Split<Structural<jcomma>> := sp; sp.SplitFrom?(cs, st => Spec.Structural(st, SpecView)))
-        && ((!cs.BOF? || !cs.EOF?) && (s0 == CLOSE as opt_byte) ==> (var sp: Split<Structural<jclose>> := sp; sp.cs.StrictSuffixOf?(cs)))
-        && ((s0 == CLOSE as opt_byte) ==> var sp: Split<Structural<jclose>> := sp; sp.SplitFrom?(cs, st => Spec.Structural(st, SpecView)))
+        && ((!cs.BOF? || !cs.EOF?) && s0 == SEPARATOR as opt_byte ==> var sp: Split<Structural<jcomma>> := sp; sp.cs.StrictSuffixOf?(cs))
+        && (s0 == SEPARATOR as opt_byte ==> var sp: Split<Structural<jcomma>> := sp; sp.SplitFrom?(cs, st => Spec.Structural(st, SpecView)))
+        && ((!cs.BOF? || !cs.EOF?) && s0 == CLOSE as opt_byte ==> var sp: Split<Structural<jclose>> := sp; sp.cs.StrictSuffixOf?(cs))
+        && (s0 == CLOSE as opt_byte ==> var sp: Split<Structural<jclose>> := sp; sp.SplitFrom?(cs, st => Spec.Structural(st, SpecView)))
     {
+      var sp := Core.TryStructural(cs);
+      var s0 := sp.t.t.Peek();
+      assert (!cs.BOF? || !cs.EOF?) && s0 == SEPARATOR as opt_byte ==> var sp: Split<Structural<jcomma>> := sp; sp.cs.StrictSuffixOf?(cs);
+      assert s0 == SEPARATOR as opt_byte ==> var sp: Split<Structural<jcomma>> := sp; sp.SplitFrom?(cs, st => Spec.Structural(st, SpecView));
+      assert (!cs.BOF? || !cs.EOF?) && s0 == CLOSE as opt_byte ==> var sp: Split<Structural<jclose>> := sp; sp.cs.StrictSuffixOf?(cs);
+      assert s0 == CLOSE as opt_byte ==> var sp: Split<Structural<jclose>> := sp; sp.SplitFrom?(cs, st => Spec.Structural(st, SpecView));
     }
 
     @IsolateAssertions
@@ -796,6 +802,7 @@ module Std.JSON.ZeroCopy.Deserializer {
       if period.Empty? then
         Success(SP(Empty(), cs))
       else
+        assert Digits(cs).t.Empty? ==> NonEmptyDigits(cs).Failure?;
         var SP(num, cs) :- NonEmptyDigits(cs);
         Success(SP(NonEmpty(JFrac(period, num)), cs))
     }

diff --git a/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Serializer.dfy b/Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Serializer.dfy
@@ -493,7 +493,9 @@ module Std.JSON.ZeroCopy.Serializer {
     for i := 0 to |members| // FIXME uint32
       invariant wr == MembersSpec(obj, members[..i], writer)
     {
-      assert members[..i+1][..i] == members[..i];
+      assert members[..i+1][..i] == members[..i] by {
+        Seq.TakeLess(members, i, i + 1);
+      }
       wr := Member(obj, members[i], wr);
     }
     assert members[..|members|] == members;