From 7d7632e2ee5463b18fe7ede5e7c4d40dc41c86ac Mon Sep 17 00:00:00 2001 From: Aseem Rastogi Date: Fri, 24 May 2024 09:58:01 +0000 Subject: [PATCH] no need for a context handle if only single context is supported --- pulse2rust/dpe/src/generated/dpe.rs | 29 ++------- .../examples/dice/dpe/DPE.TestClient.fst | 29 ++++----- share/pulse/examples/dice/dpe/DPE.fst | 62 ++++++------------- share/pulse/examples/dice/dpe/DPE.fsti | 26 +++----- share/pulse/examples/dice/dpe/DPE_CBOR.fst | 20 +++--- 5 files changed, 54 insertions(+), 112 deletions(-) diff --git a/pulse2rust/dpe/src/generated/dpe.rs b/pulse2rust/dpe/src/generated/dpe.rs index 047b11059..6046cfcf4 100644 --- a/pulse2rust/dpe/src/generated/dpe.rs +++ b/pulse2rust/dpe/src/generated/dpe.rs @@ -4,11 +4,9 @@ //// //// -pub type ctxt_hndl_t = u32; pub type sid_t = u16; #[derive(Clone)] pub struct session_state__Available__payload { - pub handle: super::dpe::ctxt_hndl_t, pub context: super::dpetypes::context_t, } #[derive(Clone)] @@ -182,27 +180,21 @@ pub fn init_engine_ctxt( let ctxt = super::dpetypes::mk_context_t_engine(engine_context); ctxt } -pub fn prng(uu___: ()) -> super::dpe::ctxt_hndl_t { - 0 -} pub fn initialize_context( sid: super::dpe::sid_t, t: (), p: (), uds_bytes: (), uds: &mut [u8], -) -> super::dpe::ctxt_hndl_t { +) -> () { let s = super::dpe::replace_session(sid, (), super::dpe::session_state::InUse, ()); match s { super::dpe::session_state::SessionStart => { let context = super::dpe::init_engine_ctxt(uds, (), ()); - let handle = super::dpe::prng(()); let s1 = super::dpe::session_state::Available(super::dpe::session_state__Available__payload { - handle: handle, context: context, }); let s2 = super::dpe::replace_session(sid, (), s1, ()); - handle } super::dpe::session_state::InUse => panic!(), super::dpe::session_state::SessionClosed => panic!(), @@ -394,11 +386,10 @@ pub fn derive_child_from_context( } pub fn derive_child( sid: super::dpe::sid_t, - ctxt_hndl: super::dpe::ctxt_hndl_t, t: (), record: super::dpetypes::record_t, rrepr: (), -) -> std::option::Option { +) -> bool { let s = super::dpe::replace_session(sid, (), super::dpe::session_state::InUse, ()); match s { super::dpe::session_state::Available(mut hc) => { @@ -414,20 +405,16 @@ pub fn derive_child( ); match ret { Some(mut nctxt) => { - let handle = super::dpe::prng(()); let s1 = super::dpe::session_state::Available(super::dpe::session_state__Available__payload { - handle: handle, context: nctxt, }); let s2 = super::dpe::replace_session(sid, (), s1, ()); - let ret1 = Some(handle); - ret1 + true } None => { let s1 = super::dpe::session_state::SessionError; let s2 = super::dpe::replace_session(sid, (), s1, ()); - let ret1 = None; - ret1 + false } } } @@ -459,7 +446,6 @@ pub fn close_session(sid: super::dpe::sid_t, t: ()) -> () { } pub fn certify_key( sid: super::dpe::sid_t, - ctxt_hndl: super::dpe::ctxt_hndl_t, pub_key: &mut [u8], crt_len: u32, crt: &mut [u8], @@ -472,9 +458,7 @@ pub fn certify_key( super::dpetypes::context_t::L1_context(mut c) => { let c_crt_len = c.aliasKeyCRT_len; if crt_len < c_crt_len { - let handle = super::dpe::prng(()); let ns = super::dpe::session_state::Available(super::dpe::session_state__Available__payload { - handle: handle, context: super::dpetypes::context_t::L1_context(c), }); let s1 = super::dpe::replace_session(sid, (), ns, ()); @@ -496,9 +480,7 @@ pub fn certify_key( (), (), ); - let handle = super::dpe::prng(()); let ns = super::dpe::session_state::Available(super::dpe::session_state__Available__payload { - handle: handle, context: super::dpetypes::context_t::L1_context(c), }); let s1 = super::dpe::replace_session(sid, (), ns, ()); @@ -513,7 +495,6 @@ pub fn certify_key( } pub fn sign( sid: super::dpe::sid_t, - ctxt_hndl: super::dpe::ctxt_hndl_t, signature: &mut [u8], msg_len: usize, msg: &mut [u8], @@ -535,9 +516,7 @@ pub fn sign( (), (), ); - let handle = super::dpe::prng(()); let ns = super::dpe::session_state::Available(super::dpe::session_state__Available__payload { - handle: handle, context: super::dpetypes::context_t::L1_context(c), }); let s1 = super::dpe::replace_session(sid, (), ns, ()); diff --git a/share/pulse/examples/dice/dpe/DPE.TestClient.fst b/share/pulse/examples/dice/dpe/DPE.TestClient.fst index 1410e19a4..5bbdc4b7e 100644 --- a/share/pulse/examples/dice/dpe/DPE.TestClient.fst +++ b/share/pulse/examples/dice/dpe/DPE.TestClient.fst @@ -55,24 +55,21 @@ fn dpe_client () let uds = get_uds (); with uds_repr. assert (A.pts_to uds uds_repr); unfold (open_session_client_perm (Some sid)); - let h = initialize_context sid _ uds; + initialize_context sid _ uds; unfold (initialize_context_client_perm sid uds_repr); let r = get_engine_record (); with repr. assert (record_perm r 1.0R repr); with t. assert (sid_pts_to trace_ref sid t); - let hopt = derive_child sid h _ r; - match hopt { - Some h -> { - unfold (derive_child_client_perm sid t repr (Some h)); - let r = get_l0_record (); - let hopt = derive_child sid h _ r; - drop_ (A.pts_to uds uds_repr); - drop_ (derive_child_client_perm _ _ _ _); - } - None -> { - drop_ (A.pts_to uds uds_repr); - drop_ (derive_child_client_perm _ _ _ _) - } + let res = derive_child sid _ r; + if res { + unfold (derive_child_client_perm sid t repr true); + let r = get_l0_record (); + let hopt = derive_child sid _ r; + drop_ (A.pts_to uds uds_repr); + drop_ (derive_child_client_perm _ _ _ _); + } else { + drop_ (A.pts_to uds uds_repr); + drop_ (derive_child_client_perm _ _ _ _) } } None -> { @@ -94,10 +91,10 @@ fn dpe_client_err () let uds = get_uds (); with uds_repr. assert (A.pts_to uds uds_repr); unfold (open_session_client_perm (Some sid)); - let h = initialize_context sid _ uds; + initialize_context sid _ uds; unfold (initialize_context_client_perm sid uds_repr); let r = get_l0_record (); - let hopt = derive_child sid h _ r; + let hopt = derive_child sid _ r; admit () } None -> { diff --git a/share/pulse/examples/dice/dpe/DPE.fst b/share/pulse/examples/dice/dpe/DPE.fst index c9b44c5ee..9013992c5 100644 --- a/share/pulse/examples/dice/dpe/DPE.fst +++ b/share/pulse/examples/dice/dpe/DPE.fst @@ -621,19 +621,6 @@ fn init_engine_ctxt } ``` -// -// TODO: FIXME -// -```pulse -fn prng () - requires emp - returns _:ctxt_hndl_t - ensures emp -{ - 0ul -} -``` - let session_state_tag_related (s:session_state) (gs:g_session_state) : GTot bool = match s, gs with | SessionStart, G_SessionStart @@ -672,8 +659,6 @@ fn initialize_context (sid:sid_t) requires A.pts_to uds #p uds_bytes ** sid_pts_to trace_ref sid t - returns r:ctxt_hndl_t - ensures A.pts_to uds #p uds_bytes ** initialize_context_client_perm sid uds_bytes { @@ -685,15 +670,13 @@ fn initialize_context (sid:sid_t) SessionStart -> { rewrite (session_state_related s (current_state t)) as emp; let context = init_engine_ctxt uds; - let handle = prng (); - let s = Available { handle; context }; + let s = Available { context }; rewrite (context_perm context (Engine_context_repr uds_bytes)) as (session_state_related s (G_Available (Engine_context_repr uds_bytes))); let s = replace_session sid t1 s (G_Available (Engine_context_repr uds_bytes)); intro_session_state_tag_related s (current_state t1); with _x _y. rewrite (session_state_related _x _y) as emp; - fold (initialize_context_client_perm sid uds_bytes); - handle + fold (initialize_context_client_perm sid uds_bytes) } InUse -> { rewrite (session_state_related s (current_state t)) as @@ -1093,9 +1076,8 @@ fn derive_child_from_context ```pulse ghost fn rewrite_session_state_related_available - handle context - (s:session_state { s == Available { handle; context } }) + (s:session_state { s == Available { context } }) (t:trace) requires session_state_related s (current_state t) returns r:G.erased context_repr_t @@ -1112,13 +1094,13 @@ fn rewrite_session_state_related_available #push-options "--fuel 2 --ifuel 2 --split_queries no" ```pulse -fn derive_child (sid:sid_t) (ctxt_hndl:ctxt_hndl_t) +fn derive_child (sid:sid_t) (t:G.erased trace) (record:record_t) (#rrepr:erased repr_t { trace_and_record_valid_for_derive_child t rrepr }) requires record_perm record 1.0R rrepr ** sid_pts_to trace_ref sid t - returns b:(option ctxt_hndl_t) + returns b:bool ensures derive_child_client_perm sid t rrepr b { intro_record_and_repr_tag_related record 1.0R rrepr; @@ -1137,7 +1119,7 @@ fn derive_child (sid:sid_t) (ctxt_hndl:ctxt_hndl_t) } _ -> { assume_ (pure (~ (L1_context? hc.context))); - let repr = rewrite_session_state_related_available hc.handle hc.context s t; + let repr = rewrite_session_state_related_available hc.context s t; intro_context_and_repr_tag_related hc.context repr; let ret = derive_child_from_context hc.context record #rrepr #repr (); @@ -1146,16 +1128,14 @@ fn derive_child (sid:sid_t) (ctxt_hndl:ctxt_hndl_t) unfold (maybe_context_perm repr rrepr (Some nctxt)); with nrepr. assert (context_perm nctxt nrepr); intro_context_and_repr_tag_related nctxt nrepr; - let handle = prng (); - let s = Available { handle; context = nctxt }; + let s = Available { context = nctxt }; rewrite (context_perm nctxt nrepr) as (session_state_related s (G_Available nrepr)); let s = replace_session sid t1 s (G_Available nrepr); intro_session_state_tag_related s (current_state t1); - let ret = Some handle; - fold (derive_child_client_perm sid t rrepr (Some handle)); + fold (derive_child_client_perm sid t rrepr true); with _x _y. rewrite (session_state_related _x _y) as emp; - ret + true } None -> { let s = SessionError; @@ -1163,10 +1143,9 @@ fn derive_child (sid:sid_t) (ctxt_hndl:ctxt_hndl_t) rewrite emp as (session_state_related s (G_SessionError (current_state t1))); let s = replace_session sid t1 s (G_SessionError (current_state t1)); intro_session_state_tag_related s (current_state t1); - let ret = None #ctxt_hndl_t; - fold (derive_child_client_perm sid t rrepr None); + fold (derive_child_client_perm sid t rrepr false); with _x _y. rewrite (session_state_related _x _y) as emp; - ret + false } } } @@ -1204,7 +1183,7 @@ fn destroy_session_state (s:session_state) (t:G.erased trace) intro_session_state_tag_related s (current_state t); match s { Available hc -> { - rewrite_session_state_related_available hc.handle hc.context s t; + rewrite_session_state_related_available hc.context s t; destroy_ctxt hc.context } _ -> { @@ -1239,7 +1218,7 @@ fn close_session (sid:sid_t) #push-options "--z3rlimit_factor 4 --fuel 2 --ifuel 1 --split_queries no" ```pulse -fn certify_key (sid:sid_t) (ctxt_hndl:ctxt_hndl_t) +fn certify_key (sid:sid_t) (pub_key:A.larray U8.t 32) (crt_len:U32.t) (crt:A.larray U8.t (U32.v crt_len)) @@ -1264,8 +1243,7 @@ fn certify_key (sid:sid_t) (ctxt_hndl:ctxt_hndl_t) L1_context c -> { let c_crt_len = c.aliasKeyCRT_len; if U32.lt crt_len c_crt_len { - let handle = prng (); - let ns = Available { handle; context = L1_context c }; + let ns = Available { context = L1_context c }; rewrite (session_state_related s (current_state t)) as (session_state_related ns (current_state t)); let s = replace_session sid t1 ns (current_state t); @@ -1274,7 +1252,7 @@ fn certify_key (sid:sid_t) (ctxt_hndl:ctxt_hndl_t) fold (certify_key_client_perm sid t); 0ul } else { - let r = rewrite_session_state_related_available hc.handle (L1_context c) s t; + let r = rewrite_session_state_related_available (L1_context c) s t; let r = rewrite_context_perm_l1 (L1_context c) c; unfold (l1_context_perm c r); @@ -1292,8 +1270,7 @@ fn certify_key (sid:sid_t) (ctxt_hndl:ctxt_hndl_t) rewrite (l1_context_perm c r) as (context_perm (L1_context c) (L1_context_repr r)); - let handle = prng (); - let ns = Available { handle; context = L1_context c }; + let ns = Available { context = L1_context c }; rewrite (context_perm (L1_context c) (L1_context_repr r)) as (session_state_related ns (current_state t)); @@ -1325,7 +1302,7 @@ fn certify_key (sid:sid_t) (ctxt_hndl:ctxt_hndl_t) #push-options "--split_queries no" ```pulse -fn sign (sid:sid_t) (ctxt_hndl:ctxt_hndl_t) +fn sign (sid:sid_t) (signature:A.larray U8.t 64) (msg_len:SZ.t { SZ.v msg_len < pow2 32 }) (msg:A.larray U8.t (SZ.v msg_len)) @@ -1347,7 +1324,7 @@ fn sign (sid:sid_t) (ctxt_hndl:ctxt_hndl_t) Available hc -> { match hc.context { L1_context c -> { - let r = rewrite_session_state_related_available hc.handle (L1_context c) s t; + let r = rewrite_session_state_related_available (L1_context c) s t; let r = rewrite_context_perm_l1 (L1_context c) c; unfold (l1_context_perm c r); @@ -1359,8 +1336,7 @@ fn sign (sid:sid_t) (ctxt_hndl:ctxt_hndl_t) rewrite (l1_context_perm c r) as (context_perm (L1_context c) (L1_context_repr r)); - let handle = prng (); - let ns = Available { handle; context = L1_context c }; + let ns = Available { context = L1_context c }; rewrite (context_perm (L1_context c) (L1_context_repr r)) as (session_state_related ns (current_state t)); diff --git a/share/pulse/examples/dice/dpe/DPE.fsti b/share/pulse/examples/dice/dpe/DPE.fsti index b669c0c30..945830195 100644 --- a/share/pulse/examples/dice/dpe/DPE.fsti +++ b/share/pulse/examples/dice/dpe/DPE.fsti @@ -39,12 +39,6 @@ open Pulse.Lib.OnRange open Pulse.Lib.HashTable.Type open Pulse.Lib.HashTable -// -// Concrete state setup -// - -type ctxt_hndl_t = U32.t - type sid_t : eqtype = U16.t // @@ -56,7 +50,7 @@ type sid_t : eqtype = U16.t noeq type session_state = | SessionStart - | Available { handle:ctxt_hndl_t; context:context_t } + | Available { context:context_t } | InUse | SessionClosed | SessionError @@ -388,7 +382,7 @@ val initialize_context (sid:sid_t) (t:G.erased trace { trace_valid_for_initialize_context t }) (#p:perm) (#uds_bytes:Ghost.erased (Seq.seq U8.t)) (uds:A.larray U8.t (SZ.v uds_len)) - : stt ctxt_hndl_t + : stt unit (requires A.pts_to uds #p uds_bytes ** sid_pts_to trace_ref sid t) @@ -410,21 +404,21 @@ let derive_child_post_trace (r:repr_t) (t:trace) = | L0_repr r, G_Available (L1_context_repr lrepr) -> lrepr.repr == r | _ -> False -let derive_child_client_perm (sid:sid_t) (t0:trace) (repr:repr_t) (c:option ctxt_hndl_t) +let derive_child_client_perm (sid:sid_t) (t0:trace) (repr:repr_t) (res:bool) : vprop = - match c with - | None -> + match res with + | false -> exists* t1. sid_pts_to trace_ref sid t1 ** pure (current_state t1 == G_SessionError (G_InUse (current_state t0))) - | Some _ -> + | true -> exists* t1. sid_pts_to trace_ref sid t1 ** pure (derive_child_post_trace repr t1) -val derive_child (sid:sid_t) (ctxt_hndl:ctxt_hndl_t) +val derive_child (sid:sid_t) (t:G.erased trace) (record:record_t) (#rrepr:erased repr_t { trace_and_record_valid_for_derive_child t rrepr }) - : stt (option ctxt_hndl_t) + : stt bool (requires record_perm record 1.0R rrepr ** sid_pts_to trace_ref sid t) @@ -462,7 +456,7 @@ let certify_key_client_perm (sid:sid_t) (t0:trace) : vprop = exists* t1. sid_pts_to trace_ref sid t1 ** pure (current_state t1 == current_state t0) -val certify_key (sid:sid_t) (ctxt_hndl:ctxt_hndl_t) +val certify_key (sid:sid_t) (pub_key:A.larray U8.t 32) (crt_len:U32.t) (crt:A.larray U8.t (U32.v crt_len)) @@ -489,7 +483,7 @@ let sign_client_perm (sid:sid_t) (t0:trace) : vprop = exists* t1. sid_pts_to trace_ref sid t1 ** pure (current_state t1 == current_state t0) -val sign (sid:sid_t) (ctxt_hndl:ctxt_hndl_t) +val sign (sid:sid_t) (signature:A.larray U8.t 64) (msg_len:SZ.t { SZ.v msg_len < pow2 32 }) (msg:A.larray U8.t (SZ.v msg_len)) diff --git a/share/pulse/examples/dice/dpe/DPE_CBOR.fst b/share/pulse/examples/dice/dpe/DPE_CBOR.fst index a05e14e9d..6aa308869 100644 --- a/share/pulse/examples/dice/dpe/DPE_CBOR.fst +++ b/share/pulse/examples/dice/dpe/DPE_CBOR.fst @@ -65,14 +65,14 @@ fn finish (c:cbor_read_t) raw_data_item_match 1.0R c.cbor_read_payload v ** A.pts_to c.cbor_read_remainder #p rem ** 'uds_is_enabled - returns _:option ctxt_hndl_t + returns _:bool ensures A.pts_to input #p s { elim_implies () #(raw_data_item_match 1.0R c.cbor_read_payload v ** A.pts_to c.cbor_read_remainder #p rem) #(A.pts_to input #p s); drop 'uds_is_enabled; - None #ctxt_hndl_t + false } ``` @@ -86,7 +86,7 @@ fn initialize_context (len:SZ.t) (#p:perm) requires A.pts_to input #p s - returns r:(option ctxt_hndl_t) + returns r:bool ensures A.pts_to input #p s { @@ -96,8 +96,7 @@ fn initialize_context (len:SZ.t) None -> { unfold (parse_dpe_cmd_post len input s p None); - let ret = None #ctxt_hndl_t; - ret + false } Some cmd -> { @@ -105,8 +104,7 @@ fn initialize_context (len:SZ.t) if (cmd.dpe_cmd_sid `FStar.UInt64.gte` 4294967296uL) { // FIXME: DPE.sid == U16.t, but the CDDL specification for DPE session messages does not specify any bound on sid (if so, I could have used a CDDL combinator and avoided this additional test here) elim_stick0 (); - let ret = None #ctxt_hndl_t; - ret + false } else { let sid : FStar.UInt16.t = Cast.uint64_to_uint16 cmd.dpe_cmd_sid; with vargs . assert (raw_data_item_match 1.0R cmd.dpe_cmd_args vargs); @@ -120,8 +118,7 @@ fn initialize_context (len:SZ.t) { unfold (cbor_map_get_with_typ_post (Cddl.str_size cbor_major_type_byte_string (SZ.v EngineTypes.uds_len)) 1.0R (Ghost.reveal vkey) vargs cmd.dpe_cmd_args NotFound); // same here; also WHY WHY WHY the explicit Ghost.reveal elim_stick0 (); - let ret = None #ctxt_hndl_t; - ret + false } Found uds_cbor -> { @@ -131,13 +128,12 @@ fn initialize_context (len:SZ.t) assume_ (exists* t. DPE.sid_pts_to DPE.trace_ref sid t ** pure (DPE.trace_valid_for_initialize_context t)); with t. assert (DPE.sid_pts_to DPE.trace_ref sid t); - let h = DPE.initialize_context sid t uds.cbor_string_payload; + DPE.initialize_context sid t uds.cbor_string_payload; elim_stick0 (); elim_stick0 (); elim_stick0 (); - let ret = Some h; drop_ (initialize_context_client_perm sid _); - ret + true } } }