rocq/theories/Formatting.v
Hello's reached plain formatting calls, not the older fortified-symbol census. HelloCode's usage and version_etc use strings, %% and promoted integers; its wide path uses L"%ls\n". Admission is independent of output success. No %n is selected, so no %n write authority is granted. Translated formats outside this grammar need a further contract or a proved translation restriction, not an invented successful parse.
From Stdlib Require Import ZArith List Bool Lia
From Nanofil Require Import Syntax Values Memory Runtime ExternalCalls ExternalMachine Stdio Streams
Import ListNotations
Open Scope Z_scope
Open Scope list_scope
Decimal digits with no redundant leading zero, interpreted in base ten. This specifies decimal output independently of a printer.
digits ≠ [ ] ∧ Forallλd ⇒ 48 ≤ d ≤ 57 digits ∧ hd48 digits = 48 → digits = 48 ∧ fold_leftλacc d ⇒ 10 × acc + d − 48 digits 0 = n
The default-promoted int/unsigned int argument is a canonical W. Negative int words print a minus sign and the absolute signed value.
Selected format interpretation, with exact consumed varargs. Each %s needs its whole in-object NUL-terminated string even on failure. Literals and %% consume no argument. Floats, lengths, positional conversions, precision, and %n are deliberately not admitted here.
narrow_formatm [ ] [ ] [ ]
format_end∀ fmt args bytes
narrow_formatm fmt args bytes
format_percent
narrow_formatm 37 :: 37 :: fmt args 37 :: bytes
∀ fmt args bytes p text
c_stringm p text
narrow_formatm fmt args bytes
format_string
narrow_formatm 37 :: 115 :: fmt WPtrp :: args text ++ bytes
∀ fmt args bytes n text
formatted_inttrue n text
narrow_formatm fmt args bytes
format_signed
narrow_formatm 37 :: 100 :: fmt WIntn :: args text ++ bytes
∀ fmt args bytes n text
formatted_intfalse n text
narrow_formatm fmt args bytes
format_unsigned
narrow_formatm 37 :: 117 :: fmt WIntn :: args text ++ bytes
Read spans for the format and pointer varargs, through their NULs. Integer words grant no capability source; no source becomes a write root or an owned release. Exact lengths follow from admission.
The selected variadic ABI permits only P and promoted W, not L or unpromoted byte/half classes. The format interpretation independently requires matching pointer or integer words at every conversion.
The three reached narrow entry points share interpretation and FIFO effects, but retain their distinct fixed argument positions.
| | | NarrowPrintf | ||
| | | NarrowFprintf | ||
| | | NarrowFputs |
The stream handle selected by each entry point.
69Definition output_targetworld api : narrow_api stdout : world → ptr w : world xs : listword : ptr ≔
match api, xs with
The readable input pointer and remaining varargs, excluding FILE.
match api, xs with
_, _
⇒
None
Plain fputs accepts the string unchanged; formatting calls interpret a readable format and its exact varargs before selecting a result.
∃ p args text ,
output_inputsapi xs = Somep, args
∧
The complete fixed and promoted argument ABI.
∧
match api with
Complete admission: represented open non-wide stream and readable, well-typed format inputs. A negative result does not weaken this.
108Definition output_preworld api : narrow_api model : stream_modelworld stdout : world → ptr xs : listword m : mem w : world : Prop ≔
∃info bytes, stream_openmodel m w output_targetapi stdout w xs info ∧ orientationstream_protocolinfo ≠ WideOriented ∧ output_textapi m xs bytes
Formatted results count all output bytes on success; fputs promises only a nonnegative int. Every negative result may follow partial OR full acceptance, including an encoding or count-overflow failure.
accepted = bytes ∧ 0 ≤ result < 2 ^ 31 ∧ api = NarrowFputs ∨ result = Z.of_natlengthbytes ∨ negative_intresult
A finite output prefix reuses Stdio's ordered obligations. Stream identifiers distinguish stdout from stderr. Delivery is not another acceptance event. Physical pending may differ from outstanding.
123Definition output_prefixworld api : narrow_api model : stream_modelworld stdout : world → ptr xs : listword m : mem w : world born : listZ trace : listevent m′ : mem w′ : world : Prop ≔
∃info info′ bytes actions tail, stream_atmodel w output_targetapi stdout w xs = Someinfo ∧ output_textapi m xs bytes ∧ bytes = acceptedactions ++ tail ∧ stream_runstream_protocolinfo actions stream_protocolinfo′ ∧ stream_openmodel m′ w′ output_targetapi stdout w xs info′ ∧ stream_identifierinfo′ = stream_identifierinfo ∧ stream_framemodel output_targetapi stdout w xs w w′ ∧ stream_delegatesmodel w output_targetapi stdout w xs born m′ w′ ∧ trace = [ ] ∧ acceptedactions = [ ] ∨ trace = StreamBytesstream_identifierinfo acceptedactions ∧ stream_aux_framemodel m w output_targetapi stdout w xs m′
A completed output call includes the cumulative acceptance event, even on failure, but does not promise descriptor delivery.
140Definition output_postworld api : narrow_api model : stream_modelworld stdout : world → ptr xs : listword m : mem w : world born : listZ trace : listevent ending : call_end m′ : mem w′ : world : Prop ≔
∃info info′ bytes actions tail result, stream_atmodel w output_targetapi stdout w xs = Someinfo ∧ output_textapi m xs bytes ∧ bytes = acceptedactions ++ tail ∧ stream_runstream_protocolinfo actions stream_protocolinfo′ ∧ stream_openmodel m′ w′ output_targetapi stdout w xs info′ ∧ stream_identifierinfo′ = stream_identifierinfo ∧ stream_framemodel output_targetapi stdout w xs w w′ ∧ stream_delegatesmodel w output_targetapi stdout w xs born m′ w′ ∧ output_resultapi bytes acceptedactions result ∧ trace = StreamBytesstream_identifierinfo acceptedactions ∧ ending = CallReturnWIntresult
The common contract retains readable inputs only as sources; its writable roots are solely the stream's, and it releases no caller object. Native temporary allocations remain explicit requests.
158Definition output_contractworld api : narrow_api model : stream_modelworld stdout : world → ptr : contractworld ≔
mkContractworld RClassW output_abiapi output_preapi model stdout
λ xs m w ⇒
λxs _ w ⇒ stream_writesmodel w output_targetapi stdout w xs
λ_ _ _ ⇒ [ ]
λxs _ w ⇒ stream_requestsmodel w output_targetapi stdout w xs
output_prefixapi model stdout
output_postapi model stdout
Plain printf uses the supplied stdout-handle projection.
output_contractNarrowPrintf model stdout
Plain fprintf takes its FILE as the first P argument.
output_contractNarrowFprintf model λ_ ⇒ mkPtr0 CNone
Plain fputs takes its FILE as the second P argument.
output_contractNarrowFputs model λ_ ⇒ mkPtr0 CNone
A readable wchar_t string, including its aligned four-byte NUL. Invalid encoding values are not excluded: output may fail on them.
access_resm ptr_addrp ptr_capp 4 × Z.of_natlengthchars + 1 Read 4 = Someok ∧ Forallλc ⇒ 0 < c < 2 ^ 32 chars ∧ ∀i c, nth_errorchars i = Somec → load_bytesm ptr_addrp + 4 × Z.of_nati 4 = c ∧ load_bytesm ptr_addrp + 4 × Z.of_natlengthchars 4 = 0
A bounded scan in wchar_t units, solely to compute the readable source footprint. As for string_length, admission grants reads.
nul_countλi ⇒ load_bytesm ptr_addrp + 4 × i 4 0 Z.to_natstring_capacitym p / 4
Selected wide realization: conversion, native buffering and its observations must be supplied independently. It is not byte Accept on a wide stream and does not create another stdout queue.
| wide_realization | : world → ptr → listZ → listZ → stream_info → optionZ → Prop |
Arguments wide_realization { world }
Admission to Hello's sole wide format L"%ls\n", with one readable wchar_t-string P argument and a non-byte-oriented stdout.
204Definition wprintf_preworld model : stream_modelworld stdout : world → ptr xs : listword m : mem w : world : Prop ≔
∃fmt text chars info, xs = WPtrfmt; WPtrtext ∧ wchar_stringm fmt 37; 108; 115; 10 ∧ wchar_stringm text chars ∧ stream_openmodel m w stdoutw info ∧ orientationstream_protocolinfo ≠ ByteOriented
Wide prefixes preserve the authoritative orientation/error state; the realization relation accounts for encoded bytes accepted and ties successful results to complete conversion. None is a finite prefix, Some result an ordinary completion.
214Definition wprintf_effectworld model : stream_modelworld stdout : world → ptr wide : wide_output_contextworld result : optionZ xs : listword m : mem w : world born : listZ trace : listevent m′ : mem w′ : world : Prop ≔
∃fmt text chars info info′ bytes, xs = WPtrfmt; WPtrtext ∧ wchar_stringm text chars ∧ stream_atmodel w stdoutw = Someinfo ∧ stream_openmodel m′ w′ stdoutw info′ ∧ wide_realizationwide w stdoutw chars ++ 10 bytes info′ result ∧ orientationstream_protocolinfo′ ≠ ByteOriented ∧ result ≠ None → orientationstream_protocolinfo′ = WideOriented ∧ orientationstream_protocolinfo = WideOriented → orientationstream_protocolinfo′ = WideOriented ∧ stream_errorstream_protocolinfo = true → stream_errorstream_protocolinfo′ = true ∧ stream_identifierinfo′ = stream_identifierinfo ∧ stream_framemodel stdoutw w w′ ∧ stream_delegatesmodel w stdoutw born m′ w′ ∧ trace = [ ] ∧ bytes = [ ] ∧ result = None ∨ trace = StreamBytesstream_identifierinfo bytes ∧ stream_aux_framemodel m w stdoutw m′
The selected wprintf contract has a separate native realization premise. Success counts wchar_t output, not encoded bytes. Resources never inherit its normal-return postcondition.
236Definition wprintf_contractworld model : stream_modelworld stdout : world → ptr wide : wide_output_contextworld : contractworld ≔
mkContractworld RClassW λr args ⇒ r = CVoid ∨ ∃d, r = CResultd W ∧ ∃fmt text, args = ArgP fmt; ArgP text wprintf_premodel stdout
λ xs m w ⇒
λ_ _ w ⇒ stream_writesmodel w stdoutw
λ_ _ _ ⇒ [ ]
λ_ _ w ⇒ stream_requestsmodel w stdoutw
wprintf_effectmodel stdout wide None
λxs m w born trace ending m′ w′ ⇒ ∃result, wprintf_effectmodel stdout wide Someresult xs m w born trace m′ w′ ∧ ending = CallReturnWIntresult ∧ 0 ≤ result < 2 ^ 31 ∧ ∃fmt text chars, xs = WPtrfmt; WPtrtext ∧ wchar_stringm text chars ∧ result = Z.of_natlengthchars + 1 ∨ negative_intresult
Selected error() decoration and internal state authority. Readiness excludes a user error_print_progname callback, supplies initialized counter/TLS/program-name state and all selected strerror dependencies. Segments include the program prefix, formatted body, optional errno text and newline. Each native formatting stage can fail independently. The frame must preserve phase, status, pending/consumed callback inventories, and permit only the explicitly described stream changes.
| diagnostic_ready | : mem → world → Prop | |
| diagnostic_sources | ||
| diagnostic_writes | : world → listspan | |
| diagnostic_requests | : world → Z → Z → Prop | |
| diagnostic_segments | : mem → world → Z → listZ → listlistZ → Prop | |
| diagnostic_frame | : world → world → Prop |
Arguments diagnostic_ready { world }
Arguments diagnostic_sources { world }
Arguments diagnostic_writes { world }
Arguments diagnostic_requests { world }
Arguments diagnostic_segments { world }
Arguments diagnostic_frame { world }
Flushing stdout does not accept diagnostic bytes. An already closed static stdout stays closed; its selected safe fflush behavior is part of native representation coverage, not valid arbitrary FILE use.
282Definition diagnostic_flushworld model : stream_modelworld stdout : world → ptr w w′ : world : Prop ≔
None
⇒
stream_atmodel w′ stdoutw = None ∧ stream_state_atmodel w′ stdoutw = stream_state_atmodel w stdoutw
Someinfo
⇒
∃info′, stream_atmodel w′ stdoutw = Someinfo′ ∧ stream_protocolinfo = stream_state_atmodel w stdoutw ∧ stream_protocolinfo′ = stream_state_atmodel w′ stdoutw ∧ stream_identifierinfo′ = stream_identifierinfo ∧ stream_settlementmodel w stdoutw stream_protocolinfo stream_protocolinfo′ false
Admission to the formatting part of error, before any exit request. The selected stderr path is narrow; wide stderr needs separate fxprintf conversion coverage. Status/errno are promoted canonical W words.
297Definition error_format_preworld model : stream_modelworld stdout stderr : world → ptr diagnostic : diagnostic_contextworld xs : listword m : mem w : world : Prop ≔
∃status errnum fmt args text body info, xs = WIntstatus :: WInterrnum :: WPtrfmt :: args ∧ 0 ≤ status < 2 ^ 32 ∧ 0 ≤ errnum < 2 ^ 32 ∧ c_stringm fmt text ∧ narrow_formatm text args body ∧ diagnostic_readydiagnostic m w ∧ Forallwritable_spanm diagnostic_writesdiagnostic w ∧ stream_openmodel m w stderrw info ∧ orientationstream_protocolinfo ≠ WideOriented ∧ stdoutw ≠ stderrw
A diagnostic can accept a prefix of EACH stage, not necessarily a prefix of the concatenation: a failed body may be followed by errno text or a newline. Nothing is labeled as stdout acceptance.
312Definition error_format_prefixworld model : stream_modelworld stdout stderr : world → ptr diagnostic : diagnostic_contextworld xs : listword m : mem w : world born : listZ trace : listevent m′ : mem w′ : world : Prop ≔
∃status errnum fmt args text body info info′ segments pieces actions, xs = WIntstatus :: WInterrnum :: WPtrfmt :: args ∧ c_stringm fmt text ∧ narrow_formatm text args body ∧ diagnostic_segmentsdiagnostic m w errnum body segments ∧ Forall2λwhole part ⇒ ∃tail, whole = part ++ tail segments pieces ∧ stream_atmodel w stderrw = Someinfo ∧ stream_openmodel m′ w′ stderrw info′ ∧ stream_identifierinfo = 2 ∧ stream_identifierinfo′ = 2 ∧ stream_runstream_protocolinfo actions stream_protocolinfo′ ∧ acceptedactions = concatpieces ∧ diagnostic_flushmodel stdout w w′ ∧ diagnostic_readydiagnostic m′ w′ ∧ diagnostic_framediagnostic w w′ ∧ stream_delegatesmodel w stdoutw born m′ w′ ∧ stream_delegatesmodel w stderrw born m′ w′ ∧ ∀root, Inroot diagnostic_writesdiagnostic w′ → available_capdiagnostic_sourcesdiagnostic m w born m′ ptr_capspan_ptrroot ∧ ∀a, span_containsroot a → write_authoritydiagnostic_writesdiagnostic w born m′ a ∧ trace = [ ] ∧ acceptedactions = [ ] ∨ trace = StreamBytes2 acceptedactions ∧ ∀a, in_objectm a → ¬write_authoritystream_aux_rootsmodel w stdoutw ++ stream_aux_rootsmodel w stderrw ++ diagnostic_writesdiagnostic w [ ] m a → m_auxm′ a = m_auxm a
error's formatting stage has the actual W,W,P variadic ABI and void return. It NEVER emits ProcessExit: the separate ending protocol owns the exit request after this stage's current-world completion.
341Definition error_format_contractworld model : stream_modelworld stdout stderr : world → ptr diagnostic : diagnostic_contextworld : contractworld ≔
mkContractworld RVoid λr args ⇒ r = CVoid ∧ ∃status errnum fmt rest, args = ArgW status :: ArgW errnum :: ArgP fmt :: rest ∧ Forallpromoted_argument rest error_format_premodel stdout stderr diagnostic
λ xs m w ⇒
stream_sourcesmodel w stdoutw
++
λ_ _ w ⇒ stream_writesmodel w stdoutw ++ stream_writesmodel w stderrw ++ diagnostic_writesdiagnostic w
λ_ _ _ ⇒ [ ]
λ_ _ w align size ⇒ stream_requestsmodel w stdoutw align size ∨ stream_requestsmodel w stderrw align size ∨ diagnostic_requestsdiagnostic w align size
error_format_prefixmodel stdout stderr diagnostic
λxs m w born trace ending m′ w′ ⇒ error_format_prefixmodel stdout stderr diagnostic xs m w born trace m′ w′ ∧ ending = CallReturn[ ]
Inversion over the supplied machine keeps ordinary returns and resource stops apart without a sibling invocation relation.
Construct an ordinary output completion from the independently witnessed prefix/effects and complete result relation.
output_abiapi r args
output_preapi model stdout xs m w
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
output_postapi model stdout xs m w born trace CallReturnWIntresult m′ w′
E.invokeoutput_contractapi model stdout r args xs s m w trace CallReturnWIntresult s′ m′ w′
Explore proof 12 tactics
Initial goal
⊢
∀world : Type api : narrow_api model : stream_modelworld stdout : world → ptr r : call_result args : listarg xs : listword s : R.state m : mem w : world born : listZ trace : listevent result : Z s′ : R.state m′ : mem w′ : world, output_abiapi r args → output_preapi model stdout xs m w → E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′ → output_postapi model stdout xs m w born trace CallReturnWIntresult m′ w′ → E.invokeoutput_contractapi model stdout r args xs s m w trace CallReturnWIntresult s′ m′ w′
intros world api model stdout r args xs s m w born trace result s′ m′ w′ Habi Hpre Hprefix Hpost
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
output_abiapi r args
Hpre :
output_preapi model stdout xs m w
Hprefix :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
Hpost :
output_postapi model stdout xs m w born trace CallReturnWIntresult m′ w′
⊢
E.invokeoutput_contractapi model stdout r args xs s m w trace CallReturnWIntresult s′ m′ w′
eapply E.invoke_normal with born := born ; try exact Habi ; try exact Hpre ; try exact Hprefix ; try exact Hpost ; try discriminate
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
output_abiapi r args
Hpre :
output_preapi model stdout xs m w
Hprefix :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
Hpost :
output_postapi model stdout xs m w born trace CallReturnWIntresult m′ w′
⊢
∀values : listword, CallReturnWIntresult = CallReturnvalues → return_shapecontract_returnsoutput_contractapi model stdout values ∧ Forallword_authoritycontract_sourcesoutput_contractapi model stdout xs m w born m′ values
intros values Heq
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
output_abiapi r args
Hpre :
output_preapi model stdout xs m w
Hprefix :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
Hpost :
output_postapi model stdout xs m w born trace CallReturnWIntresult m′ w′
values :
listword
Heq :
CallReturnWIntresult = CallReturnvalues
⊢
return_shapecontract_returnsoutput_contractapi model stdout values ∧ Forallword_authoritycontract_sourcesoutput_contractapi model stdout xs m w born m′ values
injection Heq as ←
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
output_abiapi r args
Hpre :
output_preapi model stdout xs m w
Hprefix :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
Hpost :
output_postapi model stdout xs m w born trace CallReturnWIntresult m′ w′
⊢
return_shapecontract_returnsoutput_contractapi model stdout WIntresult ∧ Forallword_authoritycontract_sourcesoutput_contractapi model stdout xs m w born m′ WIntresult
split ; | constructor ; exact I | constructor
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
output_abiapi r args
Hpre :
output_preapi model stdout xs m w
Hprefix :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
Hpost :
output_postapi model stdout xs m w born trace CallReturnWIntresult m′ w′
⊢
return_shapecontract_returnsoutput_contractapi model stdout WIntresult
exists WIntresult
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
output_abiapi r args
Hpre :
output_preapi model stdout xs m w
Hprefix :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
Hpost :
output_postapi model stdout xs m w born trace CallReturnWIntresult m′ w′
split ; reflexivity |
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
output_abiapi r args
Hpre :
output_preapi model stdout xs m w
Hprefix :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
Hpost :
output_postapi model stdout xs m w born trace CallReturnWIntresult m′ w′
⊢
word_at_classW WIntresult = SomeWIntresult
simpl
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
output_abiapi r args
Hpre :
output_preapi model stdout xs m w
Hprefix :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
Hpost :
output_postapi model stdout xs m w born trace CallReturnWIntresult m′ w′
destruct Hpost as info & info′ & bytes & actions & tail & n & _ & _ & _ & _ & _ & _ & _ & _ & Hr & _ & Hend
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
output_abiapi r args
Hpre :
output_preapi model stdout xs m w
Hprefix :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
n :
Z
Hr :
output_resultapi bytes acceptedactions n
Hend :
CallReturnWIntresult = CallReturnWIntn
injection Hend as ←
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
output_abiapi r args
Hpre :
output_preapi model stdout xs m w
Hprefix :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hr :
output_resultapi bytes acceptedactions result
rewrite Z.mod_small ; reflexivity |
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
born :
listZ
trace :
listevent
result :
Z
s′ :
R.state
m′ :
w′ :
world
Habi :
output_abiapi r args
Hpre :
output_preapi model stdout xs m w
Hprefix :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hr :
output_resultapi bytes acceptedactions result
⊢
0 ≤ result < Z.pow_pos2 32
destruct Hr as _ & Hn & _ | Hn ; unfold negative_int in * ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros world api model stdout r args xs s m w born trace result s′ m′ w′ Habi Hpre Hprefix Hpost
eapply E.invoke_normal with born := born ; try exact Habi ; try exact Hpre ; try exact Hprefix ; try exact Hpost ; try discriminate
intros values Heq
injection Heq as ←
split ; | constructor ; exact I | constructor
exists WIntresult
split ; reflexivity |
simpl
destruct Hpost as info & info′ & bytes & actions & tail & n & _ & _ & _ & _ & _ & _ & _ & _ & Hr & _ & Hend
injection Hend as ←
rewrite Z.mod_small ; reflexivity |
destruct Hr as _ & Hn & _ | Hn ; unfold negative_int in * ; lia
All three narrow contracts share this ordinary/resource disjunction.
E.invokeoutput_contractapi model stdout r args xs s m w trace ending s′ m′ w′
∃born, output_postapi model stdout xs m w born trace ending m′ w′ ∨ ∃why, ending = CallResourcewhy ∧ resource_reasonwhy
Explore proof 6 tactics
Initial goal
⊢
∀world : Type api : narrow_api model : stream_modelworld stdout : world → ptr r : call_result args : listarg xs : listword s : R.state m : mem w : world trace : listevent ending : call_end s′ : R.state m′ : mem w′ : world, E.invokeoutput_contractapi model stdout r args xs s m w trace ending s′ m′ w′ → ∃born : listZ, output_postapi model stdout xs m w born trace ending m′ w′ ∨ ∃why : reason, ending = CallResourcewhy ∧ resource_reasonwhy
intros world api model stdout r args xs s m w trace ending s′ m′ w′ Hcall
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokeoutput_contractapi model stdout r args xs s m w trace ending s′ m′ w′
⊢
∃born : listZ, output_postapi model stdout xs m w born trace ending m′ w′ ∨ ∃why : reason, ending = CallResourcewhy ∧ resource_reasonwhy
inversion Hcall ; subst
2 openworld :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokeoutput_contractapi model stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
H :
contract_abioutput_contractapi model stdout r args
H0 :
contract_preoutput_contractapi model stdout xs m w
H1 :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
H2 :
contract_postoutput_contractapi model stdout xs m w born trace ending m′ w′
H3 :
∀why : reason, ending ≠ CallResourcewhy
H4 :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnsoutput_contractapi model stdout values ∧ Forallword_authoritycontract_sourcesoutput_contractapi model stdout xs m w born m′ values
H5 :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
∃born0 : listZ, output_postapi model stdout xs m w born0 trace ending m′ w′ ∨ ∃why : reason, ending = CallResourcewhy ∧ resource_reasonwhy
focused goal
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
why :
Hcall :
E.invokeoutput_contractapi model stdout r args xs s m w trace CallResourcewhy s′ m′ w′
born :
listZ
H :
contract_abioutput_contractapi model stdout r args
H0 :
contract_preoutput_contractapi model stdout xs m w
H1 :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
H2 :
E.resource_failurecontract_requestsoutput_contractapi model stdout xs m w s′ why
H3 :
contract_resourceoutput_contractapi model stdout why
⊢
∃born0 : listZ, output_postapi model stdout xs m w born0 trace CallResourcewhy m′ w′ ∨ ∃why0 : reason, CallResourcewhy = CallResourcewhy0 ∧ resource_reasonwhy0
–left
2 openworld :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
ending :
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokeoutput_contractapi model stdout r args xs s m w trace ending s′ m′ w′
born :
listZ
H :
contract_abioutput_contractapi model stdout r args
H0 :
contract_preoutput_contractapi model stdout xs m w
H1 :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
H2 :
contract_postoutput_contractapi model stdout xs m w born trace ending m′ w′
H3 :
∀why : reason, ending ≠ CallResourcewhy
H4 :
∀values : listword, ending = CallReturnvalues → return_shapecontract_returnsoutput_contractapi model stdout values ∧ Forallword_authoritycontract_sourcesoutput_contractapi model stdout xs m w born m′ values
H5 :
∀status : Z, ending = CallExitstatus → ∃before : listevent, trace = before ++ ProcessExitstatus
⊢
∃born0 : listZ, output_postapi model stdout xs m w born0 trace ending m′ w′
deferred goal
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
why :
Hcall :
E.invokeoutput_contractapi model stdout r args xs s m w trace CallResourcewhy s′ m′ w′
born :
listZ
H :
contract_abioutput_contractapi model stdout r args
H0 :
contract_preoutput_contractapi model stdout xs m w
H1 :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
H2 :
E.resource_failurecontract_requestsoutput_contractapi model stdout xs m w s′ why
H3 :
contract_resourceoutput_contractapi model stdout why
⊢
∃born0 : listZ, output_postapi model stdout xs m w born0 trace CallResourcewhy m′ w′ ∨ ∃why0 : reason, CallResourcewhy = CallResourcewhy0 ∧ resource_reasonwhy0
match goal withHpost : contract_post_ _ _ _ _ _ _ _ |- _⇒exists born ; exact Hpostend
deferred goal
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
why :
Hcall :
E.invokeoutput_contractapi model stdout r args xs s m w trace CallResourcewhy s′ m′ w′
born :
listZ
H :
contract_abioutput_contractapi model stdout r args
H0 :
contract_preoutput_contractapi model stdout xs m w
H1 :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
H2 :
E.resource_failurecontract_requestsoutput_contractapi model stdout xs m w s′ why
H3 :
contract_resourceoutput_contractapi model stdout why
⊢
∃born0 : listZ, output_postapi model stdout xs m w born0 trace CallResourcewhy m′ w′ ∨ ∃why0 : reason, CallResourcewhy = CallResourcewhy0 ∧ resource_reasonwhy0
–right
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
why :
Hcall :
E.invokeoutput_contractapi model stdout r args xs s m w trace CallResourcewhy s′ m′ w′
born :
listZ
H :
contract_abioutput_contractapi model stdout r args
H0 :
contract_preoutput_contractapi model stdout xs m w
H1 :
E.prefixoutput_contractapi model stdout xs s m w born trace s′ m′ w′
H2 :
E.resource_failurecontract_requestsoutput_contractapi model stdout xs m w s′ why
H3 :
contract_resourceoutput_contractapi model stdout why
⊢
∃why0 : reason, CallResourcewhy = CallResourcewhy0 ∧ resource_reasonwhy0
eauto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros world api model stdout r args xs s m w trace ending s′ m′ w′ Hcall
inversion Hcall ; subst
–left
match goal withHpost : contract_post_ _ _ _ _ _ _ _ |- _⇒exists born ; exact Hpostend
–right
eauto
Hello's output frames need a canonical W, not successful output or an exact fputs byte count. Negative results remain canonical too.
E.invokeoutput_contractapi model stdout r args xs s m w trace CallReturnvalues s′ m′ w′
∃result, values = WIntresult ∧ 0 ≤ result < 2 ^ 32
Explore proof 6 tactics
Initial goal
⊢
∀world : Type api : narrow_api model : stream_modelworld stdout : world → ptr r : call_result args : listarg xs : listword s : R.state m : mem w : world trace : listevent values : listword s′ : R.state m′ : mem w′ : world, E.invokeoutput_contractapi model stdout r args xs s m w trace CallReturnvalues s′ m′ w′ → ∃result : Z, values = WIntresult ∧ 0 ≤ result < 2 ^ 32
intros world api model stdout r args xs s m w trace values s′ m′ w′ Hcall
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokeoutput_contractapi model stdout r args xs s m w trace CallReturnvalues s′ m′ w′
⊢
∃result : Z, values = WIntresult ∧ 0 ≤ result < 2 ^ 32
destruct output_invocation_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & info & info′ & bytes & actions & tail & result & _ & _ & _ & _ & _ & _ & _ & _ & Hr & _ & Hend | why & Hbad & _ ; | discriminate Hbad
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
values :
listword
s′ :
R.state
m′ :
w′ :
world
Hcall :
E.invokeoutput_contractapi model stdout r args xs s m w trace CallReturnvalues s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
result :
Z
Hr :
output_resultapi bytes acceptedactions result
Hend :
CallReturnvalues = CallReturnWIntresult
⊢
∃result0 : Z, values = WIntresult0 ∧ 0 ≤ result0 < 2 ^ 32
injection Hend as →
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
result :
Z
Hcall :
E.invokeoutput_contractapi model stdout r args xs s m w trace CallReturnWIntresult s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hr :
output_resultapi bytes acceptedactions result
exists result
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
result :
Z
Hcall :
E.invokeoutput_contractapi model stdout r args xs s m w trace CallReturnWIntresult s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hr :
output_resultapi bytes acceptedactions result
split ; reflexivity |
world :
Type
api :
model :
stream_modelworld
stdout :
world → ptr
r :
args :
listarg
xs :
listword
s :
R.state
m :
w :
world
trace :
listevent
s′ :
R.state
m′ :
w′ :
world
result :
Z
Hcall :
E.invokeoutput_contractapi model stdout r args xs s m w trace CallReturnWIntresult s′ m′ w′
born :
listZ
info, info′ :
bytes :
listZ
actions :
liststream_action
tail :
listZ
Hr :
output_resultapi bytes acceptedactions result
⊢
0 ≤ result < 2 ^ 32
destruct Hr as _ & Hrange & _ | Hrange ; unfold negative_int in * ; lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros world api model stdout r args xs s m w trace values s′ m′ w′ Hcall
destruct output_invocation_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hcall as born & info & info′ & bytes & actions & tail & result & _ & _ & _ & _ & _ & _ & _ & _ & Hr & _ & Hend | why & Hbad & _ ; | discriminate Hbad
injection Hend as →
exists result
split ; reflexivity |
destruct Hr as _ & Hrange & _ | Hrange ; unfold negative_int in * ; lia
Standalone compatibility wrapper; logic clients use FormattingOn with their actual exported machine instance.
Include FormattingOn R M
%n is not silently admitted as a read-only conversion.
Explore proof 2 tactics
Initial goal
⊢
∀m : mem args : listword bytes : listZ, ¬narrow_formatm 37; 110 args bytes
intros m args bytes H
⊢
False
inversion H ; subst ; try lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m args bytes H
inversion H ; subst ; try lia
Decimal signedness distinguishes canonical negative one from the corresponding unsigned integer.
Explore proof 8 tactics
Initial goal
⊢
formatted_inttrue 2 ^ 32 − 1 45; 49
split ; lia |
⊢
let value ≔
true && 2 ^ 31 ≤? 2 ^ 32 − 1
→
2 ^ 32 − 1 − 2 ^ 32
else
2 ^ 32 − 1
in
else
decimal_digits45; 49 value
change ∃digits, 45; 49 = 45 :: digits ∧ decimal_digitsdigits 1
⊢
∃digits : listZ, 45; 49 = 45 :: digits ∧ decimal_digitsdigits 1
exists 49
⊢
45; 49 = 45; 49 ∧ decimal_digits49 1
split ; reflexivity |
⊢
decimal_digits49 1
unfold decimal_digits
⊢
49 ≠ [ ] ∧ Forallλd : Z ⇒ 48 ≤ d ≤ 57 49 ∧ hd48 49 = 48 → 49 = 48 ∧ fold_leftλacc d : Z ⇒ 10 × acc + d − 48 49 0 = 1
split ; discriminate |
⊢
Forallλd : Z ⇒ 48 ≤ d ≤ 57 49 ∧ hd48 49 = 48 → 49 = 48 ∧ fold_leftλacc d : Z ⇒ 10 × acc + d − 48 49 0 = 1
split ; repeat constructor ; lia |
⊢
hd48 49 = 48 → 49 = 48 ∧ fold_leftλacc d : Z ⇒ 10 × acc + d − 48 49 0 = 1
split ; simpl ; discriminate | reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
split ; lia |
change ∃digits, 45; 49 = 45 :: digits ∧ decimal_digitsdigits 1
exists 49
split ; reflexivity |
unfold decimal_digits
split ; discriminate |
split ; repeat constructor ; lia |
split ; simpl ; discriminate | reflexivity
Even full acceptance may be followed by a negative format result.
Explore proof 3 tactics
Initial goal
⊢
output_resultNarrowPrintf 65; 66 65; 66 stream_eof
right
unfold negative_int , stream_eof
⊢
2 ^ 31 ≤ 2 ^ 32 − 1 < 2 ^ 32
lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A nonnegative formatted result counts bytes; fputs alone may return an arbitrary nonnegative int.
Explore proof 1 tactics
Initial goal
⊢
¬output_resultNarrowPrintf 65; 66 65; 66 1
intros _ & _ & Hapi | Hcount | Hnegative ; simpl in * ; unfold negative_int in * ; congruence || lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros _ & _ & Hapi | Hcount | Hnegative ; simpl in * ; unfold negative_int in * ; congruence || lia
Missing or integer-class %s arguments fail admission, not just a particular successful output result.
Explore proof 2 tactics
Initial goal
⊢
∀m : mem bytes : listZ, ¬narrow_formatm 37; 115 WInt0 bytes
intros m bytes H
⊢
False
inversion H ; subst ; try lia
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros m bytes H
inversion H ; subst ; try lia