rocq/theories/HelloDiagnosticChecks.v
Logical controls for Hello's four-argument diagnostic binding. These use actual fixture literals and the supplied machine, but empty private native inventories. The Iris rule is partial correctness, not native execution or a proof of the complete close_stdout body.
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 String ZArith List Lia
From Nanofil Require Import Term Syntax Values Memory Runtime Semantics Run ExternalCalls ExternalMachine Stdio Shutdown Streams Formatting Libc LibcStreams Pieces Heap ContractFrame Logic StringLogic MemLogic LentLogic Locale LibcStreamLogic LibcErrnoLogic LibcStreamTokens LibcStreamAdapter LibcDiagnosticLogic HelloModule HelloLeaf HelloReach HelloStdio
Import ListNotations
Open Scope Z_scope
Open Scope list_scope
Import LG LG.L
119; 114; 105; 116; 101; 32; 101; 114; 114; 111; 114
λ a ⇒
65744 ≤? a && a <? 65747
→
nthZ.to_nata − 65744 37; 115 0
else
m_regionsconversion_mem ++ mkRegion65680 65696 GlobalData Live; mkRegion65744 65752 GlobalData Live
Explore proof 2 tactics
Initial goal
vm_compute
⊢
Somer_base ≔ 65744; r_end ≔ 65752; r_kind ≔ GlobalData; r_life ≔ Live = Somer_base ≔ 65744; r_end ≔ 65752; r_kind ≔ GlobalData; r_life ≔ Live ∧ Live = Live
∧
∧
→
→
Datatypes.Eq = Datatypes.Gt → False
∧
Z.posH
⇒
match x1 with
H0~1%positive
⇒
match x2 with
H0~0%positive
⇒
match x2 with
=
∧
37 = 37
∧
∧
→
→
Datatypes.Lt = Datatypes.Gt → False
∧
Z.posH
⇒
match x1 with
H0~1%positive
⇒
match x2 with
H0~0%positive
⇒
match x2 with
=
∧
115 = 115
∧
∧
→
→
Datatypes.Lt = Datatypes.Gt → False
∧
Z.posH
⇒
match x1 with
H0~1%positive
⇒
match x2 with
H0~0%positive
⇒
match x2 with
=
∧
0 = 0
∧
Somer_base ≔ 65680; r_end ≔ 65696; r_kind ≔ GlobalData; r_life ≔ Live = Somer_base ≔ 65680; r_end ≔ 65696; r_kind ≔ GlobalData; r_life ≔ Live ∧ Live = Live
∧
∧
→
→
Datatypes.Eq = Datatypes.Gt → False
∧
Z.posH
⇒
match x1 with
H0~1%positive
⇒
match x2 with
H0~0%positive
⇒
match x2 with
=
∧
119 = 119
∧
∧
→
→
Datatypes.Lt = Datatypes.Gt → False
∧
Z.posH
⇒
match x1 with
H0~1%positive
⇒
match x2 with
H0~0%positive
⇒
match x2 with
=
∧
114 = 114
∧
∧
→
→
Datatypes.Lt = Datatypes.Gt → False
∧
Z.posH
⇒
match x1 with
H0~1%positive
⇒
match x2 with
H0~0%positive
⇒
match x2 with
=
∧
105 = 105
∧
∧
→
→
Datatypes.Lt = Datatypes.Gt → False
∧
Z.posH
⇒
match x1 with
H0~1%positive
⇒
match x2 with
H0~0%positive
⇒
match x2 with
=
∧
116 = 116
∧
∧
→
→
Datatypes.Lt = Datatypes.Gt → False
∧
Z.posH
⇒
match x1 with
H0~1%positive
⇒
match x2 with
H0~0%positive
⇒
match x2 with
=
∧
101 = 101
∧
∧
→
→
Datatypes.Lt = Datatypes.Gt → False
∧
Z.posH
⇒
match x1 with
H0~1%positive
⇒
match x2 with
H0~0%positive
⇒
match x2 with
=
∧
32 = 32
∧
∧
→
→
Datatypes.Lt = Datatypes.Gt → False
∧
Z.posH
⇒
match x1 with
H0~1%positive
⇒
match x2 with
H0~0%positive
⇒
match x2 with
=
∧
101 = 101
∧
∧
→
→
Datatypes.Lt = Datatypes.Gt → False
∧
Z.posH
⇒
match x1 with
H0~1%positive
⇒
match x2 with
H0~0%positive
⇒
match x2 with
=
∧
114 = 114
∧
∧
→
→
Datatypes.Lt = Datatypes.Gt → False
∧
Z.posH
⇒
match x1 with
H0~1%positive
⇒
match x2 with
H0~0%positive
⇒
match x2 with
=
∧
114 = 114
∧
∧
→
→
Datatypes.Lt = Datatypes.Gt → False
∧
Z.posH
⇒
match x1 with
H0~1%positive
⇒
match x2 with
H0~0%positive
⇒
match x2 with
=
∧
111 = 111
∧
∧
→
→
Datatypes.Lt = Datatypes.Gt → False
∧
Z.posH
⇒
match x1 with
H0~1%positive
⇒
match x2 with
H0~0%positive
⇒
match x2 with
=
∧
114 = 114
∧
∧
→
→
Datatypes.Lt = Datatypes.Gt → False
∧
Z.posH
⇒
match x1 with
H0~1%positive
⇒
match x2 with
H0~0%positive
⇒
match x2 with
=
∧
0 = 0
∧
True
repeat split ; intros;repeat match goal withH : Some_ = Some_ |- _⇒injection H as ←end;vm_compute;intuition congruence
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
vm_compute
repeat split ; intros;repeat match goal withH : Some_ = Some_ |- _⇒injection H as ←end;vm_compute;intuition congruence
Explore proof 15 tactics
Initial goal
induction ps as | k u ps IH ; intros Hdup l v Hin ; set_solver |
inversion Hdup as [ |? ? Hnot Htail ] ; subst
k :
u :
Hdup :
base.NoDupk, u :: ps.*1
l :
v :
Hin :
l, v ∈ k, u :: ps
⊢
overwritek, u :: ps h !! l = Somev
apply elem_of_cons in Hin as E | Hin
2 openk :
u :
Hdup :
base.NoDupk, u :: ps.*1
l :
v :
E :
l, v = k, u
⊢
overwritek, u :: ps h !! l = Somev
focused goal
k :
u :
Hdup :
base.NoDupk, u :: ps.*1
l :
v :
Hin :
l, v ∈ ps
⊢
overwritek, u :: ps h !! l = Somev
–injection E as ← ←
2 openl :
v :
Hdup :
base.NoDupl, v :: ps.*1
⊢
overwritel, v :: ps h !! l = Somev
deferred goal
k :
u :
Hdup :
base.NoDupk, u :: ps.*1
l :
v :
Hin :
l, v ∈ ps
⊢
overwritek, u :: ps h !! l = Somev
cbn [ overwrite ]
2 openl :
v :
Hdup :
base.NoDupl, v :: ps.*1
⊢
<[l, v.1 ≔ l, v.2]>overwriteps h !! l = Somev
deferred goal
k :
u :
Hdup :
base.NoDupk, u :: ps.*1
l :
v :
Hin :
l, v ∈ ps
⊢
overwritek, u :: ps h !! l = Somev
apply lookup_insert_eq
deferred goal
k :
u :
Hdup :
base.NoDupk, u :: ps.*1
l :
v :
Hin :
l, v ∈ ps
⊢
overwritek, u :: ps h !! l = Somev
–cbn [ overwrite ]
k :
u :
Hdup :
base.NoDupk, u :: ps.*1
l :
v :
Hin :
l, v ∈ ps
⊢
<[k, u.1 ≔ k, u.2]>overwriteps h !! l = Somev
rewrite lookup_insert_ne ; apply IH ; assumption |
k :
u :
Hdup :
base.NoDupk, u :: ps.*1
l :
v :
Hin :
l, v ∈ ps
⊢
k, u.1 ≠ l
simpl
k :
u :
Hdup :
base.NoDupk, u :: ps.*1
l :
v :
Hin :
l, v ∈ ps
⊢
k ≠ l
intros E
k :
u :
Hdup :
base.NoDupk, u :: ps.*1
l :
v :
Hin :
l, v ∈ ps
E :
k = l
⊢
False
subst k
apply Hnot
u :
l :
Hdup :
base.NoDupl, u :: ps.*1
v :
Hin :
l, v ∈ ps
apply list_elem_of_fmap
u :
l :
Hdup :
base.NoDupl, u :: ps.*1
v :
Hin :
l, v ∈ ps
exists l, v
u :
l :
Hdup :
base.NoDupl, u :: ps.*1
v :
Hin :
l, v ∈ ps
⊢
l = l, v.1 ∧ l, v ∈ ps
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
induction ps as | k u ps IH ; intros Hdup l v Hin ; set_solver |
inversion Hdup as [ |? ? Hnot Htail ] ; subst
apply elem_of_cons in Hin as E | Hin
–cbn [ overwrite ]
rewrite lookup_insert_ne ; apply IH ; assumption |
simpl
intros E
subst k
apply Hnot
apply list_elem_of_fmap
exists l, v
auto
Explore proof 3 tactics
Initial goal
⊢
∀opened : bool l : piece v : pval, l, v ∈ hello_diagnostic_pieces → heapopened !! l = Somev
intros opened
opened :
bool
⊢
∀l : piece v : pval, l, v ∈ hello_diagnostic_pieces → heapopened !! l = Somev
apply overwrite_owned
opened :
bool
⊢
base.NoDuphello_diagnostic_pieces.*1
apply NoDup_ListNoDup , hello_diagnostic_keys
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Explore proof 13 tactics
Initial goal
intros opened l v Hl
⊢
destruct lookup_overwritehello_diagnostic_pieces HelloErrnoChecks.heap l v Hl as Hin | _ Hold
2 open⊢
focused goal
⊢
–eapply all_agree_elem ; exact literals_agree | exact Hin
deferred goal
⊢
–unfold HelloErrnoChecks.heap in Hold
apply elem_of_list_to_map_2 in Hold
eapply all_agree_elem ; | exact Hold
change all_agreememory byte_ps5120 0 errno_bytesmemory 5120 0
apply errno_bytes_agree
split ; discriminate |
split ; | reflexivity
split ; simpl ; lia |
⊢
∃base : Z reg : region, ptr_capspan_ptrspan_ptr ≔ ptr_addr ≔ 5120 + 0; ptr_cap ≔ Obj5120; span_size ≔ 4 = Objbase ∧ object_regionbase m_regionsmemory = Somereg ∧ r_lifereg = Live ∧ access_resmemory ptr_addrspan_ptrspan_ptr ≔ ptr_addr ≔ 5120 + 0; ptr_cap ≔ Obj5120; span_size ≔ 4 Objbase span_sizespan_ptr ≔ ptr_addr ≔ 5120 + 0; ptr_cap ≔ Obj5120; span_size ≔ 4 Write 1 = Someok
exists 5120, mkRegion5120 5128 Heap Live
⊢
ptr_capspan_ptrspan_ptr ≔ ptr_addr ≔ 5120 + 0; ptr_cap ≔ Obj5120; span_size ≔ 4 = Obj5120 ∧ object_region5120 m_regionsmemory = Somer_base ≔ 5120; r_end ≔ 5128; r_kind ≔ Heap; r_life ≔ Live ∧ r_lifer_base ≔ 5120; r_end ≔ 5128; r_kind ≔ Heap; r_life ≔ Live = Live ∧ access_resmemory ptr_addrspan_ptrspan_ptr ≔ ptr_addr ≔ 5120 + 0; ptr_cap ≔ Obj5120; span_size ≔ 4 Obj5120 span_sizespan_ptr ≔ ptr_addr ≔ 5120 + 0; ptr_cap ≔ Obj5120; span_size ≔ 4 Write 1 = Someok
repeat split ; reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros opened l v Hl
destruct lookup_overwritehello_diagnostic_pieces HelloErrnoChecks.heap l v Hl as Hin | _ Hold
–eapply all_agree_elem ; exact literals_agree | exact Hin
–unfold HelloErrnoChecks.heap in Hold
apply elem_of_list_to_map_2 in Hold
eapply all_agree_elem ; | exact Hold
change all_agreememory byte_ps5120 0 errno_bytesmemory 5120 0
apply errno_bytes_agree
split ; discriminate |
split ; | reflexivity
split ; simpl ; lia |
repeat split ; reflexivity
∀ b reg
object_regionb m_regionsmemory = Somereg
Explore proof 3 tactics
Initial goal
⊢
∀b : Z reg : region, object_regionb m_regionsmemory = Somereg → Inb, reg 1024, r_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live; 2048, r_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live; 3072, r_base ≔ 3072; r_end ≔ 3080; r_kind ≔ Stack; r_life ≔ Live; 4096, r_base ≔ 4096; r_end ≔ 4104; r_kind ≔ GlobalData; r_life ≔ Live; 5120, r_base ≔ 5120; r_end ≔ 5128; r_kind ≔ Heap; r_life ≔ Live; 65680, r_base ≔ 65680; r_end ≔ 65696; r_kind ≔ GlobalData; r_life ≔ Live; 65744, r_base ≔ 65744; r_end ≔ 65752; r_kind ≔ GlobalData; r_life ≔ Live
intros b reg Hreg
⊢
Inb, reg 1024, r_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live; 2048, r_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live; 3072, r_base ≔ 3072; r_end ≔ 3080; r_kind ≔ Stack; r_life ≔ Live; 4096, r_base ≔ 4096; r_end ≔ 4104; r_kind ≔ GlobalData; r_life ≔ Live; 5120, r_base ≔ 5120; r_end ≔ 5128; r_kind ≔ Heap; r_life ≔ Live; 65680, r_base ≔ 65680; r_end ≔ 65696; r_kind ≔ GlobalData; r_life ≔ Live; 65744, r_base ≔ 65744; r_end ≔ 65752; r_kind ≔ GlobalData; r_life ≔ Live
cbn [ memory conversion_mem m_regions app object_region r_base ] in Hreg
b :
Z
reg :
Hreg :
else
None
=
Somereg
⊢
Inb, reg 1024, r_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live; 2048, r_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live; 3072, r_base ≔ 3072; r_end ≔ 3080; r_kind ≔ Stack; r_life ≔ Live; 4096, r_base ≔ 4096; r_end ≔ 4104; r_kind ≔ GlobalData; r_life ≔ Live; 5120, r_base ≔ 5120; r_end ≔ 5128; r_kind ≔ Heap; r_life ≔ Live; 65680, r_base ≔ 65680; r_end ≔ 65696; r_kind ≔ GlobalData; r_life ≔ Live; 65744, r_base ≔ 65744; r_end ≔ 65752; r_kind ≔ GlobalData; r_life ≔ Live
repeat destruct _ =? _ eqn :? in Hreg ; try discriminate ; injection Hreg as ←;repeat match goal withH : _ =? _ = true |- _⇒apply Z.eqb_eq in Hend;subst;simpl;tauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros b reg Hreg
cbn [ memory conversion_mem m_regions app object_region r_base ] in Hreg
repeat destruct _ =? _ eqn :? in Hreg ; try discriminate ; injection Hreg as ←;repeat match goal withH : _ =? _ = true |- _⇒apply Z.eqb_eq in Hend;subst;simpl;tauto
Explore proof 3 tactics
Initial goal
intros b1 r1 b2 r2 E1 _ E2 _ Hne
b1 :
Z
r1 :
b2 :
Z
r2 :
E1 :
object_regionb1 m_regionsmemory = Somer1
E2 :
object_regionb2 m_regionsmemory = Somer2
Hne :
b1 ≠ b2
apply regions in E1 , E2
b1 :
Z
r1 :
b2 :
Z
r2 :
E1 :
Inb1, r1 1024, r_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live; 2048, r_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live; 3072, r_base ≔ 3072; r_end ≔ 3080; r_kind ≔ Stack; r_life ≔ Live; 4096, r_base ≔ 4096; r_end ≔ 4104; r_kind ≔ GlobalData; r_life ≔ Live; 5120, r_base ≔ 5120; r_end ≔ 5128; r_kind ≔ Heap; r_life ≔ Live; 65680, r_base ≔ 65680; r_end ≔ 65696; r_kind ≔ GlobalData; r_life ≔ Live; 65744, r_base ≔ 65744; r_end ≔ 65752; r_kind ≔ GlobalData; r_life ≔ Live
E2 :
Inb2, r2 1024, r_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live; 2048, r_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live; 3072, r_base ≔ 3072; r_end ≔ 3080; r_kind ≔ Stack; r_life ≔ Live; 4096, r_base ≔ 4096; r_end ≔ 4104; r_kind ≔ GlobalData; r_life ≔ Live; 5120, r_base ≔ 5120; r_end ≔ 5128; r_kind ≔ Heap; r_life ≔ Live; 65680, r_base ≔ 65680; r_end ≔ 65696; r_kind ≔ GlobalData; r_life ≔ Live; 65744, r_base ≔ 65744; r_end ≔ 65752; r_kind ≔ GlobalData; r_life ≔ Live
Hne :
b1 ≠ b2
repeat destruct E1 as E1 | E1 ; try contradiction ; injection E1 as ← ← ; repeat destruct E2 as E2 | E2 ; try contradiction ; injection E2 as ← ← ; simpl in * ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros b1 r1 b2 r2 E1 _ E2 _ Hne
apply regions in E1 , E2
repeat destruct E1 as E1 | E1 ; try contradiction ; injection E1 as ← ← ; repeat destruct E2 as E2 | E2 ; try contradiction ; injection E2 as ← ← ; simpl in * ; lia
Explore proof 21 tactics
Initial goal
split ; change 0 < 4294967296 ≤ 281474976710656 ; lia |
⊢
∀b : Z reg : region, object_regionb m_regionsmemory = Somereg → 0 ≤ b < InterpRuntime.start ∧ r_endreg ≤ InterpRuntime.start ∧ r_lifereg = Freed → r_endreg = b ∧ ∀a : Z, InterpRuntime.start ≤ a → m_bytesmemory a = 0 ∧ m_auxmemory a = CNone
split
2 open⊢
∀b : Z reg : region, object_regionb m_regionsmemory = Somereg → 0 ≤ b < InterpRuntime.start ∧ r_endreg ≤ InterpRuntime.start ∧ r_lifereg = Freed → r_endreg = b
–intros b reg E
2 open⊢
0 ≤ b < InterpRuntime.start ∧ r_endreg ≤ InterpRuntime.start ∧ r_lifereg = Freed → r_endreg = b
apply regions in E
2 openb :
Z
reg :
E :
Inb, reg 1024, r_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live; 2048, r_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live; 3072, r_base ≔ 3072; r_end ≔ 3080; r_kind ≔ Stack; r_life ≔ Live; 4096, r_base ≔ 4096; r_end ≔ 4104; r_kind ≔ GlobalData; r_life ≔ Live; 5120, r_base ≔ 5120; r_end ≔ 5128; r_kind ≔ Heap; r_life ≔ Live; 65680, r_base ≔ 65680; r_end ≔ 65696; r_kind ≔ GlobalData; r_life ≔ Live; 65744, r_base ≔ 65744; r_end ≔ 65752; r_kind ≔ GlobalData; r_life ≔ Live
⊢
0 ≤ b < InterpRuntime.start ∧ r_endreg ≤ InterpRuntime.start ∧ r_lifereg = Freed → r_endreg = b
change 0 ≤ b < 4294967296 ∧ r_endreg ≤ 4294967296 ∧ r_lifereg = Freed → r_endreg = b
2 openb :
Z
reg :
E :
Inb, reg 1024, r_base ≔ 1024; r_end ≔ 1056; r_kind ≔ GlobalData; r_life ≔ Live; 2048, r_base ≔ 2048; r_end ≔ 2056; r_kind ≔ Stack; r_life ≔ Live; 3072, r_base ≔ 3072; r_end ≔ 3080; r_kind ≔ Stack; r_life ≔ Live; 4096, r_base ≔ 4096; r_end ≔ 4104; r_kind ≔ GlobalData; r_life ≔ Live; 5120, r_base ≔ 5120; r_end ≔ 5128; r_kind ≔ Heap; r_life ≔ Live; 65680, r_base ≔ 65680; r_end ≔ 65696; r_kind ≔ GlobalData; r_life ≔ Live; 65744, r_base ≔ 65744; r_end ≔ 65752; r_kind ≔ GlobalData; r_life ≔ Live
repeat destruct E as E | E ; try contradiction ; injection E as ← ← ; simpl ; intuition try discriminate ; lia
–intros a Ha
change 4294967296 ≤ a in Ha
cbn [ memory conversion_mem m_bytes m_aux ]
assert Htext : 65680 ≤? a && a <? 65692 = false
2 opena :
Z
Ha :
4294967296 ≤ a
⊢
65680 ≤? a && a <? 65692 = false
{apply Bool.andb_false_iff
2 opena :
Z
Ha :
4294967296 ≤ a
⊢
65680 ≤? a = false ∨ a <? 65692 = false
right
2 opena :
Z
Ha :
4294967296 ≤ a
⊢
a <? 65692 = false
apply Z.ltb_ge
2 opena :
Z
Ha :
4294967296 ≤ a
⊢
65692 ≤ a
lia
assert Hfmt : 65744 ≤? a && a <? 65747 = false
2 opena :
Z
Ha :
4294967296 ≤ a
Htext :
65680 ≤? a && a <? 65692 = false
⊢
65744 ≤? a && a <? 65747 = false
{apply Bool.andb_false_iff
2 opena :
Z
Ha :
4294967296 ≤ a
Htext :
65680 ≤? a && a <? 65692 = false
⊢
65744 ≤? a = false ∨ a <? 65747 = false
right
2 opena :
Z
Ha :
4294967296 ≤ a
Htext :
65680 ≤? a && a <? 65692 = false
⊢
a <? 65747 = false
apply Z.ltb_ge
2 opena :
Z
Ha :
4294967296 ≤ a
Htext :
65680 ≤? a && a <? 65692 = false
⊢
65747 ≤ a
lia
rewrite Htext Hfmt
repeat match goal with|- context [a =? ]⇒destruct Z.eqb_speca b ; subst ; lia | end;auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; change 0 < 4294967296 ≤ 281474976710656 ; lia |
split
–intros b reg E
apply regions in E
repeat destruct E as E | E ; try contradiction ; injection E as ← ← ; simpl ; intuition try discriminate ; lia
–intros a Ha
change 4294967296 ≤ a in Ha
cbn [ memory conversion_mem m_bytes m_aux ]
assert Htext : 65680 ≤? a && a <? 65692 = false
{apply Bool.andb_false_iff
right
apply Z.ltb_ge
lia
assert Hfmt : 65744 ≤? a && a <? 65747 = false
{apply Bool.andb_false_iff
right
apply Z.ltb_ge
lia
rewrite Htext Hfmt
repeat match goal with|- context [a =? ]⇒destruct Z.eqb_speca b ; subst ; lia | end;auto
∀ opened
libc_stream_readyλ_ _ ⇒ True memory F.worldopened
Proof 57 steps Qed
intros opened
assert Hl : locale_readyλ_ _ ⇒ True memory libc_localefstconversion_world
{split ; exact I |
split ; constructor |
split
–intros k _
split ; discriminate |
vm_compute
repeat split ; congruence
–split ; constructor |
split ; constructor |
intros k _
exists 4096
split ; right ; reflexivity | reflexivity
assert He : errno_cellmemory mkPtr5120 Obj5120
{split ; discriminate |
split ; | reflexivity
split ; simpl ; lia |
repeat split ; reflexivity
assert Hfiles : libc_file_readymemory mkPtr5120 Obj5120 F.out_file ∧ libc_file_readymemory mkPtr5120 Obj5120 F.err_file
{assert Hread : ∀a, a = 1024 ∨ a = 2048 → readable_bytesmemory mkPtra Obja 1
{intros a → | → ; split ; simpl ; lia | | simpl ; lia |
all: split
1: {exists 1024, mkRegion1024 1056 GlobalData Live
auto
all: split ; reflexivity |
all: intros i Hi ; assert i = 0 as → by lia ; vm_compute ; split ; congruence
assert Hapart : ∀a n, a ≠ 5120 → file_errno_apartmemory mkPtr5120 Obj5120 mkLibcFilemkPtra Obja n [ ] [ ] [ ]
{intros a n Hne
split ; intros root |
intros base Hbase | Hbase ; injection Hbase as <-| discriminate
split ; intros |
split ; intros Hnone | source & Hin & Hcap | source & addr & Hin & Ha & Hsize & _ | b & & _ ; try discriminate ; simpl in Hin ; destruct Hin as [ <-| [ ] ] ; simpl in * ; congruence | unfold span_contains in Ha ; simpl in Ha ; lia | discriminate | unfold span_contains in Ha ; simpl in Ha ; lia
split ; unfold F.out_file , F.err_file , libc_file_ready ; split ; discriminate | | discriminate |
all: split ; apply Hread ; auto |
all: split ; simpl ; lia |
all: split ; constructor |
all: split ; constructor |
all: split ; constructor | apply Hapart ; lia
split ; exact I |
split ; exact Hl |
split ; exact He |
split ; split ; destruct opened ; repeat constructor ; lia | reflexivity |
split ; apply stdout_initial_wf |
split ; constructor |
split ; simpl ; lia |
split ; exact I |
split ; simpl ; lia |
split ; destruct opened ; reflexivity |
split ; intros _ ; exact proj1Hfiles |
split ; intros _ ; exact proj2Hfiles |
intros p file Hfile base Hin
unfold libc_file_at in Hfile
destruct same_filep libc_stdoutF.worldopened ; destruct opened | destruct same_filep libc_stderrF.worldopened ; try discriminate ; injection Hfile as ← ; contradiction
mkDiagnosticContextlibc_world λ_ w ⇒ ∃file, libc_file_atw libc_stderrw = Somefile ∧ orientationlibc_stream_statew libc_stderrw ≠ WideOriented λ_ _ ⇒ [ ] λ_ ⇒ [ ] λ_ _ _ ⇒ False λ_ _ _ body segments ⇒ segments = body; 10 λ_ _ ⇒ True
libc_diagnostic_wiλ_ _ ⇒ True native T.out T.err 5120 0 m w h ∧ diagnostic_readynative m w
Explore proof 14 tactics
Initial goal
intros
unfold heap
opened :
bool
key :
Z
⊢
overwritehello_diagnostic_pieces HelloErrnoChecks.heap !! PNamekey = None
rewrite overwrite_out
2 openopened :
bool
key :
Z
⊢
HelloErrnoChecks.heap !! PNamekey = None
focused goal
opened :
bool
key :
Z
⊢
PNamekey ∉ hello_diagnostic_pieces.*1
–unfold HelloErrnoChecks.heap
2 opendeferred goal
opened :
bool
key :
Z
⊢
PNamekey ∉ hello_diagnostic_pieces.*1
apply not_elem_of_list_to_map_1
2 opendeferred goal
opened :
bool
key :
Z
⊢
PNamekey ∉ hello_diagnostic_pieces.*1
rewrite byte_ps_keys
2 opendeferred goal
opened :
bool
key :
Z
⊢
PNamekey ∉ hello_diagnostic_pieces.*1
intros Hin
2 opendeferred goal
opened :
bool
key :
Z
⊢
PNamekey ∉ hello_diagnostic_pieces.*1
apply list_elem_of_fmap in Hin as i & E & _
2 opendeferred goal
opened :
bool
key :
Z
⊢
PNamekey ∉ hello_diagnostic_pieces.*1
discriminate E
deferred goal
opened :
bool
key :
Z
⊢
PNamekey ∉ hello_diagnostic_pieces.*1
–intros Hin
⊢
False
apply list_elem_of_fmap in Hin as l v & E & Hin
⊢
False
apply list_elem_of_In in Hin
⊢
False
vm_compute in Hin
opened :
bool
key :
Z
l :
v :
E :
PNamekey = l, v.1
Hin :
PLive65744, VLiver_base ≔ 65744; r_end ≔ 65752; r_kind ≔ GlobalData; r_life ≔ Live = l, v ∨ PByte65744 0, VByte37 = l, v ∨ PByte65744 1, VByte115 = l, v ∨ PByte65744 2, VByte0 = l, v ∨ PLive65680, VLiver_base ≔ 65680; r_end ≔ 65696; r_kind ≔ GlobalData; r_life ≔ Live = l, v ∨ PByte65680 0, VByte119 = l, v ∨ PByte65680 1, VByte114 = l, v ∨ PByte65680 2, VByte105 = l, v ∨ PByte65680 3, VByte116 = l, v ∨ PByte65680 4, VByte101 = l, v ∨ PByte65680 5, VByte32 = l, v ∨ PByte65680 6, VByte101 = l, v ∨ PByte65680 7, VByte114 = l, v ∨ PByte65680 8, VByte114 = l, v ∨ PByte65680 9, VByte111 = l, v ∨ PByte65680 10, VByte114 = l, v ∨ PByte65680 11, VByte0 = l, v ∨ False
⊢
False
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; discriminate E
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
unfold heap
rewrite overwrite_out
–unfold HelloErrnoChecks.heap
apply not_elem_of_list_to_map_1
rewrite byte_ps_keys
intros Hin
apply list_elem_of_fmap in Hin as i & E & _
discriminate E
–intros Hin
apply list_elem_of_fmap in Hin as l v & E & Hin
apply list_elem_of_In in Hin
vm_compute in Hin
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; discriminate E
Explore proof 15 tactics
Initial goal
intros opened l v Hin
unfold heap
⊢
overwritehello_diagnostic_pieces HelloErrnoChecks.heap !! l = Somev
rewrite overwrite_out
2 open⊢
HelloErrnoChecks.heap !! l = Somev
focused goal
⊢
l ∉ hello_diagnostic_pieces.*1
–unfold HelloErrnoChecks.heap
2 open⊢
list_to_mapbyte_ps5120 0 0; 0; 0; 0 !! l = Somev
deferred goal
⊢
l ∉ hello_diagnostic_pieces.*1
apply elem_of_list_to_map_1 ; | exact Hin
2 open⊢
base.NoDupbyte_ps5120 0 0; 0; 0; 0.*1
deferred goal
⊢
l ∉ hello_diagnostic_pieces.*1
change base.NoDupPByte5120 0; PByte5120 1; PByte5120 2; PByte5120 3
2 opendeferred goal
⊢
l ∉ hello_diagnostic_pieces.*1
repeat apply base.NoDup_cons_2 ; set_solver |
2 opendeferred goal
⊢
l ∉ hello_diagnostic_pieces.*1
apply base.NoDup_nil_2
deferred goal
⊢
l ∉ hello_diagnostic_pieces.*1
–destruct MemLogic.byte_ps_elem_ _ _ _ _ Hin as i & x & Hi & → & →
opened :
bool
i :
nat
x :
Z
Hi :
0; 0; 0; 0 !! i = Somex
⊢
PByte5120 0 + i ∉ hello_diagnostic_pieces.*1
clear Hin
opened :
bool
i :
nat
x :
Z
Hi :
0; 0; 0; 0 !! i = Somex
⊢
PByte5120 0 + i ∉ hello_diagnostic_pieces.*1
intros Hkey
⊢
False
apply list_elem_of_fmap in Hkey as l v & E & Hin
opened :
bool
i :
nat
x :
Z
Hi :
0; 0; 0; 0 !! i = Somex
l :
v :
E :
PByte5120 0 + i = l, v.1
Hin :
l, v ∈ hello_diagnostic_pieces
⊢
False
apply list_elem_of_In in Hin
opened :
bool
i :
nat
x :
Z
Hi :
0; 0; 0; 0 !! i = Somex
l :
v :
E :
PByte5120 0 + i = l, v.1
Hin :
Inl, v hello_diagnostic_pieces
⊢
False
vm_compute in Hin
opened :
bool
i :
nat
x :
Z
Hi :
0; 0; 0; 0 !! i = Somex
l :
v :
E :
PByte5120 0 + i = l, v.1
Hin :
PLive65744, VLiver_base ≔ 65744; r_end ≔ 65752; r_kind ≔ GlobalData; r_life ≔ Live = l, v ∨ PByte65744 0, VByte37 = l, v ∨ PByte65744 1, VByte115 = l, v ∨ PByte65744 2, VByte0 = l, v ∨ PLive65680, VLiver_base ≔ 65680; r_end ≔ 65696; r_kind ≔ GlobalData; r_life ≔ Live = l, v ∨ PByte65680 0, VByte119 = l, v ∨ PByte65680 1, VByte114 = l, v ∨ PByte65680 2, VByte105 = l, v ∨ PByte65680 3, VByte116 = l, v ∨ PByte65680 4, VByte101 = l, v ∨ PByte65680 5, VByte32 = l, v ∨ PByte65680 6, VByte101 = l, v ∨ PByte65680 7, VByte114 = l, v ∨ PByte65680 8, VByte114 = l, v ∨ PByte65680 9, VByte111 = l, v ∨ PByte65680 10, VByte114 = l, v ∨ PByte65680 11, VByte0 = l, v ∨ False
⊢
False
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; discriminate E
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros opened l v Hin
unfold heap
rewrite overwrite_out
–unfold HelloErrnoChecks.heap
apply elem_of_list_to_map_1 ; | exact Hin
repeat apply base.NoDup_cons_2 ; set_solver |
apply base.NoDup_nil_2
–destruct MemLogic.byte_ps_elem_ _ _ _ _ Hin as i & x & Hi & → & →
clear Hin
intros Hkey
apply list_elem_of_fmap in Hkey as l v & E & Hin
apply list_elem_of_In in Hin
vm_compute in Hin
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; discriminate E
Explore proof 38 tactics
Initial goal
intros opened
assert Hoff : pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
2 openopened :
bool
⊢
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
focused goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
{intros l v Hl Hnot
2 open⊢
match l with
⇒
∀reg : region, live_atmemory b reg → 0 ≤ o → b + o < r_endreg → ¬span_containserrno_span5120 0 b + o
_
⇒
True
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
apply stream_data_lookup in Hl as Hl _
2 open⊢
match l with
⇒
∀reg : region, live_atmemory b reg → 0 ≤ o → b + o < r_endreg → ¬span_containserrno_span5120 0 b + o
_
⇒
True
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
destruct lookup_overwritehello_diagnostic_pieces HelloErrnoChecks.heap l v Hl as Hin | _ Hold
3 openopened :
bool
l :
v :
Hl :
heapopened !! l = Somev
Hnot :
l ∉ errno_keys5120 0
Hin :
l, v ∈ hello_diagnostic_pieces
⊢
match l with
⇒
∀reg : region, live_atmemory b reg → 0 ≤ o → b + o < r_endreg → ¬span_containserrno_span5120 0 b + o
_
⇒
True
focused goal
opened :
bool
l :
v :
Hl :
heapopened !! l = Somev
Hnot :
l ∉ errno_keys5120 0
Hold :
HelloErrnoChecks.heap !! l = Somev
⊢
match l with
⇒
∀reg : region, live_atmemory b reg → 0 ≤ o → b + o < r_endreg → ¬span_containserrno_span5120 0 b + o
_
⇒
True
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
–apply list_elem_of_In in Hin
3 openopened :
bool
l :
v :
Hl :
heapopened !! l = Somev
Hnot :
l ∉ errno_keys5120 0
Hin :
Inl, v hello_diagnostic_pieces
⊢
match l with
⇒
∀reg : region, live_atmemory b reg → 0 ≤ o → b + o < r_endreg → ¬span_containserrno_span5120 0 b + o
_
⇒
True
deferred goal
opened :
bool
l :
v :
Hl :
heapopened !! l = Somev
Hnot :
l ∉ errno_keys5120 0
Hold :
HelloErrnoChecks.heap !! l = Somev
⊢
match l with
⇒
∀reg : region, live_atmemory b reg → 0 ≤ o → b + o < r_endreg → ¬span_containserrno_span5120 0 b + o
_
⇒
True
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
vm_compute in Hin
3 openopened :
bool
l :
v :
Hl :
heapopened !! l = Somev
Hnot :
l ∉ errno_keys5120 0
Hin :
PLive65744, VLiver_base ≔ 65744; r_end ≔ 65752; r_kind ≔ GlobalData; r_life ≔ Live = l, v ∨ PByte65744 0, VByte37 = l, v ∨ PByte65744 1, VByte115 = l, v ∨ PByte65744 2, VByte0 = l, v ∨ PLive65680, VLiver_base ≔ 65680; r_end ≔ 65696; r_kind ≔ GlobalData; r_life ≔ Live = l, v ∨ PByte65680 0, VByte119 = l, v ∨ PByte65680 1, VByte114 = l, v ∨ PByte65680 2, VByte105 = l, v ∨ PByte65680 3, VByte116 = l, v ∨ PByte65680 4, VByte101 = l, v ∨ PByte65680 5, VByte32 = l, v ∨ PByte65680 6, VByte101 = l, v ∨ PByte65680 7, VByte114 = l, v ∨ PByte65680 8, VByte114 = l, v ∨ PByte65680 9, VByte111 = l, v ∨ PByte65680 10, VByte114 = l, v ∨ PByte65680 11, VByte0 = l, v ∨ False
⊢
match l with
⇒
∀reg : region, live_atmemory b reg → 0 ≤ o → b + o < r_endreg → ¬span_containserrno_span5120 0 b + o
_
⇒
True
deferred goal
opened :
bool
l :
v :
Hl :
heapopened !! l = Somev
Hnot :
l ∉ errno_keys5120 0
Hold :
HelloErrnoChecks.heap !! l = Somev
⊢
match l with
⇒
∀reg : region, live_atmemory b reg → 0 ≤ o → b + o < r_endreg → ¬span_containserrno_span5120 0 b + o
_
⇒
True
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; cbn ; try exact I ; intros reg Hlive Hlo Hhi Hspan ; unfold span_contains , errno_span in Hspan ; simpl in Hspan ; lia
2 opendeferred goal
opened :
bool
l :
v :
Hl :
heapopened !! l = Somev
Hnot :
l ∉ errno_keys5120 0
Hold :
HelloErrnoChecks.heap !! l = Somev
⊢
match l with
⇒
∀reg : region, live_atmemory b reg → 0 ≤ o → b + o < r_endreg → ¬span_containserrno_span5120 0 b + o
_
⇒
True
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
–exfalso
2 openopened :
bool
l :
v :
Hl :
heapopened !! l = Somev
Hnot :
l ∉ errno_keys5120 0
Hold :
HelloErrnoChecks.heap !! l = Somev
⊢
False
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
apply Hnot
2 openopened :
bool
l :
v :
Hl :
heapopened !! l = Somev
Hnot :
l ∉ errno_keys5120 0
Hold :
HelloErrnoChecks.heap !! l = Somev
⊢
l ∈ errno_keys5120 0
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
unfold HelloErrnoChecks.heap in Hold
2 openopened :
bool
l :
v :
Hl :
heapopened !! l = Somev
Hnot :
l ∉ errno_keys5120 0
Hold :
list_to_mapbyte_ps5120 0 0; 0; 0; 0 !! l = Somev
⊢
l ∈ errno_keys5120 0
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
apply elem_of_list_to_map_2 in Hold
2 openopened :
bool
l :
v :
Hl :
heapopened !! l = Somev
Hnot :
l ∉ errno_keys5120 0
Hold :
l, v ∈ byte_ps5120 0 0; 0; 0; 0
⊢
l ∈ errno_keys5120 0
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
change l ∈ byte_ps5120 0 0; 0; 0; 0.*1
2 openopened :
bool
l :
v :
Hl :
heapopened !! l = Somev
Hnot :
l ∉ errno_keys5120 0
Hold :
l, v ∈ byte_ps5120 0 0; 0; 0; 0
⊢
l ∈ byte_ps5120 0 0; 0; 0; 0.*1
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
apply list_elem_of_fmap
2 openopened :
bool
l :
v :
Hl :
heapopened !! l = Somev
Hnot :
l ∉ errno_keys5120 0
Hold :
l, v ∈ byte_ps5120 0 0; 0; 0; 0
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
exists l, v
2 openopened :
bool
l :
v :
Hl :
heapopened !! l = Somev
Hnot :
l ∉ errno_keys5120 0
Hold :
l, v ∈ byte_ps5120 0 0; 0; 0; 0
⊢
l = l, v.1 ∧ l, v ∈ byte_ps5120 0 0; 0; 0; 0
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
auto
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
assert Hpair : stream_tokens_wiλ_ _ ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
2 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
focused goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
{split ; split ; reflexivity | simpl ; lia |
2 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
token_wfT.err ∧ token_baseT.out ≠ token_baseT.err ∧ token_keyT.out ≠ token_keyT.err ∧ libc_stdoutF.worldopened = token_handleT.out ∧ libc_stderrF.worldopened = token_handleT.err ∧ stream_currentT.out F.worldopened heapopened ∧ stream_currentT.err F.worldopened heapopened ∧ ∀d : stream_token, d = T.out ∨ d = T.err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 memory F.worldopened stream_data_heaptoken_baseT.out token_baseT.err heapopened ∧ ids_apartlibc_stream_releasesF.worldopened token_handled heapopened
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
split ; split ; reflexivity | simpl ; lia |
2 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
token_baseT.out ≠ token_baseT.err ∧ token_keyT.out ≠ token_keyT.err ∧ libc_stdoutF.worldopened = token_handleT.out ∧ libc_stderrF.worldopened = token_handleT.err ∧ stream_currentT.out F.worldopened heapopened ∧ stream_currentT.err F.worldopened heapopened ∧ ∀d : stream_token, d = T.out ∨ d = T.err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 memory F.worldopened stream_data_heaptoken_baseT.out token_baseT.err heapopened ∧ ids_apartlibc_stream_releasesF.worldopened token_handled heapopened
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
split ; discriminate |
2 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
token_keyT.out ≠ token_keyT.err ∧ libc_stdoutF.worldopened = token_handleT.out ∧ libc_stderrF.worldopened = token_handleT.err ∧ stream_currentT.out F.worldopened heapopened ∧ stream_currentT.err F.worldopened heapopened ∧ ∀d : stream_token, d = T.out ∨ d = T.err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 memory F.worldopened stream_data_heaptoken_baseT.out token_baseT.err heapopened ∧ ids_apartlibc_stream_releasesF.worldopened token_handled heapopened
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
split ; discriminate |
2 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
libc_stdoutF.worldopened = token_handleT.out ∧ libc_stderrF.worldopened = token_handleT.err ∧ stream_currentT.out F.worldopened heapopened ∧ stream_currentT.err F.worldopened heapopened ∧ ∀d : stream_token, d = T.out ∨ d = T.err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 memory F.worldopened stream_data_heaptoken_baseT.out token_baseT.err heapopened ∧ ids_apartlibc_stream_releasesF.worldopened token_handled heapopened
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
split ; reflexivity |
2 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
libc_stderrF.worldopened = token_handleT.err ∧ stream_currentT.out F.worldopened heapopened ∧ stream_currentT.err F.worldopened heapopened ∧ ∀d : stream_token, d = T.out ∨ d = T.err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 memory F.worldopened stream_data_heaptoken_baseT.out token_baseT.err heapopened ∧ ids_apartlibc_stream_releasesF.worldopened token_handled heapopened
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
split ; reflexivity |
2 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
stream_currentT.out F.worldopened heapopened ∧ stream_currentT.err F.worldopened heapopened ∧ ∀d : stream_token, d = T.out ∨ d = T.err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 memory F.worldopened stream_data_heaptoken_baseT.out token_baseT.err heapopened ∧ ids_apartlibc_stream_releasesF.worldopened token_handled heapopened
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
split ; unfold stream_current ; rewrite names_absent ; exact I |
2 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
stream_currentT.err F.worldopened heapopened ∧ ∀d : stream_token, d = T.out ∨ d = T.err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 memory F.worldopened stream_data_heaptoken_baseT.out token_baseT.err heapopened ∧ ids_apartlibc_stream_releasesF.worldopened token_handled heapopened
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
split ; unfold stream_current ; rewrite names_absent ; exact I |
2 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
∀d : stream_token, d = T.out ∨ d = T.err → libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handled 5120 0 memory F.worldopened stream_data_heaptoken_baseT.out token_baseT.err heapopened ∧ ids_apartlibc_stream_releasesF.worldopened token_handled heapopened
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
intros d → | →
3 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handleT.out 5120 0 memory F.worldopened stream_data_heaptoken_baseT.out token_baseT.err heapopened ∧ ids_apartlibc_stream_releasesF.worldopened token_handleT.out heapopened
focused goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handleT.err 5120 0 memory F.worldopened stream_data_heaptoken_baseT.out token_baseT.err heapopened ∧ ids_apartlibc_stream_releasesF.worldopened token_handleT.err heapopened
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
all: split ; | intros base l v Hin ; destruct opened ; contradiction
3 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handleT.out 5120 0 memory F.worldopened stream_data_heaptoken_baseT.out token_baseT.err heapopened
focused goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
libc_errno_wiλ_ : mem _ : libc_world ⇒ True token_handleT.err 5120 0 memory F.worldopened stream_data_heaptoken_baseT.out token_baseT.err heapopened
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
all: split ; apply ready |
3 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
libc_errnoF.worldopened.1 = ptr_addr ≔ 5120 + 0; ptr_cap ≔ Obj5120 ∧ roots_apartlibc_stream_aux_rootsF.worldopened token_handleT.out stream_data_heaptoken_baseT.out token_baseT.err heapopened memory ∧ ids_apartlibc_stream_releasesF.worldopened token_handleT.out stream_data_heaptoken_baseT.out token_baseT.err heapopened ∧ pieces_offerrno_keys5120 0 stream_data_heaptoken_baseT.out token_baseT.err heapopened memory span_containserrno_span5120 0
focused goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
libc_errnoF.worldopened.1 = ptr_addr ≔ 5120 + 0; ptr_cap ≔ Obj5120 ∧ roots_apartlibc_stream_aux_rootsF.worldopened token_handleT.err stream_data_heaptoken_baseT.out token_baseT.err heapopened memory ∧ ids_apartlibc_stream_releasesF.worldopened token_handleT.err stream_data_heaptoken_baseT.out token_baseT.err heapopened ∧ pieces_offerrno_keys5120 0 stream_data_heaptoken_baseT.out token_baseT.err heapopened memory span_containserrno_span5120 0
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
all: split ; reflexivity |
3 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
roots_apartlibc_stream_aux_rootsF.worldopened token_handleT.out stream_data_heaptoken_baseT.out token_baseT.err heapopened memory ∧ ids_apartlibc_stream_releasesF.worldopened token_handleT.out stream_data_heaptoken_baseT.out token_baseT.err heapopened ∧ pieces_offerrno_keys5120 0 stream_data_heaptoken_baseT.out token_baseT.err heapopened memory span_containserrno_span5120 0
focused goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
roots_apartlibc_stream_aux_rootsF.worldopened token_handleT.err stream_data_heaptoken_baseT.out token_baseT.err heapopened memory ∧ ids_apartlibc_stream_releasesF.worldopened token_handleT.err stream_data_heaptoken_baseT.out token_baseT.err heapopened ∧ pieces_offerrno_keys5120 0 stream_data_heaptoken_baseT.out token_baseT.err heapopened memory span_containserrno_span5120 0
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
all: split ; intros root a Hin ; destruct opened ; contradiction |
3 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
ids_apartlibc_stream_releasesF.worldopened token_handleT.out stream_data_heaptoken_baseT.out token_baseT.err heapopened ∧ pieces_offerrno_keys5120 0 stream_data_heaptoken_baseT.out token_baseT.err heapopened memory span_containserrno_span5120 0
focused goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
⊢
ids_apartlibc_stream_releasesF.worldopened token_handleT.err stream_data_heaptoken_baseT.out token_baseT.err heapopened ∧ pieces_offerrno_keys5120 0 stream_data_heaptoken_baseT.out token_baseT.err heapopened memory span_containserrno_span5120 0
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
all: split ; intros base l v Hin ; destruct opened ; contradiction | exact Hoff
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
split
2 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
⊢
libc_diagnostic_wiλ_ : mem _ : libc_world ⇒ True native T.out T.err 5120 0 memory F.worldopened heapopened
focused goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
⊢
diagnostic_readynative memory F.worldopened
–split ; exact Hpair |
2 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
⊢
roots_apartdiagnostic_writesnative F.worldopened stream_data_heaptoken_baseT.out token_baseT.err heapopened memory ∧ diagnostic_nameT.out heapopened ∧ diagnostic_nameT.err heapopened
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
⊢
diagnostic_readynative memory F.worldopened
split ; intros root a |
2 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
⊢
diagnostic_nameT.out heapopened ∧ diagnostic_nameT.err heapopened
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
⊢
diagnostic_readynative memory F.worldopened
unfold diagnostic_name
2 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
⊢
_
⇒
False
∧
_
⇒
False
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
⊢
diagnostic_readynative memory F.worldopened
rewrite ! names_absent
2 openopened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
⊢
True ∧ True
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
⊢
diagnostic_readynative memory F.worldopened
auto
deferred goal
opened :
bool
Hoff :
pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
Hpair :
stream_tokens_wiλ_ : mem _ : libc_world ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
⊢
diagnostic_readynative memory F.worldopened
–split ; exists F.err_file ; destruct opened ; reflexivity | destruct opened ; discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros opened
assert Hoff : pieces_offerrno_keys5120 0 stream_data_heap1024 2048 heapopened memory span_containserrno_span5120 0
{intros l v Hl Hnot
apply stream_data_lookup in Hl as Hl _
destruct lookup_overwritehello_diagnostic_pieces HelloErrnoChecks.heap l v Hl as Hin | _ Hold
–apply list_elem_of_In in Hin
vm_compute in Hin
repeat destruct Hin as Hin | Hin ; try contradiction ; injection Hin as ← ← ; cbn ; try exact I ; intros reg Hlive Hlo Hhi Hspan ; unfold span_contains , errno_span in Hspan ; simpl in Hspan ; lia
–exfalso
apply Hnot
unfold HelloErrnoChecks.heap in Hold
apply elem_of_list_to_map_2 in Hold
change l ∈ byte_ps5120 0 0; 0; 0; 0.*1
apply list_elem_of_fmap
exists l, v
auto
assert Hpair : stream_tokens_wiλ_ _ ⇒ True T.out T.err 5120 0 memory F.worldopened heapopened
{split ; split ; reflexivity | simpl ; lia |
split ; split ; reflexivity | simpl ; lia |
split ; discriminate |
split ; discriminate |
split ; reflexivity |
split ; reflexivity |
split ; unfold stream_current ; rewrite names_absent ; exact I |
split ; unfold stream_current ; rewrite names_absent ; exact I |
intros d → | →
all: split ; | intros base l v Hin ; destruct opened ; contradiction
all: split ; apply ready |
all: split ; reflexivity |
all: split ; intros root a Hin ; destruct opened ; contradiction |
all: split ; intros base l v Hin ; destruct opened ; contradiction | exact Hoff
split
–split ; exists F.err_file ; destruct opened ; reflexivity | destruct opened ; discriminate
libc_error_contractλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False native
Explore proof 10 tactics
Initial goal
⊢
∀opened : bool, contract_prespec words memory F.worldopened
intros
opened :
bool
⊢
contract_prespec words memory F.worldopened
eapply hello_diagnostic_admitted with h := heapopened file := F.err_file
8 openopened :
bool
⊢
0 ≤ 0 < 2 ^ 32
focused goal
opened :
bool
⊢
∀l : piece v : pval, l, v ∈ hello_diagnostic_pieces → heapopened !! l = Somev
focused goal
opened :
bool
⊢
diagnostic_readynative memory F.worldopened
focused goal
opened :
bool
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True memory F.worldopened
focused goal
opened :
bool
⊢
Forallwritable_spanmemory diagnostic_writesnative F.worldopened
focused goal
opened :
bool
⊢
libc_file_atF.worldopened libc_stderrF.worldopened = SomeF.err_file
focused goal
opened :
bool
⊢
orientationlibc_stream_stateF.worldopened libc_stderrF.worldopened ≠ WideOriented
–lia
7 opendeferred goal
opened :
bool
⊢
∀l : piece v : pval, l, v ∈ hello_diagnostic_pieces → heapopened !! l = Somev
deferred goal
opened :
bool
⊢
diagnostic_readynative memory F.worldopened
deferred goal
opened :
bool
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True memory F.worldopened
deferred goal
opened :
bool
⊢
Forallwritable_spanmemory diagnostic_writesnative F.worldopened
deferred goal
opened :
bool
⊢
libc_file_atF.worldopened libc_stderrF.worldopened = SomeF.err_file
deferred goal
opened :
bool
⊢
orientationlibc_stream_stateF.worldopened libc_stderrF.worldopened ≠ WideOriented
–apply heap_agrees
6 opendeferred goal
opened :
bool
⊢
∀l : piece v : pval, l, v ∈ hello_diagnostic_pieces → heapopened !! l = Somev
deferred goal
opened :
bool
⊢
diagnostic_readynative memory F.worldopened
deferred goal
opened :
bool
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True memory F.worldopened
deferred goal
opened :
bool
⊢
Forallwritable_spanmemory diagnostic_writesnative F.worldopened
deferred goal
opened :
bool
⊢
libc_file_atF.worldopened libc_stderrF.worldopened = SomeF.err_file
deferred goal
opened :
bool
⊢
orientationlibc_stream_stateF.worldopened libc_stderrF.worldopened ≠ WideOriented
–apply heap_owned
5 opendeferred goal
opened :
bool
⊢
diagnostic_readynative memory F.worldopened
deferred goal
opened :
bool
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True memory F.worldopened
deferred goal
opened :
bool
⊢
Forallwritable_spanmemory diagnostic_writesnative F.worldopened
deferred goal
opened :
bool
⊢
libc_file_atF.worldopened libc_stderrF.worldopened = SomeF.err_file
deferred goal
opened :
bool
⊢
orientationlibc_stream_stateF.worldopened libc_stderrF.worldopened ≠ WideOriented
–exact proj2entry_wiopened
4 opendeferred goal
opened :
bool
⊢
libc_stream_readyλ_ : mem _ : libc_world ⇒ True memory F.worldopened
deferred goal
opened :
bool
⊢
Forallwritable_spanmemory diagnostic_writesnative F.worldopened
deferred goal
opened :
bool
⊢
libc_file_atF.worldopened libc_stderrF.worldopened = SomeF.err_file
deferred goal
opened :
bool
⊢
orientationlibc_stream_stateF.worldopened libc_stderrF.worldopened ≠ WideOriented
–apply ready
3 opendeferred goal
opened :
bool
⊢
Forallwritable_spanmemory diagnostic_writesnative F.worldopened
deferred goal
opened :
bool
⊢
libc_file_atF.worldopened libc_stderrF.worldopened = SomeF.err_file
deferred goal
opened :
bool
⊢
orientationlibc_stream_stateF.worldopened libc_stderrF.worldopened ≠ WideOriented
–constructor
2 opendeferred goal
opened :
bool
⊢
libc_file_atF.worldopened libc_stderrF.worldopened = SomeF.err_file
deferred goal
opened :
bool
⊢
orientationlibc_stream_stateF.worldopened libc_stderrF.worldopened ≠ WideOriented
–destruct opened ; reflexivity
deferred goal
opened :
bool
⊢
orientationlibc_stream_stateF.worldopened libc_stderrF.worldopened ≠ WideOriented
–destruct opened ; discriminate
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
eapply hello_diagnostic_admitted with h := heapopened file := F.err_file
–lia
–apply heap_agrees
–apply heap_owned
–exact proj2entry_wiopened
–apply ready
–constructor
–destruct opened ; reflexivity
–destruct opened ; discriminate
∀ m w
∃file, libc_file_atw libc_stderrw = Somefile ∧ orientationlibc_stream_statew libc_stderrw ≠ WideOriented
Explore proof 3 tactics
Initial goal
⊢
∀m : mem w : libc_world, contract_prespec words m w → ∃file : libc_file, libc_file_atw libc_stderrw = Somefile ∧ orientationlibc_stream_statew libc_stderrw ≠ WideOriented
intros m w Hfmt _ _
m :
w :
Hfmt :
contract_preerror_format_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False libc_stdout libc_stderr libc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native words m w
⊢
∃file : libc_file, libc_file_atw libc_stderrw = Somefile ∧ orientationlibc_stream_statew libc_stderrw ≠ WideOriented
destruct Hfmt as status & errnum & fmt & rest & format & body & info & Hwords & Hstatus & Herrnum & Hstring & Hformat & Hready & Hrest
m :
w :
status, errnum :
Z
fmt :
rest :
listword
format, body :
listZ
info :
Hstatus :
0 ≤ status < 2 ^ 32
Herrnum :
0 ≤ errnum < 2 ^ 32
Hstring :
c_stringm fmt format
Hformat :
narrow_formatm format rest body
Hready :
diagnostic_readylibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native m w
Hrest :
Forallwritable_spanm diagnostic_writeslibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native w ∧ stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False m w libc_stderrw info ∧ orientationstream_protocolinfo ≠ WideOriented ∧ libc_stdoutw ≠ libc_stderrw
⊢
∃file : libc_file, libc_file_atw libc_stderrw = Somefile ∧ orientationlibc_stream_statew libc_stderrw ≠ WideOriented
exact proj1Hready
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m w Hfmt _ _
destruct Hfmt as status & errnum & fmt & rest & format & body & info & Hwords & Hstatus & Herrnum & Hstring & Hformat & Hready & Hrest
exact proj1Hready
256Example closed_stderr_rejected: ∀m w, libc_file_atw libc_stderrw = None → ¬contract_prespec words m w
Explore proof 3 tactics
Initial goal
⊢
∀m : mem w : libc_world, libc_file_atw libc_stderrw = None → ¬contract_prespec words m w
intros m w Hclosed Hpre
⊢
False
destruct admission_stderrm w Hpre as file Hfile _
m :
w :
Hclosed :
libc_file_atw libc_stderrw = None
Hpre :
file :
Hfile :
libc_file_atw libc_stderrw = Somefile
⊢
False
congruence
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
262Example wide_stderr_rejected: ∀m w, orientationlibc_stream_statew libc_stderrw = WideOriented → ¬contract_prespec words m w
Explore proof 2 tactics
Initial goal
⊢
∀m : mem w : libc_world, orientationlibc_stream_statew libc_stderrw = WideOriented → ¬contract_prespec words m w
intros m w Hwide Hpre
m :
w :
Hwide :
Hpre :
⊢
False
exact proj2admission_stderrm w Hpre Hwide
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m w Hwide Hpre
exact proj2admission_stderrm w Hpre Hwide
store_bytesmemory 5120 4 16909060
mkLibcPayloadlibc_localefstconversion_world mkStdioWorldopened mkSpanlibc_errnofstconversion_world 4 libc_errnofstconversion_world mkLibcStreamsF.out_file F.err_file true mkStreamByteOriented text ++ 10 false libc_getoptfstconversion_world, mkShutdownHandlers 0 [ ] [ ] mkStreamByteOriented [ ] true
∀ opened
libc_stream_readyλ_ _ ⇒ True changed final_worldopened
Proof 40 steps Qed
intros opened
destruct readytrue as Hrep & Hlocale & He & _ & _ & Hu & Hstatus & Hphase & Hdistinct & Hroots & Ho & Herr & Hsep
assert Hfiles : libc_file_readychanged mkPtr5120 Obj5120 F.out_file ∧ libc_file_readychanged mkPtr5120 Obj5120 F.err_file
{split ; specialize Hoeq_refl ; clear Herr | specialize Herreq_refl ; clear Ho
all: destruct Ho as Hnon & Hn & Hreg & Haccess & Hbytes & Hrest || destruct Herr as Hnon & Hn & Hreg & Haccess & Hbytes & Hrest
all: split ; exact Hnon |
all: split ; | destruct Hrest as Hp & _ & _ & _ & Ha ; split ; exact Hp | ; split ; constructor | ; split ; constructor | ; split ; constructor | exact Ha
all: split ; exact Hn |
all: split ; exact Hreg |
all: split ; exact Haccess |
all: intros i Hi ; assert i = 0 as → by lia ; vm_compute ; split ; congruence
split ; exact I |
split
–destruct Hlocale as _ & _ & _ & _ & _ & Haligned
split ; exact I |
split ; constructor |
split
+intros category _
vm_compute
repeat split ; congruence
+split ; constructor |
split ; constructor | exact Haligned
–split ; exact He |
split
+change stream_wfmkStreamByteOriented [ ] true
split ; constructor | intros _ ; reflexivity
+split
∗change stream_wfmkStreamByteOriented text ++ 10 false
cbn [ stream_wf outstanding orientation text app ]
split ; repeat constructor ; lia | intros _ ; reflexivity
∗split ; exact Hu |
split ; exact Hstatus |
split ; exact Hphase |
split ; exact Hdistinct |
split ; destruct opened ; reflexivity |
split ; intros _ ; exact proj1Hfiles |
split ; intros _ ; exact proj2Hfiles |
intros p file Hfile base Hin
unfold libc_file_at in Hfile
destruct same_filep libc_stdoutfinal_worldopened ; destruct opened | destruct same_filep libc_stderrfinal_worldopened ; try discriminate ; injection Hfile as ← ; contradiction
∀ opened
error_format_prefixF.model libc_stdout libc_stderr libc_diagnostic_contextλ_ _ ⇒ True native words memory F.worldopened [ ] StreamBytes2 text ++ 10 changed final_worldopened
Proof 95 steps Qed
intros opened
exists 0, 0, mkPtr65744 Ro65744, WPtrmkPtr65680 Ro65680, 37; 115, text, mkStreamInfo2 stdout_initial 3, mkStreamInfo2 mkStreamByteOriented text ++ 10 false 3, text; 10, text; 10, Accepttext ++ 10
split ; reflexivity |
split
–pose proof hello_diagnostic_owned"closeout#str.55" memory heapopened or_introleq_refl heap_ownedopened heap_agreesopened as Hfmt
exact Hfmt
–split
+rewrite <- app_nil_rtext
apply format_string ; | constructor
pose proof hello_diagnostic_owned"closeout#str.53" memory heapopened or_introror_introleq_refl heap_ownedopened heap_agreesopened as Htext
exact Htext
+split ; reflexivity |
split
∗repeat constructor ; exists [ ] ; reflexivity |
constructor
∗split ; destruct opened ; reflexivity |
split
--split ; apply changed_ready |
split ; destruct opened ; reflexivity |
split ; reflexivity |
split
++split ; split ; repeat constructor ; lia | reflexivity | simpl ; lia
++change Forallwritable_spanchanged errno_span5120 0
constructor ; exact proj1proj2proj1proj2proj2changed_readyopened | constructor
--split ; reflexivity |
split ; reflexivity |
split
++eapply stream_next ; apply stream_accept ; discriminate | repeat constructor ; lia | constructor
++split ; reflexivity |
split
**destruct opened
---exists mkStreamInfo1 mkStreamByteOriented [ ] true 7
split ; reflexivity |
split ; reflexivity |
split ; reflexivity |
split ; reflexivity | apply F.close_settles
---split ; reflexivity
**split
---split
+++split ; exists F.err_file ; destruct opened ; reflexivity | discriminate
+++apply changed_ready
---split ; split ; exact I | repeat split ; reflexivity |
split
+++destruct opened
***split
----intros root E |
subst root
split
++++intros a Ha
left
exists errno_span5120 0
split ; left ; reflexivity |
split
*****exact proj1proj2proj1proj2proj2changed_readytrue
*****exact Ha
***split ; intros root |
split ; intros x ; contradiction
+++split
***split
----intros root E |
subst root
split
++++intros a Ha
left
exists errno_span5120 0
split ; left ; reflexivity |
split
*****exact proj1proj2proj1proj2proj2changed_readyopened
*****exact Ha
***split ; intros root |
split ; right ; reflexivity |
intros a _ _
reflexivity
∀ opened
H.M.E.invokespec CVoid call_args words InterpRuntime.start memory F.worldopened StreamBytes2 text ++ 10 CallReturn[ ] InterpRuntime.start changed final_worldopened
Explore proof 31 tactics
Initial goal
⊢
∀opened : bool, H.M.E.invokespec CVoid call_args words InterpRuntime.start memory F.worldopened StreamBytes2 text ++ 10 CallReturn[ ] InterpRuntime.start changed final_worldopened
intros opened
opened :
bool
⊢
H.M.E.invokespec CVoid call_args words InterpRuntime.start memory F.worldopened StreamBytes2 text ++ 10 CallReturn[ ] InterpRuntime.start changed final_worldopened
eapply H.M.E.invoke_normal with born := [ ]
7 openopened :
bool
focused goal
opened :
bool
⊢
contract_prespec words memory F.worldopened
focused goal
opened :
bool
⊢
H.M.E.prefixspec words InterpRuntime.start memory F.worldopened [ ] StreamBytes2 text ++ 10 InterpRuntime.start changed final_worldopened
focused goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
focused goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
focused goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
focused goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
–split ; reflexivity |
7 openopened :
bool
⊢
contract_abierror_format_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False libc_stdout libc_stderr libc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native CVoid call_args ∧ ∃status errnum format : value rest : listarg, call_args = ArgW status :: ArgW errnum :: ArgP format :: rest
deferred goal
opened :
bool
⊢
contract_prespec words memory F.worldopened
deferred goal
opened :
bool
⊢
H.M.E.prefixspec words InterpRuntime.start memory F.worldopened [ ] StreamBytes2 text ++ 10 InterpRuntime.start changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
split
8 openopened :
bool
⊢
contract_abierror_format_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False libc_stdout libc_stderr libc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native CVoid call_args
focused goal
deferred goal
opened :
bool
⊢
contract_prespec words memory F.worldopened
deferred goal
opened :
bool
⊢
H.M.E.prefixspec words InterpRuntime.start memory F.worldopened [ ] StreamBytes2 text ++ 10 InterpRuntime.start changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
+split ; reflexivity |
8 openopened :
bool
deferred goal
deferred goal
opened :
bool
⊢
contract_prespec words memory F.worldopened
deferred goal
opened :
bool
⊢
H.M.E.prefixspec words InterpRuntime.start memory F.worldopened [ ] StreamBytes2 text ++ 10 InterpRuntime.start changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
do 4 eexists
12 opendeferred goal
deferred goal
opened :
bool
⊢
contract_prespec words memory F.worldopened
deferred goal
opened :
bool
⊢
H.M.E.prefixspec words InterpRuntime.start memory F.worldopened [ ] StreamBytes2 text ++ 10 InterpRuntime.start changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
shelved goal
opened :
bool
shelved goal
opened :
bool
shelved goal
opened :
bool
shelved goal
opened :
bool
⊢
listarg
split ; reflexivity |
8 openopened :
bool
⊢
Forallpromoted_argument ArgP GlobalTAtom"closeout#str.53"
deferred goal
deferred goal
opened :
bool
⊢
contract_prespec words memory F.worldopened
deferred goal
opened :
bool
⊢
H.M.E.prefixspec words InterpRuntime.start memory F.worldopened [ ] StreamBytes2 text ++ 10 InterpRuntime.start changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
constructor ; eexists ; left ; reflexivity | constructor
7 opendeferred goal
deferred goal
opened :
bool
⊢
contract_prespec words memory F.worldopened
deferred goal
opened :
bool
⊢
H.M.E.prefixspec words InterpRuntime.start memory F.worldopened [ ] StreamBytes2 text ++ 10 InterpRuntime.start changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
+do 4 eexists
11 opendeferred goal
opened :
bool
⊢
contract_prespec words memory F.worldopened
deferred goal
opened :
bool
⊢
H.M.E.prefixspec words InterpRuntime.start memory F.worldopened [ ] StreamBytes2 text ++ 10 InterpRuntime.start changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
shelved goal
opened :
bool
shelved goal
opened :
bool
shelved goal
opened :
bool
shelved goal
opened :
bool
⊢
listarg
reflexivity
6 opendeferred goal
opened :
bool
⊢
contract_prespec words memory F.worldopened
deferred goal
opened :
bool
⊢
H.M.E.prefixspec words InterpRuntime.start memory F.worldopened [ ] StreamBytes2 text ++ 10 InterpRuntime.start changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
–apply admitted
5 opendeferred goal
opened :
bool
⊢
H.M.E.prefixspec words InterpRuntime.start memory F.worldopened [ ] StreamBytes2 text ++ 10 InterpRuntime.start changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
–split
6 openopened :
bool
⊢
H.M.E.effectscontract_sourcesspec words memory F.worldopened contract_writesspec words memory F.worldopened contract_releasesspec words memory F.worldopened contract_requestsspec words memory F.worldopened InterpRuntime.start memory [ ] InterpRuntime.start changed [ ]
focused goal
opened :
bool
⊢
contract_prefixspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
+eapply H.M.E.effects_local ; apply local_store_bytes | constructor
6 openopened :
bool
⊢
∀b : Z, 5120 ≤ b < 5120 + 4 → write_authoritycontract_writesspec words memory F.worldopened [ ] memory b
deferred goal
opened :
bool
⊢
contract_prefixspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
intros a Ha
6 openopened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
⊢
write_authoritycontract_writesspec words memory F.worldopened [ ] memory a
deferred goal
opened :
bool
⊢
contract_prefixspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
left
6 openopened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
⊢
∃s : span, Ins contract_writesspec words memory F.worldopened ∧ writable_spanmemory s ∧ span_containss a
deferred goal
opened :
bool
⊢
contract_prefixspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
exists errno_span5120 0
6 openopened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
⊢
Inerrno_span5120 0 contract_writesspec words memory F.worldopened ∧ writable_spanmemory errno_span5120 0 ∧ span_containserrno_span5120 0 a
deferred goal
opened :
bool
⊢
contract_prefixspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
split ; apply in_or_app ; right ; apply in_or_app ; left ; destruct opened ; left ; reflexivity |
6 openopened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
⊢
writable_spanmemory errno_span5120 0 ∧ span_containserrno_span5120 0 a
deferred goal
opened :
bool
⊢
contract_prefixspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
split
7 openopened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
⊢
focused goal
opened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
⊢
span_containserrno_span5120 0 a
deferred goal
opened :
bool
⊢
contract_prefixspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
∗exact proj1proj2proj1proj2proj2readyopened
6 opendeferred goal
opened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
⊢
span_containserrno_span5120 0 a
deferred goal
opened :
bool
⊢
contract_prefixspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
∗unfold span_contains , errno_span
6 openopened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
deferred goal
opened :
bool
⊢
contract_prefixspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
simpl
6 openopened :
bool
a :
Z
Ha :
5120 ≤ a < 5120 + 4
⊢
5120 + 0 ≤ a < 5120 + 0 + 4
deferred goal
opened :
bool
⊢
contract_prefixspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
lia
5 opendeferred goal
opened :
bool
⊢
contract_prefixspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 changed final_worldopened
deferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
+split ; apply format_prefix | constructor ; reflexivity | constructor
4 opendeferred goal
opened :
bool
⊢
contract_postspec words memory F.worldopened [ ] StreamBytes2 text ++ 10 CallReturn[ ] changed final_worldopened
deferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
–split ; split ; apply format_prefix | reflexivity | reflexivity
3 opendeferred goal
opened :
bool
⊢
∀why : reason, CallReturn[ ] ≠ CallResourcewhy
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
–intros why Hbad
3 open⊢
False
deferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
discriminate Hbad
2 opendeferred goal
opened :
bool
⊢
∀values : listword, CallReturn[ ] = CallReturnvalues → return_shapecontract_returnsspec values ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed values
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
–intros vs Hvs
2 open⊢
return_shapecontract_returnsspec vs ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed vs
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
injection Hvs as ←
2 openopened :
bool
⊢
return_shapecontract_returnsspec [ ] ∧ Forallword_authoritycontract_sourcesspec words memory F.worldopened [ ] changed [ ]
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
split ; reflexivity | constructor
deferred goal
opened :
bool
⊢
∀status : Z, CallReturn[ ] = CallExitstatus → ∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
–intros status Hbad
⊢
∃before : listevent, StreamBytes2 text ++ 10 = before ++ ProcessExitstatus
discriminate Hbad
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros opened
eapply H.M.E.invoke_normal with born := [ ]
–split ; reflexivity |
split
+split ; reflexivity |
do 4 eexists
split ; reflexivity |
constructor ; eexists ; left ; reflexivity | constructor
+do 4 eexists
reflexivity
–apply admitted
–split
+eapply H.M.E.effects_local ; apply local_store_bytes | constructor
intros a Ha
left
exists errno_span5120 0
split ; apply in_or_app ; right ; apply in_or_app ; left ; destruct opened ; left ; reflexivity |
split
∗exact proj1proj2proj1proj2proj2readyopened
+split ; apply format_prefix | constructor ; reflexivity | constructor
–split ; split ; apply format_prefix | reflexivity | reflexivity
–intros why Hbad
discriminate Hbad
–intros vs Hvs
injection Hvs as ←
split ; reflexivity | constructor
–intros status Hbad
discriminate Hbad
Explore proof 3 tactics
Initial goal
⊢
NoDuphello_diagnostic_pieces ++ byte_ps5120 0 0; 0; 0; 0.*1
vm_compute
repeat apply NoDup_cons ; simpl ; intros Hbad ; repeat destruct Hbad as Hbad | Hbad ; try contradiction ; discriminate |
⊢
NoDup[ ]
apply NoDup_nil
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
vm_compute
repeat apply NoDup_cons ; simpl ; intros Hbad ; repeat destruct Hbad as Hbad | Hbad ; try contradiction ; discriminate |
apply NoDup_nil
414Example entry_usable: ∀opened, agreesmemory heapopened ∧ live_disjointmemory ∧ InterpRuntime.readyInterpRuntime.start memory ∧ wimemory F.worldopened heapopened ∧ ∀l v, l, v ∈ hello_diagnostic_pieces ++ byte_ps5120 0 0; 0; 0; 0 → heapopened !! l = Somev
Explore proof 7 tactics
Initial goal
⊢
∀opened : bool, agreesmemory heapopened ∧ live_disjointmemory ∧ InterpRuntime.readyInterpRuntime.start memory ∧ wimemory F.worldopened heapopened ∧ ∀l : piece v : pval, l, v ∈ hello_diagnostic_pieces ++ byte_ps5120 0 0; 0; 0; 0 → heapopened !! l = Somev
intros
opened :
bool
⊢
agreesmemory heapopened ∧ live_disjointmemory ∧ InterpRuntime.readyInterpRuntime.start memory ∧ wimemory F.worldopened heapopened ∧ ∀l : piece v : pval, l, v ∈ hello_diagnostic_pieces ++ byte_ps5120 0 0; 0; 0; 0 → heapopened !! l = Somev
split ; apply heap_agrees |
opened :
bool
⊢
live_disjointmemory ∧ InterpRuntime.readyInterpRuntime.start memory ∧ wimemory F.worldopened heapopened ∧ ∀l : piece v : pval, l, v ∈ hello_diagnostic_pieces ++ byte_ps5120 0 0; 0; 0; 0 → heapopened !! l = Somev
split ; apply disjoint |
opened :
bool
⊢
InterpRuntime.readyInterpRuntime.start memory ∧ wimemory F.worldopened heapopened ∧ ∀l : piece v : pval, l, v ∈ hello_diagnostic_pieces ++ byte_ps5120 0 0; 0; 0; 0 → heapopened !! l = Somev
split ; apply runtime_ready |
split ; apply entry_wi |
opened :
bool
⊢
∀l : piece v : pval, l, v ∈ hello_diagnostic_pieces ++ byte_ps5120 0 0; 0; 0; 0 → heapopened !! l = Somev
intros l v Hin
⊢
heapopened !! l = Somev
apply elem_of_app in Hin as Hin | Hin ; apply heap_owned | apply heap_errno ; exact Hin
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros
split ; apply heap_agrees |
split ; apply disjoint |
split ; apply runtime_ready |
split ; apply entry_wi |
intros l v Hin
apply elem_of_app in Hin as Hin | Hin ; apply heap_owned | apply heap_errno ; exact Hin
425Example framed_return: ∀opened, ∃ys, lengthys = 4%nat ∧ agreeschanged overwritehello_diagnostic_pieces ++ byte_ps5120 0 ys heapopened ∧ overwritehello_diagnostic_pieces ++ byte_ps5120 0 ys heapopened !! PByte5120 3 = SomeVByte1 ∧ ∀l v, l, v ∈ hello_diagnostic_pieces → overwritehello_diagnostic_pieces ++ byte_ps5120 0 ys heapopened !! l = Somev
Proof 31 steps Qed
intros opened
destruct entry_usableopened as Ha & Hd & Hr & Hw & Howned
destruct H.D.error_pieces_frameλ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False native T.out T.err 5120 0 hello_diagnostic_pieces CVoid call_args words InterpRuntime.start memory F.worldopened StreamBytes2 text ++ 10 [ ] InterpRuntime.start changed final_worldopened heapopened 0; 0; 0; 0 returning_callopened Ha Hd Hr proj1Hw eq_refl Howned hello_diagnostic_errno_keys5120 0 ltac:lia ltac:lia as ys & _ & Hlen & Hkeys & Hag & _ & _ & Hwi
assert Hdup : base.NoDuphello_diagnostic_pieces ++ byte_ps5120 0 ys.*1
{rewrite Hkeys
apply NoDup_ListNoDup , combined_keys
exists ys
split ; exact Hlen |
split ; exact Hag |
split
–destruct ys as | a | b | c | d rest ; try discriminate Hlen
assert Hl : overwritehello_diagnostic_pieces ++ byte_ps5120 0 a; b; c; d heapopened !! PByte5120 3 = SomeVByted
{apply overwrite_owned ; exact Hdup |
apply elem_of_app
right
change PByte5120 3, VByted ∈ PByte5120 0, VBytea; PByte5120 1, VByteb; PByte5120 2, VBytec; PByte5120 3, VByted
do 3 apply elem_of_cons ; right
apply elem_of_cons
left
reflexivity
destruct Hag_ _ Hl as _ Hbyte
change 1 = d in Hvalue
rewrite Hvalue
exact Hl
Explore proof 10 tactics
Initial goal
⊢
¬∀l : piece v : pval, l, v ∈ PByte5120 3, VByte0 → l ∉ errno_keys5120 0
intros H
H :
∀l : piece v : pval, l, v ∈ PByte5120 3, VByte0 → l ∉ errno_keys5120 0
⊢
False
apply HPByte5120 3 VByte0
2 openH :
∀l : piece v : pval, l, v ∈ PByte5120 3, VByte0 → l ∉ errno_keys5120 0
focused goal
H :
∀l : piece v : pval, l, v ∈ PByte5120 3, VByte0 → l ∉ errno_keys5120 0
⊢
PByte5120 3 ∈ errno_keys5120 0
–apply elem_of_cons
2 openH :
∀l : piece v : pval, l, v ∈ PByte5120 3, VByte0 → l ∉ errno_keys5120 0
deferred goal
H :
∀l : piece v : pval, l, v ∈ PByte5120 3, VByte0 → l ∉ errno_keys5120 0
⊢
PByte5120 3 ∈ errno_keys5120 0
left
2 openH :
∀l : piece v : pval, l, v ∈ PByte5120 3, VByte0 → l ∉ errno_keys5120 0
deferred goal
H :
∀l : piece v : pval, l, v ∈ PByte5120 3, VByte0 → l ∉ errno_keys5120 0
⊢
PByte5120 3 ∈ errno_keys5120 0
reflexivity
deferred goal
H :
∀l : piece v : pval, l, v ∈ PByte5120 3, VByte0 → l ∉ errno_keys5120 0
⊢
PByte5120 3 ∈ errno_keys5120 0
–change PByte5120 3 ∈ PByte5120 0; PByte5120 1; PByte5120 2; PByte5120 3
do 3 apply elem_of_cons ; right
apply elem_of_cons
left
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Explore proof 3 tactics
Initial goal
constructor
⊢
∀s : InterpRuntime.state m : mem s′ : InterpRuntime.state m′ : mem w : libc_world h : gmappiece pval, InterpRuntime.safepoints m s′ m′ → wim w h → wim′ w h
intros s m s′ m′ w h → → Hw
⊢
wim w h
exact Hw
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
constructor
intros s m s′ m′ w h → → Hw
exact Hw
λ_ ⇒ Somespec
∀ args words s m w tr vs s′ m′ w′ h ys
H.M.E.invokespec CVoid args words s m w tr CallReturnvs s′ m′ w′
wim w h
lengthys = 4%nat
libc_diagnostic_wiλ_ _ ⇒ True native T.out T.err 5120 0 m′ w′ overwritehello_diagnostic_pieces ++ byte_ps5120 0 ys h
wim′ w′ overwritehello_diagnostic_pieces ++ byte_ps5120 0 ys h
Explore proof 6 tactics
Initial goal
⊢
∀args : listarg words0 : listword s : InterpRuntime.state m : mem w : libc_world tr : listevent vs : listword s′ : InterpRuntime.state m′ : mem w′ : libc_world h : gmappiece pval ys : listZ, H.M.E.invokespec CVoid args words0 s m w tr CallReturnvs s′ m′ w′ → wim w h → Datatypes.lengthys = 4%nat → libc_diagnostic_wiλ_ : mem _ : libc_world ⇒ True native T.out T.err 5120 0 m′ w′ overwritehello_diagnostic_pieces ++ byte_ps5120 0 ys h → wim′ w′ overwritehello_diagnostic_pieces ++ byte_ps5120 0 ys h
intros args ws s m w tr vs s′ m′ w′ h ys Hi _ _ Hw
args :
listarg
ws :
listword
m :
w :
tr :
listevent
vs :
listword
m′ :
w′ :
ys :
listZ
Hi :
H.M.E.invokespec CVoid args ws s m w tr CallReturnvs s′ m′ w′
Hw :
libc_diagnostic_wiλ_ : mem _ : libc_world ⇒ True native T.out T.err 5120 0 m′ w′ overwritehello_diagnostic_pieces ++ byte_ps5120 0 ys h
⊢
wim′ w′ overwritehello_diagnostic_pieces ++ byte_ps5120 0 ys h
split ; exact Hw |
args :
listarg
ws :
listword
m :
w :
tr :
listevent
vs :
listword
m′ :
w′ :
ys :
listZ
Hi :
H.M.E.invokespec CVoid args ws s m w tr CallReturnvs s′ m′ w′
Hw :
libc_diagnostic_wiλ_ : mem _ : libc_world ⇒ True native T.out T.err 5120 0 m′ w′ overwritehello_diagnostic_pieces ++ byte_ps5120 0 ys h
⊢
diagnostic_readynative m′ w′
destruct H.D.error_returned_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hi as _ born Hp
args :
listarg
ws :
listword
m :
w :
tr :
listevent
vs :
listword
m′ :
w′ :
ys :
listZ
Hi :
H.M.E.invokespec CVoid args ws s m w tr CallReturnvs s′ m′ w′
Hw :
libc_diagnostic_wiλ_ : mem _ : libc_world ⇒ True native T.out T.err 5120 0 m′ w′ overwritehello_diagnostic_pieces ++ byte_ps5120 0 ys h
born :
listZ
Hp :
H.D.M.E.prefixlibc_error_contractλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False native ws s m w born tr s′ m′ w′
⊢
diagnostic_readynative m′ w′
destruct proj2Hp as Hfmt _
args :
listarg
ws :
listword
m :
w :
tr :
listevent
vs :
listword
m′ :
w′ :
ys :
listZ
Hi :
H.M.E.invokespec CVoid args ws s m w tr CallReturnvs s′ m′ w′
Hw :
libc_diagnostic_wiλ_ : mem _ : libc_world ⇒ True native T.out T.err 5120 0 m′ w′ overwritehello_diagnostic_pieces ++ byte_ps5120 0 ys h
born :
listZ
Hp :
H.D.M.E.prefixlibc_error_contractλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False native ws s m w born tr s′ m′ w′
Hfmt :
contract_prefixerror_format_contractlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False libc_stdout libc_stderr libc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native ws m w born tr m′ w′
⊢
diagnostic_readynative m′ w′
destruct Hfmt as status & errnum & fmt & rest & text & body & info & info′ & segments & pieces & actions & Hxs & Hstring & Hformat & Hsegments & Hpieces & Hinfo & Hopen & Hid & Hid′ & Hrun & Haccepted & Hflush & Hready & Hrest
args :
listarg
ws :
listword
m :
w :
tr :
listevent
vs :
listword
m′ :
w′ :
ys :
listZ
Hi :
H.M.E.invokespec CVoid args ws s m w tr CallReturnvs s′ m′ w′
Hw :
libc_diagnostic_wiλ_ : mem _ : libc_world ⇒ True native T.out T.err 5120 0 m′ w′ overwritehello_diagnostic_pieces ++ byte_ps5120 0 ys h
born :
listZ
Hp :
H.D.M.E.prefixlibc_error_contractλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False native ws s m w born tr s′ m′ w′
status, errnum :
Z
fmt :
rest :
listword
text, body :
listZ
info, info′ :
segments, pieces :
listlistZ
actions :
liststream_action
Hstring :
c_stringm fmt text
Hformat :
narrow_formatm text rest body
Hsegments :
diagnostic_segmentslibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native m w errnum body segments
Hpieces :
Forall2λwhole part : listZ ⇒ ∃tail : listZ, whole = part ++ tail segments pieces
Hinfo :
stream_atlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False w libc_stderrw = Someinfo
Hopen :
stream_openlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False m′ w′ libc_stderrw info′
Hid :
stream_identifierinfo = 2
Hid′ :
stream_identifierinfo′ = 2
Hrun :
stream_runstream_protocolinfo actions stream_protocolinfo′
Haccepted :
acceptedactions = concatpieces
Hflush :
diagnostic_flushlibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False libc_stdout w w′
Hready :
diagnostic_readylibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native m′ w′
Hrest :
diagnostic_framelibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native w w′ ∧ stream_delegateslibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False w libc_stdoutw born m′ w′ ∧ stream_delegateslibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False w libc_stderrw born m′ w′ ∧ ∀root : span, Inroot diagnostic_writeslibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native w′ → available_capdiagnostic_sourceslibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native m w born m′ ptr_capspan_ptrroot ∧ ∀a : Z, span_containsroot a → write_authoritydiagnostic_writeslibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native w born m′ a ∧ tr = [ ] ∧ acceptedactions = [ ] ∨ tr = StreamBytes2 acceptedactions ∧ ∀a : Z, in_objectm a → ¬write_authoritystream_aux_rootslibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False w libc_stdoutw ++ stream_aux_rootslibc_stream_modelλ_ : mem _ : libc_world ⇒ True λ_ : libc_world _ : ptr _ _ : Z ⇒ False λ_ : libc_world _ : ptr _ _ : stream_state _ : bool ⇒ False w libc_stderrw ++ diagnostic_writeslibc_diagnostic_contextλ_ : mem _ : libc_world ⇒ True native w [ ] m a → m_auxm′ a = m_auxm a
⊢
diagnostic_readynative m′ w′
exact proj1Hready
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros args ws s m w tr vs s′ m′ w′ h ys Hi _ _ Hw
split ; exact Hw |
destruct H.D.error_returned_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hi as _ born Hp
destruct proj2Hp as Hfmt _
destruct Hfmt as status & errnum & fmt & rest & text & body & info & info′ & segments & pieces & actions & Hxs & Hstring & Hformat & Hsegments & Hpieces & Hinfo & Hopen & Hid & Hid′ & Hrun & Haccepted & Hflush & Hready & Hrest
exact proj1Hready
496Example diagnostic_then_return: ptshello_diagnostic_pieces −∗ ptsbyte_ps5120 0 0; 0; 0; 0 −∗ WPERunmkFramestub entry_env [ ] None ExecTAtom"body" CallCVoid GlobalTAtom"error" ArgW Const0; ArgW TmpTAtom"errnum"; ArgP GlobalTAtom"closeout#str.55"; ArgP GlobalTAtom"closeout#str.53" JRetConst0 : language.exprnanofil_langregistry ge {result. ∃ys, ⌜result = RetWInt0 ∧ lengthys = 4%nat⌝ ∗ ptshello_diagnostic_pieces ∗ ptsbyte_ps5120 0 ys}
Proof 29 steps Qed
iIntros Hps He
iApply H.wp_hello_errorregistry wi ge λ_ _ ⇒ True λ_ _ _ _ ⇒ False λ_ _ _ _ _ ⇒ False native T.out T.err 5120 0 stub entry_env [ ] TAtom"body" TmpTAtom"errnum" GlobalTAtom"closeout#str.55" GlobalTAtom"closeout#str.53" [ ] JRetConst0 0 0; 0; 0; 0 _ with Hps He []
–intros m w h Hwi Hnative
split ; exact Hwi |
split ; exact Hnative |
split ; constructor | exact Hnative
–exact compatible
–lia
–lia
–reflexivity
–reflexivity
–vm_compute
reflexivity
–vm_compute
reflexivity
–lia
–reflexivity