From dff1aeaf71d5959e98a3a3b3ce261dbf0d705317 Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gregory@skylabs-ai.com>
Date: Mon, 27 Apr 2026 15:30:10 -0400
Subject: [PATCH] The standard does not guarantee that these functions return 0
 or 1

---
 rocq-brick-libstdcpp/proof/cctype/spec.v | 25 +++++++++++++-----------
 1 file changed, 14 insertions(+), 11 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/cctype/spec.v b/rocq-brick-libstdcpp/proof/cctype/spec.v
index 0e4c6f5..c8d221e 100644
--- a/rocq-brick-libstdcpp/proof/cctype/spec.v
+++ b/rocq-brick-libstdcpp/proof/cctype/spec.v
@@ -23,60 +23,63 @@ Section with_cpp.
   (* TODO: these functions should be [extern "C"] and specified with
   [cpp.spec "isalpha" with], troubleshoot why this doesn't work on Mac. *)
 
+  (** Determine if <i> represents <true> or <false>. *)
+  #[local] Notation int_bool i b := (bool_decide (i <> 0) = b) (only parsing).
+
   cpp.spec (named "isalpha") with
     (\arg{c} "c" (Vint c)
      \require VALID c
-     \post[Vbool (isalpha c)] emp).
+     \post{z}[Vint z] [| int_bool z (isalpha c) |]).
 
   cpp.spec (named "isdigit") with
     (\arg{c} "c" (Vint c)
      \require VALID c
-     \post[Vbool (isdigit c)] emp).
+     \post{z}[Vint z] [| int_bool z (isdigit c) |]).
 
   cpp.spec (named "isalnum") with
     (\arg{c} "c" (Vint c)
      \require VALID c
-     \post[Vbool (isalnum c)] emp).
+     \post{z}[Vint z] [| int_bool z (isalnum c) |]).
 
   cpp.spec (named "isspace") with
     (\arg{c} "c" (Vint c)
      \require VALID c
-     \post[Vbool (isspace c)] emp).
+     \post{z}[Vint z] [| int_bool z (isspace c) |]).
 
   cpp.spec (named "islower") with
     (\arg{c} "c" (Vint c)
      \require VALID c
-     \post[Vbool (islower c)] emp).
+     \post{z}[Vint z] [| int_bool z (islower c) |]).
 
   cpp.spec (named "isupper") with
     (\arg{c} "c" (Vint c)
      \require VALID c
-     \post[Vbool (isupper c)] emp).
+     \post{z}[Vint z] [| int_bool z (isupper c) |]).
 
   cpp.spec (named "isprint") with
     (\arg{c} "c" (Vint c)
      \require VALID c
-     \post[Vbool (isprint c)] emp).
+     \post{z}[Vint z] [| int_bool z (isprint c) |]).
 
   cpp.spec (named "ispunct") with
     (\arg{c} "c" (Vint c)
      \require VALID c
-     \post[Vbool (ispunct c)] emp).
+     \post{z}[Vint z] [| int_bool z (ispunct c) |]).
 
   cpp.spec (named "iscntrl") with
     (\arg{c} "c" (Vint c)
      \require VALID c
-     \post[Vbool (iscntrl c)] emp).
+     \post{z}[Vint z] [| int_bool z (iscntrl c) |]).
 
   cpp.spec (named "isgraph") with
     (\arg{c} "c" (Vint c)
      \require VALID c
-     \post[Vbool (isgraph c)] emp).
+     \post{z}[Vint z] [| int_bool z (isgraph c) |]).
 
   cpp.spec (named "isxdigit") with
     (\arg{c} "c" (Vint c)
      \require VALID c
-     \post[Vbool (isxdigit c)] emp).
+     \post{z}[Vint z] [| int_bool z (isxdigit c) |]).
 
   (* Specifications for Character Conversion Functions *)