rocq/theories/StringLogic.v
C strings in the program logic of Logic.v, and the triples of the libc string calls derived from Campaign 4's contracts.
string p b reg bytes owns a C string: the life of the object b that p's capability names, read-write or read-only, and its bytes from p's offset through the terminating NUL (byte_ps). Owning it in an interpreted state gives the contracts' readings of a string, terminated_length and c_string (string_facts). One byte of it can be lent out to a load (string_byte).
The triples are each contract's precondition read from owned pieces, and its postcondition handed back as owned pieces and bound results:
wp_strlenandwp_strchr, fromstrlen_contractandstrchr_contract: pure calls, which change no memory and no world (pure_return), so the state interpretation holds again with the same ghost heap, over any registry and world;wp_puts, fromputs_contract: a call that writes its world's roots and may allocate, under the world interpretationstdio_wi: puts's rep and readiness, and the world's writable roots apart from the program's live objects. After a return, the frame for external calls (Logic.v'sprefix_agrees) keeps the program's pieces and puts's prefix the world (puts_return_frame).
Each triple is stated at any call site, so a program uses it as a rule.
From iris.proofmode Require Import proofmode
From iris.base_logic.lib Require Import gen_heap
From iris.program_logic Require Import language weakestpre
From Stdlib Require Import ZArith Lia
From Stdlib Require String
From Nanofil Require Import Term Syntax Values Memory Runtime Ops Semantics Run Machine Panics StepRules ExternalCalls ExternalMachine Pieces Heap ContractFrame Language Logic
Open Scope Z_scope
Open Scope list_scope
Byte pieces
The pieces of the bytes xs from offset o of the object b.
The first byte's piece, then the rest's.
Explore proof 5 tactics
Initial goal
unfold byte_ps
cbn [ length ]
rewrite Nat2Z.inj_succ seqZ_cons ; | lia
rewrite Z.pred_succ
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The i-th piece is the i-th byte's.
Explore proof 10 tactics
Initial goal
revert o i
induction xs as | y xs IH ; intros o i H ; discriminate |
rewrite byte_ps_cons
destruct i as | i ; cbn in H |- *
2 openb, y :
Z
xs :
listZ
x :
Z
o :
Z
H :
Somey = Somex
–injection H as →
2 openb :
Z
xs :
listZ
x :
Z
o :
Z
rewrite Z.add_0_r
2 openb :
Z
xs :
listZ
x :
Z
o :
Z
reflexivity
–rewrite IHo + 1 i H
do 3 f_equal
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
revert o i
induction xs as | y xs IH ; intros o i H ; discriminate |
rewrite byte_ps_cons
destruct i as | i ; cbn in H |- *
–injection H as →
rewrite Z.add_0_r
reflexivity
–rewrite IHo + 1 i H
do 3 f_equal
lia
Where the pieces of xs from offset o of the live object b agree, each byte is in the object and holds its value.
Explore proof 4 tactics
Initial goal
intros E Lv Ha Hx
pose proof all_agree_elem_ _ _ _ Ha list_elem_of_lookup_2_ _ _ byte_ps_lookupb o xs i x Hx as _ Hin
destruct Hinreg E Lv as Ho & He & Hv
m :
b :
Z
reg :
o :
Z
xs :
listZ
i :
nat
x :
Z
E :
object_regionb m_regionsm = Somereg
Hx :
xs !! i = Somex
Ho :
0 ≤ o + i
He :
b + o + i < r_endreg
Hv :
m_bytesm b + o + i = x
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros E Lv Ha Hx
pose proof all_agree_elem_ _ _ _ Ha list_elem_of_lookup_2_ _ _ byte_ps_lookupb o xs i x Hx as _ Hin
destruct Hinreg E Lv as Ho & He & Hv
auto
The bytes, nonzero, followed by a NUL, as the memory holds them from a, are a string_at a.
Explore proof 16 tactics
Initial goal
revert a
induction bytes as | y bytes IH ; intros a Hf Hb
2 openm :
a :
Z
Hf :
Forallλx : Z ⇒ 0 < x < 256 [ ]
Hb :
∀i : nat x : Z, [ ] ++ 0 !! i = Somex → m_bytesm a + i = x
⊢
string_atm a [ ]
focused goal
–cbn
2 openm :
a :
Z
Hf :
Forallλx : Z ⇒ 0 < x < 256 [ ]
Hb :
∀i : nat x : Z, [ ] ++ 0 !! i = Somex → m_bytesm a + i = x
⊢
m_bytesm a = 0
deferred goal
rewrite <- Z.add_0_ra
2 openm :
a :
Z
Hf :
Forallλx : Z ⇒ 0 < x < 256 [ ]
Hb :
∀i : nat x : Z, [ ] ++ 0 !! i = Somex → m_bytesm a + i = x
⊢
m_bytesm a + 0 = 0
deferred goal
exact Hb0%nat 0 eq_refl
deferred goal
–apply Forall_cons_1 in Hf as Hy Hf
cbn
m :
y :
Z
bytes :
listZ
IH :
a :
Z
Hy :
0 < y < 256
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
Hb :
∀i : nat x : Z, y :: bytes ++ 0 !! i = Somex → m_bytesm a + i = x
split ; exact Hy |
m :
y :
Z
bytes :
listZ
IH :
a :
Z
Hy :
0 < y < 256
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
Hb :
∀i : nat x : Z, y :: bytes ++ 0 !! i = Somex → m_bytesm a + i = x
split
2 openm :
y :
Z
bytes :
listZ
IH :
a :
Z
Hy :
0 < y < 256
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
Hb :
∀i : nat x : Z, y :: bytes ++ 0 !! i = Somex → m_bytesm a + i = x
⊢
m_bytesm a = y
focused goal
+rewrite <- Z.add_0_ra
2 openm :
y :
Z
bytes :
listZ
IH :
a :
Z
Hy :
0 < y < 256
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
Hb :
∀i : nat x : Z, y :: bytes ++ 0 !! i = Somex → m_bytesm a + i = x
⊢
m_bytesm a + 0 = y
deferred goal
exact Hb0%nat y eq_refl
deferred goal
+apply IH ; exact Hf |
intros i x Hx
replace a + 1 + Z.of_nati with a + Z.of_natSi by lia
apply Hb
m :
y :
Z
bytes :
listZ
IH :
a :
Z
Hy :
0 < y < 256
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
Hb :
∀i : nat x : Z, y :: bytes ++ 0 !! i = Somex → m_bytesm a + i = x
i :
nat
x :
Z
Hx :
bytes ++ 0 !! i = Somex
⊢
y :: bytes ++ 0 !! Si = Somex
exact Hx
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
revert a
induction bytes as | y bytes IH ; intros a Hf Hb
–cbn
rewrite <- Z.add_0_ra
exact Hb0%nat 0 eq_refl
–apply Forall_cons_1 in Hf as Hy Hf
cbn
split ; exact Hy |
split
+rewrite <- Z.add_0_ra
exact Hb0%nat y eq_refl
+apply IH ; exact Hf |
intros i x Hx
replace a + 1 + Z.of_nati with a + Z.of_natSi by lia
apply Hb
exact Hx
The pieces of xs ++ ys are xs's, then ys's after them.
Explore proof 7 tactics
Initial goal
revert o
induction xs as | x xs IH ; intros o ; cbn ; rewrite Z.add_0_r ; reflexivity |
cbn [ app ]
rewrite ! byte_ps_cons IH
cbn [ app length ]
replace o + Z.of_natSlengthxs with o + 1 + Z.of_natlengthxs by lia
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
revert o
induction xs as | x xs IH ; intros o ; cbn ; rewrite Z.add_0_r ; reflexivity |
cbn [ app ]
rewrite ! byte_ps_cons IH
cbn [ app length ]
replace o + Z.of_natSlengthxs with o + 1 + Z.of_natlengthxs by lia
reflexivity
The pieces of xs are byte pieces at the offsets from o.
Explore proof 9 tactics
Initial goal
revert o
induction xs as | x xs IH ; intros o ; reflexivity |
rewrite byte_ps_cons
cbn [ fmap list_fmap fst ]
rewrite IH
cbn [ length ]
rewrite Nat2Z.inj_succ seqZ_conso ; | lia
rewrite Z.pred_succ
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
revert o
induction xs as | x xs IH ; intros o ; reflexivity |
rewrite byte_ps_cons
cbn [ fmap list_fmap fst ]
rewrite IH
cbn [ length ]
rewrite Nat2Z.inj_succ seqZ_conso ; | lia
rewrite Z.pred_succ
reflexivity
Strings
The shape of a C string at p with contents bytes in the object b with the region reg: p's capability names b, read-write or read-only, at a positive base; the bytes and their NUL lie in the region, which ends within the address space; every byte is nonzero.
The pieces of the string: its object's life and its bytes from p's offset, NUL included.
Where the string's pieces agree, the memory holds its bytes and NUL from p.
Explore proof 5 tactics
Initial goal
intros _ Hl Ha i x Hx
cbn [ fst snd agree_piece ] in Hl
destruct byte_ps_agree_ _ _ _ _ _ _ Hl Ha Hx as Hv _
replace ptr_addrp + Z.of_nati with b + ptr_addrp − b + Z.of_nati by lia
exact Hv
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros _ Hl Ha i x Hx
cbn [ fst snd agree_piece ] in Hl
destruct byte_ps_agree_ _ _ _ _ _ _ Hl Ha Hx as Hv _
exact Hv
Where the string's pieces agree, p points at a terminated_length string of its length: Campaign 4's reading of a string.
∀ m p b reg bytes
terminated_lengthm p Z.of_natlengthbytes
Explore proof 22 tactics
Initial goal
intros Hok Ha
pose proof string_bytesm p b reg bytes Hok Ha as Hb
destruct Hok as Hc & H0 & H1 & H2 & H3 & Hf
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
⊢
terminated_lengthm p lengthbytes
destruct Ha as E Lv _
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
⊢
terminated_lengthm p lengthbytes
assert Hn : Z.of_natlengthbytes < 2 ^ 64 − 1 by lia
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
⊢
terminated_lengthm p lengthbytes
split ; | exact Hn
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
⊢
bounded_lengthm p 2 ^ 64 − 1 lengthbytes
split ; lia |
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
split ; lia |
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
split ; exists b, reg ; auto |
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
replace Z.of_natlengthbytes <? 2 ^ 64 − 1 with true by symmetry ; apply Z.ltb_lt ; exact Hn
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
split ; apply access_read_ b reg ; exact Hc | exact E | lia | lia | apply Z.mod_1_r |
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
split
2 openm :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
focused goal
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
–intros i Hi
2 openm :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
i :
Z
Hi :
0 ≤ i < lengthbytes
deferred goal
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
destruct lookup_lt_is_Some_2bytes Z.to_nati ltac:lia as x Hx
2 openm :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
i :
Z
Hi :
0 ≤ i < lengthbytes
x :
Z
Hx :
bytes !! Z.to_nati = Somex
deferred goal
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
rewrite <- Z2Nat.idi by lia
2 openm :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
i :
Z
Hi :
0 ≤ i < lengthbytes
x :
Z
Hx :
bytes !! Z.to_nati = Somex
deferred goal
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
rewrite HbZ.to_nati x ; | by apply lookup_app_l_Some
2 openm :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
i :
Z
Hi :
0 ≤ i < lengthbytes
x :
Z
Hx :
bytes !! Z.to_nati = Somex
⊢
0 < x < 256
deferred goal
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
exact Forall_lookup_1_ _ _ _ Hf Hx
deferred goal
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
–intros _
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
apply Hblengthbytes 0
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
⊢
bytes ++ 0 !! lengthbytes = Some0
rewrite lookup_app_r ; | lia
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
⊢
0 !! lengthbytes − lengthbytes%nat = Some0
rewrite Nat.sub_diag
m :
p :
b :
Z
reg :
bytes :
listZ
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
lengthbytes < 2 ^ 64 − 1
⊢
0 !! 0%nat = Some0
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hok Ha
pose proof string_bytesm p b reg bytes Hok Ha as Hb
destruct Hok as Hc & H0 & H1 & H2 & H3 & Hf
destruct Ha as E Lv _
assert Hn : Z.of_natlengthbytes < 2 ^ 64 − 1 by lia
split ; | exact Hn
split ; lia |
split ; lia |
split ; exists b, reg ; auto |
replace Z.of_natlengthbytes <? 2 ^ 64 − 1 with true by symmetry ; apply Z.ltb_lt ; exact Hn
split ; apply access_read_ b reg ; exact Hc | exact E | lia | lia | apply Z.mod_1_r |
split
–intros i Hi
destruct lookup_lt_is_Some_2bytes Z.to_nati ltac:lia as x Hx
rewrite <- Z2Nat.idi by lia
rewrite HbZ.to_nati x ; | by apply lookup_app_l_Some
exact Forall_lookup_1_ _ _ _ Hf Hx
–intros _
apply Hblengthbytes 0
rewrite lookup_app_r ; | lia
rewrite Nat.sub_diag
reflexivity
Where the string's pieces agree, p points at a c_string with contents bytes: puts's reading of a string.
Explore proof 7 tactics
Initial goal
intros Hok Ha
pose proof string_bytesm p b reg bytes Hok Ha as Hb
pose proof Hok as Hc & _ & H1 & H2 & _ & Hf
destruct Ha as E _ _
m :
p :
b :
Z
reg :
bytes :
listZ
Hok :
string_okp b reg bytes
E :
object_regionb m_regionsm = Somereg
H1 :
b ≤ ptr_addrp
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
⊢
c_stringm p bytes
split
2 openm :
p :
b :
Z
reg :
bytes :
listZ
Hok :
string_okp b reg bytes
E :
object_regionb m_regionsm = Somereg
H1 :
b ≤ ptr_addrp
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
⊢
access_resm ptr_addrp ptr_capp lengthbytes + 1 Read 1 = Someok
focused goal
m :
p :
b :
Z
reg :
bytes :
listZ
Hok :
string_okp b reg bytes
E :
object_regionb m_regionsm = Somereg
H1 :
b ≤ ptr_addrp
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
–apply access_read_ b reg ; exact Hc | exact E | lia | lia | apply Z.mod_1_r
deferred goal
m :
p :
b :
Z
reg :
bytes :
listZ
Hok :
string_okp b reg bytes
E :
object_regionb m_regionsm = Somereg
H1 :
b ≤ ptr_addrp
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
–apply string_at_of ; exact Hf | exact Hb
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hok Ha
pose proof string_bytesm p b reg bytes Hok Ha as Hb
pose proof Hok as Hc & _ & H1 & H2 & _ & Hf
destruct Ha as E _ _
split
–apply access_read_ b reg ; exact Hc | exact E | lia | lia | apply Z.mod_1_r
–apply string_at_of ; exact Hf | exact Hb
No piece of a string is listed twice.
Explore proof 8 tactics
Initial goal
unfold string_ps
cbn [ fmap list_fmap fst ]
rewrite byte_ps_keys
apply NoDup_cons_2
2 open–rewrite list_elem_of_fmap
2 openintros o & E & _
2 opendiscriminate E
–apply NoDup_fmap_2 ; intros x y E ; injection E as → ; reflexivity | apply NoDup_seqZ
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold string_ps
cbn [ fmap list_fmap fst ]
rewrite byte_ps_keys
apply NoDup_cons_2
–rewrite list_elem_of_fmap
intros o & E & _
discriminate E
–apply NoDup_fmap_2 ; intros x y E ; injection E as → ; reflexivity | apply NoDup_seqZ
Every piece of a string is of its object.
Explore proof 8 tactics
Initial goal
unfold string_ps
rewrite elem_of_cons
intros H | H ; injection H as → _ ; reflexivity |
apply list_elem_of_fmap_2fst in H
cbn [ fst ] in H
rewrite byte_ps_keys in H
apply list_elem_of_fmap in H as o & → & _
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold string_ps
rewrite elem_of_cons
intros H | H ; injection H as → _ ; reflexivity |
apply list_elem_of_fmap_2fst in H
cbn [ fst ] in H
rewrite byte_ps_keys in H
apply list_elem_of_fmap in H as o & → & _
reflexivity
Every piece of a string is a piece of memory.
Explore proof 8 tactics
Initial goal
unfold string_ps
rewrite elem_of_cons
intros H | H ; injection H as → _ ; exact I |
apply list_elem_of_fmap_2fst in H
cbn [ fst ] in H
rewrite byte_ps_keys in H
apply list_elem_of_fmap in H as o & → & _
exact I
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold string_ps
rewrite elem_of_cons
intros H | H ; injection H as → _ ; exact I |
apply list_elem_of_fmap_2fst in H
cbn [ fst ] in H
rewrite byte_ps_keys in H
apply list_elem_of_fmap in H as o & → & _
exact I
The suffix of the string p from its i-th byte, at q: the pieces of the string are its life, the bytes before q, and the pieces of the suffix's bytes, which are the string at q's.
Explore proof 9 tactics
Initial goal
intros Hi q
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
split ; | reflexivity
unfold string_ps
f_equal
rewrite <- take_dropi bytes at 1
rewrite <- app_assoc , byte_ps_app , length_take
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
⊢
byte_ps b (ptr_addr p - b) (take i bytes) ++
byte_ps b (ptr_addr p - b + (i `min` length bytes)%nat) (drop i bytes ++ [0]) =
byte_ps b (ptr_addr p - b) (take i bytes) ++
byte_ps b (ptr_addr q - b) (drop i bytes ++ [0])cbn [ ptr_addr q ]
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
⊢
byte_ps b (ptr_addr p - b) (take i bytes) ++
byte_ps b (ptr_addr p - b + (i `min` length bytes)%nat) (drop i bytes ++ [0]) =
byte_ps b (ptr_addr p - b) (take i bytes) ++
byte_ps b (ptr_addr p + i - b) (drop i bytes ++ [0])replace ptr_addrp − b + Z.of_natNat.mini lengthbytes with ptr_addrp + Z.of_nati − b by lia
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hi q
split ; | reflexivity
unfold string_ps
f_equal
rewrite <- take_dropi bytes at 1
rewrite <- app_assoc , byte_ps_app , length_take
cbn [ ptr_addr q ]
reflexivity
The suffix of a string from a byte before its NUL is a string.
Explore proof 11 tactics
Initial goal
intros Hi Hc & H0 & H1 & H2 & H3 & Hf
unfold string_ok
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
⊢
ptr_capptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp = Objb ∨ ptr_capptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp = Rob ∧ 0 < b ∧ b ≤ ptr_addrptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp ∧ ptr_addrptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp + lengthdropi bytes + 1 ≤ r_endreg ∧ r_endreg ≤ 2 ^ 48 ∧ Forallλx : Z ⇒ 0 < x < 256 dropi bytes
cbn [ ptr_addr ptr_cap ]
rewrite length_drop
split ; exact Hc |
split ; exact H0 |
split ; lia |
split ; lia |
split ; exact H3 |
apply Forall_drop
exact Hf
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
The stdio world
The world interpretation of a program that calls puts: puts's representation rep and stdio_ready of the world w in m, and the world's writable roots apart from the live objects owning pieces of the ghost heap h.
220Definition stdio_wirep : mem → stdio_world → Prop m : mem w : stdio_world h : gmappiece pval : Prop ≔
repm w ∧ stdio_readym w ∧ roots_apartstdio_rootsw h m
C strings and the string calls over any runtime R.
Import L LG
A safepoint keeps stdio_wi where it keeps rep and readiness: the roots stay apart since no region changes (collector_live).
∀ rep : mem → stdio_world → Prop
∀s m s′ m′ w, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
Explore proof 14 tactics
Initial goal
rep :
mem → stdio_world → Prop
⊢
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w → SafepointStablestdio_wirep
intros Hst
rep :
mem → stdio_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
split
rep :
mem → stdio_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
intros s m s′ m′ w h Hsp Hr & Hw & Ha
rep :
mem → stdio_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
repm w
Hw :
stdio_readym w
Ha :
⊢
stdio_wirep m′ w h
destruct Hst_ _ _ _ _ Hsp Hr Hw as Hr′ Hw′
rep :
mem → stdio_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
repm w
Hw :
stdio_readym w
Ha :
Hr′ :
repm′ w
Hw′ :
stdio_readym′ w
⊢
stdio_wirep m′ w h
split ; exact Hr′ |
rep :
mem → stdio_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
repm w
Hw :
stdio_readym w
Ha :
Hr′ :
repm′ w
Hw′ :
stdio_readym′ w
⊢
stdio_readym′ w ∧ roots_apartstdio_rootsw h m′
split ; exact Hw′ |
rep :
mem → stdio_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
repm w
Hw :
stdio_readym w
Ha :
Hr′ :
repm′ w
Hw′ :
stdio_readym′ w
⊢
roots_apartstdio_rootsw h m′
intros sp a Hin Hs l & v & reg & Hl & Hm & E Hlive & Hb
rep :
mem → stdio_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
repm w
Hw :
stdio_readym w
Ha :
Hr′ :
repm′ w
Hw′ :
stdio_readym′ w
sp :
a :
Z
Hin :
Insp stdio_rootsw
Hs :
span_containssp a
l :
v :
reg :
Hl :
h !! l = Somev
Hm :
E :
object_regionpiece_idl m_regionsm′ = Somereg
⊢
False
apply Hasp a Hin Hs
rep :
mem → stdio_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
repm w
Hw :
stdio_readym w
Ha :
Hr′ :
repm′ w
Hw′ :
stdio_readym′ w
sp :
a :
Z
Hin :
Insp stdio_rootsw
Hs :
span_containssp a
l :
v :
reg :
Hl :
h !! l = Somev
Hm :
E :
object_regionpiece_idl m_regionsm′ = Somereg
⊢
owned_liveh m a
rewrite R.collector_live_ _ _ _ Hsp in E
rep :
mem → stdio_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
repm w
Hw :
stdio_readym w
Ha :
Hr′ :
repm′ w
Hw′ :
stdio_readym′ w
sp :
a :
Z
Hin :
Insp stdio_rootsw
Hs :
span_containssp a
l :
v :
reg :
Hl :
h !! l = Somev
Hm :
E :
object_regionpiece_idl m_regionsm = Somereg
⊢
owned_liveh m a
exists l, v, reg
rep :
mem → stdio_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
repm w
Hw :
stdio_readym w
Ha :
Hr′ :
repm′ w
Hw′ :
stdio_readym′ w
sp :
a :
Z
Hin :
Insp stdio_rootsw
Hs :
span_containssp a
l :
v :
reg :
Hl :
h !! l = Somev
Hm :
E :
object_regionpiece_idl m_regionsm = Somereg
split ; exact Hl |
rep :
mem → stdio_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
repm w
Hw :
stdio_readym w
Ha :
Hr′ :
repm′ w
Hw′ :
stdio_readym′ w
sp :
a :
Z
Hin :
Insp stdio_rootsw
Hs :
span_containssp a
l :
v :
reg :
Hl :
h !! l = Somev
Hm :
E :
object_regionpiece_idl m_regionsm = Somereg
split ; exact Hm |
rep :
mem → stdio_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
repm w
Hw :
stdio_readym w
Ha :
Hr′ :
repm′ w
Hw′ :
stdio_readym′ w
sp :
a :
Z
Hin :
Insp stdio_rootsw
Hs :
span_containssp a
l :
v :
reg :
Hl :
h !! l = Somev
Hm :
E :
object_regionpiece_idl m_regionsm = Somereg
split ; | exact Hb
rep :
mem → stdio_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
repm w
Hw :
stdio_readym w
Ha :
Hr′ :
repm′ w
Hw′ :
stdio_readym′ w
sp :
a :
Z
Hin :
Insp stdio_rootsw
Hs :
span_containssp a
l :
v :
reg :
Hl :
h !! l = Somev
Hm :
E :
object_regionpiece_idl m_regionsm = Somereg
split ; exact E | exact Hlive
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hst
split
intros s m s′ m′ w h Hsp Hr & Hw & Ha
destruct Hst_ _ _ _ _ Hsp Hr Hw as Hr′ Hw′
split ; exact Hr′ |
split ; exact Hw′ |
intros sp a Hin Hs l & v & reg & Hl & Hm & E Hlive & Hb
apply Hasp a Hin Hs
rewrite R.collector_live_ _ _ _ Hsp in E
exists l, v, reg
split ; exact Hl |
split ; exact Hm |
split ; | exact Hb
split ; exact E | exact Hlive
A puts call returns one int.
∀ rep requests r args xs s m w trace values s′ m′ w′
M.E.invokeputs_contractrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
∃n, values = WIntn
Explore proof 7 tactics
Initial goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
⊢
M.E.invokeputs_contractrep requests r args xs s m w trace CallReturnvalues s′ m′ w′ → ∃n : Z, values = WIntn
intros Hi
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokeputs_contractrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
⊢
∃n : Z, values = WIntn
remember CallReturnvalues as en eqn: Een
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
en :
Een :
en = CallReturnvalues
Hi :
M.E.invokeputs_contractrep requests r args xs s m w trace en s′ m′ w′
⊢
∃n : Z, values = WIntn
destruct Hi as ? ? ? ? ? ? _ _ _ Hp | ? ? ? ? ? ? _ _ _ _ _ ; | discriminate Een
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
values :
listword
ending :
Een :
ending = CallReturnvalues
trace :
listevent
s′ :
R.state
m′ :
w′ :
born :
listZ
Hp :
contract_postputs_contractrep requests xs m w born trace ending m′ w′
H :
∀why : reason, ending ≠ CallResourcewhy
H0 :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnsputs_contractrep requests values ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m w born m′ values
H1 :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
∃n : Z, values = WIntn
destruct Hp as p & bytes & acc & tail & n & _ & _ & _ & _ & _ & Hend & _
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
values :
listword
ending :
Een :
ending = CallReturnvalues
trace :
listevent
s′ :
R.state
m′ :
w′ :
born :
listZ
p :
bytes, acc, tail :
listZ
n :
Z
Hend :
ending = CallReturnWIntn
H :
∀why : reason, ending ≠ CallResourcewhy
H0 :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnsputs_contractrep requests values ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m w born m′ values
H1 :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
∃n0 : Z, values = WIntn0
subst
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
values :
listword
trace :
listevent
s′ :
R.state
m′ :
w′ :
born :
listZ
p :
bytes, acc, tail :
listZ
n :
Z
H1 :
∀status : Z, CallReturnvalues = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
H0 :
∀values0 : listword, CallReturnvalues = CallReturnvalues0 → return_shapecontract_returnsputs_contractrep requests values0 ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m w born m′ values0
H :
∀why : reason, CallReturnvalues ≠ CallResourcewhy
Hend :
CallReturnvalues = CallReturnWIntn
⊢
∃n0 : Z, values = WIntn0
injection Hend as →
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
s′ :
R.state
m′ :
w′ :
born :
listZ
p :
bytes, acc, tail :
listZ
n :
Z
H :
∀why : reason, CallReturnWIntn ≠ CallResourcewhy
H0 :
∀values : listword, CallReturnWIntn = CallReturnvalues → return_shapecontract_returnsputs_contractrep requests values ∧ Forallword_authoritycontract_sourcesputs_contractrep requests xs m w born m′ values
H1 :
∀status : Z, CallReturnWIntn = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hi
remember CallReturnvalues as en eqn: Een
destruct Hi as ? ? ? ? ? ? _ _ _ Hp | ? ? ? ? ? ? _ _ _ _ _ ; | discriminate Een
destruct Hp as p & bytes & acc & tail & n & _ & _ & _ & _ & _ & Hend & _
subst
injection Hend as →
eauto
After a puts call that returns, from a state interpreted with the ghost heap h, the state is interpreted with h again: puts's prefix keeps the runtime ready, the frame keeps h agreeing and live objects apart, and the prefix gives rep and readiness of the new world, whose roots it delegated from the old roots and its born objects, so they stay apart from h.
∀ rep requests r args xs s m w trace values s′ m′ w′ h
M.E.invokeputs_contractrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
agreesm h
R.readys m
stdio_wirep m w h
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ stdio_wirep m′ w′ h
Explore proof 12 tactics
Initial goal
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
⊢
M.E.invokeputs_contractrep requests r args xs s m w trace CallReturnvalues s′ m′ w′ → agreesm h → live_disjointm → R.readys m → stdio_wirep m w h → agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ stdio_wirep m′ w′ h
intros Hi Ha Hd Hr Hrep & Hw & Hapart
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokeputs_contractrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hrep :
repm w
Hw :
stdio_readym w
Hapart :
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ stdio_wirep m′ w′ h
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hi as born & Hp
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokeputs_contractrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hrep :
repm w
Hw :
stdio_readym w
Hapart :
born :
listZ
Hp :
M.E.prefixputs_contractrep requests xs s m w born trace s′ m′ w′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ stdio_wirep m′ w′ h
destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as Hr′ _
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokeputs_contractrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hrep :
repm w
Hw :
stdio_readym w
Hapart :
born :
listZ
Hp :
M.E.prefixputs_contractrep requests xs s m w born trace s′ m′ w′
Hr′ :
R.readys′ m′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ stdio_wirep m′ w′ h
destruct prefix_agrees_ _ _ _ _ _ _ _ _ _ _ h Hp Hr Hd Ha Hapart ltac:intros ? ? ? as Ha′ & Hd′ & Hb & Hapart′
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokeputs_contractrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hrep :
repm w
Hw :
stdio_readym w
Hapart :
born :
listZ
Hp :
M.E.prefixputs_contractrep requests xs s m w born trace s′ m′ w′
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hapart′ :
roots_apartcontract_writesputs_contractrep requests xs m w h m′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ stdio_wirep m′ w′ h
destruct Hp as _ Hrep′ & Hw′ & Hdel & _
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokeputs_contractrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hrep :
repm w
Hw :
stdio_readym w
Hapart :
born :
listZ
Hrep′ :
repm′ w′
Hw′ :
stdio_readym′ w′
Hdel :
stdio_delegatesstdio_rootsw born m′ w′
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hapart′ :
roots_apartcontract_writesputs_contractrep requests xs m w h m′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ stdio_wirep m′ w′ h
change roots_apartstdio_rootsw h m′ in Hapart′
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokeputs_contractrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hrep :
repm w
Hw :
stdio_readym w
Hapart :
born :
listZ
Hrep′ :
repm′ w′
Hw′ :
stdio_readym′ w′
Hdel :
stdio_delegatesstdio_rootsw born m′ w′
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hapart′ :
roots_apartstdio_rootsw h m′
⊢
agreesm′ h ∧ live_disjointm′ ∧ R.readys′ m′ ∧ stdio_wirep m′ w′ h
split ; exact Ha′ |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokeputs_contractrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hrep :
repm w
Hw :
stdio_readym w
Hapart :
born :
listZ
Hrep′ :
repm′ w′
Hw′ :
stdio_readym′ w′
Hdel :
stdio_delegatesstdio_rootsw born m′ w′
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hapart′ :
roots_apartstdio_rootsw h m′
⊢
live_disjointm′ ∧ R.readys′ m′ ∧ stdio_wirep m′ w′ h
split ; exact Hd′ |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokeputs_contractrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hrep :
repm w
Hw :
stdio_readym w
Hapart :
born :
listZ
Hrep′ :
repm′ w′
Hw′ :
stdio_readym′ w′
Hdel :
stdio_delegatesstdio_rootsw born m′ w′
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hapart′ :
roots_apartstdio_rootsw h m′
⊢
R.readys′ m′ ∧ stdio_wirep m′ w′ h
split ; exact Hr′ |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokeputs_contractrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hrep :
repm w
Hw :
stdio_readym w
Hapart :
born :
listZ
Hrep′ :
repm′ w′
Hw′ :
stdio_readym′ w′
Hdel :
stdio_delegatesstdio_rootsw born m′ w′
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hapart′ :
roots_apartstdio_rootsw h m′
⊢
stdio_wirep m′ w′ h
split ; exact Hrep′ |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokeputs_contractrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hrep :
repm w
Hw :
stdio_readym w
Hapart :
born :
listZ
Hrep′ :
repm′ w′
Hw′ :
stdio_readym′ w′
Hdel :
stdio_delegatesstdio_rootsw born m′ w′
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hapart′ :
roots_apartstdio_rootsw h m′
⊢
stdio_readym′ w′ ∧ roots_apartstdio_rootsw′ h m′
split ; exact Hw′ |
rep :
mem → stdio_world → Prop
requests :
listword → mem → stdio_world → Z → Z → Prop
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
Hi :
M.E.invokeputs_contractrep requests r args xs s m w trace CallReturnvalues s′ m′ w′
Ha :
agreesm h
Hd :
Hr :
R.readys m
Hrep :
repm w
Hw :
stdio_readym w
Hapart :
born :
listZ
Hrep′ :
repm′ w′
Hw′ :
stdio_readym′ w′
Hdel :
stdio_delegatesstdio_rootsw born m′ w′
Hr′ :
R.readys′ m′
Ha′ :
agreesm′ h
Hd′ :
Hb :
ids_apartborn h
Hapart′ :
roots_apartstdio_rootsw h m′
⊢
roots_apartstdio_rootsw′ h m′
exact delegates_apart_ _ _ _ h Hdel Hapart′ Hb Hd′
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hi Ha Hd Hr Hrep & Hw & Hapart
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hi as born & Hp
destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as Hr′ _
destruct prefix_agrees_ _ _ _ _ _ _ _ _ _ _ h Hp Hr Hd Ha Hapart ltac:intros ? ? ? as Ha′ & Hd′ & Hb & Hapart′
destruct Hp as _ Hrep′ & Hw′ & Hdel & _
change roots_apartstdio_rootsw h m′ in Hapart′
split ; exact Ha′ |
split ; exact Hd′ |
split ; exact Hr′ |
split ; exact Hrep′ |
split ; exact Hw′ |
exact delegates_apart_ _ _ _ h Hdel Hapart′ Hb Hd′
Owning a string in an interpreted state, p points there at a terminated_length string of its length and at a c_string.
Explore proof 4 tactics
Initial goal
iIntros Hσ [%Hok Hs]
iDestruct pts_facts with Hσ Hs as %Ha & _
iPureIntro
split ; exact string_terminated_ _ _ _ _ Hok Ha | exact string_c_string_ _ _ _ _ Hok Ha
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
iIntros Hσ [%Hok Hs]
iDestruct pts_facts with Hσ Hs as %Ha & _
iPureIntro
split ; exact string_terminated_ _ _ _ _ Hok Ha | exact string_c_string_ _ _ _ _ Hok Ha
The string lends its object's life and its i-th byte, x, the NUL for i its length, and takes them back.
Explore proof 11 tactics
Initial goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
x :
Z
intros Hx
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
x :
Z
Hx :
bytes ++ 0 !! i = Somex
iIntros [%Hok [Hl Hs]]
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
x :
Z
Hx :
bytes ++ 0 !! i = Somex
Hok :
string_okp b reg bytes
∗
rewrite / live / ibyte / pts /=
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
x :
Z
Hx :
bytes ++ 0 !! i = Somex
Hok :
string_okp b reg bytes
∗
iDestruct big_sepL_lookup_acc with Hs as [Hb Hk] ; exact byte_ps_lookup_ _ _ _ _ Hx |
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
x :
Z
Hx :
bytes ++ 0 !! i = Somex
Hok :
string_okp b reg bytes
∗
iSplit ; done |
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
x :
Z
Hx :
bytes ++ 0 !! i = Somex
Hok :
string_okp b reg bytes
∗
iSplitL Hl ; iFrame |
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
x :
Z
Hx :
bytes ++ 0 !! i = Somex
Hok :
string_okp b reg bytes
∗
iSplitL Hb ; iFrame |
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
x :
Z
Hx :
bytes ++ 0 !! i = Somex
Hok :
string_okp b reg bytes
∗
iIntros [Hl _] [Hb _]
iSplit ; done |
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
x :
Z
Hx :
bytes ++ 0 !! i = Somex
Hok :
string_okp b reg bytes
Hk :
∗
iFrame Hl
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
x :
Z
Hx :
bytes ++ 0 !! i = Somex
Hok :
string_okp b reg bytes
Hk :
∗
iApply Hk with Hb
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hx
iIntros [%Hok [Hl Hs]]
iDestruct big_sepL_lookup_acc with Hs as [Hb Hk] ; exact byte_ps_lookup_ _ _ _ _ Hx |
iSplit ; done |
iSplitL Hl ; iFrame |
iSplitL Hb ; iFrame |
iIntros [Hl _] [Hb _]
iSplit ; done |
iFrame Hl
iApply Hk with Hb
A string lends the suffix from its i-th byte, before its NUL or at it, as the string at q, and takes it back.
Explore proof 14 tactics
Initial goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
intros Hi
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
destruct string_ps_suffixp b reg bytes i Hi as Ep Eq
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
Ep :
iIntros [%Hok Hs]
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
Ep :
Eq :
Hok :
string_okp b reg bytes
∗
rewrite / string Ep Eq / pts big_sepL_cons big_sepL_app
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
Ep :
Eq :
Hok :
string_okp b reg bytes
∗
⌜string_okptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp b reg dropi bytes⌝ ∗ ∗lv∈PLiveb, VLivereg :: byte_psb ptr_addrptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp − b dropi bytes ++ 0pointstolv.1 DfracOwn1 lv.2 ∗ ⌜string_okptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp b reg dropi bytes⌝ ∗ ∗lv∈PLiveb, VLivereg :: byte_psb ptr_addrptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp − b dropi bytes ++ 0pointstolv.1 DfracOwn1 lv.2 −∗ ⌜string_okp b reg bytes⌝ ∗ pointstoPLiveb, VLivereg.1 DfracOwn1 PLiveb, VLivereg.2 ∗ ∗y∈byte_psb ptr_addrp − b takei bytespointstoy.1 DfracOwn1 y.2 ∗ ∗y∈byte_psb ptr_addrptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp − b dropi bytes ++ 0pointstoy.1 DfracOwn1 y.2
iDestruct Hs as (Hl & Hpre & Hsuf)
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
Ep :
Eq :
Hok :
string_okp b reg bytes
∗
⌜string_okptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp b reg dropi bytes⌝ ∗ ∗lv∈PLiveb, VLivereg :: byte_psb ptr_addrptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp − b dropi bytes ++ 0pointstolv.1 DfracOwn1 lv.2 ∗ ⌜string_okptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp b reg dropi bytes⌝ ∗ ∗lv∈PLiveb, VLivereg :: byte_psb ptr_addrptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp − b dropi bytes ++ 0pointstolv.1 DfracOwn1 lv.2 −∗ ⌜string_okp b reg bytes⌝ ∗ pointstoPLiveb, VLivereg.1 DfracOwn1 PLiveb, VLivereg.2 ∗ ∗y∈byte_psb ptr_addrp − b takei bytespointstoy.1 DfracOwn1 y.2 ∗ ∗y∈byte_psb ptr_addrptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp − b dropi bytes ++ 0pointstoy.1 DfracOwn1 y.2
iSplitL Hl Hsuf
2 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
Ep :
Eq :
Hok :
string_okp b reg bytes
∗
focused goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
Ep :
Eq :
Hok :
string_okp b reg bytes
∗
⌜string_okptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp b reg dropi bytes⌝ ∗ ∗lv∈PLiveb, VLivereg :: byte_psb ptr_addrptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp − b dropi bytes ++ 0pointstolv.1 DfracOwn1 lv.2 −∗ ⌜string_okp b reg bytes⌝ ∗ pointstoPLiveb, VLivereg.1 DfracOwn1 PLiveb, VLivereg.2 ∗ ∗y∈byte_psb ptr_addrp − b takei bytespointstoy.1 DfracOwn1 y.2 ∗ ∗y∈byte_psb ptr_addrptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp − b dropi bytes ++ 0pointstoy.1 DfracOwn1 y.2
–iSplit ; iPureIntro ; exact string_ok_suffix_ _ _ _ _ Hi Hok |
2 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
Ep :
Eq :
Hok :
string_okp b reg bytes
∗
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
Ep :
Eq :
Hok :
string_okp b reg bytes
∗
⌜string_okptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp b reg dropi bytes⌝ ∗ ∗lv∈PLiveb, VLivereg :: byte_psb ptr_addrptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp − b dropi bytes ++ 0pointstolv.1 DfracOwn1 lv.2 −∗ ⌜string_okp b reg bytes⌝ ∗ pointstoPLiveb, VLivereg.1 DfracOwn1 PLiveb, VLivereg.2 ∗ ∗y∈byte_psb ptr_addrp − b takei bytespointstoy.1 DfracOwn1 y.2 ∗ ∗y∈byte_psb ptr_addrptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp − b dropi bytes ++ 0pointstoy.1 DfracOwn1 y.2
rewrite big_sepL_cons
2 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
Ep :
Eq :
Hok :
string_okp b reg bytes
∗
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
Ep :
Eq :
Hok :
string_okp b reg bytes
∗
⌜string_okptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp b reg dropi bytes⌝ ∗ ∗lv∈PLiveb, VLivereg :: byte_psb ptr_addrptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp − b dropi bytes ++ 0pointstolv.1 DfracOwn1 lv.2 −∗ ⌜string_okp b reg bytes⌝ ∗ pointstoPLiveb, VLivereg.1 DfracOwn1 PLiveb, VLivereg.2 ∗ ∗y∈byte_psb ptr_addrp − b takei bytespointstoy.1 DfracOwn1 y.2 ∗ ∗y∈byte_psb ptr_addrptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp − b dropi bytes ++ 0pointstoy.1 DfracOwn1 y.2
iFrame
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
Ep :
Eq :
Hok :
string_okp b reg bytes
∗
⌜string_okptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp b reg dropi bytes⌝ ∗ ∗lv∈PLiveb, VLivereg :: byte_psb ptr_addrptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp − b dropi bytes ++ 0pointstolv.1 DfracOwn1 lv.2 −∗ ⌜string_okp b reg bytes⌝ ∗ pointstoPLiveb, VLivereg.1 DfracOwn1 PLiveb, VLivereg.2 ∗ ∗y∈byte_psb ptr_addrp − b takei bytespointstoy.1 DfracOwn1 y.2 ∗ ∗y∈byte_psb ptr_addrptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp − b dropi bytes ++ 0pointstoy.1 DfracOwn1 y.2
–iIntros [_ Hq]
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
Ep :
Eq :
Hok :
string_okp b reg bytes
∗
rewrite big_sepL_cons
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
Ep :
Eq :
Hok :
string_okp b reg bytes
∗
iDestruct Hq as [Hl Hsuf]
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
Ep :
Eq :
Hok :
string_okp b reg bytes
∗
iSplit ; done |
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
p :
b :
Z
reg :
bytes :
listZ
i :
nat
Hi :
i ≤ lengthbytes%nat
Ep :
Eq :
Hok :
string_okp b reg bytes
∗
iFrame
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hi
destruct string_ps_suffixp b reg bytes i Hi as Ep Eq
iIntros [%Hok Hs]
iDestruct Hs as (Hl & Hpre & Hsuf)
iSplitL Hl Hsuf
–iIntros [_ Hq]
rewrite big_sepL_cons
iDestruct Hq as [Hl Hsuf]
iSplit ; done |
iFrame
Where the string's pieces agree, p points at a bounded_length string for any bound n: its length, or n if that is shorter. Campaign 4's reading of a string for strncmp.
∀ m p b reg bytes n
bounded_lengthm p n Z.minZ.of_natlengthbytes n
Explore proof 22 tactics
Initial goal
intros Hok Ha Hn
pose proof string_bytesm p b reg bytes Hok Ha as Hb
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
Hok :
string_okp b reg bytes
Hn :
0 ≤ n < 2 ^ 64
⊢
bounded_length m p n (length bytes `min` n)destruct Hok as Hc & H0 & H1 & H2 & H3 & Hf
destruct Ha as E Lv _
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
⊢
bounded_length m p n (length bytes `min` n)split ; exact Hn |
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
⊢
0 <= length bytes `min` n <= n
∧ (∃ (base : Z) (reg0 : region),
(ptr_cap p = Obj base ∨ ptr_cap p = Ro base)
∧ object_region base (m_regions m) = Some reg0 ∧ r_life reg0 = Live)
∧ access_res m (ptr_addr p) (ptr_cap p)
(length bytes `min` n + (if length bytes `min` n <? n then 1 else 0))
Read 1 =
Some ok
∧ (∀ i : Z,
0 <= i < length bytes `min` n → 0 < m_bytes m (ptr_addr p + i) < 256)
∧ (length bytes `min` n < n
→ m_bytes m (ptr_addr p + length bytes `min` n) = 0)split ; lia |
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
⊢
(∃ (base : Z) (reg0 : region),
(ptr_cap p = Obj base ∨ ptr_cap p = Ro base)
∧ object_region base (m_regions m) = Some reg0 ∧ r_life reg0 = Live)
∧ access_res m (ptr_addr p) (ptr_cap p)
(length bytes `min` n + (if length bytes `min` n <? n then 1 else 0))
Read 1 =
Some ok
∧ (∀ i : Z,
0 <= i < length bytes `min` n → 0 < m_bytes m (ptr_addr p + i) < 256)
∧ (length bytes `min` n < n
→ m_bytes m (ptr_addr p + length bytes `min` n) = 0)split ; exists b, reg ; auto |
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
⊢
access_res m (ptr_addr p) (ptr_cap p)
(length bytes `min` n + (if length bytes `min` n <? n then 1 else 0)) Read
1 =
Some ok
∧ (∀ i : Z,
0 <= i < length bytes `min` n → 0 < m_bytes m (ptr_addr p + i) < 256)
∧ (length bytes `min` n < n
→ m_bytes m (ptr_addr p + length bytes `min` n) = 0)split
2 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
⊢
access_res m (ptr_addr p) (ptr_cap p)
(length bytes `min` n + (if length bytes `min` n <? n then 1 else 0)) Read
1 =
Some okfocused goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
⊢
(∀ i : Z,
0 <= i < length bytes `min` n → 0 < m_bytes m (ptr_addr p + i) < 256)
∧ (length bytes `min` n < n
→ m_bytes m (ptr_addr p + length bytes `min` n) = 0)–apply access_read_ b reg ; exact Hc | exact E | lia | | apply Z.mod_1_r
2 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
⊢
ptr_addr p +
(length bytes `min` n + (if length bytes `min` n <? n then 1 else 0)) <=
r_end regdeferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
⊢
(∀ i : Z,
0 <= i < length bytes `min` n → 0 < m_bytes m (ptr_addr p + i) < 256)
∧ (length bytes `min` n < n
→ m_bytes m (ptr_addr p + length bytes `min` n) = 0)destruct Z.min_ n <? n ; lia
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
⊢
(∀ i : Z,
0 <= i < length bytes `min` n → 0 < m_bytes m (ptr_addr p + i) < 256)
∧ (length bytes `min` n < n
→ m_bytes m (ptr_addr p + length bytes `min` n) = 0)–split
2 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
⊢
∀ i : Z, 0 <= i < length bytes `min` n → 0 < m_bytes m (ptr_addr p + i) < 256focused goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
⊢
length bytes `min` n < n → m_bytes m (ptr_addr p + length bytes `min` n) = 0+intros i Hi
2 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
i :
Z
Hi : 0 <= i < length bytes `min` ndeferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
⊢
length bytes `min` n < n → m_bytes m (ptr_addr p + length bytes `min` n) = 0destruct lookup_lt_is_Some_2bytes Z.to_nati ltac:lia as x Hx
2 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
i :
Z
Hi : 0 <= i < length bytes `min` nx :
Z
Hx :
bytes !! Z.to_nati = Somex
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
⊢
length bytes `min` n < n → m_bytes m (ptr_addr p + length bytes `min` n) = 0rewrite <- Z2Nat.idi by lia
2 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
i :
Z
Hi : 0 <= i < length bytes `min` nx :
Z
Hx :
bytes !! Z.to_nati = Somex
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
⊢
length bytes `min` n < n → m_bytes m (ptr_addr p + length bytes `min` n) = 0rewrite HbZ.to_nati x ; | by apply lookup_app_l_Some
2 openhlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
i :
Z
Hi : 0 <= i < length bytes `min` nx :
Z
Hx :
bytes !! Z.to_nati = Somex
⊢
0 < x < 256
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
⊢
length bytes `min` n < n → m_bytes m (ptr_addr p + length bytes `min` n) = 0exact Forall_lookup_1_ _ _ _ Hf Hx
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
⊢
length bytes `min` n < n → m_bytes m (ptr_addr p + length bytes `min` n) = 0+intros Hk
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
Hk : length bytes `min` n < n⊢
m_bytes m (ptr_addr p + length bytes `min` n) = 0assert Z.minZ.of_natlengthbytes n = Z.of_natlengthbytes as → by lia
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
Hk : length bytes `min` n < napply Hblengthbytes 0
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
Hk : length bytes `min` n < n⊢
bytes ++ 0 !! lengthbytes = Some0
rewrite lookup_app_r ; | lia
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
Hk : length bytes `min` n < n⊢
0 !! lengthbytes − lengthbytes%nat = Some0
rewrite Nat.sub_diag
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
m :
p :
b :
Z
reg :
bytes :
listZ
n :
Z
H0 :
0 < b
H1 :
b ≤ ptr_addrp
H3 :
r_endreg ≤ 2 ^ 48
Hf :
Forallλx : Z ⇒ 0 < x < 256 bytes
E :
object_regionb m_regionsm = Somereg
Hn :
0 ≤ n < 2 ^ 64
Hk : length bytes `min` n < n⊢
0 !! 0%nat = Some0
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hok Ha Hn
pose proof string_bytesm p b reg bytes Hok Ha as Hb
destruct Hok as Hc & H0 & H1 & H2 & H3 & Hf
destruct Ha as E Lv _
split ; exact Hn |
split ; lia |
split ; exists b, reg ; auto |
split
–apply access_read_ b reg ; exact Hc | exact E | lia | | apply Z.mod_1_r
destruct Z.min_ n <? n ; lia
–split
+intros i Hi
destruct lookup_lt_is_Some_2bytes Z.to_nati ltac:lia as x Hx
rewrite <- Z2Nat.idi by lia
rewrite HbZ.to_nati x ; | by apply lookup_app_l_Some
exact Forall_lookup_1_ _ _ _ Hf Hx
+intros Hk
assert Z.minZ.of_natlengthbytes n = Z.of_natlengthbytes as → by lia
apply Hblengthbytes 0
rewrite lookup_app_r ; | lia
rewrite Nat.sub_diag
reflexivity
The calls
The Iris instance of the registry and wi.
The expressions of the language.
A call that changes no memory and no world, from a ready runtime, keeps the state interpretation, with the same ghost heap, whatever the runtime state after it.
Explore proof 10 tactics
Initial goal
intros Hi
iIntros (%h & Hh & %Hf)
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
spec :
contractworld
r :
args :
listarg
xs :
listword
σ :
lstateworld
trace :
listevent
ending :
s′ :
R.state
Hf :
agreesL.ls_memσ h ∧ live_disjointL.ls_memσ ∧ R.readyL.ls_rtσ L.ls_memσ ∧ wiL.ls_memσ L.ls_worldσ h
Hh :
gen_heap_interph
∗
destruct Hf as Ha & Hd & Hr & Hw
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
spec :
contractworld
r :
args :
listarg
xs :
listword
σ :
lstateworld
trace :
listevent
ending :
s′ :
R.state
Ha :
agreesL.ls_memσ h
Hd :
live_disjointL.ls_memσ
Hr :
R.readyL.ls_rtσ L.ls_memσ
Hw :
wiL.ls_memσ L.ls_worldσ h
Hh :
gen_heap_interph
∗
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hi as born & Hp
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
spec :
contractworld
r :
args :
listarg
xs :
listword
σ :
lstateworld
trace :
listevent
ending :
s′ :
R.state
Ha :
agreesL.ls_memσ h
Hd :
live_disjointL.ls_memσ
Hr :
R.readyL.ls_rtσ L.ls_memσ
Hw :
wiL.ls_memσ L.ls_worldσ h
born :
listZ
Hh :
gen_heap_interph
∗
destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as Hr′ _
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
spec :
contractworld
r :
args :
listarg
xs :
listword
σ :
lstateworld
trace :
listevent
ending :
s′ :
R.state
Ha :
agreesL.ls_memσ h
Hd :
live_disjointL.ls_memσ
Hr :
R.readyL.ls_rtσ L.ls_memσ
Hw :
wiL.ls_memσ L.ls_worldσ h
born :
listZ
Hr′ :
R.readys′ ls_memσ
Hh :
gen_heap_interph
∗
iExists h
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
spec :
contractworld
r :
args :
listarg
xs :
listword
σ :
lstateworld
trace :
listevent
ending :
s′ :
R.state
Ha :
agreesL.ls_memσ h
Hd :
live_disjointL.ls_memσ
Hr :
R.readyL.ls_rtσ L.ls_memσ
Hw :
wiL.ls_memσ L.ls_worldσ h
born :
listZ
Hr′ :
R.readys′ ls_memσ
Hh :
gen_heap_interph
∗
gen_heap_interph ∗ ⌜agreesL.ls_memls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ h ∧ live_disjointL.ls_memls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ ∧ R.readyL.ls_rtls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ L.ls_memls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ ∧ wiL.ls_memls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ L.ls_worldls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ h⌝
iFrame Hh
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
spec :
contractworld
r :
args :
listarg
xs :
listword
σ :
lstateworld
trace :
listevent
ending :
s′ :
R.state
Ha :
agreesL.ls_memσ h
Hd :
live_disjointL.ls_memσ
Hr :
R.readyL.ls_rtσ L.ls_memσ
Hw :
wiL.ls_memσ L.ls_worldσ h
born :
listZ
Hr′ :
R.readys′ ls_memσ
∗
⌜agreesL.ls_memls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ h ∧ live_disjointL.ls_memls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ ∧ R.readyL.ls_rtls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ L.ls_memls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ ∧ wiL.ls_memls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ L.ls_worldls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ h⌝
iPureIntro
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
spec :
contractworld
r :
args :
listarg
xs :
listword
σ :
lstateworld
trace :
listevent
ending :
s′ :
R.state
Ha :
agreesL.ls_memσ h
Hd :
live_disjointL.ls_memσ
Hr :
R.readyL.ls_rtσ L.ls_memσ
Hw :
wiL.ls_memσ L.ls_worldσ h
born :
listZ
Hr′ :
R.readys′ ls_memσ
⊢
agreesL.ls_memls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ h ∧ live_disjointL.ls_memls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ ∧ R.readyL.ls_rtls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ L.ls_memls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ ∧ wiL.ls_memls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ L.ls_worldls_mem ≔ ls_memσ; ls_rt ≔ s′; ls_fuel ≔ ls_fuelσ; ls_world ≔ ls_worldσ h
cbn
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
spec :
contractworld
r :
args :
listarg
xs :
listword
σ :
lstateworld
trace :
listevent
ending :
s′ :
R.state
Ha :
agreesL.ls_memσ h
Hd :
live_disjointL.ls_memσ
Hr :
R.readyL.ls_rtσ L.ls_memσ
Hw :
wiL.ls_memσ L.ls_worldσ h
born :
listZ
Hr′ :
R.readys′ ls_memσ
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hi
iIntros (%h & Hh & %Hf)
destruct Hf as Ha & Hd & Hr & Hw
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hi as born & Hp
destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as Hr′ _
iExists h
iFrame Hh
iPureIntro
cbn
auto
strlen's triple, from strlen_contract: owning the string at p, which v reads as, the call binds d to its length.
∀ f e ls lab d v rest j p b reg bytes Φ
registryTAtom"strlen" = Somestrlen_contractworld
lookupTAtom"strlen" ge_globalsge = None
Proof 28 steps Qed
intros Hreg Hfn Hdata Hv
iIntros Hs HK
iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ strlen_contractworld WPtrp stringp b reg bytes with Hs [HK] ; done | done | done | done | cbn [ map_option ] ; rewrite Hv ; done | | |
–split ; right ; eexists ; reflexivity | eexists ; reflexivity
–iIntros σ Hσ Hs
iDestruct string_facts with Hσ Hs as %Ht _
iPureIntro
exists p, Z.of_natlengthbytes
auto
–iNext
iIntros σ trace values s′ m′ w′ Hinv Hσ Hs
iDestruct string_facts with Hσ Hs as %Ht _
destruct M.E.strlen_invocation_ _ _ _ _ _ _ _ _ _ _ _ Hinv as _ & → & → & p′ & k & Hx & Hk & He
injection Hx as ←
injection He as →
rewrite terminated_length_unique_ _ _ _ Hk Ht
iDestruct pure_return with Hσ as Hσ ; exact Hinv |
destruct σ as m s fuel w
iModIntro
iExists _
iSplit
+iPureIntro
cbn
rewrite Z.mod_small ; reflexivity |
destruct Ht as _ ?
lia
+iFrame Hσ
iApply HK with Hs
What strchr finds in the string p with contents bytes for the int c, whose low byte is not the NUL: the first byte equal to it, at offset i, with p's capability, or null if there is none.
strchr's triple, from strchr_contract: owning the string at p, which v reads as, the call binds d to what it finds of the int c, which w reads as.
∀ f e ls lab d v w rest j p b reg bytes c Φ
registryTAtom"strchr" = Somestrchr_contractworld
lookupTAtom"strchr" ge_globalsge = None
0 ≤ c < 2 ^ 32
c mod 256 ≠ 0
Proof 61 steps Qed
intros Hreg Hfn Hdata Hv Hw Hc Hnz
iIntros Hs HK
iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ strchr_contractworld WPtrp; WIntc stringp b reg bytes with Hs [HK] ; done | done | done | done | cbn [ map_option ] ; rewrite Hv Hw ; done | | |
–split ; right ; eexists ; reflexivity | do 2 eexists ; reflexivity
–iIntros σ Hσ Hs
iDestruct string_facts with Hσ Hs as %Ht _
iPureIntro
exists p, c, Z.of_natlengthbytes
auto
–iNext
iIntros σ trace values s′ m′ w′ Hinv Hσ Hs
iDestruct Hs as [%Hok Hs]
iDestruct pts_facts with Hσ Hs as %Ha & _
pose proof string_terminated_ _ _ _ _ Hok Ha as Ht
pose proof string_bytes_ _ _ _ _ Hok Ha as Hb
destruct M.E.strchr_invocation_ _ _ _ _ _ _ _ _ _ _ _ Hinv as _ & → & → & p′ & c′ & q & Hx & _ & k & Hk & Hq & He
injection Hx as ← ←
injection He as →
rewrite terminated_length_unique_ _ _ _ Hk Ht in Hq
iDestruct pure_return with Hσ as Hσ ; exact Hinv |
destruct σ as m s fuel w0
iModIntro
iExists _
iSplit ; iPureIntro ; reflexivity |
iFrame Hσ
iApply HK with [%] [Hs] ; | by iSplit
cbn [ ls_mem ] in Hb
destruct Hq as i & Hi & Hv′ & Hbefore & → | Hnone & →
+assert Hil : Z.to_nati < lengthbytes%nat
{destruct decideZ.to_nati = lengthbytes as Heq | Hne ; | lia
exfalso
apply Hnz
rewrite <- Hv'
rewrite <- Z2Nat.idi by lia
rewrite Heq
apply Hblengthbytes 0
rewrite lookup_app_r ; | lia
rewrite Nat.sub_diag
reflexivity
destruct lookup_lt_is_Some_2bytes Z.to_nati Hil as x Hx
left
exists Z.to_nati, x
split ; exact Hx |
split
∗rewrite <- Hv'
rewrite <- Z2Nat.idi at 1 by lia
symmetry
apply Hb
by apply lookup_app_l_Some
∗split ; | rewrite Z2Nat.id ; reflexivity | lia
intros i′ x′ Hlt Hx′
specialize HbeforeZ.of_nati' ltac:lia
rewrite Hbi' x' in Hbefore ; exact Hbefore |
by apply lookup_app_l_Some
+right
split ; | reflexivity
intros i′ x′ Hx′
assert Hl : i' < lengthbytes%nat by apply lookup_lt_Some in Hx' ; exact Hx'
specialize HnoneZ.of_nati' ltac:lia
rewrite Hbi' x' in Hnone ; exact Hnone |
by apply lookup_app_l_Some
strcmp's triple, from strcmp_contract: owning the strings at p and q, which v and w read as, the call binds d to an int. Which int does not matter to a caller that only branches on it.
∀ f e ls lab d v w rest j p b reg xs q b′ reg′ ys Φ
registryTAtom"strcmp" = Somestrcmp_contractworld
lookupTAtom"strcmp" ge_globalsge = None
Proof 21 steps Qed
intros Hreg Hfn Hdata Hv Hw
iIntros Hs Ht HK
iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ strcmp_contractworld WPtrp; WPtrq stringp b reg xs ∗ stringq b' reg' ys with [$Hs $Ht] [HK] ; done | done | done | done | cbn [ map_option ] ; rewrite Hv Hw ; done | | |
–split ; right ; eexists ; reflexivity | do 2 eexists ; reflexivity
–iIntros σ Hσ [Hs Ht]
iDestruct string_facts with Hσ Hs as %Hp _
iDestruct string_facts with Hσ Ht as %Hq _
iPureIntro
exists p, q, Z.of_natlengthxs, Z.of_natlengthys
auto
–iNext
iIntros σ trace values s′ m′ w′ Hinv Hσ [Hs Ht]
destruct M.E.strcmp_invocation_ _ _ _ _ _ _ _ _ _ _ _ Hinv as _ & → & → & p′ & q′ & bits & Hx & _ & He
injection He as →
iDestruct pure_return with Hσ as Hσ ; exact Hinv |
destruct σ as m s fuel w0
iModIntro
iExists _
iSplit ; iPureIntro ; reflexivity |
iFrame Hσ
iApply HK with Hs Ht
strncmp's triple, from strncmp_contract: owning the strings at p and q, which v and w read as, compared up to n bytes, which u reads as, the call binds d to an int.
∀ f e ls lab d v w u rest j p b reg xs q b′ reg′ ys n Φ
registryTAtom"strncmp" = Somestrncmp_contractworld
lookupTAtom"strncmp" ge_globalsge = None
0 ≤ n < 2 ^ 64
Proof 22 steps Qed
intros Hreg Hfn Hdata Hv Hw Hu Hn
iIntros Hs Ht HK
iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ strncmp_contractworld WPtrp; WPtrq; WIntn stringp b reg xs ∗ stringq b' reg' ys with [$Hs $Ht] [HK] ; done | done | done | done | cbn [ map_option ] ; rewrite Hv Hw Hu ; done | | |
–split ; right ; eexists ; reflexivity | do 3 eexists ; reflexivity
–iIntros σ Hσ [[%Hok Hs] [%Hok′ Ht]]
iDestruct pts_facts with Hσ Hs as %Ha & _
iDestruct pts_facts with Hσ Ht as %Ha′ & _
iPureIntro
do 5 eexists
split ; reflexivity |
split ; exact string_bounded_ _ _ _ _ _ Hok Ha Hn | exact string_bounded_ _ _ _ _ _ Hok' Ha' Hn
–iNext
iIntros σ trace values s′ m′ w′ Hinv Hσ [Hs Ht]
destruct M.E.strncmp_invocation_ _ _ _ _ _ _ _ _ _ _ _ Hinv as _ & → & → & p′ & q′ & n′ & bits & Hx & _ & He
injection He as →
iDestruct pure_return with Hσ as Hσ ; exact Hinv |
destruct σ as m s fuel w0
iModIntro
iExists _
iSplit ; iPureIntro ; reflexivity |
iFrame Hσ
iApply HK with Hs Ht
strrchr's triple, from strrchr_contract: owning the string at p, which v reads as, the call binds d to null or to a pointer into the string before its NUL, with p's capability, for an int c, which w reads as, whose low byte is not the NUL.
∀ f e ls lab d v w rest j p b reg bytes c Φ
registryTAtom"strrchr" = Somestrrchr_contractworld
lookupTAtom"strrchr" ge_globalsge = None
0 ≤ c < 2 ^ 32
c mod 256 ≠ 0
stringp b reg bytes −∗ ▷∀q, ⌜q = mkPtr0 CNone ∨ ∃i, i < lengthbytes%nat ∧ q = mkPtrptr_addrp + Z.of_nati ptr_capp⌝ −∗ stringp b reg bytes −∗ WPERunmkFramef putd WPtrq e ls None Execlab rest j : sexpr {Φ} −∗ WPERunmkFramef e ls None Execlab CallCResultd P GlobalTAtom"strrchr" ArgP v; ArgW w :: rest j : sexpr {Φ}
Proof 40 steps Qed
intros Hreg Hfn Hdata Hv Hw Hc Hnz
iIntros Hs HK
iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ strrchr_contractworld WPtrp; WIntc stringp b reg bytes with Hs [HK] ; done | done | done | done | cbn [ map_option ] ; rewrite Hv Hw ; done | | |
–split ; right ; eexists ; reflexivity | do 2 eexists ; reflexivity
–iIntros σ Hσ Hs
iDestruct string_facts with Hσ Hs as %Ht _
iPureIntro
exists p, c, Z.of_natlengthbytes
auto
–iNext
iIntros σ trace values s′ m′ w′ Hinv Hσ Hs
iDestruct Hs as [%Hok Hs]
iDestruct pts_facts with Hσ Hs as %Ha & _
pose proof string_terminated_ _ _ _ _ Hok Ha as Ht
pose proof string_bytes_ _ _ _ _ Hok Ha as Hb
destruct M.E.strrchr_invocation_ _ _ _ _ _ _ _ _ _ _ _ Hinv as _ & → & → & p′ & c′ & q & Hx & _ & k & Hk & Hq & He
injection Hx as ← ←
injection He as →
rewrite terminated_length_unique_ _ _ _ Hk Ht in Hq
iDestruct pure_return with Hσ as Hσ ; exact Hinv |
destruct σ as m s fuel w0
iModIntro
iExists _
iSplit ; iPureIntro ; reflexivity |
iFrame Hσ
iApply HK with [%] [Hs] ; | by iSplit
cbn [ ls_mem ] in Hb
destruct Hq as i & Hi & Hv′ & _ & → | _ & → ; right | left ; reflexivity
exists Z.to_nati
split ; | rewrite Z2Nat.id ; reflexivity | lia
destruct decideZ.to_nati = lengthbytes as Heq | Hne ; | lia
exfalso
apply Hnz
rewrite <- Hv'
rewrite <- Z2Nat.idi by lia
rewrite Heq
apply Hblengthbytes 0
rewrite lookup_app_r ; | lia
rewrite Nat.sub_diag
reflexivity
puts
572Context rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop registry : name → optioncontractstdio_world `{!SafepointStablestdio_wirep} ge : genv
The Iris instance of the registry and stdio_wi.
The expressions of the language.
puts's triple, from puts_contract: owning the string at p, which v reads as, the call binds d to the int it returns, n modulo 2^32, and the string is still owned: puts writes only its world's roots, which stdio_wi keeps apart from it.
∀ f e ls lab d v rest j p b reg bytes Φ
registryTAtom"puts" = Someputs_contractrep requests
lookupTAtom"puts" ge_globalsge = None
Proof 23 steps Qed
intros Hreg Hfn Hdata Hv
iIntros Hs HK
iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ puts_contractrep requests WPtrp stringp b reg bytes with Hs [HK] ; done | done | done | done | cbn [ map_option ] ; rewrite Hv ; done | | |
–split ; right ; eexists ; reflexivity | eexists ; reflexivity
–iIntros σ Hσ Hs
iDestruct string_facts with Hσ Hs as %_ Hc
iDestruct Hσ as h [_ %Hf]
destruct Hf as _ & _ & _ & Hrep & Hw & _
iPureIntro
split ; exact Hrep |
split ; exact Hw |
exists p, bytes
auto
–iNext
iIntros σ trace values s′ m′ w′ Hinv (%h & Hh & %Hf) Hs
destruct Hf as Ha & Hd & Hr & Hwi
destruct puts_return_frame_ _ _ _ _ _ _ _ _ _ _ _ _ h Hinv Ha Hd Hr Hwi as Ha′ & Hd′ & Hr′ & Hwi′
destruct puts_returns_int_ _ _ _ _ _ _ _ _ _ _ _ _ Hinv as n & →
iModIntro
iExists _
iSplit ; iPureIntro ; reflexivity |
iSplitL Hh ; iExists h ; iFrame Hh ; iPureIntro ; auto |
iApply HK with Hs
StringLogicOn over a Logic instance of its own.