rocq/theories/HiArtifact.v

The application proof describes the checked module actually generated from hi.c. The shared program-fixture gate regenerates HiCode.v; this equality connects that artifact to the source-shaped body.

From Stdlib Require Import String ZArith List

From Nanofil Require Import Term Syntax Values Memory Runtime Semantics ExternalCalls Startup Stdio Shutdown ExternalMachine Composition Panics HiCode Hi Transport Program

Import ListNotations

Open Scope Z_scope

Decoding the pinned -O output gives exactly the module used by Hi.v, including its literal bytes, result and actual temporary argument.

13Theorem hi_generated_module

decode_modulehi_term = Somehi_module

Explore proof 1 tactics

Initial goal

⊢

decode_modulehi_term = Somehi_module

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

reflexivity

The generated main ignores its launcher words. This application-entry theorem is stronger than restricting them to startup_at; it does not prove the native launcher reaches an entry satisfying these premises.

19Module HiProgram R : Runtime

20Module P ≔ Program R

Defined main and an actual call frame, then independent admissibility and shared-classification safety for every fuel and launcher input. The exact runtime state after startup is retained, not reset to start. Opaque stdio validity and its safepoint stability remain explicit.

26Theorem hi_launcher_words_safe

∀ rep requests s_entry m w argc argv envp

∀s m s′ m′ w, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

P.H.hi_before_callrep m program_stdiow

program_world_wfw

orientationprogram_stdoutw ≠ WideOriented

∃fr, find_fnP.H.hi_genv TAtom"main" = SomeDefinedhi_function ∧ call_framehi_function main_argumentsargc argv envp = Somefr ∧ ∀fuel, R.readys_entry m → ∀trace c s w′ site, P.M.runP.registryrep requests P.H.hi_genv P.M.RunningmkConfigfr [ ] m fuel, s_entry w trace P.M.Runningc, s w′ → external_siteP.H.hi_genv c site → P.M.admissibleP.registryrep requests P.H.hi_genv c w′ site ∧ ∀b host trace why ms w′, P.runrep requests b host P.ApplicationP.M.RunningmkConfigfr [ ] m fuel, s_entry w trace P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

Explore proof 14 tactics

Initial goal

⊢

∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop s_entry : R.state m : mem w : program_world argc : Z argv envp : ptr, ∀s : R.state m₀ : mem s′ : R.state m′ : mem w₀ : stdio_world, R.safepoints m₀ s′ m′ → repm₀ w₀ → stdio_readym₀ w₀ → repm′ w₀ ∧ stdio_readym′ w₀ → P.H.hi_before_callrep m program_stdiow → program_world_wfw → orientationprogram_stdoutw ≠ WideOriented → ∃fr : frame, find_fnP.H.hi_genv TAtom"main" = SomeDefinedhi_function ∧ call_framehi_function main_argumentsargc argv envp = Somefr ∧ ∀fuel : Z, R.readys_entry m → ∀trace : listevent c : config s : R.state w′ : program_world site : call_site, P.M.runP.registryrep requests P.H.hi_genv P.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s_entry w trace P.M.Runningc, s w′ → external_siteP.H.hi_genv c site → P.M.admissibleP.registryrep requests P.H.hi_genv c w′ site ∧ ∀b : P.shutdown_boundary host : P.host_boundary trace : listevent why : ending ms : P.M.P.I.RM.mstate w′ : program_world, P.runrep requests b host P.ApplicationP.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s_entry w trace P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

intros rep requests s_entry m w argc argv envp Hstable Hpre Hwf Ho

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

⊢

∃fr : frame, find_fnP.H.hi_genv TAtom"main" = SomeDefinedhi_function ∧ call_framehi_function main_argumentsargc argv envp = Somefr ∧ ∀fuel : Z, R.readys_entry m → ∀trace : listevent c : config s : R.state w′ : program_world site : call_site, P.M.runP.registryrep requests P.H.hi_genv P.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s_entry w trace P.M.Runningc, s w′ → external_siteP.H.hi_genv c site → P.M.admissibleP.registryrep requests P.H.hi_genv c w′ site ∧ ∀b : P.shutdown_boundary host : P.host_boundary trace : listevent why : ending ms : P.M.P.I.RM.mstate w′ : program_world, P.runrep requests b host P.ApplicationP.M.Runningc_frame ≔ fr; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s_entry w trace P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

assert Hentry : ∀fuel, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

⊢

∀fuel : Z, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

focused goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

Hentry :

∀fuel : Z, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

⊢

{intros fuel

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

fuel :

⊢

P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

Hentry :

∀fuel : Z, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

⊢

split ; apply P.H.hi_body_entry ; exact Hpre |

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

fuel :

⊢

program_world_wfP.world_ofP.M.Runninghi_entrym fuel, s_entry w ∧ orientationprogram_stdoutP.world_ofP.M.Runninghi_entrym fuel, s_entry w ≠ WideOriented

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

Hentry :

∀fuel : Z, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

⊢

auto

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

Hentry :

∀fuel : Z, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

⊢

exists c_framehi_entrym 0

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

Hentry :

∀fuel : Z, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

⊢

find_fnP.H.hi_genv TAtom"main" = SomeDefinedhi_function ∧ call_framehi_function main_argumentsargc argv envp = Somec_framehi_entrym 0 ∧ ∀fuel : Z, R.readys_entry m → ∀trace : listevent c : config s : R.state w′ : program_world site : call_site, P.M.runP.registryrep requests P.H.hi_genv P.M.Runningc_frame ≔ c_framehi_entrym 0; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s_entry w trace P.M.Runningc, s w′ → external_siteP.H.hi_genv c site → P.M.admissibleP.registryrep requests P.H.hi_genv c w′ site ∧ ∀b : P.shutdown_boundary host : P.host_boundary trace : listevent why : ending ms : P.M.P.I.RM.mstate w′ : program_world, P.runrep requests b host P.ApplicationP.M.Runningc_frame ≔ c_framehi_entrym 0; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s_entry w trace P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

split ; reflexivity |

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

Hentry :

∀fuel : Z, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

⊢

call_framehi_function main_argumentsargc argv envp = Somec_framehi_entrym 0 ∧ ∀fuel : Z, R.readys_entry m → ∀trace : listevent c : config s : R.state w′ : program_world site : call_site, P.M.runP.registryrep requests P.H.hi_genv P.M.Runningc_frame ≔ c_framehi_entrym 0; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s_entry w trace P.M.Runningc, s w′ → external_siteP.H.hi_genv c site → P.M.admissibleP.registryrep requests P.H.hi_genv c w′ site ∧ ∀b : P.shutdown_boundary host : P.host_boundary trace : listevent why : ending ms : P.M.P.I.RM.mstate w′ : program_world, P.runrep requests b host P.ApplicationP.M.Runningc_frame ≔ c_framehi_entrym 0; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s_entry w trace P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

split ; reflexivity |

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

Hentry :

∀fuel : Z, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

⊢

∀fuel : Z, R.readys_entry m → ∀trace : listevent c : config s : R.state w′ : program_world site : call_site, P.M.runP.registryrep requests P.H.hi_genv P.M.Runningc_frame ≔ c_framehi_entrym 0; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s_entry w trace P.M.Runningc, s w′ → external_siteP.H.hi_genv c site → P.M.admissibleP.registryrep requests P.H.hi_genv c w′ site ∧ ∀b : P.shutdown_boundary host : P.host_boundary trace : listevent why : ending ms : P.M.P.I.RM.mstate w′ : program_world, P.runrep requests b host P.ApplicationP.M.Runningc_frame ≔ c_framehi_entrym 0; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s_entry w trace P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

intros fuel Hready

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

Hentry :

∀fuel : Z, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

fuel :

Hready :

R.readys_entry m

⊢

∀trace : listevent c : config s : R.state w′ : program_world site : call_site, P.M.runP.registryrep requests P.H.hi_genv P.M.Runningc_frame ≔ c_framehi_entrym 0; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s_entry w trace P.M.Runningc, s w′ → external_siteP.H.hi_genv c site → P.M.admissibleP.registryrep requests P.H.hi_genv c w′ site ∧ ∀b : P.shutdown_boundary host : P.host_boundary trace : listevent why : ending ms : P.M.P.I.RM.mstate w′ : program_world, P.runrep requests b host P.ApplicationP.M.Runningc_frame ≔ c_framehi_entrym 0; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s_entry w trace P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

split

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

Hentry :

∀fuel : Z, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

fuel :

Hready :

R.readys_entry m

⊢

focused goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

Hentry :

∀fuel : Z, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

fuel :

Hready :

R.readys_entry m

⊢

∀b : P.shutdown_boundary host : P.host_boundary trace : listevent why : ending ms : P.M.P.I.RM.mstate w′ : program_world, P.runrep requests b host P.ApplicationP.M.Runningc_frame ≔ c_framehi_entrym 0; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s_entry w trace P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

–intros trace c s w′ site Hrun Hsite

2 open

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

Hentry :

∀fuel : Z, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

fuel :

Hready :

R.readys_entry m

trace :

listevent

c :

config

s :

R.state

w′ :

program_world

site :

call_site

Hrun :

P.M.runP.registryrep requests P.H.hi_genv P.M.Runningc_frame ≔ c_framehi_entrym 0; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s_entry w trace P.M.Runningc, s w′

Hsite :

external_siteP.H.hi_genv c site

⊢

P.M.admissibleP.registryrep requests P.H.hi_genv c w′ site

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

Hentry :

∀fuel : Z, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

fuel :

Hready :

R.readys_entry m

⊢

eapply P.all_calls_admissible ; exact Hstable | apply Hentry | exact Hrun | exact Hsite

deferred goal

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

Hentry :

∀fuel : Z, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

fuel :

Hready :

R.readys_entry m

⊢

–intros b host trace why ms w′ Hrun

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s_entry :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

Hentry :

∀fuel : Z, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

fuel :

Hready :

R.readys_entry m

b :

P.shutdown_boundary

host :

P.host_boundary

trace :

listevent

why :

ending

ms :

P.M.P.I.RM.mstate

w′ :

program_world

Hrun :

P.runrep requests b host P.ApplicationP.M.Runningc_frame ≔ c_framehi_entrym 0; c_callers ≔ [ ]; c_mem ≔ m; c_fuel ≔ fuel, s_entry w trace P.ApplicationP.M.Stoppedwhy ms w′

⊢

¬failure_endingwhy

eapply P.application_stopped_never_panics with st := P.ApplicationP.M.Runninghi_entrym fuel, s_entry w ; exact Hstable | apply Hentry | exact Hrun

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros rep requests s_entry m w argc argv envp Hstable Hpre Hwf Ho

assert Hentry : ∀fuel, P.body_invrep P.M.Runninghi_entrym fuel, s_entry w

{intros fuel

split ; apply P.H.hi_body_entry ; exact Hpre |

auto

exists c_framehi_entrym 0

split ; reflexivity |

intros fuel Hready

split

–intros trace c s w′ site Hrun Hsite

eapply P.all_calls_admissible ; exact Hstable | apply Hentry | exact Hrun | exact Hsite

–intros b host trace why ms w′ Hrun

eapply P.application_stopped_never_panics with st := P.ApplicationP.M.Runninghi_entrym fuel, s_entry w ; exact Hstable | apply Hentry | exact Hrun

The named trusted successful-entry image for this generated program. Native launcher/libc/TLS satisfaction is trusted, probed by libc-entry.c, not proved by these predicates or by startup's copy lemmas. Constructor and environment obligations are not permissions for arbitrary callbacks.

63Definition trusted_entry_contractrep s m w argc argv envp args environment : Prop ≔

startup_atm argc argv envp args environment ∧ R.readys m ∧ P.H.hi_before_callrep m program_stdiow ∧ program_world_wfw ∧ orientationprogram_stdoutw ≠ WideOriented

Every successful trusted entry supplies the real application invariant, retaining the exact runtime and memory, for any execution fuel.

70Lemma trusted_entry_body

∀ rep s m w argc argv envp args environment fuel

trusted_entry_contractrep s m w argc argv envp args environment

P.body_invrep P.M.Runninghi_entrym fuel, s w

Explore proof 3 tactics

Initial goal

⊢

∀rep : mem → stdio_world → Prop s : R.state m : mem w : program_world argc : Z argv envp : ptr args environment : listlistZ fuel : Z, trusted_entry_contractrep s m w argc argv envp args environment → P.body_invrep P.M.Runninghi_entrym fuel, s w

intros rep s m w argc argv envp args environment fuel _ & _ & Hpre & Hwf & Ho

rep :

mem → stdio_world → Prop

s :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

args, environment :

listlistZ

fuel :

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

⊢

P.body_invrep P.M.Runninghi_entrym fuel, s w

split ; apply P.H.hi_body_entry ; exact Hpre |

rep :

mem → stdio_world → Prop

s :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

args, environment :

listlistZ

fuel :

Hpre :

P.H.hi_before_callrep m program_stdiow

Hwf :

program_world_wfw

Ho :

orientationprogram_stdoutw ≠ WideOriented

⊢

program_world_wfP.world_ofP.M.Runninghi_entrym fuel, s w ∧ orientationprogram_stdoutP.world_ofP.M.Runninghi_entrym fuel, s w ≠ WideOriented

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros rep s m w argc argv envp args environment fuel _ & _ & Hpre & Hwf & Ho

split ; apply P.H.hi_body_entry ; exact Hpre |

auto

The trusted entry image suffices for application-only nonfailure. Entry refusal or unfinished startup is not a successful-entry image; this theorem promises neither native startup success nor termination.

81Theorem trusted_entry_never_panics

∀ rep requests s m w argc argv envp args environment fuel b host trace why ms w′

∀s m s′ m′ w, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

trusted_entry_contractrep s m w argc argv envp args environment

P.runrep requests b host P.ApplicationP.M.Runninghi_entrym fuel, s w trace P.ApplicationP.M.Stoppedwhy ms w′

¬failure_endingwhy

Explore proof 3 tactics

Initial goal

⊢

∀rep : mem → stdio_world → Prop requests : listword → mem → stdio_world → Z → Z → Prop s : R.state m : mem w : program_world argc : Z argv envp : ptr args environment : listlistZ fuel : Z b : P.shutdown_boundary host : P.host_boundary trace : listevent why : ending ms : P.M.P.I.RM.mstate w′ : program_world, ∀s₀ : R.state m₀ : mem s′ : R.state m′ : mem w₀ : stdio_world, R.safepoints₀ m₀ s′ m′ → repm₀ w₀ → stdio_readym₀ w₀ → repm′ w₀ ∧ stdio_readym′ w₀ → trusted_entry_contractrep s m w argc argv envp args environment → P.runrep requests b host P.ApplicationP.M.Runninghi_entrym fuel, s w trace P.ApplicationP.M.Stoppedwhy ms w′ → ¬failure_endingwhy

intros rep requests s m w argc argv envp args environment fuel b host trace why ms w′ Hstable Hentry Hrun

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

args, environment :

listlistZ

fuel :

b :

P.shutdown_boundary

host :

P.host_boundary

trace :

listevent

why :

ending

ms :

P.M.P.I.RM.mstate

w′ :

program_world

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hentry :

trusted_entry_contractrep s m w argc argv envp args environment

Hrun :

P.runrep requests b host P.ApplicationP.M.Runninghi_entrym fuel, s w trace P.ApplicationP.M.Stoppedwhy ms w′

⊢

¬failure_endingwhy

eapply P.application_stopped_never_panics ; exact Hstable | | exact Hrun

rep :

mem → stdio_world → Prop

requests :

listword → mem → stdio_world → Z → Z → Prop

s :

R.state

m :

mem

w :

program_world

argc :

argv, envp :

ptr

args, environment :

listlistZ

fuel :

b :

P.shutdown_boundary

host :

P.host_boundary

trace :

listevent

why :

ending

ms :

P.M.P.I.RM.mstate

w′ :

program_world

Hstable :

∀s : R.state m : mem s′ : R.state m′ : mem w : stdio_world, R.safepoints m s′ m′ → repm w → stdio_readym w → repm′ w ∧ stdio_readym′ w

Hentry :

trusted_entry_contractrep s m w argc argv envp args environment

Hrun :

P.runrep requests b host P.ApplicationP.M.Runninghi_entrym fuel, s w trace P.ApplicationP.M.Stoppedwhy ms w′

⊢

P.application_saferep P.ApplicationP.M.Runninghi_entrym fuel, s w

eapply trusted_entry_body ; exact Hentry

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script

intros rep requests s m w argc argv envp args environment fuel b host trace why ms w′ Hstable Hentry Hrun

eapply P.application_stopped_never_panics ; exact Hstable | | exact Hrun

eapply trusted_entry_body ; exact Hentry

A named trusted successful-completion specification. The explicit completed witness concerns this exact handoff, not mere readiness. Native satisfaction is probed by libc-exit.c, not proved. Finished remembers the handoff snapshot, not native postmortem memory, and completion does not assert that outstanding output was delivered.

100Definition trusted_host_contractcompleted : P.host_boundary : P.host_boundary ≔