rocq/theories/LocaleLogic.v
The locale world in the program logic of Logic.v (docs/logic.md, "Strings the world lends"): locale_wi, the world interpretation of a program that calls setlocale, over Campaign 4's locale_world (Locale.v), and what it gives the triples of LentLogic.v and HelloLocale.v.
locale_wi rep m w h asks of the memory m and the ghost heap h:
locale_ready: setlocale's trusted representation rep, its writable roots, every category's name a readable C string, its read spans, the heap objects it owns, the names' aligned bases;roots_apartandids_apart: the roots setlocale writes and the objects it may release are apart from the program's pieces, as the frame of an external call needs (prefix_agrees);cap_private: the object of every read, root and name capability owns no piece of h, so libc's locale memory is not the program's;names_current: every ghost name piece is a category's current name with its text, so alenttoken is the world's name;codec_current: the codec piece, under the keycodec_key, holds the world's current codec, so a conversion can name the codec a setter selected.
From it, locale_wi_lent is LentLogic.v's hypothesis lent_at for every ghost name, and locale_wi_pre and locale_wi_query are HelloLocale.v's premises on setlocale's query, the latter from Campaign 4's LocaleOn instance over the logic's own machine. A safepoint keeps it where it keeps rep and readiness (locale_wi_safepoint).
A setter keeps it too, with every category renamed to its new name (locale_wi_setter): the frame keeps libc's roots apart, and Campaign 4's private provenance (locale_delegates_private) makes every new read, root and name a born object or an old private one. The setter also gives the codec piece the new codec. locale_set_return is that for setlocale(c, p), in the form of wp_lend's premise, and wp_setlocale_set is the setter's triple.
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 Machine Panics StepRules ExternalCalls ExternalMachine Pieces Heap ContractFrame Language Logic Locale LentLogic
Open Scope Z_scope
Open Scope list_scope
The world interpretation
The capability c names an object, read-write or read-only, that owns no piece of memory of h; a null or function capability names none.
Every ghost name piece of h is the current name, with its text, of a category of the world w.
∀k p t, h !! PNamek = SomeVNamep t → Ink locale_categories ∧ p = locale_namew k ∧ t = locale_textw k
The key of the codec piece, which is no category's.
−1
The codec piece of h, if any, holds the codec of the world w.
∀c, h !! PNamecodec_key = SomeVCodecc → locale_codecw = c
The world interpretation of a program that calls setlocale, whose trusted representation is rep: in the memory m and against the ghost heap h, the world w is ready, libc's roots and releasable objects are apart from the program's pieces, its read, root and name capabilities are private, and the ghost names and the codec are current.
73Definition locale_wirep : mem → locale_world → Prop m : mem w : locale_world h : gmappiece pval : Prop ≔
locale_readyrep m w ∧ roots_apartlocale_rootsw h m ∧ ids_apartlocale_ownedw h ∧ Forallλs ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw ∧ ∀k, Ink locale_categories → cap_privateh ptr_caplocale_namew k ∧ names_currentw h ∧ codec_currentw h
Lent names
An access that succeeds through a read-write or read-only capability of b, from a for n bytes, lies in b's region.
∀ m a c b n r al
access_resm a c n r al = Someok
∃reg, object_regionb m_regionsm = Somereg ∧ b ≤ a ∧ a + n ≤ r_endreg
Explore proof 6 tactics
Initial goal
intros Hc Ha
unfold access_res , cap_access_res in Ha
destruct Hc as → | → ; destruct object_regionb m_regionsm as reg | eqn: E ; try discriminate Ha
2 openfocused goal
all: destruct b ≤? a && a + n ≤? r_endreg eqn: Hb ; | discriminate Ha
2 openm :
a, b, n :
Z
r :
al :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Hb :
b ≤? a && a + n ≤? r_endreg = true
Ha :
Somealigned_resa al = Someok
focused goal
m :
a, b, n :
Z
r :
al :
Z
reg :
E :
object_regionb m_regionsm = Somereg
Hb :
b ≤? a && a + n ≤? r_endreg = true
Ha :
Somereadonly_access_resr a al = Someok
all: apply andb_true_iff in Hb as H1 H2 ; apply Z.leb_le in H1 ; apply Z.leb_le in H2
2 openm :
a, b, n :
Z
r :
al :
Z
reg :
E :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + n ≤ r_endreg
Ha :
Somealigned_resa al = Someok
focused goal
m :
a, b, n :
Z
r :
al :
Z
reg :
E :
object_regionb m_regionsm = Somereg
H1 :
b ≤ a
H2 :
a + n ≤ r_endreg
Ha :
Somereadonly_access_resr a al = Someok
all: exists reg ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hc Ha
unfold access_res , cap_access_res in Ha
destruct Hc as → | → ; destruct object_regionb m_regionsm as reg | eqn: E ; try discriminate Ha
all: destruct b ≤? a && a + n ≤? r_endreg eqn: Hb ; | discriminate Ha
all: apply andb_true_iff in Hb as H1 H2 ; apply Z.leb_le in H1 ; apply Z.leb_le in H2
all: exists reg ; auto
Under locale_wi, in a memory whose live objects are apart, whose objects fit and whose freed objects are empty, every ghost name is lent where lent_at says: the category's name is a C string in a live object at a multiple of 8, which, being private, is none of the program's, so no live object owning a piece overlaps it.
Explore proof 18 tactics
Initial goal
⊢
locale_wirep m w h → live_disjointm → objects_fitm_regionsm → freed_emptym_regionsm → h !! PNamek = SomeVNamep t → lent_atm h p t
intros Hready & _ & _ & _ & Hpriv & Hcur & _ Hd Hfit Hfree Hk
rep :
mem → locale_world → Prop
m :
w :
k :
Z
p :
t :
listZ
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
⊢
lent_atm h p t
destruct Hcur_ _ _ Hk as Hcat & → & →
rep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
⊢
lent_atm h locale_namew k locale_textw k
pose proof Hready as _ & _ & Hstr & _ & _ & Hal
rep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
⊢
lent_atm h locale_namew k locale_textw k
destruct Hstrk Hcat as Hnz Hcs
rep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
⊢
lent_atm h locale_namew k locale_textw k
destruct Halk Hcat as b & Hc & Hb8
rep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
b :
Z
Hc :
ptr_caplocale_namew k = Objb ∨ ptr_caplocale_namew k = Rob
Hb8 :
b mod 8 = 0
⊢
lent_atm h locale_namew k locale_textw k
destruct access_region_ _ _ _ _ _ _ Hc proj1Hcs as reg & E & Hlo & Hhi
rep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
b :
Z
Hc :
ptr_caplocale_namew k = Objb ∨ ptr_caplocale_namew k = Rob
Hb8 :
b mod 8 = 0
reg :
E :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ ptr_addrlocale_namew k
Hhi :
ptr_addrlocale_namew k + lengthlocale_textw k + 1 ≤ r_endreg
⊢
lent_atm h locale_namew k locale_textw k
destruct Hfitb reg E as Hb0 H48
rep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
b :
Z
Hc :
ptr_caplocale_namew k = Objb ∨ ptr_caplocale_namew k = Rob
Hb8 :
b mod 8 = 0
reg :
E :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ ptr_addrlocale_namew k
Hhi :
ptr_addrlocale_namew k + lengthlocale_textw k + 1 ≤ r_endreg
Hb0 :
0 ≤ b
H48 :
r_endreg ≤ 2 ^ 48
⊢
lent_atm h locale_namew k locale_textw k
assert L : r_lifereg = Live
2 openrep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
b :
Z
Hc :
ptr_caplocale_namew k = Objb ∨ ptr_caplocale_namew k = Rob
Hb8 :
b mod 8 = 0
reg :
E :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ ptr_addrlocale_namew k
Hhi :
ptr_addrlocale_namew k + lengthlocale_textw k + 1 ≤ r_endreg
Hb0 :
0 ≤ b
H48 :
r_endreg ≤ 2 ^ 48
focused goal
rep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
b :
Z
Hc :
ptr_caplocale_namew k = Objb ∨ ptr_caplocale_namew k = Rob
Hb8 :
b mod 8 = 0
reg :
E :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ ptr_addrlocale_namew k
Hhi :
ptr_addrlocale_namew k + lengthlocale_textw k + 1 ≤ r_endreg
Hb0 :
0 ≤ b
H48 :
r_endreg ≤ 2 ^ 48
⊢
lent_atm h locale_namew k locale_textw k
{destruct r_lifereg eqn: L ; reflexivity |
2 openrep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
b :
Z
Hc :
ptr_caplocale_namew k = Objb ∨ ptr_caplocale_namew k = Rob
Hb8 :
b mod 8 = 0
reg :
E :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ ptr_addrlocale_namew k
Hhi :
ptr_addrlocale_namew k + lengthlocale_textw k + 1 ≤ r_endreg
Hb0 :
0 ≤ b
H48 :
r_endreg ≤ 2 ^ 48
deferred goal
rep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
b :
Z
Hc :
ptr_caplocale_namew k = Objb ∨ ptr_caplocale_namew k = Rob
Hb8 :
b mod 8 = 0
reg :
E :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ ptr_addrlocale_namew k
Hhi :
ptr_addrlocale_namew k + lengthlocale_textw k + 1 ≤ r_endreg
Hb0 :
0 ≤ b
H48 :
r_endreg ≤ 2 ^ 48
⊢
lent_atm h locale_namew k locale_textw k
pose proof Hfreeb reg E L
2 openrep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
b :
Z
Hc :
ptr_caplocale_namew k = Objb ∨ ptr_caplocale_namew k = Rob
Hb8 :
b mod 8 = 0
reg :
E :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ ptr_addrlocale_namew k
Hhi :
ptr_addrlocale_namew k + lengthlocale_textw k + 1 ≤ r_endreg
Hb0 :
0 ≤ b
H48 :
r_endreg ≤ 2 ^ 48
H :
r_endreg = b
deferred goal
rep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
b :
Z
Hc :
ptr_caplocale_namew k = Objb ∨ ptr_caplocale_namew k = Rob
Hb8 :
b mod 8 = 0
reg :
E :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ ptr_addrlocale_namew k
Hhi :
ptr_addrlocale_namew k + lengthlocale_textw k + 1 ≤ r_endreg
Hb0 :
0 ≤ b
H48 :
r_endreg ≤ 2 ^ 48
⊢
lent_atm h locale_namew k locale_textw k
lia
deferred goal
rep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
b :
Z
Hc :
ptr_caplocale_namew k = Objb ∨ ptr_caplocale_namew k = Rob
Hb8 :
b mod 8 = 0
reg :
E :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ ptr_addrlocale_namew k
Hhi :
ptr_addrlocale_namew k + lengthlocale_textw k + 1 ≤ r_endreg
Hb0 :
0 ≤ b
H48 :
r_endreg ≤ 2 ^ 48
⊢
lent_atm h locale_namew k locale_textw k
split ; exact Hcs |
rep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
b :
Z
Hc :
ptr_caplocale_namew k = Objb ∨ ptr_caplocale_namew k = Rob
Hb8 :
b mod 8 = 0
reg :
E :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ ptr_addrlocale_namew k
Hhi :
ptr_addrlocale_namew k + lengthlocale_textw k + 1 ≤ r_endreg
Hb0 :
0 ≤ b
H48 :
r_endreg ≤ 2 ^ 48
⊢
0 < ptr_addrlocale_namew k ∧ ptr_addrlocale_namew k + lengthlocale_textw k < 2 ^ 64 ∧ ∃b0 : Z, ptr_caplocale_namew k = Objb0 ∨ ptr_caplocale_namew k = Rob0 ∧ b0 mod 8 = 0 ∧ ∀a : Z, ptr_addrlocale_namew k ≤ a ≤ ptr_addrlocale_namew k + lengthlocale_textw k → ¬owned_liveh m a
split ; lia |
rep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
b :
Z
Hc :
ptr_caplocale_namew k = Objb ∨ ptr_caplocale_namew k = Rob
Hb8 :
b mod 8 = 0
reg :
E :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ ptr_addrlocale_namew k
Hhi :
ptr_addrlocale_namew k + lengthlocale_textw k + 1 ≤ r_endreg
Hb0 :
0 ≤ b
H48 :
r_endreg ≤ 2 ^ 48
⊢
ptr_addrlocale_namew k + lengthlocale_textw k < 2 ^ 64 ∧ ∃b0 : Z, ptr_caplocale_namew k = Objb0 ∨ ptr_caplocale_namew k = Rob0 ∧ b0 mod 8 = 0 ∧ ∀a : Z, ptr_addrlocale_namew k ≤ a ≤ ptr_addrlocale_namew k + lengthlocale_textw k → ¬owned_liveh m a
split ; lia |
rep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
b :
Z
Hc :
ptr_caplocale_namew k = Objb ∨ ptr_caplocale_namew k = Rob
Hb8 :
b mod 8 = 0
reg :
E :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ ptr_addrlocale_namew k
Hhi :
ptr_addrlocale_namew k + lengthlocale_textw k + 1 ≤ r_endreg
Hb0 :
0 ≤ b
H48 :
r_endreg ≤ 2 ^ 48
⊢
∃b0 : Z, ptr_caplocale_namew k = Objb0 ∨ ptr_caplocale_namew k = Rob0 ∧ b0 mod 8 = 0 ∧ ∀a : Z, ptr_addrlocale_namew k ≤ a ≤ ptr_addrlocale_namew k + lengthlocale_textw k → ¬owned_liveh m a
split ; exists b ; auto |
rep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
b :
Z
Hc :
ptr_caplocale_namew k = Objb ∨ ptr_caplocale_namew k = Rob
Hb8 :
b mod 8 = 0
reg :
E :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ ptr_addrlocale_namew k
Hhi :
ptr_addrlocale_namew k + lengthlocale_textw k + 1 ≤ r_endreg
Hb0 :
0 ≤ b
H48 :
r_endreg ≤ 2 ^ 48
⊢
∀a : Z, ptr_addrlocale_namew k ≤ a ≤ ptr_addrlocale_namew k + lengthlocale_textw k → ¬owned_liveh m a
intros a Ha l & v & reg′ & Hl & Hm & Hlv & Hin
rep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
b :
Z
Hc :
ptr_caplocale_namew k = Objb ∨ ptr_caplocale_namew k = Rob
Hb8 :
b mod 8 = 0
reg :
E :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ ptr_addrlocale_namew k
Hhi :
ptr_addrlocale_namew k + lengthlocale_textw k + 1 ≤ r_endreg
Hb0 :
0 ≤ b
H48 :
r_endreg ≤ 2 ^ 48
a :
Z
Ha :
ptr_addrlocale_namew k ≤ a ≤ ptr_addrlocale_namew k + lengthlocale_textw k
l :
v :
reg′ :
Hl :
h !! l = Somev
Hm :
⊢
False
assert Hne : piece_idl ≠ b by exact Hprivk Hcat b Hc b l v or_introleq_refl Hl Hm
rep :
mem → locale_world → Prop
m :
w :
k :
Z
Hready :
locale_readyrep m w
Hpriv :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hcur :
Hd :
Hfit :
Hfree :
Hk :
h !! PNamek = SomeVNamelocale_namew k locale_textw k
Hcat :
Hstr :
∀category : Z, Incategory locale_categories → ptr_addrlocale_namew category ≠ 0 ∧ c_stringm locale_namew category locale_textw category
Hal :
Hnz :
ptr_addrlocale_namew k ≠ 0
Hcs :
c_stringm locale_namew k locale_textw k
b :
Z
Hc :
ptr_caplocale_namew k = Objb ∨ ptr_caplocale_namew k = Rob
Hb8 :
b mod 8 = 0
reg :
E :
object_regionb m_regionsm = Somereg
Hlo :
b ≤ ptr_addrlocale_namew k
Hhi :
ptr_addrlocale_namew k + lengthlocale_textw k + 1 ≤ r_endreg
Hb0 :
0 ≤ b
H48 :
r_endreg ≤ 2 ^ 48
a :
Z
Ha :
ptr_addrlocale_namew k ≤ a ≤ ptr_addrlocale_namew k + lengthlocale_textw k
l :
v :
reg′ :
Hl :
h !! l = Somev
Hm :
Hne :
piece_idl ≠ b
⊢
False
destruct Hd_ _ _ _ Hlv conjE L Hne ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hready & _ & _ & _ & Hpriv & Hcur & _ Hd Hfit Hfree Hk
destruct Hcur_ _ _ Hk as Hcat & → & →
pose proof Hready as _ & _ & Hstr & _ & _ & Hal
destruct Hstrk Hcat as Hnz Hcs
destruct Halk Hcat as b & Hc & Hb8
destruct access_region_ _ _ _ _ _ _ Hc proj1Hcs as reg & E & Hlo & Hhi
destruct Hfitb reg E as Hb0 H48
split ; exact Hcs |
split ; lia |
split ; lia |
split ; exists b ; auto |
intros a Ha l & v & reg′ & Hl & Hm & Hlv & Hin
assert Hne : piece_idl ≠ b by exact Hprivk Hcat b Hc b l v or_introleq_refl Hl Hm
destruct Hd_ _ _ _ Hlv conjE L Hne ; lia
Renaming the ghost names
Renaming keeps every piece of memory.
Explore proof 6 tactics
Initial goal
intros Hm
induction ks as | k ks IH ; reflexivity |
cbn [ rename ]
rewrite lookup_insert_ne ; exact IH |
intros ←
exact Hm
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hm
induction ks as | k ks IH ; reflexivity |
cbn [ rename ]
rewrite lookup_insert_ne ; exact IH |
intros ←
exact Hm
A key renaming does not touch keeps its name.
Explore proof 9 tactics
Initial goal
intros Hk
induction ks as | k′ ks IH ; reflexivity |
cbn [ rename ]
rewrite lookup_insert_ne ; | intros E ; injection E as → ; apply Hk ; left ; reflexivity
apply IH
intros Hin
apply Hk
right
exact Hin
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hk
induction ks as | k′ ks IH ; reflexivity |
cbn [ rename ]
rewrite lookup_insert_ne ; | intros E ; injection E as → ; apply Hk ; left ; reflexivity
apply IH
intros Hin
apply Hk
right
exact Hin
An address a renamed heap owns, the heap owned.
Explore proof 4 tactics
Initial goal
⊢
owned_liverenameh ks new m a → owned_liveh m a
intros l & v & reg & Hl & Hm & Hlv & Hin
exists l, v, reg
rewrite rename_mem_ _ _ _ Hm in Hl
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Objects apart from h are apart from it renamed.
Explore proof 3 tactics
Initial goal
intros Ha b l v Hb Hl Hm
rewrite rename_mem_ _ _ _ Hm in Hl
exact Hab l v Hb Hl Hm
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A capability private to h is private to it renamed.
Explore proof 3 tactics
Initial goal
⊢
cap_privateh c → cap_privaterenameh ks new c
intros Hc b Hb
apply ids_apart_rename
exact Hcb Hb
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
What the setter's locale_retained_cap keeps private: a born object, apart from h, or an old private source's own capability.
Explore proof 13 tactics
Initial goal
⊢
locale_wirep m w h → ids_apartborn h → locale_retained_capw born c → cap_privateh c
intros _ & _ & _ & Hsrc & Hnames & _ Hb base & Hin & Hc | s & Hin & →
2 openrep :
mem → locale_world → Prop
m :
w :
born :
listZ
c :
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
base :
Z
Hin :
Inbase born
⊢
cap_privateh c
focused goal
rep :
mem → locale_world → Prop
m :
w :
born :
listZ
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
s :
Hin :
–intros b Hc′
2 openrep :
mem → locale_world → Prop
m :
w :
born :
listZ
c :
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
base :
Z
Hin :
Inbase born
b :
Z
⊢
ids_apartb h
deferred goal
rep :
mem → locale_world → Prop
m :
w :
born :
listZ
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
s :
Hin :
assert b = base as →
3 openrep :
mem → locale_world → Prop
m :
w :
born :
listZ
c :
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
base :
Z
Hin :
Inbase born
b :
Z
⊢
b = base
focused goal
rep :
mem → locale_world → Prop
m :
w :
born :
listZ
c :
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
base :
Z
Hin :
Inbase born
⊢
ids_apartbase h
deferred goal
rep :
mem → locale_world → Prop
m :
w :
born :
listZ
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
s :
Hin :
{destruct Hc as → | → ; destruct Hc′ as E | E ; congruence
2 opendeferred goal
rep :
mem → locale_world → Prop
m :
w :
born :
listZ
c :
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
base :
Z
Hin :
Inbase born
⊢
ids_apartbase h
deferred goal
rep :
mem → locale_world → Prop
m :
w :
born :
listZ
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
s :
Hin :
intros b′ l v Hb′ Hl Hm
2 openrep :
mem → locale_world → Prop
m :
w :
born :
listZ
c :
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
base :
Z
Hin :
Inbase born
b′ :
Z
l :
v :
Hb′ :
Inb′ base
Hl :
h !! l = Somev
Hm :
⊢
piece_idl ≠ b′
deferred goal
rep :
mem → locale_world → Prop
m :
w :
born :
listZ
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
s :
Hin :
destruct Hb′ as ← |
2 openrep :
mem → locale_world → Prop
m :
w :
born :
listZ
c :
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
base :
Z
Hin :
Inbase born
l :
v :
Hl :
h !! l = Somev
Hm :
⊢
piece_idl ≠ base
deferred goal
rep :
mem → locale_world → Prop
m :
w :
born :
listZ
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
s :
Hin :
exact Hbbase l v Hin Hl Hm
deferred goal
rep :
mem → locale_world → Prop
m :
w :
born :
listZ
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
s :
Hin :
–unfold locale_private_sources in Hin
rep :
mem → locale_world → Prop
m :
w :
born :
listZ
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
s :
Hin :
Ins locale_readsw ++ locale_rootsw ++ maplocale_name_spanw locale_categories
apply in_app_or in Hin as Hin | Hin
2 openrep :
mem → locale_world → Prop
m :
w :
born :
listZ
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
s :
Hin :
Ins locale_readsw ++ locale_rootsw
focused goal
rep :
mem → locale_world → Prop
m :
w :
born :
listZ
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
s :
Hin :
Ins maplocale_name_spanw locale_categories
+rewrite List.Forall_forall in Hsrc
2 openrep :
mem → locale_world → Prop
m :
w :
born :
listZ
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
s :
Hin :
Ins locale_readsw ++ locale_rootsw
Hsrc :
∀x : span, Inx locale_readsw ++ locale_rootsw → cap_privateh ptr_capspan_ptrx
deferred goal
rep :
mem → locale_world → Prop
m :
w :
born :
listZ
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
s :
Hin :
Ins maplocale_name_spanw locale_categories
exact Hsrcs Hin
deferred goal
rep :
mem → locale_world → Prop
m :
w :
born :
listZ
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
s :
Hin :
Ins maplocale_name_spanw locale_categories
+apply in_map_iff in Hin as k & ← & Hk
rep :
mem → locale_world → Prop
m :
w :
born :
listZ
Hsrc :
Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw
Hnames :
∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k
Hb :
ids_apartborn h
k :
Z
Hk :
exact Hnamesk Hk
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros _ & _ & _ & Hsrc & Hnames & _ Hb base & Hin & Hc | s & Hin & →
–intros b Hc′
assert b = base as →
{destruct Hc as → | → ; destruct Hc′ as E | E ; congruence
intros b′ l v Hb′ Hl Hm
destruct Hb′ as ← |
exact Hbbase l v Hin Hl Hm
–unfold locale_private_sources in Hin
apply in_app_or in Hin as Hin | Hin
+rewrite List.Forall_forall in Hsrc
exact Hsrcs Hin
+apply in_map_iff in Hin as k & ← & Hk
exact Hnamesk Hk
The new names, after a setter, of every category of the world w'.
λk ⇒ locale_namew′ k, locale_textw′ k
The codec piece holding the codec c.
The ghost heap h with every category renamed to its name in w' and the codec piece holding w''s codec: what a setter makes of it.
Relocaling keeps every piece of memory.
Explore proof 7 tactics
Initial goal
intros Hm
unfold relocale
⊢
overwritecodec_pslocale_codecw′ renameh locale_categories current_namesw′ !! l = h !! l
rewrite overwrite_out ; exact rename_mem_ _ _ _ Hm |
⊢
l ∉ codec_pslocale_codecw′.*1
cbn
rewrite list_elem_of_singleton
intros →
exact Hm
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hm
unfold relocale
rewrite overwrite_out ; exact rename_mem_ _ _ _ Hm |
cbn
rewrite list_elem_of_singleton
intros →
exact Hm
An address a relocaled heap owns, the heap owned.
Explore proof 4 tactics
Initial goal
⊢
owned_liverelocaleh w′ m a → owned_liveh m a
intros l & v & reg & Hl & Hm & Hlv & Hin
exists l, v, reg
rewrite relocale_mem_ _ _ Hm in Hl
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A capability private to h is private to it relocaled.
Explore proof 3 tactics
Initial goal
⊢
cap_privateh c → cap_privaterelocaleh w′ c
intros Hc b Hb b′ l v Hb′ Hl Hm
rewrite relocale_mem_ _ _ Hm in Hl
exact Hcb Hb b′ l v Hb′ Hl Hm
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
After a setter with private provenance, from the world w against the ghost heap h, to the world w' in m': if w' is ready, the frame kept h agreeing and libc's old roots apart, and the born objects are none of h's, then locale_wi holds of w' and h with every category renamed to its new name and the codec piece holding the new codec (relocale).
∀ rep xs m w h born m′ w′
locale_wirep m w h
locale_readyrep m′ w′
locale_delegatesxs m w born m′ w′
roots_apartlocale_rootsw h m′
ids_apartborn h
Proof 51 steps Qed
intros Hwi Hready Hdel Hd Hra Hb
pose proof Hwi as _ & _ & Hown & _ & _ & Hcur & _
pose proof Hdel as Hroots & _ & _ & Howned
split ; exact Hready |
split ; | split ; | split ; | split ; | split
–intros sp a Hin Hs Ho
apply owned_live_relocale in Ho
exact owned_not_authority_ _ _ _ _ Hd Hra Hb Ho proj2Hrootssp Hin a Hs
–intros b l v Hin Hl Hm
rewrite relocale_mem_ _ _ Hm in Hl
–apply List.Forall_forall
intros sp Hin
apply cap_private_relocale
apply retained_privaterep m w h born _ Hwi Hb
apply locale_delegates_private_ _ _ _ _ _ _ Hdel
unfold locale_private_sources
apply in_or_app
left
exact Hin
–intros k Hk
apply cap_private_relocale
apply retained_privaterep m w h born _ Hwi Hb
apply locale_delegates_private_ _ _ _ _ _ locale_name_spanw' k Hdel
unfold locale_private_sources
apply in_or_app
right
apply in_map
exact Hk
–intros k p t Hl
+rewrite overwrite_out in Hl ; | cbn ; rewrite list_elem_of_singleton ; congruence
destruct In_decZ.eq_dec k locale_categories as Hk | Hk
The locale logic over any runtime R.
Import L LG
setlocale's query of a category whose name is lent is admitted: the world is ready and the category is one of its own.
∀ rep requests m w h k p t z
contract_presetlocale_contractrep requests WIntk; WPtrz m w
Explore proof 5 tactics
Initial goal
rep :
mem → locale_world → Prop
requests :
listword → mem → locale_world → Z → Z → Prop
m :
w :
k :
Z
p :
t :
listZ
z :
⊢
locale_wirep m w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → contract_presetlocale_contractrep requests WIntk; WPtrz m w
intros Hready & _ & _ & _ & _ & Hcur & _ Hk Hz
rep :
mem → locale_world → Prop
requests :
listword → mem → locale_world → Z → Z → Prop
m :
w :
k :
Z
p :
t :
listZ
z :
Hready :
locale_readyrep m w
Hcur :
Hz :
ptr_addrz = 0
⊢
contract_presetlocale_contractrep requests WIntk; WPtrz m w
destruct Hcur_ _ _ Hk as Hcat & _ & _
rep :
mem → locale_world → Prop
requests :
listword → mem → locale_world → Z → Z → Prop
m :
w :
k :
Z
p :
t :
listZ
z :
Hready :
locale_readyrep m w
Hcur :
Hz :
ptr_addrz = 0
Hcat :
⊢
contract_presetlocale_contractrep requests WIntk; WPtrz m w
split ; exact Hready |
rep :
mem → locale_world → Prop
requests :
listword → mem → locale_world → Z → Z → Prop
m :
w :
k :
Z
p :
t :
listZ
z :
Hready :
locale_readyrep m w
Hcur :
Hz :
ptr_addrz = 0
Hcat :
exists k, z
rep :
mem → locale_world → Prop
requests :
listword → mem → locale_world → Z → Z → Prop
m :
w :
k :
Z
p :
t :
listZ
z :
Hready :
locale_readyrep m w
Hcur :
Hz :
ptr_addrz = 0
Hcat :
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hready & _ & _ & _ & _ & Hcur & _ Hk Hz
destruct Hcur_ _ _ Hk as Hcat & _ & _
split ; exact Hready |
exists k, z
auto
setlocale's query of a category whose name is lent returns that name and changes nothing.
∀ rep requests r args s m w h k p t z trace ending s′ m′ w′
locale_wirep m w h
ptr_addrz = 0
M.E.invokesetlocale_contractrep requests r args WIntk; WPtrz s m w trace ending s′ m′ w′
s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
Explore proof 4 tactics
Initial goal
rep :
mem → locale_world → Prop
requests :
listword → mem → locale_world → Z → Z → Prop
r :
args :
listarg
s :
R.state
m :
w :
k :
Z
p :
t :
listZ
z :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
⊢
locale_wirep m w h → h !! PNamek = SomeVNamep t → ptr_addrz = 0 → M.E.invokesetlocale_contractrep requests r args WIntk; WPtrz s m w trace ending s′ m′ w′ → s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
intros _ & _ & _ & _ & _ & Hcur & _ Hk Hz Hi
rep :
mem → locale_world → Prop
requests :
listword → mem → locale_world → Z → Z → Prop
r :
args :
listarg
s :
R.state
m :
w :
k :
Z
p :
t :
listZ
z :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcur :
Hz :
ptr_addrz = 0
Hi :
M.E.invokesetlocale_contractrep requests r args WIntk; WPtrz s m w trace ending s′ m′ w′
⊢
s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrp
destruct Hcur_ _ _ Hk as _ & → & _
rep :
mem → locale_world → Prop
requests :
listword → mem → locale_world → Z → Z → Prop
r :
args :
listarg
s :
R.state
m :
w :
k :
Z
t :
listZ
z :
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
Hcur :
Hk :
h !! PNamek = SomeVNamelocale_namew k t
Hz :
ptr_addrz = 0
Hi :
M.E.invokesetlocale_contractrep requests r args WIntk; WPtrz s m w trace ending s′ m′ w′
⊢
s′ = s ∧ m′ = m ∧ w′ = w ∧ ending = CallReturnWPtrlocale_namew k
destruct LC.setlocale_query_invocation_ _ _ _ _ _ _ _ _ _ _ _ _ _ Hz Hi as _ & → & → & → & →
rep :
mem → locale_world → Prop
requests :
listword → mem → locale_world → Z → Z → Prop
r :
args :
listarg
s :
R.state
m :
w :
k :
Z
t :
listZ
z :
trace :
listevent
Hcur :
Hk :
h !! PNamek = SomeVNamelocale_namew k t
Hz :
ptr_addrz = 0
Hi :
M.E.invokesetlocale_contractrep requests r args WIntk; WPtrz s m w trace CallReturnWPtrlocale_namew k s m w
⊢
s = s ∧ m = m ∧ w = w ∧ CallReturnWPtrlocale_namew k = CallReturnWPtrlocale_namew k
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros _ & _ & _ & _ & _ & Hcur & _ Hk Hz Hi
destruct Hcur_ _ _ Hk as _ & → & _
destruct LC.setlocale_query_invocation_ _ _ _ _ _ _ _ _ _ _ _ _ _ Hz Hi as _ & → & → & → & →
auto
setlocale's setter of the category c, with a string argument p, keeps the frame of a program under locale_wi: every invocation that returns, from a state interpreted with the ghost heap h, returns null or c's new name, keeps h agreeing, the live objects apart and the runtime ready, and locale_wi holds of h with every category renamed to its new name (locale_wi_setter). This is wp_lend's premise for setlocale(c, p), with the new names current_names of the world after the call.
∀ rep requests r args s m w h c p trace values s′ m′ w′
locale_wirep m w h
agreesm h
R.readys m
ptr_addrp ≠ 0
M.E.invokesetlocale_contractrep requests r args WIntc; WPtrp s m w trace CallReturnvalues s′ m′ w′
Proof 41 steps Qed
intros Hwi Ha Hd Hr Hp Hi
assert Hq : locale_queryWIntc; WPtrp = false by cbn ; apply Z.eqb_neq ; exact Hp
pose proof Hwi as _ & Hra & Hown & _
remember CallReturnvalues as en eqn: Een
destruct Hi as trace ending s′ m′ w′ born _ _ Hpre Hpost _ _ _ | why trace s′ m′ w′ born _ _ _ _ _ ; | discriminate Een
subst ending
destruct M.E.prefix_preserve_ _ _ _ _ _ _ _ _ _ _ Hpre Hr as Hr′ _
assert Hw : roots_apartcontract_writessetlocale_contractrep requests WIntc; WPtrp m w h m
assert Hrel : ids_apartcontract_releasessetlocale_contractrep requests WIntc; WPtrp m w h
destruct prefix_agrees_ _ _ _ _ _ _ _ _ _ _ h Hpre Hr Hd Ha Hw Hrel as Ha′ & Hd′ & Hb & Hra′
unfold setlocale_contract in Hra'
cbn [ contract_writes ] in Hra'
unfold locale_writes in Hra'
rewrite Hq in Hra'
destruct Hpre as _ _ Hpre
unfold setlocale_contract in Hpre
cbn [ contract_prefix ] in Hpre
rewrite Hq in Hpre
destruct Hpre as Hready & Hdel & _
unfold setlocale_contract in Hpost
cbn [ contract_post ] in Hpost
destruct Hpost as c′ & p′ & Hxs & Hend
injection Hxs as ← ←
rewrite Hq in Hend
exists match values with WPtrq ⇒ q _ ⇒ mkPtr0 CNone end, current_namesw', codec_pslocale_codecw'
destruct Hend as Hv _ | Hv _ ; injection Hv as →
all: split ; reflexivity | ; split ; auto |
all: split ; eexists ; reflexivity | ; split ; reflexivity |
all: split ; constructor ; intros m0 ; exact I | constructor |
all: split ; exact Ha' | ; split ; exact Hd' | ; split ; exact Hr' |
all: exact locale_wi_setter_ _ _ _ _ _ _ _ Hwi Hready Hdel Hd' Hra' Hb
A safepoint keeps locale_wi where it keeps rep and readiness: the roots stay apart since no region changes (collector_live), and the rest is of the world and the ghost heap.
∀ rep : mem → locale_world → Prop
∀s m s′ m′ w, R.safepoints m s′ m′ → locale_readyrep m w → locale_readyrep m′ w
Explore proof 13 tactics
Initial goal
rep :
mem → locale_world → Prop
⊢
∀s : R.state m : mem s′ : R.state m′ : mem w : locale_world, R.safepoints m s′ m′ → locale_readyrep m w → locale_readyrep m′ w → SafepointStablelocale_wirep
intros Hst
rep :
mem → locale_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : locale_world, R.safepoints m s′ m′ → locale_readyrep m w → locale_readyrep m′ w
split
rep :
mem → locale_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : locale_world, R.safepoints m s′ m′ → locale_readyrep m w → locale_readyrep m′ w
intros s m s′ m′ w h Hsp Hr & Ha & Hrest
rep :
mem → locale_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : locale_world, R.safepoints m s′ m′ → locale_readyrep m w → locale_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
locale_readyrep m w
Ha :
Hrest :
ids_apartlocale_ownedw h ∧ Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw ∧ ∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k ∧ names_currentw h ∧ codec_currentw h
⊢
locale_wirep m′ w h
split ; exact Hst_ _ _ _ _ Hsp Hr |
rep :
mem → locale_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : locale_world, R.safepoints m s′ m′ → locale_readyrep m w → locale_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
locale_readyrep m w
Ha :
Hrest :
ids_apartlocale_ownedw h ∧ Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw ∧ ∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k ∧ names_currentw h ∧ codec_currentw h
⊢
roots_apartlocale_rootsw h m′ ∧ ids_apartlocale_ownedw h ∧ Forallλs0 : span ⇒ cap_privateh ptr_capspan_ptrs0 locale_readsw ++ locale_rootsw ∧ ∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k ∧ names_currentw h ∧ codec_currentw h
split ; | exact Hrest
rep :
mem → locale_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : locale_world, R.safepoints m s′ m′ → locale_readyrep m w → locale_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
locale_readyrep m w
Ha :
Hrest :
ids_apartlocale_ownedw h ∧ Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw ∧ ∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k ∧ names_currentw h ∧ codec_currentw h
⊢
roots_apartlocale_rootsw h m′
intros sp a Hin Hs l & v & reg & Hl & Hm & E Hlive & Hb
rep :
mem → locale_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : locale_world, R.safepoints m s′ m′ → locale_readyrep m w → locale_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
locale_readyrep m w
Ha :
Hrest :
ids_apartlocale_ownedw h ∧ Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw ∧ ∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k ∧ names_currentw h ∧ codec_currentw h
sp :
a :
Z
Hin :
Insp locale_rootsw
Hs :
span_containssp a
l :
v :
reg :
Hl :
h !! l = Somev
Hm :
E :
object_regionpiece_idl m_regionsm′ = Somereg
⊢
False
apply Hasp a Hin Hs
rep :
mem → locale_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : locale_world, R.safepoints m s′ m′ → locale_readyrep m w → locale_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
locale_readyrep m w
Ha :
Hrest :
ids_apartlocale_ownedw h ∧ Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw ∧ ∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k ∧ names_currentw h ∧ codec_currentw h
sp :
a :
Z
Hin :
Insp locale_rootsw
Hs :
span_containssp a
l :
v :
reg :
Hl :
h !! l = Somev
Hm :
E :
object_regionpiece_idl m_regionsm′ = Somereg
⊢
owned_liveh m a
rewrite R.collector_live_ _ _ _ Hsp in E
rep :
mem → locale_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : locale_world, R.safepoints m s′ m′ → locale_readyrep m w → locale_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
locale_readyrep m w
Ha :
Hrest :
ids_apartlocale_ownedw h ∧ Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw ∧ ∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k ∧ names_currentw h ∧ codec_currentw h
sp :
a :
Z
Hin :
Insp locale_rootsw
Hs :
span_containssp a
l :
v :
reg :
Hl :
h !! l = Somev
Hm :
E :
object_regionpiece_idl m_regionsm = Somereg
⊢
owned_liveh m a
exists l, v, reg
rep :
mem → locale_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : locale_world, R.safepoints m s′ m′ → locale_readyrep m w → locale_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
locale_readyrep m w
Ha :
Hrest :
ids_apartlocale_ownedw h ∧ Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw ∧ ∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k ∧ names_currentw h ∧ codec_currentw h
sp :
a :
Z
Hin :
Insp locale_rootsw
Hs :
span_containssp a
l :
v :
reg :
Hl :
h !! l = Somev
Hm :
E :
object_regionpiece_idl m_regionsm = Somereg
split ; exact Hl |
rep :
mem → locale_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : locale_world, R.safepoints m s′ m′ → locale_readyrep m w → locale_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
locale_readyrep m w
Ha :
Hrest :
ids_apartlocale_ownedw h ∧ Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw ∧ ∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k ∧ names_currentw h ∧ codec_currentw h
sp :
a :
Z
Hin :
Insp locale_rootsw
Hs :
span_containssp a
l :
v :
reg :
Hl :
h !! l = Somev
Hm :
E :
object_regionpiece_idl m_regionsm = Somereg
split ; exact Hm |
rep :
mem → locale_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : locale_world, R.safepoints m s′ m′ → locale_readyrep m w → locale_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
locale_readyrep m w
Ha :
Hrest :
ids_apartlocale_ownedw h ∧ Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw ∧ ∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k ∧ names_currentw h ∧ codec_currentw h
sp :
a :
Z
Hin :
Insp locale_rootsw
Hs :
span_containssp a
l :
v :
reg :
Hl :
h !! l = Somev
Hm :
E :
object_regionpiece_idl m_regionsm = Somereg
split ; | exact Hb
rep :
mem → locale_world → Prop
Hst :
∀s : R.state m : mem s′ : R.state m′ : mem w : locale_world, R.safepoints m s′ m′ → locale_readyrep m w → locale_readyrep m′ w
s :
R.state
m :
s′ :
R.state
m′ :
w :
Hsp :
R.safepoints m s′ m′
Hr :
locale_readyrep m w
Ha :
Hrest :
ids_apartlocale_ownedw h ∧ Forallλs : span ⇒ cap_privateh ptr_capspan_ptrs locale_readsw ++ locale_rootsw ∧ ∀k : Z, Ink locale_categories → cap_privateh ptr_caplocale_namew k ∧ names_currentw h ∧ codec_currentw h
sp :
a :
Z
Hin :
Insp locale_rootsw
Hs :
span_containssp a
l :
v :
reg :
Hl :
h !! l = Somev
Hm :
E :
object_regionpiece_idl m_regionsm = Somereg
split ; exact E | exact Hlive
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros Hst
split
intros s m s′ m′ w h Hsp Hr & Ha & Hrest
split ; exact Hst_ _ _ _ _ Hsp Hr |
split ; | exact Hrest
intros sp a Hin Hs l & v & reg & Hl & Hm & E Hlive & Hb
apply Hasp a Hin Hs
rewrite R.collector_live_ _ _ _ Hsp in E
exists l, v, reg
split ; exact Hl |
split ; exact Hm |
split ; | exact Hb
split ; exact E | exact Hlive
The setter's triple
326Context registry : name → optioncontractlocale_world rep : mem → locale_world → Prop requests : listword → mem → locale_world → Z → Z → Prop `{!SafepointStablelocale_wirep} ge : genv
The Iris instance of the registry and locale_wi.
The expressions of the language.
setlocale(c, p)'s triple over the locale world, from wp_lend and locale_set_return: owning every category's name, the codec piece and the string at p, which vc and vp read as, the call lends every category's new name for good, gives the codec piece a new codec c', which is the world's from then on (codec_current), and binds d to null or c's new name.
∀ f e ls lab d vc vp rest j c p b reg bytes old c0 Φ
registryTAtom"setlocale" = Somesetlocale_contractrep requests
lookupTAtom"setlocale" ge_globalsge = None
∗k∈locale_categoriesLL.namedk oldk.1 oldk.2 −∗ ptscodec_psc0 −∗ LL.SL.stringp b reg bytes −∗ ▷∀q new : Z → ptr × listZ c′, ⌜q = mkPtr0 CNone ∨ q = newc.1⌝ −∗ LL.SL.stringp b reg bytes −∗ ptscodec_psc′ −∗ ∗k∈locale_categoriesLL.lentk newk.1 newk.2 −∗ WPERunmkFramef putd WPtrq e ls None Execlab rest j : sexpr {Φ} −∗ WPERunmkFramef e ls None Execlab CallCResultd P GlobalTAtom"setlocale" ArgW vc; ArgP vp :: rest j : sexpr {Φ}
Proof 36 steps Qed
intros Hreg Hfn Hdata Hc Hp Hcat
iIntros Hks Hcodec Hs HK
iDestruct Hs as [%Hok Hs]
pose proof Hok as _ & Hb0 & Hlo & _
iAssert LL.SL.stringp b reg bytes with [Hs] as Hs ; iSplit ; done | iExact Hs |
iApply LL.wp_lendregistry locale_wirep ge locale_wi_lentrep f e ls lab d TAtom"setlocale" ArgW vc; ArgP vp rest j setlocale_contractrep requests WIntc; WPtrp locale_categories old codec_psc0 λq new gs′ ⇒ q = mkPtr0 CNone ∨ q = newc.1 ∧ ∃c′, gs′ = codec_psc′ with Hks Hcodec Hs [HK] ; exact Hreg | reflexivity | exact Hfn | exact Hdata | reflexivity | cbn [ map_option ] ; rewrite Hc Hp ; reflexivity | | | | |
–split ; right ; eexists ; reflexivity | do 2 eexists ; reflexivity
–apply List.Forall_forall
intros k Hk
cbn
rewrite list_elem_of_singleton
intros E
injection E as →
unfold codec_key , locale_categories in Hk
cbn in Hk
intuition lia
–iIntros σ Hσ Hs
iDestruct LL.SL.string_facts with Hσ Hs as %_ Hcs
iDestruct Hσ as h [_ %Hf]
destruct Hf as _ & _ & _ & Hready & _
iPureIntro
split ; exact Hready |
exists c, p
split ; reflexivity |
split ; exact Hcat |
right
eauto
–intros s m w h trace values s′ m′ w′ Hw Ha Hd Hr Hi
assert Hnz : ptr_addrp ≠ 0 by lia
destruct locale_set_returnrep requests _ _ _ _ _ _ _ _ _ _ _ _ _ Hw Ha Hd Hr Hnz Hi as q & new & gs′ & Hv & Hq & Hgs & Hkeys & Hrest
exists q, new, gs'
auto
–iNext
iIntros q new gs′ Hq c′ → Hs Hcodec Hl
iApply HK with [%] Hs Hcodec Hl
exact Hq
LocaleLogicOn over a Logic instance of its own.