Fil-C on Nix

Filnix wiki

the formal campaign

rocq/theories/Libio.v

A capability-backed memory view of the pinned byte stdout (milestone 3c).

Offsets are measured with the Fil-C headers, not the host's FILE. This is a view of the buffer/lock roots, not a complete predicate for native FILE validity or a proof of libio's execution. In particular, vtable dispatch, TLS initialization, protocol scheduling and native prefix coverage remain trusted realization obligations.

The selected malloc forwards to zgc_alloc: runtime refusal does not return NULL to _IO_file_doallocate. The generic libio NULL fallback and the pin's terminal resource ending are distinct.

From Stdlib Require Import ZArith List Bool Lia
From Nanofil Require Import Syntax Values Memory Runtime Identity ExternalCalls ExternalMachine Startup
Import ListNotations
Open Scope Z_scope

Source-selected capacity and buffer paths

The byte capacity of stdout's allocated buffer, given whether stat succeeded and the block size it reported. As filedoalloc.c, for the selected stdout descriptor 1 and the pinned x86-64 _STATBUF_ST_BLKSIZE configuration: use a positive st_blksize smaller than BUFSIZ (8192) only after a successful stat; otherwise retain BUFSIZ. This is NOT the capacity function for arbitrary descriptors.

29Definition file_capacitystat_ok : bool block_size : Z : Z ≔
stat_ok && 0 <? block_size && block_size <? 8192
→
block_size
else
8192

The capacity is always positive and at most 8192 bytes, so the buffer request is never too big.

35Lemma file_capacity_bounds
∀ stat_ok block_size
0 < file_capacitystat_ok block_size ≤ 8192
Explore proof 8 tactics

Initial goal

⊢
∀stat_ok : bool block_size : Z, 0 < file_capacitystat_ok block_size ≤ 8192

intros

stat_ok :
bool
block_size :
Z
⊢
0 < file_capacitystat_ok block_size ≤ 8192

unfold file_capacity

stat_ok :
bool
block_size :
Z
⊢
0 < if stat_ok && 0 <? block_size && block_size <? 8192 then block_size else 8192 ≤ 8192

destruct stat_ok && 0 <? block_size && block_size <? 8192 eqn: E ; | lia

stat_ok :
bool
block_size :
Z
E :
stat_ok && 0 <? block_size && block_size <? 8192 = true
⊢
0 < block_size ≤ 8192

apply andb_true_iff in E as E Hhi

stat_ok :
bool
block_size :
Z
E :
stat_ok && 0 <? block_size = true
Hhi :
block_size <? 8192 = true
⊢
0 < block_size ≤ 8192

apply andb_true_iff in E as _ Hlo

stat_ok :
bool
block_size :
Z
Hlo :
0 <? block_size = true
Hhi :
block_size <? 8192 = true
⊢
0 < block_size ≤ 8192

apply Z.ltb_lt in Hhi

stat_ok :
bool
block_size :
Z
Hlo :
0 <? block_size = true
Hhi :
block_size < 8192
⊢
0 < block_size ≤ 8192

apply Z.ltb_lt in Hlo

stat_ok :
bool
block_size :
Z
Hlo :
0 < block_size
Hhi :
block_size < 8192
⊢
0 < block_size ≤ 8192

lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros
destruct stat_ok && 0 <? block_size && block_size <? 8192 eqn: E ; | lia
apply andb_true_iff in E as E Hhi
apply andb_true_iff in E as _ Hlo
apply Z.ltb_lt in Hhi
apply Z.ltb_lt in Hlo
lia

Where stdout's buffer lives: no buffer yet, the one-byte buffer embedded in the FILE (_shortbuf), or a heap buffer of size bytes at base.

47Inductive buffer_storage: Type ≔
|NoBuffer
|ShortBuffer
|HeapBuffer
base size : Z

Why libio picks a buffer: one already exists, the stream is unbuffered, malloc returned base, or malloc returned NULL. These causes describe libio's control flow, not R.alloc's result. MallocNull is useful for generic libio, but is excluded at this pin. Unbuffered is for a byte stream: wide orientation takes another path.

57Inductive buffer_cause: Type ≔
|Existing
|Unbuffered
|MallocSuccess
base : Z
|MallocNull

Generic libio's buffer choice, from the old storage for a cause to the new: an existing buffer is kept; with no buffer, an unbuffered stream or a NULL malloc falls back to the embedded byte, and a successful malloc gives a heap buffer of the given capacity.

64Inductive buffer_choicecapacity : Z : buffer_storage → buffer_cause → buffer_storage → Prop ≔
∀ storage
storage ≠ NoBuffer
choice_existing
buffer_choicecapacity storage Existing storage
choice_unbuffered
∀ base
choice_allocated

The pin's buffer choice: a buffer_choice whose cause is not a NULL malloc, since this glibc's malloc ends the run on refusal instead.

75Definition pinned_choicecapacity : Z old : buffer_storage cause : buffer_cause new : buffer_storage : Prop ≔
buffer_choicecapacity old cause new ∧ cause ≠ MallocNull

Measured pointer slots and writable roots

The pointers, with their capabilities, through which stdout's state is reached: the FILE, its lock, and errno.

83Record stdout_roots: Type ≔ mkStdoutRoots
file_ptr
 : ptr
lock_ptr
 : ptr
errno_ptr
 : ptr

The writable spans of the FILE, lock and errno. stdfiles.c allocates _IO_FILE_plus: FILE (216) plus its vtable pointer (8). NPTL's lock is { int lock; int cnt; void *owner; }. errno is a separate four-byte TLS cell. These spans are authority supplied by the caller of the trusted boundary, never inferred just from the addresses stored in FILE.

95Definition fixed_rootsr : stdout_roots : listspan ≔

A pointer to the FILE's embedded one-byte buffer (_shortbuf, at offset 131), with the FILE's own capability.

100Definition short_ptrr : stdout_roots : ptr ≔

The span of the buffer the storage names: none, the embedded byte, or the heap buffer with an Obj capability for its base.

105Definition buffer_spanr : stdout_roots storage : buffer_storage : optionspan ≔
match storage with
⇒
None
HeapBufferbase size
⇒
SomemkSpanmkPtrbase Objbase size

All of stdout's writable roots: the fixed_roots, plus a heap buffer's span. The embedded byte needs no root of its own: it is inside the FILE's.

115Definition memory_rootsr : stdout_roots storage : buffer_storage : listspan ≔
++
match storage with
HeapBufferbase size
⇒
mkSpanmkPtrbase Objbase size
_
⇒
[ ]

In memory m, the FILE's _IO_buf_base and _IO_buf_end slots (offsets 56 and 64) hold, as a pointer_slot with address bytes and aux, the start and end of the storage's buffer, or null when there is none. The end pointer keeps the buffer's capability.

126Definition buffer_slotsm : mem r : stdout_roots storage : buffer_storage : Prop ≔
let a ≔ ptr_addrfile_ptrr in
match buffer_spanr storage with

Memory m holds stdout's selected state for roots r and storage:

  • every root of memory_roots is a writable_span;
  • the whole FILE and its three pointer slots (56, 64 and the lock slot 136) are readable, 8-aligned; the lock and errno writable;
  • the lock slot points at the lock, and buffer_slots holds;
  • a heap buffer is nonempty and a live heap object.

This view supplies actual address bytes and aux, not a detached logical list of roots. Heap kind, liveness and buffer bounds are checked independently of the two pointer slots. It intentionally does not describe ownership, flags, orientation, pending bytes or lock state. These are selected roots, NOT a complete puts footprint: storing THREAD_SELF in lock.owner needs another capability source.

149Definition stdout_memorym : mem r : stdout_roots storage : buffer_storage : Prop ≔
Forallwritable_spanm memory_rootsr storage
∧
∧
Forallλoffset ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
∧
∧
∧
∧
buffer_slotsm r storage
∧
match storage with
HeapBufferbase size
⇒
0 < size ∧ ∃reg, object_regionbase m_regionsm = Somereg ∧ r_kindreg = Heap ∧ r_lifereg = Live
_
⇒
True

The stdio_world this view gives: a usable stdout whose roots are memory_roots.

167Definition memory_worldr : stdout_roots storage : buffer_storage : stdio_world ≔

Where stdout_memory holds, its world is stdio_ready, as puts_pre requires.

172Theorem stdout_memory_ready
∀ m r storage
stdout_memorym r storage
Explore proof 2 tactics

Initial goal

⊢
∀m : mem r : stdout_roots storage : buffer_storage, stdout_memorym r storage → stdio_readym memory_worldr storage

intros m r storage H _

split ; reflexivity | exact H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m r storage H _
split ; reflexivity | exact H

Where the fixed roots are writable, the embedded buffer's capability is available from them and its byte is under their write authority: it neither allocates nor expands root authority. Its one byte is already inside the FILE root, with the SAME capability.

180Theorem short_buffer_delegates
Explore proof 16 tactics

Initial goal

intros m r Hroots

split

2 open

focused goal
⊢
∀a : Z, span_containsspan_ptr ≔ short_ptrr; span_size ≔ 1 a → write_authorityfixed_rootsr [ ] m a

–right

2 open

⊢
∃s : span, Ins fixed_rootsr ∧ ptr_capshort_ptrr = ptr_capspan_ptrs ∨ ∃s : span a : Z, Ins fixed_rootsr ∧ span_containss a ∧ a + 8 ≤ ptr_addrspan_ptrs + span_sizes ∧ access_resm a ptr_capspan_ptrs 8 Read 8 = Someok ∧ ptr_capshort_ptrr = m_auxm a ∨ ∃base : Z, Inbase [ ] ∧ ptr_capshort_ptrr = Objbase ∨ ptr_capshort_ptrr = Robase
deferred goal
⊢
∀a : Z, span_containsspan_ptr ≔ short_ptrr; span_size ≔ 1 a → write_authorityfixed_rootsr [ ] m a

left

2 open

deferred goal
⊢
∀a : Z, span_containsspan_ptr ≔ short_ptrr; span_size ≔ 1 a → write_authorityfixed_rootsr [ ] m a

exists mkSpanfile_ptrr 224

2 open

deferred goal
⊢
∀a : Z, span_containsspan_ptr ≔ short_ptrr; span_size ≔ 1 a → write_authorityfixed_rootsr [ ] m a

simpl

2 open

⊢
span_ptr ≔ file_ptrr; span_size ≔ 224 = span_ptr ≔ file_ptrr; span_size ≔ 224 ∨ span_ptr ≔ lock_ptrr; span_size ≔ 16 = span_ptr ≔ file_ptrr; span_size ≔ 224 ∨ span_ptr ≔ errno_ptrr; span_size ≔ 4 = span_ptr ≔ file_ptrr; span_size ≔ 224 ∨ False ∧ ptr_capfile_ptrr = ptr_capfile_ptrr
deferred goal
⊢
∀a : Z, span_containsspan_ptr ≔ short_ptrr; span_size ≔ 1 a → write_authorityfixed_rootsr [ ] m a

auto

deferred goal
⊢
∀a : Z, span_containsspan_ptr ≔ short_ptrr; span_size ≔ 1 a → write_authorityfixed_rootsr [ ] m a

–intros a Ha

left

⊢
∃s : span, Ins fixed_rootsr ∧ writable_spanm s ∧ span_containss a

exists mkSpanfile_ptrr 224

inversion Hroots as | s rest Hw Hrest ; subst

m :
Hroots :
a :
Z
Hrest :
Forallwritable_spanm span_ptr ≔ lock_ptrr; span_size ≔ 16; span_ptr ≔ errno_ptrr; span_size ≔ 4
⊢

split ; simpl ; auto |

m :
Hroots :
a :
Z
Hrest :
Forallwritable_spanm span_ptr ≔ lock_ptrr; span_size ≔ 16; span_ptr ≔ errno_ptrr; span_size ≔ 4

split ; exact Hw |

m :
Hroots :
a :
Z
Hrest :
Forallwritable_spanm span_ptr ≔ lock_ptrr; span_size ≔ 16; span_ptr ≔ errno_ptrr; span_size ≔ 4

unfold span_contains , short_ptr in *

simpl in *

m :
Hroots :
a :
Z
Ha :
ptr_addrfile_ptrr + 131 ≤ a < ptr_addrfile_ptrr + 131 + 1
Hrest :
Forallwritable_spanm span_ptr ≔ lock_ptrr; span_size ≔ 16; span_ptr ≔ errno_ptrr; span_size ≔ 4
⊢

lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m r Hroots
split
–right
left
exists mkSpanfile_ptrr 224
simpl
auto
–intros a Ha
left
exists mkSpanfile_ptrr 224
inversion Hroots as | s rest Hw Hrest ; subst
split ; simpl ; auto |
split ; exact Hw |
unfold span_contains , short_ptr in *
simpl in *
lia

Installing a buffer from the null-buffer state

This is _IO_setb's selected no-old-buffer case. The two pointer stores change bytes AND aux; the four-byte flags store changes only _IO_USER_BUF. No release is hidden in this construction. Selection of this path still needs NoBuffer and backend/mode premises.

199Definition install_bufferm : mem r : stdout_roots storage : buffer_storage : mem ≔
match buffer_spanr storage with
None
⇒
m
Somes
⇒
let a ≔ ptr_addrfile_ptrr in
let p ≔ span_ptrs in
let m1 ≔ store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp in
let m2 ≔ store_auxstore_bytesm1 a + 64 8 ptr_addrp + span_sizes a + 64 ptr_capp in
match storage with
⇒
Z.landload_bytesm a 4 −2
_
⇒
Z.lorload_bytesm a 4 1
215Theorem installed_buffer_slots
∀ m r storage s
buffer_spanr storage = Somes
0 ≤ ptr_addrspan_ptrs < 2 ^ 64
0 ≤ ptr_addrspan_ptrs + span_sizes < 2 ^ 64
buffer_slotsinstall_bufferm r storage r storage
Explore proof 11 tactics

Initial goal

⊢
∀m : mem r : stdout_roots storage : buffer_storage s : span, buffer_spanr storage = Somes → 0 ≤ ptr_addrspan_ptrs < 2 ^ 64 → 0 ≤ ptr_addrspan_ptrs + span_sizes < 2 ^ 64 → buffer_slotsinstall_bufferm r storage r storage

intros m r storage s Hs Hp Hend

m :
s :
Hs :
buffer_spanr storage = Somes
Hp :
0 ≤ ptr_addrspan_ptrs < 2 ^ 64
Hend :
0 ≤ ptr_addrspan_ptrs + span_sizes < 2 ^ 64
⊢
buffer_slotsinstall_bufferm r storage r storage

unfold buffer_slots , install_buffer

m :
s :
Hs :
buffer_spanr storage = Somes
Hp :
0 ≤ ptr_addrspan_ptrs < 2 ^ 64
Hend :
0 ≤ ptr_addrspan_ptrs + span_sizes < 2 ^ 64
⊢
match buffer_spanr storage with

rewrite Hs

split

2 open

focused goal

–apply pointer_slot_bytes_disjoint ; lia | right ; simpl ; lia |

2 open

deferred goal

eapply pointer_slot_pointer_disjoint with p := mkPtrptr_addrspan_ptrs + span_sizes ptr_capspan_ptrs ; left ; lia |

2 open

deferred goal

apply pointer_slot_written

2 open

m :
s :
Hs :
buffer_spanr storage = Somes
Hp :
0 ≤ ptr_addrspan_ptrs < 2 ^ 64
Hend :
0 ≤ ptr_addrspan_ptrs + span_sizes < 2 ^ 64
⊢
0 ≤ ptr_addrspan_ptrs < 2 ^ 64
deferred goal

exact Hp

deferred goal

–apply pointer_slot_bytes_disjoint ; lia | right ; simpl ; lia |

apply pointer_slot_written_ _ mkPtrptr_addrspan_ptrs + span_sizes ptr_capspan_ptrs

m :
s :
Hs :
buffer_spanr storage = Somes
Hp :
0 ≤ ptr_addrspan_ptrs < 2 ^ 64
Hend :
0 ≤ ptr_addrspan_ptrs + span_sizes < 2 ^ 64
⊢

exact Hend

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m r storage s Hs Hp Hend
rewrite Hs
split
–apply pointer_slot_bytes_disjoint ; lia | right ; simpl ; lia |
exact Hp
–apply pointer_slot_bytes_disjoint ; lia | right ; simpl ; lia |
exact Hend
231Theorem installed_user_buffer_flag
∀ m r storage s
buffer_spanr storage = Somes
=
match storage with
mod
2 ^ 32
Explore proof 5 tactics

Initial goal

⊢
∀ m : mem r : stdout_roots storage : buffer_storage s : span  ,
buffer_spanr storage = Somes
→
=
match storage with
mod
2 ^ 32

intros m r storage s Hs

m :
s :
Hs :
buffer_spanr storage = Somes
⊢
=
match storage with
mod
2 ^ 32

unfold install_buffer

rewrite Hs

rewrite stored_bytes_value by lia

m :
s :
Hs :
buffer_spanr storage = Somes
⊢
match storage with
mod
256 ^ 4
=
match storage with
mod
2 ^ 32

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m r storage s Hs
rewrite Hs
rewrite stored_bytes_value by lia
reflexivity
243Lemma file_write_authority
Explore proof 6 tactics

Initial goal

⊢
∀m : mem r : stdout_roots born : listZ a : Z, Forallwritable_spanm fixed_rootsr → ptr_addrfile_ptrr ≤ a < ptr_addrfile_ptrr + 224 → write_authorityfixed_rootsr born m a

intros m r born a Hroots Ha

m :
born :
listZ
a :
Z
Hroots :
Ha :

left

m :
born :
listZ
a :
Z
Hroots :
Ha :
⊢
∃s : span, Ins fixed_rootsr ∧ writable_spanm s ∧ span_containss a

exists mkSpanfile_ptrr 224

m :
born :
listZ
a :
Z
Hroots :
Ha :
⊢

inversion Hroots as | s rest Hw Hrest ; subst

m :
born :
listZ
a :
Z
Hroots :
Ha :
Hrest :
Forallwritable_spanm span_ptr ≔ lock_ptrr; span_size ≔ 16; span_ptr ≔ errno_ptrr; span_size ≔ 4
⊢

split ; simpl ; auto |

m :
born :
listZ
a :
Z
Hroots :
Ha :
Hrest :
Forallwritable_spanm span_ptr ≔ lock_ptrr; span_size ≔ 16; span_ptr ≔ errno_ptrr; span_size ≔ 4

split ; auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m r born a Hroots Ha
left
exists mkSpanfile_ptrr 224
inversion Hroots as | s rest Hw Hrest ; subst
split ; simpl ; auto |
split ; auto

Fresh allocation leaves the null slots and every caller root valid. It does not install its address into FILE.

254Lemma no_buffer_allocated
Explore proof 14 tactics

Initial goal

⊢
∀m : mem r : stdout_roots q : alloc_req base : Z, stdout_memorym r NoBuffer → object_regionbase m_regionsm = None → stdout_memoryallocatedm q base r NoBuffer

intros m r q base Hroots & Hfile & Hfields & Hlock & Herr & Hslot & Hnull & _ Hnew

m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :

split

2 open

m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :
focused goal
m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :
⊢
access_resallocatedm q base ptr_addrfile_ptrr ptr_capfile_ptrr 224 Read 8 = Someok ∧ Forallλoffset : Z ⇒ access_resallocatedm q base ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136 ∧ access_resallocatedm q base ptr_addrlock_ptrr ptr_caplock_ptrr 16 Write 8 = Someok ∧ access_resallocatedm q base ptr_addrerrno_ptrr ptr_caperrno_ptrr 4 Write 4 = Someok ∧ pointer_slotallocatedm q base ptr_addrfile_ptrr + 136 lock_ptrr ∧ buffer_slotsallocatedm q base r NoBuffer ∧ True

–eapply Forall_impl ; | exact Hroots

2 open

m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :
⊢
∀a : span, writable_spanm a → writable_spanallocatedm q base a
deferred goal
m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :
⊢
access_resallocatedm q base ptr_addrfile_ptrr ptr_capfile_ptrr 224 Read 8 = Someok ∧ Forallλoffset : Z ⇒ access_resallocatedm q base ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136 ∧ access_resallocatedm q base ptr_addrlock_ptrr ptr_caplock_ptrr 16 Write 8 = Someok ∧ access_resallocatedm q base ptr_addrerrno_ptrr ptr_caperrno_ptrr 4 Write 4 = Someok ∧ pointer_slotallocatedm q base ptr_addrfile_ptrr + 136 lock_ptrr ∧ buffer_slotsallocatedm q base r NoBuffer ∧ True

intros span Hspan

2 open

m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :
span :
span
Hspan :
⊢
deferred goal
m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :
⊢
access_resallocatedm q base ptr_addrfile_ptrr ptr_capfile_ptrr 224 Read 8 = Someok ∧ Forallλoffset : Z ⇒ access_resallocatedm q base ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136 ∧ access_resallocatedm q base ptr_addrlock_ptrr ptr_caplock_ptrr 16 Write 8 = Someok ∧ access_resallocatedm q base ptr_addrerrno_ptrr ptr_caperrno_ptrr 4 Write 4 = Someok ∧ pointer_slotallocatedm q base ptr_addrfile_ptrr + 136 lock_ptrr ∧ buffer_slotsallocatedm q base r NoBuffer ∧ True

eapply allocated_old_span ; eauto

deferred goal
m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :
⊢
access_resallocatedm q base ptr_addrfile_ptrr ptr_capfile_ptrr 224 Read 8 = Someok ∧ Forallλoffset : Z ⇒ access_resallocatedm q base ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136 ∧ access_resallocatedm q base ptr_addrlock_ptrr ptr_caplock_ptrr 16 Write 8 = Someok ∧ access_resallocatedm q base ptr_addrerrno_ptrr ptr_caperrno_ptrr 4 Write 4 = Someok ∧ pointer_slotallocatedm q base ptr_addrfile_ptrr + 136 lock_ptrr ∧ buffer_slotsallocatedm q base r NoBuffer ∧ True

–split ; eapply allocated_old_access ; eauto |

m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :
⊢
Forallλoffset : Z ⇒ access_resallocatedm q base ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136 ∧ access_resallocatedm q base ptr_addrlock_ptrr ptr_caplock_ptrr 16 Write 8 = Someok ∧ access_resallocatedm q base ptr_addrerrno_ptrr ptr_caperrno_ptrr 4 Write 4 = Someok ∧ pointer_slotallocatedm q base ptr_addrfile_ptrr + 136 lock_ptrr ∧ buffer_slotsallocatedm q base r NoBuffer ∧ True

split

2 open

m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :
⊢
Forallλoffset : Z ⇒ access_resallocatedm q base ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
focused goal
m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :

+eapply Forall_impl ; | exact Hfields

2 open

m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :
⊢
∀a : Z, λoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someoka → access_resallocatedm q base ptr_addrfile_ptrr + a ptr_capfile_ptrr 8 Read 8 = Someok
deferred goal
m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :

intros offset Hfield

2 open

m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :
offset :
Z
Hfield :
λoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someokoffset
⊢
deferred goal
m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :

eapply allocated_old_access ; eauto

deferred goal
m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :

+split ; eapply allocated_old_access ; eauto |

m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :

split ; eapply allocated_old_access ; eauto |

m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :

split ; exact Hslot |

m :
base :
Z
Hfields :
Forallλoffset : Z ⇒ access_resm ptr_addrfile_ptrr + offset ptr_capfile_ptrr 8 Read 8 = Someok 56; 64; 136
Hnew :
⊢
buffer_slotsallocatedm q base r NoBuffer ∧ True

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m r q base Hroots & Hfile & Hfields & Hlock & Herr & Hslot & Hnull & _ Hnew
split
–eapply Forall_impl ; | exact Hroots
intros span Hspan
eapply allocated_old_span ; eauto
–split ; eapply allocated_old_access ; eauto |
split
+eapply Forall_impl ; | exact Hfields
intros offset Hfield
eapply allocated_old_access ; eauto
+split ; eapply allocated_old_access ; eauto |
split ; eapply allocated_old_access ; eauto |
split ; exact Hslot |
auto

Installation preserves the checked fixed fields and lock pointer; target root bounds and heap lifetime are independent obligations. In particular, matching slot bytes alone cannot prove this view.

270Theorem installed_memory
∀ m r storage span
buffer_spanr storage = Somespan
Forallwritable_spanm memory_rootsr storage
0 ≤ ptr_addrspan_ptrspan < 2 ^ 64
0 ≤ ptr_addrspan_ptrspan + span_sizespan < 2 ^ 64
match storage with
HeapBufferbase size
⇒
0 < size ∧ ∃reg, object_regionbase m_regionsm = Somereg ∧ r_kindreg = Heap ∧ r_lifereg = Live
_
⇒
True
stdout_memoryinstall_bufferm r storage r storage
Proof 26 steps Qed
intros m r storage span Hroots & Hfile & Hfields & Hlock & Herr & Hslot & Hnull & _ Hspan Hout Hp Hend Hheap
rewrite Hspan
reflexivity
split
rewrite Hregions
exact Hout
–split ; unfold access_res ; rewrite Hregions ; exact Hfile |
split
+unfold access_res
rewrite Hregions
exact Hfields
+split ; unfold access_res ; rewrite Hregions ; exact Hlock |
split ; unfold access_res ; rewrite Hregions ; exact Herr |
split
∗unfold install_buffer
rewrite Hspan
apply pointer_slot_bytes_disjoint ; lia | right ; lia |
apply pointer_slot_pointer_disjoint with p := span_ptrspan ; right ; lia | exact Hslot
∗split ; eapply installed_buffer_slots ; eauto |
destruct storage ; try exact I
rewrite Hregions
exact Hheap

Allocation evidence over any runtime

Buffer allocation over the caller's exact machine instance.

305Module LibioOn R : Runtime M : ExternalMachineSigR
306Module E ≔ M.E

The one allocation request stdout's buffer setup makes: 16-aligned, of file_capacity bytes.

310Definition buffer_requeststat_ok : bool block_size align size : Z : Prop ≔
align = 16 ∧ size = file_capacitystat_ok block_size

When the runtime, ready in state s and memory m, grants the buffer request at base: base was no object of m, the runtime stays ready, the allocation is an effects path with born list base, and the new object's Obj capability and its capacity bytes are the call's authority. No theorem turns a logical HeapBuffer into an allocated object. This theorem starts with the runtime's actual successful answer. Installing its pointer slots and native flags is still a separate local-effects obligation.

322Theorem allocate_buffer
∀ stat_ok block_size s m base s′ sources roots releases
R.readys m
R.allocs heap_req16 file_capacitystat_ok block_size = Somebase, s′
let size ≔ file_capacitystat_ok block_size in
let m′ ≔ allocatedm heap_req16 size base in
object_regionbase m_regionsm = None ∧ R.readys′ m′ ∧ E.effectssources roots releases buffer_requeststat_ok block_size s m [ ] s′ m′ base ∧ available_capsources base m′ Objbase ∧ ∀a, base ≤ a < base + size → write_authorityroots base m′ a
Proof 37 steps Qed
intros stat_ok block_size s m base s′ sources roots releases Hr Ha
pose proof file_capacity_boundsstat_ok block_size as Hb
assert He : 0 ≤ req_extentheap_req16 file_capacitystat_ok block_size
{simpl
apply Z.mul_nonneg_nonneg ; apply Z.div_pos ; lia | lia
destruct R.fresh_allocations m heap_req16 file_capacitystat_ok block_size base s' Hr ltac:simpl ; lia He Ha as Hfresh Hr′
destruct Hfresh as Hbase & Halign & Hend & Hnone & Hrest
split ; exact Hnone |
split ; exact Hr' |
split
–eapply E.effects_alloc with align := 16 size := file_capacitystat_ok block_size
+split ; reflexivity
+exact Ha
+constructor
–split
+right
right
right
exists base
simpl
auto
+intros a Hrange
right
exists base, mkRegionbase base + req_extentheap_req16 file_capacitystat_ok block_size Heap Live
split ; simpl ; auto |
split
∗simpl
rewrite Z.eqb_refl
reflexivity
∗split ; reflexivity |
split ; reflexivity |
simpl
pose proof Z.mod_pos_boundfile_capacitystat_ok block_size + 15 16 ltac:lia as Hmod
pose proof Z.div_modfile_capacitystat_ok block_size + 15 16 ltac:lia as Hdiv
lia

If the runtime refuses the buffer request, the call may end as OutOfMemory (resource_failure).

360Theorem buffer_refusal
∀ stat_ok block_size s
R.allocs heap_req16 file_capacitystat_ok block_size = None
Explore proof 7 tactics

Initial goal

⊢
∀stat_ok : bool block_size : Z s : R.state, R.allocs heap_req16 file_capacitystat_ok block_size = None → E.resource_failurebuffer_requeststat_ok block_size s OutOfMemory

intros stat_ok block_size s H

stat_ok :
bool
block_size :
Z
s :
R.state
H :
R.allocs heap_req16 file_capacitystat_ok block_size = None

pose proof file_capacity_boundsstat_ok block_size

stat_ok :
bool
block_size :
Z
s :
R.state
H :
R.allocs heap_req16 file_capacitystat_ok block_size = None
H0 :
0 < file_capacitystat_ok block_size ≤ 8192

eapply E.failure_oom with align := 16 size := file_capacitystat_ok block_size

3 open

stat_ok :
bool
block_size :
Z
s :
R.state
H :
R.allocs heap_req16 file_capacitystat_ok block_size = None
H0 :
0 < file_capacitystat_ok block_size ≤ 8192
⊢
buffer_requeststat_ok block_size 16 file_capacitystat_ok block_size
focused goal
stat_ok :
bool
block_size :
Z
s :
R.state
H :
R.allocs heap_req16 file_capacitystat_ok block_size = None
H0 :
0 < file_capacitystat_ok block_size ≤ 8192
⊢
0 ≤ file_capacitystat_ok block_size ≤ max_allocation_size
focused goal
stat_ok :
bool
block_size :
Z
s :
R.state
H :
R.allocs heap_req16 file_capacitystat_ok block_size = None
H0 :
0 < file_capacitystat_ok block_size ≤ 8192
⊢
R.allocs heap_req16 file_capacitystat_ok block_size = None

–split ; reflexivity

2 open

deferred goal
stat_ok :
bool
block_size :
Z
s :
R.state
H :
R.allocs heap_req16 file_capacitystat_ok block_size = None
H0 :
0 < file_capacitystat_ok block_size ≤ 8192
⊢
0 ≤ file_capacitystat_ok block_size ≤ max_allocation_size
deferred goal
stat_ok :
bool
block_size :
Z
s :
R.state
H :
R.allocs heap_req16 file_capacitystat_ok block_size = None
H0 :
0 < file_capacitystat_ok block_size ≤ 8192
⊢
R.allocs heap_req16 file_capacitystat_ok block_size = None

–unfold max_allocation_size

2 open

stat_ok :
bool
block_size :
Z
s :
R.state
H :
R.allocs heap_req16 file_capacitystat_ok block_size = None
H0 :
0 < file_capacitystat_ok block_size ≤ 8192
⊢
0 ≤ file_capacitystat_ok block_size ≤ 2 ^ 48 − 1
deferred goal
stat_ok :
bool
block_size :
Z
s :
R.state
H :
R.allocs heap_req16 file_capacitystat_ok block_size = None
H0 :
0 < file_capacitystat_ok block_size ≤ 8192
⊢
R.allocs heap_req16 file_capacitystat_ok block_size = None

lia

deferred goal
stat_ok :
bool
block_size :
Z
s :
R.state
H :
R.allocs heap_req16 file_capacitystat_ok block_size = None
H0 :
0 < file_capacitystat_ok block_size ≤ 8192
⊢
R.allocs heap_req16 file_capacitystat_ok block_size = None

–exact H

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros stat_ok block_size s H
pose proof file_capacity_boundsstat_ok block_size
eapply E.failure_oom with align := 16 size := file_capacitystat_ok block_size
–split ; reflexivity
lia
–exact H

The buffer request never fails as TooBig: its capacity is at most 8192 bytes.

374Theorem buffer_never_too_big
∀ stat_ok block_size s
Explore proof 5 tactics

Initial goal

⊢
∀stat_ok : bool block_size : Z s : R.state, ¬E.resource_failurebuffer_requeststat_ok block_size s TooBig

intros stat_ok block_size s H

stat_ok :
bool
block_size :
Z
s :
R.state
⊢
False

inversion H as | align size _ → Hbig

stat_ok :
bool
block_size :
Z
s :
R.state
align :
Z
Hbig :
max_allocation_size < file_capacitystat_ok block_size
⊢
False

pose proof file_capacity_boundsstat_ok block_size

stat_ok :
bool
block_size :
Z
s :
R.state
align :
Z
Hbig :
max_allocation_size < file_capacitystat_ok block_size
H0 :
0 < file_capacitystat_ok block_size ≤ 8192
⊢
False

unfold max_allocation_size in Hbig

stat_ok :
bool
block_size :
Z
s :
R.state
align :
Z
Hbig :
2 ^ 48 − 1 < file_capacitystat_ok block_size
H0 :
0 < file_capacitystat_ok block_size ≤ 8192
⊢
False

lia

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros stat_ok block_size s H
inversion H as | align size _ → Hbig
pose proof file_capacity_boundsstat_ok block_size
unfold max_allocation_size in Hbig
lia
381Theorem install_short_effects
∀ s m r requests
Explore proof 30 tactics

Initial goal

⊢
∀s : R.state m : mem r : stdout_roots requests : Z → Z → Prop, stdout_memorym r NoBuffer → E.effectsfixed_rootsr fixed_rootsr [ ] requests s m [ ] s install_bufferm r ShortBuffer [ ]

intros s m r requests Hroots _

s :
R.state
m :
requests :
Z → Z → Prop
⊢

set a := ptr_addrfile_ptrr

s :
R.state
m :
requests :
Z → Z → Prop
⊢

set p := short_ptrr

s :
R.state
m :
requests :
Z → Z → Prop
p :=
⊢

set m1 := store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
⊢

set m2 := store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
⊢

set m3 := store_bytesm2 a 4 Z.lorload_bytesm a 4 1

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢

change E.effectsfixed_rootsr fixed_rootsr [ ] requests s m [ ] s m3 [ ]

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m [ ] s m3 [ ]

eapply E.effects_local with m1 := m1

2 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
focused goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 [ ] s m3 [ ]

–apply local_store_pointer with p := p

3 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
∀b : Z, a + 56 ≤ b < a + 56 + 8 → write_authorityfixed_rootsr [ ] m b
focused goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 [ ] s m3 [ ]

+intros b Hb

3 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
b :
Z
Hb :
a + 56 ≤ b < a + 56 + 8
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 [ ] s m3 [ ]

apply file_write_authority ; exact Hroots | simpl in * ; lia

2 open

deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 [ ] s m3 [ ]

+right

2 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
∃s0 : span, Ins0 fixed_rootsr ∧ ptr_capp = ptr_capspan_ptrs0 ∨ ∃s0 : span a0 : Z, Ins0 fixed_rootsr ∧ span_containss0 a0 ∧ a0 + 8 ≤ ptr_addrspan_ptrs0 + span_sizes0 ∧ access_resm a0 ptr_capspan_ptrs0 8 Read 8 = Someok ∧ ptr_capp = m_auxm a0 ∨ ∃base : Z, Inbase [ ] ∧ ptr_capp = Objbase ∨ ptr_capp = Robase
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 [ ] s m3 [ ]

left

2 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
∃s0 : span, Ins0 fixed_rootsr ∧ ptr_capp = ptr_capspan_ptrs0
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 [ ] s m3 [ ]

exists mkSpanfile_ptrr 224

2 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 [ ] s m3 [ ]

simpl

2 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
span_ptr ≔ file_ptrr; span_size ≔ 224 = span_ptr ≔ file_ptrr; span_size ≔ 224 ∨ span_ptr ≔ lock_ptrr; span_size ≔ 16 = span_ptr ≔ file_ptrr; span_size ≔ 224 ∨ span_ptr ≔ errno_ptrr; span_size ≔ 4 = span_ptr ≔ file_ptrr; span_size ≔ 224 ∨ False ∧ ptr_capfile_ptrr = ptr_capfile_ptrr
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 [ ] s m3 [ ]

auto

deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 [ ] s m3 [ ]

–eapply E.effects_local with m1 := m2

2 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
focused goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 [ ] s m3 [ ]

+apply local_store_pointer with p := mkPtrptr_addrp + 1 ptr_capp

3 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
∀b : Z, a + 64 ≤ b < a + 64 + 8 → write_authorityfixed_rootsr [ ] m1 b
focused goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 [ ] s m3 [ ]

∗intros b Hb

3 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
b :
Z
Hb :
a + 64 ≤ b < a + 64 + 8
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 [ ] s m3 [ ]

apply file_write_authority ; exact Hroots | simpl in * ; lia

2 open

deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 [ ] s m3 [ ]

∗right

2 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
∃s0 : span, Ins0 fixed_rootsr ∧ ptr_capptr_addr ≔ ptr_addrp + 1; ptr_cap ≔ ptr_capp = ptr_capspan_ptrs0 ∨ ∃s0 : span a0 : Z, Ins0 fixed_rootsr ∧ span_containss0 a0 ∧ a0 + 8 ≤ ptr_addrspan_ptrs0 + span_sizes0 ∧ access_resm1 a0 ptr_capspan_ptrs0 8 Read 8 = Someok ∧ ptr_capptr_addr ≔ ptr_addrp + 1; ptr_cap ≔ ptr_capp = m_auxm1 a0 ∨ ∃base : Z, Inbase [ ] ∧ ptr_capptr_addr ≔ ptr_addrp + 1; ptr_cap ≔ ptr_capp = Objbase ∨ ptr_capptr_addr ≔ ptr_addrp + 1; ptr_cap ≔ ptr_capp = Robase
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 [ ] s m3 [ ]

left

2 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
∃s0 : span, Ins0 fixed_rootsr ∧ ptr_capptr_addr ≔ ptr_addrp + 1; ptr_cap ≔ ptr_capp = ptr_capspan_ptrs0
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 [ ] s m3 [ ]

exists mkSpanfile_ptrr 224

2 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 [ ] s m3 [ ]

simpl

2 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
span_ptr ≔ file_ptrr; span_size ≔ 224 = span_ptr ≔ file_ptrr; span_size ≔ 224 ∨ span_ptr ≔ lock_ptrr; span_size ≔ 16 = span_ptr ≔ file_ptrr; span_size ≔ 224 ∨ span_ptr ≔ errno_ptrr; span_size ≔ 4 = span_ptr ≔ file_ptrr; span_size ≔ 224 ∨ False ∧ ptr_capfile_ptrr = ptr_capfile_ptrr
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 [ ] s m3 [ ]

auto

deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 [ ] s m3 [ ]

+eapply E.effects_local with m1 := m3

2 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
focused goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m3 [ ] s m3 [ ]

∗apply local_store_bytes

2 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
∀b : Z, a ≤ b < a + 4 → write_authorityfixed_rootsr [ ] m2 b
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m3 [ ] s m3 [ ]

intros b Hb

2 open

s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
b :
Z
Hb :
a ≤ b < a + 4
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m3 [ ] s m3 [ ]

apply file_write_authority ; exact Hroots | simpl in * ; lia

deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
p :=
m1 :=
store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp : mem
m3 :=
store_bytesm2 a 4 Z.lorload_bytesm a 4 1 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m3 [ ] s m3 [ ]

∗constructor

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros s m r requests Hroots _
set a := ptr_addrfile_ptrr
set p := short_ptrr
set m1 := store_auxstore_bytesm a + 56 8 ptr_addrp a + 56 ptr_capp
set m2 := store_auxstore_bytesm1 a + 64 8 ptr_addrp + 1 a + 64 ptr_capp
set m3 := store_bytesm2 a 4 Z.lorload_bytesm a 4 1
change E.effectsfixed_rootsr fixed_rootsr [ ] requests s m [ ] s m3 [ ]
eapply E.effects_local with m1 := m1
–apply local_store_pointer with p := p
+intros b Hb
apply file_write_authority ; exact Hroots | simpl in * ; lia
+right
left
exists mkSpanfile_ptrr 224
simpl
auto
–eapply E.effects_local with m1 := m2
+apply local_store_pointer with p := mkPtrptr_addrp + 1 ptr_capp
∗intros b Hb
apply file_write_authority ; exact Hroots | simpl in * ; lia
∗right
left
exists mkSpanfile_ptrr 224
simpl
auto
+eapply E.effects_local with m1 := m3
intros b Hb
apply file_write_authority ; exact Hroots | simpl in * ; lia
∗constructor
406Theorem install_heap_effects
∀ s m r requests born base size
Inbase born
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m born s install_bufferm r HeapBufferbase size born
Explore proof 29 tactics

Initial goal

⊢
∀s : R.state m : mem r : stdout_roots requests : Z → Z → Prop born : listZ base size : Z, stdout_memorym r NoBuffer → Inbase born → E.effectsfixed_rootsr fixed_rootsr [ ] requests s m born s install_bufferm r HeapBufferbase size born

intros s m r requests born base size Hroots _ Hborn

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m born s install_bufferm r HeapBufferbase size born

set a := ptr_addrfile_ptrr

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m born s install_bufferm r HeapBufferbase size born

set m1 := store_auxstore_bytesm a + 56 8 base a + 56 Objbase

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m born s install_bufferm r HeapBufferbase size born

set m2 := store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m born s install_bufferm r HeapBufferbase size born

set m3 := store_bytesm2 a 4 Z.landload_bytesm a 4 −2

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m born s install_bufferm r HeapBufferbase size born

change E.effectsfixed_rootsr fixed_rootsr [ ] requests s m born s m3 born

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m born s m3 born

eapply E.effects_local with m1 := m1

2 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
focused goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 born s m3 born

–apply local_store_pointer with p := mkPtrbase Objbase

3 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
∀b : Z, a + 56 ≤ b < a + 56 + 8 → write_authorityfixed_rootsr born m b
focused goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 born s m3 born

+intros b Hb

3 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
b :
Z
Hb :
a + 56 ≤ b < a + 56 + 8
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 born s m3 born

apply file_write_authority ; exact Hroots | simpl in * ; lia

2 open

deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 born s m3 born

+right

2 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
∃s0 : span, Ins0 fixed_rootsr ∧ ptr_capptr_addr ≔ base; ptr_cap ≔ Objbase = ptr_capspan_ptrs0 ∨ ∃s0 : span a0 : Z, Ins0 fixed_rootsr ∧ span_containss0 a0 ∧ a0 + 8 ≤ ptr_addrspan_ptrs0 + span_sizes0 ∧ access_resm a0 ptr_capspan_ptrs0 8 Read 8 = Someok ∧ ptr_capptr_addr ≔ base; ptr_cap ≔ Objbase = m_auxm a0 ∨ ∃base0 : Z, Inbase0 born ∧ ptr_capptr_addr ≔ base; ptr_cap ≔ Objbase = Objbase0 ∨ ptr_capptr_addr ≔ base; ptr_cap ≔ Objbase = Robase0
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 born s m3 born

right

2 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
∃s0 : span a0 : Z, Ins0 fixed_rootsr ∧ span_containss0 a0 ∧ a0 + 8 ≤ ptr_addrspan_ptrs0 + span_sizes0 ∧ access_resm a0 ptr_capspan_ptrs0 8 Read 8 = Someok ∧ ptr_capptr_addr ≔ base; ptr_cap ≔ Objbase = m_auxm a0 ∨ ∃base0 : Z, Inbase0 born ∧ ptr_capptr_addr ≔ base; ptr_cap ≔ Objbase = Objbase0 ∨ ptr_capptr_addr ≔ base; ptr_cap ≔ Objbase = Robase0
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 born s m3 born

right

2 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
∃base0 : Z, Inbase0 born ∧ ptr_capptr_addr ≔ base; ptr_cap ≔ Objbase = Objbase0 ∨ ptr_capptr_addr ≔ base; ptr_cap ≔ Objbase = Robase0
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 born s m3 born

exists base

2 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
Inbase born ∧ ptr_capptr_addr ≔ base; ptr_cap ≔ Objbase = Objbase ∨ ptr_capptr_addr ≔ base; ptr_cap ≔ Objbase = Robase
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 born s m3 born

auto

deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m1 born s m3 born

–eapply E.effects_local with m1 := m2

2 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
focused goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 born s m3 born

+apply local_store_pointer with p := mkPtrbase + size Objbase

3 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
∀b : Z, a + 64 ≤ b < a + 64 + 8 → write_authorityfixed_rootsr born m1 b
focused goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
available_capfixed_rootsr born m1 ptr_capptr_addr ≔ base + size; ptr_cap ≔ Objbase
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 born s m3 born

∗intros b Hb

3 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
b :
Z
Hb :
a + 64 ≤ b < a + 64 + 8
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
available_capfixed_rootsr born m1 ptr_capptr_addr ≔ base + size; ptr_cap ≔ Objbase
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 born s m3 born

apply file_write_authority ; exact Hroots | simpl in * ; lia

2 open

deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
available_capfixed_rootsr born m1 ptr_capptr_addr ≔ base + size; ptr_cap ≔ Objbase
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 born s m3 born

∗right

2 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
∃s0 : span, Ins0 fixed_rootsr ∧ ptr_capptr_addr ≔ base + size; ptr_cap ≔ Objbase = ptr_capspan_ptrs0 ∨ ∃s0 : span a0 : Z, Ins0 fixed_rootsr ∧ span_containss0 a0 ∧ a0 + 8 ≤ ptr_addrspan_ptrs0 + span_sizes0 ∧ access_resm1 a0 ptr_capspan_ptrs0 8 Read 8 = Someok ∧ ptr_capptr_addr ≔ base + size; ptr_cap ≔ Objbase = m_auxm1 a0 ∨ ∃base0 : Z, Inbase0 born ∧ ptr_capptr_addr ≔ base + size; ptr_cap ≔ Objbase = Objbase0 ∨ ptr_capptr_addr ≔ base + size; ptr_cap ≔ Objbase = Robase0
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 born s m3 born

right

2 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
∃s0 : span a0 : Z, Ins0 fixed_rootsr ∧ span_containss0 a0 ∧ a0 + 8 ≤ ptr_addrspan_ptrs0 + span_sizes0 ∧ access_resm1 a0 ptr_capspan_ptrs0 8 Read 8 = Someok ∧ ptr_capptr_addr ≔ base + size; ptr_cap ≔ Objbase = m_auxm1 a0 ∨ ∃base0 : Z, Inbase0 born ∧ ptr_capptr_addr ≔ base + size; ptr_cap ≔ Objbase = Objbase0 ∨ ptr_capptr_addr ≔ base + size; ptr_cap ≔ Objbase = Robase0
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 born s m3 born

right

2 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
∃base0 : Z, Inbase0 born ∧ ptr_capptr_addr ≔ base + size; ptr_cap ≔ Objbase = Objbase0 ∨ ptr_capptr_addr ≔ base + size; ptr_cap ≔ Objbase = Robase0
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 born s m3 born

exists base

2 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
Inbase born ∧ ptr_capptr_addr ≔ base + size; ptr_cap ≔ Objbase = Objbase ∨ ptr_capptr_addr ≔ base + size; ptr_cap ≔ Objbase = Robase
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 born s m3 born

auto

deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m2 born s m3 born

+eapply E.effects_local with m1 := m3

2 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
focused goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m3 born s m3 born

∗apply local_store_bytes

2 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
∀b : Z, a ≤ b < a + 4 → write_authorityfixed_rootsr born m2 b
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m3 born s m3 born

intros b Hb

2 open

s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
b :
Z
Hb :
a ≤ b < a + 4
deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m3 born s m3 born

apply file_write_authority ; exact Hroots | simpl in * ; lia

deferred goal
s :
R.state
m :
requests :
Z → Z → Prop
born :
listZ
base, size :
Z
Hborn :
Inbase born
m1 :=
store_auxstore_bytesm a + 56 8 base a + 56 Objbase : mem
m2 :=
store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase : mem
m3 :=
store_bytesm2 a 4 Z.landload_bytesm a 4 −2 : mem
⊢
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m3 born s m3 born

∗constructor

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros s m r requests born base size Hroots _ Hborn
set a := ptr_addrfile_ptrr
set m1 := store_auxstore_bytesm a + 56 8 base a + 56 Objbase
set m2 := store_auxstore_bytesm1 a + 64 8 base + size a + 64 Objbase
set m3 := store_bytesm2 a 4 Z.landload_bytesm a 4 −2
change E.effectsfixed_rootsr fixed_rootsr [ ] requests s m born s m3 born
eapply E.effects_local with m1 := m1
–apply local_store_pointer with p := mkPtrbase Objbase
+intros b Hb
apply file_write_authority ; exact Hroots | simpl in * ; lia
+right
right
right
exists base
auto
–eapply E.effects_local with m1 := m2
+apply local_store_pointer with p := mkPtrbase + size Objbase
∗intros b Hb
apply file_write_authority ; exact Hroots | simpl in * ; lia
∗right
right
right
exists base
auto
+eapply E.effects_local with m1 := m3
intros b Hb
apply file_write_authority ; exact Hroots | simpl in * ; lia
∗constructor
431Theorem setup_short
∀ s m r requests
R.readys m
let m′ ≔ install_bufferm r ShortBuffer in
E.effectsfixed_rootsr fixed_rootsr [ ] requests s m [ ] s m′ [ ] ∧ R.readys m′ ∧ persistsm m′ ∧ stdout_memorym′ r ShortBuffer ∧ stdio_delegatesfixed_rootsr [ ] m′ memory_worldr ShortBuffer
Proof 31 steps Qed
intros s m r requests Hr Hmem
pose proof install_short_effectss m r requests Hmem as He
destruct E.effects_preserve_ _ _ _ _ _ _ _ _ _ He Hr as Hr′ Hpersist
destruct Hmem as Hroots Hrest
inversion Hroots as | span rest Hw Htail ; subst
destruct Hw as _ & base & reg & Hcap & Hreg & Hlive & Haccess
destruct R.address_spaces m Hr base reg Hreg as Hlo Hhi
change access_resm ptr_addrfile_ptrr Objbase 224 Write 1 = Someok in Haccess
unfold access_res , cap_access_res in Haccess
rewrite Hreg in Haccess
destruct base ≤? ptr_addrfile_ptrr && ptr_addrfile_ptrr + 224 ≤? r_endreg eqn: E ; try discriminate Haccess
apply andb_true_iff in E as E1 E2
apply Z.leb_le in E1
apply Z.leb_le in E2
{eapply installed_memory with span := mkSpanshort_ptrr 1
–split ; assumption
–reflexivity
–exact Hroots
–unfold short_ptr
simpl
lia
–unfold short_ptr
simpl
lia
–exact I
split ; exact He |
split ; exact Hr' |
split ; exact Hpersist |
split ; exact Hpost |
apply stdio_delegates_refl ; reflexivity | exact proj1Hpost
462Theorem setup_heap
∀ stat_ok block_size s m r base s′
R.readys m
R.allocs heap_req16 file_capacitystat_ok block_size = Somebase, s′
let size ≔ file_capacitystat_ok block_size in
let m1 ≔ allocatedm heap_req16 size base in
let m′ ≔ install_bufferm1 r HeapBufferbase size in
E.effectsfixed_rootsr fixed_rootsr [ ] buffer_requeststat_ok block_size s m [ ] s′ m′ base ∧ R.readys′ m′ ∧ persistsm m′ ∧ stdout_memorym′ r HeapBufferbase size ∧ stdio_delegatesfixed_rootsr base m′ memory_worldr HeapBufferbase size
Proof 92 steps Qed
intros stat_ok block_size s m r base s′ Hr Hmem Ha
set size := file_capacitystat_ok block_size
set q := heap_req16 size
set m1 := allocatedm q base
pose proof file_capacity_boundsstat_ok block_size as Hsize
change 0 < size ≤ 8192 in Hsize
assert Hfit : size ≤ req_extentq
{unfold q , heap_req
simpl
pose proof Z.mod_pos_boundsize + 15 16 ltac:lia
pose proof Z.div_modsize + 15 16 ltac:lia
lia
destruct allocate_bufferstat_ok block_size s m base s' fixed_rootsr fixed_rootsr [ ] Hr Ha as Hnew & Hr1 & Healloc & Hcap & Hauthority
change R.readys' m1 in Hr1
pose proof no_buffer_allocatedm r q base Hmem Hnew as Hmem1
assert Hreg : object_regionbase m_regionsm1 = SomemkRegionbase base + req_extentq Heap Live
{unfold m1 , allocated
simpl
rewrite Z.eqb_refl
reflexivity
destruct R.address_spaces' m1 Hr1 _ _ Hreg as Hbase Hend
change base + req_extentq ≤ 2 ^ 48 in Hend
assert Hw : writable_spanm1 mkSpanmkPtrbase Objbase size
{split ; simpl ; lia |
exists base, mkRegionbase base + req_extentq Heap Live
split ; reflexivity |
split ; exact Hreg |
split ; reflexivity |
change cap_access_resObjbase m_regionsm1 base size Write 1 = Someok
rewrite Hreg
change Someif base ≤? base && base + size ≤? base + req_extentq then aligned_resbase 1 else RTrapOutOfBounds = Someok
assert base ≤? base && base + size ≤? base + req_extentq = true as E
{apply andb_true_iff
split ; apply Z.leb_le ; lia
rewrite E
rewrite Z.mod_1_r
reflexivity
pose proof install_heap_effectss' m1 r buffer_requeststat_ok block_size base base size Hmem1 ltac:simpl ; auto as Hetail
assert He : E.effectsfixed_rootsr fixed_rootsr [ ] buffer_requeststat_ok block_size s m [ ] s' install_bufferm1 r HeapBufferbase size base
{eapply E.effects_alloc with align := 16 size := size
–split ; reflexivity
lia
–exact Ha
–exact Hetail
destruct E.effects_preserve_ _ _ _ _ _ _ _ _ _ He Hr as Hr′ Hpersist
assert Hpost : stdout_memoryinstall_bufferm1 r HeapBufferbase size r HeapBufferbase size
{eapply installed_memory with span := mkSpanmkPtrbase Objbase size
–exact Hmem1
–reflexivity
–unfold memory_roots
apply Forall_app
split ; exact proj1Hmem1 |
constructor ; exact Hw | constructor
–change 0 ≤ base < 2 ^ 64
lia
–change 0 ≤ base + size < 2 ^ 64
lia
–split ; exact proj1Hsize |
exists mkRegionbase base + req_extentq Heap Live
auto
split ; exact He |
split ; exact Hr' |
split ; exact Hpersist |
split ; exact Hpost |
intros span Hin
change Inspan fixed_rootsr ++ mkSpanmkPtrbase Objbase size in Hin
apply in_app_iff in Hin as [ Hold | [ <-| [ ] ] ]
–split ; right ; left ; exists span ; auto |
intros a Hrange
left
exists span
split ; exact Hold |
split ; | exact Hrange
pose proof proj1Hpost as Hroots
rewrite Forall_forall in Hroots
apply Hroots
apply in_or_app
left
exact Hold
–split
+right
right
right
exists base
simpl
auto
+intros a Hrange
apply Hauthority
exact Hrange

Standalone wrapper for existing buffer clients.

533Module Libio R : Runtime
534Module M ≔ ExternalMachine R
Include LibioOn R M

Public branch and representation boundaries

Block sizes from 1 to 8191 after a successful stat are the capacity; 8192 and above, zero, negative, or a failed stat give 8192.

542Example capacity_edges: file_capacitytrue 1 = 1 ∧ file_capacitytrue 8191 = 8191 ∧ file_capacitytrue 8192 = 8192 ∧ file_capacitytrue 8193 = 8192 ∧ file_capacitytrue 0 = 8192 ∧ file_capacitytrue −7 = 8192 ∧ file_capacityfalse 4096 = 8192
Explore proof 2 tactics

Initial goal

⊢
file_capacitytrue 1 = 1 ∧ file_capacitytrue 8191 = 8191 ∧ file_capacitytrue 8192 = 8192 ∧ file_capacitytrue 8193 = 8192 ∧ file_capacitytrue 0 = 8192 ∧ file_capacitytrue −7 = 8192 ∧ file_capacityfalse 4096 = 8192

vm_compute

⊢
1 = 1 ∧ 8191 = 8191 ∧ 8192 = 8192 ∧ 8192 = 8192 ∧ 8192 = 8192 ∧ 8192 = 8192 ∧ 8192 = 8192

repeat split ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
vm_compute
repeat split ; reflexivity

Capacity 8191 is not rounded, though heap_req reserves 8192.

550Example capacity_not_rounded_extent: file_capacitytrue 8191 = 8191 ∧ req_extentheap_req16 8191 = 8192
Explore proof 2 tactics

Initial goal

⊢
file_capacitytrue 8191 = 8191 ∧ req_extentheap_req16 8191 = 8192

vm_compute

⊢
8191 = 8191 ∧ 8192 = 8192

auto

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
vm_compute
auto

Generic libio falls back to the embedded byte when malloc returns NULL.

556Example generic_malloc_fallback: buffer_choice4096 NoBuffer MallocNull ShortBuffer
Explore proof 1 tactics

Initial goal

constructor

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
constructor

At the pin, that NULL branch is never taken.

560Example pin_cannot_return_null: ∀size storage, ¬pinned_choicesize NoBuffer MallocNull storage
Explore proof 3 tactics

Initial goal

⊢
∀size : Z storage : buffer_storage, ¬pinned_choicesize NoBuffer MallocNull storage

intros size storage _ H

size :
Z
⊢
False

apply H

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros size storage _ H
apply H
reflexivity

An unbuffered stdout uses the embedded byte without allocating.

565Example unbuffered_needs_no_allocation: pinned_choice8192 NoBuffer Unbuffered ShortBuffer
Explore proof 1 tactics

Initial goal

split ; constructor | discriminate

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
split ; constructor | discriminate

An existing buffer has priority: no malloc replaces it.

569Example existing_buffer_not_reallocated: ∀size old new, old ≠ NoBuffer → pinned_choicesize old MallocSuccess4096 new → False
Explore proof 2 tactics

Initial goal

⊢
∀size : Z old new : buffer_storage, old ≠ NoBuffer → pinned_choicesize old MallocSuccess4096 new → False

intros size old new H Hchoice _

size :
Z
old, new :
H :
old ≠ NoBuffer
Hchoice :
⊢
False

inversion Hchoice ; subst ; contradiction

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros size old new H Hchoice _
inversion Hchoice ; subst ; contradiction

The embedded buffer's pointer has the FILE's capability.

574Example shortbuf_keeps_file_cap: ∀r, ptr_capshort_ptrr = ptr_capfile_ptrr
Explore proof 1 tactics

Initial goal

reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
reflexivity

A buffer slot with the right address bytes but no capability in its aux does not satisfy buffer_slots.

580Example buffer_address_without_aux_is_not_enough: ∀m r base size, m_auxm ptr_addrfile_ptrr + 56 = CNone → ¬buffer_slotsm r HeapBufferbase size
Explore proof 4 tactics

Initial goal

⊢
∀m : mem r : stdout_roots base size : Z, m_auxm ptr_addrfile_ptrr + 56 = CNone → ¬buffer_slotsm r HeapBufferbase size

intros m r base size Ha _ _ Hcap _

m :
base, size :
Z
Hcap :
m_auxm ptr_addrfile_ptrr + 56 = ptr_capspan_ptrspan_ptr ≔ ptr_addr ≔ base; ptr_cap ≔ Objbase; span_size ≔ size
⊢
False

simpl in Hcap

m :
base, size :
Z
Hcap :
m_auxm ptr_addrfile_ptrr + 56 = Objbase
⊢
False

rewrite Ha in Hcap

m :
base, size :
Z
Hcap :
CNone = Objbase
⊢
False

discriminate

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m r base size Ha _ _ Hcap _
simpl in Hcap
rewrite Ha in Hcap
discriminate

Nor does one with the right capability but other address bytes.

586Example buffer_cap_without_address_is_not_enough: ∀m r base size, load_bytesm ptr_addrfile_ptrr + 56 8 ≠ base → ¬buffer_slotsm r HeapBufferbase size
Explore proof 3 tactics

Initial goal

⊢
∀m : mem r : stdout_roots base size : Z, load_bytesm ptr_addrfile_ptrr + 56 8 ≠ base → ¬buffer_slotsm r HeapBufferbase size

intros m r base size Ha _ Haddr _ _

m :
base, size :
Z
Ha :
load_bytesm ptr_addrfile_ptrr + 56 8 ≠ base
Haddr :
load_bytesm ptr_addrfile_ptrr + 56 8 = ptr_addrspan_ptrspan_ptr ≔ ptr_addr ≔ base; ptr_cap ≔ Objbase; span_size ≔ size
⊢
False

apply Ha

m :
base, size :
Z
Ha :
load_bytesm ptr_addrfile_ptrr + 56 8 ≠ base
Haddr :
load_bytesm ptr_addrfile_ptrr + 56 8 = ptr_addrspan_ptrspan_ptr ≔ ptr_addr ≔ base; ptr_cap ≔ Objbase; span_size ≔ size
⊢
load_bytesm ptr_addrfile_ptrr + 56 8 = base

exact Haddr

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros m r base size Ha _ Haddr _ _
apply Ha
exact Haddr

Example roots: the FILE at 2048, its lock at 4096, errno at 8192. With the memories below, an inhabited memory view, not a fixture claiming to be native FILE.

594Definition root_example: stdout_roots ≔
mkStdoutRootsmkPtr2048 Obj2048 mkPtr4096 Obj4096 mkPtr8192 Obj8192

A memory with null buffer slots and a capability-bearing lock slot pointing at 4096.

599Definition unbuffered_example: mem ≔
λ a  ⇒
2184 ≤? a && a <? 2192
→
byte_of4096 a − 2184
else
0
λ a  ⇒
a =? 2184
→
Obj4096
else

unbuffered_example satisfies stdout_memory with no buffer.

606Example no_buffer_memory_inhabited: stdout_memoryunbuffered_example root_example NoBuffer
Proof 15 steps Qed
split
–constructor
+split ; simpl ; lia |
exists 2048, mkRegion2048 2272 GlobalData Live
repeat split ; reflexivity
+constructor
∗split ; simpl ; lia |
exists 4096, mkRegion4096 4112 GlobalData Live
repeat split ; reflexivity
∗constructor ; | constructor
split ; simpl ; lia |
exists 8192, mkRegion8192 8196 Heap Live
repeat split ; reflexivity
–vm_compute
repeat constructor ; discriminate

Storing in the two buffer slots BOTH the address bytes (the embedded byte's start 2179 and end 2180) and the FILE's capability in their aux satisfies stdout_memory with the embedded buffer.

622Example embedded_memory_inhabited: stdout_memorystore_auxstore_auxstore_bytesstore_bytesunbuffered_example 2104 8 2179 2112 8 2180 2104 Obj2048 2112 Obj2048 root_example ShortBuffer
Proof 15 steps Qed
split
–constructor
+split ; simpl ; lia |
exists 2048, mkRegion2048 2272 GlobalData Live
repeat split ; reflexivity
+constructor
∗split ; simpl ; lia |
exists 4096, mkRegion4096 4112 GlobalData Live
repeat split ; reflexivity
∗constructor ; | constructor
split ; simpl ; lia |
exists 8192, mkRegion8192 8196 Heap Live
repeat split ; reflexivity
–vm_compute
repeat constructor ; discriminate

An asymmetric capacity exercises installed slots, rounded extent, the nontrivial flag mask, and unchanged lock/errno contents.

640Definition heap_example: mem ≔
645Example installed_heap_memory_inhabited: stdout_memoryheap_example root_example HeapBuffer16384 8191
Explore proof 26 tactics

Initial goal

split

2 open

focused goal

–constructor

3 open

focused goal
deferred goal

+split ; simpl ; lia |

3 open

deferred goal
deferred goal

exists 2048, mkRegion2048 2272 GlobalData Live

3 open

deferred goal
deferred goal

repeat split ; reflexivity

2 open

deferred goal
deferred goal

+constructor

3 open

focused goal
⊢
Forallwritable_spanheap_example span_ptr ≔ errno_ptrroot_example; span_size ≔ 4; span_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191
deferred goal

∗split ; simpl ; lia |

3 open

deferred goal
⊢
Forallwritable_spanheap_example span_ptr ≔ errno_ptrroot_example; span_size ≔ 4; span_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191
deferred goal

exists 4096, mkRegion4096 4112 GlobalData Live

3 open

deferred goal
⊢
Forallwritable_spanheap_example span_ptr ≔ errno_ptrroot_example; span_size ≔ 4; span_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191
deferred goal

repeat split ; reflexivity

2 open

deferred goal
⊢
Forallwritable_spanheap_example span_ptr ≔ errno_ptrroot_example; span_size ≔ 4; span_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191
deferred goal

∗constructor

3 open

focused goal
⊢
Forallwritable_spanheap_example span_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191
deferred goal

--split ; simpl ; lia |

3 open

deferred goal
⊢
Forallwritable_spanheap_example span_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191
deferred goal

exists 8192, mkRegion8192 8196 Heap Live

3 open

deferred goal
⊢
Forallwritable_spanheap_example span_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191
deferred goal

repeat split ; reflexivity

2 open

deferred goal
⊢
Forallwritable_spanheap_example span_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191
deferred goal

--constructor ; | constructor

2 open

⊢
writable_spanheap_example span_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191
deferred goal

split ; simpl ; lia |

2 open

⊢
∃base : Z reg : region, ptr_capspan_ptrspan_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191 = Objbase ∧ object_regionbase m_regionsheap_example = Somereg ∧ r_lifereg = Live ∧ access_resheap_example ptr_addrspan_ptrspan_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191 Objbase span_sizespan_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191 Write 1 = Someok
deferred goal

exists 16384, mkRegion16384 24576 Heap Live

2 open

⊢
ptr_capspan_ptrspan_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191 = Obj16384 ∧ object_region16384 m_regionsheap_example = Somer_base ≔ 16384; r_end ≔ 24576; r_kind ≔ Heap; r_life ≔ Live ∧ r_lifer_base ≔ 16384; r_end ≔ 24576; r_kind ≔ Heap; r_life ≔ Live = Live ∧ access_resheap_example ptr_addrspan_ptrspan_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191 Obj16384 span_sizespan_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191 Write 1 = Someok
deferred goal

repeat split ; reflexivity

deferred goal

–split ; reflexivity |

split ; repeat constructor ; reflexivity |

split ; reflexivity |

split ; reflexivity |

split ; vm_compute ; repeat constructor ; discriminate |

⊢
buffer_slotsheap_example root_example HeapBuffer16384 8191 ∧ 0 < 8191 ∧ ∃reg : region, object_region16384 m_regionsheap_example = Somereg ∧ r_kindreg = Heap ∧ r_lifereg = Live

split ; vm_compute ; repeat constructor ; discriminate |

⊢
0 < 8191 ∧ ∃reg : region, object_region16384 m_regionsheap_example = Somereg ∧ r_kindreg = Heap ∧ r_lifereg = Live

split ; lia |

⊢
∃reg : region, object_region16384 m_regionsheap_example = Somereg ∧ r_kindreg = Heap ∧ r_lifereg = Live

exists mkRegion16384 24576 Heap Live

⊢
object_region16384 m_regionsheap_example = Somer_base ≔ 16384; r_end ≔ 24576; r_kind ≔ Heap; r_life ≔ Live ∧ r_kindr_base ≔ 16384; r_end ≔ 24576; r_kind ≔ Heap; r_life ≔ Live = Heap ∧ r_lifer_base ≔ 16384; r_end ≔ 24576; r_kind ≔ Heap; r_life ≔ Live = Live

repeat split ; reflexivity

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
split
–constructor
+split ; simpl ; lia |
exists 2048, mkRegion2048 2272 GlobalData Live
repeat split ; reflexivity
+constructor
∗split ; simpl ; lia |
exists 4096, mkRegion4096 4112 GlobalData Live
repeat split ; reflexivity
∗constructor
--split ; simpl ; lia |
exists 8192, mkRegion8192 8196 Heap Live
repeat split ; reflexivity
--constructor ; | constructor
split ; simpl ; lia |
exists 16384, mkRegion16384 24576 Heap Live
repeat split ; reflexivity
–split ; reflexivity |
split ; repeat constructor ; reflexivity |
split ; reflexivity |
split ; reflexivity |
split ; vm_compute ; repeat constructor ; discriminate |
split ; vm_compute ; repeat constructor ; discriminate |
split ; lia |
exists mkRegion16384 24576 Heap Live
repeat split ; reflexivity
663Example installed_capacity_and_flag: pointer_slotheap_example 2104 mkPtr16384 Obj16384 ∧ pointer_slotheap_example 2112 mkPtr24575 Obj16384 ∧ object_region16384 m_regionsheap_example = SomemkRegion16384 24576 Heap Live ∧ load_bytesheap_example 2048 4 = 305419896 ∧ pointer_slotheap_example 2184 mkPtr4096 Obj4096 ∧ load_bytesheap_example 8192 4 = 73
Explore proof 2 tactics

Initial goal

⊢
pointer_slotheap_example 2104 ptr_addr ≔ 16384; ptr_cap ≔ Obj16384 ∧ pointer_slotheap_example 2112 ptr_addr ≔ 24575; ptr_cap ≔ Obj16384 ∧ object_region16384 m_regionsheap_example = Somer_base ≔ 16384; r_end ≔ 24576; r_kind ≔ Heap; r_life ≔ Live ∧ load_bytesheap_example 2048 4 = 305419896 ∧ pointer_slotheap_example 2184 ptr_addr ≔ 4096; ptr_cap ≔ Obj4096 ∧ load_bytesheap_example 8192 4 = 73

vm_compute

⊢
Datatypes.Lt = Datatypes.Gt → False ∧ Datatypes.Lt = Datatypes.Lt ∧ 16384 = 16384 ∧ Obj16384 = Obj16384 ∧ Datatypes.Lt = Datatypes.Gt → False ∧ Datatypes.Lt = Datatypes.Lt ∧ 24575 = 24575 ∧ Obj16384 = Obj16384 ∧ Somer_base ≔ 16384; r_end ≔ 24576; r_kind ≔ Heap; r_life ≔ Live = Somer_base ≔ 16384; r_end ≔ 24576; r_kind ≔ Heap; r_life ≔ Live ∧ 305419896 = 305419896 ∧ Datatypes.Lt = Datatypes.Gt → False ∧ Datatypes.Lt = Datatypes.Lt ∧ 4096 = 4096 ∧ Obj4096 = Obj4096 ∧ 73 = 73

repeat constructor ; discriminate

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
vm_compute
repeat constructor ; discriminate
Explore proof 10 tactics

Initial goal

split ; | reflexivity

eapply installed_memory

7 open

focused goal
focused goal
focused goal
⊢
0 ≤ ptr_addrspan_ptr?span < 2 ^ 64
focused goal
⊢
0 ≤ ptr_addrspan_ptr?span + span_size?span < 2 ^ 64
focused goal
⊢
True
shelved goal
⊢

–exact no_buffer_memory_inhabited

6 open

deferred goal
deferred goal
deferred goal
⊢
0 ≤ ptr_addrspan_ptr?span < 2 ^ 64
deferred goal
⊢
0 ≤ ptr_addrspan_ptr?span + span_size?span < 2 ^ 64
deferred goal
⊢
True
shelved goal
⊢

–reflexivity

4 open

deferred goal
deferred goal
⊢
deferred goal
deferred goal
⊢
True

–exact proj1no_buffer_memory_inhabited

3 open

deferred goal
⊢
deferred goal
deferred goal
⊢
True

–change 0 ≤ 2179 < 2 ^ 64

3 open

⊢
0 ≤ 2179 < 2 ^ 64
deferred goal
deferred goal
⊢
True

lia

2 open

deferred goal
deferred goal
⊢
True

–change 0 ≤ 2180 < 2 ^ 64

2 open

⊢
0 ≤ 2180 < 2 ^ 64
deferred goal
⊢
True

lia

deferred goal
⊢
True

–exact I

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
split ; | reflexivity
–reflexivity
–change 0 ≤ 2179 < 2 ^ 64
lia
–change 0 ≤ 2180 < 2 ^ 64
lia
–exact I
Explore proof 4 tactics

Initial goal

intros _ & _ & _ & _ & _ & _ & _ & _ & reg & Hreg & _ & Hlife

reg :
Hreg :
Hlife :
r_lifereg = Live
⊢
False

change SomemkRegion16384 16384 Heap Freed = Somereg in Hreg

reg :
Hreg :
Somer_base ≔ 16384; r_end ≔ 16384; r_kind ≔ Heap; r_life ≔ Freed = Somereg
Hlife :
r_lifereg = Live
⊢
False

injection Hreg as ←

Hlife :
r_lifer_base ≔ 16384; r_end ≔ 16384; r_kind ≔ Heap; r_life ≔ Freed = Live
⊢
False

discriminate Hlife

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros _ & _ & _ & _ & _ & _ & _ & _ & reg & Hreg & _ & Hlife
change SomemkRegion16384 16384 Heap Freed = Somereg in Hreg
injection Hreg as ←
discriminate Hlife
696Example installed_undersized_heap_rejected: ¬stdout_memorymkMemm_bytesheap_example mkRegion16384 24574 Heap Live :: m_regionsheap_example m_auxheap_example root_example HeapBuffer16384 8191
Explore proof 7 tactics

Initial goal

intros Hroots _

rewrite Forall_forall in Hroots

Hroots :
⊢
False

specialize HrootsmkSpanmkPtr16384 Obj16384 8191 ltac:simpl ; auto

Hroots :
writable_spanm_bytes ≔ m_bytesheap_example; m_regions ≔ r_base ≔ 16384; r_end ≔ 24574; r_kind ≔ Heap; r_life ≔ Live :: m_regionsheap_example; m_aux ≔ m_auxheap_example span_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191
⊢
False

destruct Hroots as _ & base & reg & Hcap & _ & _ & Haccess

base :
Z
reg :
Hcap :
ptr_capspan_ptrspan_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191 = Objbase
Haccess :
access_resm_bytes ≔ m_bytesheap_example; m_regions ≔ r_base ≔ 16384; r_end ≔ 24574; r_kind ≔ Heap; r_life ≔ Live :: m_regionsheap_example; m_aux ≔ m_auxheap_example ptr_addrspan_ptrspan_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191 Objbase span_sizespan_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191 Write 1 = Someok
⊢
False

change Obj16384 = Objbase in Hcap

base :
Z
reg :
Hcap :
Obj16384 = Objbase
Haccess :
access_resm_bytes ≔ m_bytesheap_example; m_regions ≔ r_base ≔ 16384; r_end ≔ 24574; r_kind ≔ Heap; r_life ≔ Live :: m_regionsheap_example; m_aux ≔ m_auxheap_example ptr_addrspan_ptrspan_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191 Objbase span_sizespan_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191 Write 1 = Someok
⊢
False

injection Hcap as ←

reg :
Haccess :
access_resm_bytes ≔ m_bytesheap_example; m_regions ≔ r_base ≔ 16384; r_end ≔ 24574; r_kind ≔ Heap; r_life ≔ Live :: m_regionsheap_example; m_aux ≔ m_auxheap_example ptr_addrspan_ptrspan_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191 Obj16384 span_sizespan_ptr ≔ ptr_addr ≔ 16384; ptr_cap ≔ Obj16384; span_size ≔ 8191 Write 1 = Someok
⊢
False

discriminate Haccess

No remaining goals.

Qed

✓ Proof checked and closed by Rocq.

Source script
intros Hroots _
rewrite Forall_forall in Hroots
specialize HrootsmkSpanmkPtr16384 Obj16384 8191 ltac:simpl ; auto
destruct Hroots as _ & base & reg & Hcap & _ & _ & Haccess
change Obj16384 = Objbase in Hcap
injection Hcap as ←
discriminate Haccess