Merge branch 'master' into proof_refactoring_suggestions

Source/DafnyCore/AST/Members/ConstantField.cs

@@ -25,10 +25,7 @@ public override bool CanBeRevealed() {
     return true;
   }
 
-  public bool ContainsHide {
-    get => throw new NotSupportedException();
-    set => throw new NotSupportedException();
-  }
+  public bool ContainsHide { get; set; }
 
   public new bool IsGhost { get { return this.isGhost; } }
   public List<TypeParameter> TypeArgs { get { return new List<TypeParameter>(); } }

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -1367,7 +1367,7 @@ private ConcreteSyntaxTree CreateSubroutine(string name, List<TypeArgumentInstan
           for (var i = 0; i < inParams.Count; i++) {
             var p = (overriddenInParams ?? inParams)[i];
             var instantiatedType = p.Type.Subst(thisContext.ParentFormalTypeParametersToActuals);
-            if (!instantiatedType.Equals(p.Type)) {
+            if (!p.IsGhost && !instantiatedType.Equals(p.Type)) {
               // var p instantiatedType = p.(instantiatedType)
               var pName = IdName(inParams[i]);
               DeclareLocalVar(pName, instantiatedType, p.tok, true, null, w);
@@ -2236,8 +2236,11 @@ protected override void EmitNew(Type type, IToken tok, CallStmt initCall /*?*/,
       if (cl is TraitDecl { IsObjectTrait: true }) {
         wr.Write("_dafny.New_Object()");
       } else {
+        var ctor = (Constructor)initCall?.Method; // correctness of cast follows from precondition of "EmitNew"
+        var sep = "";
         wr.Write("{0}(", TypeName_Initializer(type, wr, tok));
         EmitTypeDescriptorsActuals(TypeArgumentInstantiation.ListFromClass(cl, type.TypeArgs), tok, wr);
+        wr.Write(ConstructorArguments(initCall, wStmts, ctor, sep));
         wr.Write(")");
       }
     }

Source/DafnyRuntime/DafnyRuntimePython/.gitignore

@@ -0,0 +1,30 @@
+### from https://github.com/github/gitignore/blob/main/Python.gitignore
+
+# Byte-compiled / optimized / DLL files
+__pycache__/
+*.py[cod]
+*$py.class
+
+# Distribution / packaging
+.Python
+build/
+develop-eggs/
+dist/
+downloads/
+eggs/
+.eggs/
+lib/
+lib64/
+parts/
+sdist/
+var/
+wheels/
+share/python-wheels/
+*.egg-info/
+.installed.cfg
+*.egg
+MANIFEST
+
+# Environments
+.env
+venv/

Source/DafnyRuntime/DafnyRuntimePython/BUILDING.md

@@ -0,0 +1,62 @@
+# Building the DafnyRuntimePython
+
+## Prerequisites
+
+- the `dotnet` CLI, to build Dafny
+- Python, to build and upload the package
+- [TestPyPI credentials](https://packaging.python.org/en/latest/guides/using-testpypi/), if you will upload to TestPyPI
+- PyPI credentials, if you will upload to PyPI
+
+## Steps
+
+1. Ensure that the `System_` module is up-to-date:
+
+```bash
+# Ensure that the Dafny build is up-to-date,
+# as it will be used to compile the System_ module.
+$ dotnet build --project ../../Dafny
+
+# Compile the System_ runtime module.
+$ make update-system-module
+```
+
+2. Build the distribution package:
+
+```bash
+# Set up the build tooling
+$ make setup-venv
+
+# Remove old build artifacts
+$ make clean-package
+
+# Build the distribution package
+$ make build-package
+```
+
+3. Check that the distribution package looks right locally and on TestPyPI,
+   as (production) PyPI does not allow overwriting uploaded packages:
+
+```bash
+# List the distribution package's files, and check that:
+#  1. the version number is correct
+#  2. the `System_/__init__.py` file exists
+#  3. the `dafny/__init__.py` file exists
+$ tar tf dist/dafnyruntimepython-X.Y.Z.tar.gz
+
+# Upload to TestPyPI, and check that it appears correct at
+# <https://test.pypi.org/project/DafnyRuntimePython/>.
+$ make upload-package-testpypi
+```
+
+4. Upload to PyPI:
+
+```bash
+$ make upload-package-pypi
+```
+
+You can view the uploaded package at <https://pypi.org/project/DafnyRuntimePython/>.
+
+## More info
+
+The packaging process is described in
+<https://packaging.python.org/en/latest/tutorials/packaging-projects/>

Source/DafnyRuntime/DafnyRuntimePython/Makefile

@@ -3,7 +3,9 @@
 DAFNY = dotnet run --project ../../Dafny --no-build --
 
 GENERATED_SYSTEM_MODULE_SOURCE=../obj/systemModulePopulator-py/System_.py
-GENERATED_SYSTEM_MODULE_TARGET=System_.py
+GENERATED_SYSTEM_MODULE_TARGET=System_/__init__.py
+
+VIRTUALENV = venv
 
 all: check-system-module
 
@@ -15,3 +17,19 @@ check-system-module: build-system-module
 
 update-system-module: build-system-module
 	cp $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET)
+
+setup-venv:
+	python -m venv --clear $(VIRTUALENV)
+	$(VIRTUALENV)/bin/pip install --upgrade build twine
+
+clean-package:
+	rm -rf dist/ *.egg-info/
+
+build-package:
+	$(VIRTUALENV)/bin/python -m build
+
+upload-package-testpypi:
+	$(VIRTUALENV)/bin/python -m twine upload --repository testpypi dist/*
+
+upload-package-pypi:
+	$(VIRTUALENV)/bin/python -m twine upload dist/*

Source/DafnyRuntime/DafnyRuntimePython/pyproject.toml

@@ -0,0 +1,24 @@
+[project]
+name = "DafnyRuntimePython"
+version = "4.8.1"
+authors = [
+  { name = "The Dafny core team", email = "[email protected]" },
+]
+description = "Dafny runtime for Python"
+requires-python = ">=3.8"
+classifiers = [
+  "Programming Language :: Python :: 3",
+  "License :: OSI Approved :: MIT License",
+  "Operating System :: OS Independent",
+]
+
+[project.urls]
+Homepage = "https://github.com/dafny-lang/dafny"
+Issues = "https://github.com/dafny-lang/dafny/issues"
+
+[build-system]
+requires = ["setuptools>=61.0"]
+build-backend = "setuptools.build_meta"
+
+[tool.setuptools]
+packages = ["_dafny", "System_"]

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/constantWithReveal.dfy

@@ -0,0 +1,8 @@
+// RUN: %verify %s &> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+opaque function Foo(x: int): int {
+  x
+}
+
+const C := reveal Foo(); Foo(42)

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/constantWithReveal.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Class.java

@@ -2,7 +2,7 @@
 
 import java.math.BigInteger;
 
-public class Class extends _ExternBase_Class {
+public class Class {
     private final BigInteger n;
 
     public Class(BigInteger n) {

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.go

@@ -17,12 +17,6 @@ func (obj *Class) Get() dafny.Int {
 	return obj.n
 }
 
-// have to implement this because the Go backend can't mix Dafny and Go code :-\
-
-func (obj *Class) Print() {
-	fmt.Printf("My value is %d\n", obj.n)
-}
-
 type CompanionStruct_Class_ struct{}
 var Companion_Class_ = CompanionStruct_Class_{}
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.py

@@ -17,8 +17,3 @@ def SayHi():
 
     def Get(self):
         return self.n
-
-    def Print(self):
-        _dafny.print(_dafny.string_of(_dafny.Seq("My value is ")))
-        _dafny.print(_dafny.string_of((self).Get()))
-        _dafny.print(_dafny.string_of(_dafny.Seq("\n")))

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy

@@ -1,24 +1,23 @@
 // RUN: %run --target cs "%s" --input %S/ExternCtors-externs/Library.cs > "%t"
 // RUN: %run --target java "%s" --input %S/ExternCtors-externs/Class.java >> "%t"
 // RUN: %run --target py "%s" --input %S/ExternCtors-externs/Library.py >> "%t"
+// RUN: %run --target go "%s" --input %S/ExternCtors-externs/Library.go >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
-// FIXME: Extern constructors are currently broken in Go and JavaScript,
-// so they are omitted
+// FIXME: Extern constructors are currently broken in JavaScript,
+// so that is omitted
 
 method Main() {
   Library.Class.SayHi();
   var obj := new Library.Class(42);
-  obj.Print();
+  print "My value is ", obj.Get(), "\n";
 }
 
 module {:extern "Library"} Library {
   class {:extern} Class {
     constructor {:extern} (n: int)
     static method {:extern} SayHi()
     function {:extern} Get() : int
-    method Print() {
-      print "My value is ", Get(), "\n";
-    }
   }
 }
+

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy.expect

@@ -10,3 +10,7 @@ My value is 42
 Dafny program verifier finished with 1 verified, 0 errors
 Hello!
 My value is 42
+
+Dafny program verifier finished with 1 verified, 0 errors
+Hello!
+My value is 42

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1verbose/CompileAndThenRun.dfy.expect

@@ -100,7 +100,7 @@ hello, Dafny
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to CompileAndThenRun-py/__main__.py
 Additional output written to CompileAndThenRun-py/CompileAndThenRun-py.dtr
-Additional output written to CompileAndThenRun-py/System_.py
-Additional output written to CompileAndThenRun-py/_dafny.py
+Additional output written to CompileAndThenRun-py/System_/__init__.py
+Additional output written to CompileAndThenRun-py/_dafny/__init__.py
 Additional output written to CompileAndThenRun-py/module_.py
 hello, Dafny

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile3/JustRun.dfy.expect

@@ -108,8 +108,8 @@ hello, Dafny
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to JustRun-py/__main__.py
 Additional output written to JustRun-py/JustRun-py.dtr
-Additional output written to JustRun-py/System_.py
-Additional output written to JustRun-py/_dafny.py
+Additional output written to JustRun-py/System_/__init__.py
+Additional output written to JustRun-py/_dafny/__init__.py
 Additional output written to JustRun-py/module_.py
 Running...
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy.expect

@@ -100,7 +100,7 @@ hello, Dafny
 Dafny program verifier finished with 0 verified, 0 errors
 Wrote textual form of target program to ManualCompile-py/__main__.py
 Additional output written to ManualCompile-py/ManualCompile-py.dtr
-Additional output written to ManualCompile-py/System_.py
-Additional output written to ManualCompile-py/_dafny.py
+Additional output written to ManualCompile-py/System_/__init__.py
+Additional output written to ManualCompile-py/_dafny/__init__.py
 Additional output written to ManualCompile-py/module_.py
 hello, Dafny

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify "%s" --performance-stats=10 --relax-definite-assignment --allow-axioms > "%t"
+// RUN: %exits-with 4 %verify "%s" --performance-stats=100 --relax-definite-assignment --allow-axioms > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module AssignmentToNat {

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect

@@ -91,5 +91,5 @@ SubsetTypes.dfy(459,15): Error: assertion might not hold
 SubsetTypes.dfy(464,13): Error: assertion might not hold
 
 Dafny program verifier finished with 13 verified, 91 errors
-Total resources used is 774980
-Max resources used by VC is 101850
+Total resources used is 775000
+Max resources used by VC is 101900

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-5814.dfy

@@ -0,0 +1,18 @@
+// RUN: %testDafnyForEachCompiler "%s"
+
+trait MyTrait<T> {
+  method Bar(ghost x: T, y: T) returns (z: T)
+}
+
+class MyClass extends MyTrait<int> {
+  constructor() {}
+  method Bar(ghost x: int, y: int) returns (z: int) {
+    return y;
+  }
+}
+
+method Main() {
+  var c := new MyClass();
+  var z := c.Bar(7, 42);
+  expect z == 42;
+}

docs/dev/news/5761.feat

@@ -0,0 +1 @@
+Added opaque blocks to the language. Opaque blocks enable improving verification performance. See the documentation for more details.

docs/dev/news/5779.feat

@@ -0,0 +1 @@
+By blocks ("... by { ... }") are now available for assert statements, call statements, and the three types of assignments (:=, :-, :|). Also, by blocks should now be more intuitive since they enable proving any assertions on the left-hand side of the 'by', not just the 'outermost' one. For example, previously `assert 3 / x == 1 by { assume x == 3; }` could still give a possible division by zero error, but now it won't. 

docs/dev/news/5823.fix

@@ -0,0 +1 @@
+Fix a bug that prevented using reveal statement expressions in the body of a constant.