From 44596ad68b843dcc280e2ce800581b8c8606dde6 Mon Sep 17 00:00:00 2001 From: Mahad Khan Date: Mon, 7 Sep 2026 14:09:17 +0500 Subject: [PATCH] istream: require representable integer extraction results --- rocq-brick-libstdcpp/proof/iostream/spec.v | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/iostream/spec.v b/rocq-brick-libstdcpp/proof/iostream/spec.v index 3077914b..7e6c071e 100644 --- a/rocq-brick-libstdcpp/proof/iostream/spec.v +++ b/rocq-brick-libstdcpp/proof/iostream/spec.v @@ -218,7 +218,11 @@ Module istream. end ). - (** TODO: this specification is unsound because it needs to re-buffer the + (** This contract only covers parsed values representable as [int]. + Out-of-range extraction saturates and sets [failbit], which the current + stream predicate does not model. + + TODO: this specification is unsound because it needs to re-buffer the next character that it read (the first component of the pair returned by [read_int]). *) @@ -228,7 +232,9 @@ Module istream. \pre{IS isM} this |-> istream.R IS isM 1$m \arg{nP} "" (Vref nP) \pre nP |-> anyR "int" 1$m - \pre{K : Z -> mpred} interp_itree as_event IS read_int (K ∘ snd) + \pre{K : Z -> mpred} interp_itree as_event IS read_int (fun '(_, n) => + [| (int_rank.min_val int_rank.Iint Signed <= n <= + int_rank.max_val int_rank.Iint Signed)%Z |] ** K n) \post[Vptr this] Exists isM' n, this |-> istream.R IS isM' 1$m ** nP |-> intR 1$m n **