proven_c_lib-v0.1.0
The RFC-0008 release: six security and boundary defects fixed, a rule for protected
destinations, errors a caller can act on, and native Windows verified on 64 and 32 bit.
MINOR, not PATCH, because behaviour changes: an atomic write, copy or rename over a
read-only destination is now refused, and several failures that were PROVEN_ERR_IO now
name themselves. v0.0.1 was set on 2026-09-04 and tagged only now, at its own commit; it
was never published as a GitHub release.
Changed
- Windows: an atomic write replaces a file someone is reading, as on POSIX (RFC-0008
Decision 2, option (b), the owner's choice). The rename now tries the POSIX-semantics
rename first (SetFileInformationByHandlewithFileRenameInfoEx,
REPLACE_IF_EXISTS | POSIX_SEMANTICS, Windows 10 1809+): a reader that allowed delete
sharing - whichproven_fs_opendoes - no longer blocks the write, and its open handle
keeps the old bytes. Where Windows or the volume answers "unsupported" (older Windows,
FAT/exFAT, many network shares) it falls back toMoveFileExW, and there the write is
refused withPROVEN_ERR_BUSYas before. A reader that did NOT allow delete sharing
blocks it on every Windows: BUSY. Verified on the Windows 11 VM, x86-64 and i686, plus a
test build that forces the fallback: 41 checks each, none failed. On FAT32 and exFAT
disks attached to the VM the POSIX rename answersERROR_INVALID_PARAMETER, the
fallback runs, and all three builds pass there too (nine runs in all). The same holds on
a Windows SMB network drive (a share on the VM mapped back to it): INVALID_PARAMETER,
fallback, 41 checks each for all three builds. Pre-1809 Windows and a Samba server were
not available to run on.
Fixed
- Windows: a replacement blocked by a file in use now says BUSY, not PERMISSION. Found by
the first run on the Windows 11 test VM (2026-09-11):MoveFileExWanswers
ERROR_ACCESS_DENIEDboth for a read-only destination and for one another process holds
open - with any sharing mode, delete sharing included - and never a sharing violation. The
platform layer mapped that straight to "denied", so an atomic write over a file someone was
merely reading told the caller the file was protected. The Windows rename now asks the file
after a refusal (read-only attribute, then an open for DELETE) and answers
PROVEN_ERR_BUSYfor the in-use case. The branch that expected a sharing violation from
MoveFileExWnever fired; it is kept but documented as such. - Windows: a failed path conversion in rename no longer reports success. The allocation
failure path returnedfalse, which is 0, which isPROVEN_SYS_FS_RENAME_OK. - Verified on the VM, x86-64 and i686, gcc 16.2 mingw static builds: 38 checks each, none
failed. 32-bit Windows is now confirmed rather than explained. - The job-system deadlock fix now has a Windows run.
tests/test_regression_job_permit_starvation
was proven on the POSIX semaphore path only; built statically for x86-64 and i686 and run on
the Windows 11 test VM (theCreateSemaphoreWpath), it passes on both.
Security
-
A staging file is now created private, not narrowed afterwards (RFC-0008 H-002).
Replacing a 0600 file withproven_fs_write_file_atomicorproven_fs_write_file_durable
wrote the new contents into a.pvtmpNNsibling that was created with0666 & ~umask
and narrowed a moment later. Achmoddoes not reach a descriptor another local user
opened during that moment: that descriptor stays open, stays readable, and then reads the
private payload. The staging file is now created owner-only by the creating call itself,
and the target's mode is applied through the open handle rather than by re-resolving the
staging name. A new destination ofproven_fs_copyis created the same way. The process
umask is not touched - it is shared mutable state. -
A failed metadata lookup no longer reads as "no such file" (RFC-0008 H-002).
internal_write_file_atomictreated anystatfailure as a missing target and carried
on with default permissions. It now stops before creating anything unless the target is
genuinely absent. The platform layer gainedproven_sys_fs_stat_checked, which
distinguishes the two; the publicproven_fs_statis unchanged and still answers
PROVEN_ERR_IOfor both. -
Encoding sizes are computed with checked arithmetic (RFC-0008 H-001).
proven_hex_encoded_size,proven_base64_encoded_sizeandproven_base64_decoded_size
multiplied and added inproven_size_tand wrapped at the top of the range - all three
answered 0 for the inputs where they should have said "that does not fit", and 0 passes
every capacity check there is. The encoders repeated the same arithmetic internally, so
fixing the helpers alone would not have protected them: a wrappedneedpassed
need > out_capand the loop then wrote past the caller's buffer. -
A failed atomic write no longer leaves its staging file behind on Windows (RFC-0008
H-005 follow-up, found by the first native run on 2026-09-10). The staging file carries
the target's mode; when that target is read-only, the mode is the READONLY attribute, and
Windows will not delete a read-only file - so the cleanup after a refused replacement
failed silently and the debris stayed. Owner-write is now held back until the payload is
written (it is not a read permission, so nothing about confidentiality changes), the exact
target mode goes on before the rename that publishes the file, and the cleanup path
restores write permission before removing. Found by running the code, not by reading it, and
confirmed by a second native run on the same machine: 31 checks, none failed. -
Windows: an atomic write can replace a file that already exists (RFC-0008 H-005,
first recorded as RFC-0007 C-001).proven_sys_fs_renameusedMoveFileW, which fails
outright when the destination exists - and both whole-file atomic writes rename a staging
file over their target, so on Windows the first write to a name succeeded and every write
after it failed. NowMoveFileExWwithMOVEFILE_REPLACE_EXISTING, without
MOVEFILE_COPY_ALLOWED(a cross-volume copy-and-delete is not atomic) and without
deleting the destination first (that opens an interval in which the name does not exist).
Implemented and cross-compiled for both Windows targets; not run natively, so the
behaviour against a read-only destination, ACLs, sharing modes and symlinks has no result. -
Windows: every requested entropy byte is actually requested (RFC-0008 H-006, first
recorded as RFC-0007 V-003).proven_sys_random_bytescast itssize_tlength once to
theULONGthatBCryptGenRandomtakes. On 64-bit Windows a length aboveULONG_MAX
narrowed silently - a request for exactly 2^32 bytes asked the OS for zero - and the
success of that short request was returned as success for the whole buffer, so a caller
read bytes nothing had written as fresh entropy. The request is now made in chunks the
backend accepts, the pointer advances only after the OS reports success, and a failed
chunk fails the whole call; there is no fallback to a PRNG. Failure may leave a filled
prefix, which the boolean API cannot report, so a caller must discard the whole buffer.
Implemented and cross-compiled; not run natively. -
A protected destination is refused, by every whole-file replacement (RFC-0008
follow-up; the owner's decision, 2026-09-10).proven_fs_write_file,
proven_fs_write_file_atomic,proven_fs_write_file_durableandproven_fs_copynow
returnPROVEN_ERR_PERMISSIONwhen the destination's owner-write bit is clear, and leave
the file exactly as it was. That bit is where both platforms record "do not write this
file": mode0200on POSIX, the READONLY attribute on Windows.It had been three answers to one question on ONE platform, measured:
write_filerefused
(it opens the destination for writing),write_file_atomicsucceeded (renameasks the
DIRECTORY for permission, so the file's mode was never consulted), andcopysucceeded
and left a 0444 file as 0664 - a protection the caller had set, gone, with nothing
saying so. The Windows/POSIX divergence RFC-0008 recorded was the fourth face of the same
unresolved question, not a portability wart.This is a behaviour change. Code that replaced a read-only file through
write_file_atomic,write_file_durableorcopynow getsPROVEN_ERR_PERMISSION; the
caller lifts the mark first, which is one line and visible. In particular the backup loop
intests/test_regression_fs_perms_and_types- copying a read-only source onto the same
destination twice - now fails on the second run. That behaviour was deliberately added
once, and is deliberately reversed here: the failure it produced then was
PROVEN_ERR_IO, which a caller cannot act on, and the cure was stripping the
destination's protection without saying so. It is not a security boundary: the mode is
read before the work and acted on after it, and anyone who canchmodcan lift the mark.
Changed
-
proven_fs_renameobeys the protected-destination rule, andproven_fs_removedoes
not. An audit of every public door against a0444file found two that did not follow
the rule the rest do.proven_fs_renamereplaced the protected file outright - contents
and mode both - and it is what the atomic write is built on, so a caller refused by
proven_fs_write_file_atomicgot the result fromproven_fs_renameinstead. It refuses
now.proven_fs_removestill deletes: a name is removed from a directory, and POSIX has
never let the file's own mode have a say in that; refusing there would break ordinary
cleanup of read-only files for a rule about writing. Windows does refuse it, and that
difference is now reported asPROVEN_ERR_PERMISSIONinstead of hidden behind an I/O
error.tests/test_contract_protected_destinationchecks every door one by one, so a
door added to the public API without one is a build failure rather than a discovery. -
proven_fs_open,proven_fs_renameandproven_fs_removesay WHICH failure it was.
PROVEN_ERR_NOT_FOUNDwhen the name is not there,PROVEN_ERR_PERMISSIONwhen the caller
may not,PROVEN_ERR_BUSYwhen something else holds it; everything else stays
PROVEN_ERR_IO. They used to answerPROVEN_ERR_IOfor all of it, and one code for
"ask the user", "retry" and "give up" is a code a caller cannot act on. The platform layer
gainedproven_sys_fs_open_checkedandproven_sys_fs_rename_checkedto carry the
distinction, andproven_sys_fs_remove_checkedwith them; the boolean wrappers remain.
Fixed
-
A durable write syncs the directory the file is actually in (RFC-0008 H-003).
internal_parent_dirtreated/and\as separators on every platform. On POSIX a
backslash is an ordinary character in a filename, so a durable write tod/a\b- one
file calleda\binsided- tried to syncd/a. When that name does not exist the
call returned an I/O error after the rename had already published the new contents;
when it happened to be a directory, the wrong directory was synced and the call reported
a durability it had not achieved. The separator rule is now the platform's own, and the
same rule measures the basename the staging name is derived from - a long name full of
backslashes used to be measured as a short one, so the staging name was never trimmed to
fit.proven_fs_is_absoluteis unchanged: it classifies a path that may have come from
elsewhere rather than resolving one here, which is a different question. -
The job queue no longer compares positions with a signed subtraction (RFC-0008 H-004).
proven_job_submitandproven_job_execute_onecomputed
(proven_ptrdiff_t)seq - (proven_ptrdiff_t)pos. The queue's counters run forward for
ever and wrap; only their distance is small. At the sign boundary those two casts can
producePTRDIFF_MAXandPTRDIFF_MIN, and subtracting them is signed overflow -
undefined behaviour, reached by a legitimately full queue with no concurrency involved.
The distance is now taken in the unsigned counter type, where wrapping is defined and is
the modular arithmetic the algorithm wants, through one shared helper used by both sides.
Memory ordering, admission, wake permits and drain behaviour are untouched.
Changed
- A job queue capacity at or past half the counter range is refused (RFC-0008 H-004).
proven_job_system_initanswersPROVEN_ERR_INVALID_ARGbefore it allocates anything.
Past that limit "ahead" and "behind" stop being distinguishable, so it is a correctness
condition rather than a resource one. No reachable capacity is affected. - The encoded-size helpers answer
PROVEN_SIZE_MAXfor a size that cannot be
represented (RFC-0008 H-001). They return a size and have nowhere to put an error. A
valid hex output is always even and a valid padded Base64 output is always a multiple of
four, so neither can bePROVEN_SIZE_MAXby accident; zero was not usable as the
sentinel because zero is the honest answer for empty input.proven_base64_decoded_size
needs no sentinel - its largest value fits - and now reaches it without wrapping on the
way. The encoders make the same judgement independently and answer the new
PROVEN_ERR_OVERFLOW, which is a different answer fromPROVEN_ERR_OUT_OF_BOUNDS: the
size does not exist, rather than the buffer being smaller than it. Nothing is read or
written on either refusal. - Unchanged on purpose: a brand-new atomic target still gets
0666 & ~umask. Restrictive
creation carries an existing target's mode across; it is not a new default-permissions
policy, which would be an owner decision. tests/test_docs_version_syncskips an## [Unreleased]section when it looks for the
newest released entry. The gate and the maintainers' operations notes had been asking for
opposite things.