Support for renaming using the rename attribute in charon (#239)

* support for renaming using the rename attribute in charon

* support for global decl

* add support for renaming field

* applied suggested changes and began adding support for variant

* finished support for renaming variant

* applied suggested changes

* add tests

* fixed variant and field renaming

* update charon-pin

* update flake.lock

* Update the charon pin

* Fix an issue with renaming trait method implementations

* Fix an issue with the renaming of trait implementations

* Fix an issue when renaming enumerations

* Update the Charon pin

* Fix the F* tests

* Fix an issue with the spans for the loops

* Fix the tests

* Update a comment

* Use fuel in the coq tests

* Generate the template decreases clauses by default

---------

Co-authored-by: Escherichia <escherichia@charlotte>
Co-authored-by: Son Ho <hosonmarc@gmail.com>

1 files changed, 92 insertions, 0 deletions

diff --git a/tests/lean/RenameAttribute.lean b/tests/lean/RenameAttribute.lean
new file mode 100644
index 00000000..ef42f4c5
--- /dev/null
+++ b/tests/lean/RenameAttribute.lean
@@ -0,0 +1,92 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [rename_attribute]
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace rename_attribute
+
+/- Trait declaration: [rename_attribute::BoolTrait]
+   Source: 'tests/src/rename_attribute.rs', lines 8:0-8:19 -/
+structure BoolTest (Self : Type) where
+  getTest : Self → Result Bool
+
+/- [rename_attribute::{(rename_attribute::BoolTrait for bool)}::get_bool]:
+   Source: 'tests/src/rename_attribute.rs', lines 22:4-22:30 -/
+def BoolTraitBool.getTest (self : Bool) : Result Bool :=
+  Result.ok self
+
+/- Trait implementation: [rename_attribute::{(rename_attribute::BoolTrait for bool)}]
+   Source: 'tests/src/rename_attribute.rs', lines 21:0-21:23 -/
+def BoolImpl : BoolTest Bool := {
+  getTest := BoolTraitBool.getTest
+}
+
+/- [rename_attribute::BoolTrait::ret_true]:
+   Source: 'tests/src/rename_attribute.rs', lines 15:4-15:30 -/
+def BoolTrait.retTest
+  {Self : Type} (self_clause : BoolTest Self) (self : Self) : Result Bool :=
+  Result.ok true
+
+/- [rename_attribute::test_bool_trait]:
+   Source: 'tests/src/rename_attribute.rs', lines 28:0-28:42 -/
+def BoolFn (T : Type) (x : Bool) : Result Bool :=
+  do
+  let b ← BoolTraitBool.getTest x
+  if b
+  then BoolTrait.retTest BoolImpl x
+  else Result.ok false
+
+/- [rename_attribute::SimpleEnum]
+   Source: 'tests/src/rename_attribute.rs', lines 36:0-36:15 -/
+inductive VariantsTest :=
+| Variant1 : VariantsTest
+| SecondVariant : VariantsTest
+| ThirdVariant : VariantsTest
+
+/- [rename_attribute::Foo]
+   Source: 'tests/src/rename_attribute.rs', lines 44:0-44:10 -/
+structure StructTest where
+  FieldTest : U32
+
+/- [rename_attribute::C]
+   Source: 'tests/src/rename_attribute.rs', lines 50:0-50:12 -/
+def Const_Test_body : Result U32 := do
+                                    let i ← 100#u32 + 10#u32
+                                    i + 1#u32
+def Const_Test : U32 := eval_global Const_Test_body
+
+/- [rename_attribute::CA]
+   Source: 'tests/src/rename_attribute.rs', lines 53:0-53:13 -/
+def Const_Aeneas11_body : Result U32 := 10#u32 + 1#u32
+def Const_Aeneas11 : U32 := eval_global Const_Aeneas11_body
+
+/- [rename_attribute::factorial]:
+   Source: 'tests/src/rename_attribute.rs', lines 56:0-56:27 -/
+divergent def Factfn (n : U64) : Result U64 :=
+  if n <= 1#u64
+  then Result.ok 1#u64
+  else do
+       let i ← n - 1#u64
+       let i1 ← Factfn i
+       n * i1
+
+/- [rename_attribute::sum]: loop 0:
+   Source: 'tests/src/rename_attribute.rs', lines 67:4-75:1 -/
+divergent def No_borrows_sum_loop
+  (max : U32) (i : U32) (s : U32) : Result U32 :=
+  if i < max
+  then do
+       let s1 ← s + i
+       let i1 ← i + 1#u32
+       No_borrows_sum_loop max i1 s1
+  else s * 2#u32
+
+/- [rename_attribute::sum]:
+   Source: 'tests/src/rename_attribute.rs', lines 65:0-65:27 -/
+def No_borrows_sum (max : U32) : Result U32 :=
+  No_borrows_sum_loop max 0#u32 0#u32
+
+end rename_attribute