rocq/theories/HelloConv.v
GNU Hello's conversion of its greeting through the program logic of Logic.v (docs/logic.md): libc's mbrtowc, and gnulib's rpl_mbrtowc and rpl_mbsrtowcs around it, which main calls to turn the greeting into wide characters.
mbrtowc(out, src, n, state) writes three cells the program owns: the wide character at out, the conversion state and errno. Its triple (wp_mbrtowc) takes the three as whole blocks, with their life, bytes and aux slots, and hands them back holding whatever the memory holds after the call, which conv_result describes: Campaign 4's mbrtowc_result read through the owned bytes, under the audited codec. ContractFrame.v's prefix_agrees_out keeps every other piece agreeing, though the call's roots now meet the program's objects.
The world is Libc.v's libc_world. The triple is generic in the world interpretation wi, given that wi makes libc ready, fixes the codec and the errno cell, keeps libc's private roots, releases and capabilities apart from the program's objects (libc_private), and survives the call's writes into the three blocks. The audited codec premise (Haudit) stays explicit, as docs/logic.md records: it is not derived from the locale.
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 StepRules Symbolic ExternalCalls ExternalMachine Pieces Heap ContractFrame Language Logic StringLogic MemLogic LentLogic Locale LocaleLogic Libc HelloModule HelloLeaf HelloLocale
Open Scope Z_scope
Open Scope list_scope
Memory read as lists
The n bytes of the memory m from the address a.
The n aux slots of the memory m from the address a.
As le_value(Bytes, U): the little-endian integer of the bytes xs.
fold_rightλx acc ⇒ x + 256 × acc 0 xs
As many bytes as asked for.
Explore proof 3 tactics
Source script
As many slots as asked for.
Explore proof 3 tactics
Source script
The memory reads back the bytes xs it holds from a.
Explore proof 12 tactics
Initial goal
intros H
apply list_eq
intros i
unfold mem_bytes
rewrite list_lookup_fmap
destruct xs !! i as x | eqn: E
2 open–rewrite lookup_seq_lt ; | exact lookup_lt_Some_ _ _ E
2 opencbn
2 openf_equal
2 openexact Hi x E
–rewrite lookup_seq_ge ; reflexivity |
exact lookup_ge_None_1_ _ E
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros H
apply list_eq
intros i
unfold mem_bytes
rewrite list_lookup_fmap
destruct xs !! i as x | eqn: E
–rewrite lookup_seq_lt ; | exact lookup_lt_Some_ _ _ E
cbn
f_equal
exact Hi x E
–rewrite lookup_seq_ge ; reflexivity |
exact lookup_ge_None_1_ _ E
A four-byte load is the little-endian value of the four bytes.
∀ m a
load_bytesm a 4 = le_valuemem_bytesm a 4
Explore proof 4 tactics
Initial goal
m :
a :
Z
⊢
load_bytesm a 4 = le_valuemem_bytesm a 4
unfold load_bytes , le_value , mem_bytes
change Z.to_nat4 with 4%nat
cbn
ring
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The state bytes of mbrtowc_pre are the eight bytes at state.
∀ m p
mbstate_bytesm p = mem_bytesm ptr_addrp 8
Explore proof 1 tactics
Initial goal
⊢
mbstate_bytesm p = mem_bytesm ptr_addrp 8
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
reflexivity
Spans of live objects
Spans inside two different live objects are apart.
Explore proof 4 tactics
Initial goal
intros Hd H1 H2 Hne
unfold spans_apart
⊢
b1 ≤ ptr_addrp1 → ptr_addrp1 + n1 ≤ r_endr1 → b2 ≤ ptr_addrp2 → ptr_addrp2 + n2 ≤ r_endr2 → ptr_addrspan_ptrspan_ptr ≔ p1; span_size ≔ n1 + span_sizespan_ptr ≔ p1; span_size ≔ n1 ≤ ptr_addrspan_ptrspan_ptr ≔ p2; span_size ≔ n2 ∨ ptr_addrspan_ptrspan_ptr ≔ p2; span_size ≔ n2 + span_sizespan_ptr ≔ p2; span_size ≔ n2 ≤ ptr_addrspan_ptrspan_ptr ≔ p1; span_size ≔ n1
cbn
destruct Hd_ _ _ _ H1 H2 Hne ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A span apart from an object's whole extent is apart from every span inside it.
∀ s b reg p n
spans_aparts mkSpanp n
Explore proof 3 tactics
Initial goal
unfold spans_apart
⊢
ptr_addrspan_ptrs + span_sizes ≤ ptr_addrspan_ptrspan_ptr ≔ ptr_addr ≔ b; ptr_cap ≔ Objb; span_size ≔ r_endreg − b ∨ ptr_addrspan_ptrspan_ptr ≔ ptr_addr ≔ b; ptr_cap ≔ Objb; span_size ≔ r_endreg − b + span_sizespan_ptr ≔ ptr_addr ≔ b; ptr_cap ≔ Objb; span_size ≔ r_endreg − b ≤ ptr_addrspan_ptrs → b ≤ ptr_addrp → ptr_addrp + n ≤ r_endreg → ptr_addrspan_ptrs + span_sizes ≤ ptr_addrspan_ptrspan_ptr ≔ p; span_size ≔ n ∨ ptr_addrspan_ptrspan_ptr ≔ p; span_size ≔ n + span_sizespan_ptr ≔ p; span_size ≔ n ≤ ptr_addrspan_ptrs
cbn
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Apart spans share no address.
Explore proof 2 tactics
Initial goal
s, t :
a :
Z
⊢
spans_aparts t → span_containss a → ¬span_containst a
unfold spans_apart , span_contains
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
unfold spans_apart , span_contains
lia
The bytes xs from offset o of the live object b, where they agree: in its bounds, and held by the memory.
Explore proof 13 tactics
Initial goal
intros Hl Ha Hne
destruct xs as | x0 xs′ ; congruence |
destruct byte_ps_agreem b reg o x0 :: xs′ 0 x0 Hl Ha eq_refl as _ & H0 & _
destruct lookup_lt_is_Some_2x0 :: xs′ lengthxs′ ltac:cbn ; lia as y Hy
destruct byte_ps_agree_ _ _ _ _ _ _ Hl Ha Hy as _ & _ & H1
cbn [ length ] in *
split ; lia |
split ; lia |
intros i x Hx
destruct byte_ps_agree_ _ _ _ _ _ _ Hl Ha Hx as Hv & _
rewrite <- Hv
f_equal
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hl Ha Hne
destruct xs as | x0 xs′ ; congruence |
destruct byte_ps_agreem b reg o x0 :: xs′ 0 x0 Hl Ha eq_refl as _ & H0 & _
destruct lookup_lt_is_Some_2x0 :: xs′ lengthxs′ ltac:cbn ; lia as y Hy
destruct byte_ps_agree_ _ _ _ _ _ _ Hl Ha Hy as _ & _ & H1
cbn [ length ] in *
split ; lia |
split ; lia |
intros i x Hx
destruct byte_ps_agree_ _ _ _ _ _ _ Hl Ha Hx as Hv & _
rewrite <- Hv
f_equal
lia
A block after a call
The block of k bytes from offset o of the object b, live in m' with the region reg and in its bounds, holding what m' holds there, agrees with m'.
Explore proof 36 tactics
Initial goal
intros Hl Ho He Hin
unfold block_ps in Hin
apply elem_of_cons in Hin as Hin | Hin
2 open⊢
agree_piecem′ l v
{injection Hin as → →
2 open⊢
agree_piecem′ PLiveb VLivereg
exact Hl
assert Hreg : registeredm′ b by destruct Hl as E _ ; unfold registered ; congruence
apply elem_of_app in Hin as Hin | Hin
2 openm′ :
b :
Z
reg :
o :
Z
k :
nat
l :
v :
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
Hreg :
registeredm′ b
⊢
agree_piecem′ l v
focused goal
m′ :
b :
Z
reg :
o :
Z
k :
nat
l :
v :
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
Hreg :
registeredm′ b
⊢
agree_piecem′ l v
–apply byte_ps_elem in Hin as i & x & Hx & → & →
2 openm′ :
b :
Z
reg :
o :
Z
k :
nat
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
x :
Z
Hx :
mem_bytesm′ b + o k !! i = Somex
Hreg :
registeredm′ b
⊢
agree_piecem′ PByteb o + i VBytex
deferred goal
m′ :
b :
Z
reg :
o :
Z
k :
nat
l :
v :
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
Hreg :
registeredm′ b
⊢
agree_piecem′ l v
unfold mem_bytes in Hx
2 openm′ :
b :
Z
reg :
o :
Z
k :
nat
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
x :
Z
Hx :
λi : nat ⇒ m_bytesm′ b + o + i <$> seq0 k !! i = Somex
Hreg :
registeredm′ b
⊢
agree_piecem′ PByteb o + i VBytex
deferred goal
m′ :
b :
Z
reg :
o :
Z
k :
nat
l :
v :
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
Hreg :
registeredm′ b
⊢
agree_piecem′ l v
apply list_lookup_fmap_Some in Hx as i′ & → & Hi
2 openm′ :
b :
Z
reg :
o :
Z
k :
nat
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i, i′ :
nat
Hi :
seq0 k !! i = Somei′
Hreg :
registeredm′ b
⊢
agree_piecem′ PByteb o + i VBytem_bytesm′ b + o + i′
deferred goal
m′ :
b :
Z
reg :
o :
Z
k :
nat
l :
v :
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
Hreg :
registeredm′ b
⊢
agree_piecem′ l v
apply lookup_seq in Hi as → Hi
2 openm′ :
b :
Z
reg :
o :
Z
k :
nat
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
Hi :
i < k%nat
Hreg :
registeredm′ b
⊢
agree_piecem′ PByteb o + i VBytem_bytesm′ b + o + 0 + i%nat
deferred goal
m′ :
b :
Z
reg :
o :
Z
k :
nat
l :
v :
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
Hreg :
registeredm′ b
⊢
agree_piecem′ l v
cbn [ agree_piece ]
2 openm′ :
b :
Z
reg :
o :
Z
k :
nat
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
Hi :
i < k%nat
Hreg :
registeredm′ b
⊢
registeredm′ b ∧ in_livem′ b o + i m_bytesm′ b + o + i = m_bytesm′ b + o + 0 + i%nat
deferred goal
m′ :
b :
Z
reg :
o :
Z
k :
nat
l :
v :
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
Hreg :
registeredm′ b
⊢
agree_piecem′ l v
split ; exact Hreg |
2 openm′ :
b :
Z
reg :
o :
Z
k :
nat
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
Hi :
i < k%nat
Hreg :
registeredm′ b
deferred goal
m′ :
b :
Z
reg :
o :
Z
k :
nat
l :
v :
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
Hreg :
registeredm′ b
⊢
agree_piecem′ l v
intros reg′ E L
2 openm′ :
b :
Z
reg :
o :
Z
k :
nat
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
Hi :
i < k%nat
Hreg :
registeredm′ b
reg′ :
E :
object_regionb m_regionsm′ = Somereg′
deferred goal
m′ :
b :
Z
reg :
o :
Z
k :
nat
l :
v :
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
Hreg :
registeredm′ b
⊢
agree_piecem′ l v
destruct Hl as E0 _
2 openm′ :
b :
Z
reg :
o :
Z
k :
nat
E0 :
object_regionb m_regionsm′ = Somereg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
Hi :
i < k%nat
Hreg :
registeredm′ b
reg′ :
E :
object_regionb m_regionsm′ = Somereg′
deferred goal
m′ :
b :
Z
reg :
o :
Z
k :
nat
l :
v :
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
Hreg :
registeredm′ b
⊢
agree_piecem′ l v
rewrite E0 in E
2 openm′ :
b :
Z
reg :
o :
Z
k :
nat
E0 :
object_regionb m_regionsm′ = Somereg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
Hi :
i < k%nat
Hreg :
registeredm′ b
reg′ :
E :
Somereg = Somereg′
deferred goal
m′ :
b :
Z
reg :
o :
Z
k :
nat
l :
v :
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
Hreg :
registeredm′ b
⊢
agree_piecem′ l v
injection E as ←
2 openm′ :
b :
Z
reg :
o :
Z
k :
nat
E0 :
object_regionb m_regionsm′ = Somereg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
Hi :
i < k%nat
Hreg :
registeredm′ b
deferred goal
m′ :
b :
Z
reg :
o :
Z
k :
nat
l :
v :
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
Hreg :
registeredm′ b
⊢
agree_piecem′ l v
split ; lia |
2 openm′ :
b :
Z
reg :
o :
Z
k :
nat
E0 :
object_regionb m_regionsm′ = Somereg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
Hi :
i < k%nat
Hreg :
registeredm′ b
deferred goal
m′ :
b :
Z
reg :
o :
Z
k :
nat
l :
v :
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
Hreg :
registeredm′ b
⊢
agree_piecem′ l v
split ; lia |
2 openm′ :
b :
Z
reg :
o :
Z
k :
nat
E0 :
object_regionb m_regionsm′ = Somereg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
Hi :
i < k%nat
Hreg :
registeredm′ b
deferred goal
m′ :
b :
Z
reg :
o :
Z
k :
nat
l :
v :
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
Hreg :
registeredm′ b
⊢
agree_piecem′ l v
f_equal
2 openm′ :
b :
Z
reg :
o :
Z
k :
nat
E0 :
object_regionb m_regionsm′ = Somereg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
Hi :
i < k%nat
Hreg :
registeredm′ b
⊢
b + o + i = b + o + 0 + i%nat
deferred goal
m′ :
b :
Z
reg :
o :
Z
k :
nat
l :
v :
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
Hreg :
registeredm′ b
⊢
agree_piecem′ l v
lia
deferred goal
m′ :
b :
Z
reg :
o :
Z
k :
nat
l :
v :
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
Hreg :
registeredm′ b
⊢
agree_piecem′ l v
–apply aux_ps_elem in Hin as i & c & Hc & → & →
m′ :
b :
Z
reg :
o :
Z
k :
nat
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
c :
Hc :
mem_auxesm′ b + o k !! i = Somec
Hreg :
registeredm′ b
⊢
agree_piecem′ PAuxb o + i VAuxc
unfold mem_auxes in Hc
m′ :
b :
Z
reg :
o :
Z
k :
nat
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
c :
Hc :
λi : nat ⇒ m_auxm′ b + o + i <$> seq0 k !! i = Somec
Hreg :
registeredm′ b
⊢
agree_piecem′ PAuxb o + i VAuxc
apply list_lookup_fmap_Some in Hc as i′ & → & Hi
m′ :
b :
Z
reg :
o :
Z
k :
nat
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i, i′ :
nat
Hi :
seq0 k !! i = Somei′
Hreg :
registeredm′ b
⊢
agree_piecem′ PAuxb o + i VAuxm_auxm′ b + o + i′
apply lookup_seq in Hi as → Hi
m′ :
b :
Z
reg :
o :
Z
k :
nat
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
Hi :
i < k%nat
Hreg :
registeredm′ b
⊢
agree_piecem′ PAuxb o + i VAuxm_auxm′ b + o + 0 + i%nat
cbn [ agree_piece ]
m′ :
b :
Z
reg :
o :
Z
k :
nat
Hl :
live_atm′ b reg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
Hi :
i < k%nat
Hreg :
registeredm′ b
⊢
registeredm′ b ∧ in_livem′ b o + i aux_holdsm′ b + o + i m_auxm′ b + o + 0 + i%nat
split ; exact Hreg |
intros reg′ E L
destruct Hl as E0 _
m′ :
b :
Z
reg :
o :
Z
k :
nat
E0 :
object_regionb m_regionsm′ = Somereg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
Hi :
i < k%nat
Hreg :
registeredm′ b
reg′ :
E :
object_regionb m_regionsm′ = Somereg′
rewrite E0 in E
injection E as ←
split ; lia |
split ; lia |
m′ :
b :
Z
reg :
o :
Z
k :
nat
E0 :
object_regionb m_regionsm′ = Somereg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
Hi :
i < k%nat
Hreg :
registeredm′ b
left
m′ :
b :
Z
reg :
o :
Z
k :
nat
E0 :
object_regionb m_regionsm′ = Somereg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
Hi :
i < k%nat
Hreg :
registeredm′ b
f_equal
m′ :
b :
Z
reg :
o :
Z
k :
nat
E0 :
object_regionb m_regionsm′ = Somereg
Ho :
0 ≤ o
He :
b + o + k ≤ r_endreg
i :
nat
Hi :
i < k%nat
Hreg :
registeredm′ b
⊢
b + o + i = b + o + 0 + i%nat
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hl Ho He Hin
unfold block_ps in Hin
apply elem_of_cons in Hin as Hin | Hin
{injection Hin as → →
exact Hl
assert Hreg : registeredm′ b by destruct Hl as E _ ; unfold registered ; congruence
apply elem_of_app in Hin as Hin | Hin
–apply byte_ps_elem in Hin as i & x & Hx & → & →
unfold mem_bytes in Hx
apply list_lookup_fmap_Some in Hx as i′ & → & Hi
apply lookup_seq in Hi as → Hi
cbn [ agree_piece ]
split ; exact Hreg |
intros reg′ E L
destruct Hl as E0 _
rewrite E0 in E
injection E as ←
split ; lia |
split ; lia |
f_equal
lia
–apply aux_ps_elem in Hin as i & c & Hc & → & →
unfold mem_auxes in Hc
apply list_lookup_fmap_Some in Hc as i′ & → & Hi
apply lookup_seq in Hi as → Hi
cbn [ agree_piece ]
split ; exact Hreg |
intros reg′ E L
destruct Hl as E0 _
rewrite E0 in E
injection E as ←
split ; lia |
split ; lia |
left
f_equal
lia
A byte or aux piece of a live object, inside its bounds at an address inside the k bytes from offset o of the live object b, is among the keys of the block there.
Explore proof 8 tactics
Initial goal
intros Hd Hl Ho He Hc Hk Hl′ Ho′ He′ Ha
assert b′ = b as →
2 openm :
b :
Z
reg :
o :
Z
xs :
listZ
cs :
listcap
l :
b′, o′ :
Z
reg′ :
Hd :
Hl :
live_atm b reg
Ho :
0 ≤ o
He :
b + o + lengthxs ≤ r_endreg
Hc :
lengthcs = lengthxs
Hl′ :
live_atm b′ reg′
Ho′ :
0 ≤ o′
He′ :
b′ + o′ < r_endreg′
Ha :
b + o ≤ b′ + o′ < b + o + lengthxs
⊢
b′ = b
{destruct Z.eq_decb′ b as E | Hne ; exact E |
2 openm :
b :
Z
reg :
o :
Z
xs :
listZ
cs :
listcap
l :
b′, o′ :
Z
reg′ :
Hd :
Hl :
live_atm b reg
Ho :
0 ≤ o
He :
b + o + lengthxs ≤ r_endreg
Hc :
lengthcs = lengthxs
Hl′ :
live_atm b′ reg′
Ho′ :
0 ≤ o′
He′ :
b′ + o′ < r_endreg′
Ha :
b + o ≤ b′ + o′ < b + o + lengthxs
Hne :
b′ ≠ b
⊢
b′ = b
destruct Hd_ _ _ _ Hl′ Hl Hne ; lia
rewrite fmap_app
apply elem_of_app
replace o′ with o + o′ − o in Hk by lia
destruct Hk as → | → ; left ; apply byte_ps_key | right ; apply aux_ps_key ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hd Hl Ho He Hc Hk Hl′ Ho′ He′ Ha
assert b′ = b as →
{destruct Z.eq_decb′ b as E | Hne ; exact E |
destruct Hd_ _ _ _ Hl′ Hl Hne ; lia
rewrite fmap_app
apply elem_of_app
replace o′ with o + o′ − o in Hk by lia
destruct Hk as → | → ; left ; apply byte_ps_key | right ; apply aux_ps_key ; lia
What owning a block of the bytes xs tells about the memory: its object is live, the bytes are in its bounds, and the memory holds them.
Explore proof 18 tactics
Initial goal
intros Ha Hlk Hne
assert Hl : live_atm b reg
2 openfocused goal
{apply HaPLiveb VLivereg , Hlk
2 opendeferred goal
apply elem_of_cons
2 opendeferred goal
left
2 opendeferred goal
reflexivity
deferred goal
assert Hx : all_agreem byte_psb o xs
2 open{apply all_agree_intro
2 open⊢
∀l : piece v : pval, l, v ∈ byte_psb o xs → agree_piecem l v
intros l v Hin
2 openm :
b :
Z
reg :
o :
Z
xs :
listZ
cs :
listcap
Ha :
agreesm h
Hne :
xs ≠ [ ]
Hl :
live_atm b reg
l :
v :
Hin :
l, v ∈ byte_psb o xs
⊢
agree_piecem l v
apply Ha , Hlk
2 openm :
b :
Z
reg :
o :
Z
xs :
listZ
cs :
listcap
Ha :
agreesm h
Hne :
xs ≠ [ ]
Hl :
live_atm b reg
l :
v :
Hin :
l, v ∈ byte_psb o xs
⊢
l, v ∈ block_psb reg o xs cs
unfold block_ps
2 openapply elem_of_cons
2 openright
2 openapply elem_of_app
2 openleft
2 openm :
b :
Z
reg :
o :
Z
xs :
listZ
cs :
listcap
Ha :
agreesm h
Hne :
xs ≠ [ ]
Hl :
live_atm b reg
l :
v :
Hin :
l, v ∈ byte_psb o xs
⊢
l, v ∈ byte_psb o xs
exact Hin
split ; exact Hl |
exact byte_block_factsm b reg o xs Hl Hx Hne
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Ha Hlk Hne
assert Hl : live_atm b reg
{apply all_agree_intro
intros l v Hin
apply Ha , Hlk
unfold block_ps
apply elem_of_cons
right
apply elem_of_app
left
exact Hin
split ; exact Hl |
exact byte_block_factsm b reg o xs Hl Hx Hne
A list of length k + 1 is not empty.
Explore proof 2 tactics
Initial goal
A :
Type
xs :
listA
k :
nat
⊢
lengthxs = Sk → xs ≠ [ ]
intros H →
A :
Type
k :
nat
H :
length[ ] = Sk
⊢
False
discriminate H
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros H →
discriminate H
A block's byte and aux keys hold no life piece.
Explore proof 3 tactics
Initial goal
rewrite fmap_app byte_ps_keys aux_ps_keys
intros Hin
apply elem_of_app in Hin as Hin | Hin ; apply list_elem_of_fmap in Hin as ? & E & _ ; discriminate E
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
rewrite fmap_app byte_ps_keys aux_ps_keys
intros Hin
apply elem_of_app in Hin as Hin | Hin ; apply list_elem_of_fmap in Hin as ? & E & _ ; discriminate E
A block's byte and aux keys are keys of the block after a call, of as many bytes and slots.
Explore proof 7 tactics
Initial goal
intros Hx Hc Hin
rewrite block_ps_keysb reg o xs cs ; | rewrite length_mem_bytes ; auto | rewrite length_mem_auxes ; auto
unfold block_ps
rewrite fmap_cons
apply elem_of_cons
right
exact Hin
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hx Hc Hin
rewrite block_ps_keysb reg o xs cs ; | rewrite length_mem_bytes ; auto | rewrite length_mem_auxes ; auto
unfold block_ps
rewrite fmap_cons
apply elem_of_cons
right
exact Hin
libc's private state
libc's private state keeps apart from the program's objects: no piece of h is of an object libc may release, and of every live object owning a piece of h, every private root lies outside its extent and libc's private sources hand out none of its capabilities.
ids_apartlocale_ownedlibc_localefstw h ∧ ∀l v reg, h !! l = Somev → mem_piecel → live_atm piece_idl reg → ∀root, Inroot locale_rootslibc_localefstw → spans_apartroot mkSpanmkPtrpiece_idl Objpiece_idl r_endreg − piece_idl ∧ ¬available_caplocale_sources[ ] m libc_localefstw [ ] m Objpiece_idl ∧ ¬available_caplocale_sources[ ] m libc_localefstw [ ] m Ropiece_idl
What the program learns from mbrtowc(out, src, n, state) returning r, for 0 < n and the audited codec, read through the bytes it owns (mbrtowc_result): ss are the source bytes and xo the output's bytes before the call; xo', ys' and xe' the output's, state's and errno's bytes after it. A NUL converts to 0 and resets the state; a character of r bytes, none of them NUL, to a nonzero wide character; an invalid sequence sets errno to EILSEQ (84); an incomplete one, under the audited codec, is shorter than 16 bytes with no NUL. Under the audited C codec (CodecC) an invalid sequence keeps the state's bytes ys and starts with a byte of 128 or more (mbrtowc_c_error).
218Definition conv_resultvalid : term → listZ → Prop c_codec : Prop codec : term n : Z ss xo ys xo′ ys′ xe′ : listZ r : Z : Prop ≔
r = 0 ∧ validcodec ys′ ∧ ∃i, i < Z.to_natn%nat ∧ ss !! i = Some0 ∧ le_valuexo′ = 0 ∧ le_valuetake4 ys′ = 0 ∨ 0 < r ≤ n ∧ r < 2 ^ 64 − 2 ∧ validcodec ys′ ∧ 0 < le_valuexo′ < 2 ^ 32 ∧ le_valuetake4 ys′ = 0 ∧ Forallλx ⇒ x ≠ 0 takeZ.to_natr ss ∨ r = 2 ^ 64 − 1 ∧ le_valuexe′ = 84 ∧ xo′ = xo ∧ c_codec → ys′ = ys ∧ ∃x, ss !! 0%nat = Somex ∧ 128 ≤ x < 256 ∧ validcodec ys → le_valuetake4 ys = 0 → validcodec ys′ ∧ le_valuetake4 ys′ = 0 ∧ ∃x, ss !! 0%nat = Somex ∧ x ≠ 0 ∨ r = 2 ^ 64 − 2 ∧ validcodec ys′ ∧ xo′ = xo ∧ n < 16 ∧ Forallλx ⇒ x ≠ 0 takeZ.to_natn ss
gnulib's rpl_mbrtowc
rpl_mbrtowc(pwc, s, n, ps): mbrtowc into pwc, or into a local if pwc is null; on an invalid or incomplete sequence, outside a hard locale, the first byte stands for itself.
A block of rpl_mbrtowc.
rpl_mbrtowc's entry binds its four arguments.
Explore proof 1 tactics
Initial goal
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
reflexivity
A signed byte load, then its low byte unsigned: the byte.
Explore proof 17 tactics
Initial goal
intros Hx
cbn [ extension ]
x :
Z
Hx :
0 ≤ x < 256
⊢
sign_extension256 128 x mod 2 ^ 32 mod 256 mod 2 ^ 32 = x
unfold sign_extension
x :
Z
Hx :
0 ≤ x < 256
⊢
128 ≤? x mod 256
→
x mod 256 − 256
else
x mod 256
mod
2 ^ 32
mod
256
mod
2 ^ 32
=
x
assert E : x mod 256 = x by apply Z.mod_small ; lia
x :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
⊢
128 ≤? x mod 256
→
x mod 256 − 256
else
x mod 256
mod
2 ^ 32
mod
256
mod
2 ^ 32
=
x
rewrite E
x :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
⊢
128 ≤? x
→
x − 256
else
x
mod
2 ^ 32
mod
256
mod
2 ^ 32
=
x
destruct Z.leb_spec128 x as Hh | Hh
2 openx :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
128 ≤ x
⊢
x − 256 mod 2 ^ 32 mod 256 mod 2 ^ 32 = x
focused goal
x :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
x < 128
⊢
x mod 2 ^ 32 mod 256 mod 2 ^ 32 = x
–assert E2 : x − 256 mod 2 ^ 32 = x − 256 + 2 ^ 32 by symmetry ; apply Z.mod_unique with −1 ; lia
2 openx :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
128 ≤ x
E2 :
x − 256 mod 2 ^ 32 = x − 256 + 2 ^ 32
⊢
x − 256 mod 2 ^ 32 mod 256 mod 2 ^ 32 = x
deferred goal
x :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
x < 128
⊢
x mod 2 ^ 32 mod 256 mod 2 ^ 32 = x
rewrite E2
2 openx :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
128 ≤ x
E2 :
x − 256 mod 2 ^ 32 = x − 256 + 2 ^ 32
⊢
x − 256 + 2 ^ 32 mod 256 mod 2 ^ 32 = x
deferred goal
x :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
x < 128
⊢
x mod 2 ^ 32 mod 256 mod 2 ^ 32 = x
assert E3 : x − 256 + 2 ^ 32 mod 256 = x by symmetry ; apply Z.mod_unique with 2 ^ 24 − 1 ; lia
2 openx :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
128 ≤ x
E2 :
x − 256 mod 2 ^ 32 = x − 256 + 2 ^ 32
E3 :
x − 256 + 2 ^ 32 mod 256 = x
⊢
x − 256 + 2 ^ 32 mod 256 mod 2 ^ 32 = x
deferred goal
x :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
x < 128
⊢
x mod 2 ^ 32 mod 256 mod 2 ^ 32 = x
rewrite E3
2 openx :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
128 ≤ x
E2 :
x − 256 mod 2 ^ 32 = x − 256 + 2 ^ 32
E3 :
x − 256 + 2 ^ 32 mod 256 = x
⊢
x mod 2 ^ 32 = x
deferred goal
x :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
x < 128
⊢
x mod 2 ^ 32 mod 256 mod 2 ^ 32 = x
apply Z.mod_small
2 openx :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
128 ≤ x
E2 :
x − 256 mod 2 ^ 32 = x − 256 + 2 ^ 32
E3 :
x − 256 + 2 ^ 32 mod 256 = x
⊢
0 ≤ x < 2 ^ 32
deferred goal
x :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
x < 128
⊢
x mod 2 ^ 32 mod 256 mod 2 ^ 32 = x
lia
deferred goal
x :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
x < 128
⊢
x mod 2 ^ 32 mod 256 mod 2 ^ 32 = x
–assert E2 : x mod 2 ^ 32 = x by apply Z.mod_small ; lia
x :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
x < 128
E2 :
x mod 2 ^ 32 = x
⊢
x mod 2 ^ 32 mod 256 mod 2 ^ 32 = x
rewrite E2
x :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
x < 128
E2 :
x mod 2 ^ 32 = x
⊢
x mod 256 mod 2 ^ 32 = x
rewrite E
x :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
x < 128
E2 :
x mod 2 ^ 32 = x
⊢
x mod 2 ^ 32 = x
apply Z.mod_small
x :
Z
Hx :
0 ≤ x < 256
E :
x mod 256 = x
Hh :
x < 128
E2 :
x mod 2 ^ 32 = x
⊢
0 ≤ x < 2 ^ 32
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hx
cbn [ extension ]
unfold sign_extension
assert E : x mod 256 = x by apply Z.mod_small ; lia
rewrite E
destruct Z.leb_spec128 x as Hh | Hh
–assert E2 : x − 256 mod 2 ^ 32 = x − 256 + 2 ^ 32 by symmetry ; apply Z.mod_unique with −1 ; lia
rewrite E2
assert E3 : x − 256 + 2 ^ 32 mod 256 = x by symmetry ; apply Z.mod_unique with 2 ^ 24 − 1 ; lia
rewrite E3
apply Z.mod_small
lia
–assert E2 : x mod 2 ^ 32 = x by apply Z.mod_small ; lia
rewrite E2
rewrite E
apply Z.mod_small
lia
What rpl_mbrtowc's caller learns, in conv_result's terms: mbrtowc's own answer r', or, after an invalid or incomplete sequence outside a hard locale, 1, with the first byte x stored as the wide character.
263Definition rpl_resultvalid : term → listZ → Prop c_codec : Prop codec : term n : Z ss xo ys xo′ ys′ xe′ : listZ r′ : Z : Prop ≔
conv_resultvalid c_codec codec n ss xo ys xo′ ys′ xe′ r′ ∨ r′ = 1 ∧ ∃r, 2 ^ 64 − 2 ≤ r ∧ conv_resultvalid c_codec codec n ss xo ys xo ys′ xe′ r ∧ ∃x, ss !! 0%nat = Somex ∧ xo′ = le_bytesx 4
mbrtowc's answers are 64-bit words, and the two at the top are the invalid and the incomplete sequence, which leave the output alone.
∀ valid c_codec codec n ss xo ys xo′ ys′ xe′ r
conv_resultvalid c_codec codec n ss xo ys xo′ ys′ xe′ r
0 ≤ r < 2 ^ 64 ∧ 2 ^ 64 − 2 ≤ r → xo′ = xo
Explore proof 1 tactics
Initial goal
⊢
conv_resultvalid c_codec codec n ss xo ys xo′ ys′ xe′ r → 0 ≤ r < 2 ^ 64 ∧ 2 ^ 64 − 2 ≤ r → xo′ = xo
intros → & _ | Hr & Hr2 & _ | → & _ & Hx & _ | → & _ & Hx & _ ; split ; try lia ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros → & _ | Hr & Hr2 & _ | → & _ & Hx & _ | → & _ & Hx & _ ; split ; try lia ; auto
gnulib's rpl_mbsrtowcs
rpl_mbsrtowcs(dest, srcp, len, ps): converts the string at *srcp into at most len wide characters at dest, one rpl_mbrtowc call per character, each given a window of n bytes that reaches the NUL or is 16 bytes long.
A block of rpl_mbsrtowcs.
A nonzero byte loaded signed is not zero.
∀ x
0 < x < 256
128 ≤? x
→
x − 256
else
x
mod
2 ^ 32
=?
0
=
false
Explore proof 7 tactics
Initial goal
x :
Z
⊢
0 < x < 256
→
128 ≤? x
→
x − 256
else
x
mod
2 ^ 32
=?
0
=
false
intros Hx
x :
Z
Hx :
0 < x < 256
⊢
128 ≤? x
→
x − 256
else
x
mod
2 ^ 32
=?
0
=
false
apply Z.eqb_neq
x :
Z
Hx :
0 < x < 256
⊢
128 ≤? x
→
x − 256
else
x
mod
2 ^ 32
≠
0
destruct Z.leb_spec128 x
2 openx :
Z
Hx :
0 < x < 256
H :
128 ≤ x
⊢
x − 256 mod 2 ^ 32 ≠ 0
focused goal
x :
Z
Hx :
0 < x < 256
H :
x < 128
⊢
x mod 2 ^ 32 ≠ 0
–assert E : x − 256 mod 2 ^ 32 = x − 256 + 2 ^ 32 by symmetry ; apply Z.mod_unique with −1 ; lia
2 openx :
Z
Hx :
0 < x < 256
H :
128 ≤ x
E :
x − 256 mod 2 ^ 32 = x − 256 + 2 ^ 32
⊢
x − 256 mod 2 ^ 32 ≠ 0
deferred goal
x :
Z
Hx :
0 < x < 256
H :
x < 128
⊢
x mod 2 ^ 32 ≠ 0
rewrite E
2 openx :
Z
Hx :
0 < x < 256
H :
128 ≤ x
E :
x − 256 mod 2 ^ 32 = x − 256 + 2 ^ 32
⊢
x − 256 + 2 ^ 32 ≠ 0
deferred goal
x :
Z
Hx :
0 < x < 256
H :
x < 128
⊢
x mod 2 ^ 32 ≠ 0
lia
deferred goal
x :
Z
Hx :
0 < x < 256
H :
x < 128
⊢
x mod 2 ^ 32 ≠ 0
–rewrite Z.mod_small ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hx
apply Z.eqb_neq
destruct Z.leb_spec128 x
–assert E : x − 256 mod 2 ^ 32 = x − 256 + 2 ^ 32 by symmetry ; apply Z.mod_unique with −1 ; lia
rewrite E
lia
–rewrite Z.mod_small ; lia
In a string's bytes and NUL, a zero byte is the NUL.
∀ bs k x
Forallλx ⇒ 0 < x < 256 bs
bs ++ 0 !! k = Somex
0 ≤ x < 256 ∧ x = 0 → k = lengthbs ∧ x ≠ 0 → k < lengthbs%nat
Explore proof 12 tactics
Initial goal
bs :
listZ
k :
nat
x :
Z
⊢
Forallλx0 : Z ⇒ 0 < x0 < 256 bs → bs ++ 0 !! k = Somex → 0 ≤ x < 256 ∧ x = 0 → k = lengthbs ∧ x ≠ 0 → k < lengthbs%nat
intros Hbs Hk
bs :
listZ
k :
nat
x :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hk :
bs ++ 0 !! k = Somex
⊢
0 ≤ x < 256 ∧ x = 0 → k = lengthbs ∧ x ≠ 0 → k < lengthbs%nat
pose proof proj1Forall_lookup_ _ Hbs as Hb
bs :
listZ
k :
nat
x :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hk :
bs ++ 0 !! k = Somex
Hb :
∀i : nat x : Z, bs !! i = Somex → λx0 : Z ⇒ 0 < x0 < 256x
⊢
0 ≤ x < 256 ∧ x = 0 → k = lengthbs ∧ x ≠ 0 → k < lengthbs%nat
apply lookup_app_Some in Hk as Hk | Hl Hk
2 openbs :
listZ
k :
nat
x :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hk :
bs !! k = Somex
Hb :
∀i : nat x : Z, bs !! i = Somex → λx0 : Z ⇒ 0 < x0 < 256x
⊢
0 ≤ x < 256 ∧ x = 0 → k = lengthbs ∧ x ≠ 0 → k < lengthbs%nat
focused goal
bs :
listZ
k :
nat
x :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hl :
lengthbs ≤ k%nat
Hk :
0 !! k − lengthbs%nat = Somex
Hb :
∀i : nat x : Z, bs !! i = Somex → λx0 : Z ⇒ 0 < x0 < 256x
⊢
0 ≤ x < 256 ∧ x = 0 → k = lengthbs ∧ x ≠ 0 → k < lengthbs%nat
–pose proof Hb_ _ Hk as Hx
2 openbs :
listZ
k :
nat
x :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hk :
bs !! k = Somex
Hb :
∀i : nat x : Z, bs !! i = Somex → λx0 : Z ⇒ 0 < x0 < 256x
Hx :
λx : Z ⇒ 0 < x < 256x
⊢
0 ≤ x < 256 ∧ x = 0 → k = lengthbs ∧ x ≠ 0 → k < lengthbs%nat
deferred goal
bs :
listZ
k :
nat
x :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hl :
lengthbs ≤ k%nat
Hk :
0 !! k − lengthbs%nat = Somex
Hb :
∀i : nat x : Z, bs !! i = Somex → λx0 : Z ⇒ 0 < x0 < 256x
⊢
0 ≤ x < 256 ∧ x = 0 → k = lengthbs ∧ x ≠ 0 → k < lengthbs%nat
cbv beta in Hx
2 openbs :
listZ
k :
nat
x :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hk :
bs !! k = Somex
Hb :
∀i : nat x : Z, bs !! i = Somex → λx0 : Z ⇒ 0 < x0 < 256x
Hx :
0 < x < 256
⊢
0 ≤ x < 256 ∧ x = 0 → k = lengthbs ∧ x ≠ 0 → k < lengthbs%nat
deferred goal
bs :
listZ
k :
nat
x :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hl :
lengthbs ≤ k%nat
Hk :
0 !! k − lengthbs%nat = Somex
Hb :
∀i : nat x : Z, bs !! i = Somex → λx0 : Z ⇒ 0 < x0 < 256x
⊢
0 ≤ x < 256 ∧ x = 0 → k = lengthbs ∧ x ≠ 0 → k < lengthbs%nat
apply lookup_lt_Some in Hk
2 openbs :
listZ
k :
nat
x :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hk :
k < lengthbs%nat
Hb :
∀i : nat x : Z, bs !! i = Somex → λx0 : Z ⇒ 0 < x0 < 256x
Hx :
0 < x < 256
⊢
0 ≤ x < 256 ∧ x = 0 → k = lengthbs ∧ x ≠ 0 → k < lengthbs%nat
deferred goal
bs :
listZ
k :
nat
x :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hl :
lengthbs ≤ k%nat
Hk :
0 !! k − lengthbs%nat = Somex
Hb :
∀i : nat x : Z, bs !! i = Somex → λx0 : Z ⇒ 0 < x0 < 256x
⊢
0 ≤ x < 256 ∧ x = 0 → k = lengthbs ∧ x ≠ 0 → k < lengthbs%nat
split ; lia |
2 openbs :
listZ
k :
nat
x :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hk :
k < lengthbs%nat
Hb :
∀i : nat x : Z, bs !! i = Somex → λx0 : Z ⇒ 0 < x0 < 256x
Hx :
0 < x < 256
⊢
x = 0 → k = lengthbs ∧ x ≠ 0 → k < lengthbs%nat
deferred goal
bs :
listZ
k :
nat
x :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hl :
lengthbs ≤ k%nat
Hk :
0 !! k − lengthbs%nat = Somex
Hb :
∀i : nat x : Z, bs !! i = Somex → λx0 : Z ⇒ 0 < x0 < 256x
⊢
0 ≤ x < 256 ∧ x = 0 → k = lengthbs ∧ x ≠ 0 → k < lengthbs%nat
split ; intros E ; lia | auto
deferred goal
bs :
listZ
k :
nat
x :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hl :
lengthbs ≤ k%nat
Hk :
0 !! k − lengthbs%nat = Somex
Hb :
∀i : nat x : Z, bs !! i = Somex → λx0 : Z ⇒ 0 < x0 < 256x
⊢
0 ≤ x < 256 ∧ x = 0 → k = lengthbs ∧ x ≠ 0 → k < lengthbs%nat
–apply list_lookup_singleton_Some in Hk as Hk Ex
bs :
listZ
k :
nat
x :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hl :
lengthbs ≤ k%nat
Hk :
k − lengthbs%nat = 0%nat
Ex :
0 = x
Hb :
∀i : nat x : Z, bs !! i = Somex → λx0 : Z ⇒ 0 < x0 < 256x
⊢
0 ≤ x < 256 ∧ x = 0 → k = lengthbs ∧ x ≠ 0 → k < lengthbs%nat
subst x
bs :
listZ
k :
nat
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hl :
lengthbs ≤ k%nat
Hk :
k − lengthbs%nat = 0%nat
Hb :
∀i : nat x : Z, bs !! i = Somex → λx0 : Z ⇒ 0 < x0 < 256x
⊢
0 ≤ 0 < 256 ∧ 0 = 0 → k = lengthbs ∧ 0 ≠ 0 → k < lengthbs%nat
split ; lia |
bs :
listZ
k :
nat
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hl :
lengthbs ≤ k%nat
Hk :
k − lengthbs%nat = 0%nat
Hb :
∀i : nat x : Z, bs !! i = Somex → λx0 : Z ⇒ 0 < x0 < 256x
⊢
0 = 0 → k = lengthbs ∧ 0 ≠ 0 → k < lengthbs%nat
split ; intros _ ; lia | intros E ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hbs Hk
pose proof proj1Forall_lookup_ _ Hbs as Hb
apply lookup_app_Some in Hk as Hk | Hl Hk
–pose proof Hb_ _ Hk as Hx
cbv beta in Hx
apply lookup_lt_Some in Hk
split ; lia |
split ; intros E ; lia | auto
–apply list_lookup_singleton_Some in Hk as Hk Ex
subst x
split ; lia |
split ; intros _ ; lia | intros E ; lia
A window of four bytes and a count from the fifth: what strnlen1's answer plus 4 comes to.
∀ l
4 ≤ l%nat
Z.minZ.of_natl − 4 + 1 12 + 4 = Z.minZ.of_natl + 1 16
Explore proof 2 tactics
Initial goal
l :
nat
⊢
(4 <= l)%nat → ((l - 4)%nat + 1) `min` 12 + 4 = (l + 1) `min` 16intros Hl
l :
nat
Hl :
4 ≤ l%nat
⊢
((l - 4)%nat + 1) `min` 12 + 4 = (l + 1) `min` 16lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hl
lia
A byte stored as a four-byte word reads back as itself.
Explore proof 15 tactics
Initial goal
intros Hx
unfold le_bytes , le_value , byte_of
x :
Z
Hx :
0 ≤ x < 256
⊢
foldrλx0 acc : Z ⇒ x0 + 256 × acc 0 λi : nat ⇒ x / 2 ^ 8 × i mod 256 <$> seq0 4 = x
cbn
x :
Z
Hx :
0 ≤ x < 256
⊢
x / 2 ^ 8 × 0%nat mod 256 + 256 × x / 2 ^ 8 × 1%nat mod 256 + 256 × x / 2 ^ 8 × 2%nat mod 256 + 256 × x / 2 ^ 8 × 3%nat mod 256 + 256 × 0 = x
change 8 × Z.of_nat1 with 8
x :
Z
Hx :
0 ≤ x < 256
⊢
x / 2 ^ 8 × 0%nat mod 256 + 256 × x / 2 ^ 8 mod 256 + 256 × x / 2 ^ 8 × 2%nat mod 256 + 256 × x / 2 ^ 8 × 3%nat mod 256 + 256 × 0 = x
change 8 × Z.of_nat2 with 16
x :
Z
Hx :
0 ≤ x < 256
⊢
x / 2 ^ 8 × 0%nat mod 256 + 256 × x / 2 ^ 8 mod 256 + 256 × x / 2 ^ 16 mod 256 + 256 × x / 2 ^ 8 × 3%nat mod 256 + 256 × 0 = x
change 8 × Z.of_nat3 with 24
x :
Z
Hx :
0 ≤ x < 256
⊢
x / 2 ^ 8 × 0%nat mod 256 + 256 × x / 2 ^ 8 mod 256 + 256 × x / 2 ^ 16 mod 256 + 256 × x / 2 ^ 24 mod 256 + 256 × 0 = x
change 8 × Z.of_nat0 with 0
x :
Z
Hx :
0 ≤ x < 256
⊢
x / 2 ^ 0 mod 256 + 256 × x / 2 ^ 8 mod 256 + 256 × x / 2 ^ 16 mod 256 + 256 × x / 2 ^ 24 mod 256 + 256 × 0 = x
rewrite Z.pow_0_r
x :
Z
Hx :
0 ≤ x < 256
⊢
x / 1 mod 256 + 256 × x / 2 ^ 8 mod 256 + 256 × x / 2 ^ 16 mod 256 + 256 × x / 2 ^ 24 mod 256 + 256 × 0 = x
rewrite Z.div_1_r
x :
Z
Hx :
0 ≤ x < 256
⊢
x mod 256 + 256 × x / 2 ^ 8 mod 256 + 256 × x / 2 ^ 16 mod 256 + 256 × x / 2 ^ 24 mod 256 + 256 × 0 = x
rewrite Z.mod_smallx 256 ; | lia
x :
Z
Hx :
0 ≤ x < 256
⊢
x + 256 × x / 2 ^ 8 mod 256 + 256 × x / 2 ^ 16 mod 256 + 256 × x / 2 ^ 24 mod 256 + 256 × 0 = x
rewrite Z.div_smallx 2 ^ 8 ; | lia
x :
Z
Hx :
0 ≤ x < 256
⊢
x + 256 × 0 mod 256 + 256 × x / 2 ^ 16 mod 256 + 256 × x / 2 ^ 24 mod 256 + 256 × 0 = x
rewrite Z.div_smallx 2 ^ 16 ; | lia
x :
Z
Hx :
0 ≤ x < 256
⊢
x + 256 × 0 mod 256 + 256 × 0 mod 256 + 256 × x / 2 ^ 24 mod 256 + 256 × 0 = x
rewrite Z.div_smallx 2 ^ 24 ; | lia
x :
Z
Hx :
0 ≤ x < 256
⊢
x + 256 × 0 mod 256 + 256 × 0 mod 256 + 256 × 0 mod 256 + 256 × 0 = x
rewrite Zmod_0_l
x :
Z
Hx :
0 ≤ x < 256
⊢
x + 256 × 0 + 256 × 0 + 256 × 0 + 256 × 0 = x
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hx
cbn
change 8 × Z.of_nat1 with 8
change 8 × Z.of_nat2 with 16
change 8 × Z.of_nat3 with 24
change 8 × Z.of_nat0 with 0
rewrite Z.pow_0_r
rewrite Z.div_1_r
rewrite Z.mod_smallx 256 ; | lia
rewrite Z.div_smallx 2 ^ 8 ; | lia
rewrite Z.div_smallx 2 ^ 16 ; | lia
rewrite Z.div_smallx 2 ^ 24 ; | lia
rewrite Zmod_0_l
lia
A run of nonzero bytes at the start of a string and its NUL ends before the NUL.
Explore proof 9 tactics
Initial goal
bs :
listZ
r :
Z
⊢
0 ≤ r → Forallλx : Z ⇒ x ≠ 0 takeZ.to_natr bs ++ 0 → r ≤ lengthbs
intros Hr H
⊢
r ≤ lengthbs
destruct Z.le_gt_casesr Z.of_natlengthbs as Hle | Hgt ; exact Hle |
⊢
r ≤ lengthbs
exfalso
⊢
False
rewrite Forall_lookup in H
bs :
listZ
r :
Z
Hr :
0 ≤ r
Hgt :
lengthbs < r
H :
∀i : nat x : Z, takeZ.to_natr bs ++ 0 !! i = Somex → x ≠ 0
⊢
False
apply Hlengthbs 0 ; | reflexivity
rewrite lookup_take_lt ; | lia
bs :
listZ
r :
Z
Hr :
0 ≤ r
Hgt :
lengthbs < r
H :
∀i : nat x : Z, takeZ.to_natr bs ++ 0 !! i = Somex → x ≠ 0
⊢
bs ++ 0 !! lengthbs = Some0
rewrite lookup_app_r ; | lia
bs :
listZ
r :
Z
Hr :
0 ≤ r
Hgt :
lengthbs < r
H :
∀i : nat x : Z, takeZ.to_natr bs ++ 0 !! i = Somex → x ≠ 0
⊢
0 !! lengthbs − lengthbs%nat = Some0
rewrite Nat.sub_diag
bs :
listZ
r :
Z
Hr :
0 ≤ r
Hgt :
lengthbs < r
H :
∀i : nat x : Z, takeZ.to_natr bs ++ 0 !! i = Somex → x ≠ 0
⊢
0 !! 0%nat = Some0
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hr H
destruct Z.le_gt_casesr Z.of_natlengthbs as Hle | Hgt ; exact Hle |
exfalso
rewrite Forall_lookup in H
apply Hlengthbs 0 ; | reflexivity
rewrite lookup_take_lt ; | lia
rewrite lookup_app_r ; | lia
rewrite Nat.sub_diag
reflexivity
One rpl_mbrtowc call of rpl_mbsrtowcs's converting loop, on the suffix bs of the string, with the window that reaches the NUL or is 16 bytes long, from a valid state in its initial shift state: never the incomplete answer, which would abort; EILSEQ stores 84 in errno; the NUL stores a zero character; anything else consumes r bytes before the NUL and stores a nonzero character, leaving a valid initial state.
∀ valid c codec bs xo ys xo′ ys′ xe′ r
Forallλx ⇒ 0 < x < 256 bs
validcodec ys
rpl_resultvalid c codec Z.minZ.of_natlengthbs + 1 16 bs ++ 0 xo ys xo′ ys′ xe′ r
Explore proof 20 tactics
Initial goal
⊢
Forall (λ x : Z, 0 < x < 256) bs
→ valid codec ys
→ le_value (take 4 ys) = 0
→ rpl_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo' ys' xe' r
→ 0 <= r < 2 ^ 64
∧ r ≠ 2 ^ 64 - 2
∧ (r = 2 ^ 64 - 1 → le_value xe' = 84)
∧ (r = 0 → le_value xo' = 0)
∧ (r ≠ 0
→ r ≠ 2 ^ 64 - 1
→ 0 < r <= length bs
∧ 0 < le_value xo' < 2 ^ 32
∧ valid codec ys' ∧ le_value (take 4 ys') = 0)intros Hbs Hval Hinit Hres
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
r :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
Hres :
rpl_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo' ys' xe' rassert No2 : ∀ys1 xo1 r1, ¬r1 = 2 ^ 64 − 2 ∧ validcodec ys1 ∧ xo1 = xo ∧ Z.minZ.of_natlengthbs + 1 16 < 16 ∧ Forallλx ⇒ x ≠ 0 takeZ.to_natZ.minZ.of_natlengthbs + 1 16 bs ++ 0
2 openvalid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
r :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
Hres :
rpl_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo' ys' xe' r⊢
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))focused goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
r :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
Hres :
rpl_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo' ys' xe' rNo2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0]))){intros ys1 xo1 r1 _ & _ & _ & Hn16 & Hnz
2 openvalid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
r :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
Hres :
rpl_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo' ys' xe' rys1, xo1 :
listZ
r1 :
Z
Hn16 : (length bs + 1) `min` 16 < 16Hnz :
Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0]))⊢
False
deferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
r :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
Hres :
rpl_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo' ys' xe' rNo2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))apply before_nul in Hnz ; lia
deferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
r :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
Hres :
rpl_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo' ys' xe' rNo2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))destruct Hres as Hc | → & r0 & Hr0 & Hc0 & x & Hx & →
2 openvalid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
r :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
Hc :
conv_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo' ys' xe' rNo2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))focused goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
r0 :
Z
Hr0 :
2 ^ 64 − 2 ≤ r0
Hc0 :
conv_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo ys' xe' r0x :
Z
Hx :
bs ++ 0 !! 0%nat = Somex
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))–destruct Hc as → & _ & _ & Ho & _ | Hr & Hr2 & Hv & Ho & Hs & Hnz | → & He & _ | H2
5 openvalid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
Ho :
le_valuexo′ = 0
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))focused goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
r :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
Hr : 0 < r <= (length bs + 1) `min` 16Hr2 :
r < 2 ^ 64 − 2
Hv :
validcodec ys′
Ho :
0 < le_valuexo′ < 2 ^ 32
Hnz :
Forallλx : Z ⇒ x ≠ 0 takeZ.to_natr bs ++ 0
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))focused goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
He :
le_valuexe′ = 84
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))focused goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
r :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
H2 :
r = 2 ^ 64 - 2
∧ valid codec ys'
∧ xo' = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0]))No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))deferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
r0 :
Z
Hr0 :
2 ^ 64 − 2 ≤ r0
Hc0 :
conv_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo ys' xe' r0x :
Z
Hx :
bs ++ 0 !! 0%nat = Somex
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))+repeat split ; try lia ; auto
4 opendeferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
r :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
Hr : 0 < r <= (length bs + 1) `min` 16Hr2 :
r < 2 ^ 64 − 2
Hv :
validcodec ys′
Ho :
0 < le_valuexo′ < 2 ^ 32
Hnz :
Forallλx : Z ⇒ x ≠ 0 takeZ.to_natr bs ++ 0
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))deferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
He :
le_valuexe′ = 84
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))deferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
r :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
H2 :
r = 2 ^ 64 - 2
∧ valid codec ys'
∧ xo' = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0]))No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))deferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
r0 :
Z
Hr0 :
2 ^ 64 − 2 ≤ r0
Hc0 :
conv_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo ys' xe' r0x :
Z
Hx :
bs ++ 0 !! 0%nat = Somex
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))+apply before_nul in Hnz ; | lia
4 openvalid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
r :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
Hr : 0 < r <= (length bs + 1) `min` 16Hr2 :
r < 2 ^ 64 − 2
Hv :
validcodec ys′
Ho :
0 < le_valuexo′ < 2 ^ 32
Hnz :
r ≤ lengthbs
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))deferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
He :
le_valuexe′ = 84
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))deferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
r :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
H2 :
r = 2 ^ 64 - 2
∧ valid codec ys'
∧ xo' = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0]))No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))deferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
r0 :
Z
Hr0 :
2 ^ 64 − 2 ≤ r0
Hc0 :
conv_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo ys' xe' r0x :
Z
Hx :
bs ++ 0 !! 0%nat = Somex
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))repeat split ; try lia ; auto
3 opendeferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
He :
le_valuexe′ = 84
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))deferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
r :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
H2 :
r = 2 ^ 64 - 2
∧ valid codec ys'
∧ xo' = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0]))No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))deferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
r0 :
Z
Hr0 :
2 ^ 64 − 2 ≤ r0
Hc0 :
conv_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo ys' xe' r0x :
Z
Hx :
bs ++ 0 !! 0%nat = Somex
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))+repeat split ; try lia ; auto
2 opendeferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
r :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
H2 :
r = 2 ^ 64 - 2
∧ valid codec ys'
∧ xo' = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0]))No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))deferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
r0 :
Z
Hr0 :
2 ^ 64 − 2 ≤ r0
Hc0 :
conv_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo ys' xe' r0x :
Z
Hx :
bs ++ 0 !! 0%nat = Somex
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))+exfalso
2 openvalid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, xo′, ys′, xe′ :
listZ
r :
Z
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
H2 :
r = 2 ^ 64 - 2
∧ valid codec ys'
∧ xo' = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0]))No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))⊢
False
deferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
r0 :
Z
Hr0 :
2 ^ 64 − 2 ≤ r0
Hc0 :
conv_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo ys' xe' r0x :
Z
Hx :
bs ++ 0 !! 0%nat = Somex
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))exact No2_ _ _ H2
deferred goal
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
r0 :
Z
Hr0 :
2 ^ 64 − 2 ≤ r0
Hc0 :
conv_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo ys' xe' r0x :
Z
Hx :
bs ++ 0 !! 0%nat = Somex
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))–destruct nul_index_ _ _ Hbs Hx as Hxr & _ & Hn
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
r0 :
Z
Hr0 :
2 ^ 64 − 2 ≤ r0
Hc0 :
conv_result valid c codec ((length bs + 1) `min` 16)
(bs ++ [0]) xo ys xo ys' xe' r0x :
Z
Hx :
bs ++ 0 !! 0%nat = Somex
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))Hxr :
0 ≤ x < 256
Hn :
x ≠ 0 → 0 < lengthbs%nat
destruct Hc0 as → & _ | _ & Hr2 & _ | _ & _ & _ & _ & Hlaw | H2 ; try lia ; | exfalso ; exact No2_ _ _ H2
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
r0 :
Z
Hr0 :
2 ^ 64 − 2 ≤ r0
Hlaw :
x :
Z
Hx :
bs ++ 0 !! 0%nat = Somex
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))Hxr :
0 ≤ x < 256
Hn :
x ≠ 0 → 0 < lengthbs%nat
destruct HlawHval Hinit as Hv′ & Hs′ & x′ & Hx′ & Hx0
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
r0 :
Z
Hr0 :
2 ^ 64 − 2 ≤ r0
Hlaw :
x :
Z
Hx :
bs ++ 0 !! 0%nat = Somex
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))Hxr :
0 ≤ x < 256
Hn :
x ≠ 0 → 0 < lengthbs%nat
Hv′ :
validcodec ys′
x′ :
Z
Hx′ :
bs ++ 0 !! 0%nat = Somex′
Hx0 :
x′ ≠ 0
rewrite Hx in Hx′
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
r0 :
Z
Hr0 :
2 ^ 64 − 2 ≤ r0
Hlaw :
x :
Z
Hx :
bs ++ 0 !! 0%nat = Somex
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))Hxr :
0 ≤ x < 256
Hn :
x ≠ 0 → 0 < lengthbs%nat
Hv′ :
validcodec ys′
x′ :
Z
Hx0 :
x′ ≠ 0
Hx′ :
Somex = Somex′
injection Hx′ as ←
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
r0 :
Z
Hr0 :
2 ^ 64 − 2 ≤ r0
Hlaw :
x :
Z
Hx :
bs ++ 0 !! 0%nat = Somex
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))Hxr :
0 ≤ x < 256
Hn :
x ≠ 0 → 0 < lengthbs%nat
Hv′ :
validcodec ys′
Hx0 :
x ≠ 0
pose proof HnHx0 as Hlen
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
r0 :
Z
Hr0 :
2 ^ 64 − 2 ≤ r0
Hlaw :
x :
Z
Hx :
bs ++ 0 !! 0%nat = Somex
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))Hxr :
0 ≤ x < 256
Hn :
x ≠ 0 → 0 < lengthbs%nat
Hv′ :
validcodec ys′
Hx0 :
x ≠ 0
Hlen :
0 < lengthbs%nat
rewrite le_value_bytex Hxr
valid :
term → listZ → Prop
c :
Prop
codec :
bs, xo, ys, ys′, xe′ :
listZ
Hbs :
Forallλx : Z ⇒ 0 < x < 256 bs
Hval :
validcodec ys
r0 :
Z
Hr0 :
2 ^ 64 − 2 ≤ r0
Hlaw :
x :
Z
Hx :
bs ++ 0 !! 0%nat = Somex
No2 :
∀ (ys1 xo1 : list Z) (r1 : Z),
¬ (r1 = 2 ^ 64 - 2
∧ valid codec ys1
∧ xo1 = xo
∧ (length bs + 1) `min` 16 < 16
∧ Forall (λ x : Z, x ≠ 0)
(take (Z.to_nat ((length bs + 1) `min` 16)) (bs ++ [0])))Hxr :
0 ≤ x < 256
Hn :
x ≠ 0 → 0 < lengthbs%nat
Hv′ :
validcodec ys′
Hx0 :
x ≠ 0
Hlen :
0 < lengthbs%nat
repeat split ; try lia ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hbs Hval Hinit Hres
assert No2 : ∀ys1 xo1 r1, ¬r1 = 2 ^ 64 − 2 ∧ validcodec ys1 ∧ xo1 = xo ∧ Z.minZ.of_natlengthbs + 1 16 < 16 ∧ Forallλx ⇒ x ≠ 0 takeZ.to_natZ.minZ.of_natlengthbs + 1 16 bs ++ 0
{intros ys1 xo1 r1 _ & _ & _ & Hn16 & Hnz
apply before_nul in Hnz ; lia
destruct Hres as Hc | → & r0 & Hr0 & Hc0 & x & Hx & →
–destruct Hc as → & _ & _ & Ho & _ | Hr & Hr2 & Hv & Ho & Hs & Hnz | → & He & _ | H2
+repeat split ; try lia ; auto
+apply before_nul in Hnz ; | lia
repeat split ; try lia ; auto
+repeat split ; try lia ; auto
+exfalso
exact No2_ _ _ H2
–destruct nul_index_ _ _ Hbs Hx as Hxr & _ & Hn
destruct Hc0 as → & _ | _ & Hr2 & _ | _ & _ & _ & _ & Hlaw | H2 ; try lia ; | exfalso ; exact No2_ _ _ H2
destruct HlawHval Hinit as Hv′ & Hs′ & x′ & Hx′ & Hx0
rewrite Hx in Hx′
injection Hx′ as ←
pose proof HnHx0 as Hlen
rewrite le_value_bytex Hxr
repeat split ; try lia ; auto
The four-byte words of ws are wide characters, none of them zero.
No words, no wide characters.
Explore proof 3 tactics
A nonzero wide character after i of them.
Explore proof 10 tactics
Initial goal
intros Hw Lw Lx Hx k Hk
rewrite length_app in Hk
destruct decide4 × k + 4 ≤ lengthws%nat as Hlt | Hge
2 open–rewrite drop_app_le ; | lia
2 openrewrite take_app_le ; | rewrite length_drop ; lia
2 openapply Hw
2 openexact Hlt
–assert Ek : 4 × k = lengthws%nat by lia
rewrite Ek drop_app_length
rewrite take_ge ; exact Hx | lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hw Lw Lx Hx k Hk
rewrite length_app in Hk
destruct decide4 × k + 4 ≤ lengthws%nat as Hlt | Hge
–rewrite drop_app_le ; | lia
rewrite take_app_le ; | rewrite length_drop ; lia
apply Hw
exact Hlt
–assert Ek : 4 × k = lengthws%nat by lia
rewrite Ek drop_app_length
rewrite take_ge ; exact Hx | lia
Import L LG SL ML LL HL HLo
mbrtowc's triple
403Context registry : name → optioncontractlibc_world wi : mem → libc_world → gmappiece pval → Prop `{!SafepointStablewi} ge : genv
The Iris instance of the registry and wi.
The expressions of the language.
mbrtowc has Campaign 4's contract, whose state predicate valid admits the zero state and holds only of bytes.
The world interpretation makes libc ready, with the errno cell errno, keeps the codec piece current (codec_current) and libc's private state apart. A conversion learns the codec from the codec piece, which setlocale's setter set (wp_setlocale_set).
424Context Hlibc : ∀m w h, wim w h → libc_readyrep m w ∧ codec_currentlibc_localefstw h ∧ libc_errnofstw = errno ∧ libc_privatem w h
The audited codec premise: the world's codec is one of the audited profiles, C or C.UTF-8.
The world interpretation survives a return of mbrtowc into the output, state and errno blocks the program owns, holding whatever the memory holds there afterwards.
436Context Kmbrtowc : ∀r args out src n state s m w h trace values s′ m′ w′ bo ro oo xo co bs rs os ys cs be re oe xe ce, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l v, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
Owning two blocks, they are of different objects: each life is owned once.
Explore proof 7 tactics
Initial goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
b :
Z
reg :
o :
Z
xs :
listZ
cs :
listcap
b′ :
Z
reg′ :
o′ :
Z
xs′ :
listZ
cs′ :
listcap
rewrite / block_ps / pts ! big_sepL_cons
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
b :
Z
reg :
o :
Z
xs :
listZ
cs :
listcap
b′ :
Z
reg′ :
o′ :
Z
xs′ :
listZ
cs′ :
listcap
iIntros [Hl _] [Hl′ _]
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
b :
Z
reg :
o :
Z
xs :
listZ
cs :
listcap
b′ :
Z
reg′ :
o′ :
Z
xs′ :
listZ
cs′ :
listcap
∗
⌜b ≠ b′⌝
iDestruct pointsto_ne with Hl Hl′ as %Hne
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
b :
Z
reg :
o :
Z
xs :
listZ
cs :
listcap
b′ :
Z
reg′ :
o′ :
Z
xs′ :
listZ
cs′ :
listcap
∗
⌜b ≠ b′⌝
iPureIntro
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
b :
Z
reg :
o :
Z
xs :
listZ
cs :
listcap
b′ :
Z
reg′ :
o′ :
Z
xs′ :
listZ
cs′ :
listcap
⊢
b ≠ b′
intros ←
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
b :
Z
reg :
o :
Z
xs :
listZ
cs :
listcap
reg′ :
o′ :
Z
xs′ :
listZ
cs′ :
listcap
⊢
False
apply Hne
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
b :
Z
reg :
o :
Z
xs :
listZ
cs :
listcap
reg′ :
o′ :
Z
xs′ :
listZ
cs′ :
listcap
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
The arguments are admitted (mbrtowc_pre) where the program owns the output, state and errno blocks and the source's life and bytes, of four different objects, the state's bytes valid.
∀ codec m w h out src n state bo ro oo xo co bs rs os ys cs be re oe xe ce bsrc rsrc osrc ss
wim w h
agreesm h
∀l v, l, v ∈ block_psbo ro oo xo co → h !! l = Somev
∀l v, l, v ∈ block_psbs rs os ys cs → h !! l = Somev
∀l v, l, v ∈ block_psbe re oe xe ce → h !! l = Somev
∀l v, l, v ∈ block_psbsrc rsrc osrc ss [ ] → h !! l = Somev
bo ≠ bs
bo ≠ be
bo ≠ bsrc
bs ≠ be
bs ≠ bsrc
be ≠ bsrc
ptr_addrsrc = bsrc + osrc
0 < bo
0 < bs
0 < bsrc
bo + oo mod 4 = 0
bs + os mod 4 = 0
lengthxo = 4%nat
lengthys = 8%nat
lengthxe = 4%nat
0 < n ≤ Z.of_natlengthss
Forallλx ⇒ 0 ≤ x < 256 ss
validcodec ys
Proof 125 steps Qed
intros Hw Ha Hd Hfit Hcod Ho Hs He Hsr Nos Noe Nosr Nse Nssr Nesr → → Herr Hcap Haddr Hbo Hbs Hbsrc Hoal Hsal Lxo Lys Lxe Hn Hss Hval
pose proof Hbytes_ _ Hval as Hyb
pose proof Hcur_ Hcod as Hcodec
destruct block_factsm h bo ro oo xo co Ha Ho nonempty_of_lengthxo 3 Lxo as Lo & Oo & Eo & _
destruct block_factsm h bs rs os ys cs Ha Hs nonempty_of_lengthys 7 Lys as Ls & Os & Es & Vs
destruct block_factsm h be re oe xe ce Ha He nonempty_of_lengthxe 3 Lxe as Le & Oe & Ee & _
destruct block_factsm h bsrc rsrc osrc ss [ ] Ha Hsr ltac:intros E ; rewrite E in Hn ; cbn in Hn ; lia as Lsr & Osr & Esr & Vsr
rewrite Lxo in Eo
rewrite Lys in Es
rewrite Lxe in Ee
assert Hkey : ∀b reg o zs ds, ∀l v, l, v ∈ block_psb reg o zs ds → h !! l = Somev → h !! PLiveb = SomeVLivereg
{intros b reg o zs ds H
apply H
apply elem_of_cons
left
reflexivity
destruct Hpriv_ _ _ Hkey_ _ _ _ _ Ho I Lo as Ro & Co1 & Co2
destruct Hpriv_ _ _ Hkey_ _ _ _ _ Hs I Ls as Rs & Cs1 & Cs2
destruct Hpriv_ _ _ Hkey_ _ _ _ _ He I Le as Re & Ce1 & Ce2
destruct Hpriv_ _ _ Hkey_ _ _ _ _ Hsr I Lsr as Rsr & Csr1 & Csr2
pose proof Hfit_ _ proj1Lsr as Fsr0 Fsr1
assert Hsrc_bytes : ∀i, 0 ≤ i < n → ∃x, ss !! Z.to_nati = Somex ∧ m_bytesm ptr_addrsrc + i = x ∧ 0 ≤ x < 256
{intros i Hi
destruct lookup_lt_is_Some_2ss Z.to_nati ltac:lia as x Hx
exists x
split ; exact Hx |
split ; | exact proj1Forall_lookup_ _ Hss _ _ Hx
rewrite Haddr
rewrite <- Vsr_ _ Hx
f_equal
lia
unfold mbrtowc_pre
rewrite Herrno Herr
split ; exact Hready |
split ; exact Hvalid0 |
split ; exact Hbytes |
split ; reflexivity |
split ; lia |
split ; lia |
split ; lia |
split
{split ; lia |
split ; exists bsrc, rsrc ; split ; exact Hcap | exact Lsr |
split
–destruct Hcap as Hc | Hc ; rewrite Hc Haddr ; apply access_obj_ _ rsrc _ _ Read | apply access_ro_read_ _ rsrc ; solve exact proj1Lsr | lia | apply Z.mod_1_r
split
{unfold writable_span
split ; lia |
exists bo, ro
split ; reflexivity |
split ; exact proj1Lo |
split ; exact proj2Lo |
apply access_obj_ _ ro _ _ Write ; exact proj1Lo | lia | lia | apply Z.mod_1_r
split ; exact Hoal |
split
{unfold writable_span
split ; lia |
exists bs, rs
split ; reflexivity |
split ; exact proj1Ls |
split ; exact proj2Ls |
apply access_obj_ _ rs _ _ Write ; exact proj1Ls | lia | lia | apply Z.mod_1_r
split
{split ; lia |
split ; exists bs, rs ; split ; left ; reflexivity | exact Ls |
split
apply access_obj_ _ rs _ _ Read ; exact proj1Ls | lia | lia | apply Z.mod_1_r
split ; exact Hsal |
split
{rewrite Hcodec mbstate_mem_bytes
cbn [ ptr_addr ]
rewrite <- Lys , mem_bytes_of ; exact Hval |
intros i x Hx
exact Vsi x Hx
split ; apply spans_apart_objectsm bsrc rsrc bo ro ; cbn [ ptr_addr ] ; auto ; lia |
split ; apply spans_apart_objectsm bsrc rsrc bs rs ; cbn [ ptr_addr ] ; auto ; lia |
split ; apply spans_apart_objectsm bo ro bs rs ; cbn [ ptr_addr ] ; auto ; lia |
split
{intros p size Hin
cbn in Hin
destruct Hin as E | E | E | ; injection E as ← ← ; split
–apply spans_apart_objectsm be re bsrc rsrc ; cbn [ ptr_addr ] ; auto ; lia
–intros root Hroot
apply spans_apart_withinroot bsrc rsrc ; exact Rsrroot Hroot | lia | lia
–apply spans_apart_objectsm be re bo ro ; cbn [ ptr_addr ] ; auto ; lia
–intros root Hroot
apply spans_apart_withinroot bo ro ; exact Roroot Hroot | cbn ; lia | cbn ; lia
–apply spans_apart_objectsm be re bs rs ; cbn [ ptr_addr ] ; auto ; lia
–intros root Hroot
apply spans_apart_withinroot bs rs ; exact Rsroot Hroot | cbn ; lia | cbn ; lia
split
{intros base Hbase p Hp
cbn in Hp
pose proof Hownbase _ _ Hbase Hkey_ _ _ _ _ Ho I as N1
pose proof Hownbase _ _ Hbase Hkey_ _ _ _ _ Hs I as N2
pose proof Hownbase _ _ Hbase Hkey_ _ _ _ _ He I as N3
pose proof Hownbase _ _ Hbase Hkey_ _ _ _ _ Hsr I as N4
cbn [ piece_id ] in N1 , N2 , N3 , N4
destruct Hp as [ <-| [ <-| [ <-| [ <-| [ ] ] ] ] ] ; cbn [ ptr_cap ] ; | destruct Hcap as Hc | Hc ; rewrite Hc | | ; split ; congruence
split
{intros root Hroot
apply spans_apart_withinroot be re ; exact Reroot Hroot | cbn ; lia | cbn ; lia
intros p Hp base Hc
cbn in Hp
destruct Hp as [ <-| [ <-| [ <-| [ <-| [ ] ] ] ] ] ; cbn [ ptr_cap ] in Hc
–destruct Hc as E | E ; injection E as ← ; auto | discriminate E
–destruct Hcap as Hc′ | Hc′ ; rewrite Hc' in Hc ; destruct Hc as E | E ; first discriminate E | injection E as ← ; auto
–destruct Hc as E | E ; injection E as ← ; auto | discriminate E
–destruct Hc as E | E ; injection E as ← ; auto | discriminate E
A return of the call keeps every piece but the three blocks' bytes and slots agreeing (prefix_agrees_out), so that, the blocks holding what the memory holds after it, the ghost heap agrees; the live objects stay apart and the runtime ready.
∀ r args s m w h trace values s′ m′ w′ out src n state bo ro oo xo co bs rs os ys cs be re oe xe ce
M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′
wim w h
agreesm h
R.readys m
∀l v, l, v ∈ block_psbo ro oo xo co → h !! l = Somev
∀l v, l, v ∈ block_psbs rs os ys cs → h !! l = Somev
∀l v, l, v ∈ block_psbe re oe xe ce → h !! l = Somev
lengthxo = 4%nat
lengthco = 4%nat
lengthys = 8%nat
lengthcs = 8%nat
lengthxe = 4%nat
lengthce = 4%nat
n ≠ 0
Proof 65 steps Qed
intros Hi Hw Ha Hd Hr Ho Hs He → → Herr Lxo Lco Lys Lcs Lxe Lce Hn
destruct block_factsm h bo ro oo xo co Ha Ho nonempty_of_lengthxo 3 Lxo as Lo & Oo & Eo & _
destruct block_factsm h bs rs os ys cs Ha Hs nonempty_of_lengthys 7 Lys as Ls & Os & Es & _
destruct block_factsm h be re oe xe ce Ha He nonempty_of_lengthxe 3 Lxe as Le & Oe & Ee & _
rewrite Lxo in Eo
rewrite Lys in Es
rewrite Lxe in Ee
destruct M.E.invoke_prefix_ _ _ _ _ _ _ _ _ _ _ _ _ Hi as born & Hp
destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hp Hr as Hr′ _
set ks := byte_psbo oo xo ++ aux_psbo oo co.*1 ++ byte_psbs os ys ++ aux_psbs os cs.*1 ++ byte_psbe oe xe ++ aux_psbe oe ce.*1
set outs := λa ⇒ span_containsmkSpanmkPtrbo + oo Objbo 4 a ∨ span_containsmkSpanmkPtrbs + os Objbs 8 a ∨ span_containsmkSpanmkPtrbe + oe Objbe 4 a
assert Hwr : contract_writesmbrtowc_contractvalid audit rep requests WPtrmkPtrbo + oo Objbo; WPtrsrc; WIntn; WPtrmkPtrbs + os Objbs m w = locale_rootslibc_localefstw ++ mkSpanmkPtrbo + oo Objbo 4; mkSpanmkPtrbs + os Objbs 8; mkSpanmkPtrbe + oe Objbe 4
rewrite proj2Z.eqb_neqn 0 Hn Herrno Herr
reflexivity
assert Hrel : contract_releasesmbrtowc_contractvalid audit rep requests WPtrmkPtrbo + oo Objbo; WPtrsrc; WIntn; WPtrmkPtrbs + os Objbs m w = locale_ownedlibc_localefstw
destruct prefix_agrees_out_ _ _ _ _ _ _ _ _ _ _ h ks outs Hp Hr Hd as Ha′ & _ & Hd′ & _
–intros l v Hl Hm
exact agree_piece_registered_ _ _ Hm Hal v Hl
–rewrite Hwr
intros sp a Hin Hsp Hol
apply in_app_or in Hin as Hin | Hin
+exfalso
destruct Hol as l & v & reg & Hl & Hm & Hlv & Hb
pose proof Hrootssp Hin as Hap
unfold spans_apart , span_contains in Hap , Hsp
cbn in Hap
lia
+unfold outs
destruct Hin as [ <-| [ <-| [ <-| [ ] ] ] ] ; auto
–intros l v Hl Hk
destruct l as b | b o | b o | k ; try exact I ; intros reg Hlv Ho′ He′ Hout ; apply Hk ; unfold ks ; rewrite ! elem_of_app ; destruct Hout as Hout | Hout | Hout ; unfold span_contains in Hout ; cbn in Hout ; left | right ; left | right ; right ; solve eapply block_keym bo ro oo xo co ; eauto ; lia | eapply block_keym bs rs os ys cs ; eauto ; lia | eapply block_keym be re oe xe ce ; eauto ; lia
–rewrite Hrel
exact Hown
–assert Hlive : ∀b reg o zs ds, ∀l v, l, v ∈ block_psb reg o zs ds → h !! l = Somev → live_atm' b reg
{intros b reg o zs ds H
unfold ks
rewrite ! elem_of_app
intros Hk | Hk | Hk ; exact live_not_key_ _ _ _ _ Hk
split ; | split ; exact Hd' | exact Hr'
intros l v Hl
apply lookup_overwrite in Hl as Hin | Hnk Hh
+rewrite ! elem_of_app in Hin
destruct Hin as Hin | Hin | Hin
∗exact block_afterm' bo ro oo 4 l v Hlive_ _ _ _ _ Ho Oo Eo Hin
∗exact block_afterm' be re oe 4 l v Hlive_ _ _ _ _ He Oe Ee Hin
+apply Ha'l v Hh
intros Hk
apply Hnk
unfold ks in Hk
rewrite ! fmap_app ! elem_of_app
rewrite ! elem_of_app in Hk
destruct Hk as Hk | Hk | Hk ; left | right ; left | right ; right
∗exact block_keys_afterm' bo ro oo xo co 4 l Lxo Lco Hk
∗exact block_keys_afterm' bs rs os ys cs 8 l Lys Lcs Hk
∗exact block_keys_afterm' be re oe xe ce 4 l Lxe Lce Hk
Campaign 4's mbrtowc_result, for 0 < n and the audited codec, read through the owned bytes: conv_result.
∀ codec m w out src n state res m′ bo oo xo bs os ys be oe bsrc osrc ss
mbrtowc_resultvalid audit m w out src n state res m′
locale_codeclibc_localefstw = codec
libc_errnofstw = mkPtrbe + oe Objbe
ptr_addrsrc = bsrc + osrc
lengthxo = 4%nat
∀i x, xo !! i = Somex → m_bytesm bo + oo + Z.of_nati = x
lengthys = 8%nat
∀i x, ys !! i = Somex → m_bytesm bs + os + Z.of_nati = x
0 < n ≤ Z.of_natlengthss
∀i x, ss !! i = Somex → m_bytesm bsrc + osrc + Z.of_nati = x
Proof 106 steps Qed
intros Hfull Hprof Hcodec Herrno Eout Est Haddr Lxo Vo Lys Vs Hn Vss
pose proof Hfull as _ & Hres
subst out state
{intros i Hi
destruct lookup_lt_is_Some_2ss Z.to_nati ltac:lia as x Hx
exists x
split ; exact Hx |
rewrite Haddr
rewrite <- Vss_ _ Hx
f_equal
lia
assert Hnz : ∀k, k ≤ n → ∀i, 0 ≤ i < k → m_bytesm ptr_addrsrc + i ≠ 0 → Forallλx ⇒ x ≠ 0 takeZ.to_natk ss
{intros k Hk H
apply Forall_lookup
intros i x Hx
apply lookup_take_Some in Hx as Hx Hi
destruct HsrcZ.of_nati ltac:lia as x′ & Hx′ & Hb
rewrite Nat2Z.id Hx in Hx'
injection Hx' as ←
rewrite <- Hb
apply H
lia
assert Hkept : ∀a, span_containsmkSpanmkPtrbo + oo Objbo 4 a → m_bytesm' a = m_bytesm a → mem_bytesm' bo + oo 4 = xo
{intros H
rewrite <- Lxo
apply mem_bytes_of
intros i x Hx
pose proof lookup_lt_Some_ _ _ Hx as Hi
rewrite Lxo in Hi
rewrite H ; exact Voi x Hx |
unfold span_contains
cbn
lia
destruct Hres as → & Hv & Hp | Hr & Hr2 & Hv & Hp | → & He & Hk & _ | → & Hv & Hk & Hp
–left
destruct HpHprof as i & Hi & Hz & Ho & Hs
split ; reflexivity |
split ; rewrite <- Hcodec ; exact Hv |
split
–right ; left
destruct HpHprof as Ho & Hs & Hb
split ; exact Hr |
split ; exact Hr2 |
split ; rewrite <- Hcodec ; exact Hv |
rewrite Hst4
rewrite <- ! load_bytes_4
split ; exact Ho |
split ; exact Hs |
apply Hnz ; lia | exact Hb
–right ; right ; left
split ; reflexivity |
split ; rewrite <- load_bytes_4 ; rewrite Herrno in He ; exact He |
split ; exact HkeptHk |
split
{intros Hc
rewrite <- Hcodec in Hc
destruct mbrtowc_c_error_ _ _ _ _ _ _ _ _ Hfull Hc as Hst Hsrc0
split
+destruct Hsrc0 ltac:lia as x & Hx & Hb
exists x
split ; exact Hx |
rewrite <- Hb , Z.add_0_r
exact Hsrc0
{intros Hv0 Hz0
rewrite <- Hcodec in Hv0
rewrite <- Ey in Hv0
destruct mbrtowc_initial_error_ _ _ _ _ _ _ _ _ Hfull Hprof Hl0 Hv0 as Hv′ & Hc′ & Hs0
split ; rewrite <- Hcodec ; exact Hv' |
split
+destruct Hsrc0 ltac:lia as x & Hx & Hb
exists x
split ; exact Hx |
rewrite <- Hb , Z.add_0_r
exact Hs0
–right ; right ; right
destruct HpHprof as Hn16 Hb
split ; reflexivity |
split ; rewrite <- Hcodec ; exact Hv |
split ; exact HkeptHk |
split ; exact Hn16 |
apply Hnz ; lia | exact Hb
mbrtowc(out, src, n, state)'s triple, from mbrtowc_contract: owning the output, state and errno blocks, of 4, 8 and 4 bytes with their slots, and the source's life and bytes ss, of four different objects, where vo, vs, vn and vt read as out, src, n and state, n is positive and within ss, and the state's bytes are valid, the call binds d to its result r and hands the blocks back holding new bytes and slots, which conv_result describes.
∀ f e ls lab d vo vs vn vt rest j out src n state bo ro oo xo co bs rs os ys cs be re oe xe ce bsrc rsrc osrc ss codec dq Φ
lookupTAtom"mbrtowc" ge_globalsge = None
ptr_addrsrc = bsrc + osrc
0 < bo
0 < bs
0 < bsrc
bo + oo mod 4 = 0
bs + os mod 4 = 0
lengthxo = 4%nat
lengthco = 4%nat
lengthys = 8%nat
lengthcs = 8%nat
lengthxe = 4%nat
lengthce = 4%nat
0 < n ≤ Z.of_natlengthss
Forallλx ⇒ 0 ≤ x < 256 ss
validcodec ys
pointstoPNamecodec_key dq VCodeccodec −∗ ptsblock_psbo ro oo xo co −∗ ptsblock_psbs rs os ys cs −∗ ptsblock_psbe re oe xe ce −∗ ptsblock_psbsrc rsrc osrc ss [ ] −∗ ▷∀r xo′ ys′ xe′ co′ cs′ ce′, ⌜conv_resultvalid auditcodec = SomeCodecC codec n ss xo ys xo′ ys′ xe′ r ∧ lengthxo′ = 4%nat ∧ lengthys′ = 8%nat ∧ lengthxe′ = 4%nat ∧ lengthco′ = 4%nat ∧ lengthcs′ = 8%nat ∧ lengthce′ = 4%nat⌝ −∗ pointstoPNamecodec_key dq VCodeccodec −∗ ptsblock_psbo ro oo xo′ co′ −∗ ptsblock_psbs rs os ys′ cs′ −∗ ptsblock_psbe re oe xe′ ce′ −∗ ptsblock_psbsrc rsrc osrc ss [ ] −∗ WPERunmkFramef putd WIntr e ls None Execlab rest j : cexpr {Φ} −∗ WPERunmkFramef e ls None Execlab CallCResultd L GlobalTAtom"mbrtowc" ArgP vo; ArgP vs; ArgL vn; ArgP vt :: rest j : cexpr {Φ}
Proof 71 steps Qed
intros Hfn Hdata Hvo Hvs Hvn Hvt Eout Est Herr Hcap Haddr Hbo Hbs Hbsrc Hoal Hsal Lxo Lco Lys Lcs Lxe Lce Hn Hss Hval
iIntros Hcod HBo HBs HBe HBsrc HK
iDestruct block_ne with HBo HBs as %N1
iDestruct block_ne with HBo HBe as %N2
iDestruct block_ne with HBo HBsrc as %N3
iDestruct block_ne with HBs HBe as %N4
iDestruct block_ne with HBs HBsrc as %N5
iDestruct block_ne with HBe HBsrc as %N6
iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ mbrtowc_contractvalid audit rep requests WPtrout; WPtrsrc; WIntn; WPtrstate pointstoPNamecodec_key dq VCodeccodec ∗ ptsblock_psbo ro oo xo co ∗ ptsblock_psbs rs os ys cs ∗ ptsblock_psbe re oe xe ce ∗ ptsblock_psbsrc rsrc osrc ss [ ] with [$Hcod $HBo $HBs $HBe $HBsrc] [HK] ; exact Hfn | exact Hdata | reflexivity | exact Hmbrtowc | cbn [ map_option ] ; rewrite Hvo Hvs Hvn Hvt ; reflexivity | | |
–split ; right ; eexists ; reflexivity | do 4 eexists ; reflexivity
–iIntros σ Hσ (Hc & Ho & Hs & He & Hsr)
iDestruct Hσ as h [Hh %Hf]
destruct Hf as Ha & Hd & Hr & Hw
iDestruct gen_heap_valid with Hh Hc as %Kc
iDestruct pts_lookup with Hh Ho as %Ko
iDestruct pts_lookup with Hh Hs as %Ks
iDestruct pts_lookup with Hh He as %Ke
iDestruct pts_lookup with Hh Hsr as %Ksr
iPureIntro
exact mbrtowc_admitted_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hw Ha Hd R.address_space_ _ Hr Kc Ko Ks Ke Ksr N1 N2 N3 N4 N5 N6 Eout Est Herr Hcap Haddr Hbo Hbs Hbsrc Hoal Hsal Lxo Lys Lxe Hn Hss Hval
–iNext
iIntros σ trace values s′ m′ w′ Hinv (%h & Hh & %Hf) (Hc & Ho & Hs & He & Hsr)
destruct Hf as Ha & Hd & Hr & Hw
iDestruct gen_heap_valid with Hh Hc as %Kc
iDestruct pts_lookup with Hh Ho as %Ko
iDestruct pts_lookup with Hh Hs as %Ks
iDestruct pts_lookup with Hh He as %Ke
iDestruct pts_lookup with Hh Hsr as %Ksr
destruct Hlibc_ _ _ Hw as _ & Hcur & Herrno & _
pose proof Hcur_ Kc as Hcodec
destruct block_facts_ h bo ro oo xo co Ha Ko nonempty_of_lengthxo 3 Lxo as _ & _ & _ & Vo
destruct block_facts_ h bs rs os ys cs Ha Ks nonempty_of_lengthys 7 Lys as _ & _ & _ & Vs
destruct block_facts_ h bsrc rsrc osrc ss [ ] Ha Ksr ltac:intros E ; rewrite E in Hn ; cbn in Hn ; lia as _ & _ & _ & Vsr
destruct LB.mbrtowc_returned_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hinv as res & → & Hres
rewrite proj2Z.eqb_neqn 0 ltac:lia in Hres
assert Hnl : 0 < n ≤ Z.of_natlengthss by lia
assert Hn0 : n ≠ 0 by lia
pose proof conv_of_result_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hres Haudit_ _ _ Hw Hcodec eq_transHerrno Herr Eout Est Haddr Lxo Vo Lys Vs Hnl Vsr as Hconv
destruct mbrtowc_frame_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hinv Hw Ha Hd Hr Ko Ks Ke Eout Est Herr Lxo Lco Lys Lcs Lxe Lce Hn0 as Ha′ & Hd′ & Hr′
assert Hlk : ∀l v, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev
pose proof Kmbrtowc_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hinv Hlk Hw as Hw′
iMod pts_update_ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce block_psbo ro oo mem_bytesm' bo + oo 4 mem_auxesm' bo + oo 4 ++ block_psbs rs os mem_bytesm' bs + os 8 mem_auxesm' bs + os 8 ++ block_psbe re oe mem_bytesm' be + oe 4 mem_auxesm' be + oe 4 with Hh [Ho Hs He] as [Hh Hn]
{rewrite ! fmap_app
rewrite block_ps_keysbo ro oo xo co ; | rewrite length_mem_bytes ; auto | rewrite length_mem_auxes ; auto
rewrite block_ps_keysbs rs os ys cs ; | rewrite length_mem_bytes ; auto | rewrite length_mem_auxes ; auto
rewrite block_ps_keysbe re oe xe ce ; | rewrite length_mem_bytes ; auto | rewrite length_mem_auxes ; auto
reflexivity
{rewrite ! pts_app
iFrame
iModIntro
iExists _
iSplit
iSplitL Hh
+rewrite ! pts_app
iDestruct Hn as (Ho & Hs & He)
iApply HK $! res with [%] Hc Ho Hs He Hsr
rewrite ! length_mem_bytes ! length_mem_auxes
split ; exact Hconv |
repeat split
rpl_mbrtowc's triple
The genv links Hello, whose world interpretation keeps every lent string where lent_at says: hard_locale's premises (HelloLocale.v).
797Context wi_lent : ∀m w h k p t, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
setlocale's query, as hard_locale needs it.
802Context Hset_query : ∀r args s m w h k p t z trace ending s′ m′ w′, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
strlen, memcpy and strcmp have their contracts.
The world interpretation survives a copy, a byte store and a four-byte store into a block the program owns, and an allocation.
819Context Kcopy : ∀b reg o xs cs s n m m′ wd h ys, copy_resultm mkPtrb + o Objb s n m′ → ∀l v, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h
Enter a block of rpl_mbrtowc.
A pure instruction.
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ; word_premise | ; iNext
rpl_mbrtowc from its block L11, where pr.1 is the output pointer out, whichever entry chose it: the call to mbrtowc, then the fallback outside a hard locale.
∀ pwc b8 b13 b15 out src n state bo ro oo xo co bs rs os ys cs be re oe xe ce bsrc rsrc osrc ss codec dq p t rc rp Φ
ptr_addrsrc = bsrc + osrc
0 < bo
0 < bs
0 < bsrc
0 ≤ oo
0 ≤ osrc
bo + oo + 4 ≤ r_endro
bsrc + osrc + Z.of_natlengthss ≤ r_endrsrc
r_endro ≤ 2 ^ 48
r_endrsrc ≤ 2 ^ 48
bo + oo mod 4 = 0
bs + os mod 4 = 0
lengthxo = 4%nat
lengthco = 4%nat
lengthys = 8%nat
lengthcs = 8%nat
lengthxe = 4%nat
lengthce = 4%nat
0 < n ≤ Z.of_natlengthss
Forallλx ⇒ 0 ≤ x < 256 ss
validcodec ys
LL.lent0 p t −∗ SL.stringc_ptr 65824 rc c_bytes −∗ SL.stringposix_ptr 65856 rp posix_bytes −∗ pointstoPNamecodec_key dq VCodeccodec −∗ ptsblock_psbo ro oo xo co −∗ ptsblock_psbs rs os ys cs −∗ ptsblock_psbe re oe xe ce −∗ ptsblock_psbsrc rsrc osrc ss [ ] −∗ ▷∀r xo′ ys′ xe′ co′ cs′ ce′, ⌜rpl_resultvalid auditcodec = SomeCodecC codec n ss xo ys xo′ ys′ xe′ r ∧ lengthxo′ = 4%nat ∧ lengthys′ = 8%nat ∧ lengthxe′ = 4%nat ∧ lengthco′ = 4%nat ∧ lengthcs′ = 8%nat ∧ lengthce′ = 4%nat⌝ −∗ SL.stringc_ptr 65824 rc c_bytes −∗ SL.stringposix_ptr 65856 rp posix_bytes −∗ pointstoPNamecodec_key dq VCodeccodec −∗ ptsblock_psbo ro oo xo′ co′ −∗ ptsblock_psbs rs os ys′ cs′ −∗ ptsblock_psbe re oe xe′ ce′ −∗ ptsblock_psbsrc rsrc osrc ss [ ] −∗ ΦRetWIntr −∗ WPERunmkFramerpl_fn putTAtom"pr.1" WPtrout putTAtom"v15" b15 putTAtom"v13" b13 putTAtom"v8" b8 TAtom"v6", WPtrstate; TAtom"v4", WIntn; TAtom"v2", WPtrsrc; TAtom"v0", pwc [ ] None ExecTAtom"L11" b_instsrpl_block"L11" b_jumprpl_block"L11" : cexpr {Φ}
Proof 119 steps Qed
intros Eout Est Herr Hcap Haddr Hbo Hbs Hbsrc Hoo Hosrc Heo Hesrc Ho48 Hs48 Hoal Hsal Lxo Lco Lys Lcs Lxe Lce Hn Hss Hval
iIntros #Hk Hc Hposix Hcod HBo HBs HBe HBsrc HΦ
assert Hn64 : n mod 2 ^ 64 = n by apply Z.mod_small ; lia
pose proof Hlinked as Hm & _ & Hext
iApply wp_mbrtowc with Hcod HBo HBs HBe HBsrc ; apply hello_outside ; exact Hm | reflexivity | apply Hext ; reflexivity | word_premise | word_premise | word_premise | word_premise | exact Eout | exact Est | exact Herr | exact Hcap | exact Haddr | exact Hbo | exact Hbs | exact Hbsrc | exact Hoal | exact Hsal | exact Lxo | exact Lco | exact Lys | exact Lcs | exact Lxe | exact Lce | rewrite Hn64 ; exact Hn | exact Hss | exact Hval |
iNext
iIntros res xo1 ys1 xe1 co1 cs1 ce1 Hconv & Lxo1 & Lys1 & Lxe1 & Lco1 & Lcs1 & Lce1 Hcod HBo HBs HBe HBsrc
rewrite Hn64 in Hconv
destruct conv_result_range_ _ _ _ _ _ _ _ _ _ _ Hconv as Hres Hkeep
destruct Z.le_gt_cases2 ^ 64 − 2 res as Hge | Hlt
An invalid or incomplete sequence.
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
rm_enter "L29"
iApply wp_goto
iNext
rm_enter "L30"
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
rm_enter "L35"
iApply wp_call_bind_ _ _ _ _ _ _ _ _ _ _ _ _ hard_locale_fn invocationhard_locale_fn WInt0 ; word_premise | unfold find_fn ; rewrite Hm ; vm_compute ; reflexivity | reflexivity |
iNext
iApply HLo.hard_locale_specregistry wi ge Hlinked wi_lent set_spec Hset Hset_ret Hset_abi Hset_pre Hset_query Hstrlen Hmemcpy Kcopy Kbyte Kalloc Hstrcmp with Hk Hc Hposix ; lia |
iNext
iIntros hr Hc Hposix
iExists _
iSplit ; iPureIntro ; reflexivity |
iNext
iApply wp_goto
iNext
rm_enter "L36"
iApply wp_branch ; word_premise |
iNext
lazymatch goal with|- context [if then 1 else 0]⇒destruct tend
all: change 1 mod 2 ^ 32 with 1 ; change 0 mod 2 ^ 32 with 0 ; cbn [ Z.eqb edge_label ]
Not a hard locale: the first byte stands for itself.
+rm_enter "L22"
destruct ss as | x0 ss′ ; cbn in Hn ; lia |
pose proof Forall_invHss as Hx0
cbv beta in Hx0
iEval rewrite / block_ps ; rewrite / pts big_sepL_cons big_sepL_app byte_ps_cons big_sepL_cons in HBsrc
iDestruct HBsrc as (Hls & (Hb0 & Hbs) & Has)
iDestruct HBo as (Hlo & Hbo & Hao)
iAssert ibytebsrc osrc x0 with [Hb0] as Hb0 ; rewrite / ibyte / pts big_sepL_singleton ; iExact Hb0 |
iApply wp_check_read with Hls ; reflexivity | word_premise | exact Hcap | rewrite Haddr ; addr_premise | rewrite Haddr ; cbn [ length ] in Hesrc ; addr_premise | apply Z.mod_1_r |
iNext
iIntros Hls
iApply wp_raw_load_byte with Hls Hb0 ; reflexivity | word_premise | reflexivity | reflexivity | exact Hcap | rewrite Haddr ; addr_premise |
iNext
iIntros Hls Hb0
iApply wp_let_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ WIntx0 ; reflexivity | reflexivity | word_premise | intros m′ ; cbn ; rewrite Zmod_modsign_extension256 128 x0 2 ^ 32 ; exact f_equalλz ⇒ SomeOpResRValWIntz m' ub_of_sbx0 Hx0 |
iNext
iApply wp_check with Hlo ; reflexivity | word_premise | rewrite Eout ; reflexivity | rewrite Eout ; addr_premise | rewrite Eout ; addr_premise | apply Z.mod_1_r |
iNext
iIntros Hlo
iApply wp_raw_store_w with Hlo Hbo ; word_premise | word_premise | rewrite Eout ; reflexivity | rewrite Eout ; addr_premise | exact Lxo1 | intros m′ wd h Hl Hw ; exact Kstore_ _ _ _ _ _ _ _ Hl Hw |
iNext
iIntros Hlo Hbo
assert Hx32 : x0 mod 2 ^ 32 = x0 by apply Z.mod_small ; lia
iEval rewriteHx32 in Hbo
iApply wp_ret ; reflexivity | reflexivity |
iNext
iApply HΦ $! 1 le_bytesx0 4 ys1 xe1 co1 cs1 ce1 with [%] Hc Hposix Hcod [Hlo Hbo Hao] HBs HBe [Hls Hb0 Hbs Has]
∗split ; | rewrite length_le_bytes ; repeat split ; first assumption | reflexivity
right
split ; reflexivity |
split
exists x0
split ; reflexivity
iFrame
A hard locale: mbrtowc's answer.
+rm_enter "L24"
iApply wp_ret ; reflexivity | word_premise |
iNext
rewrite Z.mod_smallres 2 ^ 64 ; | lia
iApply HΦ $! res xo1 ys1 xe1 co1 cs1 ce1 with [%] Hc Hposix Hcod HBo HBs HBe HBsrc
split ; left ; exact Hconv |
repeat split ; assumption
A character, a NUL or nothing to stand for: mbrtowc's answer.
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
rm_enter "L30"
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
rm_enter "L36"
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
rm_enter "L24"
iApply wp_ret ; reflexivity | word_premise |
iNext
rewrite Z.mod_smallres 2 ^ 64 ; | lia
iApply HΦ $! res xo1 ys1 xe1 co1 cs1 ce1 with [%] Hc Hposix Hcod HBo HBs HBe HBsrc
split ; left ; exact Hconv |
repeat split ; assumption
rpl_mbrtowc(out, src, n, state) for a non-null out, from wp_mbrtowc and HelloLocale.v's hard_locale_spec: owning the output, state and errno blocks, the source's n bytes or more, the codec piece, the literals "C" and "POSIX", and the name of LC_CTYPE (category 0) lent, the call returns what rpl_result says, and hands every block back.
∀ out src n state bo ro oo xo co bs rs os ys cs be re oe xe ce bsrc rsrc osrc ss codec dq p t rc rp Φ
ptr_addrsrc = bsrc + osrc
0 < bo
0 < bs
0 < bsrc
0 ≤ oo
0 ≤ osrc
bo + oo + 4 ≤ r_endro
bsrc + osrc + Z.of_natlengthss ≤ r_endrsrc
r_endro ≤ 2 ^ 48
r_endrsrc ≤ 2 ^ 48
bo + oo mod 4 = 0
bs + os mod 4 = 0
lengthxo = 4%nat
lengthco = 4%nat
lengthys = 8%nat
lengthcs = 8%nat
lengthxe = 4%nat
lengthce = 4%nat
0 < n ≤ Z.of_natlengthss
Forallλx ⇒ 0 ≤ x < 256 ss
validcodec ys
LL.lent0 p t −∗ SL.stringc_ptr 65824 rc c_bytes −∗ SL.stringposix_ptr 65856 rp posix_bytes −∗ pointstoPNamecodec_key dq VCodeccodec −∗ ptsblock_psbo ro oo xo co −∗ ptsblock_psbs rs os ys cs −∗ ptsblock_psbe re oe xe ce −∗ ptsblock_psbsrc rsrc osrc ss [ ] −∗ ▷∀r xo′ ys′ xe′ co′ cs′ ce′, ⌜rpl_resultvalid auditcodec = SomeCodecC codec n ss xo ys xo′ ys′ xe′ r ∧ lengthxo′ = 4%nat ∧ lengthys′ = 8%nat ∧ lengthxe′ = 4%nat ∧ lengthco′ = 4%nat ∧ lengthcs′ = 8%nat ∧ lengthce′ = 4%nat⌝ −∗ SL.stringc_ptr 65824 rc c_bytes −∗ SL.stringposix_ptr 65856 rp posix_bytes −∗ pointstoPNamecodec_key dq VCodeccodec −∗ ptsblock_psbo ro oo xo′ co′ −∗ ptsblock_psbs rs os ys′ cs′ −∗ ptsblock_psbe re oe xe′ ce′ −∗ ptsblock_psbsrc rsrc osrc ss [ ] −∗ ΦRetWIntr −∗ WPERuninvocationrpl_fn WPtrout; WPtrsrc; WIntn; WPtrstate : cexpr {Φ}
Proof 17 steps Qed
intros Eout Est Herr Hcap Haddr Hbo Hbs Hbsrc Hoo Hosrc Heo Hesrc Ho48 Hs48 Hoal Hsal Lxo Lco Lys Lcs Lxe Lce Hn Hss Hval
iIntros #Hk Hc Hposix Hcod HBo HBs HBe HBsrc HΦ
rewrite rpl_entry
rm_enter "start"
iApply wp_alloc_ _ _ _ _ _ _ _ _ _ _ _ _ 4 ; reflexivity | lia | unfold max_allocation_size ; lia | intros m wd h base Hf Hw ; exact Kalloc_ _ _ _ _ Hf Hw |
iNext
iIntros base _ _
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; subst out ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
rm_enter "L10"
iApply wp_goto
iNext
rm_enter "L11"
iApply rpl_tail with Hk Hc Hposix Hcod HBo HBs HBe HBsrc HΦ ; assumption
rpl_mbsrtowcs's window
The memchr contract, for strnlen1.
Enter a block of rpl_mbsrtowcs.
Read byte k of the window in block blk, after the first: a flight to q + k, a half check against the first check, a load and its test. Leaves the branch on the test, with the byte named x.
ms_enter blk ; iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ ptr_addrq + Z.of_natk ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise | ; iNext ; gen_env ; destruct lookup_lt_is_Some_2bs ++ 0 k as x Hx ; rewrite length_app ; cbn ; lia | ; destruct nul_index_ _ _ Hbs Hx as Hxr & Hz & Hn ; iDestruct string_byte_ _ _ _ k x with Hs as (_ & Hl & Hb & Hk) ; exact Hx | ; iApply wp_half_check_read with Hl ; reflexivity | word_premise | reflexivity | exact Hc | addr_premise | addr_premise | lia | lia | apply Z.mod_1_r | ; iNext ; iIntros Hl ; gen_env ; iApply wp_raw_load_byte with Hl Hb ; reflexivity | word_premise | reflexivity | reflexivity | exact Hc | addr_premise | ; iNext ; iIntros Hl Hb ; iDestruct Hk with Hl Hb as Hs ; gen_env ; iApply wp_let ; reflexivity | reflexivity | word_premise | intros ; word_premise | ; iNext ; gen_env
The temporaries the converting loop keeps, and their values: the destination cursor, the source cursor, the count left, the state, srcp, its check, and the destination's address.
End the window at L37, with the window's length n in pr.8.
rpl_mbsrtowcs's window, blocks L29 to L57: with the source cursor q at a string bs, the loop reads up to four bytes, stopping at the NUL, and then asks strnlen1 for at most 12 more; pr.8 is then min(len + 1, 16), and the loop's other temporaries are as they were.
∀ e q dst len st sp c0 d0 b reg bs Φ
mbs_varse q dst len st sp c0 d0
SL.stringq b reg bs −∗ ▷∀e′, ⌜mbs_varse′ q dst len st sp c0 d0 ∧ lookupTAtom"pr.8" e′ = SomeWIntZ.minZ.of_natlengthbs + 1 16⌝ −∗ SL.stringq b reg bs −∗ WPERunmkFramembs_fn e′ [ ] None ExecTAtom"L37" b_instsmbs_block"L37" b_jumpmbs_block"L37" : cexpr {Φ} −∗ WPERunmkFramembs_fn e [ ] None ExecTAtom"L29" b_instsmbs_block"L29" b_jumpmbs_block"L29" : cexpr {Φ}
Proof 119 steps Qed
intros Hq & H7 & H1 & H2 & Hv2 & Hc0 & H23
iIntros Hs HK
iDestruct Hs as [%Hok Hps]
pose proof Hok as Hc & Hb0 & Hbq & Hend & H48 & Hbs
pose proof Hm := proj1Hlinked
The first byte, through a check.
destruct lookup_lt_is_Some_2bs ++ 0 0 as x0 Hx0 ; rewrite length_app ; cbn ; lia |
destruct nul_index_ _ _ Hbs Hx0 as Hx0r & Hz0 & Hn0
iDestruct string_byte_ _ _ _ 0 x0 with Hs as (_ & Hl & Hb & Hk) ; exact Hx0 |
iApply wp_check_read with Hl ; reflexivity | word_premise | exact Hc | addr_premise | addr_premise | apply Z.mod_1_r |
iNext
iIntros Hl
iApply wp_raw_load_byte with Hl Hb ; reflexivity | word_premise | reflexivity | reflexivity | exact Hc | addr_premise |
iNext
iIntros Hl Hb
iDestruct Hk with Hl Hb as Hs
iApply wp_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise |
iNext
destruct Z.eqb_specx0 0 as E0 | E0
{subst x0
The NUL first: a window of one byte.pose proof Hz0eq_refl as L0
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
close_window L0
pose proof Hn0E0 as L0
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
The second byte.
ms_enter "L36"
iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ ptr_addrq + Z.of_nat1 ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |
iNext
destruct lookup_lt_is_Some_2bs ++ 0 1 as x1 Hx1 ; rewrite length_app ; cbn ; lia |
destruct nul_index_ _ _ Hbs Hx1 as Hx1r & Hz1 & Hn1
iDestruct string_byte_ _ _ _ 1 x1 with Hs as (_ & Hl & Hb & Hk) ; exact Hx1 |
iApply wp_half_check_read with Hl ; reflexivity | word_premise | reflexivity | exact Hc | addr_premise | addr_premise | lia | lia | apply Z.mod_1_r |
iNext
iIntros Hl
iApply wp_raw_load_byte with Hl Hb ; reflexivity | word_premise | reflexivity | reflexivity | exact Hc | addr_premise |
iNext
iIntros Hl Hb
iDestruct Hk with Hl Hb as Hs
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ; word_premise |
iNext
destruct Z.eqb_specx1 0 as E1 | E1
{subst x1
pose proof Hz1eq_refl as L1
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
close_window L1
pose proof Hn1E1 as L1
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
The third byte.
destruct Z.eqb_specx2 0 as E2 | E2
{subst x2
pose proof Hz2eq_refl as L2
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
close_window L2
pose proof Hn2E2 as L2
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
The fourth byte.
destruct Z.eqb_specx3 0 as E3 | E3
{subst x3
pose proof Hz3eq_refl as L3
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
close_window L3
pose proof Hn3E3 as L3
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
Four bytes before the NUL: strnlen1 counts the rest, up to 12.
ms_enter "L57"
iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ ptr_addrq + Z.of_nat4 ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |
iNext
iDestruct string_suffix_ _ _ _ 4 with Hs as [Hs4 Hback] ; lia |
iApply wp_call_bind_ _ _ _ _ _ _ _ _ _ _ _ _ strnlen1_fn invocationstrnlen1_fn WPtrmkPtrptr_addrq + Z.of_nat4 ptr_capq; WInt12 ; word_premise | unfold find_fn ; rewrite Hm ; vm_compute ; reflexivity | reflexivity |
iNext
iApply HL.strnlen1_specregistry wi ge Hlinked with Hs4 ; exact Hmemchr | lia |
iNext
iIntros Hs4
iDestruct Hback with Hs4 as Hs
iExists _
iSplit ; iPureIntro ; reflexivity |
iNext
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ; word_premise |
iNext
iApply wp_goto
iNext
ms_enter "L37"
iApply HK with [%] Hs
split ; repeat split ; assumption |
rewrite length_drop
rewrite window_min ; reflexivity | lia
A string's pieces are a block from its offset: its life and its bytes with the NUL, and no aux slots.
Explore proof 4 tactics
Initial goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
Hlinked :
wi_lent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
set_spec :
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_pre :
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h
Kbyte :
Kstore :
Kalloc :
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
q :
b :
Z
reg :
bs :
listZ
rewrite / SL.string / string_ps / block_ps
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
Hlinked :
wi_lent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
set_spec :
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_pre :
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h
Kbyte :
Kstore :
Kalloc :
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
q :
b :
Z
reg :
bs :
listZ
cbn [ aux_ps ]
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
Hlinked :
wi_lent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
set_spec :
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_pre :
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h
Kbyte :
Kstore :
Kalloc :
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
q :
b :
Z
reg :
bs :
listZ
rewrite app_nil_r
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
Hlinked :
wi_lent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
set_spec :
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_pre :
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h
Kbyte :
Kstore :
Kalloc :
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
q :
b :
Z
reg :
bs :
listZ
done
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
An object's life, bytes and aux slots from offset o are its block from o.
Explore proof 2 tactics
Initial goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
Hlinked :
wi_lent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
set_spec :
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_pre :
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h
Kbyte :
Kstore :
Kalloc :
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
b :
Z
reg :
o :
Z
xs :
listZ
cs :
listcap
rewrite / block_ps / pts big_sepL_cons big_sepL_app / live / bytes / auxes / pts big_sepL_singleton
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
Hlinked :
wi_lent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
set_spec :
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_pre :
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h
Kbyte :
Kstore :
Kalloc :
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
b :
Z
reg :
o :
Z
xs :
listZ
cs :
listcap
done
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
errno's lookup has Campaign 4's contract.
The world interpretation survives a pointer store into a cell the program owns.
__errno_location() returns the errno cell and changes nothing: HelloClose.v's wp_close_errno over libc_world. A local rule, for promotion to a libc logic module.
Proof 30 steps Qed
iIntros HK
iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ LB.errno_contractrep [ ] True%I with [] [HK]
–apply linked_outside ; exact Hlinked | reflexivity
–apply linked_unbound ; exact Hlinked | reflexivity
–reflexivity
–exact Herrno_reg
–reflexivity
–split ; right ; eexists ; reflexivity | reflexivity
–iIntros σ Hσ _
iDestruct Hσ as h [_ %Hσ]
destruct Hlibc_ _ _ proj2proj2proj2Hσ as Hr & _
iPureIntro
split ; reflexivity |
–done
–iNext
iIntros σ tr vs s′ m′ w′ Hi Hσ _
destruct LB.errno_exact_ _ _ _ _ _ _ _ _ _ _ _ Hi as → & → & → & → & He
injection He as →
iDestruct Hσ as h [Hh %Hσ]
destruct Hlibc_ _ _ proj2proj2proj2Hσ as _ & _ & Ec & _
iModIntro
iExists _
iSplit
+iPureIntro
rewrite Ec
reflexivity
+iSplitL Hh ; iExists h ; iFrame ; done |
iExact HK
What rpl_mbsrtowcs's caller learns when it returns r, with dest's final bytes ws, errno's bytes xe and the length l of the source: EILSEQ, -1 with 84 in errno; or r wide characters, none zero, then a zero one.
Owning the bytes xs from o is owning their first n and the rest.
Explore proof 4 tactics
Initial goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
Hlinked :
wi_lent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
set_spec :
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_pre :
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h
Kbyte :
Kstore :
Kalloc :
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
Herrno_reg :
registryTAtom"__errno_location" = SomeLB.errno_contractrep
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, l, v ∈ PLiveb, VLivereg ++ PAuxb o, VAuxptr_capx :: cellb o ptr_addrx → h !! l = Somev → wim wd h → wistore_bytesstore_auxm b + o ptr_capxp b + o 8 ptr_addrxp wd overwritePLiveb, VLivereg ++ PAuxb o, VAuxptr_capxp :: cellb o ptr_addrxp h
b, o :
Z
xs :
listZ
n :
nat
intros Hn
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
Hlinked :
wi_lent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
set_spec :
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_pre :
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h
Kbyte :
Kstore :
Kalloc :
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
Herrno_reg :
registryTAtom"__errno_location" = SomeLB.errno_contractrep
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, l, v ∈ PLiveb, VLivereg ++ PAuxb o, VAuxptr_capx :: cellb o ptr_addrx → h !! l = Somev → wim wd h → wistore_bytesstore_auxm b + o ptr_capxp b + o 8 ptr_addrxp wd overwritePLiveb, VLivereg ++ PAuxb o, VAuxptr_capxp :: cellb o ptr_addrxp h
b, o :
Z
xs :
listZ
n :
nat
Hn :
n ≤ lengthxs%nat
assert E : Z.of_natn = Z.of_natlengthtaken xs by rewrite length_take ; lia
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
Hlinked :
wi_lent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
set_spec :
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_pre :
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h
Kbyte :
Kstore :
Kalloc :
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
Herrno_reg :
registryTAtom"__errno_location" = SomeLB.errno_contractrep
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, l, v ∈ PLiveb, VLivereg ++ PAuxb o, VAuxptr_capx :: cellb o ptr_addrx → h !! l = Somev → wim wd h → wistore_bytesstore_auxm b + o ptr_capxp b + o 8 ptr_addrxp wd overwritePLiveb, VLivereg ++ PAuxb o, VAuxptr_capxp :: cellb o ptr_addrxp h
b, o :
Z
xs :
listZ
n :
nat
Hn :
n ≤ lengthxs%nat
E :
n = lengthtaken xs
rewrite E - bytes_app take_drop
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
Hlinked :
wi_lent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
set_spec :
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_pre :
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h
Kbyte :
Kstore :
Kalloc :
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
Herrno_reg :
registryTAtom"__errno_location" = SomeLB.errno_contractrep
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, l, v ∈ PLiveb, VLivereg ++ PAuxb o, VAuxptr_capx :: cellb o ptr_addrx → h !! l = Somev → wim wd h → wistore_bytesstore_auxm b + o ptr_capxp b + o 8 ptr_addrxp wd overwritePLiveb, VLivereg ++ PAuxb o, VAuxptr_capxp :: cellb o ptr_addrxp h
b, o :
Z
xs :
listZ
n :
nat
Hn :
n ≤ lengthxs%nat
E :
n = lengthtaken xs
done
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Owning the slots cs from o is owning their first n and the rest.
Explore proof 4 tactics
Initial goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
Hlinked :
wi_lent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
set_spec :
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_pre :
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h
Kbyte :
Kstore :
Kalloc :
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
Herrno_reg :
registryTAtom"__errno_location" = SomeLB.errno_contractrep
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, l, v ∈ PLiveb, VLivereg ++ PAuxb o, VAuxptr_capx :: cellb o ptr_addrx → h !! l = Somev → wim wd h → wistore_bytesstore_auxm b + o ptr_capxp b + o 8 ptr_addrxp wd overwritePLiveb, VLivereg ++ PAuxb o, VAuxptr_capxp :: cellb o ptr_addrxp h
b, o :
Z
cs :
listcap
n :
nat
intros Hn
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
Hlinked :
wi_lent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
set_spec :
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_pre :
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h
Kbyte :
Kstore :
Kalloc :
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
Herrno_reg :
registryTAtom"__errno_location" = SomeLB.errno_contractrep
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, l, v ∈ PLiveb, VLivereg ++ PAuxb o, VAuxptr_capx :: cellb o ptr_addrx → h !! l = Somev → wim wd h → wistore_bytesstore_auxm b + o ptr_capxp b + o 8 ptr_addrxp wd overwritePLiveb, VLivereg ++ PAuxb o, VAuxptr_capxp :: cellb o ptr_addrxp h
b, o :
Z
cs :
listcap
n :
nat
Hn :
n ≤ lengthcs%nat
assert E : Z.of_natn = Z.of_natlengthtaken cs by rewrite length_take ; lia
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
Hlinked :
wi_lent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
set_spec :
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_pre :
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h
Kbyte :
Kstore :
Kalloc :
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
Herrno_reg :
registryTAtom"__errno_location" = SomeLB.errno_contractrep
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, l, v ∈ PLiveb, VLivereg ++ PAuxb o, VAuxptr_capx :: cellb o ptr_addrx → h !! l = Somev → wim wd h → wistore_bytesstore_auxm b + o ptr_capxp b + o 8 ptr_addrxp wd overwritePLiveb, VLivereg ++ PAuxb o, VAuxptr_capxp :: cellb o ptr_addrxp h
b, o :
Z
cs :
listcap
n :
nat
Hn :
n ≤ lengthcs%nat
E :
n = lengthtaken cs
rewrite E - auxes_app take_drop
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
Hlinked :
wi_lent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
set_spec :
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_pre :
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h
Kbyte :
Kstore :
Kalloc :
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
Herrno_reg :
registryTAtom"__errno_location" = SomeLB.errno_contractrep
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, l, v ∈ PLiveb, VLivereg ++ PAuxb o, VAuxptr_capx :: cellb o ptr_addrx → h !! l = Somev → wim wd h → wistore_bytesstore_auxm b + o ptr_capxp b + o 8 ptr_addrxp wd overwritePLiveb, VLivereg ++ PAuxb o, VAuxptr_capxp :: cellb o ptr_addrxp h
b, o :
Z
cs :
listcap
n :
nat
Hn :
n ≤ lengthcs%nat
E :
n = lengthtaken cs
done
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hn
assert E : Z.of_natn = Z.of_natlengthtaken cs by rewrite length_take ; lia
rewrite E - auxes_app take_drop
done
rpl_mbsrtowcs's converting loop, from block L28, by Löb induction: after i wide characters from the first j bytes of the string at p, with the state valid and in its initial shift state, every path returns what mbs_post says; the abort after an incomplete sequence is never reached.
∀ p b reg bs bd rd sb sr so be re oe spb spr spo codec dq p0 t0 rc rp Φ
0 < bd
bd mod 4 = 0
bd + 4 × Z.of_natlengthbs + 1 ≤ r_endrd
r_endrd ≤ 2 ^ 48
0 < sb
sb + so mod 4 = 0
0 < spb
0 ≤ spo
spb + spo mod 8 = 0
spb + spo + 8 ≤ r_endspr
r_endspr ≤ 2 ^ 48
0 < be
0 ≤ oe
be + oe + 4 ≤ r_endre
r_endre ≤ 2 ^ 48
⊢ ∀e i j : nat wpre cpre wrest crest ys cs xe ce x, ⌜mbs_varse mkPtrptr_addrp + Z.of_natj ptr_capp WPtrmkPtrbd + Z.of_nat4 × i Objbd WIntZ.of_natlengthbs + 1 − Z.of_nati WPtrmkPtrsb + so Objsb WPtrmkPtrspb + spo Objspb WPtrmkPtrspb + spo Objspb WIntbd ∧ i ≤ j ≤ lengthbs%nat ∧ lengthwpre = 4 × i%nat ∧ lengthcpre = 4 × i%nat ∧ lengthwrest = 4 × lengthbs + 1 − i%nat ∧ lengthcrest = 4 × lengthbs + 1 − i%nat ∧ wide_okwpre ∧ validcodec ys ∧ le_valuetake4 ys = 0 ∧ lengthys = 8%nat ∧ lengthcs = 8%nat ∧ lengthxe = 4%nat ∧ lengthce = 4%nat⌝ −∗ LL.lent0 p0 t0 −∗ SL.stringc_ptr 65824 rc c_bytes −∗ SL.stringposix_ptr 65856 rp posix_bytes −∗ pointstoPNamecodec_key dq VCodeccodec −∗ SL.stringp b reg bs −∗ livebd rd −∗ bytesbd 0 wpre −∗ auxesbd 0 cpre −∗ bytesbd Z.of_nat4 × i wrest −∗ auxesbd Z.of_nat4 × i crest −∗ ptsblock_pssb sr so ys cs −∗ ptsblock_psbe re oe xe ce −∗ livespb spr −∗ pcellspb spo x −∗ ∀r ws cws ys′ cs′ xe′ ce′ x′, ⌜mbs_postlengthbs r ws xe′ ∧ lengthws = 4 × lengthbs + 1%nat⌝ −∗ SL.stringc_ptr 65824 rc c_bytes −∗ SL.stringposix_ptr 65856 rp posix_bytes −∗ pointstoPNamecodec_key dq VCodeccodec −∗ SL.stringp b reg bs −∗ livebd rd −∗ bytesbd 0 ws −∗ auxesbd 0 cws −∗ ptsblock_pssb sr so ys′ cs′ −∗ ptsblock_psbe re oe xe′ ce′ −∗ livespb spr −∗ pcellspb spo x′ −∗ ΦRetWIntr −∗ WPERunmkFramembs_fn e [ ] None ExecTAtom"L28" b_instsmbs_block"L28" b_jumpmbs_block"L28" : cexpr {Φ}
Proof 190 steps Qed
intros Herr Hbd Hbd4 Hdend Hd48 Hsb Hsal Hspb Hspo Hspal Hspend Hsp48 Hbe Hoe Heend He48
pose proof Hlinked as Hm & _ & Hext
iLöb as IH
iIntros e i j wpre cpre wrest crest ys cs xe ce x Hq & H7 & H1 & H2 & Hv2 & Hc0 & H23 & Hij & Lwp & Lcp & Lwr & Lcr & Hwide & Hval & Hinit & Lys & Lcs & Lxe & Lce #Hk Hc Hposix Hcod Hs Hdl Hdw Hda Hrw Hra HBs HBe Hspl Hsp HΦ
iDestruct Hs as [%Hok Hps]
pose proof Hok as Hc & Hb0 & Hbp & Hsend & H48 & Hbs
Characters are left to write.
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ; word_premise |
iNext
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
ms_enter "L29"
The window over the suffix from byte j.
iDestruct string_suffix_ _ _ _ j with Hs as [Hsuf Hback] ; lia |
iApply mbs_window with Hsuf ; repeat split ; eassumption |
iNext
iIntros e′ Hq′ & H7′ & H1′ & H2′ & Hv2′ & Hc0′ & H23′ & Hn8 Hsuf
The next output word, and the source as a block.
assert Lr4 : 4 ≤ lengthwrest%nat by lia
assert Lc4 : 4 ≤ lengthcrest%nat by lia
iEval rewritebytes_split_ _ _ 4 Lr4 in Hrw
iDestruct Hrw as [Hw0 Hw1]
iEval rewriteauxes_split_ _ _ 4 Lc4 in Hra
iDestruct Hra as [Ha0 Ha1]
iAssert ptsblock_psbd rd Z.of_nat4 × i take4 wrest take4 crest with [Hdl Hw0 Ha0] as HBo ; rewrite - dest_block ; iFrame |
iEval rewritestring_block in Hsuf
iDestruct Hsuf as [%Hok′ HBsrc]
iApply wp_call_bind_ _ _ _ _ _ _ _ _ _ _ _ _ rpl_fn invocationrpl_fn WPtrmkPtrbd + Z.of_nat4 × i Objbd; WPtrmkPtrptr_addrp + Z.of_natj ptr_capp; WIntZ.minZ.of_natlengthdropj bs + 1 16; WPtrmkPtrsb + so Objsb ; word_premise | unfold find_fn ; rewrite Hm ; vm_compute ; reflexivity | reflexivity |
iNext
pose proof Hok' as Hc′ & _ & Hbq′ & Hsend′ & _ & Hbs′
assert Hal : bd + Z.of_nat4 × i mod 4 = 0
{replace bd + Z.of_nat4 × i with bd + Z.of_nati × 4 by lia
rewrite Z.mod_add ; exact Hbd4 | lia
assert Hss : Forallλx ⇒ 0 ≤ x < 256 dropj bs ++ 0
{apply Forall_app
split ; | repeat constructor ; lia
apply Forall_drop
eapply Forall_impl ; exact Hbs | intros y Hy ; cbv beta in Hy |- * ; lia
iApply rpl_mbrtowc_spec_ _ _ _ bd rd Z.of_nat4 × i take4 wrest take4 crest sb sr so ys cs be re oe xe ce b reg ptr_addrp + Z.of_natj − b dropj bs ++ 0 with Hk Hc Hposix Hcod HBo HBs HBe [HBsrc]
all: try first reflexivity | assumption | exact Herr | lia | cbn [ ptr_addr ptr_cap ] ; lia | rewrite length_take ; lia | rewrite length_app length_drop ; cbn [ length ] ; lia
{iEval cbnptr_addr in HBsrc
iExact HBsrc
iNext
iIntros r xo′ ys′ xe′ co′ cs′ ce′ Hres & Lxo′ & Lys′ & Lxe′ & Lco′ & Lcs′ & Lce′ Hc Hposix Hcod HBo HBs HBe HBsrc
iExists _
iSplit ; iPureIntro ; reflexivity |
iNext
iDestruct Hback with [HBsrc] as Hs
destruct rpl_step_ _ _ dropj bs _ _ _ _ _ _ Forall_drop_ _ _ Hbs Hval Hinit Hres as Hr64 & Hn2 & Hm1 & Hz & Hpos
iEval rewrite − dest_block in HBo
iDestruct HBo as (Hdl & Hw0 & Ha0)
Never incomplete: the abort is not reached.
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ; word_premise |
iNext
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
ms_enter "L82"
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ; word_premise |
iNext
destruct Z.eqb_specr 2 ^ 64 − 1 as Er | Er
EILSEQ: the cursor goes back through srcp, errno gets 84, and -1 returns.
{iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
ms_enter "L94"
iApply wp_renew with Hspl ; reflexivity | word_premise | reflexivity | reflexivity | addr_premise | addr_premise | cbn [ ptr_addr ] ; unfold raw_address ; drop_wraps_goal ; rewrite Z.add_0_r ; exact Hspal |
iNext
iIntros Hspl
iApply wp_raw_store_pointer with Hspl Hsp ; word_premise | word_premise | reflexivity | addr_premise | exact Hspal | intros Hl Hw ; exact Kpstore_ _ _ _ _ _ _ _ Hl Hw |
iNext
iIntros Hspl Hsp
iApply wp_goto
iNext
ms_enter "L196"
iApply wp_conv_errno
iNext
iEval rewrite − dest_block in HBe
iDestruct HBe as (Hel & Hew & Hea)
iApply wp_check with Hel ; reflexivity | word_premise | rewrite Herr ; reflexivity | rewrite Herr ; addr_premise | rewrite Herr ; addr_premise | apply Z.mod_1_r |
iNext
iIntros Hel
iApply wp_raw_store_w with Hel Hew ; word_premise | word_premise | rewrite Herr ; reflexivity | rewrite Herr ; addr_premise | exact Lxe' | intros Hl Hw ; exact Kstore_ _ _ _ _ _ _ _ Hl Hw |
iNext
iIntros Hel Hew
iApply wp_ret ; reflexivity | word_premise |
iNext
change 18446744073709551615 mod 2 ^ 64 with 2 ^ 64 − 1
iApply HΦ $! _ wpre ++ xo' ++ drop4 wrest cpre ++ co' ++ drop4 crest ys' cs' le_bytes84 4 ce' with [%] Hc Hposix Hcod Hs Hdl [Hdw Hw0 Hw1] [Hda Ha0 Ha1] HBs [Hel Hew Hea] Hspl Hsp
–split ; left ; split ; reflexivity | apply le_value_byte ; lia |
rewrite ! length_app length_drop
lia
–rewrite auxes_app auxes_app Lcp Lco' Z.add_0_l
iFrame
–rewrite - dest_block
iFrame
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
ms_enter "L89"
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ; word_premise |
iNext
destruct Z.eqb_specr 0 as Ez | Ez
The NUL: null goes back through srcp, and the count of characters returns.
{subst r
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
ms_enter "L31"
iApply wp_renew with Hspl ; reflexivity | word_premise | reflexivity | reflexivity | addr_premise | addr_premise | cbn [ ptr_addr ] ; unfold raw_address ; drop_wraps_goal ; rewrite Z.add_0_r ; exact Hspal |
iNext
iIntros Hspl
iApply wp_raw_store_pointer with Hspl Hsp ; word_premise | word_premise | reflexivity | addr_premise | exact Hspal | intros Hl Hw ; exact Kpstore_ _ _ _ _ _ _ _ Hl Hw |
iNext
iIntros Hspl Hsp
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ; word_premise |
iNext
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ; word_premise |
iNext
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ; word_premise |
iNext
iApply wp_ret ; reflexivity | word_premise |
iNext
assert E4 : bd + Z.of_nati + i + i + i + 0 − bd = Z.of_nati × 4 by lia
rewrite E4
rewrite Z.div_mul ; | lia
rewrite Z.mod_small ; | lia
iApply HΦ $! _ wpre ++ xo' ++ drop4 wrest cpre ++ co' ++ drop4 crest ys' cs' xe' ce' with [%] Hc Hposix Hcod Hs Hdl [Hdw Hw0 Hw1] [Hda Ha0 Ha1] HBs HBe Hspl Hsp
–split ; right ; exists i ; split ; reflexivity | ; split ; lia | ; split |
+rewrite <- Lwp
rewrite take_app_length
exact Hwide
+rewrite <- Lwp
rewrite drop_app_length
rewrite take_app_le ; | lia
rewrite take_ge ; | lia
exact Hzeq_refl
+rewrite ! length_app length_drop
lia
–rewrite auxes_app auxes_app Lcp Lco' Z.add_0_l
iFrame
A character: both cursors move on, and the loop goes round.
destruct HposEz Er as Hr0 & Hxo & Hv′ & Hi′
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
ms_enter "L102"
rewrite length_drop in Hr0
iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ ptr_addrp + Z.of_natj + Z.to_natr ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |
iNext
iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ bd + Z.of_nat4 × Si ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |
iNext
iApply wp_let ; reflexivity | reflexivity | word_premise | intros ; word_premise |
iNext
iApply wp_goto
iNext
ms_enter "L28"
iAssert auxesbd 0 cpre ++ co' with [Hda Ha0] as Hda ; rewrite auxes_app Lcp Z.add_0_l ; iFrame |
assert Eo : Z.of_nat4 × i + Z.of_nat4 = Z.of_nat4 × Si by lia
iEval rewriteEo in Hw1
iEval rewriteEo in Ha1
iApply IH $! _ Si j + Z.to_natr%nat wpre ++ xo' cpre ++ co' drop4 wrest drop4 crest ys' cs' xe' ce' x with [%] Hk Hc Hposix Hcod Hs Hdl Hdw Hda Hw1 Ha1 HBs HBe Hspl Hsp HΦ
pose proof wide_ok_app_ _ i Hwide Lwp Lxo' Hxo as Hw′
unfold mbs_vars
repeat match goal with|- _ ∧ _⇒splitend
all: try assumption ; try lia ; try rewrite length_app ; lia ; try rewrite length_drop ; lia
rpl_mbsrtowcs
rpl_mbsrtowcs's entry binds its four arguments.
Explore proof 1 tactics
Initial goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
registry :
name → optioncontractlibc_world
wi :
mem → libc_world → gmappiece pval → Prop
SafepointStable0 :
ge :
valid :
term → listZ → Prop
audit :
term → optionaudited_codec
rep :
mem → libc_world → Prop
requests :
listword → mem → libc_world → Z → Z → Prop
Hmbrtowc :
registryTAtom"mbrtowc" = Somembrtowc_contractvalid audit rep requests
Hvalid0 :
mbstate_zero_validvalid
Hbytes :
mbstate_valid_bytesvalid
errno :
Hlibc :
∀m : mem w : libc_world h : gmappiece pval, wim w h → libc_readyrep m w ∧ codec_currentlibc_localew.1 h ∧ libc_errnow.1 = errno ∧ libc_privatem w h
Haudit :
∀m : mem w : libc_world h : gmappiece pval, wim w h → hello_codec_profileaudit w
Kmbrtowc :
∀r : call_result args : listarg out src : ptr n : Z state : ptr s : R.state m : mem w : libc_world h : gmappiece pval trace : listevent values : listword s′ : R.state m′ : mem w′ : libc_world bo : Z ro : region oo : Z xo : listZ co : listcap bs : Z rs : region os : Z ys : listZ cs : listcap be : Z re : region oe : Z xe : listZ ce : listcap, M.E.invokembrtowc_contractvalid audit rep requests r args WPtrout; WPtrsrc; WIntn; WPtrstate s m w trace CallReturnvalues s′ m′ w′ → ∀l : piece v : pval, l, v ∈ block_psbo ro oo xo co ++ block_psbs rs os ys cs ++ block_psbe re oe xe ce → h !! l = Somev → wim w h → wim′ w′ overwriteblock_psbo ro oo mem_bytesm′ bo + oo 4 mem_auxesm′ bo + oo 4 ++ block_psbs rs os mem_bytesm′ bs + os 8 mem_auxesm′ bs + os 8 ++ block_psbe re oe mem_bytesm′ be + oe 4 mem_auxesm′ be + oe 4 h
Hlinked :
wi_lent :
∀m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ, wim w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
set_spec :
Hset :
registryTAtom"setlocale" = Someset_spec
Hset_ret :
contract_returnsset_spec = RClassP
Hset_pre :
Hset_query :
∀r : call_result args : listarg s : R.state m : mem w : libc_world h : gmappiece pval k : Z p : ptr t : listZ z : ptr trace : listevent ending : call_end s′ : R.state m′ : mem w′ : libc_world, wim w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokeset_spec r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Hstrlen :
registryTAtom"strlen" = Somestrlen_contractlibc_world
Hmemcpy :
registryTAtom"memcpy" = Somememcpy_contractlibc_world
Hstrcmp :
registryTAtom"strcmp" = Somestrcmp_contractlibc_world
Kcopy :
∀b : Z reg : region o : Z xs : listZ cs : listcap s : ptr n : Z m m′ : mem wd : libc_world h : gmappiece pval ys : listZ, copy_resultm ptr_addr ≔ b + o; ptr_cap ≔ Objb s n m′ → ∀l : piece v : pval, l, v ∈ block_psb reg o xs cs → h !! l = Somev → wim wd h → lengthys = lengthxs → wim′ wd overwriteblock_psb reg o ys slots_afterm′ b o lengthxs h
Kbyte :
Kstore :
Kalloc :
Hmemchr :
registryTAtom"memchr" = Somememchr_contractlibc_world
Herrno_reg :
registryTAtom"__errno_location" = SomeLB.errno_contractrep
Kpstore :
∀b : Z reg : region o : Z x xp : ptr m : mem wd : libc_world h : gmappiece pval, ∀l : piece v : pval, l, v ∈ PLiveb, VLivereg ++ PAuxb o, VAuxptr_capx :: cellb o ptr_addrx → h !! l = Somev → wim wd h → wistore_bytesstore_auxm b + o ptr_capxp b + o 8 ptr_addrxp wd overwritePLiveb, VLivereg ++ PAuxb o, VAuxptr_capxp :: cellb o ptr_addrxp h
dst, src :
len :
Z
ps :
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
reflexivity
rpl_mbsrtowcs(dest, srcp, len, ps) as main calls it: dest a fresh buffer of len wide characters, srcp a cell holding the string p, len the string's length and its NUL, and ps a non-null state, valid and in its initial shift state. The entry allocates a local it never uses, keeps ps, loads the string through srcp, a read-only literal or not, and goes to the converting loop (mbs_loop) with nothing written yet; the counting loop, for a null dest, is not reached. The call returns what mbs_post says.
∀ p b reg bs bd rd ws cws sb sr so ys cs be re oe xe ce spb spr spo codec dq p0 t0 rc rp Φ
0 < bd
bd mod 4 = 0
bd + 4 × Z.of_natlengthbs + 1 ≤ r_endrd
r_endrd ≤ 2 ^ 48
0 < sb
0 ≤ so
sb + so mod 4 = 0
sb + so + 8 ≤ r_endsr
r_endsr ≤ 2 ^ 48
0 < spb
0 ≤ spo
spb + spo mod 8 = 0
spb + spo + 8 ≤ r_endspr
r_endspr ≤ 2 ^ 48
0 < be
0 ≤ oe
be + oe + 4 ≤ r_endre
r_endre ≤ 2 ^ 48
lengthws = 4 × lengthbs + 1%nat
lengthcws = 4 × lengthbs + 1%nat
validcodec ys
lengthys = 8%nat
lengthcs = 8%nat
lengthxe = 4%nat
lengthce = 4%nat
LL.lent0 p0 t0 −∗ SL.stringc_ptr 65824 rc c_bytes −∗ SL.stringposix_ptr 65856 rp posix_bytes −∗ pointstoPNamecodec_key dq VCodeccodec −∗ SL.stringp b reg bs −∗ livebd rd −∗ bytesbd 0 ws −∗ auxesbd 0 cws −∗ ptsblock_pssb sr so ys cs −∗ ptsblock_psbe re oe xe ce −∗ livespb spr −∗ pcellspb spo p −∗ ∀r ws′ cws′ ys′ cs′ xe′ ce′ x′, ⌜mbs_postlengthbs r ws′ xe′ ∧ lengthws′ = 4 × lengthbs + 1%nat⌝ −∗ SL.stringc_ptr 65824 rc c_bytes −∗ SL.stringposix_ptr 65856 rp posix_bytes −∗ pointstoPNamecodec_key dq VCodeccodec −∗ SL.stringp b reg bs −∗ livebd rd −∗ bytesbd 0 ws′ −∗ auxesbd 0 cws′ −∗ ptsblock_pssb sr so ys′ cs′ −∗ ptsblock_psbe re oe xe′ ce′ −∗ livespb spr −∗ pcellspb spo x′ −∗ ΦRetWIntr −∗ WPERuninvocationmbs_fn WPtrmkPtrbd Objbd; WPtrmkPtrspb + spo Objspb; WIntZ.of_natlengthbs + 1; WPtrmkPtrsb + so Objsb : cexpr {Φ}
Proof 54 steps Qed
intros Herr Hbd Hbd4 Hdend Hd48 Hsb Hso Hsal Hsend′ Hs48 Hspb Hspo Hspal Hspend Hsp48 Hbe Hoe Heend He48 Lws Lcws Hval Hinit Lys Lcs Lxe Lce
iIntros #Hk Hc Hposix Hcod Hs Hdl Hdw Hda HBs HBe Hspl Hsp HΦ
iDestruct Hs as [%Hok Hps]
pose proof Hok as Hcp & Hb0 & Hbp & Hsend & H48 & Hbs
rewrite mbs_entry
iApply wp_enter_ _ _ _ _ _ _ _ mbs_block"start" ; vm_compute ; reflexivity | word_premise | ; iNext
The local for the counting loop, never used here.
iApply wp_alloc_ _ _ _ _ _ _ _ _ _ _ _ _ 8 ; reflexivity | lia | unfold max_allocation_size ; lia | intros m wd h base Hf Hw ; exact Kalloc_ _ _ _ _ Hf Hw |
iNext
iIntros base _ _
ps is not null.
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; cbn ; rewrite Z.mod_smallsb + so ; | lia ; rewrite proj2Z.eqb_neqsb + so _ ; reflexivity | change 0 mod 2 ^ 64 mod 2 ^ 64 with 0 ; lia |
iNext
cbn [ Z.eqb edge_label ]
ms_enter "L10"
The string through srcp.
iApply wp_check_read with Hspl ; reflexivity | word_premise | left ; reflexivity | addr_premise | addr_premise | addr_premise |
iNext
iIntros Hspl
iApply wp_raw_load_pointer_in with Hspl Hsp Hps ; reflexivity | word_premise | left ; reflexivity | addr_premise | addr_premise | lia | intros xb Hxb ; exists reg ; destruct Hcp as Hcp | Hcp ; rewrite Hcp in Hxb ; destruct Hxb as Hxb | Hxb ; try discriminate Hxb ; injection Hxb as ← ; apply elem_of_cons ; left ; reflexivity |
iNext
iIntros Hspl Hsp Hps
dest is not null: the converting loop.
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; cbn ; rewrite Z.mod_smallbd ; | lia ; rewrite proj2Z.eqb_neqbd _ ; reflexivity | change 0 mod 2 ^ 64 mod 2 ^ 64 with 0 ; lia |
iNext
cbn [ Z.eqb edge_label ]
iApply wp_enter_ _ _ _ _ _ _ _ mbs_block"L28" ; vm_compute ; reflexivity | word_premise | ; iNext
iPoseProof mbs_loopp b reg bs bd rd sb sr so be re oe spb spr spo codec dq p0 t0 rc rp Φ Herr Hbd Hbd4 Hdend Hd48 Hsb Hsal Hspb Hspo Hspal Hspend Hsp48 Hbe Hoe Heend He48 as L
iApply L $! _ 0%nat 0%nat [ ] [ ] ws cws ys cs xe ce p with [%] Hk Hc Hposix Hcod Hs Hdl [] [] Hdw Hda HBs HBe Hspl Hsp HΦ
rewrite Ep
replace bd + Z.of_nat4 × 0 with bd by lia
split ; unfold mbs_vars ; repeat split ; cbn ; first reflexivity | rewrite Z.mod_small ; reflexivity | lia |
split ; lia |
split ; reflexivity |
split ; reflexivity |
split ; rewrite Lws ; lia |
split ; rewrite Lcws ; lia |
split ; exact wide_ok_nil |
repeat split ; assumption
HelloConvOn over a Logic instance of its own.