From a1ba04b3241d01bc4b87b9b2fe910e204205a629 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Wed, 15 May 2024 10:46:16 -0700
Subject: [PATCH] Move to more recent Dafny prerelease (#366)

---
 .github/workflows/pull.yml                    |  2 +-
 .github/workflows/push.yml                    |  9 +++---
 .../codegen-patches/rust/dafny-4.5.0.patch    | 30 +++++--------------
 .../codegen-patches/rust/dafny-4.5.0.patch    | 30 +++++--------------
 4 files changed, 22 insertions(+), 49 deletions(-)

diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml
index 68a287634..da19e3181 100644
--- a/.github/workflows/pull.yml
+++ b/.github/workflows/pull.yml
@@ -50,7 +50,7 @@ jobs:
         # Dafny Rust code generation, so we only test on a relatively recent prerelease instead.
         # This can be updated as needed when new features/fixes land in Dafny master.
         dafny-version:
-          - nightly-2024-05-09-8432b17
+          - nightly-2024-05-14-8da3ddd
     uses: ./.github/workflows/test_models_rust_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}
diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index cb85dea6c..96772df90 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -48,10 +48,11 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.dafny-version-list) }}
-        # The Rust backend didn't exist yet in Dafny 4.2
-        exclude:
-          - dafny-version: 4.2.0
+        # Rust code generation is under development and depends on pending changes to the
+        # Dafny Rust code generation, so we only test on a relatively recent prerelease instead.
+        # This can be updated as needed when new features/fixes land in Dafny master.
+        dafny-version:
+          - nightly-2024-05-14-8da3ddd
     uses: ./.github/workflows/test_models_rust_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}
diff --git a/TestModels/SimpleTypes/SimpleBoolean/codegen-patches/rust/dafny-4.5.0.patch b/TestModels/SimpleTypes/SimpleBoolean/codegen-patches/rust/dafny-4.5.0.patch
index ffac54632..d8a9a0b66 100644
--- a/TestModels/SimpleTypes/SimpleBoolean/codegen-patches/rust/dafny-4.5.0.patch
+++ b/TestModels/SimpleTypes/SimpleBoolean/codegen-patches/rust/dafny-4.5.0.patch
@@ -1,20 +1,15 @@
 diff --git b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/dafny_impl/src/implementation_from_dafny.rs a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/dafny_impl/src/implementation_from_dafny.rs
-index 5200278d..dd0ece8a 100644
+index ba5de6ff..dd0ece8a 100644
 --- b/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/dafny_impl/src/implementation_from_dafny.rs
 +++ a/TestModels/SimpleTypes/SimpleBoolean/runtimes/rust/dafny_impl/src/implementation_from_dafny.rs
-@@ -1,103 +1,522 @@
+@@ -1,89 +1,522 @@
  #![allow(warnings, unconditional_panic)]
  #![allow(nonstandard_style)]
 -extern crate dafny_runtime;
 -mod _System {
 -  #[derive(Clone, PartialEq)]
 -  #[repr(transparent)]
--  pub struct nat(pub ::dafny_runtime::BigInt);
--  impl ::dafny_runtime::DafnyErasable for nat {
--    type Erased = ::dafny_runtime::BigInt;
--  }
--  impl ::dafny_runtime::DafnyUnerasable<::dafny_runtime::BigInt> for nat {}
--  impl ::dafny_runtime::DafnyUnerasable<nat> for nat {}
+-  pub struct nat(pub ::dafny_runtime::DafnyInt);
 -  impl ::std::default::Default for nat {
 -    fn default() -> Self {
 -      nat(::std::default::Default::default())
@@ -26,18 +21,17 @@ index 5200278d..dd0ece8a 100644
 -    }
 -  }
 -  impl ::std::ops::Deref for nat {
--    type Target = ::dafny_runtime::BigInt;
+-    type Target = ::dafny_runtime::DafnyInt;
 -    fn deref(&self) -> &Self::Target {
 -      &self.0
 -    }
 -  }
 -  #[derive(PartialEq)]
--  pub enum Tuple2<T0,T1> {
+-  pub enum Tuple2<T0, T1> {
 -    _T2 { _0: T0, _1: T1 },
 -    _PhantomVariant(::std::marker::PhantomData::<T0>, ::std::marker::PhantomData::<T1>)
 -  }
--  impl <T0: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T0> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + 'static,T1: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T1> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + 'static>Tuple2<T0,T1>
--     where <T0 as ::dafny_runtime::DafnyErasable>::Erased: ::std::cmp::PartialEq, <T1 as ::dafny_runtime::DafnyErasable>::Erased: ::std::cmp::PartialEq,  {
+-  impl <T0: Clone + ::dafny_runtime::DafnyPrint + 'static, T1: Clone + ::dafny_runtime::DafnyPrint + 'static>Tuple2<T0, T1> {
 -    pub fn _0(&self) -> &T0 {
 -      match self {
 -        Tuple2::_T2 { _0, _1, } => _0,
@@ -51,11 +45,7 @@ index 5200278d..dd0ece8a 100644
 -      }
 -    }
 -  }
--  impl <T0: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T0> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + 'static,T1: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T1> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + 'static>::dafny_runtime::DafnyErasable for Tuple2<T0,T1> {
--    type Erased = Tuple2<T0::Erased, T1::Erased, >;
--  }
--  impl <T0__Erased, T0: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T0> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + ::dafny_runtime::DafnyUnerasable<T0__Erased> + 'static,T1__Erased, T1: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T1> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + ::dafny_runtime::DafnyUnerasable<T1__Erased> + 'static>::dafny_runtime::DafnyUnerasable<Tuple2<T0__Erased, T1__Erased, >> for Tuple2<T0,T1> {}
--  impl <T0: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T0> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + 'static,T1: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T1> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + 'static>::dafny_runtime::DafnyPrint for Tuple2<T0,T1> {
+-  impl <T0: Clone + ::dafny_runtime::DafnyPrint + 'static, T1: Clone + ::dafny_runtime::DafnyPrint + 'static>::dafny_runtime::DafnyPrint for Tuple2<T0, T1> {
 -    fn fmt_print(&self, _formatter: &mut ::std::fmt::Formatter, _in_seq: bool) -> std::fmt::Result {
 -      match self {
 -        Tuple2::_T2 { _0, _1, } => {
@@ -180,7 +170,7 @@ index 5200278d..dd0ece8a 100644
 -      }
 -    }
 -  }
--  impl <T0: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T0> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + 'static,T1: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T1> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + 'static>::std::default::Default for Tuple2<T0,T1> {
+-  impl <T0: ::std::default::Default, T1: ::std::default::Default>::std::default::Default for Tuple2<T0, T1> {
 -    fn default() -> Self {
 -      Tuple2::_T2 {
 -        _0: ::std::default::Default::default(),
@@ -193,10 +183,6 @@ index 5200278d..dd0ece8a 100644
 -    _T0 {}
 -  }
 -  impl Tuple0 {}
--  impl ::dafny_runtime::DafnyErasable for Tuple0 {
--    type Erased = Tuple0;
--  }
--  impl ::dafny_runtime::DafnyUnerasable<Tuple0> for Tuple0 {}
 -  impl ::dafny_runtime::DafnyPrint for Tuple0 {
 -    fn fmt_print(&self, _formatter: &mut ::std::fmt::Formatter, _in_seq: bool) -> std::fmt::Result {
 -      match self {
diff --git a/TestModels/SimpleTypes/SimpleString/codegen-patches/rust/dafny-4.5.0.patch b/TestModels/SimpleTypes/SimpleString/codegen-patches/rust/dafny-4.5.0.patch
index f70b25bca..340c7cacb 100644
--- a/TestModels/SimpleTypes/SimpleString/codegen-patches/rust/dafny-4.5.0.patch
+++ b/TestModels/SimpleTypes/SimpleString/codegen-patches/rust/dafny-4.5.0.patch
@@ -1,20 +1,15 @@
 diff --git b/TestModels/SimpleTypes/SimpleString/runtimes/rust/dafny_impl/src/implementation_from_dafny.rs a/TestModels/SimpleTypes/SimpleString/runtimes/rust/dafny_impl/src/implementation_from_dafny.rs
-index 5200278d..469a527f 100644
+index ba5de6ff..469a527f 100644
 --- b/TestModels/SimpleTypes/SimpleString/runtimes/rust/dafny_impl/src/implementation_from_dafny.rs
 +++ a/TestModels/SimpleTypes/SimpleString/runtimes/rust/dafny_impl/src/implementation_from_dafny.rs
-@@ -1,103 +1,637 @@
+@@ -1,89 +1,637 @@
  #![allow(warnings, unconditional_panic)]
  #![allow(nonstandard_style)]
 -extern crate dafny_runtime;
 -mod _System {
 -  #[derive(Clone, PartialEq)]
 -  #[repr(transparent)]
--  pub struct nat(pub ::dafny_runtime::BigInt);
--  impl ::dafny_runtime::DafnyErasable for nat {
--    type Erased = ::dafny_runtime::BigInt;
--  }
--  impl ::dafny_runtime::DafnyUnerasable<::dafny_runtime::BigInt> for nat {}
--  impl ::dafny_runtime::DafnyUnerasable<nat> for nat {}
+-  pub struct nat(pub ::dafny_runtime::DafnyInt);
 -  impl ::std::default::Default for nat {
 -    fn default() -> Self {
 -      nat(::std::default::Default::default())
@@ -26,18 +21,17 @@ index 5200278d..469a527f 100644
 -    }
 -  }
 -  impl ::std::ops::Deref for nat {
--    type Target = ::dafny_runtime::BigInt;
+-    type Target = ::dafny_runtime::DafnyInt;
 -    fn deref(&self) -> &Self::Target {
 -      &self.0
 -    }
 -  }
 -  #[derive(PartialEq)]
--  pub enum Tuple2<T0,T1> {
+-  pub enum Tuple2<T0, T1> {
 -    _T2 { _0: T0, _1: T1 },
 -    _PhantomVariant(::std::marker::PhantomData::<T0>, ::std::marker::PhantomData::<T1>)
 -  }
--  impl <T0: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T0> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + 'static,T1: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T1> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + 'static>Tuple2<T0,T1>
--     where <T0 as ::dafny_runtime::DafnyErasable>::Erased: ::std::cmp::PartialEq, <T1 as ::dafny_runtime::DafnyErasable>::Erased: ::std::cmp::PartialEq,  {
+-  impl <T0: Clone + ::dafny_runtime::DafnyPrint + 'static, T1: Clone + ::dafny_runtime::DafnyPrint + 'static>Tuple2<T0, T1> {
 -    pub fn _0(&self) -> &T0 {
 -      match self {
 -        Tuple2::_T2 { _0, _1, } => _0,
@@ -51,11 +45,7 @@ index 5200278d..469a527f 100644
 -      }
 -    }
 -  }
--  impl <T0: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T0> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + 'static,T1: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T1> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + 'static>::dafny_runtime::DafnyErasable for Tuple2<T0,T1> {
--    type Erased = Tuple2<T0::Erased, T1::Erased, >;
--  }
--  impl <T0__Erased, T0: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T0> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + ::dafny_runtime::DafnyUnerasable<T0__Erased> + 'static,T1__Erased, T1: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T1> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + ::dafny_runtime::DafnyUnerasable<T1__Erased> + 'static>::dafny_runtime::DafnyUnerasable<Tuple2<T0__Erased, T1__Erased, >> for Tuple2<T0,T1> {}
--  impl <T0: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T0> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + 'static,T1: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T1> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + 'static>::dafny_runtime::DafnyPrint for Tuple2<T0,T1> {
+-  impl <T0: Clone + ::dafny_runtime::DafnyPrint + 'static, T1: Clone + ::dafny_runtime::DafnyPrint + 'static>::dafny_runtime::DafnyPrint for Tuple2<T0, T1> {
 -    fn fmt_print(&self, _formatter: &mut ::std::fmt::Formatter, _in_seq: bool) -> std::fmt::Result {
 -      match self {
 -        Tuple2::_T2 { _0, _1, } => {
@@ -133,7 +123,7 @@ index 5200278d..469a527f 100644
 -      }
 -    }
 -  }
--  impl <T0: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T0> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + 'static,T1: ::dafny_runtime::DafnyErasable + ::dafny_runtime::DafnyUnerasable<T1> + Clone + ::dafny_runtime::DafnyPrint + ::std::default::Default + 'static>::std::default::Default for Tuple2<T0,T1> {
+-  impl <T0: ::std::default::Default, T1: ::std::default::Default>::std::default::Default for Tuple2<T0, T1> {
 -    fn default() -> Self {
 -      Tuple2::_T2 {
 -        _0: ::std::default::Default::default(),
@@ -146,10 +136,6 @@ index 5200278d..469a527f 100644
 -    _T0 {}
 -  }
 -  impl Tuple0 {}
--  impl ::dafny_runtime::DafnyErasable for Tuple0 {
--    type Erased = Tuple0;
--  }
--  impl ::dafny_runtime::DafnyUnerasable<Tuple0> for Tuple0 {}
 -  impl ::dafny_runtime::DafnyPrint for Tuple0 {
 -    fn fmt_print(&self, _formatter: &mut ::std::fmt::Formatter, _in_seq: bool) -> std::fmt::Result {
 -      match self {