refactor: move to DY*-extrinsic

Makefile

@@ -11,7 +11,8 @@ INNER_SOURCE_DIRS = api bootstrap common/code common/proofs glue/code glue/proof
 HACL_SNAPSHOT_DIR = $(MLS_HOME)/hacl-star-snapshot
 SOURCE_DIRS = $(addprefix $(MLS_HOME)/fstar/, $(INNER_SOURCE_DIRS))
 
-INCLUDE_DIRS = $(SOURCE_DIRS) $(HACL_SNAPSHOT_DIR)/lib $(HACL_SNAPSHOT_DIR)/specs $(COMPARSE_HOME)/src $(if $(USE_DY), $(DY_HOME) $(DY_HOME)/symbolic)
+DY_INCLUDE_DIRS = core lib lib/comparse lib/event lib/state lib/utils
+INCLUDE_DIRS = $(SOURCE_DIRS) $(HACL_SNAPSHOT_DIR)/lib $(HACL_SNAPSHOT_DIR)/specs $(COMPARSE_HOME)/src $(if $(USE_DY), $(addprefix $(DY_HOME)/src/, $(DY_INCLUDE_DIRS)))
 FSTAR_INCLUDE_DIRS = $(addprefix --include , $(INCLUDE_DIRS))
 
 ADMIT ?=
@@ -20,8 +21,7 @@ MAYBE_ADMIT = $(if $(ADMIT),--admit_smt_queries true)
 FSTAR_EXE ?= $(FSTAR_HOME)/bin/fstar.exe
 FSTAR = $(FSTAR_EXE) $(MAYBE_ADMIT)
 
-DY_EXTRACT = +CryptoLib +SecrecyLabels +ComparseGlue +LabeledCryptoAPI +CryptoEffect +GlobalRuntimeLib +LabeledRuntimeAPI +Ord +AttackerAPI
-FSTAR_EXTRACT = --extract '-* +MLS +Comparse -Comparse.Tactic $(if $(USE_DY), $(DY_EXTRACT))'
+FSTAR_EXTRACT = --extract '-* +MLS +Comparse -Comparse.Tactic $(if $(USE_DY), +DY)'
 
 # Allowed warnings:
 # - (Warning 242) Definitions of inner let-rec ... and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types
@@ -71,7 +71,7 @@ obj:
 cache/MLS.Test.fst.checked: FSTAR_RULE_FLAGS = --warn_error '+272'
 # Allow more warning in dependencies
 cache/Lib.IntTypes.fst.checked: FSTAR_RULE_FLAGS = --warn_error '+288+349'
-cache/SecrecyLabels.fst.checked: FSTAR_RULE_FLAGS = --warn_error '+337'
+cache/DY.Core.Bytes.Type.fst.checked: FSTAR_RULE_FLAGS = --warn_error '+290'
 
 %.checked: | hints obj
 	$(FSTAR) $(FSTAR_FLAGS) $(FSTAR_RULE_FLAGS) $< && touch -c $@

flake.nix

@@ -9,9 +9,11 @@
       inputs.fstar-flake.follows = "fstar-flake";
     };
 
-    dolev-yao-star-src = {
-      url = "github:Inria-Prosecco/treesync";
-      flake = false;
+    dolev-yao-star-flake = {
+      url = "github:REPROSEC/dolev-yao-star-extrinsic";
+      inputs.nixpkgs.follows = "nixpkgs";
+      inputs.fstar-flake.follows = "fstar-flake";
+      inputs.comparse-flake.follows = "comparse-flake";
     };
 
     hacl-packages-src = {
@@ -20,28 +22,15 @@
     };
   };
 
-  outputs = {self, nixpkgs, fstar-flake, comparse-flake, dolev-yao-star-src, hacl-packages-src}:
+  outputs = {self, nixpkgs, fstar-flake, comparse-flake, dolev-yao-star-flake, hacl-packages-src}:
   let
     system = "x86_64-linux";
     pkgs = import nixpkgs { inherit system; };
     z3 = fstar-flake.packages.${system}.z3;
     fstar = fstar-flake.packages.${system}.fstar;
     fstar-dune = fstar-flake.packages.${system}.fstar-dune;
     comparse = comparse-flake.packages.${system}.comparse;
-    # The following is a hack, because nix is not able to fetch a subdirectory of a git repository
-    # (there is the "?dir=..." syntax, but it works only to point to the flake.nix!)
-    # There are two repositories where we may obtain dolev-yao-star
-    # - from the private dolev-yao-star repository
-    # - from the artifact of the TreeSync paper, that contains a recent public version of DY* in the dolev-yao-star subdirectory
-    # Hence, this little condition will check whether there exists a "dolev-yao-star" subdirectory
-    # (which only happens when dolev-yao-star-src points to the TreeSync artifact),
-    # and go into it when that is the case.
-    dolev-yao-star =
-      if (builtins.readDir dolev-yao-star-src)?"dolev-yao-star" then
-        "${dolev-yao-star-src}/dolev-yao-star"
-      else
-        dolev-yao-star-src
-    ;
+    dolev-yao-star = dolev-yao-star-flake.packages.${system}.dolev-yao-star;
     mls-star = pkgs.callPackage ./default.nix {inherit fstar fstar-dune z3 comparse dolev-yao-star hacl-packages-src; ocamlPackages = pkgs.ocaml-ng.ocamlPackages_4_14;};
   in {
     packages.${system} = {

fstar/api/MLS.fst

@@ -37,16 +37,10 @@ let universal_sign_nonce =
 
 let group_id = bytes
 
-let asp: as_parameters bytes = {
-  token_t = unit;
-  credential_ok = (fun _ _ -> True);
-  valid_successor = (fun _ _ -> True);
-}
-
 noeq type state = {
   group_id:mls_bytes bytes;
   leaf_index: nat;
-  treesync_state: MLS.TreeSync.API.Types.treesync_state bytes tkt asp group_id;
+  treesync_state: MLS.TreeSync.API.Types.treesync_state bytes tkt unit group_id;
   treekem_state: treekem_state bytes leaf_index;
   treedem_state: treedem_state bytes;
   epoch: nat;