Dafny 4.8.1

[keyboardDrummer]

New features

• feat: allow type parameters of newtype declarations
  feat: support optional witness clause of constraint-less newtype declarations
  feat: show tool tips for auto-completed type parameters
  feat: show tool tips for inferred (==) characteristics
  fix: Don't let newtype well-formedness checking affect witness checking (fixes #Base type throws off witness checking #5520)
  fix: Check the emptiness status of constraint-less newtype declarations (fixes Constraint-less newtypes assumed to be nonempty #5521)
  (feat: Allow type parameters on newtypes #5495)

• New feature: model extractor

  CLI option

  The dafny verify command now has an option --extract:<file>, where (just like for the various print options) <file> is allowed to be - to denote standard output.

  Extract mechanism

  Upon successful verification, the new extract mechanism visits the AST of the given program. For any module marked with {:extract}, the extract-worthy material from the module is output. The output declarations will be in the same order as they appear textually in the module (in particular, the fact that module-level Dafny declarations are collected in an internal class _default has no bearing on the output order).

  Three kinds of declarations are extract-worthy:

  • A type declaration A<X, Y, Z> that bears an attribute {:extract_name B} is extracted into a Boogie type declaration type B _ _ _;.

    The definition of the type is ignored. (The intended usage for an extracted type is that the Dafny program give a definition for the type, which goes to show the existence of such a type.)

  • A function declaration F(x: X, y: Y): Z that bears an attribute {:extract_name G} is extracted into a Boogie function declaration function G(x: X, y: Y): Z;.

    The body of the Dafny function is ignored. (The intended usage for an extracted function is that the Dafny program give a definition for the function, which goes to show the existence of such a function.)

  • A lemma declaration L(x: X, y: Y) requires P ensures Q that bears an attribute {:extract_pattern ...} or an attribute {:extract_used_by ...} is extracted into a Boogie axiom. The axiom has the basic form axiom (forall x: X, y: Y :: P ==> Q);.

    If the lemma has an attribute {:extract_used_by F}, then the axiom will be emitted into the uses clause of the Boogie function generated for Dafny function F.

    If the lemma has no in-parameters, the axiom is just P ==> Q.

    If the lemma has in-parameters, then any attribute {:extract_pattern E, F, G} adds a matching pattern { E, F, G } to the emitted quantifier. Also, any attribute {:extract_attribute "name", E, F, G} adds an attribute {:name E, F, G} to the quantifier.

  Expressions

  The pre- and postconditions of extracted lemmas turn into analogous Boogie expressions, and the types of function/lemma parameters and bound variables are extracted into analogous Boogie types. The intended usage of the extract mechanism is that these expressions and types do indeed have analogous Boogie types.

  At this time, only a limited set of expressions and types are supported, but more can be added in the future.

  Any forall and exists quantifiers in expressions are allowed to use :extract_pattern and :extract_attribute attributes, as described above for lemmas.

  Some extracted expressions are simplified. For example, true && !!P is simplified to P.

  Soundness

  The Dafny program that is used as input for the extraction is treated like any other Dafny program. The intended usage of the extraction mechanism is to prove parts of the axiomatization in DafnyPrelude.bpl to be logically consistent. Whether or not the extracted Boogie declarations meet this goal depends on the given Dafny program. For example, if the given Dafny program formalizes sequences in terms of maps and formalizes maps in terms of sequences, then the extraction probably does not provide guarantees of consistency.
  (feat: Prelude extractor #5621)

• Dafny-to-Rust: {:test} methods generate #[test] wrappers in Rust that can be invoked using cargo test.
  Similarly, {:rust_cfg_test} on modules generates a #[cfg(test)] in the resulting rust module.
  (Feat: Translate Dafny tests to Rust tests #5676)

Bug fixes

• Allow hiding instance members using a static reference

• Enable using "hide *" in the context of a recursive function

• Support for double constant initialization in Dafny-to-Rust (Second assignment to const crashes the Rust compiler #5642)

• Support for enumerating datatypes in the Rust backend (Support for enumerating finite datatypes in Rust #5643)

• Tail-Recursion for the Dafny-to-Rust compiler (Bad code generated in Rust for recursive function having a local variable with the same name as a parameter. #5647)

• The new resolver (accessible using --type-system-refresh) can now handle revealing instance functions using a static receiver, as it is the case for the current resolver (Allow revealing using a static receiver #5760)

---

This discussion was created from the release Dafny 4.8.1.