Update charon

AeneasVerif · Nov 27, 2024 · 329c61d · 329c61d
1 parent 267526a
commit 329c61d
Show file tree

Hide file tree

Showing 5 changed files with 50 additions and 50 deletions.
diff --git a/charon-pin b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-3402870cbf5b49d92fd18c312831ef30a14e6a5b
+5e08e7a942caf19c8a3b48ba400316d783f672ed
diff --git a/flake.lock b/flake.lock
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
@@ -225,30 +225,13 @@ Definition TestType_t (T : Type) : Type := T.
     Source: 'tests/src/traits.rs', lines 129:8-129:30 *)
 Definition TestType_test_TestType1_t : Type := u64.
 
-(** Trait declaration: [traits::{traits::TestType<T>}#6::test::TestTrait]
-    Source: 'tests/src/traits.rs', lines 130:8-132:9 *)
-Record TestType_test_TestTrait_t (Self : Type) := mkTestType_test_TestTrait_t {
-  TestType_test_TestTrait_t_test : Self -> result bool;
-}.
-
-Arguments mkTestType_test_TestTrait_t { _ }.
-Arguments TestType_test_TestTrait_t_test { _ } _.
-
 (** [traits::{traits::TestType<T>}#6::test::{traits::{traits::TestType<T>}#6::test::TestTrait for traits::{traits::TestType<T>}#6::test::TestType1}::test]:
     Source: 'tests/src/traits.rs', lines 141:12-143:13 *)
 Definition testType_test_TestTraittraitsTestTypetestTestType1_test
   (self : TestType_test_TestType1_t) : result bool :=
   Ok (self s> 1%u64)
 .
 
-(** Trait implementation: [traits::{traits::TestType<T>}#6::test::{traits::{traits::TestType<T>}#6::test::TestTrait for traits::{traits::TestType<T>}#6::test::TestType1}]
-    Source: 'tests/src/traits.rs', lines 140:8-144:9 *)
-Definition TestType_test_TestTraittraitsTestTypetestTestType1 :
-  TestType_test_TestTrait_t TestType_test_TestType1_t := {|
-  TestType_test_TestTrait_t_test :=
-    testType_test_TestTraittraitsTestTypetestTestType1_test;
-|}.
-
 (** [traits::{traits::TestType<T>}#6::test]:
     Source: 'tests/src/traits.rs', lines 128:4-149:5 *)
 Definition testType_test
@@ -713,4 +696,21 @@ Definition use_foo2
   Ok (foo_foo T traitInst)
 .
 
+(** Trait declaration: [traits::{traits::TestType<T>}#6::test::TestTrait]
+    Source: 'tests/src/traits.rs', lines 130:8-132:9 *)
+Record TestType_test_TestTrait_t (Self : Type) := mkTestType_test_TestTrait_t {
+  TestType_test_TestTrait_t_test : Self -> result bool;
+}.
+
+Arguments mkTestType_test_TestTrait_t { _ }.
+Arguments TestType_test_TestTrait_t_test { _ } _.
+
+(** Trait implementation: [traits::{traits::TestType<T>}#6::test::{traits::{traits::TestType<T>}#6::test::TestTrait for traits::{traits::TestType<T>}#6::test::TestType1}]
+    Source: 'tests/src/traits.rs', lines 140:8-144:9 *)
+Definition TestType_test_TestTraittraitsTestTypetestTestType1 :
+  TestType_test_TestTrait_t TestType_test_TestType1_t := {|
+  TestType_test_TestTrait_t_test :=
+    testType_test_TestTraittraitsTestTypetestTestType1_test;
+|}.
+
 End Traits.
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
@@ -178,25 +178,12 @@ type testType_t (t : Type0) = t
     Source: 'tests/src/traits.rs', lines 129:8-129:30 *)
 type testType_test_TestType1_t = u64
 
-(** Trait declaration: [traits::{traits::TestType<T>}#6::test::TestTrait]
-    Source: 'tests/src/traits.rs', lines 130:8-132:9 *)
-noeq type testType_test_TestTrait_t (self : Type0) = {
-  test : self -> result bool;
-}
-
 (** [traits::{traits::TestType<T>}#6::test::{traits::{traits::TestType<T>}#6::test::TestTrait for traits::{traits::TestType<T>}#6::test::TestType1}::test]:
     Source: 'tests/src/traits.rs', lines 141:12-143:13 *)
 let testType_test_TestTraittraitsTestTypetestTestType1_test
   (self : testType_test_TestType1_t) : result bool =
   Ok (self > 1)
 
-(** Trait implementation: [traits::{traits::TestType<T>}#6::test::{traits::{traits::TestType<T>}#6::test::TestTrait for traits::{traits::TestType<T>}#6::test::TestType1}]
-    Source: 'tests/src/traits.rs', lines 140:8-144:9 *)
-let testType_test_TestTraittraitsTestTypetestTestType1 :
-  testType_test_TestTrait_t testType_test_TestType1_t = {
-  test = testType_test_TestTraittraitsTestTypetestTestType1_test;
-}
-
 (** [traits::{traits::TestType<T>}#6::test]:
     Source: 'tests/src/traits.rs', lines 128:4-149:5 *)
 let testType_test
@@ -535,3 +522,16 @@ let use_foo2
   =
   Ok (foo_foo t traitInst)
 
+(** Trait declaration: [traits::{traits::TestType<T>}#6::test::TestTrait]
+    Source: 'tests/src/traits.rs', lines 130:8-132:9 *)
+noeq type testType_test_TestTrait_t (self : Type0) = {
+  test : self -> result bool;
+}
+
+(** Trait implementation: [traits::{traits::TestType<T>}#6::test::{traits::{traits::TestType<T>}#6::test::TestTrait for traits::{traits::TestType<T>}#6::test::TestType1}]
+    Source: 'tests/src/traits.rs', lines 140:8-144:9 *)
+let testType_test_TestTraittraitsTestTypetestTestType1 :
+  testType_test_TestTrait_t testType_test_TestType1_t = {
+  test = testType_test_TestTraittraitsTestTypetestTestType1_test;
+}
+
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
@@ -202,25 +202,12 @@ def h4
    Source: 'tests/src/traits.rs', lines 129:8-129:30 -/
 @[reducible] def TestType.test.TestType1 := U64
 
-/- Trait declaration: [traits::{traits::TestType<T>}#6::test::TestTrait]
-   Source: 'tests/src/traits.rs', lines 130:8-132:9 -/
-structure TestType.test.TestTrait (Self : Type) where
-  test : Self → Result Bool
-
 /- [traits::{traits::TestType<T>}#6::test::{traits::{traits::TestType<T>}#6::test::TestTrait for traits::{traits::TestType<T>}#6::test::TestType1}::test]:
    Source: 'tests/src/traits.rs', lines 141:12-143:13 -/
 def TestType.test.TestTraittraitsTestTypetestTestType1.test
   (self : TestType.test.TestType1) : Result Bool :=
   Result.ok (self > 1#u64)
 
-/- Trait implementation: [traits::{traits::TestType<T>}#6::test::{traits::{traits::TestType<T>}#6::test::TestTrait for traits::{traits::TestType<T>}#6::test::TestType1}]
-   Source: 'tests/src/traits.rs', lines 140:8-144:9 -/
-@[reducible]
-def TestType.test.TestTraittraitsTestTypetestTestType1 :
-  TestType.test.TestTrait TestType.test.TestType1 := {
-  test := TestType.test.TestTraittraitsTestTypetestTestType1.test
-}
-
 /- [traits::{traits::TestType<T>}#6::test]:
    Source: 'tests/src/traits.rs', lines 128:4-149:5 -/
 def TestType.test
@@ -563,4 +550,17 @@ def use_foo2
   :=
   Result.ok (Foo.FOO T TraitInst)
 
+/- Trait declaration: [traits::{traits::TestType<T>}#6::test::TestTrait]
+   Source: 'tests/src/traits.rs', lines 130:8-132:9 -/
+structure TestType.test.TestTrait (Self : Type) where
+  test : Self → Result Bool
+
+/- Trait implementation: [traits::{traits::TestType<T>}#6::test::{traits::{traits::TestType<T>}#6::test::TestTrait for traits::{traits::TestType<T>}#6::test::TestType1}]
+   Source: 'tests/src/traits.rs', lines 140:8-144:9 -/
+@[reducible]
+def TestType.test.TestTraittraitsTestTypetestTestType1 :
+  TestType.test.TestTrait TestType.test.TestType1 := {
+  test := TestType.test.TestTraittraitsTestTypetestTestType1.test
+}
+
 end traits