Fil-C on Nix

Filnix wiki

the formal campaign

rocq/theories/GetoptLogic.v

Reading getopt's libc cells

A program reads optarg and optind straight from libc's cells, which getopt rewrites at every call. The program owns neither cell: it owns a ghost token, getopt_ps, naming the values getopt last left there, and the world interpretation ties the token to the world's getopt state and the cells' memory (getopt_current, Campaign 4's getopt_state_at). A read of either cell is then an instruction whose result the world interpretation fixes (wp_world_let_with).

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 ExternalCalls ExternalMachine Pieces Heap Language Logic Startup Getopt
Open Scope Z_scope
Open Scope list_scope

The key of the getopt token: no locale category's, not the codec's (-1), and no stream's (below -1).

23Definition getopt_key: Z ≔
64

The getopt token: optarg a and optind i.

26Definition getopt_psa : ptr i : Z : listpiece × pval ≔
PNamegetopt_key, VGetopta i

The getopt token of h, if any, holds the getopt state g's optarg and optind.

30Definition getopt_currentg : getopt_world h : gmappiece pval : Prop ≔
∀a i, h !! PNamegetopt_key = SomeVGetopta i → getopt_optargg = a ∧ getopt_optindg = i

A read access that passes at some alignment passes at alignment 1.

34Lemma access_read_align1
∀ m a c size al
access_resm a c size Read al = Someok
access_resm a c size Read 1 = Someok
Explore proof 2 tactics

Initial goal

m :
mem
a :
Z
c :
cap
size, al :
Z
⊢
access_resm a c size Read al = Someok → access_resm a c size Read 1 = Someok

unfold access_res , cap_access_res , readonly_access_res , aligned_res

m :
mem
a :
Z
c :
cap
size, al :
Z
⊢
match c with
CNone
⇒
SomeRTrapNullCapability
Objbase | Robase
⇒
let* reg ≔ object_regionbase m_regionsm in
Some
base ≤? a && a + size ≤? r_endreg
→
a mod al =? 0
→
ok
else
RTrapMisaligned
else
RTrapOutOfBounds
Fn_
⇒
SomeRTrapOutOfBounds
External_
⇒
None
=
Someok
→
match c with
CNone
⇒
SomeRTrapNullCapability
Objbase | Robase
⇒
let* reg ≔ object_regionbase m_regionsm in
Some
base ≤? a && a + size ≤? r_endreg
→
a mod 1 =? 0
→
ok
else
RTrapMisaligned
else
RTrapOutOfBounds
Fn_
⇒
SomeRTrapOutOfBounds
External_
⇒
None
=
Someok

destruct c as | b | b | g | g ; try discriminate ; destruct object_regionb m_regionsm ; try discriminate ; destruct _ && _ ; try discriminate ; rewrite Z.mod_1_r ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
unfold access_res , cap_access_res , readonly_access_res , aligned_res
destruct c as | b | b | g | g ; try discriminate ; destruct object_regionb m_regionsm ; try discriminate ; destruct _ && _ ; try discriminate ; rewrite Z.mod_1_r ; reflexivity

Sign extension, cut back to its width, is the value cut to it.

43Lemma sign_extension_mod
∀ md hf x
0 < md
sign_extensionmd hf x mod md = x mod md
Explore proof 9 tactics

Initial goal

md, hf, x :
Z
⊢
0 < md → sign_extensionmd hf x mod md = x mod md

intros Hm

md, hf, x :
Z
Hm :
0 < md
⊢
sign_extensionmd hf x mod md = x mod md

unfold sign_extension

md, hf, x :
Z
Hm :
0 < md
⊢
hf ≤? x mod md
→
x mod md − md
else
x mod md
mod
md
=
x mod md

destruct hf ≤? x mod md

2 open

md, hf, x :
Z
Hm :
0 < md
⊢
x mod md − md mod md = x mod md
focused goal
md, hf, x :
Z
Hm :
0 < md
⊢
x mod md mod md = x mod md

–replace x mod md − md with x mod md + −1 × md by lia

2 open

md, hf, x :
Z
Hm :
0 < md
⊢
x mod md + −1 × md mod md = x mod md
deferred goal
md, hf, x :
Z
Hm :
0 < md
⊢
x mod md mod md = x mod md

rewrite Z.mod_add ; | lia

2 open

md, hf, x :
Z
Hm :
0 < md
⊢
x mod md mod md = x mod md
deferred goal
md, hf, x :
Z
Hm :
0 < md
⊢
x mod md mod md = x mod md

apply Z.mod_mod

2 open

md, hf, x :
Z
Hm :
0 < md
⊢
md ≠ 0
deferred goal
md, hf, x :
Z
Hm :
0 < md
⊢
x mod md mod md = x mod md

lia

deferred goal
md, hf, x :
Z
Hm :
0 < md
⊢
x mod md mod md = x mod md

–apply Z.mod_mod

md, hf, x :
Z
Hm :
0 < md
⊢
md ≠ 0

lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros Hm
unfold sign_extension
destruct hf ≤? x mod md
–replace x mod md − md with x mod md + −1 × md by lia
rewrite Z.mod_add ; | lia
apply Z.mod_mod
lia
–apply Z.mod_mod
lia

A raw signed 32-bit load at offset off from the proven pointer p, whose read access passes: the four bytes there, as a W word.

53Lemma op_raw_load_sw
∀ m p off
access_resm raw_addressptr_addrp off ptr_capp 4 Read 1 = Someok
op_resRawLoadLdNarrowSw off W WPtrp m = SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 4 mod 2 ^ 32 m
Explore proof 10 tactics

Initial goal

m :
mem
p :
ptr
off :
Z
⊢
access_resm raw_addressptr_addrp off ptr_capp 4 Read 1 = Someok → op_resRawLoadLdNarrowSw off W WPtrp m = SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 4 mod 2 ^ 32 m

intros H

m :
mem
p :
ptr
off :
Z
H :
access_resm raw_addressptr_addrp off ptr_capp 4 Read 1 = Someok
⊢
op_resRawLoadLdNarrowSw off W WPtrp m = SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 4 mod 2 ^ 32 m

assert E : op_resRawLoadLdNarrowSw off W WPtrp m = op_res_intRawLoadLdNarrowSw off W WPtrp m by reflexivity

m :
mem
p :
ptr
off :
Z
H :
access_resm raw_addressptr_addrp off ptr_capp 4 Read 1 = Someok
E :
op_resRawLoadLdNarrowSw off W WPtrp m = op_res_intRawLoadLdNarrowSw off W WPtrp m
⊢
op_resRawLoadLdNarrowSw off W WPtrp m = SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 4 mod 2 ^ 32 m

rewrite E

m :
mem
p :
ptr
off :
Z
H :
access_resm raw_addressptr_addrp off ptr_capp 4 Read 1 = Someok
E :
op_resRawLoadLdNarrowSw off W WPtrp m = op_res_intRawLoadLdNarrowSw off W WPtrp m
⊢
op_res_intRawLoadLdNarrowSw off W WPtrp m = SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 4 mod 2 ^ 32 m

cbn - [ access_res raw_address load_bytes extended ]

m :
mem
p :
ptr
off :
Z
H :
access_resm raw_addressptr_addrp off ptr_capp 4 Read 1 = Someok
E :
op_resRawLoadLdNarrowSw off W WPtrp m = op_res_intRawLoadLdNarrowSw off W WPtrp m
⊢
let* r ≔ int_load_resLdNarrowSw W m raw_addressptr_addrp off ptr_capp in
SomeOpResraw_resr m
=
SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 4 mod 2 ^ 32 m

unfold int_load_res

m :
mem
p :
ptr
off :
Z
H :
access_resm raw_addressptr_addrp off ptr_capp 4 Read 1 = Someok
E :
op_resRawLoadLdNarrowSw off W WPtrp m = op_res_intRawLoadLdNarrowSw off W WPtrp m
⊢
let* r ≔
match access_resm raw_addressptr_addrp off ptr_capp narrow_typeSw.1 Read 1 with
SomeRVal_
⇒
let* x0 ≔ extendedSw W load_bytesm raw_addressptr_addrp off narrow_typeSw.1 in
SomeRValx0
SomeRTrapwhy
⇒
SomeRTrapwhy
SomeRUncheckedwhy
⇒
SomeRUncheckedwhy
None
⇒
None
in
SomeOpResraw_resr m
=
SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 4 mod 2 ^ 32 m

cbn - [ access_res raw_address load_bytes extension ]

m :
mem
p :
ptr
off :
Z
H :
access_resm raw_addressptr_addrp off ptr_capp 4 Read 1 = Someok
E :
op_resRawLoadLdNarrowSw off W WPtrp m = op_res_intRawLoadLdNarrowSw off W WPtrp m
⊢
let* r ≔
match access_resm raw_addressptr_addrp off ptr_capp 4 Read 1 with
SomeRVal_
⇒
SomeRValWIntextensionSw load_bytesm raw_addressptr_addrp off 4 mod 2 ^ 32
SomeRTrapwhy
⇒
SomeRTrapwhy
SomeRUncheckedwhy
⇒
SomeRUncheckedwhy
None
⇒
None
in
SomeOpResraw_resr m
=
SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 4 mod 2 ^ 32 m

rewrite H

m :
mem
p :
ptr
off :
Z
H :
access_resm raw_addressptr_addrp off ptr_capp 4 Read 1 = Someok
E :
op_resRawLoadLdNarrowSw off W WPtrp m = op_res_intRawLoadLdNarrowSw off W WPtrp m
⊢
SomeOpResraw_resRValWIntextensionSw load_bytesm raw_addressptr_addrp off 4 mod 2 ^ 32 m = SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 4 mod 2 ^ 32 m

cbn - [ raw_address load_bytes extension ]

m :
mem
p :
ptr
off :
Z
H :
access_resm raw_addressptr_addrp off ptr_capp 4 Read 1 = Someok
E :
op_resRawLoadLdNarrowSw off W WPtrp m = op_res_intRawLoadLdNarrowSw off W WPtrp m
⊢
SomeOpResRValWIntextensionSw load_bytesm raw_addressptr_addrp off 4 mod 2 ^ 32 m = SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 4 mod 2 ^ 32 m

rewrite sign_extension_mod ; | lia

m :
mem
p :
ptr
off :
Z
H :
access_resm raw_addressptr_addrp off ptr_capp 4 Read 1 = Someok
E :
op_resRawLoadLdNarrowSw off W WPtrp m = op_res_intRawLoadLdNarrowSw off W WPtrp m
⊢
SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 4 mod 2 ^ 32 m = SomeOpResRValWIntload_bytesm raw_addressptr_addrp off 4 mod 2 ^ 32 m

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros H
assert E : op_resRawLoadLdNarrowSw off W WPtrp m = op_res_intRawLoadLdNarrowSw off W WPtrp m by reflexivity
rewrite E
cbn - [ access_res raw_address load_bytes extended ]
unfold int_load_res
cbn - [ access_res raw_address load_bytes extension ]
rewrite H
cbn - [ raw_address load_bytes extension ]
rewrite sign_extension_mod ; | lia
reflexivity

A pointer cell whose pieces agree with the memory, in a live object, holding a word-sized address whose capability's object is not freed, is a pointer_slot there: Campaign 4's reading of a stored pointer.

71Lemma pcell_slot
∀ m b reg o x
live_atm b reg
agree_piecem PAuxb o VAuxptr_capx
all_agreem cellb o ptr_addrx
0 ≤ ptr_addrx < 2 ^ 64
¬freed_inm_regionsm ptr_capx
pointer_slotm b + o x
Explore proof 8 tactics

Initial goal

m :
mem
b :
Z
reg :
region
o :
Z
x :
ptr
⊢
live_atm b reg → agree_piecem PAuxb o VAuxptr_capx → all_agreem cellb o ptr_addrx → 0 ≤ ptr_addrx < 2 ^ 64 → ¬freed_inm_regionsm ptr_capx → pointer_slotm b + o x

intros Hlv Hax Hcl Hr Hf

m :
mem
b :
Z
reg :
region
o :
Z
x :
ptr
Hlv :
live_atm b reg
Hax :
agree_piecem PAuxb o VAuxptr_capx
Hcl :
all_agreem cellb o ptr_addrx
Hr :
0 ≤ ptr_addrx < 2 ^ 64
Hf :
¬freed_inm_regionsm ptr_capx
⊢
pointer_slotm b + o x

split ; exact Hr |

m :
mem
b :
Z
reg :
region
o :
Z
x :
ptr
Hlv :
live_atm b reg
Hax :
agree_piecem PAuxb o VAuxptr_capx
Hcl :
all_agreem cellb o ptr_addrx
Hr :
0 ≤ ptr_addrx < 2 ^ 64
Hf :
¬freed_inm_regionsm ptr_capx
⊢
load_bytesm b + o 8 = ptr_addrx ∧ m_auxm b + o = ptr_capx

split

2 open

m :
mem
b :
Z
reg :
region
o :
Z
x :
ptr
Hlv :
live_atm b reg
Hax :
agree_piecem PAuxb o VAuxptr_capx
Hcl :
all_agreem cellb o ptr_addrx
Hr :
0 ≤ ptr_addrx < 2 ^ 64
Hf :
¬freed_inm_regionsm ptr_capx
⊢
load_bytesm b + o 8 = ptr_addrx
focused goal
m :
mem
b :
Z
reg :
region
o :
Z
x :
ptr
Hlv :
live_atm b reg
Hax :
agree_piecem PAuxb o VAuxptr_capx
Hcl :
all_agreem cellb o ptr_addrx
Hr :
0 ≤ ptr_addrx < 2 ^ 64
Hf :
¬freed_inm_regionsm ptr_capx
⊢
m_auxm b + o = ptr_capx

–rewrite cell_loadm b reg o ptr_addrx b + o Hlv Hcl eq_refl

2 open

m :
mem
b :
Z
reg :
region
o :
Z
x :
ptr
Hlv :
live_atm b reg
Hax :
agree_piecem PAuxb o VAuxptr_capx
Hcl :
all_agreem cellb o ptr_addrx
Hr :
0 ≤ ptr_addrx < 2 ^ 64
Hf :
¬freed_inm_regionsm ptr_capx
⊢
ptr_addrx mod 2 ^ 64 = ptr_addrx
deferred goal
m :
mem
b :
Z
reg :
region
o :
Z
x :
ptr
Hlv :
live_atm b reg
Hax :
agree_piecem PAuxb o VAuxptr_capx
Hcl :
all_agreem cellb o ptr_addrx
Hr :
0 ≤ ptr_addrx < 2 ^ 64
Hf :
¬freed_inm_regionsm ptr_capx
⊢
m_auxm b + o = ptr_capx

apply Z.mod_small

2 open

m :
mem
b :
Z
reg :
region
o :
Z
x :
ptr
Hlv :
live_atm b reg
Hax :
agree_piecem PAuxb o VAuxptr_capx
Hcl :
all_agreem cellb o ptr_addrx
Hr :
0 ≤ ptr_addrx < 2 ^ 64
Hf :
¬freed_inm_regionsm ptr_capx
⊢
0 ≤ ptr_addrx < 2 ^ 64
deferred goal
m :
mem
b :
Z
reg :
region
o :
Z
x :
ptr
Hlv :
live_atm b reg
Hax :
agree_piecem PAuxb o VAuxptr_capx
Hcl :
all_agreem cellb o ptr_addrx
Hr :
0 ≤ ptr_addrx < 2 ^ 64
Hf :
¬freed_inm_regionsm ptr_capx
⊢
m_auxm b + o = ptr_capx

exact Hr

deferred goal
m :
mem
b :
Z
reg :
region
o :
Z
x :
ptr
Hlv :
live_atm b reg
Hax :
agree_piecem PAuxb o VAuxptr_capx
Hcl :
all_agreem cellb o ptr_addrx
Hr :
0 ≤ ptr_addrx < 2 ^ 64
Hf :
¬freed_inm_regionsm ptr_capx
⊢
m_auxm b + o = ptr_capx

–destruct cell_bounds_ _ _ _ _ Hlv Hcl as Ho He

m :
mem
b :
Z
reg :
region
o :
Z
x :
ptr
Hlv :
live_atm b reg
Hax :
agree_piecem PAuxb o VAuxptr_capx
Hcl :
all_agreem cellb o ptr_addrx
Hr :
0 ≤ ptr_addrx < 2 ^ 64
Hf :
¬freed_inm_regionsm ptr_capx
Ho :
0 ≤ o
He :
b + o + 8 ≤ r_endreg
⊢
m_auxm b + o = ptr_capx

apply aux_holds_kept ; exact aux_piece_holds_ _ _ _ _ Hlv Hax | exact Hf

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros Hlv Hax Hcl Hr Hf
split ; exact Hr |
split
–rewrite cell_loadm b reg o ptr_addrx b + o Hlv Hcl eq_refl
apply Z.mod_small
exact Hr
–destruct cell_bounds_ _ _ _ _ Hlv Hcl as Ho He
apply aux_holds_kept ; exact aux_piece_holds_ _ _ _ _ Hlv Hax | exact Hf

Reading getopt's cells over any runtime R and Logic instance.

82Module GetoptLogicOn R : Runtime LG0 : LogicSigR
83Module LG ≔ LG0
84Module L ≔ LG.L
Import L LG
87Section getopt
88Context `{!invGS_genhlc Σ, !gen_heapGSpiece pval Σ}
89Context world : Type registry : name → optioncontractworld wi : mem → world → gmappiece pval → Prop `{!SafepointStablewi} ge : genv

The Iris instance of the registry and wi.

93Instance getopt_irisGS: irisGS_genhlc nanofil_langregistry ge Σ ≔
nanofil_irisGSregistry wi ge

The expressions of the language.

97Notation gexpr ≔ language.exprnanofil_langregistry ge

The world's getopt state, through the projection view, is in the memory at the cells optarg_cell and optind_cell, whose addresses are words, and the getopt token is current.

102Context view : world → getopt_world
102Context optarg_cell optind_cell : ptr
102Context Hcells : 0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
102Context Hgetopt_wi : ∀m w h, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h

The check of optarg's cell for an 8-byte read passes.

109Lemma wp_optarg_check
∀ f e ls l d args rest j classes Φ
op_arg_classesCheck0 8 Read 8 A = Someclasses
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
▷WPERunmkFramef putd WPtroptarg_cell e ls None Execl rest j : gexpr {Φ} −∗ WPERunmkFramef e ls None Execl Letd A Check0 8 Read 8 args :: rest j : gexpr {Φ}
Explore proof 16 tactics

Initial goal

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
⊢
op_arg_classesCheck0 8 Read 8 A = Someclasses → map2_optionvalue_xge e classes args = SomeWPtroptarg_cell → ▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j : gexpr {v. Φv} −∗ WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd A Check0 8 Read 8 args :: rest j : gexpr {v. Φv}

intros Hc Hx

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
⊢
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j : gexpr {v. Φv} −∗ WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd A Check0 8 Read 8 args :: rest j : gexpr {v. Φv}

iIntros HK

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd A Check0 8 Read 8 args :: rest j {v. Φv}

iAssert pts[ ] as Hn ; rewrite / pts ; done |

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd A Check0 8 Read 8 args :: rest j {v. Φv}

iApply wp_world_let_withregistry wi ge [ ] with Hn [HK] ; reflexivity | exact Hc | exact Hx | |

3 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
⊢
∀m : mem w : world h : gmappiece pval, wim w h → ∀l0 : piece v : pval, l0, v ∈ [ ] → h !! l0 = Somev → op_resCheck0 8 Read 8 A WPtroptarg_cell m = SomeOpResRVal?Goal m
focused goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd ?Goal e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
shelved goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
⊢
word

–intros m w h Hw _

3 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
⊢
op_resCheck0 8 Read 8 A WPtroptarg_cell m = SomeOpResRVal?Goal m
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd ?Goal e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
shelved goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
⊢
word

destruct Hgetopt_wi_ _ _ Hw as Hpc & _ & Hoc & _ & _

3 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hpc :
exposed_pointer_cellm getopt_optarg_cellvieww getopt_optargvieww
Hoc :
getopt_optarg_cellvieww = optarg_cell
⊢
op_resCheck0 8 Read 8 A WPtroptarg_cell m = SomeOpResRVal?Goal m
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd ?Goal e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
shelved goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
⊢
word

apply op_check

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hpc :
exposed_pointer_cellm getopt_optarg_cellvieww getopt_optargvieww
Hoc :
getopt_optarg_cellvieww = optarg_cell
⊢
access_resm raw_addressptr_addroptarg_cell 0 ptr_capoptarg_cell 8 − 0 Read 8 = Someok
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

unfold raw_address

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hpc :
exposed_pointer_cellm getopt_optarg_cellvieww getopt_optargvieww
Hoc :
getopt_optarg_cellvieww = optarg_cell
⊢
access_resm ptr_addroptarg_cell + 0 mod 2 ^ 64 ptr_capoptarg_cell 8 − 0 Read 8 = Someok
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

rewrite Z.add_0_r Z.mod_small ; | lia

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hpc :
exposed_pointer_cellm getopt_optarg_cellvieww getopt_optargvieww
Hoc :
getopt_optarg_cellvieww = optarg_cell
⊢
access_resm ptr_addroptarg_cell ptr_capoptarg_cell 8 − 0 Read 8 = Someok
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

cbn

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hpc :
exposed_pointer_cellm getopt_optarg_cellvieww getopt_optargvieww
Hoc :
getopt_optarg_cellvieww = optarg_cell
⊢
access_resm ptr_addroptarg_cell ptr_capoptarg_cell 8 − 0 Read 8 = Someok
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

destruct Hpc as _ & Hacc & _

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hacc :
access_resm ptr_addrgetopt_optarg_cellvieww ptr_capgetopt_optarg_cellvieww 8 Read 8 = Someok
Hoc :
getopt_optarg_cellvieww = optarg_cell
⊢
access_resm ptr_addroptarg_cell ptr_capoptarg_cell 8 − 0 Read 8 = Someok
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

rewrite Hoc in Hacc

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hacc :
access_resm ptr_addroptarg_cell ptr_capoptarg_cell 8 Read 8 = Someok
⊢
access_resm ptr_addroptarg_cell ptr_capoptarg_cell 8 − 0 Read 8 = Someok
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

exact Hacc

deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

–iNext

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
Hn :
pts[ ]
□
HK :
WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

iIntros _

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 8 Read 8 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
Hn :
pts[ ]
□
HK :
WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptarg_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

iExact HK

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros Hc Hx
iIntros HK
iAssert pts[ ] as Hn ; rewrite / pts ; done |
iApply wp_world_let_withregistry wi ge [ ] with Hn [HK] ; reflexivity | exact Hc | exact Hx | |
–intros m w h Hw _
destruct Hgetopt_wi_ _ _ Hw as Hpc & _ & Hoc & _ & _
apply op_check
unfold raw_address
rewrite Z.add_0_r Z.mod_small ; | lia
cbn
destruct Hpc as _ & Hacc & _
rewrite Hoc in Hacc
exact Hacc
–iNext
iIntros _
iExact HK

The plain pointer load of optarg's cell: optarg a, as the token names it.

126Lemma wp_optarg_load
∀ f e ls l d args rest j classes a i Φ
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
ptsgetopt_psa i −∗ ▷ptsgetopt_psa i −∗ WPERunmkFramef putd WPtra e ls None Execl rest j : gexpr {Φ} −∗ WPERunmkFramef e ls None Execl Letd P RawLoadPointer0 AuxRead; LowerResolve; AddressRead args :: rest j : gexpr {Φ}
Explore proof 16 tactics

Initial goal

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
⊢
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses → map2_optionvalue_xge e classes args = SomeWPtroptarg_cell → ptsgetopt_psa i −∗ ▷ptsgetopt_psa i −∗ WPERunfr_fn ≔ f; fr_env ≔ putd WPtra e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j : gexpr {v. Φv} −∗ WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd P RawLoadPointer0 AuxRead; LowerResolve; AddressRead args :: rest j : gexpr {v. Φv}

intros Hc Hx

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
⊢
ptsgetopt_psa i −∗ ▷ptsgetopt_psa i −∗ WPERunfr_fn ≔ f; fr_env ≔ putd WPtra e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j : gexpr {v. Φv} −∗ WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd P RawLoadPointer0 AuxRead; LowerResolve; AddressRead args :: rest j : gexpr {v. Φv}

iIntros Ht HK

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
Ht :
ptsgetopt_psa i
HK :
▷ptsgetopt_psa i −∗ WPERunfr_fn ≔ f; fr_env ≔ putd WPtra e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd P RawLoadPointer0 AuxRead; LowerResolve; AddressRead args :: rest j {v. Φv}

iApply wp_world_let_with with Ht HK ; reflexivity | exact Hc | exact Hx |

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
⊢
∀m : mem w : world h : gmappiece pval, wim w h → ∀l0 : piece v : pval, l0, v ∈ getopt_psa i → h !! l0 = Somev → op_resRawLoadPointer0 AuxRead; LowerResolve; AddressRead P WPtroptarg_cell m = SomeOpResRValWPtra m

intros m w h Hw Hl

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
⊢
op_resRawLoadPointer0 AuxRead; LowerResolve; AddressRead P WPtroptarg_cell m = SomeOpResRValWPtra m

destruct Hgetopt_wi_ _ _ Hw as Hpc & _ & Hoc & _ & Hcur

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hpc :
exposed_pointer_cellm getopt_optarg_cellvieww getopt_optargvieww
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
⊢
op_resRawLoadPointer0 AuxRead; LowerResolve; AddressRead P WPtroptarg_cell m = SomeOpResRValWPtra m

destruct Hcura i Hl_ _ ltac:left as Ha _

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hpc :
exposed_pointer_cellm getopt_optarg_cellvieww getopt_optargvieww
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
Ha :
getopt_optargvieww = a
⊢
op_resRawLoadPointer0 AuxRead; LowerResolve; AddressRead P WPtroptarg_cell m = SomeOpResRValWPtra m

rewrite Hoc Ha in Hpc

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
Ha :
getopt_optargvieww = a
Hpc :
exposed_pointer_cellm optarg_cell a
⊢
op_resRawLoadPointer0 AuxRead; LowerResolve; AddressRead P WPtroptarg_cell m = SomeOpResRValWPtra m

assert Er : raw_addressptr_addroptarg_cell 0 = ptr_addroptarg_cell

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
Ha :
getopt_optargvieww = a
Hpc :
exposed_pointer_cellm optarg_cell a
⊢
raw_addressptr_addroptarg_cell 0 = ptr_addroptarg_cell
focused goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
Ha :
getopt_optargvieww = a
Hpc :
exposed_pointer_cellm optarg_cell a
Er :
raw_addressptr_addroptarg_cell 0 = ptr_addroptarg_cell
⊢
op_resRawLoadPointer0 AuxRead; LowerResolve; AddressRead P WPtroptarg_cell m = SomeOpResRValWPtra m

{unfold raw_address

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
Ha :
getopt_optargvieww = a
Hpc :
exposed_pointer_cellm optarg_cell a
⊢
ptr_addroptarg_cell + 0 mod 2 ^ 64 = ptr_addroptarg_cell
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
Ha :
getopt_optargvieww = a
Hpc :
exposed_pointer_cellm optarg_cell a
Er :
raw_addressptr_addroptarg_cell 0 = ptr_addroptarg_cell
⊢
op_resRawLoadPointer0 AuxRead; LowerResolve; AddressRead P WPtroptarg_cell m = SomeOpResRValWPtra m

rewrite Z.add_0_r

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
Ha :
getopt_optargvieww = a
Hpc :
exposed_pointer_cellm optarg_cell a
⊢
ptr_addroptarg_cell mod 2 ^ 64 = ptr_addroptarg_cell
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
Ha :
getopt_optargvieww = a
Hpc :
exposed_pointer_cellm optarg_cell a
Er :
raw_addressptr_addroptarg_cell 0 = ptr_addroptarg_cell
⊢
op_resRawLoadPointer0 AuxRead; LowerResolve; AddressRead P WPtroptarg_cell m = SomeOpResRValWPtra m

apply Z.mod_small

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
Ha :
getopt_optargvieww = a
Hpc :
exposed_pointer_cellm optarg_cell a
⊢
0 ≤ ptr_addroptarg_cell < 2 ^ 64
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
Ha :
getopt_optargvieww = a
Hpc :
exposed_pointer_cellm optarg_cell a
Er :
raw_addressptr_addroptarg_cell 0 = ptr_addroptarg_cell
⊢
op_resRawLoadPointer0 AuxRead; LowerResolve; AddressRead P WPtroptarg_cell m = SomeOpResRValWPtra m

lia

deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
Ha :
getopt_optargvieww = a
Hpc :
exposed_pointer_cellm optarg_cell a
Er :
raw_addressptr_addroptarg_cell 0 = ptr_addroptarg_cell
⊢
op_resRawLoadPointer0 AuxRead; LowerResolve; AddressRead P WPtroptarg_cell m = SomeOpResRValWPtra m

apply op_raw_load_pointer ; rewrite Er

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
Ha :
getopt_optargvieww = a
Hpc :
exposed_pointer_cellm optarg_cell a
Er :
raw_addressptr_addroptarg_cell 0 = ptr_addroptarg_cell
⊢
access_resm ptr_addroptarg_cell ptr_capoptarg_cell 8 Read 8 = Someok
focused goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
Ha :
getopt_optargvieww = a
Hpc :
exposed_pointer_cellm optarg_cell a
Er :
raw_addressptr_addroptarg_cell 0 = ptr_addroptarg_cell
⊢
pointer_load_effectsm ptr_addroptarg_cell AuxRead; LowerResolve; AddressRead = Somea

–destruct Hpc as _ & Hacc & _

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
Ha :
getopt_optargvieww = a
Hacc :
access_resm ptr_addroptarg_cell ptr_capoptarg_cell 8 Read 8 = Someok
Er :
raw_addressptr_addroptarg_cell 0 = ptr_addroptarg_cell
⊢
access_resm ptr_addroptarg_cell ptr_capoptarg_cell 8 Read 8 = Someok
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
Ha :
getopt_optargvieww = a
Hpc :
exposed_pointer_cellm optarg_cell a
Er :
raw_addressptr_addroptarg_cell 0 = ptr_addroptarg_cell
⊢
pointer_load_effectsm ptr_addroptarg_cell AuxRead; LowerResolve; AddressRead = Somea

exact Hacc

deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadPointer0 AuxRead; LowerResolve; AddressRead P = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptarg_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optarg_cellvieww = optarg_cell
Hcur :
getopt_currentvieww h
Ha :
getopt_optargvieww = a
Hpc :
exposed_pointer_cellm optarg_cell a
Er :
raw_addressptr_addroptarg_cell 0 = ptr_addroptarg_cell
⊢
pointer_load_effectsm ptr_addroptarg_cell AuxRead; LowerResolve; AddressRead = Somea

–exact exposed_pointer_load_ _ _ Hpc

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros Hc Hx
iIntros Ht HK
iApply wp_world_let_with with Ht HK ; reflexivity | exact Hc | exact Hx |
intros m w h Hw Hl
destruct Hgetopt_wi_ _ _ Hw as Hpc & _ & Hoc & _ & Hcur
destruct Hcura i Hl_ _ ltac:left as Ha _
rewrite Hoc Ha in Hpc
assert Er : raw_addressptr_addroptarg_cell 0 = ptr_addroptarg_cell
{unfold raw_address
rewrite Z.add_0_r
apply Z.mod_small
lia
apply op_raw_load_pointer ; rewrite Er
–destruct Hpc as _ & Hacc & _
exact Hacc
–exact exposed_pointer_load_ _ _ Hpc

The check of optind's cell for a 4-byte read at alignment 1 passes.

149Lemma wp_optind_check
∀ f e ls l d args rest j classes Φ
op_arg_classesCheck0 4 Read 1 A = Someclasses
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
▷WPERunmkFramef putd WPtroptind_cell e ls None Execl rest j : gexpr {Φ} −∗ WPERunmkFramef e ls None Execl Letd A Check0 4 Read 1 args :: rest j : gexpr {Φ}
Explore proof 16 tactics

Initial goal

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
⊢
op_arg_classesCheck0 4 Read 1 A = Someclasses → map2_optionvalue_xge e classes args = SomeWPtroptind_cell → ▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j : gexpr {v. Φv} −∗ WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd A Check0 4 Read 1 args :: rest j : gexpr {v. Φv}

intros Hc Hx

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
⊢
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j : gexpr {v. Φv} −∗ WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd A Check0 4 Read 1 args :: rest j : gexpr {v. Φv}

iIntros HK

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd A Check0 4 Read 1 args :: rest j {v. Φv}

iAssert pts[ ] as Hn ; rewrite / pts ; done |

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd A Check0 4 Read 1 args :: rest j {v. Φv}

iApply wp_world_let_withregistry wi ge [ ] with Hn [HK] ; reflexivity | exact Hc | exact Hx | |

3 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
⊢
∀m : mem w : world h : gmappiece pval, wim w h → ∀l0 : piece v : pval, l0, v ∈ [ ] → h !! l0 = Somev → op_resCheck0 4 Read 1 A WPtroptind_cell m = SomeOpResRVal?Goal m
focused goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd ?Goal e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
shelved goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
⊢
word

–intros m w h Hw _

3 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
⊢
op_resCheck0 4 Read 1 A WPtroptind_cell m = SomeOpResRVal?Goal m
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd ?Goal e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
shelved goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
⊢
word

destruct Hgetopt_wi_ _ _ Hw as _ & Hic & _ & _ & Hoc & _

3 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hic :
getopt_int_cellm getopt_optind_cellvieww getopt_optindvieww
Hoc :
getopt_optind_cellvieww = optind_cell
⊢
op_resCheck0 4 Read 1 A WPtroptind_cell m = SomeOpResRVal?Goal m
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd ?Goal e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
shelved goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
⊢
word

apply op_check

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hic :
getopt_int_cellm getopt_optind_cellvieww getopt_optindvieww
Hoc :
getopt_optind_cellvieww = optind_cell
⊢
access_resm raw_addressptr_addroptind_cell 0 ptr_capoptind_cell 4 − 0 Read 1 = Someok
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

unfold raw_address

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hic :
getopt_int_cellm getopt_optind_cellvieww getopt_optindvieww
Hoc :
getopt_optind_cellvieww = optind_cell
⊢
access_resm ptr_addroptind_cell + 0 mod 2 ^ 64 ptr_capoptind_cell 4 − 0 Read 1 = Someok
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

rewrite Z.add_0_r Z.mod_small ; | lia

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hic :
getopt_int_cellm getopt_optind_cellvieww getopt_optindvieww
Hoc :
getopt_optind_cellvieww = optind_cell
⊢
access_resm ptr_addroptind_cell ptr_capoptind_cell 4 − 0 Read 1 = Someok
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

cbn

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hic :
getopt_int_cellm getopt_optind_cellvieww getopt_optindvieww
Hoc :
getopt_optind_cellvieww = optind_cell
⊢
access_resm ptr_addroptind_cell ptr_capoptind_cell 4 − 0 Read 1 = Someok
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

destruct Hic as _ & _ & Hacc & _

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hacc :
access_resm ptr_addrgetopt_optind_cellvieww ptr_capgetopt_optind_cellvieww 4 Read 4 = Someok
Hoc :
getopt_optind_cellvieww = optind_cell
⊢
access_resm ptr_addroptind_cell ptr_capoptind_cell 4 − 0 Read 1 = Someok
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

rewrite Hoc in Hacc

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hoc :
getopt_optind_cellvieww = optind_cell
Hacc :
access_resm ptr_addroptind_cell ptr_capoptind_cell 4 Read 4 = Someok
⊢
access_resm ptr_addroptind_cell ptr_capoptind_cell 4 − 0 Read 1 = Someok
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

exact access_read_align1_ _ _ _ _ Hacc

deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
Hn :
pts[ ]
□
HK :
▷WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
▷pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

–iNext

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
Hn :
pts[ ]
□
HK :
WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
pts[ ] −∗ WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

iIntros _

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesCheck0 4 Read 1 A = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
Hn :
pts[ ]
□
HK :
WPERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
WPL.ERunfr_fn ≔ f; fr_env ≔ putd WPtroptind_cell e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}

iExact HK

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros Hc Hx
iIntros HK
iAssert pts[ ] as Hn ; rewrite / pts ; done |
iApply wp_world_let_withregistry wi ge [ ] with Hn [HK] ; reflexivity | exact Hc | exact Hx | |
–intros m w h Hw _
destruct Hgetopt_wi_ _ _ Hw as _ & Hic & _ & _ & Hoc & _
apply op_check
unfold raw_address
rewrite Z.add_0_r Z.mod_small ; | lia
cbn
destruct Hic as _ & _ & Hacc & _
rewrite Hoc in Hacc
exact access_read_align1_ _ _ _ _ Hacc
–iNext
iIntros _
iExact HK

The signed 32-bit load of optind's cell: optind i, as the token names it, as a W word.

166Lemma wp_optind_load
∀ f e ls l d args rest j classes a i Φ
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
ptsgetopt_psa i −∗ ▷ptsgetopt_psa i −∗ WPERunmkFramef putd WInti mod 2 ^ 32 e ls None Execl rest j : gexpr {Φ} −∗ WPERunmkFramef e ls None Execl Letd W RawLoadLdNarrowSw 0 args :: rest j : gexpr {Φ}
Explore proof 15 tactics

Initial goal

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
⊢
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses → map2_optionvalue_xge e classes args = SomeWPtroptind_cell → ptsgetopt_psa i −∗ ▷ptsgetopt_psa i −∗ WPERunfr_fn ≔ f; fr_env ≔ putd WInti mod 2 ^ 32 e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j : gexpr {v. Φv} −∗ WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd W RawLoadLdNarrowSw 0 args :: rest j : gexpr {v. Φv}

intros Hc Hx

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
⊢
ptsgetopt_psa i −∗ ▷ptsgetopt_psa i −∗ WPERunfr_fn ≔ f; fr_env ≔ putd WInti mod 2 ^ 32 e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j : gexpr {v. Φv} −∗ WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd W RawLoadLdNarrowSw 0 args :: rest j : gexpr {v. Φv}

iIntros Ht HK

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
Ht :
ptsgetopt_psa i
HK :
▷ptsgetopt_psa i −∗ WPERunfr_fn ≔ f; fr_env ≔ putd WInti mod 2 ^ 32 e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl rest j {v. Φv}
∗
WPERunfr_fn ≔ f; fr_env ≔ e; fr_locals ≔ ls; fr_doomed ≔ None; fr_at ≔ Execl Letd W RawLoadLdNarrowSw 0 args :: rest j {v. Φv}

iApply wp_world_let_with with Ht HK ; reflexivity | exact Hc | exact Hx |

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
⊢
∀m : mem w : world h : gmappiece pval, wim w h → ∀l0 : piece v : pval, l0, v ∈ getopt_psa i → h !! l0 = Somev → op_resRawLoadLdNarrowSw 0 W WPtroptind_cell m = SomeOpResRValWInti mod 2 ^ 32 m

intros m w h Hw Hl

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
⊢
op_resRawLoadLdNarrowSw 0 W WPtroptind_cell m = SomeOpResRValWInti mod 2 ^ 32 m

destruct Hgetopt_wi_ _ _ Hw as _ & Hic & _ & _ & Hoc & Hcur

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hic :
getopt_int_cellm getopt_optind_cellvieww getopt_optindvieww
Hoc :
getopt_optind_cellvieww = optind_cell
Hcur :
getopt_currentvieww h
⊢
op_resRawLoadLdNarrowSw 0 W WPtroptind_cell m = SomeOpResRValWInti mod 2 ^ 32 m

destruct Hcura i Hl_ _ ltac:left as _ Hi

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hic :
getopt_int_cellm getopt_optind_cellvieww getopt_optindvieww
Hoc :
getopt_optind_cellvieww = optind_cell
Hcur :
getopt_currentvieww h
Hi :
getopt_optindvieww = i
⊢
op_resRawLoadLdNarrowSw 0 W WPtroptind_cell m = SomeOpResRValWInti mod 2 ^ 32 m

rewrite Hoc Hi in Hic

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optind_cellvieww = optind_cell
Hcur :
getopt_currentvieww h
Hi :
getopt_optindvieww = i
Hic :
getopt_int_cellm optind_cell i
⊢
op_resRawLoadLdNarrowSw 0 W WPtroptind_cell m = SomeOpResRValWInti mod 2 ^ 32 m

destruct Hic as _ & _ & Hacc & _ & Hload

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optind_cellvieww = optind_cell
Hcur :
getopt_currentvieww h
Hi :
getopt_optindvieww = i
Hacc :
access_resm ptr_addroptind_cell ptr_capoptind_cell 4 Read 4 = Someok
Hload :
load_bytesm ptr_addroptind_cell 4 = i mod 2 ^ 32
⊢
op_resRawLoadLdNarrowSw 0 W WPtroptind_cell m = SomeOpResRValWInti mod 2 ^ 32 m

assert Er : raw_addressptr_addroptind_cell 0 = ptr_addroptind_cell

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optind_cellvieww = optind_cell
Hcur :
getopt_currentvieww h
Hi :
getopt_optindvieww = i
Hacc :
access_resm ptr_addroptind_cell ptr_capoptind_cell 4 Read 4 = Someok
Hload :
load_bytesm ptr_addroptind_cell 4 = i mod 2 ^ 32
⊢
raw_addressptr_addroptind_cell 0 = ptr_addroptind_cell
focused goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optind_cellvieww = optind_cell
Hcur :
getopt_currentvieww h
Hi :
getopt_optindvieww = i
Hacc :
access_resm ptr_addroptind_cell ptr_capoptind_cell 4 Read 4 = Someok
Hload :
load_bytesm ptr_addroptind_cell 4 = i mod 2 ^ 32
Er :
raw_addressptr_addroptind_cell 0 = ptr_addroptind_cell
⊢
op_resRawLoadLdNarrowSw 0 W WPtroptind_cell m = SomeOpResRValWInti mod 2 ^ 32 m

{unfold raw_address

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optind_cellvieww = optind_cell
Hcur :
getopt_currentvieww h
Hi :
getopt_optindvieww = i
Hacc :
access_resm ptr_addroptind_cell ptr_capoptind_cell 4 Read 4 = Someok
Hload :
load_bytesm ptr_addroptind_cell 4 = i mod 2 ^ 32
⊢
ptr_addroptind_cell + 0 mod 2 ^ 64 = ptr_addroptind_cell
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optind_cellvieww = optind_cell
Hcur :
getopt_currentvieww h
Hi :
getopt_optindvieww = i
Hacc :
access_resm ptr_addroptind_cell ptr_capoptind_cell 4 Read 4 = Someok
Hload :
load_bytesm ptr_addroptind_cell 4 = i mod 2 ^ 32
Er :
raw_addressptr_addroptind_cell 0 = ptr_addroptind_cell
⊢
op_resRawLoadLdNarrowSw 0 W WPtroptind_cell m = SomeOpResRValWInti mod 2 ^ 32 m

rewrite Z.add_0_r

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optind_cellvieww = optind_cell
Hcur :
getopt_currentvieww h
Hi :
getopt_optindvieww = i
Hacc :
access_resm ptr_addroptind_cell ptr_capoptind_cell 4 Read 4 = Someok
Hload :
load_bytesm ptr_addroptind_cell 4 = i mod 2 ^ 32
⊢
ptr_addroptind_cell mod 2 ^ 64 = ptr_addroptind_cell
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optind_cellvieww = optind_cell
Hcur :
getopt_currentvieww h
Hi :
getopt_optindvieww = i
Hacc :
access_resm ptr_addroptind_cell ptr_capoptind_cell 4 Read 4 = Someok
Hload :
load_bytesm ptr_addroptind_cell 4 = i mod 2 ^ 32
Er :
raw_addressptr_addroptind_cell 0 = ptr_addroptind_cell
⊢
op_resRawLoadLdNarrowSw 0 W WPtroptind_cell m = SomeOpResRValWInti mod 2 ^ 32 m

apply Z.mod_small

2 open

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optind_cellvieww = optind_cell
Hcur :
getopt_currentvieww h
Hi :
getopt_optindvieww = i
Hacc :
access_resm ptr_addroptind_cell ptr_capoptind_cell 4 Read 4 = Someok
Hload :
load_bytesm ptr_addroptind_cell 4 = i mod 2 ^ 32
⊢
0 ≤ ptr_addroptind_cell < 2 ^ 64
deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optind_cellvieww = optind_cell
Hcur :
getopt_currentvieww h
Hi :
getopt_optindvieww = i
Hacc :
access_resm ptr_addroptind_cell ptr_capoptind_cell 4 Read 4 = Someok
Hload :
load_bytesm ptr_addroptind_cell 4 = i mod 2 ^ 32
Er :
raw_addressptr_addroptind_cell 0 = ptr_addroptind_cell
⊢
op_resRawLoadLdNarrowSw 0 W WPtroptind_cell m = SomeOpResRValWInti mod 2 ^ 32 m

lia

deferred goal
hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optind_cellvieww = optind_cell
Hcur :
getopt_currentvieww h
Hi :
getopt_optindvieww = i
Hacc :
access_resm ptr_addroptind_cell ptr_capoptind_cell 4 Read 4 = Someok
Hload :
load_bytesm ptr_addroptind_cell 4 = i mod 2 ^ 32
Er :
raw_addressptr_addroptind_cell 0 = ptr_addroptind_cell
⊢
op_resRawLoadLdNarrowSw 0 W WPtroptind_cell m = SomeOpResRValWInti mod 2 ^ 32 m

rewrite op_raw_load_sw ; rewrite Er ; | exact access_read_align1_ _ _ _ _ Hacc

hlc :
has_lc
Σ :
gFunctors
invGS_gen0 :
invGS_genhlc Σ
gen_heapGS0 :
gen_heapGSpiece pval Σ
world :
Type
registry :
name → optioncontractworld
wi :
mem → world → gmappiece pval → Prop
SafepointStable0 :
SafepointStablewi
ge :
genv
view :
world → getopt_world
optarg_cell, optind_cell :
ptr
Hcells :
0 ≤ ptr_addroptarg_cell < 2 ^ 64 ∧ 0 ≤ ptr_addroptind_cell < 2 ^ 64
Hgetopt_wi :
∀m : mem w : world h : gmappiece pval, wim w h → getopt_state_atm vieww ∧ getopt_optarg_cellvieww = optarg_cell ∧ getopt_optind_cellvieww = optind_cell ∧ getopt_currentvieww h
f :
func
e :
env
ls :
listname × optionZ
l, d :
name
args :
listvalue
rest :
listinst
j :
jump
classes :
listclass
a :
ptr
i :
Z
Φ :
valnanofil_langregistry ge → iPropIΣ
Hc :
op_arg_classesRawLoadLdNarrowSw 0 W = Someclasses
Hx :
map2_optionvalue_xge e classes args = SomeWPtroptind_cell
m :
mem
w :
world
h :
gmappiece pval
Hw :
wim w h
Hl :
∀l : piece v : pval, l, v ∈ getopt_psa i → h !! l = Somev
Hoc :
getopt_optind_cellvieww = optind_cell
Hcur :
getopt_currentvieww h
Hi :
getopt_optindvieww = i
Hacc :
access_resm ptr_addroptind_cell ptr_capoptind_cell 4 Read 4 = Someok
Hload :
load_bytesm ptr_addroptind_cell 4 = i mod 2 ^ 32
Er :
raw_addressptr_addroptind_cell 0 = ptr_addroptind_cell
⊢
SomeOpResRValWIntload_bytesm ptr_addroptind_cell 4 mod 2 ^ 32 m = SomeOpResRValWInti mod 2 ^ 32 m

rewrite Hload Z.mod_mod ; reflexivity | lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros Hc Hx
iIntros Ht HK
iApply wp_world_let_with with Ht HK ; reflexivity | exact Hc | exact Hx |
intros m w h Hw Hl
destruct Hgetopt_wi_ _ _ Hw as _ & Hic & _ & _ & Hoc & Hcur
destruct Hcura i Hl_ _ ltac:left as _ Hi
rewrite Hoc Hi in Hic
destruct Hic as _ & _ & Hacc & _ & Hload
assert Er : raw_addressptr_addroptind_cell 0 = ptr_addroptind_cell
{unfold raw_address
rewrite Z.add_0_r
apply Z.mod_small
lia
rewrite op_raw_load_sw ; rewrite Er ; | exact access_read_align1_ _ _ _ _ Hacc
rewrite Hload Z.mod_mod ; reflexivity | lia