From 2dac662b3feab2577ef1973e82a3af8995b28c63 Mon Sep 17 00:00:00 2001 From: Julius Schaaf Date: Thu, 12 Jun 2025 17:00:18 +0200 Subject: [PATCH 1/2] Add missing includes and for_allP imports --- Makefile | 4 ++-- examples/NSL_with_properties/DY.NSLP.Invariants.fst | 2 ++ examples/Online_with_authn/DY.OnlineA.Invariants.fst | 2 ++ examples/Online_with_secrecy/DY.OnlineS.Invariants.fst | 2 ++ 4 files changed, 8 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index e7d8c26..6aee5cb 100644 --- a/Makefile +++ b/Makefile @@ -12,7 +12,7 @@ INNER_EXAMPLE_DIRS = NSL NSL_with_properties TwoMessageP Online Online_with_secr EXAMPLE_DIRS ?= $(addprefix $(TUTORIAL_HOME)/examples/, $(INNER_EXAMPLE_DIRS)) -DY_INCLUDE_DIRS = core lib lib/comparse lib/crypto lib/event lib/hpke lib/state lib/utils +DY_INCLUDE_DIRS = core lib lib/comparse lib/crypto lib/event lib/hpke lib/state lib/utils lib/label lib/communication INCLUDE_DIRS = $(SOURCE_DIRS) $(EXAMPLE_DIRS) $(COMPARSE_HOME)/src $(addprefix $(DY_HOME)/src/, $(DY_INCLUDE_DIRS)) FSTAR_INCLUDE_DIRS = $(addprefix --include , $(INCLUDE_DIRS)) @@ -26,7 +26,7 @@ FSTAR_EXTRACT = --extract '-* +DY +Comparse' # 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 -# - (Warning 335) Interface ... is admitted without an implementation +# - (Warning 335) Interface ... is admitted without an implementation FSTAR_FLAGS = $(FSTAR_INCLUDE_DIRS) --cache_checked_modules --already_cached '+Prims +FStar' --warn_error '@0..1000' --warn_error '+242-335' --record_hints --hint_dir $(TUTORIAL_HOME)/hints --cache_dir $(TUTORIAL_HOME)/cache --odir $(TUTORIAL_HOME)/obj --cmi diff --git a/examples/NSL_with_properties/DY.NSLP.Invariants.fst b/examples/NSL_with_properties/DY.NSLP.Invariants.fst index 92dd56f..8835882 100644 --- a/examples/NSL_with_properties/DY.NSLP.Invariants.fst +++ b/examples/NSL_with_properties/DY.NSLP.Invariants.fst @@ -8,6 +8,8 @@ open DY.Extend open DY.NSLP.Data open DY.NSLP.Protocol +open FStar.List.Tot.Base + #set-options "--fuel 0 --ifuel 1 --z3rlimit 25 --z3cliopt 'smt.qi.eager_threshold=100'" /// This module defines the protocol invariants, diff --git a/examples/Online_with_authn/DY.OnlineA.Invariants.fst b/examples/Online_with_authn/DY.OnlineA.Invariants.fst index 9ac5abb..564e2b8 100644 --- a/examples/Online_with_authn/DY.OnlineA.Invariants.fst +++ b/examples/Online_with_authn/DY.OnlineA.Invariants.fst @@ -8,6 +8,8 @@ open DY.Extend open DY.OnlineA.Data open DY.OnlineA.Protocol +open FStar.List.Tot.Base + #set-options "--fuel 0 --ifuel 1 --z3rlimit 25" /// In this module, we define the protocol invariants. diff --git a/examples/Online_with_secrecy/DY.OnlineS.Invariants.fst b/examples/Online_with_secrecy/DY.OnlineS.Invariants.fst index 8e7948d..19fef7e 100644 --- a/examples/Online_with_secrecy/DY.OnlineS.Invariants.fst +++ b/examples/Online_with_secrecy/DY.OnlineS.Invariants.fst @@ -7,6 +7,8 @@ open DY.Lib open DY.OnlineS.Data open DY.OnlineS.Protocol +open FStar.List.Tot.Base + #set-options "--fuel 0 --ifuel 1 --z3rlimit 25" /// In this module, we define the protocol invariants. From 7fcd3958aa2f98c1f0fa63694cc744c84e26d794 Mon Sep 17 00:00:00 2001 From: Julius Schaaf Date: Fri, 13 Jun 2025 10:37:34 +0200 Subject: [PATCH 2/2] Update `flake.lock` --- flake.lock | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/flake.lock b/flake.lock index 0e547e3..5c66b6f 100644 --- a/flake.lock +++ b/flake.lock @@ -12,11 +12,11 @@ ] }, "locked": { - "lastModified": 1736420028, - "narHash": "sha256-AdRcHI1fdS+nHd1KhkyVkGOmMsmYtp+AXHcJqnjeyl4=", + "lastModified": 1748215731, + "narHash": "sha256-msAys4omyJm5tdxdeyfx/BQTh68rF4SwUzqGZ91CUos=", "owner": "TWal", "repo": "comparse", - "rev": "bedffbc4239353f825070e5b392a8c91e933bc0a", + "rev": "411b0219ce4d360d60c4f72ebd855fc13f785772", "type": "github" }, "original": { @@ -36,11 +36,11 @@ ] }, "locked": { - "lastModified": 1737638596, - "narHash": "sha256-ASro+BBg2vA37dsOOWSJG55R0QNaXeWjQ0H/Q7BeyZ8=", + "lastModified": 1748944308, + "narHash": "sha256-qBl9/A+dvg86ypXBKoIH9udn7XYnw1/HK1C8H3iOzys=", "owner": "REPROSEC", "repo": "dolev-yao-star-extrinsic", - "rev": "b9e4fdfbda6c7a402b52196a94fb9c0fb7be8a65", + "rev": "cdca1dd28230fd391c5dfe9759801f9e41eab872", "type": "github" }, "original": { @@ -72,11 +72,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1736396396, - "narHash": "sha256-jiE6ra1CkiELsce5c2lSSIetnph07dVrT7IS3sz0zh4=", + "lastModified": 1748199801, + "narHash": "sha256-clP79o0NsSjoNi59GxHxfN8lfc+5BPQyWnriYceyoHg=", "owner": "FStarLang", "repo": "FStar", - "rev": "c72e8b799b4da09cda5b901c7ff1746511853db8", + "rev": "ff868e03ee0d16303c514ae396706ba283b328a3", "type": "github" }, "original": { @@ -87,11 +87,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1693158576, - "narHash": "sha256-aRTTXkYvhXosGx535iAFUaoFboUrZSYb1Ooih/auGp0=", + "lastModified": 1743588408, + "narHash": "sha256-WRZyK13yucGjwNBMOGjU8ljRJ8FYFv8MBru/bXqZUn0=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "a999c1cc0c9eb2095729d5aa03e0d8f7ed256780", + "rev": "88efe689298b1863db0310c0a22b3ebb4d04fbc3", "type": "github" }, "original": {