change the deep model of Box<T> to Box<T::DeepModelTy>

creusot-rs · Nov 10, 2023 · d82b211 · d82b211
1 parent 8453699
commit d82b211
Show file tree

Hide file tree

Showing 3 changed files with 224 additions and 2 deletions.
diff --git a/creusot-contracts/src/std/boxed.rs b/creusot-contracts/src/std/boxed.rs
@@ -3,11 +3,11 @@ pub use ::std::boxed::*;
 
 #[cfg(creusot)]
 impl<T: DeepModel + ?Sized, A: Allocator> DeepModel for Box<T, A> {
-    type DeepModelTy = T::DeepModelTy;
+    type DeepModelTy = Box<T::DeepModelTy>;
     #[ghost]
     #[open]
     fn deep_model(self) -> Self::DeepModelTy {
-        (*self).deep_model()
+        Box::new((*self).deep_model())
     }
 }
 

diff --git a/creusot/tests/should_succeed/syntax/derive_macros.mlcfg b/creusot/tests/should_succeed/syntax/derive_macros.mlcfg
@@ -1270,6 +1270,210 @@ module DeriveMacros_Impl7_Resolve
   val resolve [#"../derive_macros.rs" 56 9 56 16] (self : DeriveMacros_Sum2_Type.t_sum2 a b) : bool
     ensures { result = resolve self }
 
+end
+module Core_Option_Option_Type
+  type t_option 't =
+    | C_None
+    | C_Some 't
+
+end
+module DeriveMacros_List_Type
+  use Core_Option_Option_Type as Core_Option_Option_Type
+  type t_list 't =
+    | C_List 't (Core_Option_Option_Type.t_option (t_list 't))
+
+  let function list_elem (self : t_list 't) : 't = [@vc:do_not_keep_trace] [@vc:sp]
+    match (self) with
+      | C_List a _ -> a
+      end
+  let function list_tail (self : t_list 't) : Core_Option_Option_Type.t_option (t_list 't)
+   = [@vc:do_not_keep_trace] [@vc:sp]
+    match (self) with
+      | C_List _ a -> a
+      end
+end
+module DeriveMacros_ListDeepModel_Type
+  use Core_Option_Option_Type as Core_Option_Option_Type
+  type t_listdeepmodel 't 'proj0 =
+    | C_ListDeepModel 'proj0 (Core_Option_Option_Type.t_option (t_listdeepmodel 't 'proj0))
+
+end
+module CreusotContracts_Std1_Option_Impl0_DeepModel_Stub
+  type t
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  use Core_Option_Option_Type as Core_Option_Option_Type
+  function deep_model (self : Core_Option_Option_Type.t_option t) : Core_Option_Option_Type.t_option DeepModelTy0.deepModelTy
+
+end
+module CreusotContracts_Std1_Option_Impl0_DeepModel_Interface
+  type t
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  use Core_Option_Option_Type as Core_Option_Option_Type
+  function deep_model (self : Core_Option_Option_Type.t_option t) : Core_Option_Option_Type.t_option DeepModelTy0.deepModelTy
+
+  val deep_model (self : Core_Option_Option_Type.t_option t) : Core_Option_Option_Type.t_option DeepModelTy0.deepModelTy
+    ensures { result = deep_model self }
+
+end
+module CreusotContracts_Std1_Option_Impl0_DeepModel
+  type t
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with
+    type self = t,
+    type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy
+  use Core_Option_Option_Type as Core_Option_Option_Type
+  function deep_model (self : Core_Option_Option_Type.t_option t) : Core_Option_Option_Type.t_option DeepModelTy0.deepModelTy
+
+   =
+    [#"../../../../../creusot-contracts/src/std/option.rs" 10 8 13 9] match (self) with
+      | Core_Option_Option_Type.C_Some t -> Core_Option_Option_Type.C_Some (DeepModel0.deep_model t)
+      | Core_Option_Option_Type.C_None -> Core_Option_Option_Type.C_None
+      end
+  val deep_model (self : Core_Option_Option_Type.t_option t) : Core_Option_Option_Type.t_option DeepModelTy0.deepModelTy
+    ensures { result = deep_model self }
+
+end
+module Alloc_Boxed_Box_Type
+  use Core_Ptr_Unique_Unique_Type as Core_Ptr_Unique_Unique_Type
+  type t_box 't 'a =
+    | C_Box (Core_Ptr_Unique_Unique_Type.t_unique 't) 'a
+
+end
+module DeriveMacros_Impl8_DeepModel_Stub
+  type t
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  use DeriveMacros_ListDeepModel_Type as DeriveMacros_ListDeepModel_Type
+  use DeriveMacros_List_Type as DeriveMacros_List_Type
+  function deep_model [#"../derive_macros.rs" 62 9 62 18] (self : DeriveMacros_List_Type.t_list t) : DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy
+
+end
+module DeriveMacros_Impl8_DeepModel_Interface
+  type t
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  use DeriveMacros_ListDeepModel_Type as DeriveMacros_ListDeepModel_Type
+  use DeriveMacros_List_Type as DeriveMacros_List_Type
+  function deep_model [#"../derive_macros.rs" 62 9 62 18] (self : DeriveMacros_List_Type.t_list t) : DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy
+
+  val deep_model [#"../derive_macros.rs" 62 9 62 18] (self : DeriveMacros_List_Type.t_list t) : DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy
+    ensures { result = deep_model self }
+
+end
+module DeriveMacros_Impl8_DeepModel
+  type t
+  use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  use DeriveMacros_ListDeepModel_Type as DeriveMacros_ListDeepModel_Type
+  use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type
+  use Core_Option_Option_Type as Core_Option_Option_Type
+  use DeriveMacros_List_Type as DeriveMacros_List_Type
+  clone CreusotContracts_Std1_Option_Impl0_DeepModel_Stub as DeepModel1 with
+    type t = DeriveMacros_List_Type.t_list t,
+    type DeepModelTy0.deepModelTy = DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy
+  clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with
+    type self = t,
+    type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy
+  function deep_model [#"../derive_macros.rs" 62 9 62 18] (self : DeriveMacros_List_Type.t_list t) : DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy
+
+   =
+    [#"../derive_macros.rs" 62 9 729 44] DeriveMacros_ListDeepModel_Type.C_ListDeepModel (DeepModel0.deep_model (DeriveMacros_List_Type.list_elem self)) (DeepModel1.deep_model (DeriveMacros_List_Type.list_tail self))
+  val deep_model [#"../derive_macros.rs" 62 9 62 18] (self : DeriveMacros_List_Type.t_list t) : DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy
+    ensures { result = deep_model self }
+
+end
+module DeriveMacros_Expr_Type
+  type t_expr 'v =
+    | C_Var 'v
+    | C_Add (t_expr 'v) (t_expr 'v)
+
+end
+module DeriveMacros_ExprDeepModel_Type
+  type t_exprdeepmodel 'v 'proj0 =
+    | C_Var 'proj0
+    | C_Add (t_exprdeepmodel 'v 'proj0) (t_exprdeepmodel 'v 'proj0)
+
+end
+module CreusotContracts_Std1_Boxed_Impl0_DeepModel_Stub
+  type t
+  type a
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  function deep_model (self : t) : DeepModelTy0.deepModelTy
+end
+module CreusotContracts_Std1_Boxed_Impl0_DeepModel_Interface
+  type t
+  type a
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  function deep_model (self : t) : DeepModelTy0.deepModelTy
+  val deep_model (self : t) : DeepModelTy0.deepModelTy
+    ensures { result = deep_model self }
+
+end
+module CreusotContracts_Std1_Boxed_Impl0_DeepModel
+  type t
+  type a
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with
+    type self = t,
+    type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy
+  function deep_model (self : t) : DeepModelTy0.deepModelTy =
+    [#"../../../../../creusot-contracts/src/std/boxed.rs" 10 17 10 37] DeepModel0.deep_model self
+  val deep_model (self : t) : DeepModelTy0.deepModelTy
+    ensures { result = deep_model self }
+
+end
+module DeriveMacros_Impl9_DeepModel_Stub
+  type v
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = v
+  use DeriveMacros_ExprDeepModel_Type as DeriveMacros_ExprDeepModel_Type
+  use DeriveMacros_Expr_Type as DeriveMacros_Expr_Type
+  function deep_model [#"../derive_macros.rs" 68 9 68 18] (self : DeriveMacros_Expr_Type.t_expr v) : DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy
+
+end
+module DeriveMacros_Impl9_DeepModel_Interface
+  type v
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = v
+  use DeriveMacros_ExprDeepModel_Type as DeriveMacros_ExprDeepModel_Type
+  use DeriveMacros_Expr_Type as DeriveMacros_Expr_Type
+  function deep_model [#"../derive_macros.rs" 68 9 68 18] (self : DeriveMacros_Expr_Type.t_expr v) : DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy
+
+  val deep_model [#"../derive_macros.rs" 68 9 68 18] (self : DeriveMacros_Expr_Type.t_expr v) : DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy
+    ensures { result = deep_model self }
+
+end
+module DeriveMacros_Impl9_DeepModel
+  type v
+  use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = v
+  use DeriveMacros_ExprDeepModel_Type as DeriveMacros_ExprDeepModel_Type
+  use DeriveMacros_Expr_Type as DeriveMacros_Expr_Type
+  clone CreusotContracts_Std1_Boxed_Impl0_DeepModel_Stub as DeepModel1 with
+    type t = DeriveMacros_Expr_Type.t_expr v,
+    type a = Alloc_Alloc_Global_Type.t_global,
+    type DeepModelTy0.deepModelTy = DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy
+  clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with
+    type self = v,
+    type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy
+  function deep_model [#"../derive_macros.rs" 68 9 68 18] (self : DeriveMacros_Expr_Type.t_expr v) : DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy
+
+   =
+    [#"../derive_macros.rs" 68 9 68 18] match (self) with
+      | DeriveMacros_Expr_Type.C_Var v0_1 -> DeriveMacros_ExprDeepModel_Type.C_Var (DeepModel0.deep_model v0_1)
+      | DeriveMacros_Expr_Type.C_Add v0_1 v1_1 -> DeriveMacros_ExprDeepModel_Type.C_Add (DeepModel1.deep_model v0_1) (DeepModel1.deep_model v1_1)
+      end
+  val deep_model [#"../derive_macros.rs" 68 9 68 18] (self : DeriveMacros_Expr_Type.t_expr v) : DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy
+    ensures { result = deep_model self }
+
 end
 module DeriveMacros_Impl2
   type a
@@ -1385,6 +1589,12 @@ module DeriveMacros_Impl1
   type a
   type b
 end
+module DeriveMacros_Impl8
+  type t
+end
+module DeriveMacros_Impl9
+  type v
+end
 module DeriveMacros_Impl6
   type a
 end

diff --git a/creusot/tests/should_succeed/syntax/derive_macros.rs b/creusot/tests/should_succeed/syntax/derive_macros.rs
@@ -58,3 +58,15 @@ pub enum Sum2<A, B> {
     X(A),
     Y { a: bool, x: B },
 }
+
+#[derive(DeepModel)]
+pub struct List<T> {
+  pub elem: T,
+  pub tail : Option<Box<List<T>>>,
+}
+
+#[derive(DeepModel)]
+pub enum Expr<V> {
+    Var(V),
+    Add(Box<Expr<V>>, Box<Expr<V>>),
+}