Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR is the first step towards #43.
It only focus on the following options for now:
max_session_ttl
recording_mode
source_ip
The idea is to gather feedback on the general approach implemented here before implementing the remaining options.
From option inequalities to a simple struct
Before this PR, options were specified using inequalities. Instead now we have:
With predictable option combining (#43) there's no need to say
max_session_ttl < 10h
to try to imply that themin
will be chosen in case two of these are combined.Combining two of these inequalities using logical
AND
also doesn't seem to make sense.If we say
max_session_ttl < 10 AND max_session_ttl < 3
, this is equivalent tomax_session_ttl < 3
When Z3 solves this (see the solver proposed in #27) it will output
max_session_ttl == 0
as that's a valid solution.In general, saying
max_session_ttl < 3
could be interpreted as "max_session_ttl
can have any value smaller than 3", but this is not exactly what we want it to mean.Option combining
Option combining is implemented outside of Z3 as it's very easy to do so (e.g. just call
min
).export
outputAs options are not defined using inequalities, the
export
command now outputs them as a list.predicate export examples/access.py
outputs the following:Other changes
While working on this I made some general improvements:
examples
folder and doesn't contain outdated informationpoetry update
which updatedpoetry.lock
TeleportSolverResult
that encapsulates the outcomes of the solverLtDuration
as it's no longer neededbuild_predicate