@@ -640,13 +640,18 @@ impl<'tcx> Tree {
640640        // Register new_tag as a child of parent_tag 
641641        self . nodes . get_mut ( parent_idx) . unwrap ( ) . children . push ( idx) ; 
642642
643-         // We need to know the biggest  SIFA for `update_last_accessed_after_retag` below . 
644-         let  mut  max_sifa  = default_strongest_idempotent; 
643+         // We need to know the weakest  SIFA for `update_idempotent_foreign_access_after_retag` . 
644+         let  mut  min_sifa  = default_strongest_idempotent; 
645645        for  ( Range  {  start,  end } ,  & perm)  in 
646646            inside_perms. iter ( Size :: from_bytes ( 0 ) ,  inside_perms. size ( ) ) 
647647        { 
648648            assert ! ( perm. permission. is_initial( ) ) ; 
649-             max_sifa = cmp:: max ( max_sifa,  perm. idempotent_foreign_access ) ; 
649+             assert_eq ! ( 
650+                 perm. idempotent_foreign_access, 
651+                 perm. permission. strongest_idempotent_foreign_access( protected) 
652+             ) ; 
653+ 
654+             min_sifa = cmp:: min ( min_sifa,  perm. idempotent_foreign_access ) ; 
650655            for  ( _perms_range,  perms)  in  self 
651656                . rperms 
652657                . iter_mut ( Size :: from_bytes ( start)  + base_offset,  Size :: from_bytes ( end - start) ) 
@@ -656,22 +661,28 @@ impl<'tcx> Tree {
656661        } 
657662
658663        // Inserting the new perms might have broken the SIFA invariant (see 
659-         // `foreign_access_skipping.rs`). We now weaken the recorded SIFA for our parents, until the 
660-         // invariant is restored. We could weaken them all to `LocalAccess`, but it is more 
661-         // efficient to compute the SIFA for the new permission statically, and use that. For this 
662-         // we need the *maximum* SIFA (`Write` needs more fixup than `None`). 
663-         self . update_last_accessed_after_retag ( parent_idx,  max_sifa) ; 
664+         // `foreign_access_skipping.rs`) if the SIFA we inserted is weaker than that of some parent. 
665+         // We now weaken the recorded SIFA for our parents, until the invariant is restored. We 
666+         // could weaken them all to `None`, but it is more efficient to compute the SIFA for the new 
667+         // permission statically, and use that. For this we need the *minimum* SIFA (`None` needs 
668+         // more fixup than `Write`). 
669+         self . update_idempotent_foreign_access_after_retag ( parent_idx,  min_sifa) ; 
664670
665671        interp_ok ( ( ) ) 
666672    } 
667673
668-     /// Restores the SIFA "children are stronger" invariant after a retag. 
669- /// See `foreign_access_skipping` and `new_child`. 
670- fn  update_last_accessed_after_retag ( 
674+     /// Restores the SIFA "children are stronger"/"parents are weaker" invariant after a retag: 
675+ /// reduce the SIFA of `current` and its parents to be no stronger than `strongest_allowed`. 
676+ /// See `foreign_access_skipping.rs` and [`Tree::new_child`]. 
677+ fn  update_idempotent_foreign_access_after_retag ( 
671678        & mut  self , 
672679        mut  current :  UniIndex , 
673680        strongest_allowed :  IdempotentForeignAccess , 
674681    )  { 
682+         if  strongest_allowed == IdempotentForeignAccess :: Write  { 
683+             // Nothing is stronger than `Write`. 
684+             return ; 
685+         } 
675686        // We walk the tree upwards, until the invariant is restored 
676687        loop  { 
677688            let  current_node = self . nodes . get_mut ( current) . unwrap ( ) ; 
0 commit comments