Skip to content
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

Jump to bottom

cleanup: reduce boilerplate to merge local predicates #40

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

cleanup: reduce boilerplate to merge local predicates #40

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
75d266a
cleanup: reduce boilerplate to merge local predicates
TWal Jul 17, 2024
19f951b
remove old workaround and add a cleaner one
TWal Jul 18, 2024
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
28 changes: 8 additions & 20 deletions examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ let all_sessions = [
/// List of all local event predicates.

let all_events = [
(dh_event_instance.tag, compile_event_pred dh_event_pred)
(dh_event_instance.tag, compile_event_pred dh_event_pred);
]

/// Create the global trace invariants.
Expand All @@ -116,33 +116,21 @@ instance dh_protocol_invs: protocol_invariants = {

/// Lemmas that the global state predicate contains all the local ones

val all_sessions_has_all_sessions: unit -> Lemma (norm [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate dh_protocol_invs) all_sessions))
let all_sessions_has_all_sessions () =
val all_sessions_has_all_sessions: squash (norm [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate dh_protocol_invs) all_sessions))
fabian-hk marked this conversation as resolved.
Show resolved Hide resolved
let all_sessions_has_all_sessions =
assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_sessions)));
mk_global_local_bytes_state_predicate_correct dh_protocol_invs all_sessions;
norm_spec [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate dh_protocol_invs) all_sessions)

val full_dh_session_pred_has_pki_invariant: squash (has_pki_invariant dh_protocol_invs)
let full_dh_session_pred_has_pki_invariant = all_sessions_has_all_sessions ()

val full_dh_session_pred_has_private_keys_invariant: squash (has_private_keys_invariant dh_protocol_invs)
let full_dh_session_pred_has_private_keys_invariant = all_sessions_has_all_sessions ()

val full_dh_session_pred_has_dh_invariant: squash (has_local_state_predicate dh_protocol_invs dh_session_pred)
let full_dh_session_pred_has_dh_invariant = all_sessions_has_all_sessions ()

/// Lemmas that the global event predicate contains all the local ones

val all_events_has_all_events: unit -> Lemma (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred dh_protocol_invs) all_events))
let all_events_has_all_events () =
#push-options "--fuel 1" // fuel is a workaround for FStarLang/FStar#3360
val all_events_has_all_events: squash (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred dh_protocol_invs) all_events))
let all_events_has_all_events =
assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_events)));
mk_event_pred_correct dh_protocol_invs all_events;
norm_spec [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred dh_protocol_invs) all_events);
let dumb_lemma (x:prop) (y:prop): Lemma (requires x /\ x == y) (ensures y) = () in
dumb_lemma (for_allP (has_compiled_event_pred dh_protocol_invs) all_events) (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred dh_protocol_invs) all_events))

val full_dh_event_pred_has_dh_invariant: squash (has_event_pred dh_protocol_invs dh_event_pred)
let full_dh_event_pred_has_dh_invariant = all_events_has_all_events ()
norm_spec [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred dh_protocol_invs) all_events)
#pop-options

(*** Proofs ****)

Expand Down
4 changes: 0 additions & 4 deletions examples/iso_dh/DY.Example.DH.Protocol.Stateful.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,9 +17,6 @@ type dh_session =
%splice [ps_dh_session] (gen_parser (`dh_session))
%splice [ps_dh_session_is_well_formed] (gen_is_well_formed_lemma (`dh_session))

instance dh_session_parseable_serializeable: parseable_serializeable bytes dh_session
= mk_parseable_serializeable ps_dh_session

(*** Definition of events ***)
[@@ with_bytes bytes]
type dh_event =
Expand Down Expand Up @@ -146,4 +143,3 @@ let verify_msg3 global_sess_id alice bob msg_id bob_si =
return (Some ())
)
| _ -> return None

28 changes: 8 additions & 20 deletions examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ let all_sessions = [
/// List of all local event predicates.

let all_events = [
(event_nsl_event.tag, compile_event_pred event_predicate_nsl)
(event_nsl_event.tag, compile_event_pred event_predicate_nsl);
]

/// Create the global trace invariants.
Expand All @@ -107,33 +107,21 @@ instance protocol_invariants_nsl: protocol_invariants = {

/// Lemmas that the global state predicate contains all the local ones

val all_sessions_has_all_sessions: unit -> Lemma (norm [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate protocol_invariants_nsl) all_sessions))
let all_sessions_has_all_sessions () =
val all_sessions_has_all_sessions: squash (norm [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate protocol_invariants_nsl) all_sessions))
let all_sessions_has_all_sessions =
assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_sessions)));
mk_global_local_bytes_state_predicate_correct protocol_invariants_nsl all_sessions;
norm_spec [delta_only [`%all_sessions; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate protocol_invariants_nsl) all_sessions)

val protocol_invariants_nsl_has_pki_invariant: squash (has_pki_invariant protocol_invariants_nsl)
let protocol_invariants_nsl_has_pki_invariant = all_sessions_has_all_sessions ()

val protocol_invariants_nsl_has_private_keys_invariant: squash (has_private_keys_invariant protocol_invariants_nsl)
let protocol_invariants_nsl_has_private_keys_invariant = all_sessions_has_all_sessions ()

val protocol_invariants_nsl_has_nsl_session_invariant: squash (has_local_state_predicate protocol_invariants_nsl state_predicate_nsl)
let protocol_invariants_nsl_has_nsl_session_invariant = all_sessions_has_all_sessions ()

/// Lemmas that the global event predicate contains all the local ones

val all_events_has_all_events: unit -> Lemma (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred protocol_invariants_nsl) all_events))
let all_events_has_all_events () =
#push-options "--fuel 1" // fuel is a workaround for FStarLang/FStar#3360
val all_events_has_all_events: squash (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred protocol_invariants_nsl) all_events))
let all_events_has_all_events =
assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_events)));
mk_event_pred_correct protocol_invariants_nsl all_events;
norm_spec [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred protocol_invariants_nsl) all_events);
let dumb_lemma (x:prop) (y:prop): Lemma (requires x /\ x == y) (ensures y) = () in
dumb_lemma (for_allP (has_compiled_event_pred protocol_invariants_nsl) all_events) (norm [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred protocol_invariants_nsl) all_events))

val protocol_invariants_nsl_has_nsl_event_invariant: squash (has_event_pred protocol_invariants_nsl event_predicate_nsl)
let protocol_invariants_nsl_has_nsl_event_invariant = all_events_has_all_events ()
norm_spec [delta_only [`%all_events; `%for_allP]; iota; zeta] (for_allP (has_compiled_event_pred protocol_invariants_nsl) all_events)
#pop-options

(*** Proofs ***)

Expand Down
5 changes: 1 addition & 4 deletions examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,12 +23,9 @@ type nsl_session =
%splice [ps_nsl_session] (gen_parser (`nsl_session))
%splice [ps_nsl_session_is_well_formed] (gen_is_well_formed_lemma (`nsl_session))

instance parseable_serializeable_bytes_nsl_session: parseable_serializeable bytes nsl_session
= mk_parseable_serializeable ps_nsl_session

instance local_state_nsl_session: local_state nsl_session = {
tag = "NSL.Session";
format = parseable_serializeable_bytes_nsl_session;
format = mk_parseable_serializeable ps_nsl_session;
}

(*** Event type ***)
Expand Down
6 changes: 3 additions & 3 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.

1 change: 1 addition & 0 deletions src/lib/event/DY.Lib.Event.Typed.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,7 @@ val has_compiled_event_pred:
let has_compiled_event_pred invs (tag, epred) =
has_local_pred split_event_pred_func event_pred (tag, epred)

unfold
val has_event_pred:
#a:Type0 -> {|event a|} ->
protocol_invariants -> event_predicate a -> prop
Expand Down
5 changes: 2 additions & 3 deletions src/lib/state/DY.Lib.State.Map.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,11 +56,9 @@ noeq type map (key_t:eqtype) (value_t:Type0) {|mt:map_types key_t value_t|} = {
%splice [ps_map] (gen_parser (`map))
%splice [ps_map_is_well_formed] (gen_is_well_formed_lemma (`map))

instance parseable_serializeable_bytes_map (key_t:eqtype) (value_t:Type0) {|map_types key_t value_t|} : parseable_serializeable bytes (map key_t value_t) = mk_parseable_serializeable (ps_map key_t value_t)

instance local_state_map (key_t:eqtype) (value_t:Type0) {|mt:map_types key_t value_t|}: local_state (map key_t value_t) = {
tag = mt.tag;
format = (parseable_serializeable_bytes_map key_t value_t);
format = mk_parseable_serializeable (ps_map key_t value_t);
}

val map_elem_invariant:
Expand Down Expand Up @@ -116,6 +114,7 @@ let map_session_invariant #cinvs #key_t #value_t #mt mpred = {
);
}

unfold
val has_map_session_invariant:
#key_t:eqtype -> #value_t:Type0 -> {|map_types key_t value_t|} ->
protocol_invariants -> map_predicate key_t value_t -> prop
Expand Down
3 changes: 2 additions & 1 deletion src/lib/state/DY.Lib.State.PKI.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,12 +76,13 @@ let pki_pred #cinvs = {
pred_knowable = (fun tr prin sess_id key value -> ());
}

unfold
val has_pki_invariant: protocol_invariants -> prop
let has_pki_invariant invs =
has_map_session_invariant invs pki_pred

val pki_tag_and_invariant: {|crypto_invariants|} -> string & local_bytes_state_predicate
let pki_tag_and_invariant #ci = (map_types_pki.tag, local_state_predicate_to_local_bytes_state_predicate (map_session_invariant pki_pred))
let pki_tag_and_invariant #ci = ((local_state_map pki_key pki_value #map_types_pki).tag, local_state_predicate_to_local_bytes_state_predicate (map_session_invariant pki_pred))

(*** PKI API ***)

Expand Down
3 changes: 2 additions & 1 deletion src/lib/state/DY.Lib.State.PrivateKeys.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,12 +68,13 @@ let private_keys_pred #cinvs = {
pred_knowable = (fun tr prin sess_id key value -> ());
}

unfold
val has_private_keys_invariant: protocol_invariants -> prop
let has_private_keys_invariant invs =
has_map_session_invariant invs private_keys_pred

val private_keys_tag_and_invariant: {|crypto_invariants|} -> string & local_bytes_state_predicate
let private_keys_tag_and_invariant #ci = (map_types_private_keys.tag, local_state_predicate_to_local_bytes_state_predicate (map_session_invariant private_keys_pred))
let private_keys_tag_and_invariant #ci = ((local_state_map private_key_key private_key_value #map_types_private_keys).tag, local_state_predicate_to_local_bytes_state_predicate (map_session_invariant private_keys_pred))

val private_key_type_to_usage:
private_key_type ->
Expand Down
1 change: 1 addition & 0 deletions src/lib/state/DY.Lib.State.Typed.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,7 @@ let local_state_predicate_to_local_bytes_state_predicate #cinvs #a #ps_a tspred
);
}

unfold
val has_local_state_predicate:
#a:Type -> {|local_state a|} ->
invs:protocol_invariants -> local_state_predicate a ->
Expand Down