coop/rose-ash
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

artdag: Phase 7 non-vacuous confluence gate regression + 2 tests

Browse Source 
Assert mau/confluent? actually discriminates: the Peano-arithmetic variant of the
optimisation laws is flagged non-confluent with named non-joinable pairs, so the green
'opt module is confluent' is real evidence rather than a rubber stamp. maude-optimize
40/40, total 198/198.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
giles
2026-06-19 13:58:39 +00:00
parent d7bb3303f8
commit 4a02a9c400
4 changed files with 55 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
lib/artdag/scoreboard.json
View File

@@ -10,9 +10,9 @@
"serialize": {"pass": 13, "fail": 0},
"stats": {"pass": 12, "fail": 0},
"fault": {"pass": 14, "fail": 0},
"maude-optimize": {"pass": 38, "fail": 0}
"maude-optimize": {"pass": 40, "fail": 0}
},
"total_pass": 196,
"total_pass": 198,
"total_fail": 0,
"total": 196
"total": 198
}

4
lib/artdag/scoreboard.md
View File

@@ -14,5 +14,5 @@ _Generated by `lib/artdag/conformance.sh`_
| serialize | 13 | 0 | 13 |
| stats | 12 | 0 | 12 |
| fault | 14 | 0 | 14 |
| maude-optimize | 38 | 0 | 38 |
| **Total** | **196** | **0** | **196** |
| maude-optimize | 40 | 0 | 40 |
| **Total** | **198** | **0** | **198** |

42
lib/artdag/tests/maude-optimize.sx
View File

@@ -301,3 +301,45 @@
"opt-cheaper?: untouched DAG keeps equal cost (never a pessimisation)"
(artdag/opt-cheaper? mo-plain mo-plain-id artdag/const-cost)
true)
; ---- the confluence gate is meaningful, not vacuous ----
; the Peano-arithmetic variant of the same laws is KNOWN non-confluent (M+0 sticks,
; (A+B)+C vs A+(B+C) don't join). Assert the checker actually catches it, so the
; green "opt module is confluent" above is real evidence, not a checker that passes
; everything.
(define
mo-peano-module
(mau/parse-module
(str
"fmod ARTDAGPEANO is\n"
" sorts Img Num .\n"
" op src : -> Img .\n"
" op 0 : -> Num .\n"
" op s_ : Num -> Num .\n"
" op _+_ : Num Num -> Num .\n"
" op blur : Img Num -> Img .\n"
" op bright : Img Num -> Img .\n"
" op id : Img -> Img .\n"
" op over : Img Img -> Img [comm] .\n"
" vars I J : Img .\n"
" vars M N : Num .\n"
" eq 0 + N = N .\n"
" eq s M + N = s (M + N) .\n"
" eq id(I) = I .\n"
" eq blur(I, 0) = I .\n"
" eq bright(I, 0) = I .\n"
" eq blur(blur(I, M), N) = blur(I, M + N) .\n"
" eq bright(bright(I, M), N) = bright(I, M + N) .\n"
" eq over(I, I) = I .\n"
"endfm")))
(artdag-test
"confluence gate is real: Peano variant is flagged non-confluent"
(mau/confluent? mo-peano-module)
false)
(artdag-test
"confluence gate is real: Peano variant names its non-joinable pairs"
(> (len (mau/non-joinable-pairs mo-peano-module)) 0)
true)