experiment: support migration via extended stable interfaces

doc/md/examples/grammar.txt

@@ -336,5 +336,6 @@
 <prog> ::= 
     <list(<imp>, ';')> <list(<dec>, ';')> 
 
+    <list(<typ_dec>, ';')> 'actor' '(' '{' <list(<stab_field>, ';')> '}' ',' '{' <list(<stab_field>, ';')> '}' ')'
 
 

src/lowering/desugar.ml

@@ -541,7 +541,7 @@ and build_actor at ts exp_opt self_id es obj_typ =
   let pairs = List.map2 stabilize stabs ds in
   let idss = List.map fst pairs in
   let ids = List.concat idss in
-  let sig_ = List.sort T.compare_field
+  let sig_post = List.sort T.compare_field
     (List.map (fun (i,t) -> T.{lab = i; typ = t; src = empty_src}) ids)
   in
   let fields = List.map (fun (i,t) -> T.{lab = i; typ = T.Opt (T.as_immut t); src = T.empty_src}) ids in
@@ -550,30 +550,40 @@ and build_actor at ts exp_opt self_id es obj_typ =
   let state = fresh_var "state" (T.Mut (T.Opt ty)) in
   let get_state = fresh_var "getState" (T.Func(T.Local, T.Returns, [], [], [ty])) in
   let ds = List.map (fun mk_d -> mk_d get_state) mk_ds in
-  let stable_type, migration = match exp_opt with
+  let sig_, stable_type, migration = match exp_opt with
     | None ->
+      T.Single sig_post,
       I.{pre = ty; post = ty},
       primE (I.ICStableRead ty) [] (* as before *)
     | Some exp0 ->
       let e = exp exp0 in
       let [@warning "-8"] (_s,_c, [], [dom], [rng]) = T.as_func (exp0.note.S.note_typ) in
       let [@warning "-8"] (T.Object, dom_fields) = T.as_obj dom in
       let [@warning "-8"] (T.Object, rng_fields) = T.as_obj rng in
+      let sig_pre =
+         List.sort T.compare_field
+           (dom_fields @
+              (List.filter_map
+                 (fun (i,t) ->
+                   match T.lookup_val_field_opt i dom_fields with
+                   | Some t ->
+                     (* ignore overriden *)
+                     None
+                   | None ->
+                    (* retain others *)
+                   Some T.{lab = i; typ = t; src = T.empty_src})                                                   ids))
+      in
       let fields' =
            List.map
-             (fun (i,t) ->
-                T.{lab = i; typ = T.Opt (T.as_immut t); src = T.empty_src})
-             ((List.map (fun T.{lab;typ;_} -> (lab,typ)) dom_fields) @
-                (List.filter_map
-                   (fun (i,t) ->
-                     match T.lookup_val_field_opt i dom_fields with
-                     | Some t -> None (* ignore overriden *)
-                     | None -> Some (i, t) (* retain others *))
-                   ids)) in
-      let ty' = T.Obj (T.Memory, List.sort T.compare_field fields') in
+             (fun tf ->
+               { tf with T.typ = T.Opt (T.as_immut tf.T.typ) })
+             sig_pre
+      in
+      let ty' = T.Obj (T.Memory, fields') in
       let v = fresh_var "v" ty' in
       let v_dom = fresh_var "v_dom" dom in
       let v_rng = fresh_var "v_rng" rng in
+      T.PrePost (sig_pre, sig_post),
       I.{pre = ty'; post = ty},
       ifE (primE (I.OtherPrim "rts_in_install") [])
         (primE (I.ICStableRead ty) [])

src/mo_def/syntax.ml

@@ -235,7 +235,11 @@ and prog' = dec list
 (* Signatures (stable variables) *)
 
 type stab_sig = (stab_sig', prog_note) Source.annotated_phrase
-and stab_sig' = (dec list * typ_field list)      (* type declarations & stable actor fields *)
+and stab_sig' = (dec list * stab_body)      (* type declarations & stable actor fields *)
+and stab_body = stab_body' Source.phrase    (* type declarations & stable actor fields *)
+and stab_body' =
+  | Single of typ_field list
+  | PrePost of typ_field list * typ_field list
 
 (* Compilation units *)
 

src/mo_frontend/parser.mly

@@ -997,7 +997,22 @@ stab_field :
 parse_stab_sig :
   | start ds=seplist(typ_dec, semicolon) ACTOR LCURLY sfs=seplist(stab_field, semicolon) RCURLY
     { let trivia = !triv_table in
-      fun filename -> { it = (ds, sfs); at = at $sloc; note = { filename; trivia }}
+      let sigs = Single sfs in
+      fun filename -> {
+          it = (ds, {it=sigs; at = at $sloc; note = ()});
+          at = at $sloc;
+          note =
+          { filename; trivia }}
+    }
+  | start ds=seplist(typ_dec, semicolon)
+       ACTOR LPAR LCURLY sfs_pre=seplist(stab_field, semicolon) RCURLY COMMA
+             LCURLY sfs_post=seplist(stab_field, semicolon) RCURLY  RPAR
+    { let trivia = !triv_table in
+      let sigs = PrePost(sfs_pre, sfs_post) in (* FIX ME*)
+      fun filename -> {
+          it = (ds, {it=sigs; at = at $sloc; note = ()});
+          at = at $sloc;
+          note = { filename; trivia }}
     }
 
 %%

src/mo_frontend/stability.ml

@@ -31,16 +31,18 @@ let error_sub s tf1 tf2 =
 
 (* Relaxed rules with enhanced orthogonal persistence for more flexible upgrades.
    - Mutability of stable fields can be changed because they are never aliased.
-   - Stable fields can be dropped, however, with a warning of potential data loss. 
+   - Stable fields can be dropped, however, with a warning of potential data loss.
      For this, we give up the transitivity property of upgrades.
 
-   Upgrade transitivity means that an upgrade from a program A to B and then from B to C 
-   should have the same effect as directly upgrading from A to C. If B discards a field 
-   and C re-adds it, this transitivity is no longer maintained. However, rigorous upgrade 
+   Upgrade transitivity means that an upgrade from a program A to B and then from B to C
+   should have the same effect as directly upgrading from A to C. If B discards a field
+   and C re-adds it, this transitivity is no longer maintained. However, rigorous upgrade
    transitivity was also not guaranteed before, since B may contain initialization logic
    or pre-/post-upgrade hooks that alter the stable data.
 *)
-let match_stab_sig tfs1 tfs2 : unit Diag.result =
+let match_stab_sig sig1 sig2 : unit Diag.result =
+  let tfs1 = post sig1 in
+  let tfs2 = pre sig2 in
   (* Assume that tfs1 and tfs2 are sorted. *)
   let res = Diag.with_message_store (fun s ->
     let rec go tfs1 tfs2 = match tfs1, tfs2 with
@@ -59,7 +61,7 @@ let match_stab_sig tfs1 tfs2 : unit Diag.result =
          | -1 ->
            (* dropped field is allowed with warning, recurse on tfs1' *)
            warning_discard s tf1;
-           go tfs1' tfs2 
+           go tfs1' tfs2
          | _ ->
            go tfs1 tfs2' (* new field ok, recurse on tfs2' *)
         )
@@ -68,8 +70,8 @@ let match_stab_sig tfs1 tfs2 : unit Diag.result =
   (* cross check with simpler definition *)
   match res with
   | Ok _ ->
-    assert (Type.match_stab_sig tfs1 tfs2);
+    assert (Type.match_stab_sig sig1 sig2);
     res
   | Error _ ->
-    assert (not (Type.match_stab_sig tfs1 tfs2));
+    assert (not (Type.match_stab_sig sig1 sig2));
     res

src/mo_frontend/stability.mli

@@ -6,4 +6,4 @@ open Mo_types
    c.f. (simpler) Types.match_sig.
 *)
 
-val match_stab_sig : Type.field list -> Type.field list -> unit Diag.result
+val match_stab_sig : Type.stab_sig -> Type.stab_sig -> unit Diag.result

src/mo_frontend/typing.ml

@@ -3214,33 +3214,39 @@ let check_lib scope pkg_opt lib : Scope.t Diag.result =
         ) lib
     )
 
-let check_stab_sig scope sig_ : (T.field list) Diag.result =
+let check_stab_sig scope sig_ : T.stab_sig  Diag.result =
   Diag.with_message_store
     (fun msgs ->
       recover_opt
         (fun (decs, sfs) ->
           let env = env_of_scope msgs scope in
           let scope = infer_block_decs env decs sig_.at in
           let env1 = adjoin env scope in
-          check_ids env "object type" "field"
-            (List.filter_map (fun (field : typ_field) ->
-                 match field.it with ValF (id, _, _) -> Some id | _ -> None)
-               sfs);
-          check_ids env "object type" "type field"
-            (List.filter_map (fun (field : typ_field) ->
-                 match field.it with TypF (id, _, _) -> Some id | _ -> None)
-               sfs);
-          let _ = List.map (check_typ_field {env1 with pre = true} T.Object) sfs in
-          let fs = List.map (check_typ_field {env1 with pre = false} T.Object) sfs in
-          List.iter (fun (field : Syntax.typ_field) ->
-              match field.it with
-              | TypF _ -> ()
-              | ValF (id, typ, _) ->
-                if not (T.stable typ.note) then
-                   error env id.at "M0131" "variable %s is declared stable but has non-stable type%a"
-                   id.it
-                   display_typ typ.note)
-            sfs;
-          List.sort T.compare_field fs
+          let check_fields sfs =
+            check_ids env "object type" "field"
+              (List.filter_map (fun (field : typ_field) ->
+                   match field.it with ValF (id, _, _) -> Some id | _ -> None)
+                 sfs);
+            check_ids env "object type" "type field"
+              (List.filter_map (fun (field : typ_field) ->
+                   match field.it with TypF (id, _, _) -> Some id | _ -> None)
+                 sfs);
+            let _ = List.map (check_typ_field {env1 with pre = true} T.Object) sfs in
+            let fs = List.map (check_typ_field {env1 with pre = false} T.Object) sfs in
+            List.iter (fun (field : Syntax.typ_field) ->
+                match field.it with
+                | TypF _ -> ()
+                | ValF (id, typ, _) ->
+                  if not (T.stable typ.note) then
+                     error env id.at "M0131" "variable %s is declared stable but has non-stable type%a"
+                     id.it
+                     display_typ typ.note)
+              sfs;
+            List.sort T.compare_field fs
+          in
+          match sfs.it with
+          | Single sfs -> T.Single (check_fields sfs)
+          | PrePost (pre,post) ->
+             T.PrePost (check_fields pre, check_fields post)
         ) sig_.it
     )

src/mo_frontend/typing.mli

@@ -10,6 +10,6 @@ val infer_prog : ?viper_mode:bool -> scope -> string option -> Async_cap.async_c
 
 val check_lib : scope -> string option -> Syntax.lib -> scope Diag.result
 val check_actors : ?viper_mode:bool -> ?check_actors:bool -> scope -> Syntax.prog list -> unit Diag.result
-val check_stab_sig : scope -> Syntax.stab_sig -> (field list) Diag.result
+val check_stab_sig : scope -> Syntax.stab_sig -> Type.stab_sig Diag.result
 
 val heartbeat_type : typ

src/mo_types/type.ml

@@ -72,6 +72,11 @@ and kind =
 
 let empty_src = {depr = None; region = Source.no_region}
 
+(* Stable signatures *)
+type stab_sig =
+  | Single of field list
+  | PrePost of field list * field list
+
 (* Efficient comparison *)
 let tag_prim = function
   | Null -> 0
@@ -1754,11 +1759,15 @@ and pp_kind ppf k =
   pp_kind' vs ppf k
 
 and pp_stab_sig ppf sig_ =
+  let all_fields = match sig_ with
+    | Single tfs -> tfs
+    | PrePost (pre, post) -> pre @ post
+  in
   let cs = List.fold_right
     (cons_field false)
     (* false here ^ means ignore unreferenced Typ c components
        that would produce unreferenced bindings when unfolded *)
-    sig_ ConSet.empty in
+    all_fields ConSet.empty in
   let vs = vs_of_cs cs in
   let ds =
     let cs' = ConSet.filter (fun c ->
@@ -1776,15 +1785,22 @@ and pp_stab_sig ppf sig_ =
           typ = Typ c;
           src = empty_src }) ds)
   in
-  let pp_stab_fields ppf sig_ =
-    fprintf ppf "@[<v 2>%s{@;<0 0>%a@;<0 -2>}@]"
-      (string_of_obj_sort Actor)
-      (pp_print_list ~pp_sep:semi (pp_stab_field vs)) sig_
+  let pp_stab_actor ppf sig_ =
+    match sig_ with
+    | Single tfs ->
+      fprintf ppf "@[<v 2>%s{@;<0 0>%a@;<0 -2>}@]"
+        (string_of_obj_sort Actor)
+        (pp_print_list ~pp_sep:semi (pp_stab_field vs)) tfs
+    | PrePost (pre, post) ->
+      fprintf ppf "@[<v 2>%s({@;<0 0>%a@;<0 -2>}, {@;<0 0>%a@;<0 -2>}) @]"
+        (string_of_obj_sort Actor)
+        (pp_print_list ~pp_sep:semi (pp_stab_field vs)) pre
+        (pp_print_list ~pp_sep:semi (pp_stab_field vs)) post
   in
   fprintf ppf "@[<v 0>%a%a%a;@]"
-   (pp_print_list ~pp_sep:semi (pp_field vs)) fs
-   (if fs = [] then fun ppf () -> () else semi) ()
-   pp_stab_fields sig_
+    (pp_print_list ~pp_sep:semi (pp_field vs)) fs
+    (if fs = [] then fun ppf () -> () else semi) ()
+    pp_stab_actor sig_
 
 let rec pp_typ_expand' vs ppf t =
   match t with
@@ -1850,7 +1866,20 @@ let _ = str := string_of_typ
 
 (* Stable signatures *)
 
-let rec match_stab_sig tfs1 tfs2 =
+let pre = function
+  | Single tfs -> tfs
+  | PrePost (tfs, _) -> tfs
+
+let post = function
+  | Single tfs -> tfs
+  | PrePost (_, tfs) -> tfs
+
+let rec match_stab_sig sig1 sig2 =
+  let tfs1 = post sig1 in
+  let tfs2 = pre sig2 in
+  match_stab_fields tfs1 tfs2
+
+and match_stab_fields tfs1 tfs2 =
   (* Assume that tfs1 and tfs2 are sorted. *)
   match tfs1, tfs2 with
   | [], _ | _, [] ->
@@ -1860,16 +1889,17 @@ let rec match_stab_sig tfs1 tfs2 =
     (match compare_field tf1 tf2 with
      | 0 ->
        sub (as_immut tf1.typ) (as_immut tf2.typ) &&
-       match_stab_sig tfs1' tfs2'
+       match_stab_fields tfs1' tfs2'
      | -1 ->
        (* dropped field ok *)
-       match_stab_sig tfs1' tfs2
+       match_stab_fields tfs1' tfs2
      | _ ->
        (* new field ok *)
-       match_stab_sig tfs1 tfs2'
+       match_stab_fields tfs1 tfs2'
     )
 
-let string_of_stab_sig fields : string =
+let string_of_stab_sig stab_sig : string =
   let module Pretty = MakePretty(ParseableStamps) in
-  "// Version: 1.0.0\n" ^
-  Format.asprintf "@[<v 0>%a@]@\n" (fun ppf -> Pretty.pp_stab_sig ppf) fields
+  "// Version: 2.0\n" ^
+  Format.asprintf "@[<v 0>%a@]@\n" (fun ppf -> Pretty.pp_stab_sig ppf) stab_sig
+

src/mo_types/type.mli

@@ -262,9 +262,16 @@ val scope_bind : bind
 
 (* Signatures *)
 
-val match_stab_sig : field list -> field list -> bool
+type stab_sig =
+  | Single of field list
+  | PrePost of field list * field list
 
-val string_of_stab_sig : field list -> string
+val pre : stab_sig -> field list
+val post : stab_sig -> field list
+
+val match_stab_sig : stab_sig -> stab_sig -> bool
+
+val string_of_stab_sig : stab_sig -> string
 
 val motoko_runtime_information_type : typ