From 75d266aca85ff722281143fdb89b35815fd95c48 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= Date: Wed, 17 Jul 2024 19:37:01 +0200 Subject: [PATCH 1/2] cleanup: reduce boilerplate to merge local predicates --- .../DY.Example.DH.Protocol.Stateful.Proof.fst | 27 +++++-------------- .../DY.Example.DH.Protocol.Stateful.fst | 4 --- ...DY.Example.NSL.Protocol.Stateful.Proof.fst | 27 +++++-------------- .../DY.Example.NSL.Protocol.Stateful.fst | 5 +--- src/lib/event/DY.Lib.Event.Typed.fst | 1 + src/lib/state/DY.Lib.State.Map.fst | 5 ++-- src/lib/state/DY.Lib.State.PKI.fst | 3 ++- src/lib/state/DY.Lib.State.PrivateKeys.fst | 3 ++- src/lib/state/DY.Lib.State.Typed.fst | 1 + 9 files changed, 23 insertions(+), 53 deletions(-) diff --git a/examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst b/examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst index 2778bb4..54797d0 100644 --- a/examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst +++ b/examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst @@ -99,7 +99,8 @@ 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); + ("__dummy__", (fun _ _ _ -> False)) // workaround ] /// Create the global trace invariants. @@ -116,33 +117,19 @@ 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)) +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 () = +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) (*** Proofs ****) diff --git a/examples/iso_dh/DY.Example.DH.Protocol.Stateful.fst b/examples/iso_dh/DY.Example.DH.Protocol.Stateful.fst index 95f1c60..073745b 100644 --- a/examples/iso_dh/DY.Example.DH.Protocol.Stateful.fst +++ b/examples/iso_dh/DY.Example.DH.Protocol.Stateful.fst @@ -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 = @@ -146,4 +143,3 @@ let verify_msg3 global_sess_id alice bob msg_id bob_si = return (Some ()) ) | _ -> return None - \ No newline at end of file diff --git a/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst b/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst index f1ff45e..b9184fa 100644 --- a/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst +++ b/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst @@ -90,7 +90,8 @@ 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); + ("__dummy__", (fun _ _ _ -> False)) // workaround ] /// Create the global trace invariants. @@ -107,33 +108,19 @@ 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 () = +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) (*** Proofs ***) diff --git a/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.fst b/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.fst index 4a2403c..982e01f 100644 --- a/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.fst +++ b/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.fst @@ -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 ***) diff --git a/src/lib/event/DY.Lib.Event.Typed.fst b/src/lib/event/DY.Lib.Event.Typed.fst index 26635a2..4937aa1 100644 --- a/src/lib/event/DY.Lib.Event.Typed.fst +++ b/src/lib/event/DY.Lib.Event.Typed.fst @@ -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 diff --git a/src/lib/state/DY.Lib.State.Map.fst b/src/lib/state/DY.Lib.State.Map.fst index f050e9c..4b69bf9 100644 --- a/src/lib/state/DY.Lib.State.Map.fst +++ b/src/lib/state/DY.Lib.State.Map.fst @@ -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: @@ -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 diff --git a/src/lib/state/DY.Lib.State.PKI.fst b/src/lib/state/DY.Lib.State.PKI.fst index f28ec0c..7f9ccd7 100644 --- a/src/lib/state/DY.Lib.State.PKI.fst +++ b/src/lib/state/DY.Lib.State.PKI.fst @@ -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 ***) diff --git a/src/lib/state/DY.Lib.State.PrivateKeys.fst b/src/lib/state/DY.Lib.State.PrivateKeys.fst index 8424887..c6da073 100644 --- a/src/lib/state/DY.Lib.State.PrivateKeys.fst +++ b/src/lib/state/DY.Lib.State.PrivateKeys.fst @@ -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 -> diff --git a/src/lib/state/DY.Lib.State.Typed.fst b/src/lib/state/DY.Lib.State.Typed.fst index b14e4e1..dae34fa 100644 --- a/src/lib/state/DY.Lib.State.Typed.fst +++ b/src/lib/state/DY.Lib.State.Typed.fst @@ -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 -> From 19f951b5df1a52f9d34cbae32398bdbbf5b918dd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= Date: Thu, 18 Jul 2024 18:32:37 +0200 Subject: [PATCH 2/2] remove old workaround and add a cleaner one --- examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst | 3 ++- examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst | 3 ++- flake.lock | 6 +++--- 3 files changed, 7 insertions(+), 5 deletions(-) diff --git a/examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst b/examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst index 54797d0..28dff70 100644 --- a/examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst +++ b/examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst @@ -100,7 +100,6 @@ let all_sessions = [ let all_events = [ (dh_event_instance.tag, compile_event_pred dh_event_pred); - ("__dummy__", (fun _ _ _ -> False)) // workaround ] /// Create the global trace invariants. @@ -125,11 +124,13 @@ let all_sessions_has_all_sessions = /// Lemmas that the global event predicate contains all the local ones +#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) +#pop-options (*** Proofs ****) diff --git a/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst b/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst index b9184fa..de1a0ae 100644 --- a/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst +++ b/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst @@ -91,7 +91,6 @@ let all_sessions = [ let all_events = [ (event_nsl_event.tag, compile_event_pred event_predicate_nsl); - ("__dummy__", (fun _ _ _ -> False)) // workaround ] /// Create the global trace invariants. @@ -116,11 +115,13 @@ let all_sessions_has_all_sessions = /// Lemmas that the global event predicate contains all the local ones +#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) +#pop-options (*** Proofs ***) diff --git a/flake.lock b/flake.lock index 0c1d059..94901f9 100644 --- a/flake.lock +++ b/flake.lock @@ -46,11 +46,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1708956704, - "narHash": "sha256-xT0V7oQwR0Zns9g/MvV30ILlAX6tcp92SqWPwej1+sI=", + "lastModified": 1721275414, + "narHash": "sha256-WyV22bJ3W4CqThhawifTmC0jPn9MAaueLmLeM119dW8=", "owner": "FStarLang", "repo": "FStar", - "rev": "a48722f90e14be69b850f093b41fbbdfee7f6eb9", + "rev": "3ed3c98d39ce028c31c5908a38bc68ad5098f563", "type": "github" }, "original": {