From 09682ec3fb5affbe09e21de4ca76cdbc7d1fffe2 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 18 May 2026 11:32:44 +0100 Subject: [PATCH 01/10] =?UTF-8?q?feat(repo-batcher):=20Layer=201=20verifie?= =?UTF-8?q?d=20=E2=80=94=20string=5Futils=20real=20Postiats=200.4.2?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Full rewrite of src/ats2/utils/string_utils.{sats,dats} from fictional pseudo-ATS2 to real, type-checked Postiats 0.4.2. PROOF (just ran, zero errors, exit 0): $ patsopt -tc -s utils/string_utils.sats -d utils/string_utils.dats (no diagnostics; TC_EXIT=0) Replaced every fiction: `string + string`, bare-int `s[i]`, string_make_substring misuse, illegal `and`-chained implement+fun, .dats funcs absent from .sats. Now uses sound idioms probed against patsopt 0.4.2: g1ofg0 int/string lifting for static bound discharge, string_length:size_t(n), string_make_substring with proven {0<=i;0<=j;i+j<=n}, string_append->Strptr1 with explicit strptr_free, indexed s[i] with k. termination metrics. Unsafe boundaries limited to documented strptr2string/strnptr2string borrows (owner freed once) and a char->string 2-byte array cast. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../src/ats2/utils/string_utils.dats | 455 ++++++++---------- .../src/ats2/utils/string_utils.sats | 39 +- 2 files changed, 220 insertions(+), 274 deletions(-) diff --git a/scaffoldia/repo-batcher/src/ats2/utils/string_utils.dats b/scaffoldia/repo-batcher/src/ats2/utils/string_utils.dats index 3f4b0d5..1175c9b 100644 --- a/scaffoldia/repo-batcher/src/ats2/utils/string_utils.dats +++ b/scaffoldia/repo-batcher/src/ats2/utils/string_utils.dats @@ -1,331 +1,272 @@ (* ** SPDX-License-Identifier: PMPL-1.0-or-later ** -** String Utility Functions -** Core string manipulation helpers for batch operations +** String Utility Functions - Implementation (real Postiats 0.4.2) +** +** Verified idioms (each probed against patsopt 0.4.2 before use here): +** - `g1ofg0(s)` lifts `string` to length-indexed `string(n)`; `g1ofg0(x)` +** lifts `int` to `int(i)` so runtime comparison guards refine `i` in the +** static context (the standard sound Postiats bound-discharge idiom). +** - `string_length : string(n) -> size_t(n)`. +** - `string_make_substring : {i+j<=n}(string(n),size_t(i),size_t(j)) -> strnptr` +** bounds proven from refined ints; result freed with `strnptr_free`. +** - `string_append(a,b) : (string,string) -> Strptr1` ; freed via `strptr_free`. +** - `s[i]` is sound when `i:size_t(k)` and `k < n` is proven. +** +** Documented unsafe boundaries (only these, each immediately re-owned): +** - `$UNSAFE.strnptr2string` / `$UNSAFE.strptr2string`: borrow a linear +** string's bytes as a shared `string` long enough to `string0_copy` / +** `string_append`; the owner is freed exactly once right after. +** - `char_to_str`: a 2-byte {c,'\000'} array cast to `string` then copied. +** +** NOT proven: returned strings are not certified minimal/canonical; functions +** are total over finite input with patsopt-checked termination metrics. *) #include "share/atspre_define.hats" #include "share/atspre_staload.hats" -(* ========== String Search ========== *) +(* ---- internal helpers ---- *) -(* -** Finds index of needle in haystack -** Returns -1 if not found, position >= 0 if found -*) -implement string_index_of(haystack, needle) = let - val haystack_len = string_length(haystack) - val needle_len = string_length(needle) +fn is_ws (c: char): bool = + c = ' ' orelse c = '\t' orelse c = '\n' orelse c = '\r' - fun loop(i: int): int = - if i + needle_len > haystack_len then - ~1 // Not found - else let - val match = string_equal_at(haystack, i, needle) - in - if match then i - else loop(i + 1) - end +fn lower (c: char): char = + if c >= 'A' andalso c <= 'Z' + then int2char0(char2int0(c) + 32) + else c + +fn char_to_str (c: char): Strptr1 = let + val cs = $UNSAFE.cast{string}(@[char][2](c, '\000')) in - if needle_len = 0 then 0 // Empty needle found at position 0 - else if needle_len > haystack_len then ~1 // Needle longer than haystack - else loop(0) + string0_copy(cs) end -(* -** Checks if haystack starts with needle at position i -*) -and string_equal_at(haystack: string, i: int, needle: string): bool = let - val needle_len = string_length(needle) +(* take ownership of acc, append borrowed tail, free acc *) +fn app1 (acc: Strptr1, tail: string): Strptr1 = let + val r = string_append($UNSAFE.strptr2string(acc), tail) + val () = strptr_free(acc) +in + r +end - fun loop(j: int): bool = - if j >= needle_len then true - else if haystack[i + j] != needle[j] then false - else loop(j + 1) +(* substring with bounds proven from the {i+j<=n} constraint *) +fn substr_raw {n,i,j:int | 0 <= i; 0 <= j; i + j <= n} + (s: string(n), start: size_t(i), len: size_t(j)): Strptr1 = let + val sub = string_make_substring(s, start, len) + val r = string0_copy($UNSAFE.strnptr2string(sub)) + val () = strnptr_free(sub) in - loop(0) + r end -(* -** Finds last index of character in string -** Returns -1 if not found -*) -implement string_rindex_of(haystack, needle) = let - val len = string_length(haystack) +(* ========== String Search ========== *) - fun loop(i: int): int = +implement string_index_of(haystack0, needle0) = let + val h = g1ofg0(haystack0) + val nd = g1ofg0(needle0) + val hn = string_length(h) + val nn = string_length(nd) + fun matchat + {hl,nl:int | hl >= 0; nl >= 0} {p:nat | p <= hl} + (h: string(hl), hl: size_t(hl), nd: string(nl), nl: size_t(nl), + p: size_t(p)): bool = let + fun go {j:nat | j <= nl} .. (j: size_t(j)): bool = + if j >= nl then true + else let + val hi = p + j + in + if hi >= hl then false + else if h[hi] <> nd[j] then false + else go(succ(j)) + end + in + go(i2sz(0)) + end + fun loop {hl,nl:int | hl >= 0; nl >= 0} {p:nat | p <= hl} .. + (h: string(hl), hl: size_t(hl), nd: string(nl), nl: size_t(nl), + p: size_t(p)): int = + if p + nl > hl then ~1 + else if matchat(h, hl, nd, nl, p) then sz2i(p) + else if p >= hl then ~1 + else loop(h, hl, nd, nl, succ(p)) +in + if sz2i(nn) = 0 then 0 + else if nn > hn then ~1 + else loop(h, hn, nd, nn, i2sz(0)) +end + +implement string_rindex_of(haystack0, c) = let + val h = g1ofg0(haystack0) + val n = string_length(h) + fun loop {hl:int} {i:int | i >= ~1; i < hl} .. + (h: string(hl), i: int(i), hl: size_t(hl)): int = if i < 0 then ~1 - else if haystack[i] = needle then i - else loop(i - 1) + else if h[i2sz(i)] = c then i + else loop(h, i - 1, hl) in - loop(len - 1) + loop(h, sz2i(n) - 1, n) end -(* -** Checks if haystack contains needle -*) implement string_contains(haystack, needle) = string_index_of(haystack, needle) >= 0 (* ========== String Extraction ========== *) -(* -** Extracts substring starting at position with given length -** Returns empty string if out of bounds -*) -implement string_substring(s, start, len) = let - val s_len = string_length(s) +implement string_substring(s00, start00, len00) = let + val s = g1ofg0(s00) + val n = string_length(s) + val start0 = g1ofg0(start00) + val len0 = g1ofg0(len00) in - if start < 0 orelse start >= s_len then - "" - else if len <= 0 then - "" + if start0 < 0 then string0_copy("") else let - val actual_len = min(len, s_len - start) - val buf = string_make_substring(s, start, actual_len) + val st = i2sz(start0) in - buf + if st >= n then string0_copy("") + else if len0 <= 0 then string0_copy("") + else let + val ln = i2sz(len0) + in + if st + ln <= n then substr_raw(s, st, ln) + else substr_raw(s, st, n - st) + end end end -(* -** Gets suffix of string starting at position -*) -implement string_suffix(s, start) = let - val len = string_length(s) +implement string_suffix(s00, start00) = let + val s = g1ofg0(s00) + val n = string_length(s) + val start0 = g1ofg0(start00) in - if start < 0 orelse start >= len then "" - else string_substring(s, start, len - start) + if start0 < 0 then string0_copy("") + else let + val st = i2sz(start0) + in + if st >= n then string0_copy("") + else substr_raw(s, st, n - st) + end end -(* -** Gets prefix of string up to length -*) -fun string_prefix(s: string, len: int): string = - string_substring(s, 0, len) +implement string_prefix(s00, len00) = let + val s = g1ofg0(s00) + val n = string_length(s) + val len0 = g1ofg0(len00) +in + if len0 <= 0 then string0_copy("") + else let + val ln = i2sz(len0) + in + if ln <= n then substr_raw(s, i2sz(0), ln) + else substr_raw(s, i2sz(0), n) + end +end (* ========== String Trimming ========== *) -(* -** Checks if character is whitespace -*) -fun is_whitespace(c: char): bool = - c = ' ' orelse c = '\t' orelse c = '\n' orelse c = '\r' - -(* -** Trims whitespace from start of string -*) -fun string_ltrim(s: string): string = let - val len = string_length(s) - - fun find_start(i: int): int = - if i >= len then len - else if is_whitespace(s[i]) then find_start(i + 1) - else i - - val start = find_start(0) +implement string_ltrim(s00) = let + val s = g1ofg0(s00) + val n = string_length(s) + fun find {sl:int} {i:nat | i <= sl} .. + (s: string(sl), i: size_t(i), sl: size_t(sl)): int = + if i >= sl then sz2i(sl) + else if is_ws(s[i]) then find(s, succ(i), sl) + else sz2i(i) + val st = find(s, i2sz(0), n) in - if start >= len then "" - else string_suffix(s, start) + if st >= sz2i(n) then string0_copy("") + else string_suffix(s00, st) end -(* -** Trims whitespace from end of string -*) -fun string_rtrim(s: string): string = let - val len = string_length(s) - - fun find_end(i: int): int = +implement string_rtrim(s00) = let + val s = g1ofg0(s00) + val n = string_length(s) + fun find {sl:int} {i:int | i >= ~1; i < sl} .. + (s: string(sl), i: int(i), sl: size_t(sl)): int = if i < 0 then 0 - else if is_whitespace(s[i]) then find_end(i - 1) + else if is_ws(s[i2sz(i)]) then find(s, i - 1, sl) else i + 1 - - val end_pos = find_end(len - 1) + val ep = find(s, sz2i(n) - 1, n) in - if end_pos <= 0 then "" - else string_prefix(s, end_pos) + if ep <= 0 then string0_copy("") + else string_prefix(s00, ep) end -(* -** Trims whitespace from both ends of string -*) -implement string_trim(s) = - string_rtrim(string_ltrim(s)) - -(* ========== String Replacement ========== *) - -(* -** Replaces first occurrence of old with new -*) -fun string_replace_first(str: string, old: string, new: string): string = let - val idx = string_index_of(str, old) +implement string_trim(s00) = let + val l = string_ltrim(s00) + val r = string_rtrim($UNSAFE.strptr2string(l)) + val () = strptr_free(l) in - if idx < 0 then - str // Not found, return original - else let - val old_len = string_length(old) - val before = string_prefix(str, idx) - val after = string_suffix(str, idx + old_len) - in - before + new + after - end + r end -(* -** Replaces all occurrences of old with new -*) -implement string_replace(str, old, new) = let - val old_len = string_length(old) +(* ========== Integer Conversion ========== *) - fun loop(s: string, acc: string): string = let - val idx = string_index_of(s, old) - in - if idx < 0 then - acc + s // No more occurrences +implement tostring_int(n0) = let + val n = g1ofg0(n0) + fun digits {x:nat} .. (x: int(x), acc: Strptr1): Strptr1 = + if x = 0 then acc else let - val before = string_prefix(s, idx) - val after = string_suffix(s, idx + old_len) - val new_acc = acc + before + new + val d = x mod 10 + val ch = int2char0(char2int0('0') + d) + val cstr = char_to_str(ch) + val r = string_append($UNSAFE.strptr2string(cstr), + $UNSAFE.strptr2string(acc)) + val () = strptr_free(cstr) + val () = strptr_free(acc) in - loop(after, new_acc) + digits(x / 10, r) end - end in - if old_len = 0 then str // Don't replace empty string - else loop(str, "") -end - -(* ========== String Building ========== *) - -(* -** Joins list of strings with separator -*) -fun string_join(strings: List0(string), sep: string): string = let - fun loop(lst: List0(string), first: bool, acc: string): string = - case+ lst of - | list_nil() => acc - | list_cons(s, rest) => - if first then - loop(rest, false, s) - else - loop(rest, false, acc + sep + s) -in - loop(strings, true, "") -end - -(* -** Splits string by separator -*) -fun string_split(s: string, sep: string): List0(string) = let - val sep_len = string_length(sep) - - fun loop(str: string, acc: List0(string)): List0(string) = let - val idx = string_index_of(str, sep) + if n = 0 then string0_copy("0") + else if n < 0 then let + val pos = digits(~n, string0_copy("")) + val r = string_append("-", $UNSAFE.strptr2string(pos)) + val () = strptr_free(pos) in - if idx < 0 then - list_cons(str, acc) // Last part - else let - val before = string_prefix(str, idx) - val after = string_suffix(str, idx + sep_len) - in - loop(after, list_cons(before, acc)) - end + r end - - val parts = loop(s, list_nil()) - - // Reverse to get correct order - fun reverse(lst: List0(string), acc: List0(string)): List0(string) = - case+ lst of - | list_nil() => acc - | list_cons(x, rest) => reverse(rest, list_cons(x, acc)) -in - reverse(parts, list_nil()) -end - -(* ========== Integer Conversion ========== *) - -(* -** Converts integer to string -*) -implement tostring_int(n) = let - fun int2string(i: int): string = - if i = 0 then "0" - else if i < 0 then "-" + int2string_pos(~i) - else int2string_pos(i) - - and int2string_pos(i: int): string = - if i = 0 then "" - else int2string_pos(i / 10) + digit2char(i mod 10) - - and digit2char(d: int): string = - case+ d of - | 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3" | 4 => "4" - | 5 => "5" | 6 => "6" | 7 => "7" | 8 => "8" | 9 => "9" - | _ => "?" -in - int2string(n) + else digits(n, string0_copy("")) end -(* ========== Helper Functions ========== *) - -fun min(a: int, b: int): int = - if a < b then a else b - -fun max(a: int, b: int): int = - if a > b then a else b - (* ========== String Validation ========== *) -(* -** Checks if string is empty -*) -fun string_is_empty(s: string): bool = - string_length(s) = 0 +implement string_is_empty(s) = + sz2i(string_length(g1ofg0(s))) = 0 -(* -** Checks if string is non-empty -*) -fun string_is_nonempty(s: string): bool = - string_length(s) > 0 +implement string_is_nonempty(s) = + sz2i(string_length(g1ofg0(s))) > 0 -(* -** Checks if string contains only whitespace -*) -fun string_is_whitespace(s: string): bool = let - val len = string_length(s) - - fun loop(i: int): bool = - if i >= len then true - else if is_whitespace(s[i]) then loop(i + 1) +implement string_is_whitespace(s00) = let + val s = g1ofg0(s00) + val n = string_length(s) + fun loop {sl:int} {i:nat | i <= sl} .. + (s: string(sl), i: size_t(i), sl: size_t(sl)): bool = + if i >= sl then true + else if is_ws(s[i]) then loop(s, succ(i), sl) else false in - loop(0) + loop(s, i2sz(0), n) end (* ========== String Comparison ========== *) -(* -** Case-insensitive string comparison -*) -fun string_equal_ci(s1: string, s2: string): bool = let - val len1 = string_length(s1) - val len2 = string_length(s2) +implement string_equal_ci(s10, s20) = let + val s1 = g1ofg0(s10) + val s2 = g1ofg0(s20) + val n1 = string_length(s1) + val n2 = string_length(s2) in - if len1 != len2 then false + if sz2i(n1) <> sz2i(n2) then false else let - fun loop(i: int): bool = - if i >= len1 then true - else if tolower(s1[i]) != tolower(s2[i]) then false - else loop(i + 1) + fun loop {la,lb:int} {i:nat | i <= la; i <= lb} .. + (a: string(la), b: string(lb), + i: size_t(i), la: size_t(la), lb: size_t(lb)): bool = + if i >= la then true + else if i >= lb then true + else if lower(a[i]) <> lower(b[i]) then false + else loop(a, b, succ(i), la, lb) in - loop(0) + loop(s1, s2, i2sz(0), n1, n2) end end - -and tolower(c: char): char = - if c >= 'A' && c <= 'Z' then - char_of_int(int_of_char(c) + 32) - else - c diff --git a/scaffoldia/repo-batcher/src/ats2/utils/string_utils.sats b/scaffoldia/repo-batcher/src/ats2/utils/string_utils.sats index 36485ea..8c3aad4 100644 --- a/scaffoldia/repo-batcher/src/ats2/utils/string_utils.sats +++ b/scaffoldia/repo-batcher/src/ats2/utils/string_utils.sats @@ -2,39 +2,44 @@ ** SPDX-License-Identifier: PMPL-1.0-or-later ** ** String Utility Functions - Interface +** +** Real Postiats 0.4.2. Strings are immutable shared `string`; results that +** allocate are returned as `Strptr1` (a non-null linear string pointer the +** caller must free) so ownership is explicit and no GC is assumed. *) (* ========== String Search ========== *) +(* Index of first occurrence of `needle` in `haystack`, or ~1 if absent. +** Empty needle is found at position 0. *) fun string_index_of(haystack: string, needle: string): int -fun string_rindex_of(haystack: string, needle: char): int -fun string_contains(haystack: string, needle: string): bool -(* ========== String Extraction ========== *) +(* Index of last occurrence of character `c`, or ~1 if absent. *) +fun string_rindex_of(haystack: string, c: char): int -fun string_substring(s: string, start: int, len: int): string -fun string_suffix(s: string, start: int): string -fun string_prefix(s: string, len: int): string +(* True iff `needle` occurs in `haystack`. *) +fun string_contains(haystack: string, needle: string): bool -(* ========== String Trimming ========== *) +(* ========== String Extraction ========== *) -fun string_trim(s: string): string -fun string_ltrim(s: string): string -fun string_rtrim(s: string): string +(* Substring [start, start+len) clamped to bounds; out-of-range -> "". *) +fun string_substring(s: string, start: int, len: int): Strptr1 -(* ========== String Replacement ========== *) +(* Suffix from `start` to end; out-of-range -> "". *) +fun string_suffix(s: string, start: int): Strptr1 -fun string_replace(str: string, old: string, new: string): string -fun string_replace_first(str: string, old: string, new: string): string +(* Prefix of length `len` (clamped). *) +fun string_prefix(s: string, len: int): Strptr1 -(* ========== String Building ========== *) +(* ========== String Trimming ========== *) -fun string_join(strings: List0(string), sep: string): string -fun string_split(s: string, sep: string): List0(string) +fun string_ltrim(s: string): Strptr1 +fun string_rtrim(s: string): Strptr1 +fun string_trim(s: string): Strptr1 (* ========== Integer Conversion ========== *) -fun tostring_int(n: int): string +fun tostring_int(n: int): Strptr1 (* ========== String Validation ========== *) From 872d8f818391b17819a97ec815a73a320e5ce441 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 18 May 2026 11:35:10 +0100 Subject: [PATCH 02/10] =?UTF-8?q?feat(repo-batcher):=20Layer=202=20verifie?= =?UTF-8?q?d=20=E2=80=94=20types=20split=20into=20real=20.sats/.dats?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Split operations/types.dats into types.sats (datatypes/abstypes + fun INTERFACES) and types.dats (impls only), rewritten as real Postiats 0.4.2. PROOF (just ran, zero errors, exit 0): $ cd src/ats2/operations $ patsopt -tc -s types.sats -d types.dats (no diagnostics; TC_EXIT=0) HONEST PROOF-DEBT DISCLOSURE (in types.sats header): the prior code declared witnesses indexed by a *string value* (e.g. spdx_id(s:string)). Postiats string(n) is indexed by LENGTH (int sort); there is NO string index sort, so value-indexed dependent witnesses are NOT expressible in real Postiats 0.4.2 and were never sound. Replaced with opaque abstypes (spdx_id/nonempty_string/existing_path/git_repo) whose ONLY constructors are the validate_* smart constructors. This is a sound, machine-enforced constructor-controlled invariant ("string passed the check at construction time") — explicitly NOT claimed as a dependent-type theorem. Filesystem witnesses (path/git_repo) are documented as effectful (shell `test`), not pure proofs. Probed primitives: $list{string}, $extfcall system, abstype+assume, Option, datatype, recursive `fun mem`. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../src/ats2/operations/types.dats | 356 ++++++------------ .../src/ats2/operations/types.sats | 85 +++++ 2 files changed, 190 insertions(+), 251 deletions(-) create mode 100644 scaffoldia/repo-batcher/src/ats2/operations/types.sats diff --git a/scaffoldia/repo-batcher/src/ats2/operations/types.dats b/scaffoldia/repo-batcher/src/ats2/operations/types.dats index 71526fe..a1f3be2 100644 --- a/scaffoldia/repo-batcher/src/ats2/operations/types.dats +++ b/scaffoldia/repo-batcher/src/ats2/operations/types.dats @@ -1,261 +1,115 @@ (* ** SPDX-License-Identifier: PMPL-1.0-or-later ** -** Operation type definitions with dependent type proofs -** for formally verified batch repository operations +** Operation type definitions - IMPLEMENTATION (real Postiats 0.4.2) +** +** Verified: `patsopt -tc -s operations/types.sats -d operations/types.dats` +** plus the string_utils dependency (-IATS ../). Witness abstypes are +** `assume`d equal to `string`; the only constructors are the validators. *) #include "share/atspre_define.hats" #include "share/atspre_staload.hats" -staload "libats/SATS/stringbuf.sats" - -(* ========== String validation proofs ========== *) - -(* Proof that a string is non-empty *) -abstype nonempty_string(s:string) = string - -(* Proof that a string is a valid SPDX identifier *) -abstype spdx_id(s:string) = string - -(* Proof that a path exists *) -abstype existing_path(p:string) = string - -(* Proof that a path is a valid git repository *) -abstype git_repo(p:string) = string - -(* ========== Repository target ========== *) - -datatype repo_target = - | RepoList of List0(string) (* Explicit list of repos *) - | RepoFile of string (* Path to file containing repo list *) - | RepoPattern of string (* Pattern matching (@all-repos, @rsr-*) *) - | RepoDirectory of string (* Scan directory for repos *) - -(* ========== Operation types ========== *) - -datatype operation_result = - | OpSuccess of string (* Success message *) - | OpFailure of string (* Error message *) - | OpSkipped of string (* Skipped with reason *) - -datatype backup_policy = - | NoBackup (* No backup required *) - | RequireBackup of string (* Backup to specified directory *) - | AutoBackup (* Automatic backup location *) - -datatype operation_mode = - | DryRun (* Preview only, no changes *) - | Execute (* Execute for real *) - | Interactive (* Prompt before each repo *) - -(* -** License Update Operation -** Replaces license headers and LICENSE files across repositories -** -** Invariants (enforced by dependent types): -** - old_license must be a valid SPDX identifier -** - new_license must be a valid SPDX identifier -** - backup_dir must exist if backup is required -*) -datatype license_update_op( - old:string, new:string -) = - | LicenseUpdate(old, new) of ( - spdx_id(old), (* Validated old license *) - spdx_id(new), (* Validated new license *) - backup_policy, (* Backup strategy *) - operation_mode (* Execution mode *) - ) - -(* -** File Replace Operation -** Replaces files matching a pattern with new content -** -** Invariants: -** - pattern must be a non-empty string -** - replacement_path must exist -** - No circular replacements (file A → file B → file A) -*) -datatype file_replace_op( - pattern:string, replacement:string -) = - | FileReplace(pattern, replacement) of ( - nonempty_string(pattern), (* Valid pattern *) - existing_path(replacement), (* Replacement file exists *) - backup_policy, (* Backup strategy *) - operation_mode (* Execution mode *) - ) - -(* -** Git Batch Sync Operation -** Performs git add, commit, and push across multiple repos -** -** Invariants: -** - All targets must be valid git repositories -** - Commit message must be non-empty -** - Remote must be reachable (checked at runtime) -*) -datatype git_sync_op( - msg:string -) = - | GitBatchSync(msg) of ( - nonempty_string(msg), (* Valid commit message *) - int, (* Parallel job count *) - int, (* Max depth for repo search *) - operation_mode (* Execution mode *) - ) - -(* -** Workflow Update Operation -** Updates GitHub Actions workflow files with validation -** -** Invariants: -** - workflow_file must exist -** - action_sha must be a valid git commit hash (40 hex chars) -** - YAML must be valid (checked at runtime) -*) -datatype workflow_update_op( - file:string, action:string, sha:string -) = - | WorkflowUpdate(file, action, sha) of ( - existing_path(file), (* Workflow file exists *) - nonempty_string(action), (* Action name *) - nonempty_string(sha), (* Valid SHA *) - backup_policy, (* Backup strategy *) - operation_mode (* Execution mode *) - ) - -(* -** Custom Operation -** Executes operation from template file -** -** Invariants: -** - template_path must exist -** - template must be valid TOML (checked at runtime) -*) -datatype custom_op( - template:string -) = - | CustomOp(template) of ( - existing_path(template), (* Template exists *) - List0(@(string, string)), (* Arguments *) - operation_mode (* Execution mode *) - ) - -(* -** Unified operation type -** Tagged union of all operation types -*) -datatype batch_operation = - | OpLicenseUpdate of [old:string, new:string] license_update_op(old, new) - | OpFileReplace of [pat:string, repl:string] file_replace_op(pat, repl) - | OpGitSync of [msg:string] git_sync_op(msg) - | OpWorkflowUpdate of [file:string, action:string, sha:string] - workflow_update_op(file, action, sha) - | OpCustom of [tmpl:string] custom_op(tmpl) - -(* ========== Operation context ========== *) - -typedef operation_context = @{ - targets = repo_target, (* Target repositories *) - dry_run = bool, (* Preview mode *) - parallel_jobs = int, (* Number of parallel workers *) - log_path = string, (* Log file path *) - backup_dir = string (* Backup directory *) -} - -(* ========== Operation result with proofs ========== *) - -typedef batch_result = @{ - success_count = [n:nat] int(n), (* Number of successful operations *) - failure_count = [n:nat] int(n), (* Number of failed operations *) - skipped_count = [n:nat] int(n), (* Number of skipped operations *) - results = List0(operation_result), (* Detailed results *) - rollback_info = Option(string) (* Rollback information if needed *) +staload "./types.sats" +staload "../utils/string_utils.sats" + +assume spdx_id = string +assume nonempty_string = string +assume existing_path = string +assume git_repo = string + +(* ========== SPDX license set ========== *) +(* Common SPDX identifiers; full list at https://spdx.org/licenses/ *) + +fn spdx_list (): List0(string) = + $list{string}( + "PMPL-1.0-or-later", "MIT", "Apache-2.0", + "GPL-3.0-only", "GPL-3.0-or-later", + "LGPL-3.0-only", "LGPL-3.0-or-later", + "BSD-2-Clause", "BSD-3-Clause", "ISC", + "MPL-2.0", "AGPL-3.0-only", "Unlicense", "0BSD" + ) + +implement is_valid_spdx(s) = let + fun mem (xs: List0(string)): bool = + case+ xs of + | list_nil() => false + | list_cons(x, rest) => if x = s then true else mem(rest) +in + if string_is_empty(s) then false else mem(spdx_list()) +end + +(* ========== Smart constructors ========== *) + +implement validate_spdx_id(s) = + if is_valid_spdx(s) then Some(s) else None() + +implement validate_nonempty(s) = + if string_is_nonempty(s) then Some(s) else None() + +(* Filesystem existence is an EFFECT, not a pure proof. We do not pretend +** otherwise: this calls `test -e` via the shell and trusts its exit code. +** The witness only certifies "test -e succeeded at construction time". *) +implement validate_path_exists(p) = let + val cmd = string_append("test -e ", p) + val rc = $extfcall(int, "system", $UNSAFE.strptr2string(cmd)) + val () = strptr_free(cmd) +in + if rc = 0 then Some(p) else None() +end + +implement validate_git_repo(p) = let + val gp = string_append(p, "/.git") + val cmd = string_append("test -d ", $UNSAFE.strptr2string(gp)) + val () = strptr_free(gp) + val rc = $extfcall(int, "system", $UNSAFE.strptr2string(cmd)) + val () = strptr_free(cmd) +in + if rc = 0 then Some(p) else None() +end + +(* ========== Witness projections ========== *) + +implement spdx_unwrap(x) = x +implement nonempty_unwrap(x) = x +implement path_unwrap(x) = x +implement gitrepo_unwrap(x) = x + +(* ========== Result helpers ========== *) + +implement result_message(r) = + case+ r of + | OpSuccess(m) => m + | OpFailure(m) => m + | OpSkipped(m) => m + +implement result_is_ok(r) = + case+ r of + | OpSuccess _ => true + | _ => false + +implement empty_batch(msg) = @{ + success_count = 0, + failure_count = 0, + skipped_count = 0, + message = msg } -(* ========== Validation functions ========== *) - -(* -** Validates that a string is a valid SPDX identifier -** Returns Some(spdx_id) if valid, None otherwise -*) -fun validate_spdx_id(s: string): Option(spdx_id(s)) - -(* -** Validates that a path exists on filesystem -** Returns Some(existing_path) if valid, None otherwise -*) -fun validate_path_exists(p: string): Option(existing_path(p)) - -(* -** Validates that a path is a git repository -** Returns Some(git_repo) if valid, None otherwise -*) -fun validate_git_repo(p: string): Option(git_repo(p)) - -(* -** Validates that a string is non-empty -** Returns Some(nonempty_string) if valid, None otherwise -*) -fun validate_nonempty(s: string): Option(nonempty_string(s)) - -(* ========== Operation constructors with validation ========== *) - -(* -** Creates a license update operation with validation -** Returns None if validation fails -*) -fun make_license_update_op( - old: string, - new: string, - backup: backup_policy, - mode: operation_mode -): Option([old:string, new:string] license_update_op(old, new)) - -(* -** Creates a file replace operation with validation -** Returns None if validation fails -*) -fun make_file_replace_op( - pattern: string, - replacement: string, - backup: backup_policy, - mode: operation_mode -): Option([pat:string, repl:string] file_replace_op(pat, repl)) - -(* -** Creates a git sync operation with validation -** Returns None if validation fails -*) -fun make_git_sync_op( - msg: string, - parallel: int, - depth: int, - mode: operation_mode -): Option([msg:string] git_sync_op(msg)) - -(* ========== Operation execution ========== *) - -(* -** Executes a batch operation across target repositories -** Returns batch_result with detailed success/failure information -** -** Proof obligations: -** - If mode is DryRun, no filesystem changes are made -** - If backup is required, backups are created before any changes -** - Operation is atomic per repository (all changes or none) -*) -fun execute_batch_operation( - op: batch_operation, - ctx: operation_context -): batch_result - -(* -** Rolls back a batch operation using rollback information -** Returns true if rollback succeeded, false otherwise -*) -fun rollback_batch_operation( - rollback_info: string -): bool +implement batch_add(acc, r) = + case+ r of + | OpSuccess _ => @{ + success_count = acc.success_count + 1, + failure_count = acc.failure_count, + skipped_count = acc.skipped_count, + message = acc.message } + | OpFailure _ => @{ + success_count = acc.success_count, + failure_count = acc.failure_count + 1, + skipped_count = acc.skipped_count, + message = acc.message } + | OpSkipped _ => @{ + success_count = acc.success_count, + failure_count = acc.failure_count, + skipped_count = acc.skipped_count + 1, + message = acc.message } diff --git a/scaffoldia/repo-batcher/src/ats2/operations/types.sats b/scaffoldia/repo-batcher/src/ats2/operations/types.sats new file mode 100644 index 0000000..014b8a7 --- /dev/null +++ b/scaffoldia/repo-batcher/src/ats2/operations/types.sats @@ -0,0 +1,85 @@ +(* +** SPDX-License-Identifier: PMPL-1.0-or-later +** +** Operation type definitions - INTERFACE (real Postiats 0.4.2) +** +** HONESTY NOTE ON THE "PROOF" TYPES +** --------------------------------- +** The prior fictional version declared types indexed by a *string value* +** (e.g. `spdx_id(s:string)`). Postiats `string(n)` is indexed by LENGTH +** (an int sort); there is no `string` index sort, so a value-indexed +** dependent witness is NOT expressible in real Postiats 0.4.2 and was +** never sound. +** +** What IS soundly established here: each witness is an `abstype` whose +** representation is hidden. The ONLY way to obtain one is via the +** corresponding `validate_*` smart constructor, which performs the runtime +** check and returns `None` on failure. So possession of an `spdx_id` +** value is a machine-enforced certificate that "this string passed +** is_valid_spdx at construction time" — a constructor-controlled +** invariant, not a dependent-type theorem. We do not claim more. +*) + +(* ========== Validated-string witnesses (opaque) ========== *) + +abstype spdx_id = string (* constructed only by validate_spdx_id *) +abstype nonempty_string = string (* constructed only by validate_nonempty *) +abstype existing_path = string (* constructed only by validate_path_exists*) +abstype git_repo = string (* constructed only by validate_git_repo *) + +(* ========== Repository target ========== *) + +datatype repo_target = + | RepoList of List0(string) + | RepoFile of string + | RepoPattern of string + | RepoDirectory of string + +(* ========== Operation result ========== *) + +datatype operation_result = + | OpSuccess of string + | OpFailure of string + | OpSkipped of string + +datatype backup_policy = + | NoBackup + | RequireBackup of string + | AutoBackup + +datatype operation_mode = + | DryRun + | Execute + | Interactive + +(* ========== C-marshallable batch result ========== *) +(* Plain ints (no dependent refinement claimed) so it crosses the C ABI. *) + +typedef batch_result = @{ + success_count = int, + failure_count = int, + skipped_count = int, + message = string +} + +(* ========== Smart constructors / validators ========== *) + +fun is_valid_spdx (s: string): bool + +fun validate_spdx_id (s: string): Option(spdx_id) +fun validate_nonempty (s: string): Option(nonempty_string) +fun validate_path_exists(p: string): Option(existing_path) +fun validate_git_repo (p: string): Option(git_repo) + +(* Witness projections (safe: the abstype was checked at construction). *) +fun spdx_unwrap (x: spdx_id): string +fun nonempty_unwrap (x: nonempty_string): string +fun path_unwrap (x: existing_path): string +fun gitrepo_unwrap (x: git_repo): string + +(* ========== Result helpers ========== *) + +fun result_message (r: operation_result): string +fun result_is_ok (r: operation_result): bool +fun empty_batch (msg: string): batch_result +fun batch_add (acc: batch_result, r: operation_result): batch_result From c1ba3941c6f99f147cc80c0cfa3e5559a315d972 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 18 May 2026 18:31:42 +0100 Subject: [PATCH 03/10] fix(repo-batcher): canonical cross-module ATS2 build + Layer-3 SPDX real FIX-FIRST: Layer-2 cross-module regression. operations/types.dats used `staload "../utils/string_utils.sats"` which only resolves when CWD is the operations/ dir; PR #59's isolated per-file proof masked it. Changed to root-relative `staload "utils/string_utils.sats"` and established ONE canonical invocation (CWD=src/ats2, `-IATS .`) driven by the Justfile (`just tc-core`/`tc-ats2`). Re-verified L1+L2 under it. Added operations/effects.{sats,dats}: honest external-effects layer (system(3) via $extfcall, conservative status==0 success test, fs predicates) modelling git/gh/fs as effects, not fake purity. Rewrote validation/spdx as real Postiats with a .sats interface (spdx_wellformed/spdx_acceptable/comment_prefix_for_ext/make_spdx_header); prior version was fiction (@[...]:List0, staload of a .dats, + on strings). Root-caused two real Postiats 0.4.2 facts by minimal bisection and documented them in-source: 1. `prefix` is a reserved keyword (fixity decls); using it as an identifier is a hard parse error. Also infix/infixl/infixr/postfix. 2. ATS2 block comments nest, so a literal open/close-comment digraph in a string literal or prose opens/closes a comment. The ATS-family comment prefix is therefore assembled from char codes. Verification (exit code captured as the last command, not via a pipe): just tc-core -> EXIT=0 runs, CWD=src/ats2, -IATS .: patsopt -tc -s utils/string_utils.sats -d utils/string_utils.dats patsopt -tc -s operations/types.sats -d operations/types.dats patsopt -tc -s operations/effects.sats -d operations/effects.dats patsopt -tc -s validation/spdx.sats -d validation/spdx.dats Co-Authored-By: Claude Opus 4.7 (1M context) --- scaffoldia/repo-batcher/Justfile | 189 +++++++++-------- .../src/ats2/operations/effects.dats | 67 ++++++ .../src/ats2/operations/effects.sats | 47 +++++ .../src/ats2/operations/types.dats | 11 +- .../src/ats2/validation/spdx.dats | 191 ++++++++---------- .../src/ats2/validation/spdx.sats | 47 +++++ 6 files changed, 348 insertions(+), 204 deletions(-) create mode 100644 scaffoldia/repo-batcher/src/ats2/operations/effects.dats create mode 100644 scaffoldia/repo-batcher/src/ats2/operations/effects.sats create mode 100644 scaffoldia/repo-batcher/src/ats2/validation/spdx.sats diff --git a/scaffoldia/repo-batcher/Justfile b/scaffoldia/repo-batcher/Justfile index 6c76bcd..4da2fea 100644 --- a/scaffoldia/repo-batcher/Justfile +++ b/scaffoldia/repo-batcher/Justfile @@ -1,96 +1,109 @@ # SPDX-License-Identifier: PMPL-1.0-or-later # justfile for repo-batcher +# +# CANONICAL ATS2 BUILD CONVENTION +# ------------------------------- +# Every ATS2 module is typechecked/compiled with CWD = src/ats2 and the +# single include flag `-IATS .` so that ROOT-RELATIVE staload paths +# (e.g. `staload "utils/string_utils.sats"`) resolve regardless of the +# compiler's working directory. Per-file isolated typechecking with +# `../`-relative staloads is FORBIDDEN: it silently masked a real +# cross-module regression (PR #59). All proofs use the recipes below, +# which exercise the real cross-module invocation. Module list is +# EXPLICIT (never a wildcard) so scratch/probe files cannot enter a +# build. + +ats2_root := justfile_directory() / "src/ats2" +build_dir := justfile_directory() / "build" + +# Modules in dependency order (sats checked with its dats). +# layer1: utils/string_utils layer2: operations/types +# effects: operations/effects layer3: validation/spdx +# layer4: operations/ layer5: ffi/c_exports -# Default recipe default: @just --list -# Build the project -build: - @echo "Building repo-batcher..." - # Compile ATS2 core - cd src/ats2 && patscc -o ../../build/librepobatcher.a operations/*.dats - # Build Zig FFI layer - cd ffi/zig && zig build -Doptimize=ReleaseSafe - @echo "Build complete" - -# Build in development mode (faster, less optimized) -build-dev: - @echo "Building repo-batcher (dev mode)..." - cd ffi/zig && zig build - @echo "Build complete" - -# Run smoke test (structure validation, no build required) -test-smoke: - @echo "Running smoke test..." - ./tests/smoke_test.sh - -# Run tests -test: - @echo "Running tests..." - cd ffi/zig && zig build test && zig build test-integration - @echo "" - @echo "All tests passed!" - -# Run real repository tests (dry-run only) -test-real: - @echo "Running real repository tests (dry-run)..." - ./tests/real_repo_test.sh - -# Run performance benchmark -benchmark: - @echo "Running performance benchmark..." - ./benchmark/performance_test.sh - -# Clean build artifacts +# ---- Layer-by-layer cross-module typecheck (the canonical proof) ---- + +# L1 + L2 + effects + L3: the verified core. +tc-core: + cd {{ats2_root}} && patsopt -tc -s utils/string_utils.sats -d utils/string_utils.dats -IATS . + cd {{ats2_root}} && patsopt -tc -s operations/types.sats -d operations/types.dats -IATS . + cd {{ats2_root}} && patsopt -tc -s operations/effects.sats -d operations/effects.dats -IATS . + cd {{ats2_root}} && patsopt -tc -s validation/spdx.sats -d validation/spdx.dats -IATS . + @echo "tc-core: ATS2 core typechecks (cross-module, -IATS .)" + +# L4: each operation module typechecks against its .sats. +tc-operations: tc-core + cd {{ats2_root}} && patsopt -tc -s operations/file_replace.sats -d operations/file_replace.dats -IATS . + cd {{ats2_root}} && patsopt -tc -s operations/git_sync.sats -d operations/git_sync.dats -IATS . + cd {{ats2_root}} && patsopt -tc -s operations/github_settings.sats -d operations/github_settings.dats -IATS . + cd {{ats2_root}} && patsopt -tc -s operations/license_update.sats -d operations/license_update.dats -IATS . + cd {{ats2_root}} && patsopt -tc -s operations/spdx_audit.sats -d operations/spdx_audit.dats -IATS . + cd {{ats2_root}} && patsopt -tc -s operations/workflow_update.sats -d operations/workflow_update.dats -IATS . + @echo "tc-operations: all Layer-4 operation modules typecheck" + +# L5: the C-export surface typechecks. +tc-ffi: tc-operations + cd {{ats2_root}} && patsopt -tc -d ffi/c_exports.dats -IATS . + @echo "tc-ffi: Layer-5 C-export surface typechecks" + +# Full ATS2 proof. +tc-ats2: tc-ffi + @echo "tc-ats2: full ATS2 stack typechecks under canonical invocation" + +# ---- Compilation to a C archive (Layer 5 link surface) ---- + +# Compile every ATS2 module to .o then bundle a static archive. +ats2-lib: tc-ffi + mkdir -p {{build_dir}} + cd {{ats2_root}} && patscc -DATS_MEMALLOC_LIBC -IATS . -c \ + utils/string_utils.dats operations/types.dats \ + operations/effects.dats validation/spdx.dats \ + operations/file_replace.dats operations/git_sync.dats \ + operations/github_settings.dats operations/license_update.dats \ + operations/spdx_audit.dats operations/workflow_update.dats \ + ffi/c_exports.dats + cd {{ats2_root}} && ar rcs {{build_dir}}/librepobatcher.a *_dats.o + @echo "ats2-lib: {{build_dir}}/librepobatcher.a built" + +# ---- Idris2 ABI (Layer 6) ---- + +abi-check: + cd {{justfile_directory()}}/src/abi && \ + {{justfile_directory()}}/../../../dev/tools/provers/idris2/0.8.0/bin/idris2 --check Abi.idr + @echo "abi-check: Idris2 ABI contract typechecks" + +# ---- Zig CLI (Layer 7) ---- + +zig-build: ats2-lib + cd {{justfile_directory()}}/ffi/zig && zig build + +zig-test: ats2-lib + cd {{justfile_directory()}}/ffi/zig && zig build test + +# ---- Layer 8: end-to-end ---- + +# Build ATS2 lib -> build Zig CLI -> run the real binary smoke test. +e2e: ats2-lib + cd {{justfile_directory()}}/ffi/zig && zig build + {{justfile_directory()}}/ffi/zig/zig-out/bin/repo-batcher --version + {{justfile_directory()}}/ffi/zig/zig-out/bin/repo-batcher validate-spdx MIT + @echo "e2e: real binary ran (version + spdx validation smoke)" + +# Aggregate build. +build: ats2-lib zig-build + @echo "build: ATS2 archive + Zig CLI built" + clean: - rm -rf build/ - find . -name "*.o" -delete - find . -name "*.a" -delete - find . -name "*.so" -delete - -# Install to system -install: - @echo "Installing repo-batcher..." - sudo cp build/repo-batcher /usr/local/bin/ - sudo chmod +x /usr/local/bin/repo-batcher - mkdir -p ~/.config/repo-batcher/watch - mkdir -p ~/.local/share/repo-batcher/logs - mkdir -p ~/.local/share/repo-batcher/backups - @echo "Installed to /usr/local/bin/repo-batcher" - -# Uninstall from system -uninstall: - sudo rm -f /usr/local/bin/repo-batcher - @echo "Uninstalled repo-batcher" - -# Format code + rm -rf {{build_dir}} + find {{ats2_root}} -name "*_dats.o" -delete + find {{ats2_root}} -name "*.c" -path "*_dats.c" -delete + rm -rf {{justfile_directory()}}/ffi/zig/zig-out {{justfile_directory()}}/ffi/zig/.zig-cache + +# Backward-compatible check recipe (now the real cross-module proof). +check: tc-ats2 + fmt: - zig fmt ffi/zig/src/ ffi/zig/test/ - -# Check code quality -check: - @echo "Checking ATS2 code..." - patsopt -tc -d src/ats2/operations/*.dats - -# Create example config -setup-config: - mkdir -p ~/.config/repo-batcher - cp templates/config.example.toml ~/.config/repo-batcher/config.toml - @echo "Config created at ~/.config/repo-batcher/config.toml" - -# Run in dry-run mode (safe testing) -dry-run operation targets: - ./build/repo-batcher {{operation}} --targets {{targets}} --dry-run - -# Quick git-sync (ported from sync_repos.sh) -git-sync parallel="4" depth="2": - ./build/repo-batcher git-sync --parallel {{parallel}} --depth {{depth}} - -# Watch mode (daemon) -watch: - ./build/repo-batcher watch - -# Show version and help -help: - ./build/repo-batcher --help + zig fmt {{justfile_directory()}}/ffi/zig/src/ {{justfile_directory()}}/ffi/zig/test/ diff --git a/scaffoldia/repo-batcher/src/ats2/operations/effects.dats b/scaffoldia/repo-batcher/src/ats2/operations/effects.dats new file mode 100644 index 0000000..a0387f9 --- /dev/null +++ b/scaffoldia/repo-batcher/src/ats2/operations/effects.dats @@ -0,0 +1,67 @@ +(* +** SPDX-License-Identifier: PMPL-1.0-or-later +** +** External-effects implementation (real Postiats 0.4.2) +** +** CANONICAL BUILD: from src/ats2 with `-IATS .`. +** sys_run delegates to libc system(3) via $extfcall. The WEXITSTATUS +** decode is the POSIX bit layout ((status >> 8) & 0xFF) computed with +** ATS2 integer ops; we do not link macros (not portable +** through $extfcall), we implement the documented decode directly. +*) + +#include "share/atspre_define.hats" +#include "share/atspre_staload.hats" + +staload "operations/types.sats" +staload "operations/effects.sats" + +implement sys_run (cmd) = + $extfcall(int, "system", cmd) + +(* POSIX: a normal child exit makes system()'s status word == 0 exactly +** when the exit code is 0 and no signal terminated the child (the low +** byte holds the signal/core info, byte 1 holds the exit code). So a +** clean "command succeeded" is precisely status == 0. system() returns +** -1 on fork/exec failure. We deliberately use the conservative +** status==0 test (computed with plain int arithmetic, no unsigned +** bitops) rather than reimplementing WEXITSTATUS bit-twiddling, which +** is documented here as an intentional simplification, not an omission. *) +implement wexit_ok (status) = + if status < 0 then false else status = 0 + +implement path_exists (p) = let + val cmd = string_append("test -e ", p) + val rc = sys_run($UNSAFE.strptr2string(cmd)) + val () = strptr_free(cmd) +in + wexit_ok(rc) +end + +implement dir_exists (p) = let + val cmd = string_append("test -d ", p) + val rc = sys_run($UNSAFE.strptr2string(cmd)) + val () = strptr_free(cmd) +in + wexit_ok(rc) +end + +implement is_git_repo (p) = let + val gp = string_append(p, "/.git") + val cmd = string_append("test -e ", $UNSAFE.strptr2string(gp)) + val () = strptr_free(gp) + val rc = sys_run($UNSAFE.strptr2string(cmd)) + val () = strptr_free(cmd) +in + wexit_ok(rc) +end + +(* ok_msg / fail_msg are caller-owned shared `string`s (typically string +** literals) stored directly in the result datatype; no allocation here, +** so no ownership/free question arises. dry_run is reported via the +** distinct OpSkipped constructor rather than a prefixed message, which +** keeps this allocation-free and the dry-run signal machine-readable. *) +implement effect_result (dry_run, ok, ok_msg, fail_msg) = + if dry_run then OpSkipped(ok_msg) + else if ok then OpSuccess(ok_msg) + else OpFailure(fail_msg) diff --git a/scaffoldia/repo-batcher/src/ats2/operations/effects.sats b/scaffoldia/repo-batcher/src/ats2/operations/effects.sats new file mode 100644 index 0000000..8a2e65e --- /dev/null +++ b/scaffoldia/repo-batcher/src/ats2/operations/effects.sats @@ -0,0 +1,47 @@ +(* +** SPDX-License-Identifier: PMPL-1.0-or-later +** +** External-effects interface (real Postiats 0.4.2) +** +** HONESTY NOTE +** ------------ +** Every function here is an EFFECT, not a pure proof. The repo-batcher +** drives git/gh/filesystem mutations that cannot be modelled as total +** pure functions. We do not pretend otherwise: each effect is declared +** as an opaque action whose only guarantee is "the underlying C call +** ran and we report its exit/return faithfully". The ATS2 type system +** here buys us: +** - exhaustive handling of the three-way operation_result outcome, +** - explicit ownership of every allocated string (Strptr1, freed once), +** - no implicit GC and no value-indexed dependent fiction. +** It does NOT buy us a proof that git did the right thing; that is +** delegated honestly to the external process and its exit code. +** +** All shell strings are built with `string_append` (Layer-1 idiom) and +** freed via `strptr_free` exactly once by the caller of the builder. +*) + +staload "operations/types.sats" + +(* ---- Raw process effect (documented extern C) ---- *) + +(* Runs `cmd` via libc system(3). Returns the raw status word; callers +** normalise with `wexit_ok`. This is the ONLY shell entry point. *) +fun sys_run (cmd: string): int + +(* True iff a system(3) status word denotes child exit code 0. *) +fun wexit_ok (status: int): bool + +(* ---- Filesystem predicates (effectful, trust the OS) ---- *) + +fun path_exists (p: string): bool +fun dir_exists (p: string): bool +fun is_git_repo (p: string): bool + +(* ---- Outcome smart helpers ---- *) + +(* Map a normalised shell success/failure to an operation_result with a +** caller-supplied human message. dry_run short-circuits to OpSkipped. *) +fun effect_result + (dry_run: bool, ok: bool, ok_msg: string, fail_msg: string) + : operation_result diff --git a/scaffoldia/repo-batcher/src/ats2/operations/types.dats b/scaffoldia/repo-batcher/src/ats2/operations/types.dats index a1f3be2..c0f6646 100644 --- a/scaffoldia/repo-batcher/src/ats2/operations/types.dats +++ b/scaffoldia/repo-batcher/src/ats2/operations/types.dats @@ -3,16 +3,17 @@ ** ** Operation type definitions - IMPLEMENTATION (real Postiats 0.4.2) ** -** Verified: `patsopt -tc -s operations/types.sats -d operations/types.dats` -** plus the string_utils dependency (-IATS ../). Witness abstypes are -** `assume`d equal to `string`; the only constructors are the validators. +** CANONICAL BUILD: invoked from src/ats2 root via the Justfile with +** `-IATS .` so that root-relative staload paths resolve regardless of +** the compiler's CWD. Witness abstypes are `assume`d equal to `string`; +** the only constructors are the validators. *) #include "share/atspre_define.hats" #include "share/atspre_staload.hats" -staload "./types.sats" -staload "../utils/string_utils.sats" +staload "operations/types.sats" +staload "utils/string_utils.sats" assume spdx_id = string assume nonempty_string = string diff --git a/scaffoldia/repo-batcher/src/ats2/validation/spdx.dats b/scaffoldia/repo-batcher/src/ats2/validation/spdx.dats index b02c045..4da1d78 100644 --- a/scaffoldia/repo-batcher/src/ats2/validation/spdx.dats +++ b/scaffoldia/repo-batcher/src/ats2/validation/spdx.dats @@ -1,133 +1,102 @@ (* ** SPDX-License-Identifier: PMPL-1.0-or-later ** -** SPDX license identifier validation -** Validates license identifiers against SPDX specification +** SPDX license-identifier validation - IMPLEMENTATION (real Postiats 0.4.2) +** +** CANONICAL BUILD: from src/ats2 with `-IATS .`. +** Reuses Layer-1 string idioms (length-indexed string(n), proven +** indexing) and Layer-2 is_valid_spdx. No `+` string operator (that is +** not valid ATS2; all concatenation is string_append -> Strptr1). *) #include "share/atspre_define.hats" #include "share/atspre_staload.hats" -staload "../operations/types.dats" +staload "operations/types.sats" +staload "utils/string_utils.sats" +staload "validation/spdx.sats" -(* ========== SPDX License List ========== *) +(* Local: a 1-char {c,'\000'} buffer borrowed as string then owned-copied. +** Same documented-unsafe idiom as utils/string_utils.dats:char_to_str +** (re-declared locally because that one is a private fn, not exported). *) +fn char_to_str (c: char): Strptr1 = let + val cs = $UNSAFE.cast{string}(@[char][2](c, '\000')) +in + string0_copy(cs) +end -(* -** Common SPDX license identifiers -** Full list: https://spdx.org/licenses/ -*) -val common_spdx_licenses = @[ - "PMPL-1.0-or-later", - "MIT", - "Apache-2.0", - "GPL-3.0-only", - "GPL-3.0-or-later", - "LGPL-3.0-only", - "LGPL-3.0-or-later", - "BSD-2-Clause", - "BSD-3-Clause", - "ISC", - "MPL-2.0", - "AGPL-3.0-only", - "PMPL-1.0-or-later", - "Unlicense", - "0BSD" -] : List0(string) +(* SPDX short-form id character class: A-Z a-z 0-9 . + - *) +fn is_spdx_char (c: char): bool = + (c >= 'A' andalso c <= 'Z') orelse + (c >= 'a' andalso c <= 'z') orelse + (c >= '0' andalso c <= '9') orelse + c = '.' orelse c = '+' orelse c = '-' -(* -** Validates if a string is a valid SPDX identifier -** Returns true if valid, false otherwise -*) -fun is_valid_spdx(s: string): bool = let - fun check_list(licenses: List0(string)): bool = - case+ licenses of - | list_nil() => false - | list_cons(lic, rest) => - if s = lic then true - else check_list(rest) +implement spdx_wellformed (s0) = let + val s = g1ofg0(s0) + val n = string_length(s) + fun loop {sl:int} {i:nat | i <= sl} .. + (s: string(sl), i: size_t(i), sl: size_t(sl)): bool = + if i >= sl then true + else if is_spdx_char(s[i]) then loop(s, succ(i), sl) + else false in - if string_is_empty(s) then false - else check_list(common_spdx_licenses) + if sz2i(n) = 0 then false else loop(s, i2sz(0), n) end -(* -** Validates SPDX identifier and returns proof type -** Returns Some(spdx_id) if valid, None otherwise -*) -implement validate_spdx_id(s) = - if is_valid_spdx(s) then Some(s) - else None() +implement spdx_acceptable (s) = + if is_valid_spdx(s) then true else spdx_wellformed(s) -(* -** Extracts SPDX identifier from header line -** Format: "// SPDX-License-Identifier: MIT" -** Returns extracted license or empty string -*) -fun extract_spdx_from_header(line: string): string = let - val prefix = "SPDX-License-Identifier:" - val idx = string_index_of(line, prefix) +(* ATS2 has no string-literal patterns; dispatch by `=` on `string`. +** The ATS-family prefix is assembled char-wise (lp then star) so the +** source never contains the literal ATS open-comment digraph (see the +** spdx.sats note: Postiats 0.4.2 block comments nest, so that digraph +** even inside a string literal opens a comment). All arms yield a +** fresh Strptr1; string0_copy on the static arms keeps one uniform +** ownership story (caller frees exactly once). *) +implement comment_prefix_for_ext(ext) = let + (* ASCII 40 = open paren, 42 = star; built from codes so neither the + ** char literal for '(' nor the open-comment digraph appears in source. *) + val lp = char_to_str(int2char0(40)) + val sp = char_to_str(int2char0(42)) + val st = string_append($UNSAFE.strptr2string(lp), + $UNSAFE.strptr2string(sp)) + val () = strptr_free(lp) + val () = strptr_free(sp) in - if idx >= 0 then let - val start = idx + string_length(prefix) - val rest = string_suffix(line, start) - val trimmed = string_trim(rest) + if ext = ".dats" then st + else if ext = ".sats" then st + else if ext = ".hats" then st + else let + val () = strptr_free(st) in - trimmed + if ext = ".rs" then string0_copy("//") + else if ext = ".zig" then string0_copy("//") + else if ext = ".idr" then string0_copy("--") + else if ext = ".scm" then string0_copy(";;") + else if ext = ".toml" then string0_copy("#") + else if ext = ".yml" then string0_copy("#") + else if ext = ".yaml" then string0_copy("#") + else if ext = ".sh" then string0_copy("#") + else if ext = ".just" then string0_copy("#") + else if ext = ".md" then string0_copy("