File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -24,7 +24,7 @@ pub tracked struct VmIoPermission<'a> {
2424/// A tracked struct for reasoning about verification-only properties of a [`VmSpace`].
2525///
2626/// This struct serves as a bookkeeper for all _active_ readers/writers within a specific
27- /// virtual memory space. It maintains a holistic view of the memory range coverted by the
27+ /// virtual memory space. It maintains a holistic view of the memory range covered by the
2828/// VM space it is tracking using a [`Ghost<MemView>`]. It also maintains a [`Tracked<MemView>`]
2929/// for the current memories it is holding permissions for, which is a subset of the total
3030/// memory range.
Original file line number Diff line number Diff line change @@ -273,7 +273,7 @@ impl<'a> VmSpace<'a> {
273273 /// # Verification Design
274274 ///
275275 /// This function is marked as `external_body` for now as the current design does not entail
276- /// the conrete implementation details of the underlying data structure of the [`VmSpace`].
276+ /// the concrete implementation details of the underlying data structure of the [`VmSpace`].
277277 ///
278278 /// ## Preconditions
279279 /// None
You can’t perform that action at this time.
0 commit comments