From 04b3ec57dc0acffce2c508aa1a4a4fb899a895af Mon Sep 17 00:00:00 2001 From: David Cok Date: Mon, 20 Feb 2023 18:47:54 -0500 Subject: [PATCH] Updating the original files in libraries to Dafny 4 (#2) (#97) Also applies dafny format and changes the lit commands to use the new CLI. Co-authored-by: Robin Salkeld --- .github/workflows/check-format | 9 + .github/workflows/check-format.yml | 38 ++ .github/workflows/tests.yml | 50 +- .gitignore | 7 + README-TESTING.md | 32 ++ Scripts/pydiff.py | 99 ++++ Scripts/test-exit.py | 33 ++ examples/Collections/Arrays/BinarySearch.dfy | 12 +- examples/FileIO/ReadBytesFromFile.dfy | 18 +- examples/FileIO/WriteBytesToFile.dfy | 20 +- .../LittleEndianNatCustomExample.dfy | 16 +- .../LittleEndianNatExample.dfy | 8 +- examples/Relations.dfy | 14 +- examples/Unicode/UnicodeExamples.dfy | 8 +- .../Unicode/Utf16EncodingFormExamples.dfy | 12 +- examples/Unicode/Utf8EncodingFormExamples.dfy | 12 +- examples/Wrappers.dfy | 12 +- lit.site.cfg | 183 +++---- src/BoundedInts.dfy | 4 +- src/Collections/Arrays/BinarySearch.dfy | 12 +- src/Collections/Maps/Imaps.dfy | 18 +- src/Collections/Maps/Maps.dfy | 16 +- src/Collections/Sequences/LittleEndianNat.dfy | 170 +++---- .../Sequences/LittleEndianNatConversions.dfy | 54 +-- src/Collections/Sequences/MergeSort.dfy | 10 +- src/Collections/Sequences/Seq.dfy | 160 +++---- src/Collections/Sets/Isets.dfy | 24 +- src/Collections/Sets/Sets.dfy | 24 +- src/FileIO/FileIO.dfy | 56 +-- src/Functions.dfy | 24 +- src/Math.dfy | 12 +- src/NonlinearArithmetic/DivMod.dfy | 452 +++++++++--------- .../Internals/DivInternals.dfy | 50 +- .../Internals/DivInternalsNonlinear.dfy | 26 +- .../Internals/GeneralInternals.dfy | 20 +- .../Internals/ModInternals.dfy | 50 +- .../Internals/ModInternalsNonlinear.dfy | 18 +- .../Internals/MulInternals.dfy | 28 +- .../Internals/MulInternalsNonlinear.dfy | 16 +- src/NonlinearArithmetic/Mul.dfy | 64 +-- src/NonlinearArithmetic/Power.dfy | 154 +++--- src/NonlinearArithmetic/Power2.dfy | 22 +- src/Relations.dfy | 22 +- src/Unicode/Unicode.dfy | 28 +- src/Unicode/UnicodeEncodingForm.dfy | 154 +++--- src/Unicode/Utf16EncodingForm.dfy | 26 +- src/Unicode/Utf8EncodingForm.dfy | 76 +-- src/Unicode/Utf8EncodingScheme.dfy | 56 +-- src/Wrappers.dfy | 16 +- 49 files changed, 1346 insertions(+), 1099 deletions(-) create mode 100755 .github/workflows/check-format create mode 100644 .github/workflows/check-format.yml create mode 100644 README-TESTING.md create mode 100755 Scripts/pydiff.py create mode 100755 Scripts/test-exit.py diff --git a/.github/workflows/check-format b/.github/workflows/check-format new file mode 100755 index 00000000..1929d3f9 --- /dev/null +++ b/.github/workflows/check-format @@ -0,0 +1,9 @@ +#! /usr/bin/env bash + +FAIL=0 +for f in `find $1 -name '*.dfy'`; do \ + echo $f ;\ + dafny format --check $f || ( dafny format --print $f | diff $f - ) ;\ + if [ "$?" != 0 ] ; then FAIL=1 ; fi; \ +done +exit $FAIL diff --git a/.github/workflows/check-format.yml b/.github/workflows/check-format.yml new file mode 100644 index 00000000..9b59fdc0 --- /dev/null +++ b/.github/workflows/check-format.yml @@ -0,0 +1,38 @@ +# This workflow does static verification of the legacy modules +name: Check formatting + +on: + workflow_dispatch: + pull_request: + branches: [ master ] + +jobs: + formatting: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v3 + + - name: switch branch + run: | + git fetch + git checkout cok-code + + - name: Install Dafny + uses: dafny-lang/setup-dafny-action@v1 + with: + dafny-version: "nightly-2023-02-15-567a5ba" + + - name: Install lit + run: pip install lit OutputCheck + + - name: Set up JS dependencies + run: npm install bignumber.js + + - name: Check exe + run: | + dafny --version + + - name: Check formatting + run: | + chmod +x ./.github/workflows/check-format + ./.github/workflows/check-format src diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 18ec49db..c944f0b9 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -1,23 +1,42 @@ -# This workflow performs static analysis checks. -name: tests +# This workflow does static verification of the DafnyCore library +name: Dafny Core verification on: + # Scheduled to be run sometime after the nightly build of dafny + schedule: + - cron: "7 10 * * *" workflow_dispatch: - push: - branches: [ master ] pull_request: branches: [ master ] jobs: verification: - runs-on: ubuntu-latest + continue-on-error: true + strategy: + fail-fast: false + matrix: + # nightly-latest to catch anything that breaks these tests in current development + # 2/18/2023 version is the first that supports logging + # 3.11.0 supports new CLI but does not support logging + version: [ nightly-latest, nightly-2023-02-18-ef4f346, 3.11.0] + os: [ ubuntu-latest ] + + runs-on: ${{ matrix.os }} steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v3 - name: Install Dafny - uses: dafny-lang/setup-dafny-action@v1 + uses: dafny-lang/setup-dafny-action@v1.6.0 with: - dafny-version: "3.9.1" + dafny-version: ${{ matrix.version }} + + - name: Version information + run: | + dafny --version + echo ${{ matrix.os }} ${{ runner.os }} ${{ matrix.version }} + + - name: Upgrade outdated pip + run: python -m pip install --upgrade pip - name: Install lit run: pip install lit OutputCheck @@ -25,14 +44,23 @@ jobs: - name: Set up JS dependencies run: npm install bignumber.js - - name: Verify Dafny Code - run: lit --time-tests -v --param 'dafny_params=/verificationLogger:trx /verificationLogger:csv' . + - name: Verify Code and Examples without logging + id: nolog + if: matrix.version == '3.11.0' + run: lit --time-tests -v . + + - name: Verify Code and Examples + id: withlog + if: steps.nolog.conclusion == 'skipped' + run: | + lit --time-tests -v --param 'dafny_params=--log-format trx --log-format csv' . - name: Generate Report + if: always() && steps.withlog.conclusion != 'skipped' run: find . -name '*.csv' -print0 | xargs -0 --verbose dafny-reportgenerator summarize-csv-results --max-duration-seconds 10 - uses: actions/upload-artifact@v2 # upload test results - if: success() || failure() # run this step even if previous step failed + if: always() && steps.withlog.conclusion != 'skipped' with: name: verification-results path: '**/TestResults/*.trx' diff --git a/.gitignore b/.gitignore index 05c99deb..b5a6561e 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,9 @@ +**/.DS_Store **/Output/ **/TestResults/ +examples/FileIO/ReadBytesFromFile.cs +examples/FileIO/ReadBytesFromFile.jar +examples/FileIO/ReadBytesFromFile.js +examples/FileIO/WriteBytesToFile.cs +examples/FileIO/WriteBytesToFile.jar +examples/FileIO/WriteBytesToFile.js diff --git a/README-TESTING.md b/README-TESTING.md new file mode 100644 index 00000000..dd08ec90 --- /dev/null +++ b/README-TESTING.md @@ -0,0 +1,32 @@ +# Testing the libraries + +The code in these libraries is tested both with deductive verification, using dafny, +and with traditional runtime testing of compilations by dafny. +The latter is important as a check that dafny compiled the (verified) dafny code correctly. +Also, some functionality (e.g. FileIO) is partially implemented using +custom code in the target programming language, which is not verified by dafny. +All files are also checked that they conform to standard dafny formatting, +using `dafny format`. + +The tests are run using `lit`. The configuration of the tests is controlled by +(a) the lit.site.cfg file and (b) the yml files in .github/workflows. + +The tests are run on each push to a pull_request and are required to pass to enable merging. +They are also run on a nightly schedule. + +To run the files manually: run `lit .` in this directory (`libraries`, at the top +of the clone of the repo). You can also manually run individual files or directories, +but `lit` must be invoked in the `libraries` directory. You can also trigger the workflow +using `workflow_dispatch`. To do a manual check of formatting, use `dafny format --check `. + +The tests themselves are specially formatted lines (those beginning with `// RUN:`) in +each .dfy file. The tests use dafny's new command-line syntax, using the lit +macros `%verify` and `%run` and the like. + +The versions of dafny being run are set in the `tests.yml` file. The versions tested +must be recent enough to support the new CLI syntax, so 3.11ff. Also, if +verification logging is desired, the version must be at least that of 3/18/2023 when +the logging parameters were implemented in the new CLI. + +Testing can be run on older versions if (a) the lit macros like `%verify` are redefined using +old CLI syntax and (b) the runtime testing tests are rewritten to not use `dafny run`. diff --git a/Scripts/pydiff.py b/Scripts/pydiff.py new file mode 100755 index 00000000..f98ce5a4 --- /dev/null +++ b/Scripts/pydiff.py @@ -0,0 +1,99 @@ +#!/usr/bin/env python +""" +Simple driver around python's difflib that implements a basic ``diff`` like +tool. This exists to provide a simple ``diff`` like tool that will run on +Windows where only the ``fc`` tool is available. +""" +import argparse +import difflib +import os +import sys + +def main(args): + parser = argparse.ArgumentParser(formatter_class=argparse.RawDescriptionHelpFormatter, + description=__doc__ + ) + # Open in binary mode so python doesn't try and do + # universal line endings for us. + parser.add_argument('from-file', + type=argparse.FileType('rb'), + ) + parser.add_argument('to-file', + type=argparse.FileType('rb'), + ) + parser.add_argument('-U','--unified=', + type=int, + default=3, + help='Number of context lines to show. ' + 'Default %(default)s' + ) + parser.add_argument('--strip-trailing-cr', + action='store_true', + help='strip trailing carriage return when comparing' + ) + parser.add_argument('--ignore-all-space','-w', + action='store_true', + help='Ignore all whitespace characters when comparing' + ) + + parsedArgs = parser.parse_args(args) + fromFile, fromFileName = preProcess(getattr(parsedArgs,'from-file'), + parsedArgs.strip_trailing_cr, + parsedArgs.ignore_all_space + ) + toFile, toFileName = preProcess(getattr(parsedArgs,'to-file'), + parsedArgs.strip_trailing_cr, + parsedArgs.ignore_all_space + ) + result = difflib.unified_diff(fromFile, + toFile, + fromFileName, + toFileName, + n=getattr(parsedArgs,'unified='), + ) + # Force lazy computation to happen now + result = list(result) + + if len(result) == 0: + # Files are identical + return 0 + else: + for l in result: + sys.stdout.write(l) + return 1 + +def preProcess(openFile, stripTrailingCR=False, ignoreAllSpace=False): + """ + Helper function to read lines in a file and do any necessary + pre-processing + """ + original = openFile.readlines() + + # Translation table deletes white space characters Note we don't remove + # newline characters because this will create a mess when outputting the + # diff. Is this the right behaviour? + deleteChars=' \t' + if sys.version_info.major >= 3: + translationTable = str.maketrans('','', deleteChars) + + copy = [ ] + for line in original: + newLine = str(line.decode()) + + if stripTrailingCR: + if newLine[-2:] == '\r\n' or newLine[-2:] == '\n\r': + newLine = newLine[:-2] + '\n' + + if ignoreAllSpace: + newLine = newLine.translate(translationTable) + + copy.append(newLine) + + return (copy, openFile.name) + +def getFileName(openFile): + return openFile.name + +if __name__ == '__main__': + sys.exit(main(sys.argv[1:])) + diff --git a/Scripts/test-exit.py b/Scripts/test-exit.py new file mode 100755 index 00000000..68dba1f7 --- /dev/null +++ b/Scripts/test-exit.py @@ -0,0 +1,33 @@ +## This small script takes as first argument a test indicator +## and the rest of the arguments are a command to run, with its +## command-line arguments. +## The script runs the command and then if the first argument is +## (1) -any -- returns success, ignoring the exit code of the command +## (2) -z -- returns success iff the exit code is non-zero +## (3) some integer literal -- return success iff the exit code +## matches the given integer +## (4) -skip -- does not run the command and just exits with success + +import sys +import subprocess + +arg = sys.argv[1] +if arg == "-skip": + print( 'Skipping' ) + exit(0) + +p = subprocess.run( sys.argv[2:] ) + +if arg == "-any": + exit(0) +if arg == "-z": + if p.returncode == 0 : + print( 'Expected non-zero exit code' ) + exit(1) + else: + exit(0) +if p.returncode != int(arg) : + print( 'Expected exit code', arg, ', actual result is', p.returncode ) + exit(1) + +exit(0) diff --git a/examples/Collections/Arrays/BinarySearch.dfy b/examples/Collections/Arrays/BinarySearch.dfy index 019e6ecb..45b4c5da 100644 --- a/examples/Collections/Arrays/BinarySearch.dfy +++ b/examples/Collections/Arrays/BinarySearch.dfy @@ -1,12 +1,12 @@ -// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %run "%s" > "%t" // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK-L: [-6, 0, 1, 3, 7, 7, 9] // CHECK-NEXT-L: 3 /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../../src/Relations.dfy" include "../../../src/Collections/Arrays/BinarySearch.dfy" @@ -20,14 +20,14 @@ module BinarySearchExamples { import opened Seq.MergeSort import opened Relations - lemma SortedByLessThanOrEqualTo(s: seq) + lemma SortedByLessThanOrEqualTo(s: seq) requires SortedBy(s, (x, y) => x <= y) ensures SortedBy(s, (x, y) => x < y || x == y) {} method {:vcs_split_on_every_assert} SortAndSearch() { var input := [1, 7, 7, 3, 9, 0, -6]; - + var sortedInput := MergeSortBy(input, (x, y) => x <= y); print sortedInput, "\n"; diff --git a/examples/FileIO/ReadBytesFromFile.dfy b/examples/FileIO/ReadBytesFromFile.dfy index 43e9c22a..dd740ec4 100644 --- a/examples/FileIO/ReadBytesFromFile.dfy +++ b/examples/FileIO/ReadBytesFromFile.dfy @@ -1,13 +1,13 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" -// RUN: %baredafny run --no-verify --target:cs "%s" --input "%S/../../src/FileIO/FileIO.cs" -- "%S/data.txt" "System.ArgumentException:" -// RUN: %baredafny run --no-verify --target:java "%s" --input "%S/../../src/FileIO/FileIO.java" -- "%S/data.txt" "java.io.IOException:" -// RUN: %baredafny run --no-verify --target:js "%s" --input "%S/../../src/FileIO/FileIO.js" -- "%S/data.txt" "Error: ENOENT" +// #RUN: %run --no-verify --unicode-char:false --target:cs "%s" --input "%S/../../src/FileIO/FileIO.cs" -- "%S/data.txt" "System.ArgumentException:" +// #RUN: %run --no-verify --unicode-char:false --target:java "%s" --input "%S/../../src/FileIO/FileIO.java" -- "%S/data.txt" "java.io.IOException:" +// #RUN: %run --no-verify --unicode-char:false --target:js "%s" --input "%S/../../src/FileIO/FileIO.js" -- "%S/data.txt" "Error: ENOENT" include "../../src/FileIO/FileIO.dfy" @@ -20,7 +20,7 @@ module ReadBytesFromFile { var dataPath := args[1]; var expectedErrorPrefix := args[2]; - // Happy path: read from the data file, and check that we see the expected content. + // Happy path: read from the data file, and check that we see the expected content. { var expectedStr := "Hello world\nGoodbye\n"; // This conversion is safe only for ASCII values. For Unicode conversions, see the Unicode modules. @@ -33,7 +33,7 @@ module ReadBytesFromFile { expect readBytes == expectedBytes, "read unexpected byte sequence"; } - // Failure path: attempting to read from a blank file path should never work. + // Failure path: attempting to read from a blank file path should never work. { var res := FileIO.ReadBytesFromFile(""); expect res.Failure?, "unexpected success"; diff --git a/examples/FileIO/WriteBytesToFile.dfy b/examples/FileIO/WriteBytesToFile.dfy index a65e2048..63820c88 100644 --- a/examples/FileIO/WriteBytesToFile.dfy +++ b/examples/FileIO/WriteBytesToFile.dfy @@ -1,13 +1,13 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" -// RUN: %baredafny run --no-verify --target:cs "%s" --input "%S/../../src/FileIO/FileIO.cs" -- "%t_cs" "System.ArgumentException:" -// RUN: %baredafny run --no-verify --target:java "%s" --input "%S/../../src/FileIO/FileIO.java" -- "%t_java" "java.nio.file.FileSystemException:" -// RUN: %baredafny run --no-verify --target:js "%s" --input "%S/../../src/FileIO/FileIO.js" -- "%t_js" "Error: ENOENT" +// RUN: %run --no-verify --unicode-char:false --target:cs "%s" --input "%S/../../src/FileIO/FileIO.cs" -- "%t_cs" "System.ArgumentException:" +// RUN: %run --no-verify --unicode-char:false --target:java "%s" --input "%S/../../src/FileIO/FileIO.java" -- "%t_java" "java.nio.file.FileSystemException:" +// RUN: %run --no-verify --unicode-char:false --target:js "%s" --input "%S/../../src/FileIO/FileIO.js" -- "%t_js" "Error: ENOENT" //// Check that written files match expectations // RUN: %diff "%S/data.txt" "%t_cs/output_plain" @@ -31,7 +31,7 @@ module WriteBytesToFile { var outputDir := args[1]; var expectedErrorPrefix := args[2]; - // Happy paths: write files to the output dir. (The %diff LIT commands check that we wrote the correct content.) + // Happy paths: write files to the output dir. (The %diff LIT commands check that we wrote the correct content.) { // Ideally we would define `str` as a constant and compute `bytes` automatically. // To do so, we would need to convert each `char` in `str` to a `bv8` value, by using `as bv8`. @@ -47,7 +47,7 @@ module WriteBytesToFile { ]; assert forall i | 0 <= i < |bytes| :: bytes[i] as int == str[i] as int; - // Write directly into the output directory + // Write directly into the output directory { var res := FileIO.WriteBytesToFile(outputDir + "/output_plain", bytes); expect res.Success?, "unexpected failure writing to output_plain: " + res.error; @@ -64,7 +64,7 @@ module WriteBytesToFile { } } - // Failure path: attempting to write to a blank file path should never work. + // Failure path: attempting to write to a blank file path should never work. { var res := FileIO.WriteBytesToFile("", []); expect res.Failure?, "unexpected success"; diff --git a/examples/LittleEndianNat/LittleEndianNatCustomExample.dfy b/examples/LittleEndianNat/LittleEndianNatCustomExample.dfy index c60e7020..332cf21e 100644 --- a/examples/LittleEndianNat/LittleEndianNatCustomExample.dfy +++ b/examples/LittleEndianNat/LittleEndianNatCustomExample.dfy @@ -1,27 +1,27 @@ -// RUN: %dafny /compile:3 /noNLarith "%s" +// RUN: %run --disable-nonlinear-arithmetic "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../src/Collections/Sequences/LittleEndianNatConversions.dfy" -module Uint3_6 refines LittleEndianNatConversions { +module {:options "--function-syntax:4"} Uint3_6 refines LittleEndianNatConversions { module Uint3Seq refines SmallSeq { - function method BITS(): nat { 3 } + function BITS(): nat { 3 } } module Uint6Seq refines LargeSeq { import Small = Uint3Seq - function method BITS(): nat { 6 } + function BITS(): nat { 6 } } import opened Large = Uint6Seq import Small = Large.Small } -module LittleEndianNatCustomExample { +module {:options "--function-syntax:4"} LittleEndianNatCustomExample { import opened Uint3_6 diff --git a/examples/LittleEndianNat/LittleEndianNatExample.dfy b/examples/LittleEndianNat/LittleEndianNatExample.dfy index 232bda48..76dfa91f 100644 --- a/examples/LittleEndianNat/LittleEndianNatExample.dfy +++ b/examples/LittleEndianNat/LittleEndianNatExample.dfy @@ -1,9 +1,9 @@ -// RUN: %dafny /compile:3 /noNLarith "%s" +// RUN: %run --disable-nonlinear-arithmetic "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../src/Collections/Sequences/LittleEndianNatConversions.dfy" diff --git a/examples/Relations.dfy b/examples/Relations.dfy index a9560ab6..a44f098f 100644 --- a/examples/Relations.dfy +++ b/examples/Relations.dfy @@ -1,9 +1,9 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../src/Relations.dfy" @@ -11,11 +11,11 @@ module RelationsExamples { import opened Relations - lemma BuiltInIntLTIsStrictTotalOrdering() + lemma BuiltInIntLTIsStrictTotalOrdering() ensures StrictTotalOrdering((x: int, y: int) => x < y) {} - lemma BuiltInIntLEIsTotalOrdering() + lemma BuiltInIntLEIsTotalOrdering() ensures TotalOrdering((x: int, y: int) => x <= y) {} -} \ No newline at end of file +} diff --git a/examples/Unicode/UnicodeExamples.dfy b/examples/Unicode/UnicodeExamples.dfy index b445da9c..b4e572a7 100644 --- a/examples/Unicode/UnicodeExamples.dfy +++ b/examples/Unicode/UnicodeExamples.dfy @@ -1,9 +1,9 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../src/Unicode/Unicode.dfy" diff --git a/examples/Unicode/Utf16EncodingFormExamples.dfy b/examples/Unicode/Utf16EncodingFormExamples.dfy index a9cb46fe..a54b121d 100644 --- a/examples/Unicode/Utf16EncodingFormExamples.dfy +++ b/examples/Unicode/Utf16EncodingFormExamples.dfy @@ -1,9 +1,9 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../src/Unicode/Utf16EncodingForm.dfy" @@ -20,7 +20,7 @@ module Utf16EncodingFormExamples { lemma TestEncodeScalarValue() ensures forall pair | pair in TEST_SCALAR_VALUES - :: EncodeScalarValue(pair.0) == pair.1 + :: EncodeScalarValue(pair.0) == pair.1 {} // Because surrogate code points are not Unicode scalar values, isolated UTF-16 code units in the range @@ -33,6 +33,6 @@ module Utf16EncodingFormExamples { lemma TestDecodeIllFormedSequence() ensures forall s | s in TEST_ILL_FORMED_SEQUENCES - :: DecodeCodeUnitSequenceChecked(s).None? + :: DecodeCodeUnitSequenceChecked(s).None? {} } diff --git a/examples/Unicode/Utf8EncodingFormExamples.dfy b/examples/Unicode/Utf8EncodingFormExamples.dfy index f3ca0941..2aeda6c0 100644 --- a/examples/Unicode/Utf8EncodingFormExamples.dfy +++ b/examples/Unicode/Utf8EncodingFormExamples.dfy @@ -1,9 +1,9 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../src/Unicode/Utf8EncodingForm.dfy" @@ -24,7 +24,7 @@ module Utf8EncodingFormExamples { lemma TestEncodeScalarValue() ensures forall pair | pair in TEST_SCALAR_VALUES - :: EncodeScalarValue(pair.0) == pair.1 + :: EncodeScalarValue(pair.0) == pair.1 {} // Examples taken from description of Table 3-7. @@ -37,7 +37,7 @@ module Utf8EncodingFormExamples { lemma TestDecodeIllFormedSequence() ensures forall s | s in TEST_ILL_FORMED_SEQUENCES - :: DecodeCodeUnitSequenceChecked(s).None? + :: DecodeCodeUnitSequenceChecked(s).None? {} } diff --git a/examples/Wrappers.dfy b/examples/Wrappers.dfy index f9f5b111..4358bd3b 100644 --- a/examples/Wrappers.dfy +++ b/examples/Wrappers.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %run "%s" > "%t" // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK-L: Hello // CHECK-NEXT-L: Error: 'name' was not found @@ -8,7 +8,7 @@ include "../src/Wrappers.dfy" -module Demo { +module {:options "--function-syntax:4"} Demo { import opened Wrappers // ------ Demo for Option ---------------------------- @@ -20,12 +20,12 @@ module Demo { constructor () { m := map[]; } - function method Get(k: K): Option + function Get(k: K): Option reads this { if k in m then Some(m[k]) else None() } - method Put(k: K, v: V) + method Put(k: K, v: V) modifies this { this.m := this.m[k := v]; @@ -163,13 +163,13 @@ module Demo { // Get a string that we can't reason about statically var contents :- fs.ReadFile(fromPath); - // Dynamically test whether the string is at least 5 characters long, and return a failure if not. + // Dynamically test whether the string is at least 5 characters long, and return a failure if not. // If we pass this line, Dafny can now assume that the string is long enough. :- Need(|contents| >= 5, "File contents not long enough."); // Now we can get the character var c := contents[4]; - + return Success(c); } diff --git a/lit.site.cfg b/lit.site.cfg index 81c355ce..60666266 100644 --- a/lit.site.cfg +++ b/lit.site.cfg @@ -6,13 +6,14 @@ import os import sys import re import platform +import shutil from os import path import lit.util import lit.formats # name: The name of this test suite. -config.name = 'Dafny Standard Libraries' +config.name = 'Dafny Libraries' config.test_format = lit.formats.ShTest(execute_external=False) @@ -33,45 +34,49 @@ config.test_exec_root = config.test_source_root config.environment['MSBUILDSINGLELOADCONTEXT'] = "1" -# Propagate 'HOME' through the environment. -if 'HOME' in os.environ: - config.environment['HOME'] = os.environ['HOME'] +up = os.path.dirname +repositoryRoot = up( + up( os.path.abspath(__file__) ) + ) +lit_config.note('Repository root is {}'.format(repositoryRoot)) -# Propagate 'INCLUDE' through the environment. -if 'INCLUDE' in os.environ: - config.environment['INCLUDE'] = os.environ['INCLUDE'] +PROPAGATE_ENV = [ + 'APPDATA', + 'HOME', + 'INCLUDE', + 'LIB', -# Prevent this issue on windows: https://github.com/dotnet/sdk/issues/8887 -if 'HOMEPATH' in os.environ and 'HOMEDRIVE' in os.environ: - config.environment['DOTNET_CLI_HOME'] = os.environ['HOMEDRIVE'] + os.environ['HOMEPATH'] + # Fixes error on Windows: build cache is required, but could not be located: + # GOCACHE is not defined and %LocalAppData% is not defined + 'LOCALAPPDATA', + + 'NODE_PATH', + + # Fixes NuGet.targets(564,5): error : Value cannot be null. (Parameter 'path1') + 'ProgramFiles', + 'ProgramFiles(x86)', -# Propagate 'LIB' through the environment. -if 'LIB' in os.environ: - config.environment['LIB'] = os.environ['LIB'] + # Prevent dotnet from creating a folder called %SystemDrive% + 'SystemDrive', -if 'USERPROFILE' in os.environ: - config.environment['USERPROFILE'] = os.environ['USERPROFILE'] + 'TEMP', + 'TMP', + 'USERPROFILE', +] -# Propagate the temp directory. Windows requires this because it uses \Windows\ -# if none of these are present. -if 'TMP' in os.environ: - config.environment['TMP'] = os.environ['TMP'] -if 'TEMP' in os.environ: - config.environment['TEMP'] = os.environ['TEMP'] +for var in PROPAGATE_ENV: + if var in os.environ: + config.environment[var] = os.environ[var] + +# Prevent this issue on windows: https://github.com/dotnet/sdk/issues/8887 +if 'HOMEPATH' in os.environ and 'HOMEDRIVE' in os.environ: + config.environment['DOTNET_CLI_HOME'] = os.environ['HOMEDRIVE'] + os.environ['HOMEPATH'] # Propagate PYTHON_EXECUTABLE into the environment config.environment['PYTHON_EXECUTABLE'] = getattr(config, 'python_executable', '') -# Propagate 'NODE_PATH' through the environment. -if 'NODE_PATH' in os.environ: - config.environment['NODE_PATH'] = os.environ['NODE_PATH'] - -# Propagate 'LOCALAPPDATA' into lit's environment -# Fixes error on Windows -# build cache is required, but could not be located: -# GOCACHE is not defined and %LocalAppData% is not defined -if 'LOCALAPPDATA' in os.environ: - config.environment['LOCALAPPDATA'] = os.environ['LOCALAPPDATA'] +# Silence dotnet's welcome message +config.environment['DOTNET_NOLOGO'] = "true" # Check that the object root is known. if config.test_exec_root is None: @@ -91,90 +96,88 @@ def quotePath(path): ### Add Dafny specific substitutions -# Find Dafny.exe -up = os.path.dirname -repositoryRoot = up( - up( os.path.abspath(__file__) ) - ) -lit_config.note('Repository root is {}'.format(repositoryRoot)) - -binaryDir = os.path.join(repositoryRoot, 'Binaries') -config.dafnyBinaryDir = binaryDir -sourceDirectory = os.path.join(repositoryRoot, 'Source') - -defaultDafnyExecutable = 'dotnet run --no-build --project ' + quotePath(os.path.join(sourceDirectory, 'DafnyDriver', 'DafnyDriver.csproj')) -# dafnyExecutable = lit_config.params.get('executable', defaultDafnyExecutable + " --") dafnyExecutable = 'dafny' -defaultServerExecutable = 'dotnet run --no-build --project ' + quotePath(os.path.join(sourceDirectory, 'DafnyServer', 'DafnyServer.csproj')) -# serverExecutable = lit_config.params.get('serverExecutable', defaultServerExecutable) +## defaultServerExecutable = 'dotnet run --no-build --project ' + quotePath(os.path.join(sourceDirectory, 'DafnyServer', 'DafnyServer.csproj')) +## serverExecutable = lit_config.params.get('serverExecutable', defaultServerExecutable) config.suffixes.append('.transcript') -# just the command needed to run dafny, without any additional command line options -# bareDafnyExecutable = dafnyExecutable -bareDafnyExecutable = 'dafny' +ver = "0" +if os.name != "nt": + ver = os.uname().version +newDafnyArgs = [ # We do not want absolute or relative paths in error messages, just the basename of the file -dafnyExecutable += ' -useBaseNameForFileName' +'--use-basename-for-filename', -dafnyExecutable += ' -timeLimit:30' +# Try to verify 2 verification conditions at once +'--cores=2', -# We do not want output such as "Compiled program written to Foo.cs" -# from the compilers, since that changes with the target language -dafnyExecutable += ' -compileVerbose:0' +# Set a default time limit, to catch cases where verification time runs off the rails +'--verification-time-limit=300' +] -# Allow user to provide extra arguments to Dafny -dafnyParams = lit_config.params.get('dafny_params','') -if len(dafnyParams) > 0: - dafnyExecutable = dafnyExecutable + ' ' + dafnyParams +# Add standard parameters +def addParams(cmd): + dafnyParams = lit_config.params.get('dafny_params','') + if len(dafnyParams) > 0: + return f'{cmd} {dafnyParams}' + else: + return cmd -# Inform user what executable is being used -lit_config.note('Using Dafny (%dafny): {}\n'.format(dafnyExecutable)) -lit_config.note('%baredafny will expand to {}\n'.format(bareDafnyExecutable)) +# Add run specific parameters +def buildCmd(args): + if len(args) > 0: + argStr = ' /'.join(args) + return f'{dafnyExecutable} /{argStr}' + else: + return args -ver = "0" -if os.name != "nt": - ver = os.uname().version +standardArguments = addParams(' '.join([])) + +resolveArgs = ' resolve --use-basename-for-filename ' + standardArguments +verifyArgs = ' verify --use-basename-for-filename --cores:2 --verification-time-limit:300 ' + standardArguments +buildArgs = ' build --use-basename-for-filename --cores:2 --verification-time-limit:300 ' + standardArguments +runArgs = ' run --use-basename-for-filename --cores:2 --verification-time-limit:300 ' + standardArguments + +config.substitutions.append( ('%trargs', '--use-basename-for-filename --cores:2 --verification-time-limit:300' ) ) + +config.substitutions.append( ('%resolve', dafnyExecutable + resolveArgs ) ) +config.substitutions.append( ('%verify', dafnyExecutable + verifyArgs ) ) +config.substitutions.append( ('%translate', dafnyExecutable + ' translate' ) ) +config.substitutions.append( ('%build', dafnyExecutable + buildArgs ) ) +config.substitutions.append( ('%run', dafnyExecutable + runArgs ) ) -config.substitutions.append( ('%dafny', dafnyExecutable) ) -config.substitutions.append( ('%baredafny', bareDafnyExecutable) ) +# config.substitutions.append( ('%repositoryRoot', repositoryRoot) ) +# config.substitutions.append( ('%binaryDir', binaryDir) ) +# config.substitutions.append( ('%dafny', dafny) ) +# config.substitutions.append( ('%args', standardArguments) ) +# config.substitutions.append( ('%testDafnyForEachCompiler', testDafnyExecutable) ) +# config.substitutions.append( ('%baredafny', dafnyExecutable) ) # config.substitutions.append( ('%server', serverExecutable) ) +# config.substitutions.append( ('%refmanexamples', os.path.join(repositoryRoot, 'docs', 'DafnyRef', 'examples')) ) config.substitutions.append( ('%os', os.name) ) config.substitutions.append( ('%ver', ver ) ) +config.substitutions.append( ('%sed', 'sed -E' ) ) +config.substitutions.append( ('%exits-with', 'python3 ' + os.path.join(repositoryRoot, 'Scripts/test-exit.py') ) ) +config.substitutions.append( ('!', 'python3 ' + os.path.join(repositoryRoot, 'Scripts/test-exit.py') + " -z" ) ) + if os.name == "nt": config.available_features = [ 'windows' ] elif "Darwin" in ver: config.available_features = [ 'macosx', 'posix' ] -elif "16.04" in ver and "Ubuntu" in ver: - config.available_features = [ 'ubuntu16', 'ubuntu', 'posix' ] +elif "18.04" in ver and "Ubuntu" in ver: + config.available_features = [ 'ubuntu18', 'ubuntu', 'posix' ] else: config.available_features = [ 'ubuntu', 'posix' ] -# Sanity check: Check solver executable is available -# z3Path = None - -# potentialSolverRoots = [path.dirname(bareDafnyExecutable), binaryDir] -# potentialSolverExecutables = ['cvc4.exe', path.join("z3", "bin", "z3"), 'z3.exe', path.join("z3", "bin", "z3.exe")] - -# for root in potentialSolverRoots: -# for executable in potentialSolverExecutables: -# if not z3Path: -# potentialPath = path.join(root, executable) -# if path.exists(potentialPath): -# z3Path = potentialPath - -# if not z3Path: -# lit_config.fatal('Could not find solver') -# config.substitutions.append( ('%z3', z3Path ) ) # Add diff tool substitution commonDiffFlags=' --unified=3 --strip-trailing-cr' diffExecutable = None -if os.name == 'posix': - diffExecutable = lit.util.which('diff') + commonDiffFlags -elif os.name == 'nt': - pydiff = quotePath( os.path.join(config.test_source_root, 'pydiff.py') ) +if os.name == 'posix' or os.name == 'nt': + pydiff = quotePath( os.path.join(config.test_source_root, 'Scripts', 'pydiff.py') ) diffExecutable = sys.executable + ' ' + pydiff + commonDiffFlags else: lit_config.fatal('Unsupported platform') @@ -187,6 +190,6 @@ outputCheckPath = lit.util.which('OutputCheck') if outputCheckPath == None: lit_config.fatal('The OutputCheck tool is not in your PATH. Please install it.') -config.substitutions.append( ('%OutputCheck', outputCheckPath + ' --dump-file-to-check --comment=//') ) +config.substitutions.append( ('%OutputCheck', outputCheckPath + ' --dump-file-to-check --comment=//') ) -config.substitutions.append( ('%{dirsep}', os.sep) ) \ No newline at end of file +config.substitutions.append( ('%{dirsep}', os.sep) ) diff --git a/src/BoundedInts.dfy b/src/BoundedInts.dfy index 6e1d653c..df143075 100644 --- a/src/BoundedInts.dfy +++ b/src/BoundedInts.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" module {:options "-functionSyntax:4"} BoundedInts { const TWO_TO_THE_0: int := 1 @@ -18,7 +18,7 @@ module {:options "-functionSyntax:4"} BoundedInts { const TWO_TO_THE_128: int := 0x1_00000000_00000000_00000000_00000000 const TWO_TO_THE_256: int := 0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000 const TWO_TO_THE_512: int := - 0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000; + 0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000; newtype uint8 = x: int | 0 <= x < TWO_TO_THE_8 newtype uint16 = x: int | 0 <= x < TWO_TO_THE_16 diff --git a/src/Collections/Arrays/BinarySearch.dfy b/src/Collections/Arrays/BinarySearch.dfy index d8bfeb4f..06499a79 100644 --- a/src/Collections/Arrays/BinarySearch.dfy +++ b/src/Collections/Arrays/BinarySearch.dfy @@ -1,9 +1,9 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../Wrappers.dfy" include "../../Relations.dfy" @@ -36,5 +36,5 @@ module BinarySearch { } return None; - } -} \ No newline at end of file + } +} diff --git a/src/Collections/Maps/Imaps.dfy b/src/Collections/Maps/Imaps.dfy index b5da6de7..8e42b87b 100644 --- a/src/Collections/Maps/Imaps.dfy +++ b/src/Collections/Maps/Imaps.dfy @@ -1,13 +1,13 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, -* ETH Zurich, and University of Washington -* SPDX-License-Identifier: BSD-2-Clause -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, + * ETH Zurich, and University of Washington + * SPDX-License-Identifier: BSD-2-Clause + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../Wrappers.dfy" @@ -71,7 +71,7 @@ module {:options "-functionSyntax:4"} Imaps { { forall x, x' {:trigger m[x], m[x']} :: x != x' && x in m && x' in m ==> m[x] != m[x'] } - + /* Swaps imap keys and values. Values are not required to be unique; no promises on which key is chosen on the intersection. */ ghost function {:opaque} Invert(m: imap): imap diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy index f666d8c4..44c7264e 100644 --- a/src/Collections/Maps/Maps.dfy +++ b/src/Collections/Maps/Maps.dfy @@ -1,13 +1,13 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, -* ETH Zurich, and University of Washington -* SPDX-License-Identifier: BSD-2-Clause -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, + * ETH Zurich, and University of Washington + * SPDX-License-Identifier: BSD-2-Clause + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../Wrappers.dfy" diff --git a/src/Collections/Sequences/LittleEndianNat.dfy b/src/Collections/Sequences/LittleEndianNat.dfy index 8e014ed7..f642f872 100644 --- a/src/Collections/Sequences/LittleEndianNat.dfy +++ b/src/Collections/Sequences/LittleEndianNat.dfy @@ -1,12 +1,12 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" +// RUN: %verify --disable-nonlinear-arithmetic "%s" /******************************************************************************* -* Original: Copyright (c) 2020 Secure Foundations Lab -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original: Copyright (c) 2020 Secure Foundations Lab + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ /* Little endian interpretation of a sequence of numbers with a given base. The first element of a sequence is the least significant position; the last @@ -66,33 +66,33 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat { calc { ToNatLeft(xs); Last(xs) * Pow(BASE(), |xs| - 1); - { reveal Pow(); } + { reveal Pow(); } Last(xs); First(xs); - { assert ToNatRight(DropFirst(xs)) == 0; } + { assert ToNatRight(DropFirst(xs)) == 0; } ToNatRight(xs); } } else { calc { ToNatLeft(xs); ToNatLeft(DropLast(xs)) + Last(xs) * Pow(BASE(), |xs| - 1); - { LemmaToNatLeftEqToNatRight(DropLast(xs)); } + { LemmaToNatLeftEqToNatRight(DropLast(xs)); } ToNatRight(DropLast(xs)) + Last(xs) * Pow(BASE(), |xs| - 1); ToNatRight(DropFirst(DropLast(xs))) * BASE() + First(xs) + Last(xs) - * Pow(BASE(), |xs| - 1); - { LemmaToNatLeftEqToNatRight(DropFirst(DropLast(xs))); } + * Pow(BASE(), |xs| - 1); + { LemmaToNatLeftEqToNatRight(DropFirst(DropLast(xs))); } ToNatLeft(DropFirst(DropLast(xs))) * BASE() + First(xs) + Last(xs) - * Pow(BASE(), |xs| - 1); - { - assert DropFirst(DropLast(xs)) == DropLast(DropFirst(xs)); - reveal Pow(); - LemmaMulProperties(); - } + * Pow(BASE(), |xs| - 1); + { + assert DropFirst(DropLast(xs)) == DropLast(DropFirst(xs)); + reveal Pow(); + LemmaMulProperties(); + } ToNatLeft(DropLast(DropFirst(xs))) * BASE() + First(xs) + Last(xs) - * Pow(BASE(), |xs| - 2) * BASE(); - { LemmaMulIsDistributiveAddOtherWayAuto(); } + * Pow(BASE(), |xs| - 2) * BASE(); + { LemmaMulIsDistributiveAddOtherWayAuto(); } ToNatLeft(DropFirst(xs)) * BASE() + First(xs); - { LemmaToNatLeftEqToNatRight(DropFirst(xs)); } + { LemmaToNatLeftEqToNatRight(DropFirst(xs)); } ToNatRight(xs); } } @@ -131,7 +131,7 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat { } /* Appending a zero does not change the nat representation of the sequence. */ - lemma LemmaSeqAppendZero(xs: seq) + lemma LemmaSeqAppendZero(xs: seq) ensures ToNatRight(xs + [0]) == ToNatRight(xs) { reveal ToNatLeft(); @@ -140,7 +140,7 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat { ToNatRight(xs + [0]); ToNatLeft(xs + [0]); ToNatLeft(xs) + 0 * Pow(BASE(), |xs|); - { LemmaMulBasicsAuto(); } + { LemmaMulBasicsAuto(); } ToNatLeft(xs); ToNatRight(xs); } @@ -159,21 +159,21 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat { var pow := Pow(BASE(), len'); calc { ToNatRight(xs); - { LemmaToNatLeftEqToNatRight(xs); } + { LemmaToNatLeftEqToNatRight(xs); } ToNatLeft(xs); - { reveal ToNatLeft(); } + { reveal ToNatLeft(); } ToNatLeft(DropLast(xs)) + Last(xs) * pow; - < { - LemmaToNatLeftEqToNatRight(DropLast(xs)); - LemmaSeqNatBound(DropLast(xs)); - } + < { + LemmaToNatLeftEqToNatRight(DropLast(xs)); + LemmaSeqNatBound(DropLast(xs)); + } pow + Last(xs) * pow; - <= { - LemmaPowPositiveAuto(); - LemmaMulInequalityAuto(); - } + <= { + LemmaPowPositiveAuto(); + LemmaMulInequalityAuto(); + } pow + (BASE() - 1) * pow; - { LemmaMulIsDistributiveAuto(); } + { LemmaMulIsDistributiveAuto(); } Pow(BASE(), len' + 1); } } @@ -193,14 +193,14 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat { calc { ToNatRight(xs[..i]) + ToNatRight(xs[i..]) * Pow(BASE(), i); ToNatRight(DropFirst(xs[..i])) * BASE() + First(xs) + ToNatRight(xs[i..]) * Pow(BASE(), i); - { - assert DropFirst(xs[..i]) == DropFirst(xs)[..i-1]; - LemmaMulProperties(); - } + { + assert DropFirst(xs[..i]) == DropFirst(xs)[..i-1]; + LemmaMulProperties(); + } ToNatRight(DropFirst(xs)[..i-1]) * BASE() + First(xs) + (ToNatRight(xs[i..]) * Pow(BASE(), i - 1)) * BASE(); - { LemmaMulIsDistributiveAddOtherWayAuto(); } + { LemmaMulIsDistributiveAddOtherWayAuto(); } (ToNatRight(DropFirst(xs)[..i-1]) + ToNatRight(DropFirst(xs)[i-1..]) * Pow(BASE(), i - 1)) * BASE() + First(xs); - { LemmaSeqPrefix(DropFirst(xs), i - 1); } + { LemmaSeqPrefix(DropFirst(xs), i - 1); } ToNatRight(xs); } } @@ -220,11 +220,11 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat { calc { ToNatRight(xs); ToNatLeft(xs); - < { LemmaSeqNatBound(DropLast(xs)); } + < { LemmaSeqNatBound(DropLast(xs)); } Pow(BASE(), len') + Last(xs) * Pow(BASE(), len'); - == { LemmaMulIsDistributiveAuto(); } + == { LemmaMulIsDistributiveAuto(); } (1 + Last(xs)) * Pow(BASE(), len'); - <= { LemmaPowPositiveAuto(); LemmaMulInequalityAuto(); } + <= { LemmaPowPositiveAuto(); LemmaMulInequalityAuto(); } ToNatLeft(ys); ToNatRight(ys); } @@ -299,7 +299,7 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat { { calc ==> { xs != ys; - { LemmaSeqNeq(xs, ys); } + { LemmaSeqNeq(xs, ys); } ToNatRight(xs) != ToNatRight(ys); false; } @@ -319,9 +319,9 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat { reveal ToNatRight(); calc ==> { true; - { LemmaModEquivalence(ToNatRight(xs), ToNatRight(DropFirst(xs)) * BASE() + First(xs), BASE()); } + { LemmaModEquivalence(ToNatRight(xs), ToNatRight(DropFirst(xs)) * BASE() + First(xs), BASE()); } IsModEquivalent(ToNatRight(xs), ToNatRight(DropFirst(xs)) * BASE() + First(xs), BASE()); - { LemmaModMultiplesBasicAuto(); } + { LemmaModMultiplesBasicAuto(); } IsModEquivalent(ToNatRight(xs), First(xs), BASE()); } } @@ -355,14 +355,14 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat { } else { calc { |FromNat(n)|; - == { LemmaDivBasicsAuto(); } + == { LemmaDivBasicsAuto(); } 1 + |FromNat(n / BASE())|; - <= { - LemmaMultiplyDivideLtAuto(); - LemmaDivDecreasesAuto(); - reveal Pow(); - LemmaFromNatLen(n / BASE(), len - 1); - } + <= { + LemmaMultiplyDivideLtAuto(); + LemmaDivDecreasesAuto(); + reveal Pow(); + LemmaFromNatLen(n / BASE(), len - 1); + } len; } } @@ -380,15 +380,15 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat { } else { calc { ToNatRight(FromNat(n)); - { LemmaDivBasicsAuto(); } + { LemmaDivBasicsAuto(); } ToNatRight([n % BASE()] + FromNat(n / BASE())); n % BASE() + ToNatRight(FromNat(n / BASE())) * BASE(); - { - LemmaDivDecreasesAuto(); - LemmaNatSeqNat(n / BASE()); - } + { + LemmaDivDecreasesAuto(); + LemmaNatSeqNat(n / BASE()); + } n % BASE() + n / BASE() * BASE(); - { LemmaFundamentalDivMod(n, BASE()); } + { LemmaFundamentalDivMod(n, BASE()); } n; } } @@ -473,7 +473,7 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat { if |xs| > 0 { calc { FromNatWithLen(ToNatRight(xs), |xs|) != xs; - { LemmaSeqNeq(FromNatWithLen(ToNatRight(xs), |xs|), xs); } + { LemmaSeqNeq(FromNatWithLen(ToNatRight(xs), |xs|), xs); } ToNatRight(FromNatWithLen(ToNatRight(xs), |xs|)) != ToNatRight(xs); ToNatRight(xs) != ToNatRight(xs); false; @@ -491,7 +491,7 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat { function {:opaque} SeqAdd(xs: seq, ys: seq): (seq, nat) requires |xs| == |ys| ensures var (zs, cout) := SeqAdd(xs, ys); - |zs| == |xs| && 0 <= cout <= 1 + |zs| == |xs| && 0 <= cout <= 1 decreases xs { if |xs| == 0 then ([], 0) @@ -526,18 +526,18 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat { ToNatRight(zs); ToNatLeft(zs); ToNatLeft(zs') + z * pow; - { LemmaSeqAdd(DropLast(xs), DropLast(ys), zs', cin); } + { LemmaSeqAdd(DropLast(xs), DropLast(ys), zs', cin); } ToNatLeft(DropLast(xs)) + ToNatLeft(DropLast(ys)) - cin * pow + z * pow; - { - LemmaMulEquality(sum, z + cout * BASE(), pow); - assert sum * pow == (z + cout * BASE()) * pow; - LemmaMulIsDistributiveAuto(); - } + { + LemmaMulEquality(sum, z + cout * BASE(), pow); + assert sum * pow == (z + cout * BASE()) * pow; + LemmaMulIsDistributiveAuto(); + } ToNatLeft(xs) + ToNatLeft(ys) - cout * BASE() * pow; - { - LemmaMulIsAssociative(cout, BASE(), pow); - reveal Pow(); - } + { + LemmaMulIsAssociative(cout, BASE(), pow); + reveal Pow(); + } ToNatLeft(xs) + ToNatLeft(ys) - cout * Pow(BASE(), |xs|); ToNatRight(xs) + ToNatRight(ys) - cout * Pow(BASE(), |xs|); } @@ -548,11 +548,11 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat { function {:opaque} SeqSub(xs: seq, ys: seq): (seq, nat) requires |xs| == |ys| ensures var (zs, cout) := SeqSub(xs, ys); - |zs| == |xs| && 0 <= cout <= 1 + |zs| == |xs| && 0 <= cout <= 1 decreases xs { if |xs| == 0 then ([], 0) - else + else var (zs, cin) := SeqSub(DropLast(xs), DropLast(ys)); var (diff_out, cout) := if Last(xs) >= Last(ys) + cin then (Last(xs) - Last(ys) - cin, 0) @@ -574,8 +574,8 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat { var pow := Pow(BASE(), |xs| - 1); var (zs', cin) := SeqSub(DropLast(xs), DropLast(ys)); var z := if Last(xs) >= Last(ys) + cin - then Last(xs) - Last(ys) - cin - else BASE() + Last(xs) - Last(ys) - cin; + then Last(xs) - Last(ys) - cin + else BASE() + Last(xs) - Last(ys) - cin; assert cout * BASE() + Last(xs) - cin - Last(ys) == z; reveal ToNatLeft(); @@ -584,18 +584,18 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat { ToNatRight(zs); ToNatLeft(zs); ToNatLeft(zs') + z * pow; - { LemmaSeqSub(DropLast(xs), DropLast(ys), zs', cin); } + { LemmaSeqSub(DropLast(xs), DropLast(ys), zs', cin); } ToNatLeft(DropLast(xs)) - ToNatLeft(DropLast(ys)) + cin * pow + z * pow; - { - LemmaMulEquality(cout * BASE() + Last(xs) - cin - Last(ys), z, pow); - assert pow * (cout * BASE() + Last(xs) - cin - Last(ys)) == pow * z; - LemmaMulIsDistributiveAuto(); - } + { + LemmaMulEquality(cout * BASE() + Last(xs) - cin - Last(ys), z, pow); + assert pow * (cout * BASE() + Last(xs) - cin - Last(ys)) == pow * z; + LemmaMulIsDistributiveAuto(); + } ToNatLeft(xs) - ToNatLeft(ys) + cout * BASE() * pow; - { - LemmaMulIsAssociative(cout, BASE(), pow); - reveal Pow(); - } + { + LemmaMulIsAssociative(cout, BASE(), pow); + reveal Pow(); + } ToNatLeft(xs) - ToNatLeft(ys) + cout * Pow(BASE(), |xs|); ToNatRight(xs) - ToNatRight(ys) + cout * Pow(BASE(), |xs|); } diff --git a/src/Collections/Sequences/LittleEndianNatConversions.dfy b/src/Collections/Sequences/LittleEndianNatConversions.dfy index 16d30314..a1ff3f6e 100644 --- a/src/Collections/Sequences/LittleEndianNatConversions.dfy +++ b/src/Collections/Sequences/LittleEndianNatConversions.dfy @@ -1,9 +1,9 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" +// RUN: %verify --disable-nonlinear-arithmetic "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../NonlinearArithmetic/DivMod.dfy" include "../../NonlinearArithmetic/Mul.dfy" @@ -105,12 +105,12 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNatConversions { calc { Small.ToNatRight(ToSmall(xs)); Small.ToNatRight(Small.FromNatWithLen(First(xs), E()) + ToSmall(DropFirst(xs))); - { - Small.LemmaSeqPrefix(Small.FromNatWithLen(First(xs), E()) + ToSmall(DropFirst(xs)), E()); - LemmaToSmall(DropFirst(xs)); - } + { + Small.LemmaSeqPrefix(Small.FromNatWithLen(First(xs), E()) + ToSmall(DropFirst(xs)), E()); + LemmaToSmall(DropFirst(xs)); + } First(xs) + Large.ToNatRight(DropFirst(xs)) * Pow(Small.BASE(), E()); - { assert Pow(Small.BASE(), E()) == Large.BASE(); } + { assert Pow(Small.BASE(), E()) == Large.BASE(); } Large.ToNatRight(xs); } } @@ -129,15 +129,15 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNatConversions { } else { calc { Large.ToNatRight(ToLarge(xs)); - { - LemmaModIsZero(|xs|, E()); - LemmaModSubMultiplesVanishAuto(); - Small.LemmaSeqNatBound(xs[..E()]); - } + { + LemmaModIsZero(|xs|, E()); + LemmaModSubMultiplesVanishAuto(); + Small.LemmaSeqNatBound(xs[..E()]); + } Large.ToNatRight([Small.ToNatRight(xs[..E()]) as Large.uint] + ToLarge(xs[E()..])); - { LemmaToLarge(xs[E()..]); } + { LemmaToLarge(xs[E()..]); } Small.ToNatRight(xs[..E()]) + Small.ToNatRight(xs[E()..]) * Pow(Small.BASE(), E()); - { Small.LemmaSeqPrefix(xs, E()); } + { Small.LemmaSeqPrefix(xs, E()); } Small.ToNatRight(xs); } } @@ -157,7 +157,7 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNatConversions { /* ToLarge is injective. */ lemma LemmaToLargeIsInjective(xs: seq, ys: seq) - requires |xs| % E() == |ys| % E() == 0 + requires |xs| % E() == |ys| % E() == 0 requires ToLarge(xs) == ToLarge(ys) requires |xs| == |ys| ensures xs == ys @@ -180,17 +180,17 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNatConversions { } else { calc { ToSmall(ToLarge(xs)); - { - LemmaModIsZero(|xs|, E()); - Small.LemmaSeqNatBound(xs[..E()]); - LemmaModSubMultiplesVanishAuto(); - } + { + LemmaModIsZero(|xs|, E()); + Small.LemmaSeqNatBound(xs[..E()]); + LemmaModSubMultiplesVanishAuto(); + } ToSmall([Small.ToNatRight(xs[..E()]) as Large.uint] + ToLarge(xs[E()..])); Small.FromNatWithLen(Small.ToNatRight(xs[..E()]), E()) + ToSmall(ToLarge(xs[E()..])); - { - Small.LemmaSeqNatSeq(xs[..E()]); - LemmaSmallLargeSmall(xs[E()..]); - } + { + Small.LemmaSeqNatSeq(xs[..E()]); + LemmaSmallLargeSmall(xs[E()..]); + } xs; } } @@ -212,7 +212,7 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNatConversions { ToLarge(Small.FromNatWithLen(First(xs), E()) + ToSmall(DropFirst(xs))); [Small.ToNatRight(Small.FromNatWithLen(First(xs), E())) as Large.uint] + ToLarge(ToSmall(DropFirst(xs))); [First(xs)] + ToLarge(ToSmall(DropFirst(xs))); - { LemmaLargeSmallLarge(DropFirst(xs)); } + { LemmaLargeSmallLarge(DropFirst(xs)); } [First(xs)] + DropFirst(xs); xs; } diff --git a/src/Collections/Sequences/MergeSort.dfy b/src/Collections/Sequences/MergeSort.dfy index 7fad4d44..42be3a36 100644 --- a/src/Collections/Sequences/MergeSort.dfy +++ b/src/Collections/Sequences/MergeSort.dfy @@ -1,9 +1,9 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../Relations.dfy" @@ -54,4 +54,4 @@ module {:options "-functionSyntax:4"} Seq.MergeSort { [right[0]] + MergeSortedWith(left, right[1..], lessThanOrEq) } -} \ No newline at end of file +} diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 4c4d5b2f..f986e1b9 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -1,17 +1,17 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Original Copyright under the following: -* Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, -* ETH Zurich, and University of Washington -* SPDX-License-Identifier: BSD-2-Clause -* -* Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original Copyright under the following: + * Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, + * ETH Zurich, and University of Washington + * SPDX-License-Identifier: BSD-2-Clause + * + * Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../Wrappers.dfy" include "../../Math.dfy" @@ -26,10 +26,10 @@ module {:options "-functionSyntax:4"} Seq { import Math /********************************************************** - * - * Manipulating the End of a Sequence - * - ***********************************************************/ + * + * Manipulating the End of a Sequence + * + ***********************************************************/ /* Returns the first element of a non-empty sequence. */ function First(xs: seq): T @@ -55,7 +55,7 @@ module {:options "-functionSyntax:4"} Seq { /* Returns the subsequence of a non-empty sequence obtained by dropping the last element. */ - function DropLast(xs: seq): seq + function DropLast(xs: seq): seq requires |xs| > 0; { xs[..|xs|-1] @@ -85,18 +85,18 @@ module {:options "-functionSyntax:4"} Seq { } /********************************************************** - * - * Manipulating the Content of a Sequence - * - ***********************************************************/ - + * + * Manipulating the Content of a Sequence + * + ***********************************************************/ + /* Is true if the sequence xs is a prefix of the sequence ys. */ ghost predicate IsPrefix(xs: seq, ys: seq) ensures IsPrefix(xs, ys) ==> (|xs| <= |ys| && xs == ys[..|xs|]) { - xs <= ys + xs <= ys } - + /* Is true if the sequence xs is a suffix of the sequence ys. */ ghost predicate IsSuffix(xs: seq, ys: seq) { @@ -149,7 +149,7 @@ module {:options "-functionSyntax:4"} Seq { } /* Converts a sequence to a set. */ - function {:opaque} ToSet(xs: seq): set + function {:opaque} ToSet(xs: seq): set { set x: T | x in xs } @@ -157,7 +157,7 @@ module {:options "-functionSyntax:4"} Seq { /* The cardinality of a set of elements is always less than or equal to that of the full sequence of elements. */ lemma LemmaCardinalityOfSet(xs: seq) - ensures |ToSet(xs)| <= |xs| + ensures |ToSet(xs)| <= |xs| { reveal ToSet(); if |xs| == 0 { @@ -166,7 +166,7 @@ module {:options "-functionSyntax:4"} Seq { LemmaCardinalityOfSet(DropLast(xs)); } } - + /* A sequence is of length 0 if and only if its conversion to a set results in the empty set. */ lemma LemmaCardinalityOfEmptySetIs0(xs: seq) @@ -179,7 +179,7 @@ module {:options "-functionSyntax:4"} Seq { } /* Is true if there are no duplicate values in the sequence. */ - ghost predicate {:opaque} HasNoDuplicates(xs: seq) + ghost predicate {:opaque} HasNoDuplicates(xs: seq) { (forall i, j {:trigger xs[i], xs[j]}:: 0 <= i < |xs| && 0 <= j < |xs| && i != j ==> xs[i] != xs[j]) } @@ -197,11 +197,11 @@ module {:options "-functionSyntax:4"} Seq { var zs := xs + ys; if |zs| > 1 { assert forall i {:trigger zs[i]} :: 0 <= i < |xs| ==> - zs[i] in multiset(xs); + zs[i] in multiset(xs); assert forall j {:trigger zs[j]} :: |xs| <= j < |zs| ==> - zs[j] in multiset(ys); + zs[j] in multiset(ys); assert forall i, j {:trigger zs[i], zs[j]} :: i != j && 0 <= i < |xs| && |xs| <= j < |zs| ==> - zs[i] != zs[j]; + zs[i] != zs[j]; } } @@ -281,10 +281,10 @@ module {:options "-functionSyntax:4"} Seq { { if |xs| == 0 then None() else - if xs[0] == v then Some(0) - else - var o' := IndexOfOption(xs[1..], v); - if o'.Some? then Some(o'.value + 1) else None() + if xs[0] == v then Some(0) + else + var o' := IndexOfOption(xs[1..], v); + if o'.Some? then Some(o'.value + 1) else None() } /* For an element that occurs at least once in a sequence, the index of its @@ -355,7 +355,7 @@ module {:options "-functionSyntax:4"} Seq { { if xs == [] then [] else [xs[|xs|-1]] + Reverse(xs[0 .. |xs|-1]) } - + /* Returns a constant sequence of a given length. */ function {:opaque} Repeat(v: T, length: nat): (xs: seq) ensures |xs| == length @@ -366,12 +366,12 @@ module {:options "-functionSyntax:4"} Seq { else [v] + Repeat(v, length - 1) } - + /* Unzips a sequence that contains pairs into two separate sequences. */ function {:opaque} Unzip(xs: seq<(A, B)>): (seq, seq) ensures |Unzip(xs).0| == |Unzip(xs).1| == |xs| - ensures forall i {:trigger Unzip(xs).0[i]} {:trigger Unzip(xs).1[i]} - :: 0 <= i < |xs| ==> (Unzip(xs).0[i], Unzip(xs).1[i]) == xs[i] + ensures forall i {:trigger Unzip(xs).0[i]} {:trigger Unzip(xs).1[i]} + :: 0 <= i < |xs| ==> (Unzip(xs).0[i], Unzip(xs).1[i]) == xs[i] { if |xs| == 0 then ([], []) else @@ -398,10 +398,10 @@ module {:options "-functionSyntax:4"} Seq { } /********************************************************** - * - * Extrema in Sequences - * - ***********************************************************/ + * + * Extrema in Sequences + * + ***********************************************************/ /* Returns the maximum integer value in a non-empty sequence of integers. */ function {:opaque} Max(xs: seq): int @@ -483,10 +483,10 @@ module {:options "-functionSyntax:4"} Seq { } /********************************************************** - * - * Sequences of Sequences - * - ***********************************************************/ + * + * Sequences of Sequences + * + ***********************************************************/ /* Flattens a sequence of sequences into a single sequence by concatenating subsequences, starting from the first element. */ @@ -508,7 +508,7 @@ module {:options "-functionSyntax:4"} Seq { } else { calc == { Flatten(xs + ys); - { assert (xs + ys)[0] == xs[0]; assert (xs + ys)[1..] == xs[1..] + ys; } + { assert (xs + ys)[0] == xs[0]; assert (xs + ys)[1..] == xs[1..] + ys; } xs[0] + Flatten(xs[1..] + ys); xs[0] + Flatten(xs[1..]) + Flatten(ys); Flatten(xs) + Flatten(ys); @@ -538,7 +538,7 @@ module {:options "-functionSyntax:4"} Seq { } else { calc == { FlattenReverse(xs + ys); - { assert Last(xs + ys) == Last(ys); assert DropLast(xs + ys) == xs + DropLast(ys); } + { assert Last(xs + ys) == Last(ys); assert DropLast(xs + ys) == xs + DropLast(ys); } FlattenReverse(xs + DropLast(ys)) + Last(ys); FlattenReverse(xs) + FlattenReverse(DropLast(ys)) + Last(ys); FlattenReverse(xs) + FlattenReverse(ys); @@ -556,11 +556,11 @@ module {:options "-functionSyntax:4"} Seq { calc == { FlattenReverse(xs); FlattenReverse(DropLast(xs)) + Last(xs); - { LemmaFlattenAndFlattenReverseAreEquivalent(DropLast(xs)); } + { LemmaFlattenAndFlattenReverseAreEquivalent(DropLast(xs)); } Flatten(DropLast(xs)) + Last(xs); Flatten(DropLast(xs)) + Flatten([Last(xs)]); - { LemmaFlattenConcat(DropLast(xs), [Last(xs)]); - assert xs == DropLast(xs) + [Last(xs)]; } + { LemmaFlattenConcat(DropLast(xs), [Last(xs)]); + assert xs == DropLast(xs) + [Last(xs)]; } Flatten(xs); } } @@ -593,10 +593,10 @@ module {:options "-functionSyntax:4"} Seq { /********************************************************** - * - * Higher-Order Sequence Functions - * - ***********************************************************/ + * + * Higher-Order Sequence Functions + * + ***********************************************************/ /* Returns the sequence one obtains by applying a function to every element of a sequence. */ @@ -610,16 +610,16 @@ module {:options "-functionSyntax:4"} Seq { else [f(xs[0])] + Map(f, xs[1..]) } -/* Applies a function to every element of a sequence, returning a Result value (which is a - failure-compatible type). Returns either a failure, or, if successful at every element, - the transformed sequence. */ + /* Applies a function to every element of a sequence, returning a Result value (which is a + failure-compatible type). Returns either a failure, or, if successful at every element, + the transformed sequence. */ function {:opaque} MapWithResult(f: (T ~> Result), xs: seq): (result: Result, E>) requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i]) ensures result.Success? ==> - && |result.value| == |xs| - && (forall i :: 0 <= i < |xs| ==> - && f(xs[i]).Success? - && result.value[i] == f(xs[i]).value) + && |result.value| == |xs| + && (forall i :: 0 <= i < |xs| ==> + && f(xs[i]).Success? + && result.value[i] == f(xs[i]).value) reads set i, o | 0 <= i < |xs| && o in f.reads(xs[i]) :: o { if |xs| == 0 then Success([]) @@ -643,10 +643,10 @@ module {:options "-functionSyntax:4"} Seq { } else { calc { Map(f, xs + ys); - { assert (xs + ys)[0] == xs[0]; assert (xs + ys)[1..] == xs[1..] + ys; } + { assert (xs + ys)[0] == xs[0]; assert (xs + ys)[1..] == xs[1..] + ys; } Map(f, [xs[0]]) + Map(f, xs[1..] + ys); Map(f, [xs[0]]) + Map(f, xs[1..]) + Map(f, ys); - {assert [(xs + ys)[0]] + xs[1..] + ys == xs + ys;} + {assert [(xs + ys)[0]] + xs[1..] + ys == xs + ys;} Map(f, xs) + Map(f, ys); } } @@ -678,16 +678,16 @@ module {:options "-functionSyntax:4"} Seq { } else { calc { Filter(f, xs + ys); - { assert {:split_here} (xs + ys)[0] == xs[0]; assert (xs + ys)[1..] == xs[1..] + ys; } + { assert {:split_here} (xs + ys)[0] == xs[0]; assert (xs + ys)[1..] == xs[1..] + ys; } Filter(f, [xs[0]]) + Filter(f, xs[1..] + ys); - { assert Filter(f, xs[1..] + ys) == Filter(f, xs[1..]) + Filter(f, ys); } + { assert Filter(f, xs[1..] + ys) == Filter(f, xs[1..]) + Filter(f, ys); } Filter(f, [xs[0]]) + (Filter(f, xs[1..]) + Filter(f, ys)); - { assert {:split_here} [(xs + ys)[0]] + (xs[1..] + ys) == xs + ys; } + { assert {:split_here} [(xs + ys)[0]] + (xs[1..] + ys) == xs + ys; } Filter(f, xs) + Filter(f, ys); } } } - + /* Folds a sequence xs from the left (the beginning), by repeatedly acting on the accumulator init via the function f. */ function {:opaque} FoldLeft(f: (A, T) -> A, init: A, xs: seq): A @@ -712,10 +712,10 @@ module {:options "-functionSyntax:4"} Seq { calc { FoldLeft(f, FoldLeft(f, init, xs), ys); FoldLeft(f, FoldLeft(f, f(init, xs[0]), xs[1..]), ys); - { LemmaFoldLeftDistributesOverConcat(f, f(init, xs[0]), xs[1..], ys); } + { LemmaFoldLeftDistributesOverConcat(f, f(init, xs[0]), xs[1..], ys); } FoldLeft(f, f(init, xs[0]), xs[1..] + ys); - { assert (xs + ys)[0] == xs[0]; - assert (xs + ys)[1..] == xs[1..] + ys; } + { assert (xs + ys)[0] == xs[0]; + assert (xs + ys)[1..] == xs[1..] + ys; } FoldLeft(f, init, xs + ys); } } @@ -724,7 +724,7 @@ module {:options "-functionSyntax:4"} Seq { /* Is true, if inv is an invariant under stp, which is a relational version of the function f passed to fold. */ ghost predicate InvFoldLeft(inv: (B, seq) -> bool, - stp: (B, A, B) -> bool) + stp: (B, A, B) -> bool) { forall x: A, xs: seq, b: B, b': B :: inv(b, [x] + xs) && stp(b, x, b') ==> inv(b', xs) @@ -772,8 +772,8 @@ module {:options "-functionSyntax:4"} Seq { FoldRight(f, xs, FoldRight(f, ys, init)); f(xs[0], FoldRight(f, xs[1..], FoldRight(f, ys, init))); f(xs[0], FoldRight(f, xs[1..] + ys, init)); - { assert (xs + ys)[0] == xs[0]; - assert (xs +ys)[1..] == xs[1..] + ys; } + { assert (xs + ys)[0] == xs[0]; + assert (xs +ys)[1..] == xs[1..] + ys; } FoldRight(f, xs + ys, init); } } @@ -782,7 +782,7 @@ module {:options "-functionSyntax:4"} Seq { /* Is true, if inv is an invariant under stp, which is a relational version of the function f passed to fold. */ ghost predicate InvFoldRight(inv: (seq, B) -> bool, - stp: (A, B, B) -> bool) + stp: (A, B, B) -> bool) { forall x: A, xs: seq, b: B, b': B :: inv(xs, b) && stp(x, b, b') ==> inv(([x] + xs), b') @@ -808,10 +808,10 @@ module {:options "-functionSyntax:4"} Seq { /********************************************************** - * - * Sets to Ordered Sequences - * - ***********************************************************/ + * + * Sets to Ordered Sequences + * + ***********************************************************/ /* Converts a set to a sequence (ghost). */ ghost function SetToSeqSpec(s: set): (xs: seq) diff --git a/src/Collections/Sets/Isets.dfy b/src/Collections/Sets/Isets.dfy index 1a1b6db5..84143e5d 100644 --- a/src/Collections/Sets/Isets.dfy +++ b/src/Collections/Sets/Isets.dfy @@ -1,17 +1,17 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Original Copyright under the following: -* Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, -* ETH Zurich, and University of Washington -* SPDX-License-Identifier: BSD-2-Clause -* -* Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original Copyright under the following: + * Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, + * ETH Zurich, and University of Washington + * SPDX-License-Identifier: BSD-2-Clause + * + * Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../Functions.dfy" diff --git a/src/Collections/Sets/Sets.dfy b/src/Collections/Sets/Sets.dfy index 4a13b10f..b0c1d6ef 100644 --- a/src/Collections/Sets/Sets.dfy +++ b/src/Collections/Sets/Sets.dfy @@ -1,17 +1,17 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Original Copyright under the following: -* Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, -* ETH Zurich, and University of Washington -* SPDX-License-Identifier: BSD-2-Clause -* -* Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original Copyright under the following: + * Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, + * ETH Zurich, and University of Washington + * SPDX-License-Identifier: BSD-2-Clause + * + * Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../Functions.dfy" diff --git a/src/FileIO/FileIO.dfy b/src/FileIO/FileIO.dfy index 48ea0950..6e6118e0 100644 --- a/src/FileIO/FileIO.dfy +++ b/src/FileIO/FileIO.dfy @@ -1,22 +1,22 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" include "../Wrappers.dfy" /** - * This module provides basic file I/O operations: reading and writing bytes from/to a file. - * The provided API is intentionally limited in scope and will be expanded later. - * - * Where the API accepts file paths as strings, there are some limitations. - * File paths containing only ASCII characters work identically across languages and platforms; - * non-ASCII Unicode codepoints may cause different language- or platform-specific behavior. - * - * File path symbols including . and .. are allowed. - */ + * This module provides basic file I/O operations: reading and writing bytes from/to a file. + * The provided API is intentionally limited in scope and will be expanded later. + * + * Where the API accepts file paths as strings, there are some limitations. + * File paths containing only ASCII characters work identically across languages and platforms; + * non-ASCII Unicode codepoints may cause different language- or platform-specific behavior. + * + * File path symbols including . and .. are allowed. + */ module {:options "-functionSyntax:4"} FileIO { import opened Wrappers @@ -27,25 +27,25 @@ module {:options "-functionSyntax:4"} FileIO { */ /** - * Attempts to read all bytes from the file at the given file path. - * If an error occurs, a `Result.Failure` value is returned containing an implementation-specific - * error message (which may also contain a stack trace). - * - * NOTE: See the module description for limitations on the path argument. - */ + * Attempts to read all bytes from the file at the given file path. + * If an error occurs, a `Result.Failure` value is returned containing an implementation-specific + * error message (which may also contain a stack trace). + * + * NOTE: See the module description for limitations on the path argument. + */ method ReadBytesFromFile(path: string) returns (res: Result, string>) { var isError, bytesRead, errorMsg := INTERNAL_ReadBytesFromFile(path); return if isError then Failure(errorMsg) else Success(bytesRead); } /** - * Attempts to write the given bytes to the file at the given file path, - * creating nonexistent parent directories as necessary. - * If an error occurs, a `Result.Failure` value is returned containing an implementation-specific - * error message (which may also contain a stack trace). - * - * NOTE: See the module description for limitations on the path argument. - */ + * Attempts to write the given bytes to the file at the given file path, + * creating nonexistent parent directories as necessary. + * If an error occurs, a `Result.Failure` value is returned containing an implementation-specific + * error message (which may also contain a stack trace). + * + * NOTE: See the module description for limitations on the path argument. + */ method WriteBytesToFile(path: string, bytes: seq) returns (res: Result<(), string>) { var isError, errorMsg := INTERNAL_WriteBytesToFile(path, bytes); @@ -58,11 +58,11 @@ module {:options "-functionSyntax:4"} FileIO { method {:extern "DafnyLibraries.FileIO", "INTERNAL_ReadBytesFromFile"} - INTERNAL_ReadBytesFromFile(path: string) + INTERNAL_ReadBytesFromFile(path: string) returns (isError: bool, bytesRead: seq, errorMsg: string) method {:extern "DafnyLibraries.FileIO", "INTERNAL_WriteBytesToFile"} - INTERNAL_WriteBytesToFile(path: string, bytes: seq) + INTERNAL_WriteBytesToFile(path: string, bytes: seq) returns (isError: bool, errorMsg: string) } diff --git a/src/Functions.dfy b/src/Functions.dfy index 85757547..8436f50f 100644 --- a/src/Functions.dfy +++ b/src/Functions.dfy @@ -1,17 +1,17 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Original Copyright under the following: -* Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, -* ETH Zurich, and University of Washington -* SPDX-License-Identifier: BSD-2-Clause -* -* Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original Copyright under the following: + * Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, + * ETH Zurich, and University of Washington + * SPDX-License-Identifier: BSD-2-Clause + * + * Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ module {:options "-functionSyntax:4"} Functions { ghost predicate Injective(f: X-->Y) diff --git a/src/Math.dfy b/src/Math.dfy index 0230ae28..6ec5d2ed 100644 --- a/src/Math.dfy +++ b/src/Math.dfy @@ -1,15 +1,15 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ module {:options "-functionSyntax:4"} Math { function Min(a: int, b: int): int { if a < b - then a + then a else b } @@ -17,7 +17,7 @@ module {:options "-functionSyntax:4"} Math { function Max(a: int, b: int): int { if a < b - then b + then b else a } diff --git a/src/NonlinearArithmetic/DivMod.dfy b/src/NonlinearArithmetic/DivMod.dfy index 81d50582..b6a924c6 100644 --- a/src/NonlinearArithmetic/DivMod.dfy +++ b/src/NonlinearArithmetic/DivMod.dfy @@ -1,12 +1,12 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" +// RUN: %verify --disable-nonlinear-arithmetic "%s" /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original: Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ /* Every lemma comes in 2 forms: 'LemmaProperty' and 'LemmaPropertyAuto'. The former takes arguments and may be more stable and less reliant on Z3 @@ -27,8 +27,8 @@ module {:options "-functionSyntax:4"} DivMod { import opened GeneralInternals /***************************************************************************** - * Division: - *****************************************************************************/ + * Division: + *****************************************************************************/ /* the common syntax of division gives the same quotient as performing division through recursion */ lemma LemmaDivIsDivRecursive(x: int, d: int) @@ -54,7 +54,7 @@ module {:options "-functionSyntax:4"} DivMod { lemma LemmaDivBySelf(d: int) requires d != 0 ensures d / d == 1 - { + { DivINL.LemmaDivBySelf(d); } @@ -62,7 +62,7 @@ module {:options "-functionSyntax:4"} DivMod { lemma LemmaDivOf0(d: int) requires d != 0 ensures 0 / d == 0 - { + { DivINL.LemmaDivOf0(d); } @@ -78,7 +78,7 @@ module {:options "-functionSyntax:4"} DivMod { LemmaDivOf0(x); } } - + lemma LemmaDivBasicsAuto() ensures forall x {:trigger 0 / x} :: x != 0 ==> 0 / x == 0 ensures forall x {:trigger x / 1} :: x / 1 == x @@ -122,8 +122,8 @@ module {:options "-functionSyntax:4"} DivMod { { reveal DivRecursive(); LemmaDivIsDivRecursiveAuto(); - assert forall u: int, d: int {:trigger u / d} {:trigger DivRecursive(u, d)} - :: d > 0 ==> DivRecursive(u, d) == u / d; + assert forall u: int, d: int {:trigger u / d} {:trigger DivRecursive(u, d)} + :: d > 0 ==> DivRecursive(u, d) == u / d; if (x < z) { @@ -177,18 +177,18 @@ module {:options "-functionSyntax:4"} DivMod { calc ==> { a % d + b % d == R + (a + b) % d; (a + b) - (a + b) % d - R == a - (a % d) + b - (b % d); - { - LemmaFundamentalDivMod(a + b, d); - LemmaFundamentalDivMod(a, d); - LemmaFundamentalDivMod(b, d); - } + { + LemmaFundamentalDivMod(a + b, d); + LemmaFundamentalDivMod(a, d); + LemmaFundamentalDivMod(b, d); + } d * ((a + b) / d) - R == d * (a / d) + d * (b / d); } } lemma LemmaDividingSumsAuto() ensures forall a: int, b: int, d: int, R: int {:trigger d * ((a + b) / d) - R, d*(a/d) + d*(b/d)} - :: 0 < d && R == a%d + b%d - (a+b)%d ==> d*((a+b)/d) - R == d*(a/d) + d*(b/d) + :: 0 < d && R == a%d + b%d - (a+b)%d ==> d*((a+b)/d) - R == d*(a/d) + d*(b/d) { forall (a: int, b: int, d: int, R: int | 0< d && R == a%d + b%d - (a+b)%d) ensures d*((a+b)/d) - R == d*(a/d) + d*(b/d) @@ -326,7 +326,7 @@ module {:options "-functionSyntax:4"} DivMod { ensures forall x: int, d: int {:trigger x / d } :: 0 <= x && 0 < d ==> x / d <= x { forall (x: int, d: int | 0 <= x && 0 < d) - ensures x / d <= x + ensures x / d <= x { LemmaDivNonincreasing(x, d); } @@ -354,46 +354,46 @@ module {:options "-functionSyntax:4"} DivMod { calc { (y * (x / y)) % (y * z) + (x % y) % (y * z); - <= { LemmaPartBound1(x, y, z); } + <= { LemmaPartBound1(x, y, z); } y * (z - 1) + (x % y) % (y * z); - < { LemmaPartBound2(x, y, z); } + < { LemmaPartBound2(x, y, z); } y * (z - 1) + y; - { LemmaMulBasicsAuto(); } + { LemmaMulBasicsAuto(); } y * (z - 1) + y * 1; - { LemmaMulIsDistributiveAuto(); } + { LemmaMulIsDistributiveAuto(); } y * (z - 1 + 1); y * z; } calc { x % (y * z); - { LemmaFundamentalDivMod(x,y); } + { LemmaFundamentalDivMod(x,y); } (y * (x / y) + x % y) % (y * z); - { - LemmaModPropertiesAuto(); - assert 0 <= x % y; - LemmaMulNonnegative(y, x / y); - assert (y * (x / y)) % (y * z) + (x % y) % (y * z) < y * z; - LemmaModAdds(y * (x / y), x % y, y * z); - } + { + LemmaModPropertiesAuto(); + assert 0 <= x % y; + LemmaMulNonnegative(y, x / y); + assert (y * (x / y)) % (y * z) + (x % y) % (y * z) < y * z; + LemmaModAdds(y * (x / y), x % y, y * z); + } (y * (x / y)) % (y * z) + (x % y) % (y * z); - { - LemmaModPropertiesAuto(); - LemmaMulIncreases(z, y); - LemmaMulIsCommutativeAuto(); - assert x % y < y <= y * z; - LemmaSmallMod(x % y, y * z); - assert (x % y) % (y * z) == x % y; - } + { + LemmaModPropertiesAuto(); + LemmaMulIncreases(z, y); + LemmaMulIsCommutativeAuto(); + assert x % y < y <= y * z; + LemmaSmallMod(x % y, y * z); + assert (x % y) % (y * z) == x % y; + } (y * (x / y)) % (y * z) + x % y; - { LemmaTruncateMiddle(x / y, y, z); } + { LemmaTruncateMiddle(x / y, y, z); } y * ((x / y) % z) + x % y; } } lemma LemmaBreakdownAuto() - ensures forall x: int, y: int, z: int {:trigger y * z, x % (y * z), y * ((x / y) % z) + x % y} - :: 0 <= x && 0 < y && 0 < z ==> 0 < y * z && x % (y * z) == y * ((x / y) % z) + x % y + ensures forall x: int, y: int, z: int {:trigger y * z, x % (y * z), y * ((x / y) % z) + x % y} + :: 0 <= x && 0 < y && 0 < z ==> 0 < y * z && x % (y * z) == y * ((x / y) % z) + x % y { forall (x: int, y: int, z: int | 0 <= x && 0 < y && 0 < z) ensures 0 < y * z && x % (y * z) == y * ((x / y) % z) + x % y @@ -401,7 +401,7 @@ module {:options "-functionSyntax:4"} DivMod { LemmaBreakdown(x, y, z); } } - + lemma LemmaRemainderUpper(x: int, d: int) requires 0 <= x requires 0 < d @@ -420,7 +420,7 @@ module {:options "-functionSyntax:4"} DivMod { LemmaRemainderUpper(x, d); } } - + lemma LemmaRemainderLower(x: int, d: int) requires 0 <= x requires 0 < d @@ -439,7 +439,7 @@ module {:options "-functionSyntax:4"} DivMod { LemmaRemainderLower(x, d); } } - + lemma LemmaRemainder(x: int, d: int) requires 0 <= x requires 0 < d @@ -452,14 +452,14 @@ module {:options "-functionSyntax:4"} DivMod { lemma LemmaRemainderAuto() ensures forall x: int, d: int {:trigger x - (x / d * d)} :: 0 <= x && 0 < d ==> 0 <= x - (x / d * d) < d { - forall x: int, d: int | 0 <= x && 0 < d + forall x: int, d: int | 0 <= x && 0 < d ensures 0 <= x - (x / d * d) < d { LemmaRemainder(x, d); } } - /* describes fundementals of the modulus operator */ + /* describes fundementals of the modulus operator */ lemma LemmaFundamentalDivMod(x: int, d: int) requires d != 0 ensures x == d * (x / d) + (x % d) @@ -468,7 +468,7 @@ module {:options "-functionSyntax:4"} DivMod { } lemma LemmaFundamentalDivModAuto() - ensures forall x: int, d: int {:trigger d * (x / d) + (x % d)} :: d != 0 ==> x == d * (x / d) + (x % d) + ensures forall x: int, d: int {:trigger d * (x / d) + (x % d)} :: d != 0 ==> x == d * (x / d) + (x % d) { forall x: int, d: int | d != 0 ensures x == d * (x / d) + (x % d) @@ -516,64 +516,64 @@ module {:options "-functionSyntax:4"} DivMod { calc { c * ((x / c) % d) + x % c; - { LemmaModMultiplesVanish(-k, x / c, d); LemmaMulIsCommutativeAuto(); } + { LemmaModMultiplesVanish(-k, x / c, d); LemmaMulIsCommutativeAuto(); } c * ((x / c + (-k) * d) % d) + x % c; - { LemmaHoistOverDenominator(x, (-k)*d, c); } + { LemmaHoistOverDenominator(x, (-k)*d, c); } c * (((x + (((-k) * d) * c)) / c) % d) + x % c; - { LemmaMulIsAssociative(-k, d, c); } + { LemmaMulIsAssociative(-k, d, c); } c * (((x + ((-k) * (d * c))) / c) % d) + x % c; - { LemmaMulUnaryNegation(k, d * c); } + { LemmaMulUnaryNegation(k, d * c); } c * (((x + (-(k * (d * c)))) / c) % d) + x % c; - { LemmaMulIsAssociative(k, d, c); } + { LemmaMulIsAssociative(k, d, c); } c * (((x + (-(k * d * c))) / c) % d) + x % c; c * (((x - k * d * c) / c) % d) + x % c; - { - LemmaMulIsAssociativeAuto(); - LemmaMulIsCommutativeAuto(); - } + { + LemmaMulIsAssociativeAuto(); + LemmaMulIsCommutativeAuto(); + } c * ((R / c) % d) + x % c; c * (R / c) + x % c; - { LemmaFundamentalDivMod(R, c); - assert R == c * (R / c) + R % c; - LemmaModMod(x, c, d); - assert R % c == x % c; - } + { LemmaFundamentalDivMod(R, c); + assert R == c * (R / c) + R % c; + LemmaModMod(x, c, d); + assert R % c == x % c; + } R; - { LemmaModIsModRecursiveAuto(); } + { LemmaModIsModRecursiveAuto(); } R % (c * d); (x - (c * d) * k) % (c * d); - { LemmaMulUnaryNegation(c * d, k); } + { LemmaMulUnaryNegation(c * d, k); } (x + (c * d) * (-k)) % (c * d); - { LemmaModMultiplesVanish(-k, x, c * d); } + { LemmaModMultiplesVanish(-k, x, c * d); } x % (c * d); } calc ==> { c * (x / c) + x % c - R == c * (x / c) - c * ((x / c) % d); - { LemmaFundamentalDivMod(x, c); } + { LemmaFundamentalDivMod(x, c); } x - R == c * (x / c) - c * ((x / c) % d); } calc ==> { true; - { LemmaFundamentalDivMod(x / c, d); } + { LemmaFundamentalDivMod(x / c, d); } d * ((x / c) / d) == x / c - ((x / c) % d); c * (d * ((x / c) / d)) == c * (x / c - ((x / c) % d)); - { LemmaMulIsAssociativeAuto(); } + { LemmaMulIsAssociativeAuto(); } (c * d) * ((x / c) / d) == c * (x / c - ((x / c) % d)); - { LemmaMulIsDistributiveAuto(); } + { LemmaMulIsDistributiveAuto(); } (c * d) * ((x / c) / d) == c * (x / c) - c * ((x / c) % d); (c * d) * ((x / c) / d) == x - R; - { LemmaFundamentalDivMod(x, c * d); } + { LemmaFundamentalDivMod(x, c * d); } (c * d) * ((x / c) / d) == (c * d) * (x / (c * d)) + x % (c * d) - R; (c * d) * ((x / c) / d) == (c * d) * (x / (c * d)); - { LemmaMulEqualityConverse(c * d, (x / c) / d, x / (c * d)); } + { LemmaMulEqualityConverse(c * d, (x / c) / d, x / (c * d)); } (x / c) / d == x / (c * d); } } - + lemma LemmaDivDenominatorAuto() ensures forall c: nat, d: nat {:trigger c * d} :: 0 < c && 0 < d ==> c * d != 0 - ensures forall x: int, c: nat, d: nat {:trigger (x / c) / d} - :: 0 <= x && 0 < c && 0 < d ==> (x / c) / d == x / (c * d) + ensures forall x: int, c: nat, d: nat {:trigger (x / c) / d} + :: 0 <= x && 0 < c && 0 < d ==> (x / c) / d == x / (c * d) { LemmaMulNonzeroAuto(); forall x: int, c: nat, d: nat | 0 <= x && 0 < c && 0 < d @@ -596,22 +596,22 @@ module {:options "-functionSyntax:4"} DivMod { (x * (z * (y / z) + y % z)) / z; { LemmaMulIsDistributiveAuto(); } (x * (z * (y / z)) + x * (y % z)) / z; - >= { - LemmaModPropertiesAuto(); - LemmaMulNonnegative(x, y % z); - LemmaDivIsOrdered(x * (z * (y / z)), x * (z * (y / z)) + x * (y % z), z); } + >= { + LemmaModPropertiesAuto(); + LemmaMulNonnegative(x, y % z); + LemmaDivIsOrdered(x * (z * (y / z)), x * (z * (y / z)) + x * (y % z), z); } (x * (z * (y / z))) / z; - { LemmaMulIsAssociativeAuto(); - LemmaMulIsCommutativeAuto(); } + { LemmaMulIsAssociativeAuto(); + LemmaMulIsCommutativeAuto(); } (z * (x * (y / z))) / z; - { LemmaDivMultiplesVanish(x * (y / z), z); } + { LemmaDivMultiplesVanish(x * (y / z), z); } x * (y / z); } } - + lemma LemmaMulHoistInequalityAuto() - ensures forall x: int, y: int, z: int {:trigger x * (y / z), (x * y) / z} - :: 0 <= x && 0 < z ==> x * (y / z) <= (x * y) / z + ensures forall x: int, y: int, z: int {:trigger x * (y / z), (x * y) / z} + :: 0 <= x && 0 < z ==> x * (y / z) <= (x * y) / z { forall (x: int, y: int, z: int | 0 <= x && 0 < z) ensures x * (y / z) <= (x * y) / z @@ -629,14 +629,14 @@ module {:options "-functionSyntax:4"} DivMod { } lemma LemmaIndistinguishableQuotientsAuto() - ensures forall a: int, b: int, d: int {:trigger a / d, b / d} - :: 0 < d && 0 <= a - a % d <= b < a + d - a % d ==> a / d == b / d + ensures forall a: int, b: int, d: int {:trigger a / d, b / d} + :: 0 < d && 0 <= a - a % d <= b < a + d - a % d ==> a / d == b / d { - forall a: int, b: int, d: int | 0 < d && 0 <= a - a % d <= b < a + d - a % d + forall a: int, b: int, d: int | 0 < d && 0 <= a - a % d <= b < a + d - a % d ensures a / d == b / d { LemmaIndistinguishableQuotients(a, b, d); - } + } } /* common factors from the dividend and divisor of a modulus operation can be factored out */ @@ -651,30 +651,30 @@ module {:options "-functionSyntax:4"} DivMod { LemmaMulNonnegativeAuto(); calc { b * x; - { LemmaFundamentalDivMod(b * x, b * c); } + { LemmaFundamentalDivMod(b * x, b * c); } (b * c) * ((b * x) / (b * c)) + (b * x) % (b * c); - { LemmaDivDenominator(b * x, b, c); } + { LemmaDivDenominator(b * x, b, c); } (b * c) * (((b * x) / b) / c) + (b * x) % (b * c); - { LemmaMulIsCommutativeAuto(); LemmaDivByMultiple(x, b); } + { LemmaMulIsCommutativeAuto(); LemmaDivByMultiple(x, b); } (b * c) * (x / c) + (b * x) % (b * c); } calc ==> { true; - { LemmaFundamentalDivMod(x, c); } + { LemmaFundamentalDivMod(x, c); } x == c * (x / c) + x % c; b * x == b * (c * (x / c) + x % c); - { LemmaMulIsDistributiveAuto(); } + { LemmaMulIsDistributiveAuto(); } b * x == b * (c * (x / c)) + b * (x % c); - { LemmaMulIsAssociativeAuto(); } + { LemmaMulIsAssociativeAuto(); } b * x == (b * c) * (x / c) + b * (x % c); } } lemma LemmaTruncateMiddleAuto() - ensures forall x: int, b: int, c: int {:trigger b * (x % c)} - :: 0 <= x && 0 < b && 0 < c && 0 < b * c ==> (b * x) % (b * c) == b * (x % c) + ensures forall x: int, b: int, c: int {:trigger b * (x % c)} + :: 0 <= x && 0 < b && 0 < c && 0 < b * c ==> (b * x) % (b * c) == b * (x % c) { - forall x: int, b: int, c: int | 0 <= x && 0 < b && 0 < c && 0 < b * c + forall x: int, b: int, c: int | 0 <= x && 0 < b && 0 < c && 0 < b * c ensures (b * x) % (b * c) == b * (x % c) { LemmaTruncateMiddle(x, b, c); @@ -692,18 +692,18 @@ module {:options "-functionSyntax:4"} DivMod { LemmaMulStrictlyPositive(x,d); calc { (x * a) / (x * d); - { - LemmaMulNonnegative(x, a); - LemmaDivDenominator(x * a, x, d); } + { + LemmaMulNonnegative(x, a); + LemmaDivDenominator(x * a, x, d); } ((x * a) / x) / d; - { LemmaDivMultiplesVanish(a, x); } + { LemmaDivMultiplesVanish(a, x); } a / d; } } lemma LemmaDivMultiplesVanishQuotientAuto() - ensures forall x: int, a: int, d: int {:trigger a / d, x * d, x * a} - :: 0 < x && 0 <= a && 0 < d ==> 0 < x * d && a / d == (x * a) / (x * d) + ensures forall x: int, a: int, d: int {:trigger a / d, x * d, x * a} + :: 0 < x && 0 <= a && 0 < d ==> 0 < x * d && a / d == (x * a) / (x * d) { forall x: int, a: int, d: int | 0 < x && 0 <= a && 0 < d ensures 0 < x * d && a / d == (x * a) / (x * d) @@ -725,8 +725,8 @@ module {:options "-functionSyntax:4"} DivMod { } lemma LemmaRoundDownAuto() - ensures forall a: int, r: int, d: int {:trigger d * ((a + r) / d)} - :: 0 < d && a % d == 0 && 0 <= r < d ==> a == d * ((a + r) / d) + ensures forall a: int, r: int, d: int {:trigger d * ((a + r) / d)} + :: 0 < d && a % d == 0 && 0 <= r < d ==> a == d * ((a + r) / d) { forall a: int, r: int, d: int | 0 < d && a % d == 0 && 0 <= r < d ensures a == d * ((a + r) / d) @@ -749,9 +749,9 @@ module {:options "-functionSyntax:4"} DivMod { lemma LemmaDivMultiplesVanishFancyAuto() ensures forall x: int, b: int, d: int {:trigger (d * x + b) / d} - :: 0 < d && 0 <= b < d ==> (d * x + b) / d == x + :: 0 < d && 0 <= b < d ==> (d * x + b) / d == x { - forall x: int, b: int, d: int | 0 < d && 0 <= b < d + forall x: int, b: int, d: int | 0 < d && 0 <= b < d ensures (d * x + b) / d == x { LemmaDivMultiplesVanishFancy(x, b, d); @@ -769,7 +769,7 @@ module {:options "-functionSyntax:4"} DivMod { lemma LemmaDivMultiplesVanishAuto() ensures forall x: int, d: int {:trigger (d * x) / d} :: 0 < d ==> (d * x) / d == x { - forall x: int, d: int | 0 < d + forall x: int, d: int | 0 < d ensures (d * x) / d == x { LemmaDivMultiplesVanish(x, d); @@ -781,7 +781,7 @@ module {:options "-functionSyntax:4"} DivMod { requires 0 <= b requires 0 < d ensures (b * d) / d == b - { + { LemmaDivMultiplesVanish(b,d); } @@ -793,7 +793,7 @@ module {:options "-functionSyntax:4"} DivMod { { LemmaDivByMultiple(b, d); } - } + } /* a dividend y that is a positive multiple of the divisor z will always yield a greater quotient than a dividend x that is less than y */ @@ -808,15 +808,15 @@ module {:options "-functionSyntax:4"} DivMod { } lemma LemmaDivByMultipleIsStronglyOrderedAuto() - ensures forall x: int, y: int, m: int, z: int {:trigger x / z, m * z, y / z} - :: x < y && y == m * z && 0 < z ==> x / z < y / z + ensures forall x: int, y: int, m: int, z: int {:trigger x / z, m * z, y / z} + :: x < y && y == m * z && 0 < z ==> x / z < y / z { forall x: int, y: int, m: int, z: int | x < y && y == m * z && 0 < z ensures x / z < y / z { LemmaDivByMultipleIsStronglyOrdered(x, y, m, z); } - } + } /* if an integer a is less than or equal to the product of two other integers b and c, then the quotient of a/b will be less than or equal to c */ @@ -891,31 +891,31 @@ module {:options "-functionSyntax:4"} DivMod { LemmaMulStrictlyPositiveAuto(); calc { b * (a / b) % (b * c); - { LemmaFundamentalDivMod(b * (a / b), b * c); } + { LemmaFundamentalDivMod(b * (a / b), b * c); } b * (a / b) - (b * c) * ((b * (a / b)) / (b * c)); - { LemmaMulIsAssociativeAuto(); } + { LemmaMulIsAssociativeAuto(); } b * (a / b) - b * (c * ((b * (a / b)) / (b * c))); - { LemmaMulIsDistributiveAuto(); } + { LemmaMulIsDistributiveAuto(); } b * ((a / b) - (c * ((b * (a / b)) / (b * c)))); } calc ==> { true; - { LemmaModPropertiesAuto(); } + { LemmaModPropertiesAuto(); } b * (a / b) % (b * c) < b * c; b * ((a / b) - (c * ((b * (a / b)) / (b * c)))) < b * c; - { LemmaMulIsCommutativeAuto(); LemmaMulStrictInequalityConverseAuto(); } + { LemmaMulIsCommutativeAuto(); LemmaMulStrictInequalityConverseAuto(); } ((a / b) - (c * ((b * (a / b)) / (b * c)))) < c; ((a / b) - (c * ((b * (a / b)) / (b * c)))) <= c - 1; - { LemmaMulIsCommutativeAuto(); LemmaMulInequalityAuto(); } + { LemmaMulIsCommutativeAuto(); LemmaMulInequalityAuto(); } b * ((a / b) - (c * ((b * (a / b)) / (b * c)))) <= b * (c - 1); b * (a / b) % (b * c) <= b * (c - 1); } } lemma LemmaPartBound1Auto() - ensures forall a: int, b: int, c: int {:trigger b * (a / b) % (b * c)} - :: 0 <= a && 0 < b && 0 < c ==> 0 < b * c && (b * (a / b) % (b * c)) <= b * (c - 1) + ensures forall a: int, b: int, c: int {:trigger b * (a / b) % (b * c)} + :: 0 <= a && 0 < b && 0 < c ==> 0 < b * c && (b * (a / b) % (b * c)) <= b * (c - 1) { forall a: int, b: int, c: int | 0 <= a && 0 < b && 0 < c ensures 0 < b * c && (b * (a / b) % (b * c)) <= b * (c - 1) @@ -925,10 +925,10 @@ module {:options "-functionSyntax:4"} DivMod { } -/******************************************************************************* -* Modulus: -*******************************************************************************/ - + /******************************************************************************* + * Modulus: + *******************************************************************************/ + /* the common syntax of the modulus operation results in the same remainder as recursively calculating the modulus */ lemma LemmaModIsModRecursive(x: int, m: int) @@ -937,32 +937,32 @@ module {:options "-functionSyntax:4"} DivMod { decreases if x < 0 then -x + m else x { reveal ModRecursive(); - if x < 0 { - calc { + if x < 0 { + calc { ModRecursive(x, m); ModRecursive(x + m, m); - { LemmaModIsModRecursive(x + m, m); } + { LemmaModIsModRecursive(x + m, m); } (x + m) % m; - { LemmaAddModNoop(x, m, m); } + { LemmaAddModNoop(x, m, m); } ((x % m) + (m % m)) % m; - { LemmaModBasicsAuto(); } + { LemmaModBasicsAuto(); } (x % m) % m; - { LemmaModBasicsAuto(); } + { LemmaModBasicsAuto(); } x % m; } - } else if x < m { + } else if x < m { LemmaSmallMod(x, m); } else { - calc { + calc { ModRecursive(x, m); ModRecursive(x - m, m); - { LemmaModIsModRecursive(x - m, m); } + { LemmaModIsModRecursive(x - m, m); } (x - m) % m; - { LemmaSubModNoop(x, m, m); } + { LemmaSubModNoop(x, m, m); } ((x % m) - (m % m)) % m; - { LemmaModBasicsAuto(); } + { LemmaModBasicsAuto(); } (x % m) % m; - { LemmaModBasicsAuto(); } + { LemmaModBasicsAuto(); } x % m; } } @@ -1040,7 +1040,7 @@ module {:options "-functionSyntax:4"} DivMod { { calc ==> { x < m; - { LemmaSmallMod(x, m); } + { LemmaSmallMod(x, m); } x % m == x; false; } @@ -1048,7 +1048,7 @@ module {:options "-functionSyntax:4"} DivMod { lemma LemmaModIsZeroAuto() ensures forall x: nat, m: nat {:trigger x % m} :: (x > 0 && m > 0 - && x % m == 0) ==> x >= m + && x % m == 0) ==> x >= m { forall x: nat, m: nat | x > 0 && m > 0 && x % m == 0 ensures x >= m @@ -1056,7 +1056,7 @@ module {:options "-functionSyntax:4"} DivMod { LemmaModIsZero(x, m); } } - + /* a dividend that is any multiple of the divisor will result in a remainder of 0 */ lemma LemmaModMultiplesBasic(x: int, m: int) requires m > 0 @@ -1088,7 +1088,7 @@ module {:options "-functionSyntax:4"} DivMod { lemma LemmaModAddMultiplesVanishAuto() ensures forall b: int, m: int {:trigger b % m} :: 0 < m ==> (m + b) % m == b % m { - forall b: int, m: int | 0 < m + forall b: int, m: int | 0 < m ensures (m + b) % m == b % m { LemmaModAddMultiplesVanish(b, m); @@ -1107,7 +1107,7 @@ module {:options "-functionSyntax:4"} DivMod { lemma LemmaModSubMultiplesVanishAuto() ensures forall b: int, m: int {:trigger b % m} :: 0 < m ==> (-m + b) % m == b % m { - forall b: int, m: int | 0 < m + forall b: int, m: int | 0 < m ensures (-m + b) % m == b % m { LemmaModSubMultiplesVanish(b, m); @@ -1115,7 +1115,7 @@ module {:options "-functionSyntax:4"} DivMod { } /* the remainder of adding any multiple of the divisor m to the dividend b will be the same - as simply performing b % m */ + as simply performing b % m */ lemma LemmaModMultiplesVanish(a: int, b: int, m: int) decreases if a > 0 then a else -a requires 0 < m @@ -1146,7 +1146,7 @@ module {:options "-functionSyntax:4"} DivMod { lemma LemmaModSubtractionAuto() ensures forall x: nat, s: nat, d: nat {:trigger (x - s) % d} - :: 0 < d && 0 <= s <= x % d ==> x % d - s % d == (x - s) % d + :: 0 < d && 0 <= s <= x % d ==> x % d - s % d == (x - s) % d { forall x: nat, s: nat, d: nat | 0 < d && 0 <= s <= x % d ensures x % d - s % d == (x - s) % d @@ -1154,7 +1154,7 @@ module {:options "-functionSyntax:4"} DivMod { LemmaModSubtraction(x, s, d); } } - + /* describes expanded and succinct version of modulus operator in relation to addition (read "ensures") */ lemma LemmaAddModNoop(x: int, y: int, m: int) requires 0 < m @@ -1165,9 +1165,9 @@ module {:options "-functionSyntax:4"} DivMod { lemma LemmaAddModNoopAuto() ensures forall x: int, y: int, m: int {:trigger (x + y) % m} - :: 0 < m ==> ((x % m) + (y % m)) % m == (x + y) % m + :: 0 < m ==> ((x % m) + (y % m)) % m == (x + y) % m { - forall x: int, y: int, m: int | 0 < m + forall x: int, y: int, m: int | 0 < m ensures ((x % m) + (y % m)) % m == (x + y) % m { LemmaAddModNoop(x, y, m); @@ -1184,7 +1184,7 @@ module {:options "-functionSyntax:4"} DivMod { lemma LemmaAddModNoopRightAuto() ensures forall x: int, y: int, m: int {:trigger (x + y) % m} - :: 0 < m ==> (x + (y % m)) % m == (x + y) % m + :: 0 < m ==> (x + (y % m)) % m == (x + y) % m { forall x: int, y: int, m: int | 0 < m ensures (x + (y % m)) % m == (x + y) % m @@ -1202,8 +1202,8 @@ module {:options "-functionSyntax:4"} DivMod { } lemma LemmaSubModNoopAuto() - ensures forall x: int, y: int, m: int {:trigger (x - y) % m} - :: 0 < m ==> ((x % m) - (y % m)) % m == (x - y) % m + ensures forall x: int, y: int, m: int {:trigger (x - y) % m} + :: 0 < m ==> ((x % m) - (y % m)) % m == (x - y) % m { forall x: int, y: int, m: int | 0 < m ensures ((x % m) - (y % m)) % m == (x - y) % m @@ -1221,8 +1221,8 @@ module {:options "-functionSyntax:4"} DivMod { } lemma LemmaSubModNoopRightAuto() - ensures forall x: int, y: int, m: int {:trigger (x - y) % m} - :: 0 < m ==> (x - (y % m)) % m == (x - y) % m + ensures forall x: int, y: int, m: int {:trigger (x - y) % m} + :: 0 < m ==> (x - (y % m)) % m == (x - y) % m { forall x: int, y: int, m: int | 0 < m ensures (x - (y % m)) % m == (x - y) % m @@ -1242,13 +1242,13 @@ module {:options "-functionSyntax:4"} DivMod { } lemma LemmaModAddsAuto() - ensures forall a: int, b: int, d: int {:trigger (a + b) % d} - :: 0 < d ==> a % d + b % d == (a + b) % d + d * ((a % d + b % d) / d) - && (a % d + b % d) < d ==> a % d + b % d == (a + b) % d + ensures forall a: int, b: int, d: int {:trigger (a + b) % d} + :: 0 < d ==> a % d + b % d == (a + b) % d + d * ((a % d + b % d) / d) + && (a % d + b % d) < d ==> a % d + b % d == (a + b) % d { forall a: int, b: int, d: int | 0 < d - ensures a % d + b % d == (a + b) % d + d * ((a % d + b % d) / d) - && (a % d + b % d) < d ==> a % d + b % d == (a + b) % d + ensures a % d + b % d == (a + b) % d + d * ((a % d + b % d) / d) + && (a % d + b % d) < d ==> a % d + b % d == (a + b) % d { LemmaModAdds(a, b, d); } @@ -1258,8 +1258,8 @@ module {:options "-functionSyntax:4"} DivMod { requires 0 < d ensures x % d == (x * (1 - d)) % d { - forall ensures (x - x * d) % d == x % d - { + assert (x - x * d) % d == x % d + by { LemmaModAuto(d); var f := i => (x - i * d) % d == x % d; assert MulAuto() ==> && f(0) @@ -1269,13 +1269,13 @@ module {:options "-functionSyntax:4"} DivMod { } LemmaMulAuto(); } - + /* proves the validity of the quotient and remainder */ lemma {:timeLimitMultiplier 5} LemmaFundamentalDivModConverse(x: int, d: int, q: int, r: int) requires d != 0 requires 0 <= r < d requires x == q * d + r - ensures q == x / d + ensures q == x / d ensures r == x % d { LemmaDivAuto(d); @@ -1285,7 +1285,7 @@ module {:options "-functionSyntax:4"} DivMod { lemma {:timeLimitMultiplier 5} LemmaFundamentalDivModConverseAuto() ensures forall x: int, d: int, q: int, r: int {:trigger q * d + r, x % d} - :: d != 0 && 0 <= r < d && x == q * d + r ==> q == x / d && r == x % d + :: d != 0 && 0 <= r < d && x == q * d + r ==> q == x / d && r == x % d { forall x: int, d: int, q: int, r: int | d != 0 && 0 <= r < d && x == q * d + r ensures q == x / d && r == x % d @@ -1308,13 +1308,13 @@ module {:options "-functionSyntax:4"} DivMod { lemma LemmaModPosBoundAuto() ensures forall x: int, m: int {:trigger x % m} :: 0 <= x && 0 < m ==> 0 <= x % m < m { - forall x: int, m: int | 0 <= x && 0 < m + forall x: int, m: int | 0 <= x && 0 < m ensures 0 <= x % m < m { LemmaModPosBound(x, m); } } - + lemma LemmaMulModNoopLeft(x: int, y: int, m: int) requires 0 < m ensures (x % m) * y % m == x * y % m @@ -1332,7 +1332,7 @@ module {:options "-functionSyntax:4"} DivMod { LemmaMulModNoopLeft(x, y, m); } } - + lemma LemmaMulModNoopRight(x: int, y: int, m: int) requires 0 < m ensures x * (y % m) % m == (x * y) % m @@ -1342,16 +1342,16 @@ module {:options "-functionSyntax:4"} DivMod { } lemma LemmaMulModNoopRightAuto() - ensures forall x: int, y: int, m: int {:trigger (x * y) % m} - :: 0 < m ==> x * (y % m) % m == (x * y) % m + ensures forall x: int, y: int, m: int {:trigger (x * y) % m} + :: 0 < m ==> x * (y % m) % m == (x * y) % m { - forall x: int, y: int, m: int | 0 < m + forall x: int, y: int, m: int | 0 < m ensures x * (y % m) % m == (x * y) % m { LemmaMulModNoopRight(x, y, m); } } - + /* combines previous no-op mod lemmas into a general, overarching lemma */ lemma LemmaMulModNoopGeneral(x: int, y: int, m: int) requires 0 < m @@ -1367,7 +1367,7 @@ module {:options "-functionSyntax:4"} DivMod { lemma LemmaMulModNoopGeneralAuto() ensures forall x: int, y: int, m: int {:trigger (x * y) % m} - :: 0 < m ==> ((x % m) * y) % m == (x * (y % m)) % m == ((x % m) * (y % m)) % m == (x * y) % m + :: 0 < m ==> ((x % m) * y) % m == (x * (y % m)) % m == ((x % m) * (y % m)) % m == (x * y) % m { forall x: int, y: int, m: int | 0 < m ensures ((x % m) * y) % m == (x * (y % m)) % m == ((x % m) * (y % m)) % m == (x * y) % m @@ -1375,7 +1375,7 @@ module {:options "-functionSyntax:4"} DivMod { LemmaMulModNoopGeneral(x, y, m); } } - + lemma LemmaMulModNoop(x: int, y: int, m: int) requires 0 < m ensures (x % m) * (y % m) % m == (x * y) % m @@ -1384,8 +1384,8 @@ module {:options "-functionSyntax:4"} DivMod { } lemma LemmaMulModNoopAuto() - ensures forall x: int, y: int, m: int {:trigger (x * y) % m} - :: 0 < m ==> (x % m) * (y % m) % m == (x * y) % m + ensures forall x: int, y: int, m: int {:trigger (x * y) % m} + :: 0 < m ==> (x % m) * (y % m) % m == (x * y) % m { forall x: int, y: int, m: int | 0 < m ensures (x % m) * (y % m) % m == (x * y) % m @@ -1403,10 +1403,10 @@ module {:options "-functionSyntax:4"} DivMod { } lemma LemmaModEquivalenceAuto() - ensures forall x: int, y: int, m: int {:trigger x % m , y % m} - :: 0 < m && x % m == y % m <==> 0 < m && (x - y) % m == 0 + ensures forall x: int, y: int, m: int {:trigger x % m , y % m} + :: 0 < m && x % m == y % m <==> 0 < m && (x - y) % m == 0 { - forall x: int, y: int, m: int | 0 < m + forall x: int, y: int, m: int | 0 < m ensures x % m == y % m <==> 0 < m && (x - y) % m == 0 { LemmaModEquivalence(x, y, m); @@ -1434,8 +1434,8 @@ module {:options "-functionSyntax:4"} DivMod { lemma LemmaModMulEquivalentAuto() ensures forall x: int, y: int, z: int, m: int - {:trigger IsModEquivalent(x * z, y * z, m)} - :: m > 0 && IsModEquivalent(x, y, m) ==> IsModEquivalent(x * z, y * z, m) + {:trigger IsModEquivalent(x * z, y * z, m)} + :: m > 0 && IsModEquivalent(x, y, m) ==> IsModEquivalent(x * z, y * z, m) { forall x: int, y: int, z: int, m: int | m > 0 && IsModEquivalent(x, y, m) ensures IsModEquivalent(x * z, y * z, m) @@ -1454,31 +1454,31 @@ module {:options "-functionSyntax:4"} DivMod { LemmaMulStrictlyIncreases(d,k); calc { x % d + d * (x / d); - { LemmaFundamentalDivMod(x, d); } + { LemmaFundamentalDivMod(x, d); } x; - { LemmaFundamentalDivMod(x, d * k); } + { LemmaFundamentalDivMod(x, d * k); } x % (d * k) + (d * k) * (x / (d * k)); - { LemmaMulIsAssociativeAuto(); } + { LemmaMulIsAssociativeAuto(); } x % (d * k) + d * (k * (x / (d * k))); } calc { x % d; - { LemmaModPropertiesAuto(); } + { LemmaModPropertiesAuto(); } (x % d) % d; - { LemmaModMultiplesVanish(x / d - k * (x / (d * k)), x % d, d); } + { LemmaModMultiplesVanish(x / d - k * (x / (d * k)), x % d, d); } (x % d + d * (x / d - k * (x / (d * k)))) % d; - { LemmaMulIsDistributiveSubAuto(); } + { LemmaMulIsDistributiveSubAuto(); } (x % d + d * (x / d) - d * (k * (x / (d * k)))) % d; (x % (d * k)) % d; - <= { LemmaModPropertiesAuto(); - LemmaModDecreases(x % (d * k), d); } + <= { LemmaModPropertiesAuto(); + LemmaModDecreases(x % (d * k), d); } x % (d * k); } } lemma LemmaModOrderingAuto() - ensures forall x: int, k: int, d: int {:trigger x % (d * k)} - :: 1 < d && 0 < k ==> 0 < d * k && x % d <= x % (d * k) + ensures forall x: int, k: int, d: int {:trigger x % (d * k)} + :: 1 < d && 0 < k ==> 0 < d * k && x % d <= x % (d * k) { forall x: int, k: int, d: int | 1 < d && 0 < k ensures d * k > 0 && x % d <= x % (d * k) @@ -1486,7 +1486,7 @@ module {:options "-functionSyntax:4"} DivMod { LemmaModOrdering(x, k, d); } } - + lemma LemmaModMod(x: int, a: int, b: int) requires 0 < a requires 0 < b @@ -1496,13 +1496,13 @@ module {:options "-functionSyntax:4"} DivMod { LemmaMulStrictlyPositiveAuto(); calc { x; - { LemmaFundamentalDivMod(x, a * b); } + { LemmaFundamentalDivMod(x, a * b); } (a * b) * (x / (a * b)) + x % (a * b); - { LemmaMulIsAssociativeAuto(); } + { LemmaMulIsAssociativeAuto(); } a * (b * (x / (a * b))) + x % (a * b); - { LemmaFundamentalDivMod(x % (a * b), a); } + { LemmaFundamentalDivMod(x % (a * b), a); } a * (b * (x / (a * b))) + a * (x % (a * b) / a) + (x % (a * b)) % a; - { LemmaMulIsDistributiveAuto(); } + { LemmaMulIsDistributiveAuto(); } a * (b * (x / (a * b)) + x % (a * b) / a) + (x % (a * b)) % a; } LemmaModPropertiesAuto(); @@ -1511,10 +1511,10 @@ module {:options "-functionSyntax:4"} DivMod { } lemma LemmaModModAuto() - ensures forall x: int, a: int, b: int {:trigger a * b, x % a} - :: 0 < a && 0 < b ==> 0 < a * b && (x % (a * b)) % a == x % a + ensures forall x: int, a: int, b: int {:trigger a * b, x % a} + :: 0 < a && 0 < b ==> 0 < a * b && (x % (a * b)) % a == x % a { - forall x: int, a: int, b: int | 0 < a && 0 < b + forall x: int, a: int, b: int | 0 < a && 0 < b ensures 0 < a * b && (x % (a * b)) % a == x % a { LemmaModMod(x, a, b); @@ -1542,7 +1542,7 @@ module {:options "-functionSyntax:4"} DivMod { lemma LemmaPartBound2Auto() ensures forall x: int, y: int, z: int {:trigger y * z, x % y} - :: 0 <= x && 0 < y && 0 < z ==> y * z > 0 && (x % y) % (y * z) < y + :: 0 <= x && 0 < y && 0 < z ==> y * z > 0 && (x % y) % (y * z) < y { forall x: int, y: int, z: int | 0 <= x && 0 < y && 0 < z ensures y * z > 0 && (x % y) % (y * z) < y @@ -1566,48 +1566,48 @@ module {:options "-functionSyntax:4"} DivMod { calc { (y * (x / y)) % (y * z) + (x % y) % (y * z); - <= { LemmaPartBound1(x, y, z); } + <= { LemmaPartBound1(x, y, z); } y * (z - 1) + (x % y) % (y * z); - < { LemmaPartBound2(x, y, z); } + < { LemmaPartBound2(x, y, z); } y * (z - 1) + y; - { LemmaMulBasicsAuto(); } + { LemmaMulBasicsAuto(); } y * (z - 1) + y * 1; - { LemmaMulIsDistributiveAuto(); } + { LemmaMulIsDistributiveAuto(); } y * (z - 1 + 1); y * z; } calc { x % (y * z); - { LemmaFundamentalDivMod(x, y); } - (y * (x / y) + x% y) % (y * z); - { - LemmaModPropertiesAuto(); - assert 0 <= x % y; - LemmaMulNonnegative(y, x / y); - assert (y * (x / y)) % (y * z) + (x % y) % (y * z) < y * z; - LemmaModAdds(y * (x / y), x % y, y * z); - } - (y * (x / y)) % (y * z) + (x % y) % (y * z); - { - LemmaModPropertiesAuto(); - LemmaMulIncreases(z, y); - LemmaMulIsCommutativeAuto(); - assert x % y < y <= y * z; - LemmaSmallMod(x % y, y * z); - assert (x % y) % (y * z) == x % y; - } - (y * (x / y)) % (y * z) + x % y; - { LemmaTruncateMiddle(x / y, y, z); } - y * ((x / y) % z) + x % y; + { LemmaFundamentalDivMod(x, y); } + (y * (x / y) + x% y) % (y * z); + { + LemmaModPropertiesAuto(); + assert 0 <= x % y; + LemmaMulNonnegative(y, x / y); + assert (y * (x / y)) % (y * z) + (x % y) % (y * z) < y * z; + LemmaModAdds(y * (x / y), x % y, y * z); + } + (y * (x / y)) % (y * z) + (x % y) % (y * z); + { + LemmaModPropertiesAuto(); + LemmaMulIncreases(z, y); + LemmaMulIsCommutativeAuto(); + assert x % y < y <= y * z; + LemmaSmallMod(x % y, y * z); + assert (x % y) % (y * z) == x % y; + } + (y * (x / y)) % (y * z) + x % y; + { LemmaTruncateMiddle(x / y, y, z); } + y * ((x / y) % z) + x % y; } } lemma LemmaModBreakdownAuto() ensures forall x: int, y: int, z: int {:trigger x % (y * z)} - :: 0 <= x && 0 < y && 0 < z ==> y * z > 0 && x % (y * z) == y * ((x / y) % z) + x % y + :: 0 <= x && 0 < y && 0 < z ==> y * z > 0 && x % (y * z) == y * ((x / y) % z) + x % y { - forall x: int, y: int, z: int | 0 <= x && 0 < y && 0 < z + forall x: int, y: int, z: int | 0 <= x && 0 < y && 0 < z ensures y * z > 0 && x % (y * z) == y * ((x / y) % z) + x % y { LemmaModBreakdown(x, y, z); diff --git a/src/NonlinearArithmetic/Internals/DivInternals.dfy b/src/NonlinearArithmetic/Internals/DivInternals.dfy index 33c9fa33..921a2fea 100644 --- a/src/NonlinearArithmetic/Internals/DivInternals.dfy +++ b/src/NonlinearArithmetic/Internals/DivInternals.dfy @@ -1,12 +1,12 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" +// RUN: %verify --disable-nonlinear-arithmetic "%s" /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original: Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ /* lemmas and functions in this file are used in the proofs in DivMod.dfy @@ -83,12 +83,12 @@ module {:options "-functionSyntax:4"} DivInternals { && (forall x: int {:trigger x / n} :: 0 <= x < n <==> x / n == 0) && (forall x: int, y: int {:trigger (x + y) / n} :: (var z := (x % n) + (y % n); - ((0 <= z < n && (x + y) / n == x / n + y / n) || - (n <= z < n + n && (x + y) / n == x / n + y / n + 1)))) + ((0 <= z < n && (x + y) / n == x / n + y / n) || + (n <= z < n + n && (x + y) / n == x / n + y / n + 1)))) && (forall x: int, y: int {:trigger (x - y) / n} :: (var z := (x % n) - (y % n); - ((0 <= z < n && (x - y) / n == x / n - y / n) || - (-n <= z < 0 && (x - y) / n == x / n - y / n - 1)))) + ((0 <= z < n && (x - y) / n == x / n - y / n) || + (-n <= z < 0 && (x - y) / n == x / n - y / n - 1)))) } /* Ensures that DivAuto is true */ @@ -102,13 +102,13 @@ module {:options "-functionSyntax:4"} DivInternals { assert (0 - n) / n == -1; forall x:int, y:int {:trigger (x + y) / n} ensures var z := (x % n) + (y % n); - (|| (0 <= z < n && (x + y) / n == x / n + y / n) - || (n <= z < 2 * n && (x + y) / n == x / n + y / n + 1)) + (|| (0 <= z < n && (x + y) / n == x / n + y / n) + || (n <= z < 2 * n && (x + y) / n == x / n + y / n + 1)) { var f := (xx:int, yy:int) => - (var z := (xx % n) + (yy % n); - ( (0 <= z < n && (xx + yy) / n == xx / n + yy / n) - || (n <= z < 2 * n && (xx + yy) / n == xx / n + yy / n + 1))); + (var z := (xx % n) + (yy % n); + ( (0 <= z < n && (xx + yy) / n == xx / n + yy / n) + || (n <= z < 2 * n && (xx + yy) / n == xx / n + yy / n + 1))); forall i, j ensures j >= 0 && f(i, j) ==> f(i, j + n) ensures i < n && f(i, j) ==> f(i - n, j) @@ -133,13 +133,13 @@ module {:options "-functionSyntax:4"} DivInternals { } forall x:int, y:int {:trigger (x - y) / n} ensures var z := (x % n) - (y % n); - (|| (0 <= z < n && (x - y) / n == x / n - y / n) - || (-n <= z < 0 && (x - y) / n == x / n - y / n - 1)) + (|| (0 <= z < n && (x - y) / n == x / n - y / n) + || (-n <= z < 0 && (x - y) / n == x / n - y / n - 1)) { var f := (xx:int, yy:int) => - (var z := (xx % n) - (yy % n); - ( (0 <= z < n && (xx - yy) / n == xx / n - yy / n) - || (-n <= z < 0 && (xx - yy) / n == xx / n - yy / n - 1))); + (var z := (xx % n) - (yy % n); + ( (0 <= z < n && (xx - yy) / n == xx / n - yy / n) + || (-n <= z < 0 && (xx - yy) / n == xx / n - yy / n - 1))); forall i, j ensures j >= 0 && f(i, j) ==> f(i, j + n) ensures i < n && f(i, j) ==> f(i - n, j) @@ -168,8 +168,8 @@ module {:options "-functionSyntax:4"} DivInternals { lemma LemmaDivInductionAuto(n: int, x: int, f: int->bool) requires n > 0 requires DivAuto(n) ==> && (forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && i < n ==> f(i)) - && (forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && f(i) ==> f(i + n)) - && (forall i {:trigger IsLe(i + 1, n)} :: IsLe(i + 1, n) && f(i) ==> f(i - n)) + && (forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && f(i) ==> f(i + n)) + && (forall i {:trigger IsLe(i + 1, n)} :: IsLe(i + 1, n) && f(i) ==> f(i - n)) ensures DivAuto(n) ensures f(x) { @@ -185,8 +185,8 @@ module {:options "-functionSyntax:4"} DivInternals { lemma LemmaDivInductionAutoForall(n:int, f:int->bool) requires n > 0 requires DivAuto(n) ==> && (forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && i < n ==> f(i)) - && (forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && f(i) ==> f(i + n)) - && (forall i {:trigger IsLe(i + 1, n)} :: IsLe(i + 1, n) && f(i) ==> f(i - n)) + && (forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && f(i) ==> f(i + n)) + && (forall i {:trigger IsLe(i + 1, n)} :: IsLe(i + 1, n) && f(i) ==> f(i - n)) ensures DivAuto(n) ensures forall i {:trigger f(i)} :: f(i) { diff --git a/src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy b/src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy index 94bc252f..a9f8de03 100644 --- a/src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy +++ b/src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy @@ -1,12 +1,12 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original: Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ module {:options "-functionSyntax:4"} DivInternalsNonlinear { @@ -17,30 +17,30 @@ module {:options "-functionSyntax:4"} DivInternalsNonlinear { lemma LemmaDivOf0(d:int) requires d != 0 ensures 0 / d == 0 - { + { } /* the quotient of an integer divided by itself is 1 */ lemma LemmaDivBySelf(d:int) requires d != 0 ensures d / d == 1 - { + { } /* dividing a smaller integer by a larger integer results in a quotient of 0 */ lemma LemmaSmallDiv() ensures forall x, d {:trigger x / d} :: 0 <= x < d && d > 0 ==> x / d == 0 - { + { } /* the quotient of dividing a positive real number (not 0) by a smaller positive real number - will be greater than 1 */ + will be greater than 1 */ lemma LemmaRealDivGt(x:real, y:real) requires x > y requires x >= 0.0 requires y > 0.0 ensures x / y > 1 as real - { + { } - + } diff --git a/src/NonlinearArithmetic/Internals/GeneralInternals.dfy b/src/NonlinearArithmetic/Internals/GeneralInternals.dfy index 4be213fc..15073cda 100644 --- a/src/NonlinearArithmetic/Internals/GeneralInternals.dfy +++ b/src/NonlinearArithmetic/Internals/GeneralInternals.dfy @@ -1,19 +1,19 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" +// RUN: %verify --disable-nonlinear-arithmetic "%s" /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original: Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ module {:options "-functionSyntax:4"} GeneralInternals { /* this predicate is primarily used as a trigger */ - ghost predicate IsLe(x: int, y: int) - { - x <= y + ghost predicate IsLe(x: int, y: int) + { + x <= y } /* aids in the process of induction for modulus */ diff --git a/src/NonlinearArithmetic/Internals/ModInternals.dfy b/src/NonlinearArithmetic/Internals/ModInternals.dfy index 188f3410..d192970e 100644 --- a/src/NonlinearArithmetic/Internals/ModInternals.dfy +++ b/src/NonlinearArithmetic/Internals/ModInternals.dfy @@ -1,12 +1,12 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" +// RUN: %verify --disable-nonlinear-arithmetic "%s" /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original: Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ /* lemmas and functions in this file are used in the proofs in DivMod.dfy @@ -46,7 +46,7 @@ module {:options "-functionSyntax:4"} ModInternals { ModRecursive(x - d, d) } - /* performs induction on modulus */ + /* performs induction on modulus */ lemma LemmaModInductionForall(n: int, f: int -> bool) requires n > 0 requires forall i :: 0 <= i < n ==> f(i) @@ -199,22 +199,22 @@ module {:options "-functionSyntax:4"} ModInternals { /* automates the modulus operator process */ ghost predicate ModAuto(n: int) - requires n > 0; + requires n > 0; { - && (n % n == (-n) % n == 0) - && (forall x: int {:trigger (x % n) % n} :: (x % n) % n == x % n) - && (forall x: int {:trigger x % n} :: 0 <= x < n <==> x % n == x) - && (forall x: int, y: int {:trigger (x + y) % n} :: - (var z := (x % n) + (y % n); - ( (0 <= z < n && (x + y) % n == z) - || (n <= z < n + n && (x + y) % n == z - n)))) - && (forall x: int, y: int {:trigger (x - y) % n} :: - (var z := (x % n) - (y % n); - ( (0 <= z < n && (x - y) % n == z) - || (-n <= z < 0 && (x - y) % n == z + n)))) + && (n % n == (-n) % n == 0) + && (forall x: int {:trigger (x % n) % n} :: (x % n) % n == x % n) + && (forall x: int {:trigger x % n} :: 0 <= x < n <==> x % n == x) + && (forall x: int, y: int {:trigger (x + y) % n} :: + (var z := (x % n) + (y % n); + ( (0 <= z < n && (x + y) % n == z) + || (n <= z < n + n && (x + y) % n == z - n)))) + && (forall x: int, y: int {:trigger (x - y) % n} :: + (var z := (x % n) - (y % n); + ( (0 <= z < n && (x - y) % n == z) + || (-n <= z < 0 && (x - y) % n == z + n)))) } -/* ensures that ModAuto is true */ + /* ensures that ModAuto is true */ lemma LemmaModAuto(n: int) requires n > 0 ensures ModAuto(n) @@ -267,8 +267,8 @@ module {:options "-functionSyntax:4"} ModInternals { lemma LemmaModInductionAuto(n: int, x: int, f: int -> bool) requires n > 0 requires ModAuto(n) ==> && (forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && i < n ==> f(i)) - && (forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && f(i) ==> f(i + n)) - && (forall i {:trigger IsLe(i + 1, n)} :: IsLe(i + 1, n) && f(i) ==> f(i - n)) + && (forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && f(i) ==> f(i + n)) + && (forall i {:trigger IsLe(i + 1, n)} :: IsLe(i + 1, n) && f(i) ==> f(i - n)) ensures ModAuto(n) ensures f(x) { @@ -285,8 +285,8 @@ module {:options "-functionSyntax:4"} ModInternals { lemma LemmaModInductionAutoForall(n: int, f: int -> bool) requires n > 0 requires ModAuto(n) ==> && (forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && i < n ==> f(i)) - && (forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && f(i) ==> f(i + n)) - && (forall i {:trigger IsLe(i + 1, n)} :: IsLe(i + 1, n) && f(i) ==> f(i - n)) + && (forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && f(i) ==> f(i + n)) + && (forall i {:trigger IsLe(i + 1, n)} :: IsLe(i + 1, n) && f(i) ==> f(i - n)) ensures ModAuto(n) ensures forall i {:trigger f(i)} :: f(i) { diff --git a/src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy b/src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy index e58956ee..69f64943 100644 --- a/src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy +++ b/src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy @@ -1,15 +1,15 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original: Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ module {:options "-functionSyntax:4"} ModInternalsNonlinear { - + /* WARNING: Think three times before adding to this file, as nonlinear verification is highly unstable! */ @@ -17,7 +17,7 @@ module {:options "-functionSyntax:4"} ModInternalsNonlinear { lemma LemmaModOfZeroIsZero(m:int) requires 0 < m ensures 0 % m == 0 - { + { } /* describes fundementals of the modulus operator */ diff --git a/src/NonlinearArithmetic/Internals/MulInternals.dfy b/src/NonlinearArithmetic/Internals/MulInternals.dfy index c6885021..448405d2 100644 --- a/src/NonlinearArithmetic/Internals/MulInternals.dfy +++ b/src/NonlinearArithmetic/Internals/MulInternals.dfy @@ -1,12 +1,12 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" +// RUN: %verify --disable-nonlinear-arithmetic "%s" /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original: Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ /* lemmas and functions in this file are used in the proofs in Mul.dfy */ @@ -26,14 +26,14 @@ module {:options "-functionSyntax:4"} MulInternals { else y + MulPos(x - 1, y) } - /* performs multiplication for both positive and negative integers */ + /* performs multiplication for both positive and negative integers */ function MulRecursive(x: int, y: int) : int { if x >= 0 then MulPos(x, y) else -1 * MulPos(-1 * x, y) } - /* performs induction on multiplication */ + /* performs induction on multiplication */ lemma LemmaMulInduction(f: int -> bool) requires f(0) requires forall i {:trigger f(i), f(i + 1)} :: i >= 0 && f(i) ==> f(i + 1) @@ -113,8 +113,8 @@ module {:options "-functionSyntax:4"} MulInternals { /* performs auto induction for multiplication */ lemma LemmaMulInductionAuto(x: int, f: int -> bool) requires MulAuto() ==> f(0) - && (forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && f(i) ==> f(i + 1)) - && (forall i {:trigger IsLe(i, 0)} :: IsLe(i, 0) && f(i) ==> f(i - 1)) + && (forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && f(i) ==> f(i + 1)) + && (forall i {:trigger IsLe(i, 0)} :: IsLe(i, 0) && f(i) ==> f(i - 1)) ensures MulAuto() ensures f(x) { @@ -129,8 +129,8 @@ module {:options "-functionSyntax:4"} MulInternals { /* performs auto induction on multiplication for all i s.t. f(i) exists */ lemma LemmaMulInductionAutoForall(f: int -> bool) requires MulAuto() ==> f(0) - && (forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && f(i) ==> f(i + 1)) - && (forall i {:trigger IsLe(i, 0)} :: IsLe(i, 0) && f(i) ==> f(i - 1)) + && (forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && f(i) ==> f(i + 1)) + && (forall i {:trigger IsLe(i, 0)} :: IsLe(i, 0) && f(i) ==> f(i - 1)) ensures MulAuto() ensures forall i {:trigger f(i)} :: f(i) { @@ -141,4 +141,4 @@ module {:options "-functionSyntax:4"} MulInternals { LemmaMulInduction(f); } -} +} diff --git a/src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy b/src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy index 164648d0..e6a6cad3 100644 --- a/src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy +++ b/src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy @@ -1,12 +1,12 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original: Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ module {:options "-functionSyntax:4"} MulInternalsNonlinear { @@ -33,7 +33,7 @@ module {:options "-functionSyntax:4"} MulInternalsNonlinear { ensures x * (y + z) == x * y + x * z {} - /* the product of two integers is greater than the value of each individual integer */ + /* the product of two integers is greater than the value of each individual integer */ lemma LemmaMulOrdering(x: int, y: int) requires x != 0 requires y != 0 diff --git a/src/NonlinearArithmetic/Mul.dfy b/src/NonlinearArithmetic/Mul.dfy index 2de1b7f2..805a38c0 100644 --- a/src/NonlinearArithmetic/Mul.dfy +++ b/src/NonlinearArithmetic/Mul.dfy @@ -1,12 +1,12 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" +// RUN: %verify --disable-nonlinear-arithmetic "%s" /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original: Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ /* Every lemma comes in 2 forms: 'LemmaProperty' and 'LemmaPropertyAuto'. The former takes arguments and may be more stable and less reliant on Z3 @@ -41,7 +41,7 @@ module {:options "-functionSyntax:4"} Mul { } /* the built-in syntax of multiplying two positive integers results in the same product as - MulPos, which is achieved by recursive addition */ + MulPos, which is achieved by recursive addition */ lemma LemmaMulIsMulPos(x: int, y: int) requires x >= 0 ensures x * y == MulPos(x, y) @@ -67,7 +67,7 @@ module {:options "-functionSyntax:4"} Mul { { } - /* multiplying two nonzero integers will never result in 0 as the poduct */ + /* multiplying two nonzero integers will never result in 0 as the poduct */ lemma LemmaMulNonzero(x: int, y: int) ensures x * y != 0 <==> x != 0 && y != 0 { @@ -84,7 +84,7 @@ module {:options "-functionSyntax:4"} Mul { LemmaMulNonzero(x, y); } } - + /* any integer multiplied by 0 results in a product of 0 */ lemma LemmaMulByZeroIsZeroAuto() ensures forall x: int {:trigger 0 * x} {:trigger x * 0} :: x * 0 == 0 * x == 0 @@ -105,8 +105,8 @@ module {:options "-functionSyntax:4"} Mul { /* multiplication is always associative for all integers*/ lemma LemmaMulIsAssociativeAuto() - ensures forall x: int, y: int, z: int {:trigger x * (y * z)} {:trigger (x * y) * z} - :: x * (y * z) == (x * y) * z + ensures forall x: int, y: int, z: int {:trigger x * (y * z)} {:trigger (x * y) * z} + :: x * (y * z) == (x * y) * z { forall (x: int, y: int, z: int) ensures x * (y * z) == (x * y) * z @@ -127,7 +127,7 @@ module {:options "-functionSyntax:4"} Mul { { } - /* the product of two integers is greater than the value of each individual integer */ + /* the product of two integers is greater than the value of each individual integer */ lemma LemmaMulOrdering(x: int, y: int) requires x != 0 requires y != 0 @@ -143,7 +143,7 @@ module {:options "-functionSyntax:4"} Mul { ensures forall x: int, y: int {:trigger x * y} :: (0 != x && 0 != y && x * y >= 0) ==> x * y >= x && x * y >= y { forall x: int, y: int | 0 != x && 0 != y && x * y >= 0 - ensures x * y >= x && x * y >= y + ensures x * y >= x && x * y >= y { LemmaMulOrdering(x, y); } @@ -157,7 +157,7 @@ module {:options "-functionSyntax:4"} Mul { lemma LemmaMulEqualityAuto() ensures forall x: int, y: int, z: int {:trigger x * z, y * z } :: x == y ==> x * z == y * z { - forall (x: int, y: int, z: int | x == y) + forall (x: int, y: int, z: int | x == y) ensures x * z == y * z { LemmaMulEquality(x, y, z); @@ -218,7 +218,7 @@ module {:options "-functionSyntax:4"} Mul { lemma LemmaMulUpperBoundAuto() ensures forall x: int, XBound: int, y: int, YBound: int {:trigger x * y, XBound * YBound} - :: x <= XBound && y <= YBound && 0 <= x && 0 <= y ==> x * y <= XBound * YBound + :: x <= XBound && y <= YBound && 0 <= x && 0 <= y ==> x * y <= XBound * YBound { forall (x: int, XBound: int, y: int, YBound: int | x <= XBound && y <= YBound && 0 <= x && 0 <= y) ensures x * y <= XBound * YBound @@ -229,8 +229,8 @@ module {:options "-functionSyntax:4"} Mul { /* the product of two strictly upper bounded integers is less than the product of their upper bounds */ lemma LemmaMulStrictUpperBound(x: int, XBound: int, y: int, YBound: int) - requires x < XBound - requires y < YBound + requires x < XBound + requires y < YBound requires 0 < x requires 0 < y ensures x * y <= (XBound - 1) * (YBound - 1) @@ -240,8 +240,8 @@ module {:options "-functionSyntax:4"} Mul { } lemma LemmaMulStrictUpperBoundAuto() - ensures forall x: int, XBound: int, y: int, YBound: int {:trigger x * y, (XBound - 1) * (YBound - 1)} - :: x < XBound && y < YBound && 0 < x && 0 < y ==> x * y <= (XBound - 1) * (YBound - 1) + ensures forall x: int, XBound: int, y: int, YBound: int {:trigger x * y, (XBound - 1) * (YBound - 1)} + :: x < XBound && y < YBound && 0 < x && 0 < y ==> x * y <= (XBound - 1) * (YBound - 1) { forall (x: int, XBound: int, y: int, YBound: int | x < XBound && y < YBound && 0 < x && 0 < y) ensures x * y <= (XBound - 1) * (YBound - 1) @@ -262,7 +262,7 @@ module {:options "-functionSyntax:4"} Mul { lemma LemmaMulLeftInequalityAuto() ensures forall x: int, y: int, z: int {:trigger x * y, x * z} - :: x > 0 ==> (y <= z ==> x * y <= x * z) && (y < z ==> x * y < x * z) + :: x > 0 ==> (y <= z ==> x * y <= x * z) && (y < z ==> x * y < x * z) { forall (x: int, y: int, z: int | (y <= z || y < z) && 0 < x) ensures (y <= z ==> x * y <= x * z) && (y < z ==> x * y < x * z) @@ -271,8 +271,8 @@ module {:options "-functionSyntax:4"} Mul { } } -/* if two seperate integers are each multiplied by a common integer and the products are equal, the - two original integers are equal */ + /* if two seperate integers are each multiplied by a common integer and the products are equal, the + two original integers are equal */ lemma LemmaMulEqualityConverse(m: int, x: int, y: int) requires m != 0 requires m * x == m * y @@ -283,7 +283,7 @@ module {:options "-functionSyntax:4"} Mul { LemmaMulInductionAuto(m, u => x < y && 0 < u ==> x * u < y * u); LemmaMulInductionAuto(m, u => x < y && 0 > u ==> x * u > y * u); } - + /* if any two seperate integers are each multiplied by a common integer and the products are equal, the two original integers are equal */ lemma LemmaMulEqualityConverseAuto() @@ -331,11 +331,11 @@ module {:options "-functionSyntax:4"} Mul { lemma LemmaMulStrictInequalityConverseAuto() ensures forall x: int, y: int, z: int {:trigger x * z, y * z} :: x * z < y * z && z >= 0 ==> x < y { - forall (x: int, y: int, z: int | x * z < y * z && z >= 0) - ensures x < y; - { - LemmaMulStrictInequalityConverse(x, y, z); - } + forall (x: int, y: int, z: int | x * z < y * z && z >= 0) + ensures x < y; + { + LemmaMulStrictInequalityConverse(x, y, z); + } } /* multiplication is distributive */ @@ -487,7 +487,7 @@ module {:options "-functionSyntax:4"} Mul { { LemmaMulInductionAuto(x, u => 0 <= u ==> 0 <= u * y); } - + /* multiplying any two positive numbers will result in a positive product */ lemma LemmaMulNonnegativeAuto() ensures forall x: int, y: int {:trigger x * y} :: 0 <= x && 0 <= y ==> 0 <= x * y @@ -510,7 +510,7 @@ module {:options "-functionSyntax:4"} Mul { lemma LemmaMulUnaryNegationAuto() ensures forall x: int, y: int {:trigger (-x) * y} {:trigger x * (-y)} :: (-x) * y == -(x * y) == x * (-y) { - forall (x: int, y: int) + forall (x: int, y: int) ensures (-x) * y == -(x * y) == x * (-y) { LemmaMulUnaryNegation(x, y); @@ -528,7 +528,7 @@ module {:options "-functionSyntax:4"} Mul { lemma LemmaMulCancelsNegativesAuto() ensures forall x: int, y: int {:trigger x * y} :: x * y == (-x) * (-y) { - forall x: int, y: int + forall x: int, y: int ensures x * y == (-x) * (-y) { LemmaMulCancelsNegatives(x, y); diff --git a/src/NonlinearArithmetic/Power.dfy b/src/NonlinearArithmetic/Power.dfy index 666e8ee8..4e55851d 100644 --- a/src/NonlinearArithmetic/Power.dfy +++ b/src/NonlinearArithmetic/Power.dfy @@ -1,12 +1,12 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" +// RUN: %verify --disable-nonlinear-arithmetic "%s" /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original: Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ /* Every lemma comes in 2 forms: 'LemmaProperty' and 'LemmaPropertyAuto'. The former takes arguments and may be more stable and less reliant on Z3 @@ -56,11 +56,11 @@ module {:options "-functionSyntax:4"} Power { { calc { Pow(b, 1); - { reveal Pow(); } + { reveal Pow(); } b * Pow(b, 0); - { LemmaPow0(b); } + { LemmaPow0(b); } b * 1; - { LemmaMulBasicsAuto(); } + { LemmaMulBasicsAuto(); } b; } } @@ -148,7 +148,7 @@ module {:options "-functionSyntax:4"} Power { lemma LemmaPowPositiveAuto() ensures forall b: int, e: nat {:trigger Pow(b, e)} - :: b > 0 ==> 0 < Pow(b, e) + :: b > 0 ==> 0 < Pow(b, e) { reveal Pow(); forall b: int, e: nat {:trigger Pow(b, e)} | b > 0 @@ -166,22 +166,22 @@ module {:options "-functionSyntax:4"} Power { if e1 == 0 { calc { Pow(b, e1) * Pow(b, e2); - { LemmaPow0(b); } + { LemmaPow0(b); } 1 * Pow(b, e2); - { LemmaMulBasicsAuto(); } + { LemmaMulBasicsAuto(); } Pow(b, 0 + e2); } } else { calc { Pow(b, e1) * Pow(b, e2); - { reveal Pow(); } + { reveal Pow(); } (b * Pow(b, e1 - 1)) * Pow(b, e2); - { LemmaMulIsAssociativeAuto(); } + { LemmaMulIsAssociativeAuto(); } b * (Pow(b, e1 - 1) * Pow(b, e2)); - { LemmaPowAdds(b, e1 - 1, e2); } + { LemmaPowAdds(b, e1 - 1, e2); } b * Pow(b, e1 - 1 + e2); - { reveal Pow(); } + { reveal Pow(); } Pow(b, e1 + e2); } } @@ -189,7 +189,7 @@ module {:options "-functionSyntax:4"} Power { lemma LemmaPowAddsAuto() ensures forall b: int, e1: nat, e2: nat {:trigger Pow(b, e1 + e2)} - :: Pow(b, e1 + e2) == Pow(b, e1) * Pow(b, e2) + :: Pow(b, e1 + e2) == Pow(b, e1) * Pow(b, e2) { reveal Pow(); forall b: int, e1: nat, e2: nat {:trigger Pow(b, e1 + e2)} @@ -209,7 +209,7 @@ module {:options "-functionSyntax:4"} Power { lemma LemmaPowSubAddCancelAuto() ensures forall b: int, e1: nat, e2: nat {:trigger Pow(b, e1 - e2)} | e1 >= e2 - :: Pow(b, e1 - e2) * Pow(b, e2) == Pow(b, e1) + :: Pow(b, e1 - e2) * Pow(b, e2) == Pow(b, e1) { reveal Pow(); forall b: int, e1: nat, e2: nat | e1 >= e2 @@ -228,9 +228,9 @@ module {:options "-functionSyntax:4"} Power { LemmaPowPositiveAuto(); calc { Pow(b, e2) / Pow(b, e1); - { LemmaPowSubAddCancel(b, e2, e1); } + { LemmaPowSubAddCancel(b, e2, e1); } Pow(b, e2 - e1) * Pow(b, e1) / Pow(b, e1); - { LemmaDivByMultiple(Pow(b, e2 - e1), Pow(b, e1)); } + { LemmaDivByMultiple(Pow(b, e2 - e1), Pow(b, e1)); } Pow(b, e2 - e1); } } @@ -238,8 +238,8 @@ module {:options "-functionSyntax:4"} Power { lemma LemmaPowSubtractsAuto() ensures forall b: nat, e1: nat :: b > 0 ==> Pow(b, e1) > 0 ensures forall b: nat, e1: nat, e2: nat {:trigger Pow(b, e2 - e1)} - :: b > 0 && e1 <= e2 ==> - Pow(b, e2 - e1) == Pow(b, e2) / Pow(b, e1) > 0 + :: b > 0 && e1 <= e2 ==> + Pow(b, e2 - e1) == Pow(b, e2) / Pow(b, e1) > 0 { reveal Pow(); LemmaPowPositiveAuto(); @@ -262,18 +262,18 @@ module {:options "-functionSyntax:4"} Power { LemmaMulBasicsAuto(); calc { Pow(a, b * c); - { LemmaPow0(a); } + { LemmaPow0(a); } 1; - { LemmaPow0(Pow(a, b)); } + { LemmaPow0(Pow(a, b)); } Pow(Pow(a, b), c); } } else { calc { b * c - b; - { LemmaMulBasicsAuto(); } + { LemmaMulBasicsAuto(); } b * c - b * 1; - { LemmaMulIsDistributiveAuto(); } + { LemmaMulIsDistributiveAuto(); } b * (c - 1); } LemmaMulNonnegative(b, c - 1); @@ -282,12 +282,12 @@ module {:options "-functionSyntax:4"} Power { calc { Pow(a, b * c); Pow(a, b + b * c - b); - { LemmaPowAdds(a, b, b * c - b); } + { LemmaPowAdds(a, b, b * c - b); } Pow(a, b) * Pow(a, b * c - b); Pow(a, b) * Pow(a, b * (c - 1)); - { LemmaPowMultiplies(a, b, c - 1); } + { LemmaPowMultiplies(a, b, c - 1); } Pow(a, b) * Pow(Pow(a, b), c - 1); - { reveal Pow(); } + { reveal Pow(); } Pow(Pow(a, b), c); } } @@ -296,7 +296,7 @@ module {:options "-functionSyntax:4"} Power { lemma LemmaPowMultipliesAuto() ensures forall b: nat, c: nat {:trigger b * c} :: 0 <= b * c ensures forall a: int, b: nat, c: nat {:trigger Pow(a, b * c)} - :: Pow(Pow(a, b), c) == Pow(a, b * c) + :: Pow(Pow(a, b), c) == Pow(a, b * c) { reveal Pow(); LemmaMulNonnegativeAuto(); @@ -318,9 +318,9 @@ module {:options "-functionSyntax:4"} Power { calc { Pow(a * b, e); (a * b) * Pow(a * b, e - 1); - { LemmaPowDistributes(a, b, e - 1); } + { LemmaPowDistributes(a, b, e - 1); } (a * b) * (Pow(a, e - 1) * Pow(b, e - 1)); - { LemmaMulIsAssociativeAuto(); LemmaMulIsCommutativeAuto(); } + { LemmaMulIsAssociativeAuto(); LemmaMulIsCommutativeAuto(); } (a * Pow(a, e - 1)) * (b * Pow(b, e - 1)); Pow(a, e) * Pow(b, e); } @@ -329,7 +329,7 @@ module {:options "-functionSyntax:4"} Power { lemma LemmaPowDistributesAuto() ensures forall a: int, b: int, e: nat {:trigger Pow(a * b, e)} - :: Pow(a * b, e) == Pow(a, e) * Pow(b, e) + :: Pow(a * b, e) == Pow(a, e) * Pow(b, e) { reveal Pow(); forall a: int, b: int, e: nat {:trigger Pow(a * b, e)} @@ -379,13 +379,13 @@ module {:options "-functionSyntax:4"} Power { { calc { Pow(b, e1 + i); - <= { LemmaPowPositive(b, e1 + i); - LemmaMulLeftInequality(Pow(b, e1 + i), 1, b); } - Pow(b, e1 + i) * b; - == { LemmaPow1(b); } - Pow(b, e1 + i) * Pow(b, 1); - == { LemmaPowAdds(b, e1 + i, 1); } - Pow(b, e1 + i + 1); + <= { LemmaPowPositive(b, e1 + i); + LemmaMulLeftInequality(Pow(b, e1 + i), 1, b); } + Pow(b, e1 + i) * b; + == { LemmaPow1(b); } + Pow(b, e1 + i) * Pow(b, 1); + == { LemmaPowAdds(b, e1 + i, 1); } + Pow(b, e1 + i + 1); } } LemmaMulInductionAuto(e2 - e1, f); @@ -393,7 +393,7 @@ module {:options "-functionSyntax:4"} Power { lemma LemmaPowStrictlyIncreasesAuto() ensures forall b: nat, e1: nat, e2: nat {:trigger Pow(b, e1), - Pow(b, e2)} :: (1 < b && e1 < e2) ==> Pow(b, e1) < Pow(b, e2) + Pow(b, e2)} :: (1 < b && e1 < e2) ==> Pow(b, e1) < Pow(b, e2) { reveal Pow(); forall b: nat, e1: nat, e2: nat {:trigger Pow(b, e1), Pow(b, e2)} @@ -417,13 +417,13 @@ module {:options "-functionSyntax:4"} Power { { calc { Pow(b, e1 + i); - <= { LemmaPowPositive(b, e1 + i); - LemmaMulLeftInequality(Pow(b, e1 + i), 1, b); } - Pow(b, e1 + i) * b; - == { LemmaPow1(b); } - Pow(b, e1 + i) * Pow(b, 1); - == { LemmaPowAdds(b, e1 + i, 1); } - Pow(b, e1 + i + 1); + <= { LemmaPowPositive(b, e1 + i); + LemmaMulLeftInequality(Pow(b, e1 + i), 1, b); } + Pow(b, e1 + i) * b; + == { LemmaPow1(b); } + Pow(b, e1 + i) * Pow(b, 1); + == { LemmaPowAdds(b, e1 + i, 1); } + Pow(b, e1 + i + 1); } } LemmaMulInductionAuto(e2 - e1, f); @@ -431,7 +431,7 @@ module {:options "-functionSyntax:4"} Power { lemma LemmaPowIncreasesAuto() ensures forall b: nat, e1: nat, e2: nat {:trigger Pow(b, e1), - Pow(b, e2)} :: (1 < b && e1 <= e2) ==> Pow(b, e1) <= Pow(b, e2) + Pow(b, e2)} :: (1 < b && e1 <= e2) ==> Pow(b, e1) <= Pow(b, e2) { reveal Pow(); forall b: nat, e1: nat, e2: nat {:trigger Pow(b, e1), Pow(b, e2)} @@ -457,8 +457,8 @@ module {:options "-functionSyntax:4"} Power { lemma LemmaPowStrictlyIncreasesConverseAuto() ensures forall b: nat, e1: nat, e2: nat - {:trigger Pow(b, e1), Pow(b, e2)} - :: b > 0 && Pow(b, e1) < Pow(b, e2) ==> e1 < e2 + {:trigger Pow(b, e1), Pow(b, e2)} + :: b > 0 && Pow(b, e1) < Pow(b, e2) ==> e1 < e2 { reveal Pow(); forall b: nat, e1: nat, e2: nat {:trigger Pow(b, e1), Pow(b, e2)} @@ -483,8 +483,8 @@ module {:options "-functionSyntax:4"} Power { lemma LemmaPowIncreasesConverseAuto() ensures forall b: nat, e1: nat, e2: nat - {:trigger Pow(b, e1), Pow(b, e2)} - :: 1 < b && Pow(b, e1) <= Pow(b, e2) ==> e1 <= e2 + {:trigger Pow(b, e1), Pow(b, e2)} + :: 1 < b && Pow(b, e1) <= Pow(b, e2) ==> e1 <= e2 { reveal Pow(); forall b: nat, e1: nat, e2: nat {:trigger Pow(b, e1), Pow(b, e2)} @@ -507,9 +507,9 @@ module {:options "-functionSyntax:4"} Power { LemmaPowPositive(b, x); calc { Pow(Pow(b, x * y), z); - { LemmaPowMultiplies(b, x, y); } + { LemmaPowMultiplies(b, x, y); } Pow(Pow(Pow(b, x), y), z); - { LemmaPowMultiplies(Pow(b, x), y, z); } + { LemmaPowMultiplies(Pow(b, x), y, z); } Pow(Pow(b, x), y * z); } } @@ -517,8 +517,8 @@ module {:options "-functionSyntax:4"} Power { lemma LemmaPullOutPowsAuto() ensures forall y: nat, z: nat {:trigger z * y} :: 0 <= z * y && 0 <= y * z ensures forall b: nat, x: nat, y: nat, z: nat - {:trigger Pow(Pow(b, x * y), z)} - :: b > 0 ==> Pow(Pow(b, x * y), z) == Pow(Pow(b, x), y * z) + {:trigger Pow(Pow(b, x * y), z)} + :: b > 0 ==> Pow(Pow(b, x * y), z) == Pow(Pow(b, x), y * z) { reveal Pow(); LemmaMulNonnegativeAuto(); @@ -540,14 +540,14 @@ module {:options "-functionSyntax:4"} Power { LemmaPowPositiveAuto(); calc ==> { x / Pow(b, e2) >= Pow(b, e1 - e2); - { LemmaMulInequality(Pow(b, e1 - e2), x / Pow(b, e2), Pow(b, e2)); } + { LemmaMulInequality(Pow(b, e1 - e2), x / Pow(b, e2), Pow(b, e2)); } x / Pow(b, e2) * Pow(b, e2) >= Pow(b, e1 - e2) * Pow(b, e2); - { LemmaFundamentalDivMod(x, Pow(b, e2)); - LemmaMulIsCommutativeAuto(); } + { LemmaFundamentalDivMod(x, Pow(b, e2)); + LemmaMulIsCommutativeAuto(); } x - x % Pow(b, e2) >= Pow(b, e1 - e2) * Pow(b, e2); - { LemmaPowAdds(b, e1 - e2, e2); } + { LemmaPowAdds(b, e1 - e2, e2); } x - x % Pow(b, e2) >= Pow(b, e1); - { LemmaModPropertiesAuto(); } + { LemmaModPropertiesAuto(); } x >= Pow(b, e1); false; } @@ -556,9 +556,9 @@ module {:options "-functionSyntax:4"} Power { lemma LemmaPowDivisionInequalityAuto() ensures forall b: nat, e2: nat :: b > 0 ==> Pow(b, e2) > 0 ensures forall x: nat, b: nat, e1: nat, e2: nat - {:trigger x / Pow(b, e2), Pow(b, e1 - e2)} - :: b > 0 && e2 <= e1 && x < Pow(b, e1) ==> - x / Pow(b, e2) < Pow(b, e1 - e2) + {:trigger x / Pow(b, e2), Pow(b, e1 - e2)} + :: b > 0 && e2 <= e1 && x < Pow(b, e1) ==> + x / Pow(b, e2) < Pow(b, e1 - e2) { reveal Pow(); LemmaPowPositiveAuto(); @@ -572,7 +572,7 @@ module {:options "-functionSyntax:4"} Power { } /* b^e % b = 0 */ - lemma LemmaPowMod(b: nat, e: nat) + lemma LemmaPowMod(b: nat, e: nat) requires b > 0 && e > 0 ensures Pow(b, e) % b == 0; { @@ -580,19 +580,19 @@ module {:options "-functionSyntax:4"} Power { calc { Pow(b, e) % b; (b * Pow(b, e - 1)) % b; - { LemmaMulIsAssociativeAuto(); } + { LemmaMulIsAssociativeAuto(); } (Pow(b, e - 1) * b) % b; - { - LemmaPowPositiveAuto(); - LemmaModMultiplesBasic(Pow(b, e-1) , b); - } + { + LemmaPowPositiveAuto(); + LemmaModMultiplesBasic(Pow(b, e-1) , b); + } 0; } } lemma LemmaPowModAuto() ensures forall b: nat, e: nat {:trigger Pow(b, e)} - :: b > 0 && e > 0 ==> Pow(b, e) % b == 0 + :: b > 0 && e > 0 ==> Pow(b, e) % b == 0 { reveal Pow(); forall b: nat, e: nat {:trigger Pow(b, e)} | b > 0 && e > 0 @@ -614,11 +614,11 @@ module {:options "-functionSyntax:4"} Power { calc { Pow(b % m, e) % m; ((b % m) * Pow(b % m, e - 1)) % m; - { LemmaMulModNoopGeneral(b, Pow(b % m, e - 1), m); } + { LemmaMulModNoopGeneral(b, Pow(b % m, e - 1), m); } ((b % m) * (Pow(b % m, e - 1) % m) % m) % m; - { LemmaPowModNoop(b, e - 1, m); } + { LemmaPowModNoop(b, e - 1, m); } ((b % m) * (Pow(b, e - 1) % m) % m) % m; - { LemmaMulModNoopGeneral(b, Pow(b, e - 1), m); } + { LemmaMulModNoopGeneral(b, Pow(b, e - 1), m); } (b * (Pow(b, e - 1)) % m) % m; (b * (Pow(b, e - 1))) % m; Pow(b, e) % m; @@ -628,7 +628,7 @@ module {:options "-functionSyntax:4"} Power { lemma LemmaPowModNoopAuto() ensures forall b: nat, e: nat, m: nat {:trigger Pow(b % m, e)} - :: m > 0 ==> Pow(b % m, e) % m == Pow(b, e) % m + :: m > 0 ==> Pow(b % m, e) % m == Pow(b, e) % m { reveal Pow(); forall b: nat, e: nat, m: nat {:trigger Pow(b % m, e)} diff --git a/src/NonlinearArithmetic/Power2.dfy b/src/NonlinearArithmetic/Power2.dfy index e34feb2f..03f3d24c 100644 --- a/src/NonlinearArithmetic/Power2.dfy +++ b/src/NonlinearArithmetic/Power2.dfy @@ -1,12 +1,12 @@ -// RUN: %dafny /compile:0 /noNLarith "%s" +// RUN: %verify --disable-nonlinear-arithmetic "%s" /******************************************************************************* -* Original: Copyright (c) Microsoft Corporation -* SPDX-License-Identifier: MIT -* -* Modifications and Extensions: Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Original: Copyright (c) Microsoft Corporation + * SPDX-License-Identifier: MIT + * + * Modifications and Extensions: Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ /* Every lemma comes in 2 forms: 'LemmaProperty' and 'LemmaPropertyAuto'. The former takes arguments and may be more stable and less reliant on Z3 @@ -35,7 +35,7 @@ module {:options "-functionSyntax:4"} Power2 { { reveal Pow(); reveal Pow2(); - + if e != 0 { LemmaPow2(e - 1); } @@ -46,7 +46,7 @@ module {:options "-functionSyntax:4"} Power2 { { reveal Pow(); reveal Pow2(); - + forall e: nat {:trigger Pow2(e)} ensures Pow2(e) == Pow(2, e) { @@ -69,7 +69,7 @@ module {:options "-functionSyntax:4"} Power2 { lemma LemmaPow2MaskDiv2Auto() ensures forall e: nat {:trigger Pow2(e)} :: 0 < e ==> - (Pow2(e) - 1) / 2 == Pow2(e - 1) - 1 + (Pow2(e) - 1) / 2 == Pow2(e - 1) - 1 { reveal Pow2(); forall e: nat {:trigger Pow2(e)} | 0 < e @@ -118,4 +118,4 @@ module {:options "-functionSyntax:4"} Power2 { reveal Pow2(); } -} +} diff --git a/src/Relations.dfy b/src/Relations.dfy index a64635a3..3315fb75 100644 --- a/src/Relations.dfy +++ b/src/Relations.dfy @@ -1,11 +1,11 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ -module {:options "-functionSyntax:4"} Relations { +module {:options "-functionSyntax:4"} Relations { ghost predicate Reflexive(R: (T, T) -> bool) { forall x :: R(x, x) @@ -36,14 +36,14 @@ module {:options "-functionSyntax:4"} Relations { && AntiSymmetric(R) && Transitive(R) && StronglyConnected(R) - } + } ghost predicate StrictTotalOrdering(R: (T, T) -> bool) { && Irreflexive(R) && AntiSymmetric(R) && Transitive(R) && Connected(R) - } + } ghost predicate SortedBy(a: seq, lessThan: (T, T) -> bool) { forall i, j | 0 <= i < j < |a| :: lessThan(a[i], a[j]) @@ -64,16 +64,16 @@ module {:options "-functionSyntax:4"} Relations { m := x; } else { var m' := LemmaUniqueMinimum(R, s - {x}); - if + if case R(m', x) => m := m'; case R(x, m') => m := x; } } - lemma LemmaNewFirstElementStillSortedBy(x: T, s: seq, lessThan: (T, T) -> bool) + lemma LemmaNewFirstElementStillSortedBy(x: T, s: seq, lessThan: (T, T) -> bool) requires SortedBy(s, lessThan) requires |s| == 0 || lessThan(x, s[0]) requires TotalOrdering(lessThan) ensures SortedBy([x] + s, lessThan) - {} -} \ No newline at end of file + {} +} diff --git a/src/Unicode/Unicode.dfy b/src/Unicode/Unicode.dfy index 316e61e0..6e9376c3 100644 --- a/src/Unicode/Unicode.dfy +++ b/src/Unicode/Unicode.dfy @@ -1,9 +1,9 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../Wrappers.dfy" include "../Collections/Sequences/Seq.dfy" @@ -15,32 +15,32 @@ module {:options "-functionSyntax:4"} Unicode { import Seq /** - * Any value in the Unicode codespace (a range of integers from 0 to 10FFFF_16). (Section 3.9 D9-D10) - */ + * Any value in the Unicode codespace (a range of integers from 0 to 10FFFF_16). (Section 3.9 D9-D10) + */ type CodePoint = i: bv24 | 0 <= i <= 0x10FFFF /** - * A Unicode code point in the range U+D800 to U+DBFF. (Section 3.8 D71) - */ + * A Unicode code point in the range U+D800 to U+DBFF. (Section 3.8 D71) + */ type HighSurrogateCodePoint = p: CodePoint | HIGH_SURROGATE_MIN <= p <= HIGH_SURROGATE_MAX witness HIGH_SURROGATE_MIN const HIGH_SURROGATE_MIN: CodePoint := 0xD800 const HIGH_SURROGATE_MAX: CodePoint := 0xDBFF /** - * A Unicode code point in the range U+DC00 to U+DFFF. (Section 3.8 D73) - */ + * A Unicode code point in the range U+DC00 to U+DFFF. (Section 3.8 D73) + */ type LowSurrogateCodePoint = p: CodePoint | LOW_SURROGATE_MIN <= p <= LOW_SURROGATE_MAX witness LOW_SURROGATE_MIN const LOW_SURROGATE_MIN: CodePoint := 0xDC00 const LOW_SURROGATE_MAX: CodePoint := 0xDFFF /** - * Any Unicode code point except high-surrogate and low-surrogate code points. (Section 3.9 D76) - */ + * Any Unicode code point except high-surrogate and low-surrogate code points. (Section 3.9 D76) + */ type ScalarValue = p: CodePoint | - && (p < HIGH_SURROGATE_MIN || p > HIGH_SURROGATE_MAX) - && (p < LOW_SURROGATE_MIN || p > LOW_SURROGATE_MAX) + && (p < HIGH_SURROGATE_MIN || p > HIGH_SURROGATE_MAX) + && (p < LOW_SURROGATE_MIN || p > LOW_SURROGATE_MAX) const ASSIGNED_PLANES: set := { 0, // Basic Multilingual Plane diff --git a/src/Unicode/UnicodeEncodingForm.dfy b/src/Unicode/UnicodeEncodingForm.dfy index 1cd3c366..d7f8a463 100644 --- a/src/Unicode/UnicodeEncodingForm.dfy +++ b/src/Unicode/UnicodeEncodingForm.dfy @@ -1,9 +1,9 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../Wrappers.dfy" include "../Functions.dfy" @@ -12,19 +12,19 @@ include "../Collections/Sequences/Seq.dfy" include "Unicode.dfy" /** - * A Unicode encoding form assigns each Unicode scalar value to a unique code unit sequence. - * - * A concrete `EncodingForm` MUST define the following: - * - The type `CodeUnit`. - * - The predicate `IsMinimalWellFormedCodeUnitSubsequence`, which defines the set of encodings of scalar values, - * known as "minimal well-formed code unit subsequences". - * - The function `SplitPrefixMinimalWellFormedCodeUnitSubsequence`, which defines the algorithm by which to parse - * a minimal well-formed code unit subsequence from the beginning of a code unit sequence. - * - The function `EncodeScalarValue`, which defines the mapping from scalar values to minimal well-formed code unit - * subsequences. - * - The function `DecodeMinimalWellFormedCodeUnitSubsequence`, which defines the mapping from minimal well-formed - * code unit subsequences to scalar values. - */ + * A Unicode encoding form assigns each Unicode scalar value to a unique code unit sequence. + * + * A concrete `EncodingForm` MUST define the following: + * - The type `CodeUnit`. + * - The predicate `IsMinimalWellFormedCodeUnitSubsequence`, which defines the set of encodings of scalar values, + * known as "minimal well-formed code unit subsequences". + * - The function `SplitPrefixMinimalWellFormedCodeUnitSubsequence`, which defines the algorithm by which to parse + * a minimal well-formed code unit subsequence from the beginning of a code unit sequence. + * - The function `EncodeScalarValue`, which defines the mapping from scalar values to minimal well-formed code unit + * subsequences. + * - The function `DecodeMinimalWellFormedCodeUnitSubsequence`, which defines the mapping from minimal well-formed + * code unit subsequences to scalar values. + */ abstract module {:options "-functionSyntax:4"} UnicodeEncodingForm { import opened Wrappers @@ -45,46 +45,46 @@ abstract module {:options "-functionSyntax:4"} UnicodeEncodingForm { // /** - * A code unit is the minimal bit combination that can represent a unit of encoded text for processing or - * interchange. (Section 3.9 D77.) - */ + * A code unit is the minimal bit combination that can represent a unit of encoded text for processing or + * interchange. (Section 3.9 D77.) + */ type CodeUnit /** - * A well-formed Unicode code unit sequence that maps to a single Unicode scalar value. - * (Section 3.9 D85a.) - */ + * A well-formed Unicode code unit sequence that maps to a single Unicode scalar value. + * (Section 3.9 D85a.) + */ function IsMinimalWellFormedCodeUnitSubsequence(s: CodeUnitSeq): (b: bool) ensures b ==> - && |s| > 0 - && forall i | 0 < i < |s| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i]) + && |s| > 0 + && forall i | 0 < i < |s| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i]) decreases |s| /** - * Returns the shortest prefix of `s` that is a minimal well-formed code unit subsequence, - * or None if there is no such prefix. - */ + * Returns the shortest prefix of `s` that is a minimal well-formed code unit subsequence, + * or None if there is no such prefix. + */ function SplitPrefixMinimalWellFormedCodeUnitSubsequence(s: CodeUnitSeq): (maybePrefix: Option) ensures |s| == 0 ==> maybePrefix.None? ensures (exists i | 0 < i <= |s| :: IsMinimalWellFormedCodeUnitSubsequence(s[..i])) <==> - && maybePrefix.Some? + && maybePrefix.Some? ensures maybePrefix.Some? ==> - && var prefix := maybePrefix.Extract(); - && 0 < |prefix| <= |s| - && prefix == s[..|prefix|] - && forall i | 0 < i < |prefix| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i]) + && var prefix := maybePrefix.Extract(); + && 0 < |prefix| <= |s| + && prefix == s[..|prefix|] + && forall i | 0 < i < |prefix| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i]) /** - * Returns the minimal well-formed code unit subsequence that this encoding form assigns to the given scalar value. - * The Unicode standard requires that this is injective. - * - * TODO: enforce that implementations satisfy Functions.Injective - */ + * Returns the minimal well-formed code unit subsequence that this encoding form assigns to the given scalar value. + * The Unicode standard requires that this is injective. + * + * TODO: enforce that implementations satisfy Functions.Injective + */ function EncodeScalarValue(v: Unicode.ScalarValue): (m: MinimalWellFormedCodeUnitSeq) /** - * Returns the scalar value that this encoding form assigns to the given minimal well-formed code unit subsequence. - */ + * Returns the scalar value that this encoding form assigns to the given minimal well-formed code unit subsequence. + */ function DecodeMinimalWellFormedCodeUnitSubsequence(m: MinimalWellFormedCodeUnitSeq): (v: Unicode.ScalarValue) ensures EncodeScalarValue(v) == m @@ -93,9 +93,9 @@ abstract module {:options "-functionSyntax:4"} UnicodeEncodingForm { // /** - * If `ms` is the concatenation of a minimal well-formed code unit subsequence `m` and a code unit sequence `s`, - * then the shortest minimal well-formed code unit subsequence prefix of `ms` is simply `m`. - */ + * If `ms` is the concatenation of a minimal well-formed code unit subsequence `m` and a code unit sequence `s`, + * then the shortest minimal well-formed code unit subsequence prefix of `ms` is simply `m`. + */ lemma LemmaSplitPrefixMinimalWellFormedCodeUnitSubsequenceInvertsPrepend(m: MinimalWellFormedCodeUnitSeq, s: CodeUnitSeq) ensures SplitPrefixMinimalWellFormedCodeUnitSubsequence(m + s) == Some(m) { @@ -110,18 +110,18 @@ abstract module {:options "-functionSyntax:4"} UnicodeEncodingForm { } /** - * Returns the unique partition of the given code unit sequence into minimal well-formed code unit subsequences, - * or None if no such partition exists. - */ + * Returns the unique partition of the given code unit sequence into minimal well-formed code unit subsequences, + * or None if no such partition exists. + */ function PartitionCodeUnitSequenceChecked(s: CodeUnitSeq): (maybeParts: Option>) ensures maybeParts.Some? ==> Seq.Flatten(maybeParts.Extract()) == s decreases |s| { if s == [] then Some([]) - else ( + else var maybePrefix := SplitPrefixMinimalWellFormedCodeUnitSubsequence(s); if maybePrefix.None? then None - else ( + else var prefix := maybePrefix.Extract(); // Recursing on subsequences leads to quadratic running time in most/all Dafny runtimes as of this writing. // This definition (and others in the Unicode modules) emphasizes clarify and correctness, @@ -130,14 +130,12 @@ abstract module {:options "-functionSyntax:4"} UnicodeEncodingForm { var restParts := PartitionCodeUnitSequenceChecked(s[|prefix|..]); if restParts.Some? then Some([prefix] + restParts.Extract()) else None - ) - ) } /** - * Returns the unique partition of the given well-formed code unit sequence into minimal well-formed code unit - * subsequences. - */ + * Returns the unique partition of the given well-formed code unit sequence into minimal well-formed code unit + * subsequences. + */ function PartitionCodeUnitSequence(s: WellFormedCodeUnitSeq): (parts: seq) ensures Seq.Flatten(parts) == s { @@ -145,9 +143,9 @@ abstract module {:options "-functionSyntax:4"} UnicodeEncodingForm { } /** - * The partitioning of a minimal well-formed code unit subsequence is the singleton sequence - * containing exactly the minimal well-formed code unit subsequence. - */ + * The partitioning of a minimal well-formed code unit subsequence is the singleton sequence + * containing exactly the minimal well-formed code unit subsequence. + */ lemma LemmaPartitionMinimalWellFormedCodeUnitSubsequence(m: MinimalWellFormedCodeUnitSeq) ensures PartitionCodeUnitSequenceChecked(m) == Some([m]) { @@ -167,16 +165,16 @@ abstract module {:options "-functionSyntax:4"} UnicodeEncodingForm { } /** - * A code unit sequence is well-formed iff it can be partitioned into a sequence of minimal well-formed code unit subsequences. - */ + * A code unit sequence is well-formed iff it can be partitioned into a sequence of minimal well-formed code unit subsequences. + */ function IsWellFormedCodeUnitSequence(s: CodeUnitSeq): (b: bool) { PartitionCodeUnitSequenceChecked(s).Some? } /** - * A minimal well-formed code unit subsequence is a well-formed code unit sequence. - */ + * A minimal well-formed code unit subsequence is a well-formed code unit sequence. + */ lemma LemmaMinimalWellFormedCodeUnitSubsequenceIsWellFormedSequence(m: MinimalWellFormedCodeUnitSeq) ensures IsWellFormedCodeUnitSequence(m) { @@ -184,9 +182,9 @@ abstract module {:options "-functionSyntax:4"} UnicodeEncodingForm { } /** - * The concatenation of a minimal well-formed code unit subsequence and a well-formed code unit sequence - * is itself a well-formed code unit sequence. - */ + * The concatenation of a minimal well-formed code unit subsequence and a well-formed code unit sequence + * is itself a well-formed code unit sequence. + */ lemma LemmaPrependMinimalWellFormedCodeUnitSubsequence(m: MinimalWellFormedCodeUnitSeq, s: WellFormedCodeUnitSeq) ensures IsWellFormedCodeUnitSequence(m + s) { @@ -196,8 +194,8 @@ abstract module {:options "-functionSyntax:4"} UnicodeEncodingForm { } /** - * The concatenation of minimal well-formed code unit subsequences is itself a well-formed code unit sequence. - */ + * The concatenation of minimal well-formed code unit subsequences is itself a well-formed code unit sequence. + */ lemma LemmaFlattenMinimalWellFormedCodeUnitSubsequences(ms: seq) ensures IsWellFormedCodeUnitSequence(Seq.Flatten(ms)) { @@ -215,8 +213,8 @@ abstract module {:options "-functionSyntax:4"} UnicodeEncodingForm { } /** - * The concatenation of well-formed code unit sequences is itself a well-formed code unit sequence. - */ + * The concatenation of well-formed code unit sequences is itself a well-formed code unit sequence. + */ lemma LemmaConcatWellFormedCodeUnitSubsequences(s: WellFormedCodeUnitSeq, t: WellFormedCodeUnitSeq) ensures IsWellFormedCodeUnitSequence(s + t) { @@ -227,14 +225,14 @@ abstract module {:options "-functionSyntax:4"} UnicodeEncodingForm { assert s + t == Seq.Flatten(partsST); assert forall part | part in partsST :: - && |part| > 0 - && IsMinimalWellFormedCodeUnitSubsequence(part); + && |part| > 0 + && IsMinimalWellFormedCodeUnitSubsequence(part); LemmaFlattenMinimalWellFormedCodeUnitSubsequences(partsST); } /** - * Returns the well-formed Unicode string that is the encoding of the given scalar value sequence. - */ + * Returns the well-formed Unicode string that is the encoding of the given scalar value sequence. + */ function EncodeScalarSequence(vs: seq): (s: WellFormedCodeUnitSeq) { var ms := Seq.Map(EncodeScalarValue, vs); @@ -243,8 +241,8 @@ abstract module {:options "-functionSyntax:4"} UnicodeEncodingForm { } /** - * Returns the scalar value sequence encoded by the given well-formed Unicode string. - */ + * Returns the scalar value sequence encoded by the given well-formed Unicode string. + */ function DecodeCodeUnitSequence(s: WellFormedCodeUnitSeq): (vs: seq) ensures EncodeScalarSequence(vs) == s { @@ -261,13 +259,13 @@ abstract module {:options "-functionSyntax:4"} UnicodeEncodingForm { } /** - * Returns the scalar value sequence encoded by the given code unit sequence, or None if the given Unicode string - * is not well-formed. - */ + * Returns the scalar value sequence encoded by the given code unit sequence, or None if the given Unicode string + * is not well-formed. + */ function DecodeCodeUnitSequenceChecked(s: CodeUnitSeq): (maybeVs: Option>) ensures IsWellFormedCodeUnitSequence(s) ==> - && maybeVs.Some? - && maybeVs.Extract() == DecodeCodeUnitSequence(s) + && maybeVs.Some? + && maybeVs.Extract() == DecodeCodeUnitSequence(s) ensures !IsWellFormedCodeUnitSequence(s) ==> && maybeVs.None? { // IsWellFormedCodeUnitSequence and DecodeCodeUnitSequence each call PartitionCodeUnitSequence, diff --git a/src/Unicode/Utf16EncodingForm.dfy b/src/Unicode/Utf16EncodingForm.dfy index f6f8f36b..88c64780 100644 --- a/src/Unicode/Utf16EncodingForm.dfy +++ b/src/Unicode/Utf16EncodingForm.dfy @@ -1,9 +1,9 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../Collections/Sequences/Seq.dfy" include "../Functions.dfy" @@ -23,10 +23,10 @@ module {:options "-functionSyntax:4"} Utf16EncodingForm refines UnicodeEncodingF { if |s| == 1 then IsWellFormedSingleCodeUnitSequence(s) else if |s| == 2 then ( - var b := IsWellFormedDoubleCodeUnitSequence(s); - assert b ==> forall i | 0 < i < |s| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i]); - b - ) + var b := IsWellFormedDoubleCodeUnitSequence(s); + assert b ==> forall i | 0 < i < |s| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i]); + b + ) else false } @@ -51,12 +51,12 @@ module {:options "-functionSyntax:4"} Utf16EncodingForm refines UnicodeEncodingF function SplitPrefixMinimalWellFormedCodeUnitSubsequence(s: CodeUnitSeq): (maybePrefix: Option) ensures |s| == 0 ==> maybePrefix.None? ensures (exists i | 0 < i <= |s| :: IsMinimalWellFormedCodeUnitSubsequence(s[..i])) <==> - && maybePrefix.Some? + && maybePrefix.Some? ensures maybePrefix.Some? ==> - && var prefix := maybePrefix.Extract(); - && 0 < |prefix| <= |s| - && prefix == s[..|prefix|] - && IsMinimalWellFormedCodeUnitSubsequence(prefix) + && var prefix := maybePrefix.Extract(); + && 0 < |prefix| <= |s| + && prefix == s[..|prefix|] + && IsMinimalWellFormedCodeUnitSubsequence(prefix) { if |s| >= 1 && IsWellFormedSingleCodeUnitSequence(s[..1]) then Some(s[..1]) else if |s| >= 2 && IsWellFormedDoubleCodeUnitSequence(s[..2]) then Some(s[..2]) diff --git a/src/Unicode/Utf8EncodingForm.dfy b/src/Unicode/Utf8EncodingForm.dfy index b766e100..8a41129d 100644 --- a/src/Unicode/Utf8EncodingForm.dfy +++ b/src/Unicode/Utf8EncodingForm.dfy @@ -1,9 +1,9 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../Collections/Sequences/Seq.dfy" include "../Functions.dfy" @@ -12,9 +12,9 @@ include "Unicode.dfy" include "UnicodeEncodingForm.dfy" /** - * The Unicode encoding form that assigns each Unicode scalar value to an unsigned byte sequence of one to four bytes - * in length, as specified in Table 3-6 and Table 3-7. - */ + * The Unicode encoding form that assigns each Unicode scalar value to an unsigned byte sequence of one to four bytes + * in length, as specified in Table 3-6 and Table 3-7. + */ module {:options "-functionSyntax:4"} Utf8EncodingForm refines UnicodeEncodingForm { type CodeUnit = bv8 @@ -25,25 +25,25 @@ module {:options "-functionSyntax:4"} Utf8EncodingForm refines UnicodeEncodingFo function IsMinimalWellFormedCodeUnitSubsequence(s: CodeUnitSeq): (b: bool) { if |s| == 1 then ( - var b := IsWellFormedSingleCodeUnitSequence(s); - assert b ==> forall i | 0 < i < |s| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i]); - b - ) + var b := IsWellFormedSingleCodeUnitSequence(s); + assert b ==> forall i | 0 < i < |s| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i]); + b + ) else if |s| == 2 then ( - var b := IsWellFormedDoubleCodeUnitSequence(s); - assert b ==> forall i | 0 < i < |s| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i]); - b - ) + var b := IsWellFormedDoubleCodeUnitSequence(s); + assert b ==> forall i | 0 < i < |s| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i]); + b + ) else if |s| == 3 then ( - var b := IsWellFormedTripleCodeUnitSequence(s); - assert b ==> forall i | 0 < i < |s| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i]); - b - ) + var b := IsWellFormedTripleCodeUnitSequence(s); + assert b ==> forall i | 0 < i < |s| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i]); + b + ) else if |s| == 4 then ( - var b := IsWellFormedQuadrupleCodeUnitSequence(s); - assert b ==> forall i | 0 < i < |s| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i]); - b - ) + var b := IsWellFormedQuadrupleCodeUnitSequence(s); + assert b ==> forall i | 0 < i < |s| :: !IsMinimalWellFormedCodeUnitSubsequence(s[..i]); + b + ) else false } @@ -57,7 +57,7 @@ module {:options "-functionSyntax:4"} Utf8EncodingForm refines UnicodeEncodingFo function IsWellFormedDoubleCodeUnitSequence(s: CodeUnitSeq): (b: bool) requires |s| == 2 ensures b ==> - && !IsWellFormedSingleCodeUnitSequence(s[..1]) + && !IsWellFormedSingleCodeUnitSequence(s[..1]) { var firstByte := s[0]; var secondByte := s[1]; @@ -68,37 +68,37 @@ module {:options "-functionSyntax:4"} Utf8EncodingForm refines UnicodeEncodingFo function IsWellFormedTripleCodeUnitSequence(s: CodeUnitSeq): (b: bool) requires |s| == 3 ensures b ==> - && !IsWellFormedSingleCodeUnitSequence(s[..1]) - && !IsWellFormedDoubleCodeUnitSequence(s[..2]) + && !IsWellFormedSingleCodeUnitSequence(s[..1]) + && !IsWellFormedDoubleCodeUnitSequence(s[..2]) { var firstByte := s[0]; var secondByte := s[1]; var thirdByte := s[2]; && ( - || (firstByte == 0xE0 && 0xA0 <= secondByte <= 0xBF) - || (0xE1 <= firstByte <= 0xEC && 0x80 <= secondByte <= 0xBF) - || (firstByte == 0xED && 0x80 <= secondByte <= 0x9F) - || (0xEE <= firstByte <= 0xEF && 0x80 <= secondByte <= 0xBF) - ) + || (firstByte == 0xE0 && 0xA0 <= secondByte <= 0xBF) + || (0xE1 <= firstByte <= 0xEC && 0x80 <= secondByte <= 0xBF) + || (firstByte == 0xED && 0x80 <= secondByte <= 0x9F) + || (0xEE <= firstByte <= 0xEF && 0x80 <= secondByte <= 0xBF) + ) && 0x80 <= thirdByte <= 0xBF } function IsWellFormedQuadrupleCodeUnitSequence(s: CodeUnitSeq): (b: bool) requires |s| == 4 ensures b ==> - && !IsWellFormedSingleCodeUnitSequence(s[..1]) - && !IsWellFormedDoubleCodeUnitSequence(s[..2]) - && !IsWellFormedTripleCodeUnitSequence(s[..3]) + && !IsWellFormedSingleCodeUnitSequence(s[..1]) + && !IsWellFormedDoubleCodeUnitSequence(s[..2]) + && !IsWellFormedTripleCodeUnitSequence(s[..3]) { var firstByte := s[0]; var secondByte := s[1]; var thirdByte := s[2]; var fourthByte := s[3]; && ( - || (firstByte == 0xF0 && 0x90 <= secondByte <= 0xBF) - || (0xF1 <= firstByte <= 0xF3 && 0x80 <= secondByte <= 0xBF) - || (firstByte == 0xF4 && 0x80 <= secondByte <= 0x8F) - ) + || (firstByte == 0xF0 && 0x90 <= secondByte <= 0xBF) + || (0xF1 <= firstByte <= 0xF3 && 0x80 <= secondByte <= 0xBF) + || (firstByte == 0xF4 && 0x80 <= secondByte <= 0x8F) + ) && 0x80 <= thirdByte <= 0xBF && 0x80 <= fourthByte <= 0xBF } diff --git a/src/Unicode/Utf8EncodingScheme.dfy b/src/Unicode/Utf8EncodingScheme.dfy index 210e1082..4e6f2c39 100644 --- a/src/Unicode/Utf8EncodingScheme.dfy +++ b/src/Unicode/Utf8EncodingScheme.dfy @@ -1,9 +1,9 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../Collections/Sequences/Seq.dfy" include "../BoundedInts.dfy" @@ -12,22 +12,22 @@ include "Unicode.dfy" include "Utf8EncodingForm.dfy" /** - * The Unicode encoding scheme that serializes a UTF-8 code unit sequence in exactly the same order as the code unit - * sequence itself. - * - * Because the UTF-8 encoding form deals in ordered byte sequences, the UTF-8 encoding scheme is trivial. - * The byte ordering is completely defined by the UTF-8 code unit sequence itself. - * We implement the encoding scheme here for completeness of the Unicode character encoding model, - * and to perform the (trivial) conversion between `uint8`/`byte` and `bv8` values. - * - * (Section 3.10 D95) - * - * TODO: this should refine an abstract UnicodeEncodingScheme module - * that states lemmas/conditions about Serialize and Deserialize - * which refining modules would prove about their own implementations. - * Proving those lemmas are easier to write using `calc`, - * but that runs into . - */ + * The Unicode encoding scheme that serializes a UTF-8 code unit sequence in exactly the same order as the code unit + * sequence itself. + * + * Because the UTF-8 encoding form deals in ordered byte sequences, the UTF-8 encoding scheme is trivial. + * The byte ordering is completely defined by the UTF-8 code unit sequence itself. + * We implement the encoding scheme here for completeness of the Unicode character encoding model, + * and to perform the (trivial) conversion between `uint8`/`byte` and `bv8` values. + * + * (Section 3.10 D95) + * + * TODO: this should refine an abstract UnicodeEncodingScheme module + * that states lemmas/conditions about Serialize and Deserialize + * which refining modules would prove about their own implementations. + * Proving those lemmas are easier to write using `calc`, + * but that runs into . + */ module {:options "-functionSyntax:4"} Utf8EncodingScheme { import opened Wrappers @@ -39,31 +39,31 @@ module {:options "-functionSyntax:4"} Utf8EncodingScheme { type byte = BoundedInts.uint8 /** - * Returns the byte serialization of the given code unit sequence. - */ + * Returns the byte serialization of the given code unit sequence. + */ function Serialize(s: Utf8EncodingForm.CodeUnitSeq): (b: seq) { Seq.Map(c => c as byte, s) } /** - * Returns the code unit sequence that serializes to the given byte sequence. - */ + * Returns the code unit sequence that serializes to the given byte sequence. + */ function Deserialize(b: seq): (s: Utf8EncodingForm.CodeUnitSeq) { Seq.Map(b => b as Utf8EncodingForm.CodeUnit, b) } /** - * Serializing a code unit sequence and then deserializing the result, yields the original code unit sequence. - */ + * Serializing a code unit sequence and then deserializing the result, yields the original code unit sequence. + */ lemma LemmaSerializeDeserialize(s: Utf8EncodingForm.CodeUnitSeq) ensures Deserialize(Serialize(s)) == s {} /** - * Deserializing a byte sequence and then serializing the result, yields the original byte sequence. - */ + * Deserializing a byte sequence and then serializing the result, yields the original byte sequence. + */ lemma LemmaDeserializeSerialize(b: seq) ensures Serialize(Deserialize(b)) == b {} diff --git a/src/Wrappers.dfy b/src/Wrappers.dfy index 22fc4bf5..852d9a8c 100644 --- a/src/Wrappers.dfy +++ b/src/Wrappers.dfy @@ -1,19 +1,19 @@ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ module {:options "-functionSyntax:4"} Wrappers { - + datatype Option<+T> = None | Some(value: T) { function ToResult(): Result { match this case Some(v) => Success(v) case None() => Failure("Option is None") } - + function UnwrapOr(default: T): T { match this case Some(v) => v @@ -38,14 +38,14 @@ module {:options "-functionSyntax:4"} Wrappers { } datatype Result<+T, +R> = | Success(value: T) | Failure(error: R) { - function ToOption(): Option + function ToOption(): Option { match this case Success(s) => Some(s) case Failure(e) => None() } - function UnwrapOr(default: T): T + function UnwrapOr(default: T): T { match this case Success(s) => s