@@ -2985,13 +2985,21 @@ mod prop_test_policy_set_operations {
29852985
29862986 /// Production PolicySet along with simplified model of policy set
29872987 /// for Proptesting
2988+ ///
2989+ /// We model the PolicySet state machine as lists of static policies, links and templates.
2990+ /// In the real policy set, a static policy will be a in both `ast.links` and `ast.templates`
2991+ /// (with the same `PolicyId`). Links and templates will be in `ast.links` and `ast.templates`
2992+ /// respectively.
2993+ ///
2994+ /// In the model, no name should occur in multiple lists or in the same list multiple times.
2995+ /// Every links should have a templates and a template should store a (possibly empty) list of it's links.
29882996 struct PolicySetModel {
29892997 //The production PolicySet implementation
29902998 policy_set : PolicySet ,
29912999
2992- //We model the PolicySet state machine in terms of the below:
3000+ // The model
3001+ static_policy_names : Vec < String > ,
29933002 link_names : Vec < String > ,
2994-
29953003 template_names : Vec < String > ,
29963004
29973005 //Every existent template has a (possibly empty) vector of the links to that template
@@ -3007,27 +3015,34 @@ mod prop_test_policy_set_operations {
30073015 fn new ( ) -> Self {
30083016 Self {
30093017 policy_set : PolicySet :: new ( ) ,
3018+ static_policy_names : Vec :: new ( ) ,
30103019 link_names : Vec :: new ( ) ,
30113020 template_names : Vec :: new ( ) ,
30123021 template_to_link_map : HashMap :: new ( ) ,
30133022 link_to_template_map : HashMap :: new ( ) ,
30143023 }
30153024 }
30163025
3026+ fn assert_name_unique ( & self , policy_id : & String ) {
3027+ assert ! ( !self . static_policy_names. iter( ) . any( |p| p == policy_id) ) ;
3028+ assert ! ( !self . link_names. iter( ) . any( |p| p == policy_id) ) ;
3029+ assert ! ( !self . template_names. iter( ) . any( |p| p == policy_id) ) ;
3030+ }
3031+
30173032 fn add_static ( & mut self , policy_name : String ) {
30183033 let policy_str = "permit(principal, action, resource);" ;
30193034 let p = Policy :: parse ( Some ( policy_name. clone ( ) ) , policy_str) . unwrap ( ) ;
30203035 if self . policy_set . add ( p) . is_ok ( ) {
3021- println ! ( "Add_static { policy_name}" ) ;
3022- self . link_names . push ( policy_name) ;
3036+ self . assert_name_unique ( & policy_name) ;
3037+ self . static_policy_names . push ( policy_name) ;
30233038 }
30243039 }
30253040
30263041 fn add_template ( & mut self , template_name : String ) {
30273042 let template_str = "permit(principal == ?principal, action, resource);" ;
30283043 let template = Template :: parse ( Some ( template_name. clone ( ) ) , template_str) . unwrap ( ) ;
30293044 if self . policy_set . add_template ( template) . is_ok ( ) {
3030- println ! ( "Add_template { template_name}" ) ;
3045+ self . assert_name_unique ( & template_name) ;
30313046 self . template_names . push ( template_name. clone ( ) ) ;
30323047 self . template_to_link_map . insert ( template_name, Vec :: new ( ) ) ;
30333048 }
@@ -3047,7 +3062,7 @@ mod prop_test_policy_set_operations {
30473062 )
30483063 . is_ok ( )
30493064 {
3050- println ! ( "Link { policy_name}" ) ;
3065+ self . assert_name_unique ( & policy_name) ;
30513066 self . link_names . push ( policy_name. clone ( ) ) ;
30523067 match self . template_to_link_map . entry ( template_name. clone ( ) ) {
30533068 Entry :: Occupied ( v) => v. into_mut ( ) . push ( policy_name. clone ( ) ) ,
@@ -3078,7 +3093,7 @@ mod prop_test_policy_set_operations {
30783093 . is_ok ( )
30793094 {
30803095 println ! ( "Remove_static {policy_id}" ) ;
3081- Self :: remove_policy_name ( & mut self . link_names , policy_id) ;
3096+ Self :: remove_policy_name ( & mut self . static_policy_names , policy_id) ;
30823097 }
30833098 }
30843099
@@ -3135,11 +3150,14 @@ mod prop_test_policy_set_operations {
31353150 }
31363151 }
31373152
3138- /// Panics if policy_set.links () or policy_set.templates() doesn't match the model's
3153+ /// Panics if policy_set.policies () or policy_set.templates() doesn't match the model's
31393154 /// static policies, links or templates
31403155 fn check_equiv ( & self ) {
31413156 let real_policy_set_links: Vec < _ > = self . policy_set . policies ( ) . collect ( ) ;
3142- for policy_name in & self . link_names {
3157+ let real_policy_set_templates: Vec < _ > = self . policy_set . templates ( ) . collect ( ) ;
3158+ // A static policy (in the model) should be in the `PolicySet`'s ast.links and ast.templates,
3159+ // but is only returned by policy_set.policies().
3160+ for policy_name in & self . static_policy_names {
31433161 assert ! ( real_policy_set_links
31443162 . iter( )
31453163 . any( |p| p. id( ) == & PolicyId :: from_str( & policy_name) . unwrap( ) ) ) ;
@@ -3149,9 +3167,10 @@ mod prop_test_policy_set_operations {
31493167 . iter( )
31503168 . any( |p| p. id( ) == & PolicyId :: from_str( & policy_name) . unwrap( ) ) ) ;
31513169 }
3170+
31523171 for link_name in real_policy_set_links {
31533172 assert ! (
3154- self . link_names
3173+ self . static_policy_names
31553174 . iter( )
31563175 . any( |p| link_name. id( ) == & PolicyId :: from_str( p) . unwrap( ) )
31573176 || self
@@ -3161,7 +3180,6 @@ mod prop_test_policy_set_operations {
31613180 ) ;
31623181 }
31633182
3164- let real_policy_set_templates: Vec < _ > = self . policy_set . templates ( ) . collect ( ) ;
31653183 for template_name in & self . template_names {
31663184 assert ! ( real_policy_set_templates
31673185 . iter( )
0 commit comments