Function lemma_sub_mapping_pa_compose

pub proof fn lemma_sub_mapping_pa_compose(m: Mapping, p: Mapping, orig: Mapping)

Expand description

requires

m.inv(),

orig.inv(),

p.va_range.start >= orig.va_range.start,

p.va_range.end <= orig.va_range.end,

p.pa_range.start
    == (orig.pa_range.start + (p.va_range.start - orig.va_range.start)) as usize,

p.property == orig.property,

m.va_range.start >= p.va_range.start,

m.va_range.end <= p.va_range.end,

m.pa_range.start == (p.pa_range.start + (m.va_range.start - p.va_range.start)) as usize,

m.property == p.property,

ensures

orig.va_range.start <= m.va_range.start,

m.va_range.end <= orig.va_range.end,

m.pa_range.start
    == (orig.pa_range.start + (m.va_range.start - orig.va_range.start)) as usize,

m.property == orig.property,

If m is a sub-mapping of p and p is a sub-mapping of orig, then m is a sub-mapping of orig (PA arithmetic composes).

lemma_sub_mapping_pa_compose