rocq/theories/HelloProgName.v
set_program_name preserves strings, not just capabilities. This strengthens HelloName's control-flow proofs while reusing its IR definitions, literals, cells and store proof.
From iris.proofmode Require Import proofmode
From iris.base_logic.lib Require Import gen_heap
From iris.program_logic Require Import language weakestpre
From Stdlib Require Import ZArith Lia
From Nanofil Require Import Term Syntax Values Memory Runtime Ops Semantics Run StepRules Symbolic ExternalCalls ExternalMachine Pieces Heap ContractFrame Language Logic StringLogic MemLogic HelloModule HelloLeaf HelloName
Open Scope Z_scope
Open Scope list_scope
Arguments Z.add : simpl nomatch
Arguments Z.sub : simpl nomatch
Arguments Z.mul : simpl nomatch
Keep symbolic address arithmetic folded during computation.
Promotion candidate: a zero bounded comparison implies equal bounded lengths, since an earlier NUL would differ from a nonzero byte.
∀ m p q n left right
left = right
Explore proof 23 tactics
Initial goal
⊢
bounded_lengthm p n left → bounded_lengthm q n right → strncmp_resultm p q n 0 → left = right
intros Hl Hr l & r & Hpl & Hqr & _ & ordering & Horder & Hsign
m :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
l, r :
Z
Hpl :
bounded_lengthm p n l
Hqr :
bounded_lengthm q n r
ordering :
Horder :
memcmp_orderm p q strncmp_windown l r ordering
Hsign : (sign_extension (2 ^ 32) (2 ^ 31) 0 ?= 0) = ordering⊢
left = right
pose proof bounded_length_unique_ _ _ _ _ Hl Hpl as ←
m :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
r :
Z
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n r
ordering :
Horder :
memcmp_orderm p q strncmp_windown left r ordering
Hsign : (sign_extension (2 ^ 32) (2 ^ 31) 0 ?= 0) = ordering⊢
left = right
pose proof bounded_length_unique_ _ _ _ _ Hr Hqr as ←
m :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
ordering :
Horder :
memcmp_orderm p q strncmp_windown left right ordering
Hsign : (sign_extension (2 ^ 32) (2 ^ 31) 0 ?= 0) = ordering⊢
left = right
change Datatypes.Eq = ordering in Hsign
m :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
ordering :
Horder :
memcmp_orderm p q strncmp_windown left right ordering
Hsign :
Datatypes.Eq = ordering
⊢
left = right
subst ordering
m :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
⊢
left = right
assert Hsame : ∀i, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
2 openm :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
⊢
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
focused goal
m :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hsame :
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
⊢
left = right
{destruct Horder as _ & Hsame | k & Hk & Hb & Hne & Heq ; exact Hsame |
2 openm :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
k :
Z
Hk :
0 ≤ k < strncmp_windown left right
Heq :
Datatypes.Eq = (m_bytes m (ptr_addr p + k) ?= m_bytes m (ptr_addr q + k))⊢
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
deferred goal
m :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hsame :
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
⊢
left = right
exfalso
2 openm :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
k :
Z
Hk :
0 ≤ k < strncmp_windown left right
Heq :
Datatypes.Eq = (m_bytes m (ptr_addr p + k) ?= m_bytes m (ptr_addr q + k))⊢
False
deferred goal
m :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hsame :
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
⊢
left = right
apply Hne
2 openm :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
k :
Z
Hk :
0 ≤ k < strncmp_windown left right
Heq :
Datatypes.Eq = (m_bytes m (ptr_addr p + k) ?= m_bytes m (ptr_addr q + k))deferred goal
m :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hsame :
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
⊢
left = right
apply Z.compare_eq
2 openm :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
k :
Z
Hk :
0 ≤ k < strncmp_windown left right
Heq :
Datatypes.Eq = (m_bytes m (ptr_addr p + k) ?= m_bytes m (ptr_addr q + k))⊢
(m_bytes m (ptr_addr p + k) ?= m_bytes m (ptr_addr q + k)) = Datatypes.Eqdeferred goal
m :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hsame :
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
⊢
left = right
symmetry
2 openm :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
k :
Z
Hk :
0 ≤ k < strncmp_windown left right
Heq :
Datatypes.Eq = (m_bytes m (ptr_addr p + k) ?= m_bytes m (ptr_addr q + k))⊢
Datatypes.Eq = (m_bytes m (ptr_addr p + k) ?= m_bytes m (ptr_addr q + k))deferred goal
m :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hsame :
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
⊢
left = right
exact Heq
deferred goal
m :
p, q :
n, left, right :
Z
Hl :
bounded_lengthm p n left
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hsame :
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
⊢
left = right
destruct Hl as Hn & Hl & Hlp & Hap & Hbp & Hnp
m :
p, q :
n, left, right :
Z
Hn :
0 ≤ n < 2 ^ 64
Hl :
0 ≤ left ≤ n
Hlp :
Hap :
Hr :
bounded_lengthm q n right
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hsame :
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
⊢
left = right
destruct Hr as _ & Hr & Hlq & Haq & Hbq & Hnq
m :
p, q :
n, left, right :
Z
Hn :
0 ≤ n < 2 ^ 64
Hl :
0 ≤ left ≤ n
Hlp :
Hap :
Hr :
0 ≤ right ≤ n
Hlq :
Haq :
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hsame :
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
⊢
left = right
destruct Z.lt_trichotomyleft right as Hlt | Heq | Hgt ; | exact Heq |
2 openm :
p, q :
n, left, right :
Z
Hn :
0 ≤ n < 2 ^ 64
Hl :
0 ≤ left ≤ n
Hlp :
Hap :
Hr :
0 ≤ right ≤ n
Hlq :
Haq :
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hsame :
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
Hlt :
left < right
⊢
left = right
focused goal
m :
p, q :
n, left, right :
Z
Hn :
0 ≤ n < 2 ^ 64
Hl :
0 ≤ left ≤ n
Hlp :
Hap :
Hr :
0 ≤ right ≤ n
Hlq :
Haq :
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hsame :
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
Hgt :
right < left
⊢
left = right
–specialize Hsameleft ltac:unfold strncmp_window ; lia
2 openm :
p, q :
n, left, right :
Z
Hn :
0 ≤ n < 2 ^ 64
Hl :
0 ≤ left ≤ n
Hlp :
Hap :
Hr :
0 ≤ right ≤ n
Hlq :
Haq :
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hlt :
left < right
⊢
left = right
deferred goal
m :
p, q :
n, left, right :
Z
Hn :
0 ≤ n < 2 ^ 64
Hl :
0 ≤ left ≤ n
Hlp :
Hap :
Hr :
0 ≤ right ≤ n
Hlq :
Haq :
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hsame :
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
Hgt :
right < left
⊢
left = right
rewrite Hnpltac:lia in Hsame
2 openm :
p, q :
n, left, right :
Z
Hn :
0 ≤ n < 2 ^ 64
Hl :
0 ≤ left ≤ n
Hlp :
Hap :
Hr :
0 ≤ right ≤ n
Hlq :
Haq :
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hlt :
left < right
⊢
left = right
deferred goal
m :
p, q :
n, left, right :
Z
Hn :
0 ≤ n < 2 ^ 64
Hl :
0 ≤ left ≤ n
Hlp :
Hap :
Hr :
0 ≤ right ≤ n
Hlq :
Haq :
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hsame :
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
Hgt :
right < left
⊢
left = right
specialize Hbqleft ltac:lia
2 openm :
p, q :
n, left, right :
Z
Hn :
0 ≤ n < 2 ^ 64
Hl :
0 ≤ left ≤ n
Hlp :
Hap :
Hr :
0 ≤ right ≤ n
Hlq :
Haq :
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hlt :
left < right
⊢
left = right
deferred goal
m :
p, q :
n, left, right :
Z
Hn :
0 ≤ n < 2 ^ 64
Hl :
0 ≤ left ≤ n
Hlp :
Hap :
Hr :
0 ≤ right ≤ n
Hlq :
Haq :
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hsame :
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
Hgt :
right < left
⊢
left = right
lia
deferred goal
m :
p, q :
n, left, right :
Z
Hn :
0 ≤ n < 2 ^ 64
Hl :
0 ≤ left ≤ n
Hlp :
Hap :
Hr :
0 ≤ right ≤ n
Hlq :
Haq :
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hsame :
∀i : Z, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
Hgt :
right < left
⊢
left = right
–specialize Hsameright ltac:unfold strncmp_window ; lia
m :
p, q :
n, left, right :
Z
Hn :
0 ≤ n < 2 ^ 64
Hl :
0 ≤ left ≤ n
Hlp :
Hap :
Hr :
0 ≤ right ≤ n
Hlq :
Haq :
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hgt :
right < left
⊢
left = right
rewrite Hnqltac:lia in Hsame
m :
p, q :
n, left, right :
Z
Hn :
0 ≤ n < 2 ^ 64
Hl :
0 ≤ left ≤ n
Hlp :
Hap :
Hr :
0 ≤ right ≤ n
Hlq :
Haq :
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hgt :
right < left
⊢
left = right
specialize Hbpright ltac:lia
m :
p, q :
n, left, right :
Z
Hn :
0 ≤ n < 2 ^ 64
Hl :
0 ≤ left ≤ n
Hlp :
Hap :
Hr :
0 ≤ right ≤ n
Hlq :
Haq :
Hpl :
bounded_lengthm p n left
Hqr :
bounded_lengthm q n right
Horder :
memcmp_orderm p q strncmp_windown left right Datatypes.Eq
Hgt :
right < left
⊢
left = right
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hl Hr l & r & Hpl & Hqr & _ & ordering & Horder & Hsign
pose proof bounded_length_unique_ _ _ _ _ Hl Hpl as ←
pose proof bounded_length_unique_ _ _ _ _ Hr Hqr as ←
change Datatypes.Eq = ordering in Hsign
subst ordering
assert Hsame : ∀i, 0 ≤ i < strncmp_windown left right → m_bytesm ptr_addrp + i = m_bytesm ptr_addrq + i
{destruct Horder as _ & Hsame | k & Hk & Hb & Hne & Heq ; exact Hsame |
exfalso
apply Hne
apply Z.compare_eq
symmetry
exact Heq
destruct Hl as Hn & Hl & Hlp & Hap & Hbp & Hnp
destruct Hr as _ & Hr & Hlq & Haq & Hbq & Hnq
destruct Z.lt_trichotomyleft right as Hlt | Heq | Hgt ; | exact Heq |
–specialize Hsameleft ltac:unfold strncmp_window ; lia
rewrite Hnpltac:lia in Hsame
specialize Hbqleft ltac:lia
lia
–specialize Hsameright ltac:unfold strncmp_window ; lia
rewrite Hnqltac:lia in Hsame
specialize Hbpright ltac:lia
lia
String-valued program-name reasoning over any runtime.
Import the existing module paths rather than copying their nested signatures into another chain of aliases.
Import HN.L HN.LG HN.SL HN.ML HN.HL HN
The linked module and the three external contracts already used by HelloName.
Exactly HelloName's global-cell layout and world-preserving store premises.
The same Iris interpretation as HelloName.
Expressions in the linked language.
Promotion candidate: expose the length consequence of strncmp's result instead of discarding all information about the returned integer.
∀ f e ls lab d v w u rest j p b reg xs q b′ reg′ ys n Φ
registryTAtom"strncmp" = Somestrncmp_contractworld
lookupTAtom"strncmp" ge_globalsge = None
0 ≤ n < 2 ^ 64
stringp b reg xs −∗ stringq b′ reg′ ys −∗ ▷∀bits, ⌜bits mod 2 ^ 32 = 0 → Z.minZ.of_natlengthxs n = Z.minZ.of_natlengthys n⌝ −∗ stringp b reg xs −∗ stringq b′ reg′ ys −∗ WPERunmkFramef putd WIntbits e ls None Execlab rest j : nexpr {Φ} −∗ WPERunmkFramef e ls None Execlab CallCResultd W GlobalTAtom"strncmp" ArgP v; ArgP w; ArgL u :: rest j : nexpr {Φ}
Proof 34 steps Qed
intros Hreg Hfn Hdata Hv Hw Hu Hn
iIntros Hs Ht HK
iApply wp_external_ _ _ _ _ _ _ _ _ _ _ _ strncmp_contractworld WPtrp; WPtrq; WIntn stringp b reg xs ∗ stringq b' reg' ys with [$Hs $Ht] [HK] ; done | done | done | done | cbn [ map_option ] ; rewrite Hv Hw Hu ; done | | |
–split ; right ; eexists ; reflexivity | do 3 eexists ; reflexivity
–iIntros σ Hσ [[%Hok Hs] [%Hok′ Ht]]
iDestruct pts_facts with Hσ Hs as %Ha & _
iDestruct pts_facts with Hσ Ht as %Ha′ & _
iPureIntro
do 5 eexists
split ; reflexivity |
split ; exact string_bounded_ _ _ _ _ _ Hok Ha Hn | exact string_bounded_ _ _ _ _ _ Hok' Ha' Hn
–iNext
iIntros σ trace values s′ m′ w′ Hinv Hσ [[%Hok Hs] [%Hok′ Ht]]
iDestruct pts_facts with Hσ Hs as %Ha & _
iDestruct pts_facts with Hσ Ht as %Ha′ & _
destruct M.E.strncmp_invocation_ _ _ _ _ _ _ _ _ _ _ _ Hinv as _ & → & → & p′ & q′ & n′ & bits & Hx & Hresult & He
injection Hx as ← ← ←
injection He as →
assert Hlength : bits = 0 → Z.minZ.of_natlengthxs n = Z.minZ.of_natlengthys n
{intros →
eapply strncmp_zero_lengths ; | | exact Hresult ; eapply string_bounded ; eauto
destruct Hresult as left & right & _ & _ & Hbits & _
iDestruct pure_return with Hσ as Hσ ; exact Hinv |
destruct σ as m s fuel w0
iModIntro
iExists _
iSplit ; iPureIntro ; reflexivity |
iFrame Hσ
rewrite Z.mod_smallbits 2 ^ 32 Hbits
iApply HK with [%] [Hs] [Ht]
+rewrite Z.mod_smallbits 2 ^ 32 Hbits
exact Hlength
+by iSplit
+by iSplit
The cells and the existing store proof specialized to this layout.
The lt-prefix test only advances by three when those bytes exist. Both the full invocation name and the short name remain suffixes.
∀ e p b reg ys j r3 r4 x0 x1 y0 Φ
stringp b reg ys −∗ literalsr3 r4 −∗ cellsx0 x1 y0 −∗ ▷∀i k, ⌜i ≤ lengthys%nat ∧ k ≤ lengthys%nat⌝ −∗ stringp b reg ys −∗ literalsr3 r4 −∗ cellsmkPtrptr_addrp + Z.of_nati ptr_capp mkPtrptr_addrp + Z.of_nati ptr_capp mkPtrptr_addrp + Z.of_natk ptr_capp −∗ ΦRetVoid −∗ WPERunmkFrameset_program_name_fn e [ ] None ExecTAtom"L16" b_instss_L16 b_jumps_L16 : nexpr {Φ}
Proof 50 steps Qed
intros Hv15 Hj
destruct name_lookupsge Hlinked as _ & _ & Hlt
iIntros Hs [Hlibs Hlt] Hc HΦ
iDestruct Hs as [%Hok Hps]
iAssert stringp b reg ys with [$Hps] as Hs ; done |
pose proof Hok as Hcap & Hb0 & Hb1 & Hb2 & Hb3 & _
iApply wp_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise |
iNext
iDestruct string_suffix_ _ _ _ j with Hs as [Hsuf Hback] ; exact Hj |
iApply wp_strncmp_lengths with Hsuf Hlt ; exact Hstrncmp | apply linked_outside ; exact Hlinked | reflexivity | apply linked_unbound ; exact Hlinked | reflexivity | word_premise | word_premise | word_premise | vm_compute ; intuition congruence |
iNext
iIntros bits Hlength Hsuf Hlt
iDestruct Hback with Hsuf as Hs
iApply wp_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise |
iNext
iApply wp_branch ; word_premise |
iNext
destruct Z.eqbbits mod 2 ^ 32 0 eqn: E ; cbn [ edge_label ]
–apply Z.eqb_eq in E
specialize HlengthE
rewrite length_drop in Hlength
change Z.minZ.of_natlengthys − j 3 = 3 in Hlength
assert Hj3 : j + 3 ≤ lengthys%nat by lia
iApply wp_enter ; exact find_s_L35 | reflexivity |
iNext
iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ ptr_addrp + Z.of_natj + 3 ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |
iNext
iApply wp_goto
iNext
iApply wp_enter ; exact find_s_L18 | word_premise |
iNext
iApply store_names with Hc ; reflexivity | reflexivity |
iNext
iIntros Hc
iApply HΦ $! j + 3%nat j + 3%nat with [%] Hs [$Hlibs $Hlt] Hc
auto
–iApply wp_enter ; exact find_s_L18 | word_premise |
iNext
iApply store_names with Hc ; reflexivity | reflexivity |
iNext
iIntros Hc
iApply HΦ $! j j with [%] Hs [$Hlibs $Hlt] Hc
auto
The directory-prefix comparison keeps the base-name offset; only L16 can advance it, using the comparison's length consequence.
∀ e p b reg ys j r3 r4 x0 x1 y0 Φ
j ≤ lengthys%nat
stringp b reg ys −∗ literalsr3 r4 −∗ cellsx0 x1 y0 −∗ ▷∀i k, ⌜i ≤ lengthys%nat ∧ k ≤ lengthys%nat⌝ −∗ stringp b reg ys −∗ literalsr3 r4 −∗ cellsmkPtrptr_addrp + Z.of_nati ptr_capp mkPtrptr_addrp + Z.of_nati ptr_capp mkPtrptr_addrp + Z.of_natk ptr_capp −∗ ΦRetVoid −∗ WPERunmkFrameset_program_name_fn e [ ] None ExecTAtom"L8" b_instss_L8 b_jumps_L8 : nexpr {Φ}
Proof 99 steps Qed
intros Hv15 Hv0 Hj
destruct name_lookupsge Hlinked as _ & Hlibs & _
iIntros Hs [Hl3 Hl4] Hc HΦ
iDestruct Hs as [%Hok Hps]
iAssert stringp b reg ys with [$Hps] as Hs ; done |
pose proof Hok as Hcap & Hb0 & Hb1 & Hb2 & Hb3 & Hys
assert Hjz : Z.of_natj ≤ Z.of_natlengthys by lia
iApply wp_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise |
iNext
iApply wp_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise |
iNext
iApply wp_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise |
iNext
iApply wp_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise |
iNext
destruct Nat.lt_ge_casesj 7 as Hj7 | Hj7
–assert Hz7 : Z.of_natj < 7 by lia
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
iApply wp_enter ; exact find_s_L26 | reflexivity |
iNext
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
iApply wp_enter ; exact find_s_L18 | word_premise |
iNext
iApply store_names with Hc ; word_premise | word_premise |
iNext
iIntros Hc
iApply HΦ $! 0%nat j with [%] Hs [$Hl3 $Hl4] [Hc] ; lia |
cbn [ Z.of_nat ]
rewrite Z.add_0_r
destruct p
iExact Hc
–assert Hz7 : 7 ≤ Z.of_natj by lia
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
iApply wp_enter ; exact find_s_L25 | reflexivity |
iNext
iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ b + ptr_addrp − b + Z.of_natj − 7 ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |
iNext
iApply wp_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise |
iNext
iDestruct string_window_ _ _ _ j − 7 7 with Hs as (_ & Hl & Hw & Hback) ; lia |
iDestruct string_window_ _ _ _ 0 7 with Hl3 as (%Hok3 & Hl3 & Hw3 & Hback3) ; cbn ; lia |
pose proof Hok3 as _ & _ & _ & H3end & _
iApply wp_call_bind_ _ _ _ _ _ _ _ _ _ _ _ _ memeq_fn invocationmemeq_fn WPtrmkPtrb + ptr_addrp − b + Z.of_natj − 7 ptr_capp; WPtrlibs_ptr; WInt7 ; word_premise | apply find_memeq ; exact proj1Hlinked | reflexivity |
iNext
iApply memeq_specregistry wi ge Hlinked b reg ptr_addrp − b + Z.of_natj − 7 _ ptr_capp 66112 r3 ptr_addrlibs_ptr − 66112 + Z.of_nat0 _ Ro66112 with Hl Hw Hl3 Hw3 ; exact Hmemcmp | rewrite length_take length_drop ; lia | exact Hcap | right ; reflexivity | rewrite ! length_take ! length_drop ; cbn [ length libs_bytes ] ; lia | lia | cbn ; lia | rewrite length_take length_drop ; lia | rewrite length_take length_drop ; cbn [ ptr_addr libs_ptr length libs_bytes ] in H3end |- * ; lia | rewrite length_take length_drop ; lia | apply Forall_take , Forall_drop ; eapply Forall_impl ; exact Hys | intros x Hx ; cbn in Hx ; lia | vm_compute ; repeat constructor ; discriminate |
iNext
iIntros k Hl Hw Hl3 Hw3
iDestruct Hback with Hl Hw as Hs
iDestruct Hback3 with Hl3 Hw3 as Hl3
iExists _
iSplit ; iPureIntro ; reflexivity |
iNext
iApply wp_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise |
iNext
iApply wp_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise |
iNext
iApply wp_goto
iNext
iApply wp_enter ; exact find_s_L26 | word_premise |
iNext
iApply wp_branch ; word_premise |
iNext
repeat match goal with|- context [if then _ else _]⇒destruct tend;cbn [ edge_label ]
+iApply wp_enter ; exact find_s_L18 | word_premise |
iNext
iApply store_names with Hc ; word_premise | word_premise |
iNext
iIntros Hc
iApply HΦ $! 0%nat j with [%] Hs [$Hl3 $Hl4] [Hc] ; lia |
cbn [ Z.of_nat ]
rewrite Z.add_0_r
destruct p
iExact Hc
+iApply wp_enter ; exact find_s_L16 | reflexivity |
iNext
iApply spn_L16_suffix with Hs [$Hl3 $Hl4] Hc ; word_premise | exact Hj |
iExact HΦ
The strengthened triple: the first two name cells hold the same suffix pointer, the short-name cell another suffix pointer. The original string is returned intact, so string_suffix lends either selected string for printing and restores argv0 afterwards.
∀ p b reg ys r3 r4 x0 x1 y0 Φ
stringp b reg ys −∗ literalsr3 r4 −∗ cellsx0 x1 y0 −∗ ▷∀i k, ⌜i ≤ lengthys%nat ∧ k ≤ lengthys%nat⌝ −∗ stringp b reg ys −∗ literalsr3 r4 −∗ cellsmkPtrptr_addrp + Z.of_nati ptr_capp mkPtrptr_addrp + Z.of_nati ptr_capp mkPtrptr_addrp + Z.of_natk ptr_capp −∗ ΦRetVoid −∗ WPERuninvocationset_program_name_fn WPtrp : nexpr {Φ}
Proof 39 steps Qed
iIntros Hs Hlit Hc HΦ
iDestruct Hs as [%Hok Hps]
iAssert stringp b reg ys with [$Hps] as Hs ; done |
pose proof Hok as Hcap & Hb0 & Hb1 & Hb2 & Hb3 & _
rewrite set_program_name_entry
iApply wp_enter ; exact find_s_start | reflexivity |
iNext
iApply wp_strrchr with Hs ; exact Hstrrchr | apply linked_outside ; exact Hlinked | reflexivity | apply linked_unbound ; exact Hlinked | reflexivity | reflexivity | reflexivity | vm_compute ; intuition congruence | vm_compute ; intuition congruence |
iNext
iIntros q Hq Hs
destruct Hq as → | i & Hi & →
–iApply wp_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise |
iNext
iApply wp_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise |
iNext
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 0 ; reflexivity |
iNext
cbn [ Z.eqb edge_label ]
iNext
iApply spn_L8_suffix_ _ _ _ _ 0 with Hs Hlit Hc HΦ ; destruct p ; cbn ; rewrite Z.add_0_r ; reflexivity | reflexivity | lia
–iApply wp_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise |
iNext
iApply wp_let ; reflexivity | reflexivity | word_premise | intros m ; word_premise |
iNext
iApply wp_branch_ _ _ _ _ _ _ _ _ _ 1 ; word_premise |
iNext
cbn [ Z.eqb edge_label ]
iNext
iApply wp_flight_ _ _ _ _ _ _ _ _ _ _ _ _ _ ptr_addrp + Z.of_natSi ; word_premise | cbn ; f_equal ; f_equal ; addr_premise | word_premise |
iNext
iApply wp_goto
iNext
iNext
iApply spn_L8_suffix_ _ _ _ _ Si with Hs Hlit Hc HΦ ; reflexivity | reflexivity | lia
A printing-ready form of set_program_name_suffix_spec: own the selected program-name string, with a wand restoring the full argv0. The suffix may be empty, including when argv0 ends in a slash.
∀ p b reg ys r3 r4 x0 x1 y0 Φ
stringp b reg ys −∗ literalsr3 r4 −∗ cellsx0 x1 y0 −∗ ▷∀i k, ⌜i ≤ lengthys%nat ∧ k ≤ lengthys%nat⌝ −∗ stringmkPtrptr_addrp + Z.of_nati ptr_capp b reg dropi ys −∗ stringmkPtrptr_addrp + Z.of_nati ptr_capp b reg dropi ys −∗ stringp b reg ys −∗ literalsr3 r4 −∗ cellsmkPtrptr_addrp + Z.of_nati ptr_capp mkPtrptr_addrp + Z.of_nati ptr_capp mkPtrptr_addrp + Z.of_natk ptr_capp −∗ ΦRetVoid −∗ WPERuninvocationset_program_name_fn WPtrp : nexpr {Φ}
Explore proof 7 tactics
Initial goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
Hlinked :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractworld
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractworld
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractworld
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
store_keepswi nb nreg
Ksb :
store_keepswi sb sreg
p :
b :
Z
reg :
ys :
listZ
r3, r4 :
x0, x1, y0 :
Φ :
outcome → iPropIΣ
⊢
stringp b reg ys −∗ literalsr3 r4 −∗ cellsx0 x1 y0 −∗ ▷∀i k : nat, ⌜i ≤ lengthys%nat ∧ k ≤ lengthys%nat⌝ −∗ stringptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp b reg dropi ys −∗ stringptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp b reg dropi ys −∗ stringp b reg ys −∗ literalsr3 r4 −∗ cellsptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp ptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp ptr_addr ≔ ptr_addrp + k; ptr_cap ≔ ptr_capp −∗ ΦRetVoid −∗ WPERuninvocationset_program_name_fn WPtrp : nexpr {v. Φv}
iIntros Hs Hlit Hc HΦ
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
Hlinked :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractworld
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractworld
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractworld
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
store_keepswi nb nreg
Ksb :
store_keepswi sb sreg
p :
b :
Z
reg :
ys :
listZ
r3, r4 :
x0, x1, y0 :
Φ :
outcome → iPropIΣ
Hs :
stringp b reg ys
Hlit :
literalsr3 r4
Hc :
cellsx0 x1 y0
HΦ :
▷∀i k : nat, ⌜i ≤ lengthys%nat ∧ k ≤ lengthys%nat⌝ −∗ stringptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp b reg dropi ys −∗ stringptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp b reg dropi ys −∗ stringp b reg ys −∗ literalsr3 r4 −∗ cellsptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp ptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp ptr_addr ≔ ptr_addrp + k; ptr_cap ≔ ptr_capp −∗ ΦRetVoid
∗
WPERuninvocationset_program_name_fn WPtrp {v. Φv}
iApply set_program_name_suffix_spec with Hs Hlit Hc
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
Hlinked :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractworld
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractworld
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractworld
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
store_keepswi nb nreg
Ksb :
store_keepswi sb sreg
p :
b :
Z
reg :
ys :
listZ
r3, r4 :
x0, x1, y0 :
Φ :
outcome → iPropIΣ
HΦ :
▷∀i k : nat, ⌜i ≤ lengthys%nat ∧ k ≤ lengthys%nat⌝ −∗ stringptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp b reg dropi ys −∗ stringptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp b reg dropi ys −∗ stringp b reg ys −∗ literalsr3 r4 −∗ cellsptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp ptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp ptr_addr ≔ ptr_addrp + k; ptr_cap ≔ ptr_capp −∗ ΦRetVoid
∗
iNext
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
Hlinked :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractworld
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractworld
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractworld
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
store_keepswi nb nreg
Ksb :
store_keepswi sb sreg
p :
b :
Z
reg :
ys :
listZ
r3, r4 :
x0, x1, y0 :
Φ :
outcome → iPropIΣ
HΦ :
∀i k : nat, ⌜i ≤ lengthys%nat ∧ k ≤ lengthys%nat⌝ −∗ stringptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp b reg dropi ys −∗ stringptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp b reg dropi ys −∗ stringp b reg ys −∗ literalsr3 r4 −∗ cellsptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp ptr_addr ≔ ptr_addrp + i; ptr_cap ≔ ptr_capp ptr_addr ≔ ptr_addrp + k; ptr_cap ≔ ptr_capp −∗ ΦRetVoid
∗
iIntros i k Hi Hk Hs Hlit Hc
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
Hlinked :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractworld
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractworld
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractworld
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
store_keepswi nb nreg
Ksb :
store_keepswi sb sreg
p :
b :
Z
reg :
ys :
listZ
r3, r4 :
x0, x1, y0 :
Φ :
outcome → iPropIΣ
i, k :
nat
Hi :
i ≤ lengthys%nat
Hk :
k ≤ lengthys%nat
HΦ :
∀i0 k0 : nat, ⌜i0 ≤ lengthys%nat ∧ k0 ≤ lengthys%nat⌝ −∗ stringptr_addr ≔ ptr_addrp + i0; ptr_cap ≔ ptr_capp b reg dropi0 ys −∗ stringptr_addr ≔ ptr_addrp + i0; ptr_cap ≔ ptr_capp b reg dropi0 ys −∗ stringp b reg ys −∗ literalsr3 r4 −∗ cellsptr_addr ≔ ptr_addrp + i0; ptr_cap ≔ ptr_capp ptr_addr ≔ ptr_addrp + i0; ptr_cap ≔ ptr_capp ptr_addr ≔ ptr_addrp + k0; ptr_cap ≔ ptr_capp −∗ ΦRetVoid
Hs :
stringp b reg ys
Hlit :
literalsr3 r4
∗
iDestruct string_suffix_ _ _ _ i with Hs as [Hs Hback] ; exact Hi |
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
Hlinked :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractworld
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractworld
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractworld
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
store_keepswi nb nreg
Ksb :
store_keepswi sb sreg
p :
b :
Z
reg :
ys :
listZ
r3, r4 :
x0, x1, y0 :
Φ :
outcome → iPropIΣ
i, k :
nat
Hi :
i ≤ lengthys%nat
Hk :
k ≤ lengthys%nat
HΦ :
∀i0 k0 : nat, ⌜i0 ≤ lengthys%nat ∧ k0 ≤ lengthys%nat⌝ −∗ stringptr_addr ≔ ptr_addrp + i0; ptr_cap ≔ ptr_capp b reg dropi0 ys −∗ stringptr_addr ≔ ptr_addrp + i0; ptr_cap ≔ ptr_capp b reg dropi0 ys −∗ stringp b reg ys −∗ literalsr3 r4 −∗ cellsptr_addr ≔ ptr_addrp + i0; ptr_cap ≔ ptr_capp ptr_addr ≔ ptr_addrp + i0; ptr_cap ≔ ptr_capp ptr_addr ≔ ptr_addrp + k0; ptr_cap ≔ ptr_capp −∗ ΦRetVoid
Hlit :
literalsr3 r4
Hc :
∗
iApply HΦ $! i k with [%] Hs Hback Hlit Hc
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
world :
Type
SafepointStable0 :
ge :
Hlinked :
Hstrrchr :
registryTAtom"strrchr" = Somestrrchr_contractworld
Hmemcmp :
registryTAtom"memcmp" = Somememcmp_contractworld
Hstrncmp :
registryTAtom"strncmp" = Somestrncmp_contractworld
pn, nreg, sreg :
nb, sb :
Z
Hpn_end :
program_name_b + 8 ≤ r_endpn
Hnb_cell :
0 ≤ nb ∧ nb mod 8 = 0 ∧ nb + 8 ≤ r_endnreg ≤ 2 ^ 48
Hsb_cell :
0 ≤ sb ∧ sb mod 8 = 0 ∧ sb + 8 ≤ r_endsreg ≤ 2 ^ 48
Kpn :
Knb :
store_keepswi nb nreg
Ksb :
store_keepswi sb sreg
p :
b :
Z
reg :
ys :
listZ
r3, r4 :
x0, x1, y0 :
Φ :
outcome → iPropIΣ
i, k :
nat
Hi :
i ≤ lengthys%nat
Hk :
k ≤ lengthys%nat
⊢
i ≤ lengthys%nat ∧ k ≤ lengthys%nat
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
iIntros Hs Hlit Hc HΦ
iApply set_program_name_suffix_spec with Hs Hlit Hc
iNext
iIntros i k Hi Hk Hs Hlit Hc
iDestruct string_suffix_ _ _ _ i with Hs as [Hs Hback] ; exact Hi |
iApply HΦ $! i k with [%] Hs Hback Hlit Hc
auto
HelloProgNameOn over a Logic instance of its own.