Fil-C on Nix

Filnix wiki

the formal campaign

rocq/theories/Interval.v

What ir.pl's offset intervals derive, and that they hold (Campaign 3; docs/rocq.md).

The reuse forms' rules bound the offset of a flight from its base by offset_interval/8 (Validate.v's oi): the interval of values an integer name can hold, walked through the single definitions of the function. This file states the same derivations as an inductive relation, iv, one constructor per clause of op_interval/9, and proves two things:

  • whatever oi answers, iv derives (offset_interval_iv), so oi's memo and depth limit need no further thought;
  • an iv interval holds of the value a run reads, wherever each name the derivation walks holds what its definition computes from its operands' values where it ran, and each single-definition operand still holds that value (iv_sound). Which names do, at a point of a run, is the run-level invariant's to say; here it is any predicate ok closed under single-definition operands.

Decisions

DecisionWhy
one constructor per clause, each a little more generalop_interval/9 commits to the first clause whose head matches; the relation needs no order, only that each derivation is sound
the depth limit and the memo are not in iva memo keeps only answers derived earlier, so they need no depth; oi_sound carries the memo's invariant
mul names its scaled operand, with the two orders as a premisean iv under a disjunction gets no induction hypothesis
an interval holds modulo the classan l interval is not wrapped (interval_fits/3 accepts any), so it bounds some integer congruent to the value; a w interval fits, so it bounds the signed word itself
a narrow load's relation does not mention memoryany loaded value, extended, lies in the narrow range, so the relation survives every store
an operand that is not a single definition is read where the definition ranit may be defined again after; the clauses that walk an operand walk only single definitions, and the others (and's, urem's, a narrow ext's) bound the result whatever the operand holds
From Stdlib Require Import String ZArith List Bool Lia
From Nanofil Require Import Term Maps Syntax Values Memory Ops Semantics Machine Validate Dominance
Import ListNotations
Open Scope Z_scope

Two classes k and k' that class_eqb finds equal are equal.

38Lemma class_eqb_true
∀ k k′
class_eqbk k′ = true
k = k′
Explore proof 2 tactics

Initial goal

⊢
∀k k′ : class, class_eqbk k′ = true → k = k′

intros k k′ H

k, k′ :
class
H :
class_eqbk k′ = true
⊢
k = k′

destruct k , k′ ; try discriminate H ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros k k′ H
destruct k , k′ ; try discriminate H ; reflexivity

Closes the goal of a clause that answered no interval (H says so) and returned the old memo, derived by Hm: there is no interval to derive, and the memo is still derived.

44Ltac no_answer_now H Hm ≔
injection H as ← ← ; split ; intros ? ? Hno ; discriminate Hno | exact Hm

no_answer_now, for a clause that answers none whatever an operand is: it takes the operands apart until each case closes.

49Ltac no_answer H Hm ≔
first|no_answer_now H Hm|match goal withv : value |- _⇒destruct v ; cbn in H ; no_answer H Hmend

The intervals of one function, read over its single definitions.

55Section Intervals

The function's single definitions, each name with its one definition, as single_definitions builds them.

59Variable once : listname × def

The name n has a single definition, the let that defines n at the class k by the op o from args: let(tmp(n), k, o, args).

63Definition definedn : name k : class o : op args : listvalue : Prop ≔
∃n′, lookupn once = SomeDInstLetn′ k o args ∧ name_eqbn′ n = true

The offset intervals offset_interval/8 derives, as a relation: ivv k lo hi says the operand v read at the class k lies from lo to hi (for l, modulo 2^64). One constructor per clause of op_interval/9, each a little more general than its clause, with the interval_fits test the walk applies to each name.

71Inductive iv: value → class → Z → Z → Prop ≔
∀ c k x
signed_valuek c = Somex
iv_const
ivConstc k x x
∀ n k t args lo hi
definedn k Extt args
narrow_ranget = Somelo, hi
interval_fitsk lo hi = true
iv_narrow
ivTmpn k lo hi
∀ n k a lo hi
definedn k ExtSw a
iva W lo hi
interval_fitsk lo hi = true
iv_sw
ivTmpn k lo hi
∀ n k a lo hi
definedn k ExtUw a
iva W lo hi
0 ≤ lo
interval_fitsk lo hi = true
iv_uw
ivTmpn k lo hi
∀ n k t off args lo hi
definedn k RawLoadLdNarrowt off args
narrow_ranget = Somelo, hi
interval_fitsk lo hi = true
iv_load
ivTmpn k lo hi
∀ n k a lo hi
definedn k Copy a
iva k lo hi
interval_fitsk lo hi = true
iv_copy
ivTmpn k lo hi
∀ n k a b c v
definedn k And a; b
a = Constc ∨ b = Constc
signed_valuek c = Somev
0 ≤ v
interval_fitsk 0 v = true
iv_and
ivTmpn k 0 v
∀ n k a c bits
definedn k Urem a; Constc
class_bitsk = Somebits
0 < c mod 2 ^ bits
c mod 2 ^ bits ≤ 2 ^ bits − 1
interval_fitsk 0 c mod 2 ^ bits − 1 = true
iv_urem
ivTmpn k 0 c mod 2 ^ bits − 1
∀ n k a s bits lo hi
definedn k Shl a; Consts
class_bitsk = Somebits
0 ≤ s
s < bits
iva k lo hi
interval_fitsk lo × 2 ^ s hi × 2 ^ s = true
iv_shl
ivTmpn k lo × 2 ^ s hi × 2 ^ s
∀ n k args x c v lo0 hi0 lo hi
definedn k Mul args
args = x; Constc ∨ args = Constc; x
ivx k lo0 hi0
signed_valuek c = Somev
0 ≤? v
→
lo0 × v, hi0 × v
else
hi0 × v, lo0 × v
=
lo, hi
interval_fitsk lo hi = true
iv_mul
ivTmpn k lo hi
∀ n k a b lo1 hi1 lo2 hi2
definedn k Add a; b
iva k lo1 hi1
ivb k lo2 hi2
interval_fitsk lo1 + lo2 hi1 + hi2 = true
iv_add
ivTmpn k lo1 + lo2 hi1 + hi2
∀ n k a c v lo hi
definedn k Sub a; Constc
signed_valuek c = Somev
iva k lo hi
interval_fitsk lo − v hi − v = true
iv_sub
ivTmpn k lo − v hi − v

The invariant of oi's memo m: each interval it keeps for a name at a class is derived (iv).

111Definition memo_okm : memo : Prop ≔
∀n k lo hi, memo_lookupn k m = SomeSomelo, hi → ivTmpn k lo hi

The empty memo is derived.

115Lemma memo_ok_nil
memo_ok[ ]
Explore proof 2 tactics

Initial goal

once :
listname × def
⊢
memo_ok[ ]

intros n k lo hi E

once :
listname × def
n :
name
k :
class
lo, hi :
Z
E :
memo_lookupn k [ ] = SomeSomelo, hi
⊢
ivTmpn k lo hi

discriminate E

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros n k lo hi E
discriminate E

Recording the answer r for the name n at the class k keeps a derived memo m derived, when r, if an interval, is derived.

120Lemma memo_ok_cons
∀ n k r m
memo_okm
∀lo hi, r = Somelo, hi → ivTmpn k lo hi
memo_okn, k, r :: m
Explore proof 10 tactics

Initial goal

once :
listname × def
⊢
∀n : name k : class r : optionZ × Z m : memo, memo_okm → ∀lo hi : Z, r = Somelo, hi → ivTmpn k lo hi → memo_okn, k, r :: m

intros n k r m Hm Hr n′ k′ lo hi H

once :
listname × def
n :
name
k :
class
r :
optionZ × Z
m :
memo
Hm :
memo_okm
Hr :
∀lo hi : Z, r = Somelo, hi → ivTmpn k lo hi
n′ :
name
k′ :
class
lo, hi :
Z
H :
memo_lookupn′ k′ n, k, r :: m = SomeSomelo, hi
⊢
ivTmpn′ k′ lo hi

simpl in H

once :
listname × def
n :
name
k :
class
r :
optionZ × Z
m :
memo
Hm :
memo_okm
Hr :
∀lo hi : Z, r = Somelo, hi → ivTmpn k lo hi
n′ :
name
k′ :
class
lo, hi :
Z
H :
name_eqbn n′ && class_eqbk k′
→
Somer
else
memo_lookupn′ k′ m
=
SomeSomelo, hi
⊢
ivTmpn′ k′ lo hi

destruct name_eqbn n′ && class_eqbk k′ eqn: E

2 open

once :
listname × def
n :
name
k :
class
r :
optionZ × Z
m :
memo
Hm :
memo_okm
Hr :
∀lo hi : Z, r = Somelo, hi → ivTmpn k lo hi
n′ :
name
k′ :
class
lo, hi :
Z
E :
name_eqbn n′ && class_eqbk k′ = true
H :
Somer = SomeSomelo, hi
⊢
ivTmpn′ k′ lo hi
focused goal
once :
listname × def
n :
name
k :
class
r :
optionZ × Z
m :
memo
Hm :
memo_okm
Hr :
∀lo hi : Z, r = Somelo, hi → ivTmpn k lo hi
n′ :
name
k′ :
class
lo, hi :
Z
E :
name_eqbn n′ && class_eqbk k′ = false
H :
memo_lookupn′ k′ m = SomeSomelo, hi
⊢
ivTmpn′ k′ lo hi

–apply andb_true_iff in E as E1 E2

2 open

once :
listname × def
n :
name
k :
class
r :
optionZ × Z
m :
memo
Hm :
memo_okm
Hr :
∀lo hi : Z, r = Somelo, hi → ivTmpn k lo hi
n′ :
name
k′ :
class
lo, hi :
Z
E1 :
name_eqbn n′ = true
E2 :
class_eqbk k′ = true
H :
Somer = SomeSomelo, hi
⊢
ivTmpn′ k′ lo hi
deferred goal
once :
listname × def
n :
name
k :
class
r :
optionZ × Z
m :
memo
Hm :
memo_okm
Hr :
∀lo hi : Z, r = Somelo, hi → ivTmpn k lo hi
n′ :
name
k′ :
class
lo, hi :
Z
E :
name_eqbn n′ && class_eqbk k′ = false
H :
memo_lookupn′ k′ m = SomeSomelo, hi
⊢
ivTmpn′ k′ lo hi

apply term_eqb_eq in E1

2 open

once :
listname × def
n :
name
k :
class
r :
optionZ × Z
m :
memo
Hm :
memo_okm
Hr :
∀lo hi : Z, r = Somelo, hi → ivTmpn k lo hi
n′ :
name
k′ :
class
lo, hi :
Z
E1 :
n = n′
E2 :
class_eqbk k′ = true
H :
Somer = SomeSomelo, hi
⊢
ivTmpn′ k′ lo hi
deferred goal
once :
listname × def
n :
name
k :
class
r :
optionZ × Z
m :
memo
Hm :
memo_okm
Hr :
∀lo hi : Z, r = Somelo, hi → ivTmpn k lo hi
n′ :
name
k′ :
class
lo, hi :
Z
E :
name_eqbn n′ && class_eqbk k′ = false
H :
memo_lookupn′ k′ m = SomeSomelo, hi
⊢
ivTmpn′ k′ lo hi

apply class_eqb_true in E2

2 open

once :
listname × def
n :
name
k :
class
r :
optionZ × Z
m :
memo
Hm :
memo_okm
Hr :
∀lo hi : Z, r = Somelo, hi → ivTmpn k lo hi
n′ :
name
k′ :
class
lo, hi :
Z
E1 :
n = n′
E2 :
k = k′
H :
Somer = SomeSomelo, hi
⊢
ivTmpn′ k′ lo hi
deferred goal
once :
listname × def
n :
name
k :
class
r :
optionZ × Z
m :
memo
Hm :
memo_okm
Hr :
∀lo hi : Z, r = Somelo, hi → ivTmpn k lo hi
n′ :
name
k′ :
class
lo, hi :
Z
E :
name_eqbn n′ && class_eqbk k′ = false
H :
memo_lookupn′ k′ m = SomeSomelo, hi
⊢
ivTmpn′ k′ lo hi

subst n′ k′

2 open

once :
listname × def
n :
name
k :
class
r :
optionZ × Z
m :
memo
Hm :
memo_okm
Hr :
∀lo hi : Z, r = Somelo, hi → ivTmpn k lo hi
lo, hi :
Z
H :
Somer = SomeSomelo, hi
⊢
ivTmpn k lo hi
deferred goal
once :
listname × def
n :
name
k :
class
r :
optionZ × Z
m :
memo
Hm :
memo_okm
Hr :
∀lo hi : Z, r = Somelo, hi → ivTmpn k lo hi
n′ :
name
k′ :
class
lo, hi :
Z
E :
name_eqbn n′ && class_eqbk k′ = false
H :
memo_lookupn′ k′ m = SomeSomelo, hi
⊢
ivTmpn′ k′ lo hi

injection H as →

2 open

once :
listname × def
n :
name
k :
class
m :
memo
Hm :
memo_okm
lo, hi :
Z
Hr :
∀lo0 hi0 : Z, Somelo, hi = Somelo0, hi0 → ivTmpn k lo0 hi0
⊢
ivTmpn k lo hi
deferred goal
once :
listname × def
n :
name
k :
class
r :
optionZ × Z
m :
memo
Hm :
memo_okm
Hr :
∀lo hi : Z, r = Somelo, hi → ivTmpn k lo hi
n′ :
name
k′ :
class
lo, hi :
Z
E :
name_eqbn n′ && class_eqbk k′ = false
H :
memo_lookupn′ k′ m = SomeSomelo, hi
⊢
ivTmpn′ k′ lo hi

exact Hr_ _ eq_refl

deferred goal
once :
listname × def
n :
name
k :
class
r :
optionZ × Z
m :
memo
Hm :
memo_okm
Hr :
∀lo hi : Z, r = Somelo, hi → ivTmpn k lo hi
n′ :
name
k′ :
class
lo, hi :
Z
E :
name_eqbn n′ && class_eqbk k′ = false
H :
memo_lookupn′ k′ m = SomeSomelo, hi
⊢
ivTmpn′ k′ lo hi

–exact Hm_ _ _ _ H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros n k r m Hm Hr n′ k′ lo hi H
simpl in H
destruct name_eqbn n′ && class_eqbk k′ eqn: E
–apply andb_true_iff in E as E1 E2
apply term_eqb_eq in E1
apply class_eqb_true in E2
subst n′ k′
injection H as →
exact Hr_ _ eq_refl
–exact Hm_ _ _ _ H

What the walk rec of an operand promises op_interval: from a derived memo, an interval it answers is derived, and the memo it returns is derived too.

133Definition rec_okrec : value → class → memo → optionZ × Z × memo : Prop ≔
∀a k m r m′, memo_okm → reca k m = r, m′ → ∀lo hi, r = Somelo, hi → iva k lo hi ∧ memo_okm′

Each clause of op_interval (op_interval/9) is sound: where the name n is defined by the op o over args and the operand walk rec keeps rec_ok, an interval the clause answers that fits the class is derived for n, and the memo stays derived.

141Lemma op_interval_ok
∀ rec o args k m r m′ n
rec_okrec
memo_okm
definedn k o args
op_intervalrec o args k m = r, m′
∀lo hi, r = Somelo, hi → interval_fitsk lo hi = true → ivTmpn k lo hi ∧ memo_okm′
Proof 141 steps Qed
intros rec o args k m r m′ n Hrec Hm Hd H

the cases where the op's operands' walks are the answer

destruct o ; simpl in H ; try no_answer H Hm

add

–destruct args as | a | b | c args ; cbn in H ; try no_answer H Hm
destruct reca k m as lo1 hi1 | m1 eqn: Ea ; destruct Hrec_ _ _ _ _ Hm Ea as Ha Hm1
+destruct recb k m1 as lo2 hi2 | m2 eqn: Eb ; destruct Hrec_ _ _ _ _ Hm1 Eb as Hb Hm2
∗injection H as ← ←
split ; | exact Hm2
intros lo hi E Hf
injection E as ← ←
exact iv_add_ _ _ _ _ _ _ _ Hd Ha_ _ eq_refl Hb_ _ eq_refl Hf
∗injection H as ← ←
split ; intros lo hi E ; discriminate E | exact Hm2
+injection H as ← ←
split ; intros lo hi E ; discriminate E | exact Hm1

sub

–destruct args as | a | b | c args ; cbn in H ; try no_answer H Hm
destruct b as nb | cb | gb ; cbn in H ; try no_answer H Hm
destruct signed_valuek cb as v | eqn: Ev ; | no_answer H Hm
destruct reca k m as lo0 hi0 | m1 eqn: Er ; destruct Hrec_ _ _ _ _ Hm Er as Hr Hm1
+injection H as ← ←
split ; | exact Hm1
intros lo hi E Hf
injection E as ← ←
exact iv_sub_ _ _ _ _ _ _ Hd Ev Hr_ _ eq_refl Hf
+injection H as ← ←
split ; intros lo hi E ; discriminate E | exact Hm1

mul

–assert Hsc : ∀x c r0 m0, args = x; Constc ∨ args = Constc; x → match signed_valuek c with Somev ⇒ match recx k m with Somelo, hi, m1 ⇒ Someif 0 ≤? v then lo × v, hi × v else hi × v, lo × v, m1 | r ⇒ r end | None ⇒ None, m end = r0, m0 → ∀lo hi, r0 = Somelo, hi → interval_fitsk lo hi = true → ivTmpn k lo hi ∧ memo_okm0
{intros x c r0 m0 Ha E
destruct signed_valuek c as v | eqn: Ev ; | no_answer_now E Hm
destruct recx k m as lo0 hi0 | m1 eqn: Er ; destruct Hrec_ _ _ _ _ Hm Er as Hr Hm1 ; | no_answer_now E Hm1
injection E as ← ←
split ; | exact Hm1
intros lo hi E′ Hf
injection E' as E′
exact iv_mul_ _ _ _ _ _ _ _ _ _ Hd Ha Hr_ _ eq_refl Ev E' Hf
destruct args as | a | b | x args ; cbn in H ; try no_answer H Hm
destruct b as nb | cb | gb ; destruct a as na | ca | ga ; cbn in H ; try no_answer H Hm
+exact Hsc_ ca _ _ or_introreq_refl H
+exact Hsc_ cb _ _ or_introleq_refl H
+exact Hsc_ cb _ _ or_introleq_refl H
+exact Hsc_ ca _ _ or_introreq_refl H

urem

–destruct args as | a | b | c args ; cbn in H ; try no_answer H Hm
destruct b as nb | cb | gb ; cbn in H ; try no_answer H Hm
destruct class_bitsk as bits | eqn: Eb ; | no_answer H Hm
injection H as ← ←
split ; | exact Hm
intros lo hi E Hf
destruct 0 <? cb mod 2 ^ bits && cb mod 2 ^ bits ≤? 2 ^ bits − 1 eqn: Ec ; | discriminate E
injection E as ← ←
apply andb_true_iff in Ec as E1 E2
apply Z.ltb_lt in E1
apply Z.leb_le in E2
exact iv_urem_ _ _ _ _ Hd Eb E1 E2 Hf

and

–assert Hmask : ∀c lo hi, ∃a b, args = a; b ∧ a = Constc ∨ b = Constc → match signed_valuek c with Somev ⇒ if 0 ≤? v then Some0, v else None | None ⇒ None end = Somelo, hi → interval_fitsk lo hi = true → ivTmpn k lo hi
{intros c lo hi a & b & → & Hc E Hf
destruct signed_valuek c as v | eqn: Ev ; | discriminate E
destruct 0 ≤? v eqn: Ez ; | discriminate E
injection E as ← ←
apply Z.leb_le in Ez
exact iv_and_ _ _ _ _ _ Hd Hc Ev Ez Hf
destruct args as | a | b | x args ; cbn in H ; try no_answer H Hm

ir.pl tries the right operand's mask first, then the left's.

destruct a as na | ca | ga ; destruct b as nb | cb | gb ; cbn in H ; try no_answer H Hm
+destruct signed_valuek cb as vb | eqn: Evb ; destruct 0 ≤? vb eqn: Ezb | ; cbn in H ; | no_answer H Hm | no_answer H Hm
injection H as ← ←
split ; | exact Hm
intros lo hi E Hf
apply Hmaskcb lo hi ex_intro_ _ ex_intro_ _ conjeq_refl or_introreq_refl ; | exact Hf
rewrite Evb , Ezb
exact E
+injection H as ← ←
split ; | exact Hm
intros lo hi E Hf
exact Hmaskca lo hi ex_intro_ _ ex_intro_ _ conjeq_refl or_introleq_refl E Hf
+destruct signed_valuek cb as vb | eqn: Evb ; destruct 0 ≤? vb eqn: Ezb | ; cbn in H ; injection H as ← ← ; split ; try exact Hm ; intros lo hi E Hf
∗apply Hmaskcb lo hi ex_intro_ _ ex_intro_ _ conjeq_refl or_introreq_refl ; | exact Hf
rewrite Evb , Ezb
exact E
∗exact Hmaskca lo hi ex_intro_ _ ex_intro_ _ conjeq_refl or_introleq_refl E Hf
∗exact Hmaskca lo hi ex_intro_ _ ex_intro_ _ conjeq_refl or_introleq_refl E Hf
+injection H as ← ←
split ; | exact Hm
intros lo hi E Hf
exact Hmaskca lo hi ex_intro_ _ ex_intro_ _ conjeq_refl or_introleq_refl E Hf
+destruct signed_valuek cb as vb | eqn: Evb ; destruct 0 ≤? vb eqn: Ezb | ; cbn in H ; | no_answer H Hm | no_answer H Hm
injection H as ← ←
split ; | exact Hm
intros lo hi E Hf
apply Hmaskcb lo hi ex_intro_ _ ex_intro_ _ conjeq_refl or_introreq_refl ; | exact Hf
rewrite Evb , Ezb
exact E

shl

–destruct args as | a | b | c args ; cbn in H ; try no_answer H Hm
destruct b as nb | s | gb ; cbn in H ; try no_answer H Hm
destruct class_bitsk as bits | eqn: Eb ; | no_answer H Hm
destruct 0 ≤? s && s <? bits eqn: Es ; | no_answer H Hm
apply andb_true_iff in Es as Es1 Es2
apply Z.leb_le in Es1
apply Z.ltb_lt in Es2
destruct reca k m as lo0 hi0 | m1 eqn: Er
+destruct Hrec_ _ _ _ _ Hm Er as Hr Hm1
injection H as ← ←
split ; | exact Hm1
intros lo hi E Hf
injection E as ← ←
exact iv_shl_ _ _ _ _ _ _ Hd Eb Es1 Es2 Hr_ _ eq_refl Hf
+destruct Hrec_ _ _ _ _ Hm Er as _ Hm1
injection H as ← ←
split ; intros lo hi E ; discriminate E | exact Hm1

copy

–destruct args as | a | a2 args ; cbn in H ; try no_answer H Hm
destruct Hrec_ _ _ _ _ Hm H as Hr Hm′
split ; | exact Hm'
intros lo hi E Hf
exact iv_copy_ _ _ _ _ Hd Hr_ _ E Hf

ext

–destruct narrow_ranget as lo0 hi0 | eqn: Et
+injection H as ← ←
split ; | exact Hm
intros lo hi E Hf
injection E as ← ←
exact iv_narrow_ _ _ _ _ _ Hd Et Hf
+destruct t ; try discriminate Et ; destruct args as | a | a2 args ; try no_answer H Hm
∗destruct Hrec_ _ _ _ _ Hm H as Hr Hm′
split ; | exact Hm'
intros lo hi E Hf
exact iv_sw_ _ _ _ _ Hd Hr_ _ E Hf
∗destruct reca W m as lo0 hi0 | m1 eqn: Er
--destruct Hrec_ _ _ _ _ Hm Er as Hr Hm1
destruct 0 ≤? lo0 eqn: El
++injection H as ← ←
split ; | exact Hm1
intros lo hi E Hf
injection E as ← ←
apply Z.leb_le in El
exact iv_uw_ _ _ _ _ Hd Hr_ _ eq_refl El Hf
++injection H as ← ←
split ; intros lo hi E ; discriminate E | exact Hm1
--injection H as ← ←
destruct Hrec_ _ _ _ _ Hm Er as _ Hm1
split ; intros lo hi E ; discriminate E | exact Hm1

raw_load

–destruct t ; try no_answer H Hm
injection H as ← ←
split ; | exact Hm
intros lo hi E Hf
exact iv_load_ _ _ _ _ _ _ Hd E Hf

Whatever its fuel and depth, from a derived memo, an interval the walk oi (offset_interval/8) answers for v at the class k is derived, and the memo it returns is derived. So the memo and the depth limit need no further thought.

279Lemma oi_sound
∀ fuel v k depth m r m′
memo_okm
oionce fuel v k depth m = r, m′
∀lo hi, r = Somelo, hi → ivv k lo hi ∧ memo_okm′
Proof 45 steps Qed
induction fuel as | f IH ; intros v k depth m r m′ Hm H ; destruct v as n | c | g ; simpl in H
all: try no_answer H Hm
all: try destruct signed_valuek c as x | eqn: Ex ; injection H as ← ← ; split ; intros lo hi E ; injection E as ← ← ; exact iv_const_ _ _ Ex | exact Hm | intros lo hi E ; discriminate E | exact Hm
–destruct memo_lookupn k m as r0 | eqn: Em
+injection H as ← ←
split ; | exact Hm
intros lo hi E
subst r0
exact Hm_ _ _ _ Em
+injection H as ← ←
split ; intros lo hi E ; discriminate E |
apply memo_ok_cons ; exact Hm | intros lo hi E ; discriminate E
–destruct memo_lookupn k m as r0 | eqn: Em
+injection H as ← ←
split ; | exact Hm
intros lo hi E
subst r0
exact Hm_ _ _ _ Em
+assert Hrec : rec_okλv k m ⇒ oionce f v k depth + 1 m by intros a k′ m0 r0 m1 Hm0 E ; exact IH_ _ _ _ _ _ Hm0 E
assert Hres : ∀r0 m0, if depth <? 32 then match lookupn once with SomeDInstLetn′ k′ o args ⇒ if name_eqbn′ n && class_eqbk′ k then match op_intervalλv k m ⇒ oionce f v k depth + 1 m o args k m with Somelo, hi, m1 ⇒ if interval_fitsk lo hi then Somelo, hi, m1 else None, m | None, _ ⇒ None, m end else None, m | _ ⇒ None, m end else None, m = r0, m0 → ∀lo hi, r0 = Somelo, hi → ivTmpn k lo hi ∧ memo_okm0
{intros r0 m0 E
destruct depth <? 32 ; | no_answer E Hm
destruct lookupn once as | ph | i | eqn: El ; try no_answer E Hm
destruct i as n′ k′ o args | | | | | | | | ; try no_answer E Hm
destruct name_eqbn' n && class_eqbk' k eqn: Ek ; | no_answer E Hm
apply andb_true_iff in Ek as Ek1 Ek2
apply class_eqb_true in Ek2
subst k'
assert Hd : definedn k o args by exists n' ; split ; exact El | exact Ek1
destruct op_interval_ o args k m as lo0 hi0 | m1 eqn: Eo ; destruct op_interval_ok_ _ _ _ _ _ _ _ Hrec Hm Hd Eo as Ho Hm1
–destruct interval_fitsk lo0 hi0 eqn: Ef
+injection E as ← ←
split ; | exact Hm1
intros lo hi E
injection E as ← ←
exact Ho_ _ eq_refl Ef
+injection E as ← ←
split ; intros lo hi E ; discriminate E | exact Hm
–injection E as ← ←
split ; intros lo hi E ; discriminate E | exact Hm
match type of H withlet '_, _ ≔ ?x in _ = _⇒destruct x as r0 m0 eqn: Exend
injection H as ← ←
destruct Hres_ _ eq_refl as Hr Hm0
split ; exact Hr |
apply memo_ok_cons ; exact Hm0 | exact Hr

An interval offset_interval (offset_interval/6, as the validator calls it) answers for v at the class k is derived: what oi_sound gives from the empty memo. Chain.v reads the validator's intervals back through it.

337Theorem offset_interval_iv
∀ v k lo hi
offset_intervalonce v k = Somelo, hi
ivv k lo hi
Explore proof 7 tactics

Initial goal

once :
listname × def
⊢
∀v : value k : class lo hi : Z, offset_intervalonce v k = Somelo, hi → ivv k lo hi

intros v k lo hi H

once :
listname × def
v :
value
k :
class
lo, hi :
Z
H :
offset_intervalonce v k = Somelo, hi
⊢
ivv k lo hi

unfold offset_interval in H

once :
listname × def
v :
value
k :
class
lo, hi :
Z
H :
fstoionce 33 v k 0 [ ] = Somelo, hi
⊢
ivv k lo hi

destruct oionce 33 v k 0 [ ] as r m′ eqn: E

once :
listname × def
v :
value
k :
class
lo, hi :
Z
r :
optionZ × Z
m′ :
memo
E :
oionce 33 v k 0 [ ] = r, m′
H :
fstr, m′ = Somelo, hi
⊢
ivv k lo hi

simpl in H

once :
listname × def
v :
value
k :
class
lo, hi :
Z
r :
optionZ × Z
m′ :
memo
E :
oionce 33 v k 0 [ ] = r, m′
H :
r = Somelo, hi
⊢
ivv k lo hi

subst r

once :
listname × def
v :
value
k :
class
lo, hi :
Z
m′ :
memo
E :
oionce 33 v k 0 [ ] = Somelo, hi, m′
⊢
ivv k lo hi

apply oi_sound_ _ _ _ _ _ _ memo_ok_nil E

once :
listname × def
v :
value
k :
class
lo, hi :
Z
m′ :
memo
E :
oionce 33 v k 0 [ ] = Somelo, hi, m′
⊢
Somelo, hi = Somelo, hi

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros v k lo hi H
unfold offset_interval in H
destruct oionce 33 v k 0 [ ] as r m′ eqn: E
simpl in H
subst r
apply oi_sound_ _ _ _ _ _ _ memo_ok_nil E
reflexivity

What an interval means on a run

An interval speaks of the values the names it walks hold. Where each of those names holds what its definition computes from its operands' values, the value an iv derivation reads lies in its interval (iv_sound). Which names hold their definitions at a point of a run is the run-level invariant's to say; here it is a predicate ok closed under operands.

As interp:inst_result/5 of a let: the value of the temporary n in the environment e is what let(tmp(n), k, o, args) computes (interp:alu/4) from its operands' values in e0, the environment it ran in, with ge the global environment. For a narrow load it is some loaded value, extended (interp:extended_res/4).

359Definition let_holdsge : genv e0 e : env n : name k : class o : op args : listvalue : Prop ≔
match o with
RawLoadLdNarrowt _
⇒
∃u x, extendedt k u = Somex ∧ lookupn e = Somex
_
⇒
∃classes xs x, op_arg_classeso k = Someclasses ∧ map2_optionvalue_xge e0 classes args = Somexs ∧ aluo k xs = Somex ∧ lookupn e = Somex

The ops an interval derivation walks through, one per clause of op_interval/9: those whose results let_holds speaks of.

369Definition iv_opo : op : bool ≔
match o with
Ext_ | RawLoadLdNarrow_ _ | Copy | And | Urem | Shl | Mul | Add | Sub
⇒
true
_
⇒
false

What an interval means of a value: the operand v, read at the integer class k in the environment e (ge the global environment), is some x from lo to hi, modulo the class's width.

378Definition in_ivge : genv e : env k : class v : value lo hi : Z : Prop ≔
∃bits u x, class_bitsk = Somebits ∧ value_xge e k v = SomeWIntu ∧ lo ≤ x ≤ hi ∧ u = x mod 2 ^ bits

Arithmetic

An interval that fits the class k (interval_fits) is of an integer class: k has a bit width bits, and its modulus is 2^bits, which is positive.

387Lemma fits_bits
∀ k lo hi
interval_fitsk lo hi = true
∃bits, class_bitsk = Somebits ∧ modulusk = Some2 ^ bits ∧ 0 < 2 ^ bits
Explore proof 2 tactics

Initial goal

once :
listname × def
⊢
∀k : class lo hi : Z, interval_fitsk lo hi = true → ∃bits : Z, class_bitsk = Somebits ∧ modulusk = Some2 ^ bits ∧ 0 < 2 ^ bits

intros k lo hi H

once :
listname × def
k :
class
lo, hi :
Z
H :
interval_fitsk lo hi = true
⊢
∃bits : Z, class_bitsk = Somebits ∧ modulusk = Some2 ^ bits ∧ 0 < 2 ^ bits

destruct k ; try discriminate H ; eexists ; split ; reflexivity | split ; reflexivity | lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros k lo hi H
destruct k ; try discriminate H ; eexists ; split ; reflexivity | split ; reflexivity | lia

The signed value x of the constant c at a class of width bits (signed_value) is congruent to c modulo 2^bits and lies in the signed range of that width.

394Lemma signed_value_mod
∀ k c x bits
signed_valuek c = Somex
class_bitsk = Somebits
x mod 2 ^ bits = c mod 2 ^ bits ∧ −2 ^ bits − 1 ≤ x < 2 ^ bits − 1
Explore proof 15 tactics

Initial goal

once :
listname × def
⊢
∀k : class c x bits : Z, signed_valuek c = Somex → class_bitsk = Somebits → x mod 2 ^ bits = c mod 2 ^ bits ∧ −2 ^ bits − 1 ≤ x < 2 ^ bits − 1

intros k c x bits H Hb

once :
listname × def
k :
class
c, x, bits :
Z
H :
signed_valuek c = Somex
Hb :
class_bitsk = Somebits
⊢
x mod 2 ^ bits = c mod 2 ^ bits ∧ −2 ^ bits − 1 ≤ x < 2 ^ bits − 1

unfold signed_value in H

once :
listname × def
k :
class
c, x, bits :
Z
H :
let* bits ≔ class_bitsk in
Some
2 ^ bits − 1 ≤? c mod 2 ^ bits
→
c mod 2 ^ bits − 2 ^ bits
else
c mod 2 ^ bits
=
Somex
Hb :
class_bitsk = Somebits
⊢
x mod 2 ^ bits = c mod 2 ^ bits ∧ −2 ^ bits − 1 ≤ x < 2 ^ bits − 1

rewrite Hb in H

once :
listname × def
k :
class
c, x, bits :
Z
H :
Some
2 ^ bits − 1 ≤? c mod 2 ^ bits
→
c mod 2 ^ bits − 2 ^ bits
else
c mod 2 ^ bits
=
Somex
Hb :
class_bitsk = Somebits
⊢
x mod 2 ^ bits = c mod 2 ^ bits ∧ −2 ^ bits − 1 ≤ x < 2 ^ bits − 1

simpl in H

once :
listname × def
k :
class
c, x, bits :
Z
H :
Some
2 ^ bits − 1 ≤? c mod 2 ^ bits
→
c mod 2 ^ bits − 2 ^ bits
else
c mod 2 ^ bits
=
Somex
Hb :
class_bitsk = Somebits
⊢
x mod 2 ^ bits = c mod 2 ^ bits ∧ −2 ^ bits − 1 ≤ x < 2 ^ bits − 1

injection H as ←

once :
listname × def
k :
class
c, bits :
Z
Hb :
class_bitsk = Somebits
⊢
2 ^ bits − 1 ≤? c mod 2 ^ bits
→
c mod 2 ^ bits − 2 ^ bits
else
c mod 2 ^ bits
mod
2 ^ bits
=
c mod 2 ^ bits
∧
−2 ^ bits − 1 ≤ if 2 ^ bits − 1 ≤? c mod 2 ^ bits then c mod 2 ^ bits − 2 ^ bits else c mod 2 ^ bits < 2 ^ bits − 1

assert Hp : 2 ^ bits = 2 × 2 ^ bits − 1 ∧ 0 < 2 ^ bits − 1

2 open

once :
listname × def
k :
class
c, bits :
Z
Hb :
class_bitsk = Somebits
⊢
2 ^ bits = 2 × 2 ^ bits − 1 ∧ 0 < 2 ^ bits − 1
focused goal
once :
listname × def
k :
class
c, bits :
Z
Hb :
class_bitsk = Somebits
Hp :
2 ^ bits = 2 × 2 ^ bits − 1 ∧ 0 < 2 ^ bits − 1
⊢
2 ^ bits − 1 ≤? c mod 2 ^ bits
→
c mod 2 ^ bits − 2 ^ bits
else
c mod 2 ^ bits
mod
2 ^ bits
=
c mod 2 ^ bits
∧
−2 ^ bits − 1 ≤ if 2 ^ bits − 1 ≤? c mod 2 ^ bits then c mod 2 ^ bits − 2 ^ bits else c mod 2 ^ bits < 2 ^ bits − 1

{destruct k ; try discriminate Hb ; injection Hb as ← ; simpl ; lia

deferred goal
once :
listname × def
k :
class
c, bits :
Z
Hb :
class_bitsk = Somebits
Hp :
2 ^ bits = 2 × 2 ^ bits − 1 ∧ 0 < 2 ^ bits − 1
⊢
2 ^ bits − 1 ≤? c mod 2 ^ bits
→
c mod 2 ^ bits − 2 ^ bits
else
c mod 2 ^ bits
mod
2 ^ bits
=
c mod 2 ^ bits
∧
−2 ^ bits − 1 ≤ if 2 ^ bits − 1 ≤? c mod 2 ^ bits then c mod 2 ^ bits − 2 ^ bits else c mod 2 ^ bits < 2 ^ bits − 1

pose proof Z.mod_pos_boundc 2 ^ bits ltac:lia

once :
listname × def
k :
class
c, bits :
Z
Hb :
class_bitsk = Somebits
Hp :
2 ^ bits = 2 × 2 ^ bits − 1 ∧ 0 < 2 ^ bits − 1
H :
0 ≤ c mod 2 ^ bits < 2 ^ bits
⊢
2 ^ bits − 1 ≤? c mod 2 ^ bits
→
c mod 2 ^ bits − 2 ^ bits
else
c mod 2 ^ bits
mod
2 ^ bits
=
c mod 2 ^ bits
∧
−2 ^ bits − 1 ≤ if 2 ^ bits − 1 ≤? c mod 2 ^ bits then c mod 2 ^ bits − 2 ^ bits else c mod 2 ^ bits < 2 ^ bits − 1

destruct 2 ^ bits − 1 ≤? c mod 2 ^ bits eqn: E ; apply Z.leb_le in E | apply Z.leb_gt in E ; split ; try lia

2 open

once :
listname × def
k :
class
c, bits :
Z
Hb :
class_bitsk = Somebits
Hp :
2 ^ bits = 2 × 2 ^ bits − 1 ∧ 0 < 2 ^ bits − 1
H :
0 ≤ c mod 2 ^ bits < 2 ^ bits
E :
2 ^ bits − 1 ≤ c mod 2 ^ bits
⊢
c mod 2 ^ bits − 2 ^ bits mod 2 ^ bits = c mod 2 ^ bits
focused goal
once :
listname × def
k :
class
c, bits :
Z
Hb :
class_bitsk = Somebits
Hp :
2 ^ bits = 2 × 2 ^ bits − 1 ∧ 0 < 2 ^ bits − 1
H :
0 ≤ c mod 2 ^ bits < 2 ^ bits
E :
c mod 2 ^ bits < 2 ^ bits − 1
⊢
c mod 2 ^ bits mod 2 ^ bits = c mod 2 ^ bits

–replace c mod 2 ^ bits − 2 ^ bits with c mod 2 ^ bits + −1 × 2 ^ bits by lia

2 open

once :
listname × def
k :
class
c, bits :
Z
Hb :
class_bitsk = Somebits
Hp :
2 ^ bits = 2 × 2 ^ bits − 1 ∧ 0 < 2 ^ bits − 1
H :
0 ≤ c mod 2 ^ bits < 2 ^ bits
E :
2 ^ bits − 1 ≤ c mod 2 ^ bits
⊢
c mod 2 ^ bits + −1 × 2 ^ bits mod 2 ^ bits = c mod 2 ^ bits
deferred goal
once :
listname × def
k :
class
c, bits :
Z
Hb :
class_bitsk = Somebits
Hp :
2 ^ bits = 2 × 2 ^ bits − 1 ∧ 0 < 2 ^ bits − 1
H :
0 ≤ c mod 2 ^ bits < 2 ^ bits
E :
c mod 2 ^ bits < 2 ^ bits − 1
⊢
c mod 2 ^ bits mod 2 ^ bits = c mod 2 ^ bits

rewrite Z.mod_add by lia

2 open

once :
listname × def
k :
class
c, bits :
Z
Hb :
class_bitsk = Somebits
Hp :
2 ^ bits = 2 × 2 ^ bits − 1 ∧ 0 < 2 ^ bits − 1
H :
0 ≤ c mod 2 ^ bits < 2 ^ bits
E :
2 ^ bits − 1 ≤ c mod 2 ^ bits
⊢
c mod 2 ^ bits mod 2 ^ bits = c mod 2 ^ bits
deferred goal
once :
listname × def
k :
class
c, bits :
Z
Hb :
class_bitsk = Somebits
Hp :
2 ^ bits = 2 × 2 ^ bits − 1 ∧ 0 < 2 ^ bits − 1
H :
0 ≤ c mod 2 ^ bits < 2 ^ bits
E :
c mod 2 ^ bits < 2 ^ bits − 1
⊢
c mod 2 ^ bits mod 2 ^ bits = c mod 2 ^ bits

apply Z.mod_mod

2 open

once :
listname × def
k :
class
c, bits :
Z
Hb :
class_bitsk = Somebits
Hp :
2 ^ bits = 2 × 2 ^ bits − 1 ∧ 0 < 2 ^ bits − 1
H :
0 ≤ c mod 2 ^ bits < 2 ^ bits
E :
2 ^ bits − 1 ≤ c mod 2 ^ bits
⊢
2 ^ bits ≠ 0
deferred goal
once :
listname × def
k :
class
c, bits :
Z
Hb :
class_bitsk = Somebits
Hp :
2 ^ bits = 2 × 2 ^ bits − 1 ∧ 0 < 2 ^ bits − 1
H :
0 ≤ c mod 2 ^ bits < 2 ^ bits
E :
c mod 2 ^ bits < 2 ^ bits − 1
⊢
c mod 2 ^ bits mod 2 ^ bits = c mod 2 ^ bits

lia

deferred goal
once :
listname × def
k :
class
c, bits :
Z
Hb :
class_bitsk = Somebits
Hp :
2 ^ bits = 2 × 2 ^ bits − 1 ∧ 0 < 2 ^ bits − 1
H :
0 ≤ c mod 2 ^ bits < 2 ^ bits
E :
c mod 2 ^ bits < 2 ^ bits − 1
⊢
c mod 2 ^ bits mod 2 ^ bits = c mod 2 ^ bits

–apply Z.mod_mod

once :
listname × def
k :
class
c, bits :
Z
Hb :
class_bitsk = Somebits
Hp :
2 ^ bits = 2 × 2 ^ bits − 1 ∧ 0 < 2 ^ bits − 1
H :
0 ≤ c mod 2 ^ bits < 2 ^ bits
E :
c mod 2 ^ bits < 2 ^ bits − 1
⊢
2 ^ bits ≠ 0

lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros k c x bits H Hb
unfold signed_value in H
rewrite Hb in H
simpl in H
injection H as ←
assert Hp : 2 ^ bits = 2 × 2 ^ bits − 1 ∧ 0 < 2 ^ bits − 1
{destruct k ; try discriminate Hb ; injection Hb as ← ; simpl ; lia
pose proof Z.mod_pos_boundc 2 ^ bits ltac:lia
destruct 2 ^ bits − 1 ≤? c mod 2 ^ bits eqn: E ; apply Z.leb_le in E | apply Z.leb_gt in E ; split ; try lia
–replace c mod 2 ^ bits − 2 ^ bits with c mod 2 ^ bits + −1 × 2 ^ bits by lia
rewrite Z.mod_add by lia
apply Z.mod_mod
lia
–apply Z.mod_mod
lia

A constant's signed value fits its class (interval_fits) as an interval of one point.

409Lemma signed_value_fits
∀ k c x
signed_valuek c = Somex
interval_fitsk x x = true
Explore proof 6 tactics

Initial goal

once :
listname × def
⊢
∀k : class c x : Z, signed_valuek c = Somex → interval_fitsk x x = true

intros k c x H

once :
listname × def
k :
class
c, x :
Z
H :
signed_valuek c = Somex
⊢
interval_fitsk x x = true

destruct k ; try unfold signed_value in H ; discriminate H ; | reflexivity

once :
listname × def
c, x :
Z
H :
signed_valueW c = Somex
⊢
interval_fitsW x x = true

destruct signed_value_mod_ _ _ _ H eq_refl as _ Hr

once :
listname × def
c, x :
Z
H :
signed_valueW c = Somex
Hr :
−2 ^ 32 − 1 ≤ x < 2 ^ 32 − 1
⊢
interval_fitsW x x = true

simpl

once :
listname × def
c, x :
Z
H :
signed_valueW c = Somex
Hr :
−2 ^ 32 − 1 ≤ x < 2 ^ 32 − 1
⊢
−2147483648 ≤? x && x ≤? 2147483647 = true

apply andb_true_iff

once :
listname × def
c, x :
Z
H :
signed_valueW c = Somex
Hr :
−2 ^ 32 − 1 ≤ x < 2 ^ 32 − 1
⊢
−2147483648 ≤? x = true ∧ x ≤? 2147483647 = true

split ; apply Z.leb_le | apply Z.leb_le ; lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros k c x H
destruct k ; try unfold signed_value in H ; discriminate H ; | reflexivity
destruct signed_value_mod_ _ _ _ H eq_refl as _ Hr
simpl
apply andb_true_iff
split ; apply Z.leb_le | apply Z.leb_le ; lia

Every interval derived (iv) fits its class (interval_fits).

417Lemma iv_fits
∀ v k lo hi
ivv k lo hi
interval_fitsk lo hi = true
Explore proof 3 tactics

Initial goal

once :
listname × def
⊢
∀v : value k : class lo hi : Z, ivv k lo hi → interval_fitsk lo hi = true

intros v k lo hi H

once :
listname × def
v :
value
k :
class
lo, hi :
Z
H :
ivv k lo hi
⊢
interval_fitsk lo hi = true

destruct H ; try assumption

once :
listname × def
c :
Z
k :
class
x :
Z
H :
signed_valuek c = Somex
⊢
interval_fitsk x x = true

exact signed_value_fits_ _ _ H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros v k lo hi H
destruct H ; try assumption
exact signed_value_fits_ _ _ H

Sign-extending u from the modulus m = 2h (sign_extension) gives at least -h and less than h.

422Lemma sign_extension_range
∀ m h u
0 < h
m = 2 × h
−h ≤ sign_extensionm h u < h
Explore proof 4 tactics

Initial goal

once :
listname × def
⊢
∀m h u : Z, 0 < h → m = 2 × h → −h ≤ sign_extensionm h u < h

intros m h u Hh Hm

once :
listname × def
m, h, u :
Z
Hh :
0 < h
Hm :
m = 2 × h
⊢
−h ≤ sign_extensionm h u < h

unfold sign_extension

once :
listname × def
m, h, u :
Z
Hh :
0 < h
Hm :
m = 2 × h
⊢
−h ≤ if h ≤? u mod m then u mod m − m else u mod m < h

pose proof Z.mod_pos_boundu m ltac:lia

once :
listname × def
m, h, u :
Z
Hh :
0 < h
Hm :
m = 2 × h
H :
0 ≤ u mod m < m
⊢
−h ≤ if h ≤? u mod m then u mod m − m else u mod m < h

destruct h ≤? u mod m eqn: E ; apply Z.leb_le in E | apply Z.leb_gt in E ; lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m h u Hh Hm
unfold sign_extension
pose proof Z.mod_pos_boundu m ltac:lia
destruct h ≤? u mod m eqn: E ; apply Z.leb_le in E | apply Z.leb_gt in E ; lia

Any x extended from the narrow type t (extension) lies in t's range (narrow_range), so a narrow ext or load is bounded whatever it reads.

431Lemma narrow_extension
∀ t lo hi x
narrow_ranget = Somelo, hi
lo ≤ extensiont x ≤ hi
Explore proof 10 tactics

Initial goal

once :
listname × def
⊢
∀t : narrow lo hi x : Z, narrow_ranget = Somelo, hi → lo ≤ extensiont x ≤ hi

intros t lo hi x H

once :
listname × def
t :
narrow
lo, hi, x :
Z
H :
narrow_ranget = Somelo, hi
⊢
lo ≤ extensiont x ≤ hi

destruct t ; simpl in H ; try discriminate H ; injection H as ← ← ; simpl

4 open

once :
listname × def
x :
Z
⊢
−32768 ≤ sign_extension65536 32768 x ≤ 32767
focused goal
once :
listname × def
x :
Z
⊢
0 ≤ x mod 65536 ≤ 65535
focused goal
once :
listname × def
x :
Z
⊢
−128 ≤ sign_extension256 128 x ≤ 127
focused goal
once :
listname × def
x :
Z
⊢
0 ≤ x mod 256 ≤ 255

–pose proof sign_extension_range65536 32768 x ltac:lia ltac:lia

4 open

once :
listname × def
x :
Z
H :
−32768 ≤ sign_extension65536 32768 x < 32768
⊢
−32768 ≤ sign_extension65536 32768 x ≤ 32767
deferred goal
once :
listname × def
x :
Z
⊢
0 ≤ x mod 65536 ≤ 65535
deferred goal
once :
listname × def
x :
Z
⊢
−128 ≤ sign_extension256 128 x ≤ 127
deferred goal
once :
listname × def
x :
Z
⊢
0 ≤ x mod 256 ≤ 255

lia

3 open

deferred goal
once :
listname × def
x :
Z
⊢
0 ≤ x mod 65536 ≤ 65535
deferred goal
once :
listname × def
x :
Z
⊢
−128 ≤ sign_extension256 128 x ≤ 127
deferred goal
once :
listname × def
x :
Z
⊢
0 ≤ x mod 256 ≤ 255

–pose proof Z.mod_pos_boundx 65536 ltac:lia

3 open

once :
listname × def
x :
Z
H :
0 ≤ x mod 65536 < 65536
⊢
0 ≤ x mod 65536 ≤ 65535
deferred goal
once :
listname × def
x :
Z
⊢
−128 ≤ sign_extension256 128 x ≤ 127
deferred goal
once :
listname × def
x :
Z
⊢
0 ≤ x mod 256 ≤ 255

lia

2 open

deferred goal
once :
listname × def
x :
Z
⊢
−128 ≤ sign_extension256 128 x ≤ 127
deferred goal
once :
listname × def
x :
Z
⊢
0 ≤ x mod 256 ≤ 255

–pose proof sign_extension_range256 128 x ltac:lia ltac:lia

2 open

once :
listname × def
x :
Z
H :
−128 ≤ sign_extension256 128 x < 128
⊢
−128 ≤ sign_extension256 128 x ≤ 127
deferred goal
once :
listname × def
x :
Z
⊢
0 ≤ x mod 256 ≤ 255

lia

deferred goal
once :
listname × def
x :
Z
⊢
0 ≤ x mod 256 ≤ 255

–pose proof Z.mod_pos_boundx 256 ltac:lia

once :
listname × def
x :
Z
H :
0 ≤ x mod 256 < 256
⊢
0 ≤ x mod 256 ≤ 255

lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros t lo hi x H
destruct t ; simpl in H ; try discriminate H ; injection H as ← ← ; simpl
–pose proof sign_extension_range65536 32768 x ltac:lia ltac:lia
lia
–pose proof Z.mod_pos_boundx 65536 ltac:lia
lia
–pose proof sign_extension_range256 128 x ltac:lia ltac:lia
lia
–pose proof Z.mod_pos_boundx 256 ltac:lia
lia

A sign-extended word is the signed value it holds: a signed 32-bit x, taken modulo 2^32 and sign-extended, is x again.

442Lemma sign_extension_mod
∀ x
−2 ^ 31 ≤ x < 2 ^ 31
sign_extension2 ^ 32 2 ^ 31 x mod 2 ^ 32 = x
Explore proof 11 tactics

Initial goal

once :
listname × def
⊢
∀x : Z, −2 ^ 31 ≤ x < 2 ^ 31 → sign_extension2 ^ 32 2 ^ 31 x mod 2 ^ 32 = x

intros x Hx

once :
listname × def
x :
Z
Hx :
−2 ^ 31 ≤ x < 2 ^ 31
⊢
sign_extension2 ^ 32 2 ^ 31 x mod 2 ^ 32 = x

unfold sign_extension

once :
listname × def
x :
Z
Hx :
−2 ^ 31 ≤ x < 2 ^ 31
⊢
2 ^ 31 ≤? x mod 2 ^ 32 mod 2 ^ 32
→
x mod 2 ^ 32 mod 2 ^ 32 − 2 ^ 32
else
x mod 2 ^ 32 mod 2 ^ 32
=
x

rewrite Z.mod_mod by lia

once :
listname × def
x :
Z
Hx :
−2 ^ 31 ≤ x < 2 ^ 31
⊢
2 ^ 31 ≤? x mod 2 ^ 32
→
x mod 2 ^ 32 − 2 ^ 32
else
x mod 2 ^ 32
=
x

destruct Z_lt_le_decx 0

2 open

once :
listname × def
x :
Z
Hx :
−2 ^ 31 ≤ x < 2 ^ 31
l :
x < 0
⊢
2 ^ 31 ≤? x mod 2 ^ 32
→
x mod 2 ^ 32 − 2 ^ 32
else
x mod 2 ^ 32
=
x
focused goal
once :
listname × def
x :
Z
Hx :
−2 ^ 31 ≤ x < 2 ^ 31
l :
0 ≤ x
⊢
2 ^ 31 ≤? x mod 2 ^ 32
→
x mod 2 ^ 32 − 2 ^ 32
else
x mod 2 ^ 32
=
x

–replace x mod 2 ^ 32 with x + 2 ^ 32

3 open

once :
listname × def
x :
Z
Hx :
−2 ^ 31 ≤ x < 2 ^ 31
l :
x < 0
⊢
2 ^ 31 ≤? x + 2 ^ 32
→
x + 2 ^ 32 − 2 ^ 32
else
x + 2 ^ 32
=
x
focused goal
once :
listname × def
x :
Z
Hx :
−2 ^ 31 ≤ x < 2 ^ 31
l :
x < 0
⊢
x + 2 ^ 32 = x mod 2 ^ 32
deferred goal
once :
listname × def
x :
Z
Hx :
−2 ^ 31 ≤ x < 2 ^ 31
l :
0 ≤ x
⊢
2 ^ 31 ≤? x mod 2 ^ 32
→
x mod 2 ^ 32 − 2 ^ 32
else
x mod 2 ^ 32
=
x

+rewrite proj2Z.leb_le_ _ by lia

3 open

once :
listname × def
x :
Z
Hx :
−2 ^ 31 ≤ x < 2 ^ 31
l :
x < 0
⊢
x + 2 ^ 32 − 2 ^ 32 = x
deferred goal
once :
listname × def
x :
Z
Hx :
−2 ^ 31 ≤ x < 2 ^ 31
l :
x < 0
⊢
x + 2 ^ 32 = x mod 2 ^ 32
deferred goal
once :
listname × def
x :
Z
Hx :
−2 ^ 31 ≤ x < 2 ^ 31
l :
0 ≤ x
⊢
2 ^ 31 ≤? x mod 2 ^ 32
→
x mod 2 ^ 32 − 2 ^ 32
else
x mod 2 ^ 32
=
x

lia

2 open

deferred goal
once :
listname × def
x :
Z
Hx :
−2 ^ 31 ≤ x < 2 ^ 31
l :
x < 0
⊢
x + 2 ^ 32 = x mod 2 ^ 32
deferred goal
once :
listname × def
x :
Z
Hx :
−2 ^ 31 ≤ x < 2 ^ 31
l :
0 ≤ x
⊢
2 ^ 31 ≤? x mod 2 ^ 32
→
x mod 2 ^ 32 − 2 ^ 32
else
x mod 2 ^ 32
=
x

+apply Z.mod_unique with −1 ; lia

deferred goal
once :
listname × def
x :
Z
Hx :
−2 ^ 31 ≤ x < 2 ^ 31
l :
0 ≤ x
⊢
2 ^ 31 ≤? x mod 2 ^ 32
→
x mod 2 ^ 32 − 2 ^ 32
else
x mod 2 ^ 32
=
x

–rewrite Z.mod_small by lia

once :
listname × def
x :
Z
Hx :
−2 ^ 31 ≤ x < 2 ^ 31
l :
0 ≤ x
⊢
2 ^ 31 ≤? x
→
x − 2 ^ 32
else
x
=
x

rewrite proj2Z.leb_gt_ _ by lia

once :
listname × def
x :
Z
Hx :
−2 ^ 31 ≤ x < 2 ^ 31
l :
0 ≤ x
⊢
x = x

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros x Hx
unfold sign_extension
rewrite Z.mod_mod by lia
destruct Z_lt_le_decx 0
–replace x mod 2 ^ 32 with x + 2 ^ 32
+rewrite proj2Z.leb_le_ _ by lia
lia
+apply Z.mod_unique with −1 ; lia
–rewrite Z.mod_small by lia
rewrite proj2Z.leb_gt_ _ by lia
reflexivity

The bitwise and of two nonnegative integers x and y lies from 0 to y: a nonnegative mask bounds an and.

455Lemma land_le
∀ x y
0 ≤ x
0 ≤ y
0 ≤ Z.landx y ≤ y
Explore proof 7 tactics

Initial goal

once :
listname × def
⊢
∀x y : Z, 0 ≤ x → 0 ≤ y → 0 ≤ Z.landx y ≤ y

intros x y Hx Hy

once :
listname × def
x, y :
Z
Hx :
0 ≤ x
Hy :
0 ≤ y
⊢
0 ≤ Z.landx y ≤ y

split ; apply Z.land_nonneg ; auto |

once :
listname × def
x, y :
Z
Hx :
0 ≤ x
Hy :
0 ≤ y
⊢
Z.landx y ≤ y

apply Z.ldiff_le_ _ Hy

once :
listname × def
x, y :
Z
Hx :
0 ≤ x
Hy :
0 ≤ y
⊢
Z.ldiffZ.landx y y = 0

apply Z.bits_inj'

once :
listname × def
x, y :
Z
Hx :
0 ≤ x
Hy :
0 ≤ y
⊢
∀n : Z, 0 ≤ n → Z.testbitZ.ldiffZ.landx y y n = Z.testbit0 n

intros i Hi

once :
listname × def
x, y :
Z
Hx :
0 ≤ x
Hy :
0 ≤ y
i :
Z
Hi :
0 ≤ i
⊢
Z.testbitZ.ldiffZ.landx y y i = Z.testbit0 i

rewrite Z.ldiff_spec , Z.land_spec , Z.bits_0

once :
listname × def
x, y :
Z
Hx :
0 ≤ x
Hy :
0 ≤ y
i :
Z
Hi :
0 ≤ i
⊢
Z.testbitx i && Z.testbity i && negbZ.testbity i = false

destruct Z.testbitx i , Z.testbity i ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros x y Hx Hy
split ; apply Z.land_nonneg ; auto |
apply Z.ldiff_le_ _ Hy
apply Z.bits_inj'
intros i Hi
rewrite Z.ldiff_spec , Z.land_spec , Z.bits_0
destruct Z.testbitx i , Z.testbity i ; reflexivity

A temporary n holding the integer w, read at an integer class of width bits, reads as w modulo 2^bits.

464Lemma read_tmp
∀ ge e k n w bits
class_bitsk = Somebits
lookupn e = SomeWIntw
value_xge e k Tmpn = SomeWIntw mod 2 ^ bits
Explore proof 4 tactics

Initial goal

once :
listname × def
⊢
∀ge : genv e : listname × word k : class n : name w bits : Z, class_bitsk = Somebits → lookupn e = SomeWIntw → value_xge e k Tmpn = SomeWIntw mod 2 ^ bits

intros ge e k n w bits Hb H

once :
listname × def
ge :
genv
e :
listname × word
k :
class
n :
name
w, bits :
Z
Hb :
class_bitsk = Somebits
H :
lookupn e = SomeWIntw
⊢
value_xge e k Tmpn = SomeWIntw mod 2 ^ bits

simpl

once :
listname × def
ge :
genv
e :
listname × word
k :
class
n :
name
w, bits :
Z
Hb :
class_bitsk = Somebits
H :
lookupn e = SomeWIntw
⊢
let* x ≔ lookupn e in
word_at_classk x
=
SomeWIntw mod 2 ^ bits

rewrite H

once :
listname × def
ge :
genv
e :
listname × word
k :
class
n :
name
w, bits :
Z
Hb :
class_bitsk = Somebits
H :
lookupn e = SomeWIntw
⊢
word_at_classk WIntw = SomeWIntw mod 2 ^ bits

destruct k ; try discriminate Hb ; injection Hb as ← ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros ge e k n w bits Hb H
simpl
rewrite H
destruct k ; try discriminate Hb ; injection Hb as ← ; reflexivity

Any operand that reads as an integer u at an integer class of width bits has u at least 0 and below 2^bits.

470Lemma value_int_range
∀ ge e k v u bits
class_bitsk = Somebits
value_xge e k v = SomeWIntu
0 ≤ u < 2 ^ bits
Explore proof 5 tactics

Initial goal

once :
listname × def
⊢
∀ge : genv e : env k : class v : value u bits : Z, class_bitsk = Somebits → value_xge e k v = SomeWIntu → 0 ≤ u < 2 ^ bits

intros ge e k v u bits Hb H

once :
listname × def
ge :
genv
e :
env
k :
class
v :
value
u, bits :
Z
Hb :
class_bitsk = Somebits
H :
value_xge e k v = SomeWIntu
⊢
0 ≤ u < 2 ^ bits

destruct k ; try discriminate Hb ; injection Hb as ← ; destruct v as n | c | g ; simpl in H

6 open

once :
listname × def
ge :
genv
e :
env
n :
name
u :
Z
H :
match lookupn e with
SomeWIntn
⇒
SomeWIntn mod Z.pow_pos2 32
_
⇒
None
=
SomeWIntu
⊢
0 ≤ u < 2 ^ 32
focused goal
once :
listname × def
ge :
genv
e :
env
c, u :
Z
H :
SomeWIntc mod Z.pow_pos2 32 = SomeWIntu
⊢
0 ≤ u < 2 ^ 32
focused goal
once :
listname × def
ge :
genv
e :
env
g :
name
u :
Z
H :
match lookupg ge_globalsge with
Somep
⇒
SomeWPtrp
None
⇒
SomeWPtrptr_addr ≔ 0; ptr_cap ≔ Externalg
=
SomeWIntu
⊢
0 ≤ u < 2 ^ 32
focused goal
once :
listname × def
ge :
genv
e :
env
n :
name
u :
Z
H :
match lookupn e with
SomeWIntn
⇒
SomeWIntn mod Z.pow_pos2 64
SomeWLimit_ _ as x
⇒
Somex
_
⇒
None
=
SomeWIntu
⊢
0 ≤ u < 2 ^ 64
focused goal
once :
listname × def
ge :
genv
e :
env
c, u :
Z
H :
SomeWIntc mod Z.pow_pos2 64 = SomeWIntu
⊢
0 ≤ u < 2 ^ 64
focused goal
once :
listname × def
ge :
genv
e :
env
g :
name
u :
Z
H :
match lookupg ge_globalsge with
Somep
⇒
SomeWPtrp
None
⇒
SomeWPtrptr_addr ≔ 0; ptr_cap ≔ Externalg
=
SomeWIntu
⊢
0 ≤ u < 2 ^ 64

all: try destruct lookupn e as w | | | ; simpl in H ; try discriminate H ; injection H as ← ; apply Z.mod_pos_bound ; lia

4 open

once :
listname × def
ge :
genv
e :
env
c, u :
Z
H :
SomeWIntc mod Z.pow_pos2 32 = SomeWIntu
⊢
0 ≤ u < 2 ^ 32
focused goal
once :
listname × def
ge :
genv
e :
env
g :
name
u :
Z
H :
match lookupg ge_globalsge with
Somep
⇒
SomeWPtrp
None
⇒
SomeWPtrptr_addr ≔ 0; ptr_cap ≔ Externalg
=
SomeWIntu
⊢
0 ≤ u < 2 ^ 32
focused goal
once :
listname × def
ge :
genv
e :
env
c, u :
Z
H :
SomeWIntc mod Z.pow_pos2 64 = SomeWIntu
⊢
0 ≤ u < 2 ^ 64
focused goal
once :
listname × def
ge :
genv
e :
env
g :
name
u :
Z
H :
match lookupg ge_globalsge with
Somep
⇒
SomeWPtrp
None
⇒
SomeWPtrptr_addr ≔ 0; ptr_cap ≔ Externalg
=
SomeWIntu
⊢
0 ≤ u < 2 ^ 64

all: try injection H as ← ; apply Z.mod_pos_bound ; lia

2 open

once :
listname × def
ge :
genv
e :
env
g :
name
u :
Z
H :
match lookupg ge_globalsge with
Somep
⇒
SomeWPtrp
None
⇒
SomeWPtrptr_addr ≔ 0; ptr_cap ≔ Externalg
=
SomeWIntu
⊢
0 ≤ u < 2 ^ 32
focused goal
once :
listname × def
ge :
genv
e :
env
g :
name
u :
Z
H :
match lookupg ge_globalsge with
Somep
⇒
SomeWPtrp
None
⇒
SomeWPtrptr_addr ≔ 0; ptr_cap ≔ Externalg
=
SomeWIntu
⊢
0 ≤ u < 2 ^ 64

all: destruct lookupg ge_globalsge ; discriminate H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros ge e k v u bits Hb H
destruct k ; try discriminate Hb ; injection Hb as ← ; destruct v as n | c | g ; simpl in H
all: try destruct lookupn e as w | | | ; simpl in H ; try discriminate H ; injection H as ← ; apply Z.mod_pos_bound ; lia
all: try injection H as ← ; apply Z.mod_pos_bound ; lia
all: destruct lookupg ge_globalsge ; discriminate H

A temporary n holding w lies in the interval from lo to hi (in_iv) when some x in it is congruent to w modulo the class's width.

483Lemma in_iv_tmp
∀ ge e k n w bits x lo hi
class_bitsk = Somebits
lookupn e = SomeWIntw
w mod 2 ^ bits = x mod 2 ^ bits
lo ≤ x ≤ hi
in_ivge e k Tmpn lo hi
Explore proof 4 tactics

Initial goal

once :
listname × def
⊢
∀ge : genv e : listname × word k : class n : name w bits x lo hi : Z, class_bitsk = Somebits → lookupn e = SomeWIntw → w mod 2 ^ bits = x mod 2 ^ bits → lo ≤ x ≤ hi → in_ivge e k Tmpn lo hi

intros ge e k n w bits x lo hi Hb H Hw Hx

once :
listname × def
ge :
genv
e :
listname × word
k :
class
n :
name
w, bits, x, lo, hi :
Z
Hb :
class_bitsk = Somebits
H :
lookupn e = SomeWIntw
Hw :
w mod 2 ^ bits = x mod 2 ^ bits
Hx :
lo ≤ x ≤ hi
⊢
in_ivge e k Tmpn lo hi

exists bits, w mod 2 ^ bits, x

once :
listname × def
ge :
genv
e :
listname × word
k :
class
n :
name
w, bits, x, lo, hi :
Z
Hb :
class_bitsk = Somebits
H :
lookupn e = SomeWIntw
Hw :
w mod 2 ^ bits = x mod 2 ^ bits
Hx :
lo ≤ x ≤ hi
⊢
class_bitsk = Somebits ∧ value_xge e k Tmpn = SomeWIntw mod 2 ^ bits ∧ lo ≤ x ≤ hi ∧ w mod 2 ^ bits = x mod 2 ^ bits

rewrite read_tmp_ _ _ _ _ _ Hb H

once :
listname × def
ge :
genv
e :
listname × word
k :
class
n :
name
w, bits, x, lo, hi :
Z
Hb :
class_bitsk = Somebits
H :
lookupn e = SomeWIntw
Hw :
w mod 2 ^ bits = x mod 2 ^ bits
Hx :
lo ≤ x ≤ hi
⊢
class_bitsk = Somebits ∧ SomeWIntw mod 2 ^ bits = SomeWIntw mod 2 ^ bits ∧ lo ≤ x ≤ hi ∧ w mod 2 ^ bits = x mod 2 ^ bits

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros ge e k n w bits x lo hi Hb H Hw Hx
exists bits, w mod 2 ^ bits, x
rewrite read_tmp_ _ _ _ _ _ Hb H
auto

A constant c read at an integer class of width bits reads as c modulo 2^bits.

490Lemma const_read
∀ ge e k c bits
class_bitsk = Somebits
value_xge e k Constc = SomeWIntc mod 2 ^ bits
Explore proof 2 tactics

Initial goal

once :
listname × def
⊢
∀ge : genv e : env k : class c bits : Z, class_bitsk = Somebits → value_xge e k Constc = SomeWIntc mod 2 ^ bits

intros ge e k c bits Hb

once :
listname × def
ge :
genv
e :
env
k :
class
c, bits :
Z
Hb :
class_bitsk = Somebits
⊢
value_xge e k Constc = SomeWIntc mod 2 ^ bits

destruct k ; try discriminate Hb ; injection Hb as ← ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros ge e k c bits Hb
destruct k ; try discriminate Hb ; injection Hb as ← ; reflexivity

map2_option over two two-element lists succeeds only when f succeeds on each pair, and gives the two results.

496Lemma map2_two
∀ X Y W : Type f : X → Y → optionW k1 k2 a b xs
map2_optionf k1; k2 a; b = Somexs
∃x y, fk1 a = Somex ∧ fk2 b = Somey ∧ xs = x; y
Explore proof 6 tactics

Initial goal

once :
listname × def
⊢
∀X Y W : Type f : X → Y → optionW k1 k2 : X a b : Y xs : listW, map2_optionf k1; k2 a; b = Somexs → ∃x y : W, fk1 a = Somex ∧ fk2 b = Somey ∧ xs = x; y

intros X Y W f k1 k2 a b xs H

once :
listname × def
X :
Type
Y :
Type
W :
Type
f :
X → Y → optionW
k1, k2 :
X
a, b :
Y
xs :
listW
H :
map2_optionf k1; k2 a; b = Somexs
⊢
∃x y : W, fk1 a = Somex ∧ fk2 b = Somey ∧ xs = x; y

simpl in H

once :
listname × def
X :
Type
Y :
Type
W :
Type
f :
X → Y → optionW
k1, k2 :
X
a, b :
Y
xs :
listW
H :
let* z ≔ fk1 a in
let* zs ≔
let* z0 ≔ fk2 b in
Somez0
in
Somez :: zs
=
Somexs
⊢
∃x y : W, fk1 a = Somex ∧ fk2 b = Somey ∧ xs = x; y

destruct fk1 a as x | ; | discriminate H

once :
listname × def
X :
Type
Y :
Type
W :
Type
f :
X → Y → optionW
k1, k2 :
X
a, b :
Y
xs :
listW
x :
W
H :
let* zs ≔
let* z ≔ fk2 b in
Somez
in
Somex :: zs
=
Somexs
⊢
∃x0 y : W, Somex = Somex0 ∧ fk2 b = Somey ∧ xs = x0; y

destruct fk2 b as y | ; | discriminate H

once :
listname × def
X :
Type
Y :
Type
W :
Type
f :
X → Y → optionW
k1, k2 :
X
a, b :
Y
xs :
listW
x, y :
W
H :
Somex; y = Somexs
⊢
∃x0 y0 : W, Somex = Somex0 ∧ Somey = Somey0 ∧ xs = x0; y0

injection H as ←

once :
listname × def
X :
Type
Y :
Type
W :
Type
f :
X → Y → optionW
k1, k2 :
X
a, b :
Y
x, y :
W
⊢
∃x0 y0 : W, Somex = Somex0 ∧ Somey = Somey0 ∧ x; y = x0; y0

eauto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros X Y W f k1 k2 a b xs H
simpl in H
destruct fk1 a as x | ; | discriminate H
destruct fk2 b as y | ; | discriminate H
injection H as ←
eauto

The theorem

Soundness in one environment of a run: the names that hold their definitions there are a predicate ok, which the run-level invariant supplies (Chain.v's interval_at takes the names whose definitions dominate the point).

510Section Sound

The global environment ge, the environment e the interval is read in, and ok, the names that hold their definitions there.

514Variables ge : genv
514Variables e : env
514Variables ok : name → Prop

What ok must promise, the hypothesis of iv_sound: each name n that is ok and whose definition (defined) is one a derivation walks (iv_op), at an integer class, holds what that definition computed in some environment e0 (let_holds); each of its single-definition operands is ok and holds in e0 what it holds in e.

521Hypothesis Hok
∀ n k o args
definedn k o args
iv_opo = true
class_bitsk ≠ None
okn
∃e0, let_holdsge e0 e n k o args ∧ ∀a, InTmpa args → once_hasonce a = true → oka ∧ lookupa e0 = lookupa e

A temporary n with a derived interval has a single definition: every iv constructor for a name rests on defined.

527Lemma iv_once
∀ v k lo hi n
ivv k lo hi
v = Tmpn
once_hasonce n = true
Explore proof 2 tactics

Initial goal

once :
listname × def
ge :
genv
e :
env
ok :
name → Prop
Hok :
∀n : name k : class o : op args : listvalue, definedn k o args → iv_opo = true → class_bitsk ≠ None → okn → ∃e0 : env, let_holdsge e0 e n k o args ∧ ∀a : name, InTmpa args → once_hasonce a = true → oka ∧ lookupa e0 = lookupa e
⊢
∀v : value k : class lo hi : Z, ivv k lo hi → ∀n : name, v = Tmpn → once_hasonce n = true

intros v k lo hi H n E

once :
listname × def
ge :
genv
e :
env
ok :
name → Prop
Hok :
∀n : name k : class o : op args : listvalue, definedn k o args → iv_opo = true → class_bitsk ≠ None → okn → ∃e0 : env, let_holdsge e0 e n k o args ∧ ∀a : name, InTmpa args → once_hasonce a = true → oka ∧ lookupa e0 = lookupa e
v :
value
k :
class
lo, hi :
Z
H :
ivv k lo hi
n :
name
E :
v = Tmpn
⊢
once_hasonce n = true

destruct H ; try discriminate E ; injection E as →;match goal withHd : defined_ _ _ _ |- _⇒destruct Hd as n′ & Hl & _end;unfold once_has;rewrite Hl;reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros v k lo hi H n E
destruct H ; try discriminate E ; injection E as →;match goal withHd : defined_ _ _ _ |- _⇒destruct Hd as n′ & Hl & _end;unfold once_has;rewrite Hl;reflexivity

An operand a of a definition that ran in e0, where a has a derived interval and the definition's single-definition operands are ok and unchanged since (Hok's conclusion): a, if a temporary, is ok, and a reads the same in e0 as in e, at any class.

538Lemma walked
∀ e0 args a k′ lo hi
∀a, InTmpa args → once_hasonce a = true → oka ∧ lookupa e0 = lookupa e
Ina args
iva k′ lo hi
∀n, a = Tmpn → okn ∧ ∀k′′, value_xge e0 k′′ a = value_xge e k′′ a
Explore proof 5 tactics

Initial goal

once :
listname × def
ge :
genv
e :
env
ok :
name → Prop
Hok :
∀n : name k : class o : op args : listvalue, definedn k o args → iv_opo = true → class_bitsk ≠ None → okn → ∃e0 : env, let_holdsge e0 e n k o args ∧ ∀a : name, InTmpa args → once_hasonce a = true → oka ∧ lookupa e0 = lookupa e
⊢
∀e0 : listname × word args : listvalue a : value k′ : class lo hi : Z, ∀a0 : name, InTmpa0 args → once_hasonce a0 = true → oka0 ∧ lookupa0 e0 = lookupa0 e → Ina args → iva k′ lo hi → ∀n : name, a = Tmpn → okn ∧ ∀k′′ : class, value_xge e0 k′′ a = value_xge e k′′ a

intros e0 args a k′ lo hi Ha Hin Hiv

once :
listname × def
ge :
genv
e :
env
ok :
name → Prop
Hok :
∀n : name k : class o : op args : listvalue, definedn k o args → iv_opo = true → class_bitsk ≠ None → okn → ∃e0 : env, let_holdsge e0 e n k o args ∧ ∀a : name, InTmpa args → once_hasonce a = true → oka ∧ lookupa e0 = lookupa e
e0 :
listname × word
args :
listvalue
a :
value
k′ :
class
lo, hi :
Z
Ha :
∀a : name, InTmpa args → once_hasonce a = true → oka ∧ lookupa e0 = lookupa e
Hin :
Ina args
Hiv :
iva k′ lo hi
⊢
∀n : name, a = Tmpn → okn ∧ ∀k′′ : class, value_xge e0 k′′ a = value_xge e k′′ a

assert Hag : ∀n, a = Tmpn → okn ∧ lookupn e0 = lookupn e by intros n E ; subst a ; exact Ha_ Hin iv_once_ _ _ _ Hiv _ eq_refl

once :
listname × def
ge :
genv
e :
env
ok :
name → Prop
Hok :
∀n : name k : class o : op args : listvalue, definedn k o args → iv_opo = true → class_bitsk ≠ None → okn → ∃e0 : env, let_holdsge e0 e n k o args ∧ ∀a : name, InTmpa args → once_hasonce a = true → oka ∧ lookupa e0 = lookupa e
e0 :
listname × word
args :
listvalue
a :
value
k′ :
class
lo, hi :
Z
Ha :
∀a : name, InTmpa args → once_hasonce a = true → oka ∧ lookupa e0 = lookupa e
Hin :
Ina args
Hiv :
iva k′ lo hi
Hag :
∀n : name, a = Tmpn → okn ∧ lookupn e0 = lookupn e
⊢
∀n : name, a = Tmpn → okn ∧ ∀k′′ : class, value_xge e0 k′′ a = value_xge e k′′ a

split ; intros n E ; exact proj1Hag_ E |

once :
listname × def
ge :
genv
e :
env
ok :
name → Prop
Hok :
∀n : name k : class o : op args : listvalue, definedn k o args → iv_opo = true → class_bitsk ≠ None → okn → ∃e0 : env, let_holdsge e0 e n k o args ∧ ∀a : name, InTmpa args → once_hasonce a = true → oka ∧ lookupa e0 = lookupa e
e0 :
listname × word
args :
listvalue
a :
value
k′ :
class
lo, hi :
Z
Ha :
∀a : name, InTmpa args → once_hasonce a = true → oka ∧ lookupa e0 = lookupa e
Hin :
Ina args
Hiv :
iva k′ lo hi
Hag :
∀n : name, a = Tmpn → okn ∧ lookupn e0 = lookupn e
⊢
∀k′′ : class, value_xge e0 k′′ a = value_xge e k′′ a

intros k′′

once :
listname × def
ge :
genv
e :
env
ok :
name → Prop
Hok :
∀n : name k : class o : op args : listvalue, definedn k o args → iv_opo = true → class_bitsk ≠ None → okn → ∃e0 : env, let_holdsge e0 e n k o args ∧ ∀a : name, InTmpa args → once_hasonce a = true → oka ∧ lookupa e0 = lookupa e
e0 :
listname × word
args :
listvalue
a :
value
k′ :
class
lo, hi :
Z
Ha :
∀a : name, InTmpa args → once_hasonce a = true → oka ∧ lookupa e0 = lookupa e
Hin :
Ina args
Hiv :
iva k′ lo hi
Hag :
∀n : name, a = Tmpn → okn ∧ lookupn e0 = lookupn e
k′′ :
class
⊢
value_xge e0 k′′ a = value_xge e k′′ a

destruct a as n | c | g ; simpl ; rewrite proj2Hag_ eq_refl | | ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros e0 args a k′ lo hi Ha Hin Hiv
assert Hag : ∀n, a = Tmpn → okn ∧ lookupn e0 = lookupn e by intros n E ; subst a ; exact Ha_ Hin iv_once_ _ _ _ Hiv _ eq_refl
split ; intros n E ; exact proj1Hag_ E |
intros k′′
destruct a as n | c | g ; simpl ; rewrite proj2Hag_ eq_refl | | ; reflexivity

Takes apart every match in the statement of H, discarding the cases that make H contradictory.

552Ltac opens H ≔
repeat match type of H withcontext [match ?x with _ ⇒ _ end]⇒destruct x eqn :? ; cbv beta iota zeta in H ; try discriminate Hend;try discriminate H

Offset intervals are sound: if ivv k lo hi is derived and v, if a temporary, is ok, then the value v reads in e at the class k lies from lo to hi, modulo the class (in_iv). With offset_interval_iv, an interval the validator answers bounds the offset a run computes.

561Theorem iv_sound
∀ v k lo hi
ivv k lo hi
∀n, v = Tmpn → okn
in_ivge e k v lo hi
Proof 244 steps Qed
intros v k lo hi H
induction H ; intros Hv

a constant

–assert Hb : ∃bits, class_bitsk = Somebits by destruct k ; try discriminate H ; eexists ; reflexivity
destruct Hb as bits Hb
destruct signed_value_mod_ _ _ _ H Hb as Hm _
exists bits, c mod 2 ^ bits, x
rewrite const_read_ _ _ _ _ Hb
auto with zarith

ext to a narrow type

–destruct fits_bits_ _ _ H1 as bits & Hb & Hm & Hp
destruct Hok_ _ _ _ H eq_refl ltac:congruence Hv_ eq_refl as e0 & Hl & _
destruct Hl as cls & xs & x & Hc & Hx & Ha & Hn
simpl in Hc
injection Hc as ←
destruct args as | a | a′ args ; simpl in Hx ; opens Hx ; injection Hx as ← ; simpl in Ha ; opens Ha
injection Hm as →
injection Ha as ←
match type of Hn withlookup_ _ = SomeWIntextensiont ?y mod _⇒apply in_iv_tmp_ _ _ _ _ _ extensiont y _ _ Hb Hnend;|apply Z.mod_mod ; lia|exact narrow_extension_ _ _ _ H0

ext(sw)

–destruct fits_bits_ _ _ H1 as bits & Hb & Hm & Hp
destruct Hok_ _ _ _ H eq_refl ltac:congruence Hv_ eq_refl as e0 & Hl & Ha′
destruct walked_ _ _ _ _ _ Ha' or_introleq_refl H0 as Hoka Hra
destruct IHivHoka as b32 & ua & xa & Hb32 & Hua & Hxa & →
simpl in Hb32
injection Hb32 as ←
pose proof iv_fits_ _ _ _ H0 as Hf
simpl in Hf
apply andb_true_iff in Hf as Hf1 Hf2
apply Z.leb_le in Hf1
apply Z.leb_le in Hf2
destruct Hl as cls & xs & x & Hc & Hx & Ha & Hn
simpl in Hc
injection Hc as ←
simpl in Hx
rewrite Hra , Hua in Hx
injection Hx as ←
simpl in Ha
rewrite Hm in Ha
injection Ha as ←
apply in_iv_tmp_ _ _ _ _ _ xa _ _ Hb Hn ; | lia
rewrite Z.mod_mod by lia
f_equal
apply sign_extension_mod
lia

ext(uw)

–destruct fits_bits_ _ _ H2 as bits & Hb & Hm & Hp
destruct Hok_ _ _ _ H eq_refl ltac:congruence Hv_ eq_refl as e0 & Hl & Ha′
destruct walked_ _ _ _ _ _ Ha' or_introleq_refl H0 as Hoka Hra
destruct IHivHoka as b32 & ua & xa & Hb32 & Hua & Hxa & →
simpl in Hb32
injection Hb32 as ←
pose proof iv_fits_ _ _ _ H0 as Hf
simpl in Hf
apply andb_true_iff in Hf as Hf1 Hf2
apply Z.leb_le in Hf1
apply Z.leb_le in Hf2
destruct Hl as cls & xs & x & Hc & Hx & Ha & Hn
simpl in Hc
injection Hc as ←
simpl in Hx
rewrite Hra , Hua in Hx
injection Hx as ←
simpl in Ha
rewrite Hm in Ha
injection Ha as ←
apply in_iv_tmp_ _ _ _ _ _ xa _ _ Hb Hn ; | lia
rewrite Z.mod_mod by lia
f_equal
simpl
rewrite Z.mod_mod by lia
apply Z.mod_small
lia

a narrow load

–destruct fits_bits_ _ _ H1 as bits & Hb & Hm & Hp
destruct Hok_ _ _ _ H eq_refl ltac:congruence Hv_ eq_refl as e0 & Hl & _
destruct Hl as u & x & Hx & Hn
unfold extended in Hx
rewrite Hm in Hx
injection Hx as ←
apply in_iv_tmp_ _ _ _ _ _ extensiont u _ _ Hb Hn ; apply Z.mod_mod ; lia | exact narrow_extension_ _ _ _ H0

copy

–destruct fits_bits_ _ _ H1 as bits & Hb & Hm & Hp
destruct Hok_ _ _ _ H eq_refl ltac:congruence Hv_ eq_refl as e0 & Hl & Ha′
destruct walked_ _ _ _ _ _ Ha' or_introleq_refl H0 as Hoka Hra
destruct IHivHoka as b′ & ua & xa & Hb′ & Hua & Hxa & →
rewrite Hb in Hb'
injection Hb' as ←
destruct Hl as cls & xs & x & Hc & Hx & Ha & Hn
simpl in Hc
injection Hc as ←
simpl in Hx
rewrite Hra , Hua in Hx
injection Hx as ←
simpl in Ha
injection Ha as ←
apply in_iv_tmp_ _ _ _ _ _ xa _ _ Hb Hn ; apply Z.mod_mod ; lia | exact Hxa

and with a mask

–destruct fits_bits_ _ _ H3 as bits & Hb & Hm & Hp
destruct Hok_ _ _ _ H eq_refl ltac:congruence Hv_ eq_refl as e0 & Hl & _
destruct signed_value_mod_ _ _ _ H1 Hb as Hcv Hr
assert Hh : 2 ^ bits = 2 × 2 ^ bits − 1 by destruct k ; try discriminate Hb ; injection Hb as ← ; reflexivity
assert Hcu : c mod 2 ^ bits = v by rewrite <- Hcv ; apply Z.mod_small ; lia
destruct Hl as cls & xs & x & Hc & Hx & Ha & Hn
simpl in Hc
injection Hc as ←
destruct map2_two_ _ _ _ _ _ _ _ _ Hx as xa & xb & Ea & Eb & →
destruct xa as ya | | ; destruct xb as yb | | ; simpl in Ha ; try discriminate Ha
injection Ha as ←
pose proof value_int_range_ _ _ _ _ _ Hb Ea
pose proof value_int_range_ _ _ _ _ _ Hb Eb
assert Hy : ya = v ∨ yb = v
{destruct H0 as → | → ; left | right
–rewrite const_read_ _ _ _ _ Hb in Ea
injection Ea as ←
exact Hcu
–rewrite const_read_ _ _ _ _ Hb in Eb
injection Eb as ←
exact Hcu
assert Hland : 0 ≤ Z.landya yb ≤ v by destruct Hy as → | → ; rewrite Z.land_comm | ; apply land_le ; lia
apply in_iv_tmp_ _ _ _ _ _ Z.landya yb _ _ Hb Hn ; reflexivity | lia

urem by a constant

–destruct fits_bits_ _ _ H3 as bits′ & Hb′ & Hm & Hp
rewrite H0 in Hb'
injection Hb' as ←
destruct Hok_ _ _ _ H eq_refl ltac:congruence Hv_ eq_refl as e0 & Hl & _
destruct Hl as cls & xs & x & Hc & Hx & Ha & Hn
simpl in Hc
injection Hc as ←
destruct map2_two_ _ _ _ _ _ _ _ _ Hx as xa & xb & Ea & Eb & →
rewrite const_read_ _ _ _ _ H0 in Eb
injection Eb as ←
destruct xa as ya | | ; simpl in Ha ; try discriminate Ha
injection Ha as ←
pose proof value_int_range_ _ _ _ _ _ H0 Ea
pose proof Z.mod_pos_boundya c mod 2 ^ bits H1
unfold unsigned_division in Hn
rewrite proj2Z.eqb_neq_ _ in Hn by lia
apply in_iv_tmp_ _ _ _ _ _ ya mod c mod 2 ^ bits _ _ H0 Hn ; reflexivity | lia

shl by a constant

–destruct fits_bits_ _ _ H4 as bits′ & Hb′ & Hm & Hp
rewrite H0 in Hb'
injection Hb' as ←
destruct Hok_ _ _ _ H eq_refl ltac:congruence Hv_ eq_refl as e0 & Hl & Ha′
destruct walked_ _ _ _ _ _ Ha' or_introleq_refl H3 as Hoka Hra
destruct IHivHoka as b′ & ua & xa & Hb′ & Hua & Hxa & →
rewrite H0 in Hb'
injection Hb' as ←
destruct Hl as cls & xs & x & Hc & Hx & Ha & Hn
simpl in Hc
injection Hc as ←
assert Hbits : bits = 32 ∨ bits = 64 by destruct k ; try discriminate H0 ; injection H0 as ← ; auto
simpl in Hx
rewrite Hra , Hua in Hx
simpl in Hx
injection Hx as ←
simpl in Ha
unfold shift_factor in Ha
rewrite H0 in Ha
simpl in Ha
rewrite Hm in Ha
injection Ha as ←
change Z.pow_pos2 32 with 2 ^ 32 in Hn
rewrite Z.mod_smalls 2 ^ 32 in Hn by destruct Hbits ; subst ; lia
rewrite Z.mod_smalls bits in Hn by lia
apply in_iv_tmp_ _ _ _ _ _ xa × 2 ^ s _ _ H0 Hn
+rewrite Z.mod_mod by lia
apply Z.mul_mod_idemp_l
lia
+assert 0 < 2 ^ s by apply Z.pow_pos_nonneg ; lia
nia

mul by a constant

–destruct fits_bits_ _ _ H4 as bits & Hb & Hm & Hp
destruct Hok_ _ _ _ H eq_refl ltac:congruence Hv_ eq_refl as e0 & Hl & Ha′
destruct signed_value_mod_ _ _ _ H2 Hb as Hcv _
assert Hin : Inx args by destruct H0 as → | → ; simpl ; auto
destruct walked_ _ _ _ _ _ Ha' Hin H1 as Hoka Hra
destruct IHivHoka as b′ & ua & xa & Hb′ & Hua & Hxa & →
rewrite Hb in Hb'
injection Hb' as ←
destruct Hl as cls & xs & y & Hc & Hy & Ha & Hn
simpl in Hc
injection Hc as ←
assert Hprod : lo0 ≤ hi0 → lo ≤ xa × v ≤ hi by intros _ ; destruct 0 ≤? v eqn: Ez ; apply Z.leb_le in Ez | apply Z.leb_gt in Ez ; injection H3 as ← ← ; nia
destruct H0 as → | → ; destruct map2_two_ _ _ _ _ _ _ _ _ Hy as y1 & y2 & E1 & E2 & →
+rewrite Hra , Hua in E1
injection E1 as ←
rewrite const_read_ _ _ _ _ Hb in E2
injection E2 as ←
simpl in Ha
rewrite Hm in Ha
injection Ha as ←
apply in_iv_tmp_ _ _ _ _ _ xa × v _ _ Hb Hn ; | apply Hprod ; lia
rewrite Z.mod_mod by lia
rewrite <- Hcv
rewrite <- Z.mul_mod by lia
reflexivity
+rewrite Hra , Hua in E2
injection E2 as ←
rewrite const_read_ _ _ _ _ Hb in E1
injection E1 as ←
simpl in Ha
rewrite Hm in Ha
injection Ha as ←
apply in_iv_tmp_ _ _ _ _ _ xa × v _ _ Hb Hn ; | apply Hprod ; lia
rewrite Z.mod_mod by lia
rewrite <- Hcv , Z.mul_commxa
rewrite <- Z.mul_mod by lia
reflexivity

add

–destruct fits_bits_ _ _ H2 as bits & Hb & Hm & Hp
destruct Hok_ _ _ _ H eq_refl ltac:congruence Hv_ eq_refl as e0 & Hl & Ha′
destruct walked_ _ _ _ _ _ Ha' or_introleq_refl H0 as Hoka Hra
destruct walked_ _ _ _ _ _ Ha' or_introror_introleq_refl H1 as Hokb Hrb
destruct IHiv1Hoka as b1 & ua & xa & Hb1 & Hua & Hxa & →
destruct IHiv2Hokb as b2 & ub & xb & Hb2 & Hub & Hxb & →
rewrite Hb in Hb1 , Hb2
injection Hb1 as ←
injection Hb2 as ←
destruct Hl as cls & xs & x & Hc & Hx & Ha & Hn
assert Hcl : cls = k; k by destruct k ; try discriminate Hb ; simpl in Hc ; injection Hc as ← ; reflexivity
subst cls
simpl in Hx
rewrite Hra , Hrb , Hua , Hub in Hx
injection Hx as ←
simpl in Ha
rewrite Hm in Ha
injection Ha as ←
apply in_iv_tmp_ _ _ _ _ _ xa + xb _ _ Hb Hn ; | lia
rewrite Z.mod_mod by lia
rewrite <- Z.add_mod by lia
reflexivity

sub a constant

–destruct fits_bits_ _ _ H2 as bits & Hb & Hm & Hp
destruct Hok_ _ _ _ H eq_refl ltac:congruence Hv_ eq_refl as e0 & Hl & Ha′
destruct signed_value_mod_ _ _ _ H0 Hb as Hcv _
destruct walked_ _ _ _ _ _ Ha' or_introleq_refl H1 as Hoka Hra
destruct IHivHoka as b′ & ua & xa & Hb′ & Hua & Hxa & →
rewrite Hb in Hb'
injection Hb' as ←
destruct Hl as cls & xs & x & Hc & Hx & Ha & Hn
assert Hcl : cls = k; k by destruct k ; try discriminate Hb ; simpl in Hc ; injection Hc as ← ; reflexivity
subst cls
destruct map2_two_ _ _ _ _ _ _ _ _ Hx as y1 & y2 & E1 & E2 & →
rewrite Hra , Hua in E1
injection E1 as ←
rewrite const_read_ _ _ _ _ Hb in E2
injection E2 as ←
simpl in Ha
rewrite Hm in Ha
injection Ha as ←
apply in_iv_tmp_ _ _ _ _ _ xa − v _ _ Hb Hn ; | lia
rewrite Z.mod_mod by lia
rewrite <- Hcv
rewrite <- Zminus_mod
reflexivity