rocq/spikes/IrisLang.v

Spike: nanofil's core machine as an Iris language, and Iris adequacy as a proof of never_panics.

An expression is a configuration less its memory (EConf: the running frame, the suspended callers and the fuel) or a finished run (EEnd: an outcome, which is also the value). The Iris state is the memory with the runtime's state. A primitive step is a step of Machine.v's mstep from a configuration that does not fails, a refused allocation (which ends in a refusal trap), or an ending that is not a failure. A failing configuration is therefore never reducible, so a weakest precondition with NotStuck for the entry call rules out every failure; wp_never_panics proves that Panics.v's never_panics follows from such a weakest precondition, for every fuel.

From iris.proofmode Require Import proofmode

From iris.program_logic Require Import language weakestpre adequacy

From Stdlib Require Import ZArith Relations

From Nanofil Require Import Term Syntax Values Memory Runtime Ops Semantics Run Machine Panics

21Module IrisMachine R : Runtime

22Module P ≔ Panics R

23Module RM ≔ P.RM

An expression: a configuration without its memory (the frame, the callers and the fuel), or the outcome a run ended with.

27Inductive expr: Type ≔

\|	EConf	fr : frame callers : listframe × pending fuel : Z
\|	EEnd	o : outcome

The Iris state: the memory and the runtime's state.

32Definition nstate: Type ≔

mem × R.state%type

A value is an outcome, written as the ended expression.

35Definition of_valo : outcome : expr ≔

EEndo

The outcome of an ended expression; None for a configuration.

38Definition to_vale : expr : optionoutcome ≔

match e with

EEndo

⇒

Someo

EConf_ _ _

⇒

None

The expression of the configuration c.

42Definition conf_exprc : config : expr ≔

EConfc_framec c_callersc c_fuelc

A primitive step in the genv ge, with no observations and no forks:

ps_machine: a machine step of a configuration that does not fails (a failing configuration may have a safepoint due, and must still not count as reducible);
ps_refused: an allocation R refuses ends the run with the refusal trap OutOfMemory;
ps_done: an ending that is not a failure.

51Inductive prim_stepge : genv : expr → nstate → listunit → expr → nstate → listexpr → Prop ≔

∀ fr callers fuel m s c′ s′

¬failsge mkConfigfr callers m fuel

RM.mstepge mkConfigfr callers m fuel, s c′, s′

ps_machine

prim_stepge EConffr callers fuel m, s [ ] conf_exprc′ c_memc′, s′ [ ]

∀ fr callers fuel m s q k

Semantics.stepge mkConfigfr callers m fuel = Freshq k

0 ≤ req_extentq%Z

R.allocs q = None

ps_refused

prim_stepge EConffr callers fuel m, s [ ] EEndTrapOutOfMemory m, s [ ]

∀ fr callers fuel m s o

Semantics.stepge mkConfigfr callers m fuel = Doneo

¬failureo

ps_done

prim_stepge EConffr callers fuel m, s [ ] EEndo m, s [ ]

The language laws: values round-trip, and a value takes no step.

67Lemma nanofil_lang_mixin

∀ ge : genv

LanguageMixinof_val to_val prim_stepge

Explore proof 6 tactics

Initial goal

ge :

genv

⊢

LanguageMixinof_val to_val prim_stepge

split

3 open

ge :

genv

⊢

∀v : outcome, to_valof_valv = Somev

focused goal

ge :

genv

⊢

∀e : expr v : outcome, to_vale = Somev → of_valv = e

focused goal

ge :

genv

⊢

∀e : expr σ : nstate κ : list() e′ : expr σ′ : nstate efs : listexpr, prim_stepge e σ κ e′ σ′ efs → to_vale = None

–reflexivity

2 open

deferred goal

ge :

genv

⊢

∀e : expr v : outcome, to_vale = Somev → of_valv = e

deferred goal

ge :

genv

⊢

∀e : expr σ : nstate κ : list() e′ : expr σ′ : nstate efs : listexpr, prim_stepge e σ κ e′ σ′ efs → to_vale = None

–intros e o H

2 open

ge :

genv

e :

expr

o :

outcome

H :

to_vale = Someo

⊢

of_valo = e

deferred goal

ge :

genv

⊢

∀e : expr σ : nstate κ : list() e′ : expr σ′ : nstate efs : listexpr, prim_stepge e σ κ e′ σ′ efs → to_vale = None

destruct e ; inversion H ; reflexivity

deferred goal

ge :

genv

⊢

∀e : expr σ : nstate κ : list() e′ : expr σ′ : nstate efs : listexpr, prim_stepge e σ κ e′ σ′ efs → to_vale = None

–intros e σ κ e′ σ′ efs H

ge :

genv

e :

expr

σ :

nstate

κ :

list()

e′ :

expr

σ′ :

nstate

efs :

listexpr

H :

prim_stepge e σ κ e′ σ′ efs

⊢

to_vale = None

destruct H ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

split

–reflexivity

–intros e o H

destruct e ; inversion H ; reflexivity

–intros e σ κ e′ σ′ efs H

destruct H ; reflexivity

Nanofil's core machine in the genv ge as an Iris language.

76Canonical Structure nanofil_langge : genv : language ≔

Languagenanofil_lang_mixinge

A configuration is its parts put back together.

80Lemma config_eta

∀ c : config

mkConfigc_framec c_callersc c_memc c_fuelc = c

Explore proof 1 tactics

Initial goal

c :

config

⊢

c_frame ≔ c_framec; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc = c

destruct c ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

destruct c ; reflexivity

A configuration that fails is not reducible: a failing ending, a stuck step and a negative extent each rule out all three kinds of primitive step.

86Lemma fails_not_reducible

∀ ge : genv fr callers m fuel s

failsge mkConfigfr callers m fuel

¬@reduciblenanofil_langge EConffr callers fuel m, s

Explore proof 10 tactics

Initial goal

ge :

genv

fr :

frame

callers :

listframe × pending

m :

mem

fuel :

s :

R.state

⊢

failsge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel → ¬reducibleEConffr callers fuel m, s

intros Hf κ & e′ & σ′ & efs & Hs

ge :

genv

fr :

frame

callers :

listframe × pending

m :

mem

fuel :

s :

R.state

Hf :

failsge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel

κ :

listobservationnanofil_langge

e′ :

language.exprnanofil_langge

σ′ :

statenanofil_langge

efs :

listlanguage.exprnanofil_langge

Hs :

language.prim_stepEConffr callers fuel m, s κ e′ σ′ efs

⊢

False

cbn in Hs

ge :

genv

fr :

frame

callers :

listframe × pending

m :

mem

fuel :

s :

R.state

Hf :

failsge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel

κ :

listobservationnanofil_langge

e′ :

language.exprnanofil_langge

σ′ :

statenanofil_langge

efs :

listlanguage.exprnanofil_langge

Hs :

prim_stepge EConffr callers fuel m, s κ e′ σ′ efs

⊢

False

inversion Hs ; subst

3 open

ge :

genv

fr :

frame

callers :

listframe × pending

m :

mem

fuel :

s :

R.state

Hf :

failsge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel

c′ :

config

s′ :

R.state

Hs :

prim_stepge EConffr callers fuel m, s [ ] conf_exprc′ c_memc′, s′ [ ]

H₈ :

¬failsge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel

H₉ :

RM.mstepge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel, s c′, s′

⊢

False

focused goal

ge :

genv

fr :

frame

callers :

listframe × pending

m :

mem

fuel :

s :

R.state

Hf :

failsge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel

Hs :

prim_stepge EConffr callers fuel m, s [ ] EEndTrapOutOfMemory m, s [ ]

q :

alloc_req

k :

Z → config

H₈ :

stepge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel = Freshq k

H₉ :

0 ≤ req_extentq

H₁₀ :

R.allocs q = None

⊢

False

focused goal

ge :

genv

fr :

frame

callers :

listframe × pending

m :

mem

fuel :

s :

R.state

Hf :

failsge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel

o :

outcome

Hs :

prim_stepge EConffr callers fuel m, s [ ] EEndo m, s [ ]

H₈ :

stepge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel = Doneo

H₉ :

¬failureo

⊢

False

–contradiction

2 open

deferred goal

ge :

genv

fr :

frame

callers :

listframe × pending

m :

mem

fuel :

s :

R.state

Hf :

failsge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel

Hs :

prim_stepge EConffr callers fuel m, s [ ] EEndTrapOutOfMemory m, s [ ]

q :

alloc_req

k :

Z → config

H₈ :

stepge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel = Freshq k

H₉ :

0 ≤ req_extentq

H₁₀ :

R.allocs q = None

⊢

False

deferred goal

ge :

genv

fr :

frame

callers :

listframe × pending

m :

mem

fuel :

s :

R.state

Hf :

failsge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel

o :

outcome

Hs :

prim_stepge EConffr callers fuel m, s [ ] EEndo m, s [ ]

H₈ :

stepge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel = Doneo

H₉ :

¬failureo

⊢

False

–unfold fails in Hf

2 open

ge :

genv

fr :

frame

callers :

listframe × pending

m :

mem

fuel :

s :

R.state

Hf :

match stepge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel with

Next_

⇒

False

Doneo

⇒

failureo

Freshq _

⇒

req_extentq < 0

Stuck_

⇒

True

Hs :

prim_stepge EConffr callers fuel m, s [ ] EEndTrapOutOfMemory m, s [ ]

q :

alloc_req

k :

Z → config

H₈ :

stepge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel = Freshq k

H₉ :

0 ≤ req_extentq

H₁₀ :

R.allocs q = None

⊢

False

deferred goal

ge :

genv

fr :

frame

callers :

listframe × pending

m :

mem

fuel :

s :

R.state

Hf :

failsge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel

o :

outcome

Hs :

prim_stepge EConffr callers fuel m, s [ ] EEndo m, s [ ]

H₈ :

stepge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel = Doneo

H₉ :

¬failureo

⊢

False

match goal withE : Semantics.step_ _ = Fresh_ _ |- _⇒rewrite E in Hfend

2 open

ge :

genv

fr :

frame

callers :

listframe × pending

m :

mem

fuel :

s :

R.state

Hs :

prim_stepge EConffr callers fuel m, s [ ] EEndTrapOutOfMemory m, s [ ]

q :

alloc_req

k :

Z → config

H₈ :

stepge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel = Freshq k

H₉ :

0 ≤ req_extentq

H₁₀ :

R.allocs q = None

Hf :

req_extentq < 0

⊢

False

deferred goal

ge :

genv

fr :

frame

callers :

listframe × pending

m :

mem

fuel :

s :

R.state

Hf :

failsge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel

o :

outcome

Hs :

prim_stepge EConffr callers fuel m, s [ ] EEndo m, s [ ]

H₈ :

stepge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel = Doneo

H₉ :

¬failureo

⊢

False

lia

deferred goal

ge :

genv

fr :

frame

callers :

listframe × pending

m :

mem

fuel :

s :

R.state

Hf :

failsge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel

o :

outcome

Hs :

prim_stepge EConffr callers fuel m, s [ ] EEndo m, s [ ]

H₈ :

stepge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel = Doneo

H₉ :

¬failureo

⊢

False

–unfold fails in Hf

ge :

genv

fr :

frame

callers :

listframe × pending

m :

mem

fuel :

s :

R.state

Hf :

match stepge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel with

Next_

⇒

False

Doneo

⇒

failureo

Freshq _

⇒

req_extentq < 0

Stuck_

⇒

True

o :

outcome

Hs :

prim_stepge EConffr callers fuel m, s [ ] EEndo m, s [ ]

H₈ :

stepge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel = Doneo

H₉ :

¬failureo

⊢

False

match goal withE : Semantics.step_ _ = Done_ |- _⇒rewrite E in Hfend

ge :

genv

fr :

frame

callers :

listframe × pending

m :

mem

fuel :

s :

R.state

o :

outcome

Hs :

prim_stepge EConffr callers fuel m, s [ ] EEndo m, s [ ]

H₈ :

stepge c_frame ≔ fr; c_callers ≔ callers; c_mem ≔ m; c_fuel ≔ fuel = Doneo

H₉ :

¬failureo

Hf :

failureo

⊢

False

contradiction

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros Hf κ & e′ & σ′ & efs & Hs

cbn in Hs

inversion Hs ; subst

–contradiction

–unfold fails in Hf

match goal withE : Semantics.step_ _ = Fresh_ _ |- _⇒rewrite E in Hfend

lia

–unfold fails in Hf

match goal withE : Semantics.step_ _ = Done_ |- _⇒rewrite E in Hfend

contradiction

The Iris configuration of the machine state st: its expression as the only thread, with its memory and runtime state.

101Definition cfg_ofge : genv st : RM.mstate : cfgnanofil_langge ≔

conf_exprfstst, c_memfstst, sndst

A machine step from a configuration that does not fails is an Iris step between the corresponding Iris configurations.

106Lemma mstep_erased_step

∀ ge : genv st st′

¬failsge fstst

RM.mstepge st st′

erased_stepcfg_ofge st cfg_ofge st′

Explore proof 9 tactics

Initial goal

ge :

genv

st :

config × R.state

st′ :

RM.mstate

⊢

¬failsge st.1 → RM.mstepge st st′ → erased_stepcfg_ofge st cfg_ofge st′

destruct st as c s , st′ as c′ s′

ge :

genv

c :

config

s :

R.state

c′ :

config

s′ :

R.state

⊢

¬failsge c, s.1 → RM.mstepge c, s c′, s′ → erased_stepcfg_ofge c, s cfg_ofge c′, s′

cbn [ fst ]

ge :

genv

c :

config

s :

R.state

c′ :

config

s′ :

R.state

⊢

¬failsge c → RM.mstepge c, s c′, s′ → erased_stepcfg_ofge c, s cfg_ofge c′, s′

intros Hf Hs

ge :

genv

c :

config

s :

R.state

c′ :

config

s′ :

R.state

Hf :

¬failsge c

Hs :

RM.mstepge c, s c′, s′

⊢

erased_stepcfg_ofge c, s cfg_ofge c′, s′

exists [ ]

ge :

genv

c :

config

s :

R.state

c′ :

config

s′ :

R.state

Hf :

¬failsge c

Hs :

RM.mstepge c, s c′, s′

⊢

language.stepcfg_ofge c, s [ ] cfg_ofge c′, s′

apply step_atomic with t₁ := [ ] t₂ := [ ] efs := [ ] e₁ := conf_exprc σ₁ := c_memc, s e₂ := conf_exprc′ σ₂ := c_memc′, s′ ; reflexivity | reflexivity |

ge :

genv

c :

config

s :

R.state

c′ :

config

s′ :

R.state

Hf :

¬failsge c

Hs :

RM.mstepge c, s c′, s′

⊢

language.prim_stepconf_exprc c_memc, s [ ] conf_exprc′ c_memc′, s′ [ ]

rewrite <- config_etac in Hf , Hs

ge :

genv

c :

config

s :

R.state

c′ :

config

s′ :

R.state

Hf :

¬failsge c_frame ≔ c_framec; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc

Hs :

RM.mstepge c_frame ≔ c_framec; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc, s c′, s′

⊢

language.prim_stepconf_exprc c_memc, s [ ] conf_exprc′ c_memc′, s′ [ ]

unfold conf_expr at 1

ge :

genv

c :

config

s :

R.state

c′ :

config

s′ :

R.state

Hf :

¬failsge c_frame ≔ c_framec; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc

Hs :

RM.mstepge c_frame ≔ c_framec; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc, s c′, s′

⊢

language.prim_stepEConfc_framec c_callersc c_fuelc c_memc, s [ ] conf_exprc′ c_memc′, s′ [ ]

cbn

ge :

genv

c :

config

s :

R.state

c′ :

config

s′ :

R.state

Hf :

¬failsge c_frame ≔ c_framec; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc

Hs :

RM.mstepge c_frame ≔ c_framec; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc, s c′, s′

⊢

prim_stepge EConfc_framec c_callersc c_fuelc c_memc, s [ ] conf_exprc′ c_memc′, s′ [ ]

exact ps_machinege _ _ _ _ _ _ _ Hf Hs

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

destruct st as c s , st′ as c′ s′

cbn [ fst ]

intros Hf Hs

exists [ ]

apply step_atomic with t₁ := [ ] t₂ := [ ] efs := [ ] e₁ := conf_exprc σ₁ := c_memc, s e₂ := conf_exprc′ σ₂ := c_memc′, s′ ; reflexivity | reflexivity |

rewrite <- config_etac in Hf , Hs

unfold conf_expr at 1

cbn

exact ps_machinege _ _ _ _ _ _ _ Hf Hs

Where Iris adequacy holds for the configuration c's expression, every Iris configuration reached is not stuck, so no machine state reached fails; therefore every machine state the run reaches is Iris-reachable, and none fails.

121Lemma adequate_no_fails

∀ ge : genv c₀ s₀ φ st

@adequatenanofil_langge NotStuck conf_exprc₀ c_memc₀, s₀ φ

RM.mreachablege c₀, s₀ st

¬failsge fstst

Explore proof 18 tactics

Initial goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

⊢

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ → ∀st : RM.mstate, RM.mreachablege c₀, s₀ st → ¬failsge st.1

intros Had

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

⊢

∀st : RM.mstate, RM.mreachablege c₀, s₀ st → ¬failsge st.1

assert Hok : ∀st, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge fstst

2 open

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

⊢

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

focused goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

⊢

∀st : RM.mstate, RM.mreachablege c₀, s₀ st → ¬failsge st.1

{intros c s Hr Hf

2 open

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

c :

config

s :

R.state

Hr :

rtcerased_step cfg_ofge c₀, s₀ cfg_ofge c, s

Hf :

failsge c, s.1

⊢

False

deferred goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

⊢

∀st : RM.mstate, RM.mreachablege c₀, s₀ st → ¬failsge st.1

cbn [ fst ] in Hf

2 open

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

c :

config

s :

R.state

Hr :

rtcerased_step cfg_ofge c₀, s₀ cfg_ofge c, s

Hf :

failsge c

⊢

False

deferred goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

⊢

∀st : RM.mstate, RM.mreachablege c₀, s₀ st → ¬failsge st.1

destruct adequate_not_stuck_ _ _ _ Had _ _ conf_exprc eq_refl Hr as v Hv | Hred

4 open

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

c :

config

s :

R.state

Hr :

rtcerased_step cfg_ofge c₀, s₀ cfg_ofge c, s

Hf :

failsge c

⊢

conf_exprc ∈ conf_exprc, s.1

focused goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

c :

config

s :

R.state

Hr :

rtcerased_step cfg_ofge c₀, s₀ cfg_ofge c, s

Hf :

failsge c

v :

valnanofil_langge

Hv :

language.to_valconf_exprc = Somev

⊢

False

focused goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

c :

config

s :

R.state

Hr :

rtcerased_step cfg_ofge c₀, s₀ cfg_ofge c, s

Hf :

failsge c

Hred :

reducibleconf_exprc c_memc, s.1, c, s.2

⊢

False

deferred goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

⊢

∀st : RM.mstate, RM.mreachablege c₀, s₀ st → ¬failsge st.1

–set_solver

3 open

deferred goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

c :

config

s :

R.state

Hr :

rtcerased_step cfg_ofge c₀, s₀ cfg_ofge c, s

Hf :

failsge c

v :

valnanofil_langge

Hv :

language.to_valconf_exprc = Somev

⊢

False

deferred goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

c :

config

s :

R.state

Hr :

rtcerased_step cfg_ofge c₀, s₀ cfg_ofge c, s

Hf :

failsge c

Hred :

reducibleconf_exprc c_memc, s.1, c, s.2

⊢

False

deferred goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

⊢

∀st : RM.mstate, RM.mreachablege c₀, s₀ st → ¬failsge st.1

–discriminate Hv

2 open

deferred goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

c :

config

s :

R.state

Hr :

rtcerased_step cfg_ofge c₀, s₀ cfg_ofge c, s

Hf :

failsge c

Hred :

reducibleconf_exprc c_memc, s.1, c, s.2

⊢

False

deferred goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

⊢

∀st : RM.mstate, RM.mreachablege c₀, s₀ st → ¬failsge st.1

–rewrite <- config_etac in Hf

2 open

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

c :

config

s :

R.state

Hr :

rtcerased_step cfg_ofge c₀, s₀ cfg_ofge c, s

Hf :

failsge c_frame ≔ c_framec; c_callers ≔ c_callersc; c_mem ≔ c_memc; c_fuel ≔ c_fuelc

Hred :

reducibleconf_exprc c_memc, s.1, c, s.2

⊢

False

deferred goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

⊢

∀st : RM.mstate, RM.mreachablege c₀, s₀ st → ¬failsge st.1

exact fails_not_reduciblege _ _ _ _ s Hf Hred

deferred goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

⊢

∀st : RM.mstate, RM.mreachablege c₀, s₀ st → ¬failsge st.1

assert Hgen : ∀st₁ st₂, RM.mreachablege st₁ st₂ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₁ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₂

2 open

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

⊢

∀st₁ st₂ : RM.mstate, RM.mreachablege st₁ st₂ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₁ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₂

focused goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

Hgen :

∀st₁ st₂ : RM.mstate, RM.mreachablege st₁ st₂ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₁ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₂

⊢

∀st : RM.mstate, RM.mreachablege c₀, s₀ st → ¬failsge st.1

{intros st₁ st₂ H

2 open

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

st₁, st₂ :

RM.mstate

H :

RM.mreachablege st₁ st₂

⊢

rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₁ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₂

deferred goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

Hgen :

∀st₁ st₂ : RM.mstate, RM.mreachablege st₁ st₂ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₁ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₂

⊢

∀st : RM.mstate, RM.mreachablege c₀, s₀ st → ¬failsge st.1

induction H as st₁ st₂ Hs | st₁ | st₁ st₂ st₃ _ IH₁ _ IH₂ ; auto

2 open

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

st₁, st₂ :

RM.mstate

Hs :

RM.mstepge st₁ st₂

⊢

rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₁ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₂

deferred goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

Hgen :

∀st₁ st₂ : RM.mstate, RM.mreachablege st₁ st₂ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₁ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₂

⊢

∀st : RM.mstate, RM.mreachablege c₀, s₀ st → ¬failsge st.1

intros Hr

2 open

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

st₁, st₂ :

RM.mstate

Hs :

RM.mstepge st₁ st₂

Hr :

rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₁

⊢

rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₂

deferred goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

Hgen :

∀st₁ st₂ : RM.mstate, RM.mreachablege st₁ st₂ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₁ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₂

⊢

∀st : RM.mstate, RM.mreachablege c₀, s₀ st → ¬failsge st.1

eapply rtc_r ; exact Hr |

2 open

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

st₁, st₂ :

RM.mstate

Hs :

RM.mstepge st₁ st₂

Hr :

rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₁

⊢

erased_stepcfg_ofge st₁ cfg_ofge st₂

deferred goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

Hgen :

∀st₁ st₂ : RM.mstate, RM.mreachablege st₁ st₂ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₁ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₂

⊢

∀st : RM.mstate, RM.mreachablege c₀, s₀ st → ¬failsge st.1

apply mstep_erased_step ; apply Hok , Hr | exact Hs

deferred goal

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

Hgen :

∀st₁ st₂ : RM.mstate, RM.mreachablege st₁ st₂ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₁ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₂

⊢

∀st : RM.mstate, RM.mreachablege c₀, s₀ st → ¬failsge st.1

intros st Hreach

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

Hgen :

∀st₁ st₂ : RM.mstate, RM.mreachablege st₁ st₂ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₁ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₂

st :

RM.mstate

Hreach :

RM.mreachablege c₀, s₀ st

⊢

¬failsge st.1

apply Hok , Hgen_ _ Hreach

ge :

genv

c₀ :

config

s₀ :

R.state

φ :

valnanofil_langge → statenanofil_langge → Prop

Had :

adequateNotStuck conf_exprc₀ c_memc₀, s₀ φ

Hok :

∀st : RM.mstate, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge st.1

Hgen :

∀st₁ st₂ : RM.mstate, RM.mreachablege st₁ st₂ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₁ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₂

st :

RM.mstate

Hreach :

RM.mreachablege c₀, s₀ st

⊢

rtcerased_step cfg_ofge c₀, s₀ cfg_ofge c₀, s₀

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros Had

assert Hok : ∀st, rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st → ¬failsge fstst

{intros c s Hr Hf

cbn [ fst ] in Hf

destruct adequate_not_stuck_ _ _ _ Had _ _ conf_exprc eq_refl Hr as v Hv | Hred

–set_solver

–discriminate Hv

–rewrite <- config_etac in Hf

exact fails_not_reduciblege _ _ _ _ s Hf Hred

assert Hgen : ∀st₁ st₂, RM.mreachablege st₁ st₂ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₁ → rtcerased_step cfg_ofge c₀, s₀ cfg_ofge st₂

{intros st₁ st₂ H

induction H as st₁ st₂ Hs | st₁ | st₁ st₂ st₃ _ IH₁ _ IH₂ ; auto

intros Hr

eapply rtc_r ; exact Hr |

apply mstep_erased_step ; apply Hok , Hr | exact Hs

intros st Hreach

apply Hok , Hgen_ _ Hreach

reflexivity

Iris adequacy proves never_panics: where the module's initial memory and entry function exist, every admissible input makes the entry's frame, and (where R is ready at its start in that memory) for every fuel and every invariant instance a state interpretation stateI can be allocated that holds of the initial state and gives a NotStuck weakest precondition of the entry call, the module never panics. The later-credit flag hlc is left to the caller.

147Theorem wp_never_panics

∀ hlc : has_lc Σ `{!invGpreSΣ} md entry input : listword → Prop globals m f

initial_memorymd = Someglobals, m

find_fnP.program_genvmd globals entry = SomeDefinedf

∀xs, inputxs → ∃fr, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let _ : irisGS_genhlc nanofil_langP.program_genvmd globals Σ ≔ IrisGHinv λσ _ _ _ ⇒ stateIσ λ_ ⇒ True%I λ_ ⇒ 0%nat λ_ _ _ _ ⇒ fupd_intro_ _ in stateIm, R.start ∗ WP_{NotStuck; ⊤}EConffr [ ] fuel : language.exprnanofil_langP.program_genvmd globals {_. True}

P.never_panicsmd entry input

Explore proof 21 tactics

Initial goal

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

⊢

initial_memorymd = Someglobals, m → find_fnP.program_genvmd globals entry = SomeDefinedf → ∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langP.program_genvmd globals _ : nat _ : listobservationnanofil_langP.program_genvmd globals _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langP.program_genvmd globals ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langP.program_genvmd globals _ : nat _ : listobservationnanofil_langP.program_genvmd globals _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langP.program_genvmd globals {_. True} → P.never_panicsmd entry input

intros Hm Hf Hwp

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

Hf :

find_fnP.program_genvmd globals entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langP.program_genvmd globals _ : nat _ : listobservationnanofil_langP.program_genvmd globals _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langP.program_genvmd globals ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langP.program_genvmd globals _ : nat _ : listobservationnanofil_langP.program_genvmd globals _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langP.program_genvmd globals {_. True}

⊢

P.never_panicsmd entry input

exists globals, m, f

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

Hf :

find_fnP.program_genvmd globals entry = SomeDefinedf

Hwp :

⊢

initial_memorymd = Someglobals, m ∧ find_fnP.program_genvmd globals entry = SomeDefinedf ∧ ∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z st : P.RM.mstate, P.RM.mreachableP.program_genvmd globals c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st → ¬failsP.program_genvmd globals st.1

split ; exact Hm |

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

Hf :

find_fnP.program_genvmd globals entry = SomeDefinedf

Hwp :

⊢

find_fnP.program_genvmd globals entry = SomeDefinedf ∧ ∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z st : P.RM.mstate, P.RM.mreachableP.program_genvmd globals c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st → ¬failsP.program_genvmd globals st.1

split ; exact Hf |

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

Hf :

find_fnP.program_genvmd globals entry = SomeDefinedf

Hwp :

⊢

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z st : P.RM.mstate, P.RM.mreachableP.program_genvmd globals c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st → ¬failsP.program_genvmd globals st.1

intros xs Hxs

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

Hf :

find_fnP.program_genvmd globals entry = SomeDefinedf

Hwp :

xs :

listword

Hxs :

inputxs

⊢

∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z st : P.RM.mstate, P.RM.mreachableP.program_genvmd globals c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st → ¬failsP.program_genvmd globals st.1

destruct Hwpxs Hxs as fr & Hfr & Hw

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

Hf :

find_fnP.program_genvmd globals entry = SomeDefinedf

Hwp :

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langP.program_genvmd globals _ : nat _ : listobservationnanofil_langP.program_genvmd globals _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langP.program_genvmd globals ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langP.program_genvmd globals _ : nat _ : listobservationnanofil_langP.program_genvmd globals _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel {_. True}

⊢

∃fr₀ : frame, call_framef xs = Somefr₀ ∧ R.readyR.start m → ∀fuel : Z st : P.RM.mstate, P.RM.mreachableP.program_genvmd globals c_frame ≔ fr₀; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st → ¬failsP.program_genvmd globals st.1

exists fr

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

Hf :

find_fnP.program_genvmd globals entry = SomeDefinedf

Hwp :

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

⊢

call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z st : P.RM.mstate, P.RM.mreachableP.program_genvmd globals c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st → ¬failsP.program_genvmd globals st.1

split ; exact Hfr |

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

Hf :

find_fnP.program_genvmd globals entry = SomeDefinedf

Hwp :

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

⊢

R.readyR.start m → ∀fuel : Z st : P.RM.mstate, P.RM.mreachableP.program_genvmd globals c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st → ¬failsP.program_genvmd globals st.1

intros Hready fuel st Hreach

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

Hf :

find_fnP.program_genvmd globals entry = SomeDefinedf

Hwp :

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachableP.program_genvmd globals c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

⊢

¬failsP.program_genvmd globals st.1

set ge := P.program_genvmd globals in *

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel {_. True}

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

⊢

¬failsge st.1

assert Had : @adequatenanofil_langge NotStuck conf_exprmkConfigfr [ ] m fuel c_memmkConfigfr [ ] m fuel, R.start λ_ _ ⇒ True

2 open

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

⊢

adequateNotStuck conf_exprc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel c_memc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start λ_ : valnanofil_langge _ : statenanofil_langge ⇒ True

focused goal

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Had :

⊢

¬failsge st.1

{apply wp_adequacy_genhlc Σ nanofil_langge NotStuck _ _ λ_ ⇒ True

2 open

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

⊢

∀Hinv : invGS_genhlc Σ κs : listobservationnanofil_langge, ⊢ |⇛^⊤ ∃stateI : statenanofil_langge → listobservationnanofil_langge → iPropΣ fork_post : valnanofil_langge → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat κs₀ : listobservationnanofil_langge _ : nat ⇒ stateIσ κs₀; fork_post ≔ fork_post; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat κs₀ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ κs₀ in stateIc_memc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start κs ∗ WPconf_exprc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel {_. True}

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Had :

⊢

¬failsge st.1

intros Hinv κs

2 open

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Hinv :

invGS_genhlc Σ

κs :

listobservationnanofil_langge

⊢

⊢ |⇛^⊤ ∃stateI : statenanofil_langge → listobservationnanofil_langge → iPropΣ fork_post : valnanofil_langge → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat κs₀ : listobservationnanofil_langge _ : nat ⇒ stateIσ κs₀; fork_post ≔ fork_post; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat κs₀ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ κs₀ in stateIc_memc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start κs ∗ WPconf_exprc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel {_. True}

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Had :

⊢

¬failsge st.1

iMod HwHready fuel Hinv as stateI [Hσ Hwp]

2 open

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Hinv :

invGS_genhlc Σ

κs :

listobservationnanofil_langge

stateI :

nstate → iPropΣ

Hσ :

stateIm, R.start

Hwp :

WPEConffr [ ] fuel {_. True}

∗

|⇛^⊤ ∃stateI₀ : statenanofil_langge → listobservationnanofil_langge → iPropΣ fork_post : valnanofil_langge → iPropΣ, stateI₀c_memc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start κs ∗ WPconf_exprc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel {_. True}

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Had :

⊢

¬failsge st.1

iModIntro

2 open

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Hinv :

invGS_genhlc Σ

κs :

listobservationnanofil_langge

stateI :

nstate → iPropΣ

Hσ :

stateIm, R.start

Hwp :

WPEConffr [ ] fuel {_. True}

∗

∃stateI₀ : statenanofil_langge → listobservationnanofil_langge → iPropΣ fork_post : valnanofil_langge → iPropΣ, stateI₀c_memc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start κs ∗ WPconf_exprc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel {_. True}

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Had :

⊢

¬failsge st.1

iExists λσ _ ⇒ stateIσ, λ_ ⇒ True%I

2 open

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Hinv :

invGS_genhlc Σ

κs :

listobservationnanofil_langge

stateI :

nstate → iPropΣ

Hσ :

stateIm, R.start

Hwp :

WPEConffr [ ] fuel {_. True}

∗

stateIc_memc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start ∗ WPconf_exprc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel {_. True}

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Had :

⊢

¬failsge st.1

cbn

2 open

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Hinv :

invGS_genhlc Σ

κs :

listobservationnanofil_langge

stateI :

nstate → iPropΣ

Hσ :

stateIm, R.start

Hwp :

WPEConffr [ ] fuel {_. True}

∗

stateIm, R.start ∗ WPconf_exprc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel {_. True}

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Had :

⊢

¬failsge st.1

iFrame Hσ

2 open

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Hinv :

invGS_genhlc Σ

κs :

listobservationnanofil_langge

stateI :

nstate → iPropΣ

Hwp :

WPEConffr [ ] fuel {_. True}

∗

WPconf_exprc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel {_. True}

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Had :

⊢

¬failsge st.1

iApply wp_mono with Hwp

2 open

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Hinv :

invGS_genhlc Σ

κs :

listobservationnanofil_langge

stateI :

nstate → iPropΣ

⊢

valnanofil_langge → True ⊢ True

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Had :

⊢

¬failsge st.1

auto

deferred goal

hlc :

has_lc

Σ :

gFunctors

invGpreS₀ :

invGpreSΣ

md :

module

entry :

name

input :

listword → Prop

globals :

listname × ptr

m :

mem

f :

func

Hm :

initial_memorymd = Someglobals, m

ge :=

P.program_genvmd globals : genv

Hf :

find_fnge entry = SomeDefinedf

Hwp :

∀xs : listword, inputxs → ∃fr : frame, call_framef xs = Somefr ∧ R.readyR.start m → ∀fuel : Z Hinv : invGS_genhlc Σ, ⊢ |⇛^⊤ ∃stateI : nstate → iPropΣ, let H ≔ iris_invGS ≔ Hinv; state_interp ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ stateIσ; fork_post ≔ λ_ : valnanofil_langge ⇒ True; num_laters_per_step ≔ λ_ : nat ⇒ 0%nat; state_interp_mono ≔ λσ : statenanofil_langge _ : nat _ : listobservationnanofil_langge _ : nat ⇒ fupd_intro∅ stateIσ in stateIm, R.start ∗ WPEConffr [ ] fuel : language.exprnanofil_langge {_. True}

xs :

listword

Hxs :

inputxs

fr :

frame

Hfr :

call_framef xs = Somefr

Hw :

Hready :

R.readyR.start m

fuel :

st :

P.RM.mstate

Hreach :

P.RM.mreachablege c_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, R.start st

Had :

⊢

¬failsge st.1

exact adequate_no_failsge _ _ _ Had st Hreach

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros Hm Hf Hwp

exists globals, m, f

split ; exact Hm |

split ; exact Hf |

intros xs Hxs

destruct Hwpxs Hxs as fr & Hfr & Hw

exists fr

split ; exact Hfr |

intros Hready fuel st Hreach

set ge := P.program_genvmd globals in *

assert Had : @adequatenanofil_langge NotStuck conf_exprmkConfigfr [ ] m fuel c_memmkConfigfr [ ] m fuel, R.start λ_ _ ⇒ True

{apply wp_adequacy_genhlc Σ nanofil_langge NotStuck _ _ λ_ ⇒ True

intros Hinv κs

iMod HwHready fuel Hinv as stateI [Hσ Hwp]

iModIntro

iExists λσ _ ⇒ stateIσ, λ_ ⇒ True%I

cbn

iFrame Hσ

iApply wp_mono with Hwp

auto

exact adequate_no_failsge _ _ _ Had st Hreach