diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo index 9d33f712f29..815f253050b 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo index 58789cb25e6..245f678b573 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo index a58887ff468..6059092c78f 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo index 01ceb428541..48df0950419 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo index e8d767a1a4d..f320bf2c8ec 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo index 54b0913b674..a6de78d0e2b 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo index 7f39906f9ef..1044b550116 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo differ diff --git a/Source/DafnyStandardLibraries/src/Std/JSON/ByteStrConversion.dfy b/Source/DafnyStandardLibraries/src/Std/JSON/ByteStrConversion.dfy index 05ed37a44dd..a9dc9bc2676 100644 --- a/Source/DafnyStandardLibraries/src/Std/JSON/ByteStrConversion.dfy +++ b/Source/DafnyStandardLibraries/src/Std/JSON/ByteStrConversion.dfy @@ -22,4 +22,8 @@ module {:disableNonlinearArithmetic} Std.JSON.ByteStrConversion refines Strings. '4' as byte := 4, '5' as byte := 5, '6' as byte := 6, '7' as byte := 7, '8' as byte := 8, '9' as byte := 9 ] + + lemma CharsConsistent() + ensures forall c <- chars :: c in charToDigit && chars[charToDigit[c]] == c + {} } \ No newline at end of file diff --git a/Source/DafnyStandardLibraries/src/Std/JSON/Deserializer.dfy b/Source/DafnyStandardLibraries/src/Std/JSON/Deserializer.dfy index ced3e61bd0c..dd3641eb7f9 100644 --- a/Source/DafnyStandardLibraries/src/Std/JSON/Deserializer.dfy +++ b/Source/DafnyStandardLibraries/src/Std/JSON/Deserializer.dfy @@ -50,6 +50,10 @@ module Std.JSON.Deserializer { 'a' as uint16 := 0xA, 'b' as uint16 := 0xB, 'c' as uint16 := 0xC, 'd' as uint16 := 0xD, 'e' as uint16 := 0xE, 'f' as uint16 := 0xF, 'A' as uint16 := 0xA, 'B' as uint16 := 0xB, 'C' as uint16 := 0xC, 'D' as uint16 := 0xD, 'E' as uint16 := 0xE, 'F' as uint16 := 0xF ] + + // The size of the map makes this impractical to verify easily. + lemma {:axiom} CharsConsistent() + ensures forall c <- chars :: c in charToDigit && chars[charToDigit[c]] == c } const HEX_TABLE_16 := Uint16StrConversion.charToDigit diff --git a/Source/DafnyStandardLibraries/src/Std/JSON/Spec.dfy b/Source/DafnyStandardLibraries/src/Std/JSON/Spec.dfy index 9b1be70bba7..7183a4bb2e6 100644 --- a/Source/DafnyStandardLibraries/src/Std/JSON/Spec.dfy +++ b/Source/DafnyStandardLibraries/src/Std/JSON/Spec.dfy @@ -74,7 +74,7 @@ module Std.JSON.Spec { if i == 0 { } else { var isHexDigit := c => c in Strings.HexConversion.HEX_DIGITS; - assert Strings.HexConversion.OfNumberStr(s, '-'); + assert Strings.HexConversion.IsNumberStr(s, '-'); assert isHexDigit(s[i]); } } diff --git a/Source/DafnyStandardLibraries/src/Std/Strings.dfy b/Source/DafnyStandardLibraries/src/Std/Strings.dfy index f479eb2d430..a9acc6b46f0 100644 --- a/Source/DafnyStandardLibraries/src/Std/Strings.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Strings.dfy @@ -11,7 +11,7 @@ module {:disableNonlinearArithmetic} Std.Strings { Refine this module to use it. The refinee must define: - the type of character used, Char - - a conversion from nat to Char and vice versa + - a conversion from nat to Char (the chars sequences) and vice versa (charToDigit) */ abstract module {:disableNonlinearArithmetic} ParametricConversion refines Arithmetic.LittleEndianNat { import opened Wrappers @@ -20,16 +20,25 @@ module {:disableNonlinearArithmetic} Std.Strings { type String = seq type CharSeq = chars: seq | |chars| > 1 witness * + // Canoncial digit characters: converting to strings will uses these characters. const chars: CharSeq const base := |chars| + // All recognized digit characters: converting from strings will use this map, + // which may associate multiple characters with the same digit. const charToDigit: map + lemma CharsConsistent() + ensures forall c <- chars :: c in charToDigit && chars[charToDigit[c]] == c + function BASE(): nat { base } + predicate IsDigitChar(c: Char) { + c in charToDigit + } + function OfDigits(digits: seq) : (str: String) - requires forall d | d in digits :: 0 <= d < base ensures forall c <- str :: c in chars ensures |str| == |digits| { @@ -51,16 +60,10 @@ module {:disableNonlinearArithmetic} Std.Strings { else LemmaFromNatLen2(n); OfDigits(FromNat(n)) } - predicate OfNumberStr(str: String, minus: Char) { - str != [] ==> - && (str[0] == minus || str[0] in chars) - && forall c <- str[1..] :: c in chars - } - - predicate ToNumberStr(str: String, minus: Char) { + predicate IsNumberStr(str: String, minus: Char) { str != [] ==> && (str[0] == minus || str[0] in charToDigit) - && forall c <- str[1..] :: c in charToDigit + && forall c <- str[1..] :: IsDigitChar(c) } /* @@ -68,8 +71,9 @@ module {:disableNonlinearArithmetic} Std.Strings { given a particular minus character. */ function OfInt(n: int, minus: Char) : (str: String) - ensures OfNumberStr(str, minus) + ensures IsNumberStr(str, minus) { + CharsConsistent(); if n >= 0 then OfNat(n) else [minus] + OfNat(-n) } @@ -78,18 +82,19 @@ module {:disableNonlinearArithmetic} Std.Strings { Convert a String that represents a natural number, back into that number. */ function {:vcs_split_on_every_assert} ToNat(str: String) : (n: nat) - requires forall c <- str :: c in charToDigit + requires forall c <- str :: IsDigitChar(c) { if str == [] then 0 else LemmaMulNonnegativeAuto(); - ToNat(str[..|str| - 1]) * base + charToDigit[str[|str| - 1]] + var c := str[|str| - 1]; + assert IsDigitChar(c); + ToNat(str[..|str| - 1]) * base + charToDigit[c] } lemma {:induction false} ToNatBound(str: String) requires base > 0 - requires forall c <- str :: c in charToDigit - requires forall c <- str :: charToDigit[c] < base + requires forall c <- str :: IsDigitChar(c) ensures ToNat(str) < Pow(base, |str|) { if str == [] { @@ -97,6 +102,7 @@ module {:disableNonlinearArithmetic} Std.Strings { } else { calc <= { ToNat(str); + { assert IsDigitChar(str[|str| - 1]); } ToNat(str[..|str| - 1]) * base + charToDigit[str[|str| - 1]]; ToNat(str[..|str| - 1]) * base + (base - 1); { ToNatBound(str[..|str| - 1]); @@ -115,7 +121,7 @@ module {:disableNonlinearArithmetic} Std.Strings { */ function ToInt(str: String, minus: Char): (s: int) requires str != [minus] - requires ToNumberStr(str, minus) + requires IsNumberStr(str, minus) { if [minus] <= str then -(ToNat(str[1..]) as int) else @@ -172,6 +178,9 @@ module {:disableNonlinearArithmetic} Std.Strings { 'a' := 0xA, 'b' := 0xB, 'c' := 0xC, 'd' := 0xD, 'e' := 0xE, 'f' := 0xF, 'A' := 0xA, 'B' := 0xB, 'C' := 0xC, 'D' := 0xD, 'E' := 0xE, 'F' := 0xF ] + // The size of the map makes this impractical to verify easily. + lemma {:axiom} CharsConsistent() + ensures forall c <- chars :: c in charToDigit && chars[charToDigit[c]] == c } module {:disableNonlinearArithmetic} DecimalConversion refines ParametricConversion { @@ -182,6 +191,9 @@ module {:disableNonlinearArithmetic} Std.Strings { map[ '0' := 0, '1' := 1, '2' := 2, '3' := 3, '4' := 4, '5' := 5, '6' := 6, '7' := 7, '8' := 8, '9' := 9 ] + lemma CharsConsistent() + ensures forall c <- chars :: c in charToDigit && chars[charToDigit[c]] == c + {} } module CharStrEscaping refines ParametricEscaping { @@ -202,7 +214,7 @@ module {:disableNonlinearArithmetic} Std.Strings { Convert an integer into its String representation for a decimal number system */ function OfInt(n: int) : (str: string) - ensures DecimalConversion.OfNumberStr(str, '-') + ensures DecimalConversion.IsNumberStr(str, '-') { DecimalConversion.OfInt(n, '-') } @@ -211,7 +223,7 @@ module {:disableNonlinearArithmetic} Std.Strings { Given a natural number represented as a decimal number in a String, back into an integer */ function ToNat(str: string) : (n: nat) - requires forall c <- str :: c in DecimalConversion.charToDigit && DecimalConversion.charToDigit[c] as int < DecimalConversion.base + requires forall c <- str :: DecimalConversion.IsDigitChar(c) ensures n < Pow(DecimalConversion.base, |str|) { DecimalConversion.ToNatBound(str); @@ -223,7 +235,7 @@ module {:disableNonlinearArithmetic} Std.Strings { */ function ToInt(str: string) : (n: int) requires str != "-" - requires DecimalConversion.ToNumberStr(str, '-') + requires DecimalConversion.IsNumberStr(str, '-') { DecimalConversion.ToInt(str, '-') }