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

src/JSON/Deserializer.dfy

@@ -6,7 +6,6 @@
 
 include "../Collections/Sequences/Seq.dfy"
 include "../BoundedInts.dfy"
-include "Utils/Math.dfy"
 
 include "Utils/Views.dfy"
 include "Utils/Vectors.dfy"
@@ -18,10 +17,11 @@ include "Spec.dfy"
 
 module {:options "-functionSyntax:4"} JSON.Deserializer {
   import Seq
-  import Utils.Math
 
   import opened Wrappers
   import opened BoundedInts
+  import opened Logarithm
+  import opened Power
   import opened Utils.Str
   import Utils.Unicode
 
@@ -56,7 +56,7 @@ module {:options "-functionSyntax:4"} JSON.Deserializer {
             else
               var tl :- Unescape(str, start + 6);
               var hd := Str.ToNat(code, 16);
-              assert hd < 0x10000 by { reveal Math.IntPow(); }
+              assert hd < 0x10000 by { reveal Pow(); }
               Success([hd as char] + tl)
         else
           var unescaped: uint16 := match c
@@ -118,7 +118,7 @@ module {:options "-functionSyntax:4"} JSON.Deserializer {
       case NonEmpty(JFrac(_, num)) =>
         var pow10 := num.Length() as int;
         var frac :- ToInt(minus, num);
-        Success(AST.Decimal(n * Math.IntPow(10, pow10) + frac, e10 - pow10))
+        Success(AST.Decimal(n * Pow(10, pow10) + frac, e10 - pow10))
   }
 
   function KV(js: Grammar.jkv): DeserializationResult<(string, AST.JSON)> {

src/JSON/README.md

@@ -55,8 +55,6 @@ Most of the contents of the `Utils/` directory are not specific to JSON.  They a
 
 - [`Str.dfy`](Utils/Str.dfy) implements functions to convert between (big-endian) strings and numbers.  This module shares similarities with [LittleEndianNat.dfy](../Collections/Sequences/LittleEndianNat.dfy) (except for the digit order), although `LittleEndianNat.dfy` makes the base a module parameter instead of a function argument.
 
-- [`Math.dfy`](Utils/Math.dfy) implements `IntPow` and its left inverse `IntLog`.  These functions are used to characterize the length of strings produced from numbers and the value of numbers produced from strings.  They could be migrated to [`NonlinearArithmetic/Power.dfy`](../NonlinearArithmetic/Power.dfy), but the `Nonlinear` part of the library uses custom Dafny flags for arithmetic and Dafny does not (yet) support specifying these flags per-module.
-
 - [`Parsers.dfy`](Utils/Parsers.dfy) has definitions of well-formedness for parsers (stating that they must consume part of their input).  This file would have to be significantly expanded to create a composable library of parsing combinators to be useful as part of the main library.
 
 ## Caveats

src/JSON/Spec.dfy

@@ -6,6 +6,7 @@
 /// ``JSON.Serializer.dfy``.
 
 include "../BoundedInts.dfy"
+include "../NonlinearArithmetic/Logarithm.dfy"
 
 include "AST.dfy"
 include "Utils/Unicode.dfy"
@@ -17,17 +18,18 @@ module {:options "-functionSyntax:4"} JSON.Spec {
   import opened Utils.Str
   import opened AST
   import opened Utils.Unicode
+  import opened Logarithm
 
   type bytes = seq<uint8>
 
   function EscapeUnicode(c: uint16): string {
     var s := Str.OfNat(c as nat, 16);
     assert |s| <= 4 by {
       assert c as nat <= 0xFFFF;
-      assert Math.IntLog(16, c as nat) <= Math.IntLog(16, 0xFFFF) by {
-        Math.IntLog_Increasing(16, c as nat, 0xFFFF);
+      assert Log(16, c as nat) <= Log(16, 0xFFFF) by {
+        LemmaLogIsOrdered(16, c as nat, 0xFFFF);
       }
-      assert Math.IntLog(16, 0xFFFF) == 3 by { reveal Math.IntLog(); }
+      assert Log(16, 0xFFFF) == 3 by { reveal Log(); }
     }
     s + seq(4 - |s|, _ => ' ')
   }

src/JSON/Utils/Str.dfy

@@ -1,14 +1,23 @@
+// RUN: %dafny /compile:0 /noNLarith "%s"
+
 include "../../BoundedInts.dfy"
 include "../../Wrappers.dfy"
-include "Math.dfy"
+include "../../NonlinearArithmetic/Mul.dfy"
+include "../../NonlinearArithmetic/DivMod.dfy"
+include "../../NonlinearArithmetic/Logarithm.dfy"
+include "../../NonlinearArithmetic/Power.dfy"
 
 module {:options "-functionSyntax:4"} JSON.Utils.Str {
   import opened Wrappers
-  import Math
+  import opened Power
+  import opened Logarithm
 
   abstract module ParametricConversion {
     import opened Wrappers
-    import Math
+    import opened Mul
+    import opened DivMod
+    import opened Power
+    import opened Logarithm
 
     type Char(==)
     type String = seq<Char>
@@ -19,24 +28,24 @@ module {:options "-functionSyntax:4"} JSON.Utils.Str {
       requires base > 1
       decreases n
       ensures n == 0 ==> |digits| == 0
-      ensures n > 0 ==> |digits| == Math.IntLog(base, n) + 1
+      ensures n > 0 ==> |digits| == Log(base, n) + 1
       ensures forall d | d in digits :: 0 <= d < base
     {
       if n == 0 then
-        assert Math.IntPow(base, 0) == 1 by { reveal Math.IntPow(); }
+        assert Pow(base, 0) == 1 by { reveal Pow(); }
         []
       else
-        assert n < base * n;
-        assert n / base < n;
+        LemmaDivPosIsPosAuto(); LemmaDivDecreasesAuto();
         var digits' := Digits(n / base, base);
         var digits := digits' + [n % base];
-        assert |digits| == Math.IntLog(base, n) + 1 by {
+        assert |digits| == Log(base, n) + 1 by {
+          assert |digits| == |digits'| + 1;
           if n < base {
-            assert |digits| == 1;
-            assert Math.IntLog(base, n) == 0 by { reveal Math.IntLog(); }
+            LemmaLog0(base, n);
+            assert n / base == 0 by { LemmaBasicDiv(base); }
           } else {
-            assert |digits'| == |digits| - 1;
-            assert Math.IntLog(base, n) == Math.IntLog(base, n / base) + 1 by { reveal Math.IntLog(); }
+            LemmaLogS(base, n);
+            assert n / base > 0 by { LemmaDivNonZeroAuto(); }
           }
         }
         digits
@@ -56,11 +65,11 @@ module {:options "-functionSyntax:4"} JSON.Utils.Str {
 
     function OfNat_any(n: nat, chars: seq<Char>) : (str: String)
       requires |chars| > 1
-      ensures |str| == Math.IntLog(|chars|, n) + 1
+      ensures |str| == Log(|chars|, n) + 1
       ensures forall c | c in str :: c in chars
     {
       var base := |chars|;
-      if n == 0 then reveal Math.IntLog(); [chars[0]]
+      if n == 0 then reveal Log(); [chars[0]]
       else OfDigits(Digits(n, base), chars)
     }
 
@@ -89,24 +98,31 @@ module {:options "-functionSyntax:4"} JSON.Utils.Str {
       requires forall c | c in str :: c in digits
     {
       if str == [] then 0
-      else ToNat_any(str[..|str| - 1], base, digits) * base + digits[str[|str| - 1]]
+      else
+        LemmaMulNonnegativeAuto();
+        ToNat_any(str[..|str| - 1], base, digits) * base + digits[str[|str| - 1]]
     }
 
     lemma {:induction false} ToNat_bound(str: String, base: nat, digits: map<Char, nat>)
       requires base > 0
       requires forall c | c in str :: c in digits
       requires forall c | c in str :: digits[c] < base
-      ensures ToNat_any(str, base, digits) < Math.IntPow(base, |str|)
+      ensures ToNat_any(str, base, digits) < Pow(base, |str|)
     {
-      reveal Math.IntPow();
       if str == [] {
+        reveal Pow();
       } else {
         calc <= {
           ToNat_any(str, base, digits);
           ToNat_any(str[..|str| - 1], base, digits) * base + digits[str[|str| - 1]];
-          { ToNat_bound(str[..|str| - 1], base, digits); }
-          (Math.IntPow(base, |str| - 1) - 1) * base + base - 1;
-          Math.IntPow(base, |str| - 1) * base - 1;
+          ToNat_any(str[..|str| - 1], base, digits) * base + (base - 1);
+          { ToNat_bound(str[..|str| - 1], base, digits);
+            LemmaMulInequalityAuto(); }
+            (Pow(base, |str| - 1) - 1) * base + base - 1;
+          { LemmaMulIsDistributiveAuto(); }
+          Pow(base, |str| - 1) * base - 1;
+          { reveal Pow(); LemmaMulIsCommutativeAuto(); }
+          Pow(base, |str|) - 1;
         }
       }
     }
@@ -178,7 +194,7 @@ module {:options "-functionSyntax:4"} JSON.Utils.Str {
 
   function OfNat(n: nat, base: int := 10) : (str: string)
     requires 2 <= base <= 16
-    ensures |str| == Math.IntLog(base, n) + 1
+    ensures |str| == Log(base, n) + 1
     ensures forall c | c in str :: c in HEX_DIGITS[..base]
   {
     CharStrConversion.OfNat_any(n, HEX_DIGITS[..base])
@@ -194,7 +210,7 @@ module {:options "-functionSyntax:4"} JSON.Utils.Str {
   function ToNat(str: string, base: int := 10) : (n: nat)
     requires 2 <= base <= 16
     requires forall c | c in str :: c in HEX_TABLE && HEX_TABLE[c] as int < base
-    ensures n < Math.IntPow(base, |str|)
+    ensures n < Pow(base, |str|)
   {
     CharStrConversion.ToNat_bound(str, base, HEX_TABLE);
     CharStrConversion.ToNat_any(str, base, HEX_TABLE)

src/NonlinearArithmetic/DivMod.dfy

@@ -111,6 +111,22 @@ module DivMod {
     }
   }
 
+  lemma LemmaDivNonZero(x: int, d: int)
+    requires x >= d > 0
+    ensures x / d > 0
+  {
+    LemmaDivPosIsPosAuto();
+    if x / d == 0 {
+      LemmaSmallDivConverseAuto();
+    }
+  }
+
+  lemma LemmaDivNonZeroAuto()
+    ensures forall x, d {:trigger x / d } | x >= d > 0 :: x / d > 0
+  {
+    forall x, d | x >= d > 0 { LemmaDivNonZero(x, d); }
+  }
+
   /* given two fractions with the same numerator, the order of numbers is determined by 
   the denominators. However, if the numerator is 0, the fractions are equal regardless of 
   the denominators' values */