rocq/theories/HelloConvDefs.v
The pure part of GNU Hello's conversion proofs
The definitions and lemmas of HelloConv that do not need the program logic: memory read as lists, spans of live objects, a block after a call, libc's private state, and the IR of gnulib's rpl_mbrtowc and rpl_mbsrtowcs. They live apart so that HelloMain, which uses a few of them, does not wait for the conversion's triples.
From iris.proofmode Require Import proofmode
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
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).
202Definition 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.
247Definition 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