Complain about ppcalls to lower (or equal) priorities

Signed-off-by: julia <[email protected]>

tool/microkit/src/main.rs

@@ -2348,6 +2348,7 @@ fn build_system(
     for cc in &system.channels {
         for (send, recv) in [(&cc.end_a, &cc.end_b), (&cc.end_b, &cc.end_a)] {
             let send_pd = &system.protection_domains[send.pd];
+            let recv_pd = &system.protection_domains[recv.pd];
             let send_cnode_obj = cnode_objs_by_pd[send_pd];
             let recv_notification_obj = &notification_objs[recv.pd];
 
@@ -2381,6 +2382,12 @@ fn build_system(
                 let recv_endpoint_obj =
                     pd_endpoint_objs[recv.pd].expect("endpoint object to exist");
 
+                assert!(
+                    send_pd.priority < recv_pd.priority,
+                    "ppcalls must be to a higher priority PD; you specified from pd {} (priority: {}) to pd {} (priority {})",
+                    send_pd.name, send_pd.priority, recv_pd.name, recv_pd.priority,
+                );
+
                 system_invocations.push(Invocation::new(
                     config,
                     InvocationArgs::CnodeMint {