Skip to content

Add missing includes and for_allP imports #20

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
qaphla merged 3 commits into from
Jun 13, 2025
Merged

Add missing includes and for_allP imports #20

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2dac662
Add missing includes and for_allP imports
schaafjs Jun 12, 2025
2e64b9b
Merge branch 'main' into main
TWal Jun 13, 2025
7fcd395
Update `flake.lock`
schaafjs Jun 13, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))

Expand All @@ -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

Expand Down
2 changes: 2 additions & 0 deletions examples/NSL_with_properties/DY.NSLP.Invariants.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
2 changes: 2 additions & 0 deletions examples/Online_with_authn/DY.OnlineA.Invariants.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 2 additions & 0 deletions examples/Online_with_secrecy/DY.OnlineS.Invariants.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
24 changes: 12 additions & 12 deletions flake.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.