fix(deps): update dependency org.dafny:dafnyruntime to v4.8.1

[mend-for-github.aaakk.us.kg]

This PR contains the following updates:

Package	Change	Age	Adoption	Passing	Confidence
org.dafny:DafnyRuntime	4.8.0 -> 4.8.1

---

Release Notes

dafny-lang/dafny (org.dafny:DafnyRuntime)

v4.8.1

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 ##​5520)
  fix: Check the emptiness status of constraint-less newtype declarations (fixes #​5521)
  https://github.com/dafny-lang/dafny/pull/54955495)

• 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.
(https://github.com/dafny-lang/dafny/pull/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.
  https://github.com/dafny-lang/dafny/pull/56765676)

Bug fixes

• Allow hiding instance member using a static reference

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

• Support for double constant initialization in Dafny-to-Rust (https://github.com/dafny-lang/dafny/pull/5642)

• Support for enumerating datatypes in the Rust backend (https://github.com/dafny-lang/dafny/pull/5643)

• Tail-Recursion for the Dafny-to-Rust compiler (https://github.com/dafny-lang/dafny/pull/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 (https://github.com/dafny-lang/dafny/pull/5760)

---

Configuration

📅 Schedule: Branch creation - At any time (no schedule defined), Automerge - At any time (no schedule defined).

🚦 Automerge: Disabled by config. Please merge this manually once you are satisfied.

♻ Rebasing: Whenever PR becomes conflicted, or you tick the rebase/retry checkbox.

🔕 Ignore: Close this PR and you won't be reminded about this update again.

---

• If you want to rebase/retry this PR, check this box

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 78.04%. Comparing base (d0879d7) to head (27a50b6).
Report is 2 commits behind head on main.

Additional details and impacted files

@@             Coverage Diff              @@
##               main     #901      +/-   ##
============================================
+ Coverage     77.97%   78.04%   +0.06%     
  Complexity      977      977              
============================================
  Files            97       97              
  Lines          4554     4554              
  Branches        423      423              
============================================
+ Hits           3551     3554       +3     
+ Misses          827      823       -4     
- Partials        176      177       +1     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.