Skip to content

Commit 420e209

Browse files
nilehmannnilehmann
authored
Use type-relative associated refinements (#47)
1 parent c86f064 commit 420e209

5 files changed

Lines changed: 207 additions & 207 deletions

File tree

‎arch/cortex-m/src/mpu.rs‎

Lines changed: 37 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -422,7 +422,7 @@ fn next_aligned_power_of_two(po2_aligned_start: usize, min_size: usize) -> Optio
422422
#[flux_rs::assoc(fn perms(r: Self) -> mpu::Permissions { r.perms })]
423423
#[flux_rs::assoc(fn overlaps(region1: Self, start: int, end: int) -> bool { region_overlaps(region1, start, end)})]
424424
impl mpu::RegionDescriptor for CortexMRegion {
425-
#[flux_rs::sig(fn (rnum: usize) -> Self {r: !<Self as RegionDescriptor>::is_set(r) && <Self as RegionDescriptor>::rnum(r) == rnum})]
425+
#[flux_rs::sig(fn (rnum: usize) -> Self {r: !Self::is_set(r) && Self::rnum(r) == rnum})]
426426
fn default(region_num: usize) -> Self {
427427
// TODO: Do better with precondition
428428
if region_num < 8 {
@@ -432,7 +432,7 @@ impl mpu::RegionDescriptor for CortexMRegion {
432432
}
433433
}
434434

435-
#[flux_rs::sig(fn (&Self[@r]) -> Option<FluxPtrU8{ptr: <Self as RegionDescriptor>::start(r) == ptr}>[<Self as RegionDescriptor>::is_set(r)])]
435+
#[flux_rs::sig(fn (&Self[@r]) -> Option<FluxPtrU8{ptr: Self::start(r) == ptr}>[Self::is_set(r)])]
436436
fn start(&self) -> Option<FluxPtrU8> {
437437
match self.location {
438438
Some(loc) => Some(loc.accessible_start),
@@ -441,20 +441,20 @@ impl mpu::RegionDescriptor for CortexMRegion {
441441
}
442442

443443
#[flux_rs::reveal(valid_size)]
444-
#[flux_rs::sig(fn (&Self[@r]) -> Option<usize{sz: <Self as RegionDescriptor>::size(r) == sz && valid_size(sz) && valid_size(<Self as RegionDescriptor>::start(r) + sz)}>[<Self as RegionDescriptor>::is_set(r)])]
444+
#[flux_rs::sig(fn (&Self[@r]) -> Option<usize{sz: Self::size(r) == sz && valid_size(sz) && valid_size(Self::start(r) + sz)}>[Self::is_set(r)])]
445445
fn size(&self) -> Option<usize> {
446446
match self.location {
447447
Some(loc) => Some(loc.accessible_size),
448448
None => None,
449449
}
450450
}
451451

452-
#[flux_rs::sig(fn (&Self[@r]) -> bool[<Self as RegionDescriptor>::is_set(r)])]
452+
#[flux_rs::sig(fn (&Self[@r]) -> bool[Self::is_set(r)])]
453453
fn is_set(&self) -> bool {
454454
self.location.is_some()
455455
}
456456

457-
#[flux_rs::sig(fn (&Self[@r], start: usize, end: usize) -> bool[<Self as RegionDescriptor>::overlaps(r, start, end)])]
457+
#[flux_rs::sig(fn (&Self[@r], start: usize, end: usize) -> bool[Self::overlaps(r, start, end)])]
458458
fn overlaps(&self, start: usize, end: usize) -> bool {
459459
self.region_overlaps(start, end)
460460
}
@@ -467,22 +467,22 @@ impl mpu::RegionDescriptor for CortexMRegion {
467467
region_size: usize,
468468
permissions: mpu::Permissions,
469469
) -> Option<Pair<Self, Self>{p:
470-
<Self as RegionDescriptor>::start(p.fst) >= available_start &&
471-
((!<Self as RegionDescriptor>::is_set(p.snd)) =>
472-
<Self as RegionDescriptor>::regions_can_access_exactly(
470+
Self::start(p.fst) >= available_start &&
471+
((!Self::is_set(p.snd)) =>
472+
Self::regions_can_access_exactly(
473473
p.fst,
474474
p.snd,
475-
<Self as RegionDescriptor>::start(p.fst),
476-
<Self as RegionDescriptor>::start(p.fst) + <Self as RegionDescriptor>::size(p.fst),
475+
Self::start(p.fst),
476+
Self::start(p.fst) + Self::size(p.fst),
477477
permissions
478478
)
479479
) &&
480-
(<Self as RegionDescriptor>::is_set(p.snd) =>
481-
<Self as RegionDescriptor>::regions_can_access_exactly(
480+
(Self::is_set(p.snd) =>
481+
Self::regions_can_access_exactly(
482482
p.fst,
483483
p.snd,
484-
<Self as RegionDescriptor>::start(p.fst),
485-
<Self as RegionDescriptor>::start(p.fst) + <Self as RegionDescriptor>::size(p.fst) + <Self as RegionDescriptor>::size(p.snd),
484+
Self::start(p.fst),
485+
Self::start(p.fst) + Self::size(p.fst) + Self::size(p.snd),
486486
permissions
487487
)
488488
)
@@ -575,25 +575,25 @@ impl mpu::RegionDescriptor for CortexMRegion {
575575
max_region_number: usize,
576576
permissions: mpu::Permissions,
577577
) -> Option<Pair<Self, Self>{p:
578-
((!<Self as RegionDescriptor>::is_set(p.snd)) =>
579-
<Self as RegionDescriptor>::regions_can_access_exactly(
578+
((!Self::is_set(p.snd)) =>
579+
Self::regions_can_access_exactly(
580580
p.fst,
581581
p.snd,
582582
region_start,
583-
region_start + <Self as RegionDescriptor>::size(p.fst),
583+
region_start + Self::size(p.fst),
584584
permissions
585585
) &&
586-
<Self as RegionDescriptor>::size(p.fst) >= region_size
586+
Self::size(p.fst) >= region_size
587587
) &&
588-
(<Self as RegionDescriptor>::is_set(p.snd) =>
589-
<Self as RegionDescriptor>::regions_can_access_exactly(
588+
(Self::is_set(p.snd) =>
589+
Self::regions_can_access_exactly(
590590
p.fst,
591591
p.snd,
592592
region_start,
593-
region_start + <Self as RegionDescriptor>::size(p.fst) + <Self as RegionDescriptor>::size(p.snd),
593+
region_start + Self::size(p.fst) + Self::size(p.snd),
594594
permissions
595595
) &&
596-
<Self as RegionDescriptor>::size(p.fst) + <Self as RegionDescriptor>::size(p.snd) >= region_size
596+
Self::size(p.fst) + Self::size(p.snd) >= region_size
597597
)
598598
}> requires max_region_number > 0 && max_region_number < 8)]
599599
fn update_regions(
@@ -683,7 +683,7 @@ impl mpu::RegionDescriptor for CortexMRegion {
683683
start: FluxPtrU8,
684684
size: usize,
685685
permissions: mpu::Permissions,
686-
) -> Option<Self{r: <Self as RegionDescriptor>::region_can_access_exactly(r, start, start + size, permissions)}>
686+
) -> Option<Self{r: Self::region_can_access_exactly(r, start, start + size, permissions)}>
687687
requires region_number < 8
688688
)]
689689
fn create_exact_region(
@@ -753,10 +753,10 @@ impl mpu::RegionDescriptor for CortexMRegion {
753753

754754
#[flux_rs::sig(fn (&Self[@r], start: FluxPtrU8, end: FluxPtrU8, perms: mpu::Permissions)
755755
requires
756-
<Self as RegionDescriptor>::region_can_access_exactly(r, start, end, perms)
756+
Self::region_can_access_exactly(r, start, end, perms)
757757
ensures
758-
!<Self as RegionDescriptor>::overlaps(r, 0, start) &&
759-
!<Self as RegionDescriptor>::overlaps(r, end, u32::MAX)
758+
!Self::overlaps(r, 0, start) &&
759+
!Self::overlaps(r, end, u32::MAX)
760760
)]
761761
fn lemma_region_can_access_exactly_implies_no_overlap(
762762
&self,
@@ -767,12 +767,12 @@ impl mpu::RegionDescriptor for CortexMRegion {
767767
}
768768

769769
#[flux_rs::sig(fn (&Self[@r1], &Self[@r2], start: FluxPtrU8, end: FluxPtrU8, perms: mpu::Permissions)
770-
requires <Self as RegionDescriptor>::regions_can_access_exactly(r1, r2, start, end, perms)
770+
requires Self::regions_can_access_exactly(r1, r2, start, end, perms)
771771
ensures
772-
!<Self as RegionDescriptor>::overlaps(r1, 0, start) &&
773-
!<Self as RegionDescriptor>::overlaps(r1, end, u32::MAX) &&
774-
!<Self as RegionDescriptor>::overlaps(r2, 0, start) &&
775-
!<Self as RegionDescriptor>::overlaps(r2, end, u32::MAX)
772+
!Self::overlaps(r1, 0, start) &&
773+
!Self::overlaps(r1, end, u32::MAX) &&
774+
!Self::overlaps(r2, 0, start) &&
775+
!Self::overlaps(r2, end, u32::MAX)
776776
)]
777777
#[flux_rs::trusted_impl]
778778
fn lemma_regions_can_access_exactly_implies_no_overlap(
@@ -786,9 +786,9 @@ impl mpu::RegionDescriptor for CortexMRegion {
786786

787787
#[flux_rs::sig(fn (&Self[@r], access_end: FluxPtrU8, desired_end: FluxPtrU8)
788788
requires
789-
!<Self as RegionDescriptor>::overlaps(r, access_end, u32::MAX) &&
789+
!Self::overlaps(r, access_end, u32::MAX) &&
790790
access_end <= desired_end
791-
ensures !<Self as RegionDescriptor>::overlaps(r, desired_end, u32::MAX)
791+
ensures !Self::overlaps(r, desired_end, u32::MAX)
792792
)]
793793
fn lemma_no_overlap_le_addr_implies_no_overlap_addr(
794794
&self,
@@ -798,8 +798,8 @@ impl mpu::RegionDescriptor for CortexMRegion {
798798
}
799799

800800
#[flux_rs::sig(fn (&Self[@r], start: FluxPtrU8, end: FluxPtrU8)
801-
requires !<Self as RegionDescriptor>::is_set(r)
802-
ensures !<Self as RegionDescriptor>::overlaps(r, start, end)
801+
requires !Self::is_set(r)
802+
ensures !Self::overlaps(r, start, end)
803803
)]
804804
fn lemma_region_not_set_implies_no_overlap(&self, _start: FluxPtrU8, _end: FluxPtrU8) {}
805805

@@ -810,11 +810,11 @@ impl mpu::RegionDescriptor for CortexMRegion {
810810
mem_end: FluxPtrU8
811811
)
812812
requires
813-
<Self as RegionDescriptor>::region_can_access_exactly(r, flash_start, flash_end, mpu::Permissions { r: true, x: true, w: false })
813+
Self::region_can_access_exactly(r, flash_start, flash_end, mpu::Permissions { r: true, x: true, w: false })
814814
&&
815815
flash_end <= mem_start
816816
ensures
817-
!<Self as RegionDescriptor>::overlaps(r, mem_start, mem_end)
817+
!Self::overlaps(r, mem_start, mem_end)
818818
819819
)]
820820
fn lemma_region_can_access_flash_implies_no_app_block_overlaps(

‎arch/rv32i/src/pmp.rs‎

Lines changed: 38 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -885,25 +885,25 @@ impl<const MPU_REGIONS: usize> PMPUserRegion<MPU_REGIONS> {
885885
#[flux_rs::assoc(fn perms(r: Self) -> mpu::Permissions { r.perms })]
886886
#[flux_rs::assoc(fn overlaps(r1: Self, start: int, end: int) -> bool { region_overlaps(r1, start, end) })]
887887
impl<const MPU_REGIONS: usize> RegionDescriptor for PMPUserRegion<MPU_REGIONS> {
888-
#[flux_rs::sig(fn (&Self[@r]) -> Option<FluxPtrU8{ptr: <Self as RegionDescriptor>::start(r) == ptr}>[<Self as RegionDescriptor>::is_set(r)])]
888+
#[flux_rs::sig(fn (&Self[@r]) -> Option<FluxPtrU8{ptr: Self::start(r) == ptr}>[Self::is_set(r)])]
889889
fn start(&self) -> Option<FluxPtrU8> {
890890
self.start
891891
}
892892

893-
#[flux_rs::sig(fn (&Self[@r]) -> Option<usize{sz: <Self as RegionDescriptor>::size(r) == sz && valid_size(sz) && valid_size(<Self as RegionDescriptor>::start(r) + sz)}>[<Self as RegionDescriptor>::is_set(r)])]
893+
#[flux_rs::sig(fn (&Self[@r]) -> Option<usize{sz: Self::size(r) == sz && valid_size(sz) && valid_size(Self::start(r) + sz)}>[Self::is_set(r)])]
894894
fn size(&self) -> Option<usize> {
895895
match (self.start, self.end) {
896896
(Some(start), Some(end)) => Some(end.as_usize() - start.as_usize()),
897897
_ => None,
898898
}
899899
}
900900

901-
#[flux_rs::sig(fn (&Self[@r]) -> bool[<Self as RegionDescriptor>::is_set(r)])]
901+
#[flux_rs::sig(fn (&Self[@r]) -> bool[Self::is_set(r)])]
902902
fn is_set(&self) -> bool {
903903
self.start.is_some() && self.end.is_some()
904904
}
905905

906-
#[flux_rs::sig(fn (rnum: usize) -> Self {r: !<Self as RegionDescriptor>::is_set(r) && <Self as RegionDescriptor>::rnum(r) == rnum})]
906+
#[flux_rs::sig(fn (rnum: usize) -> Self {r: !Self::is_set(r) && Self::rnum(r) == rnum})]
907907
fn default(region_number: usize) -> Self {
908908
Self {
909909
region_number,
@@ -914,7 +914,7 @@ impl<const MPU_REGIONS: usize> RegionDescriptor for PMPUserRegion<MPU_REGIONS> {
914914
}
915915
}
916916

917-
#[flux_rs::sig(fn (&Self[@r], start: usize, end: usize) -> bool[<Self as RegionDescriptor>::overlaps(r, start, end)])]
917+
#[flux_rs::sig(fn (&Self[@r], start: usize, end: usize) -> bool[Self::overlaps(r, start, end)])]
918918
fn overlaps(&self, start: usize, end: usize) -> bool {
919919
region_overlaps(self, start, end)
920920
}
@@ -926,7 +926,7 @@ impl<const MPU_REGIONS: usize> RegionDescriptor for PMPUserRegion<MPU_REGIONS> {
926926
size: usize,
927927
permissions: mpu::Permissions,
928928
) -> Option<Self{r:
929-
<Self as RegionDescriptor>::region_can_access_exactly(r, start, start + size, permissions)
929+
Self::region_can_access_exactly(r, start, start + size, permissions)
930930
}>
931931
requires region_number < 8
932932
)]
@@ -978,26 +978,26 @@ impl<const MPU_REGIONS: usize> RegionDescriptor for PMPUserRegion<MPU_REGIONS> {
978978
region_size: usize,
979979
permissions: mpu::Permissions,
980980
) -> Option<Pair<Self, Self>{p:
981-
<Self as RegionDescriptor>::start(p.fst) >= available_start &&
982-
((!<Self as RegionDescriptor>::is_set(p.snd)) =>
983-
<Self as RegionDescriptor>::regions_can_access_exactly(
981+
Self::start(p.fst) >= available_start &&
982+
((!Self::is_set(p.snd)) =>
983+
Self::regions_can_access_exactly(
984984
p.fst,
985985
p.snd,
986-
<Self as RegionDescriptor>::start(p.fst),
987-
<Self as RegionDescriptor>::start(p.fst) + <Self as RegionDescriptor>::size(p.fst),
986+
Self::start(p.fst),
987+
Self::start(p.fst) + Self::size(p.fst),
988988
permissions
989989
)
990990
) &&
991-
(<Self as RegionDescriptor>::is_set(p.snd) =>
992-
<Self as RegionDescriptor>::regions_can_access_exactly(
991+
(Self::is_set(p.snd) =>
992+
Self::regions_can_access_exactly(
993993
p.fst,
994994
p.snd,
995-
<Self as RegionDescriptor>::start(p.fst),
996-
<Self as RegionDescriptor>::start(p.fst) + <Self as RegionDescriptor>::size(p.fst) + <Self as RegionDescriptor>::size(p.snd),
995+
Self::start(p.fst),
996+
Self::start(p.fst) + Self::size(p.fst) + Self::size(p.snd),
997997
permissions
998998
)
999999
) &&
1000-
!<Self as RegionDescriptor>::is_set(p.snd)
1000+
!Self::is_set(p.snd)
10011001
}> requires max_region_number > 0 && max_region_number < 8
10021002
)]
10031003
fn allocate_regions(
@@ -1085,25 +1085,25 @@ impl<const MPU_REGIONS: usize> RegionDescriptor for PMPUserRegion<MPU_REGIONS> {
10851085
max_region_number: usize,
10861086
permissions: mpu::Permissions,
10871087
) -> Option<Pair<Self, Self>{p:
1088-
((!<Self as RegionDescriptor>::is_set(p.snd)) =>
1089-
<Self as RegionDescriptor>::regions_can_access_exactly(
1088+
((!Self::is_set(p.snd)) =>
1089+
Self::regions_can_access_exactly(
10901090
p.fst,
10911091
p.snd,
10921092
region_start,
1093-
region_start + <Self as RegionDescriptor>::size(p.fst),
1093+
region_start + Self::size(p.fst),
10941094
permissions
10951095
) &&
1096-
<Self as RegionDescriptor>::size(p.fst) >= region_size
1096+
Self::size(p.fst) >= region_size
10971097
) &&
1098-
(<Self as RegionDescriptor>::is_set(p.snd) =>
1099-
<Self as RegionDescriptor>::regions_can_access_exactly(
1098+
(Self::is_set(p.snd) =>
1099+
Self::regions_can_access_exactly(
11001100
p.fst,
11011101
p.snd,
11021102
region_start,
1103-
region_start + <Self as RegionDescriptor>::size(p.fst) + <Self as RegionDescriptor>::size(p.snd),
1103+
region_start + Self::size(p.fst) + Self::size(p.snd),
11041104
permissions
11051105
) &&
1106-
<Self as RegionDescriptor>::size(p.fst) + <Self as RegionDescriptor>::size(p.snd) >= region_size
1106+
Self::size(p.fst) + Self::size(p.snd) >= region_size
11071107
)
11081108
}> requires max_region_number > 0 && max_region_number < 8)]
11091109
fn update_regions(
@@ -1151,10 +1151,10 @@ impl<const MPU_REGIONS: usize> RegionDescriptor for PMPUserRegion<MPU_REGIONS> {
11511151
}
11521152

11531153
#[flux_rs::sig(fn (&Self[@r], start: FluxPtrU8, end: FluxPtrU8, perms: mpu::Permissions)
1154-
requires <Self as RegionDescriptor>::region_can_access_exactly(r, start, end, perms)
1154+
requires Self::region_can_access_exactly(r, start, end, perms)
11551155
ensures
1156-
!<Self as RegionDescriptor>::overlaps(r, 0, start) &&
1157-
!<Self as RegionDescriptor>::overlaps(r, end, u32::MAX)
1156+
!Self::overlaps(r, 0, start) &&
1157+
!Self::overlaps(r, end, u32::MAX)
11581158
)]
11591159
fn lemma_region_can_access_exactly_implies_no_overlap(
11601160
&self,
@@ -1165,12 +1165,12 @@ impl<const MPU_REGIONS: usize> RegionDescriptor for PMPUserRegion<MPU_REGIONS> {
11651165
}
11661166

11671167
#[flux_rs::sig(fn (&Self[@r1], &Self[@r2], start: FluxPtrU8, end: FluxPtrU8, perms: mpu::Permissions)
1168-
requires <Self as RegionDescriptor>::regions_can_access_exactly(r1, r2, start, end, perms)
1168+
requires Self::regions_can_access_exactly(r1, r2, start, end, perms)
11691169
ensures
1170-
!<Self as RegionDescriptor>::overlaps(r1, 0, start) &&
1171-
!<Self as RegionDescriptor>::overlaps(r1, end, u32::MAX) &&
1172-
!<Self as RegionDescriptor>::overlaps(r2, 0, start) &&
1173-
!<Self as RegionDescriptor>::overlaps(r2, end, u32::MAX)
1170+
!Self::overlaps(r1, 0, start) &&
1171+
!Self::overlaps(r1, end, u32::MAX) &&
1172+
!Self::overlaps(r2, 0, start) &&
1173+
!Self::overlaps(r2, end, u32::MAX)
11741174
)]
11751175
fn lemma_regions_can_access_exactly_implies_no_overlap(
11761176
_r1: &Self,
@@ -1186,9 +1186,9 @@ impl<const MPU_REGIONS: usize> RegionDescriptor for PMPUserRegion<MPU_REGIONS> {
11861186

11871187
#[flux_rs::sig(fn (&Self[@r], access_end: FluxPtrU8, desired_end: FluxPtrU8)
11881188
requires
1189-
!<Self as RegionDescriptor>::overlaps(r, access_end, u32::MAX) &&
1189+
!Self::overlaps(r, access_end, u32::MAX) &&
11901190
access_end <= desired_end
1191-
ensures !<Self as RegionDescriptor>::overlaps(r, desired_end, u32::MAX)
1191+
ensures !Self::overlaps(r, desired_end, u32::MAX)
11921192
)]
11931193
fn lemma_no_overlap_le_addr_implies_no_overlap_addr(
11941194
&self,
@@ -1198,8 +1198,8 @@ impl<const MPU_REGIONS: usize> RegionDescriptor for PMPUserRegion<MPU_REGIONS> {
11981198
}
11991199

12001200
#[flux_rs::sig(fn (&Self[@r], start: FluxPtrU8, end: FluxPtrU8)
1201-
requires !<Self as RegionDescriptor>::is_set(r)
1202-
ensures !<Self as RegionDescriptor>::overlaps(r, start, end)
1201+
requires !Self::is_set(r)
1202+
ensures !Self::overlaps(r, start, end)
12031203
)]
12041204
fn lemma_region_not_set_implies_no_overlap(&self, start: FluxPtrU8, end: FluxPtrU8) {}
12051205

@@ -1210,11 +1210,11 @@ impl<const MPU_REGIONS: usize> RegionDescriptor for PMPUserRegion<MPU_REGIONS> {
12101210
mem_end: FluxPtrU8
12111211
)
12121212
requires
1213-
<Self as RegionDescriptor>::region_can_access_exactly(r, flash_start, flash_end, mpu::Permissions { r: true, x: true, w: false })
1213+
Self::region_can_access_exactly(r, flash_start, flash_end, mpu::Permissions { r: true, x: true, w: false })
12141214
&&
12151215
flash_end <= mem_start
12161216
ensures
1217-
!<Self as RegionDescriptor>::overlaps(r, mem_start, mem_end)
1217+
!Self::overlaps(r, mem_start, mem_end)
12181218
12191219
)]
12201220
fn lemma_region_can_access_flash_implies_no_app_block_overlaps(

‎flux_support/src/extern_specs/partial_ord.rs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,9 @@ use core::cmp::PartialOrd;
66
#[flux_rs::assoc(fn lt(this: Self, other: Rhs) -> bool { true })]
77
#[flux_rs::assoc(fn le(this: Self, other: Rhs) -> bool { true })]
88
trait PartialOrd<Rhs: ?Sized = Self> {
9-
#[flux_rs::sig(fn (&Self[@l], &Rhs[@r]) -> bool[<Self as PartialOrd>::lt(l, r)])]
9+
#[flux_rs::sig(fn (&Self[@l], &Rhs[@r]) -> bool[Self::lt(l, r)])]
1010
fn lt(&self, other: &Rhs) -> bool;
1111

12-
#[flux_rs::sig(fn (&Self[@l], &Rhs[@r]) -> bool[<Self as PartialOrd>::le(l, r)])]
12+
#[flux_rs::sig(fn (&Self[@l], &Rhs[@r]) -> bool[Self::le(l, r)])]
1313
fn le(&self, other: &Rhs) -> bool;
1414
}

0 commit comments

Comments
 (0)