giles
4a02a9c400
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>
346 lines
9.9 KiB
Plaintext
346 lines
9.9 KiB
Plaintext
; Phase 7 — rule-based optimization via maude-on-sx.
|
|
; Bridge round-trip: dag->term->dag is the identity on canonical (content-id) form.
|
|
|
|
; ---- linear chain a -> b -> c (b carries params) ----
|
|
|
|
(define
|
|
mo-chain
|
|
(artdag/build
|
|
(list
|
|
(list "a" "in" (list) {:v 5})
|
|
(list "b" "blur" (list "a") {:radius 2})
|
|
(list "c" "blur" (list "b") {:radius 3}))))
|
|
(define mo-c-id (artdag/dag-id mo-chain "c"))
|
|
(define mo-chain-rt (artdag/mb-roundtrip mo-chain mo-c-id))
|
|
|
|
(artdag-test
|
|
"roundtrip: sink id preserved"
|
|
(artdag/member? mo-c-id (keys (artdag/dag-nodes mo-chain-rt)))
|
|
true)
|
|
|
|
(artdag-test
|
|
"roundtrip: node count preserved"
|
|
(artdag/node-count mo-chain-rt)
|
|
3)
|
|
|
|
(artdag-test
|
|
"roundtrip: sink op preserved"
|
|
(artdag/node-op (artdag/dag-get mo-chain-rt mo-c-id))
|
|
"blur")
|
|
|
|
(artdag-test
|
|
"roundtrip: sink params preserved"
|
|
(artdag/node-params (artdag/dag-get mo-chain-rt mo-c-id))
|
|
{:radius 3})
|
|
|
|
(artdag-test
|
|
"roundtrip: full reconstructed node equals original"
|
|
(= (artdag/dag-get mo-chain-rt mo-c-id) (artdag/dag-get mo-chain mo-c-id))
|
|
true)
|
|
|
|
; ---- term shape ----
|
|
|
|
(define mo-c-term (artdag/dag->term mo-chain mo-c-id))
|
|
|
|
(artdag-test "term: sink op is the maude operator" (mau/op mo-c-term) "blur")
|
|
|
|
(artdag-test
|
|
"term: params recovered from meta"
|
|
(artdag/term-params mo-c-term)
|
|
{:radius 3})
|
|
|
|
(artdag-test
|
|
"term: commutative flag recovered (false)"
|
|
(artdag/term-commutative mo-c-term)
|
|
false)
|
|
|
|
(artdag-test
|
|
"term->entries: one entry per node"
|
|
(len (artdag/term->entries mo-c-term))
|
|
3)
|
|
|
|
; ---- commutative node: order-insensitive id survives round-trip ----
|
|
|
|
(define
|
|
mo-comm
|
|
(artdag/build
|
|
(list
|
|
(list "x" "src" (list) {})
|
|
(list "y" "noise" (list) {})
|
|
(list "z" "over" (list "x" "y") {} true))))
|
|
(define mo-z-id (artdag/dag-id mo-comm "z"))
|
|
(define mo-comm-rt (artdag/mb-roundtrip mo-comm mo-z-id))
|
|
|
|
(artdag-test
|
|
"roundtrip comm: commutative id preserved"
|
|
(artdag/member? mo-z-id (keys (artdag/dag-nodes mo-comm-rt)))
|
|
true)
|
|
|
|
(artdag-test
|
|
"term comm: commutative flag recovered (true)"
|
|
(artdag/term-commutative (artdag/dag->term mo-comm mo-z-id))
|
|
true)
|
|
|
|
; ---- diamond: shared subgraph re-collapses to one node ----
|
|
|
|
(define
|
|
mo-diamond
|
|
(artdag/build
|
|
(list
|
|
(list "a" "src" (list) {})
|
|
(list "b" "blur" (list "a") {:radius 1})
|
|
(list "c" "bright" (list "a") {:gain 2})
|
|
(list "d" "over" (list "b" "c") {} true))))
|
|
(define mo-d-id (artdag/dag-id mo-diamond "d"))
|
|
(define mo-diamond-rt (artdag/mb-roundtrip mo-diamond mo-d-id))
|
|
|
|
(artdag-test
|
|
"roundtrip diamond: shared node not duplicated"
|
|
(artdag/node-count mo-diamond-rt)
|
|
4)
|
|
|
|
(artdag-test
|
|
"roundtrip diamond: sink id preserved"
|
|
(artdag/member? mo-d-id (keys (artdag/dag-nodes mo-diamond-rt)))
|
|
true)
|
|
|
|
(artdag-test
|
|
"roundtrip diamond: shared src id preserved"
|
|
(artdag/member?
|
|
(artdag/dag-id mo-diamond "a")
|
|
(keys (artdag/dag-nodes mo-diamond-rt)))
|
|
true)
|
|
|
|
; ---- optimisation laws as a confluent maude module (optimize-rules.sx) ----
|
|
; The optimised pipeline is the normal form; confluence => stable content id.
|
|
|
|
(artdag-test "opt module is confluent" (artdag/opt-confluent?) true)
|
|
|
|
(artdag-test
|
|
"opt module has no non-joinable critical pairs"
|
|
(len (artdag/opt-non-joinable))
|
|
0)
|
|
|
|
(artdag-test
|
|
"law: identity elimination"
|
|
(artdag/opt-normal-form "id(src)")
|
|
"src")
|
|
|
|
(artdag-test
|
|
"law: zero-radius blur is a no-op"
|
|
(artdag/opt-normal-form "blur(src, 0)")
|
|
"src")
|
|
|
|
(artdag-test
|
|
"law: zero-radius bright is a no-op"
|
|
(artdag/opt-normal-form "bright(src, 0)")
|
|
"src")
|
|
|
|
(artdag-test
|
|
"law: adjacent blur fusion adds radii"
|
|
(artdag/opt-normal-form "blur(blur(src, 1), 1)")
|
|
"blur(src, _+_(1, 1))")
|
|
|
|
(artdag-test
|
|
"fusion normal form is rewrite-order stable"
|
|
(artdag/opt-same-form?
|
|
"blur(blur(blur(src, 1), 1), 1)"
|
|
"blur(blur(src, 1 + 1), 1)")
|
|
true)
|
|
|
|
(artdag-test
|
|
"laws compose: id + no-op + fusion"
|
|
(artdag/opt-normal-form "bright(id(blur(blur(src, 1), 1)), 0)")
|
|
"blur(src, _+_(1, 1))")
|
|
|
|
(artdag-test
|
|
"law: idempotent over dedup (CSE)"
|
|
(artdag/opt-normal-form "over(blur(src, 1), blur(src, 1))")
|
|
"blur(src, 1)")
|
|
|
|
(artdag-test
|
|
"distinct over operands do not dedup"
|
|
(artdag/opt-same-form? "over(blur(src, 1), blur(src, 1 + 1))" "blur(src, 1)")
|
|
false)
|
|
|
|
(artdag-test
|
|
"distinct pipelines stay distinct"
|
|
(artdag/opt-same-form? "blur(src, 1)" "bright(src, 1)")
|
|
false)
|
|
|
|
; ---- bridge the normal form back to a runnable DAG (opt-reduce) ----
|
|
; result-preserving: the maude-optimised DAG executes to the same result as the
|
|
; original, with fewer nodes. Runner is a numeric op model (blur/bright additive in
|
|
; radius, id pass-through, over idempotent) so the pipeline algebra holds concretely.
|
|
|
|
(define
|
|
mo-eq-runner
|
|
(artdag/op-table-runner
|
|
{:src (fn (params inputs) 0)
|
|
:blur (fn (params inputs) (+ (first inputs) (get params :radius)))
|
|
:bright (fn (params inputs) (+ (first inputs) (* 100 (get params :radius))))
|
|
:id (fn (params inputs) (first inputs))
|
|
:over (fn (params inputs) (if (= (nth inputs 0) (nth inputs 1)) (nth inputs 0) (+ (nth inputs 0) (nth inputs 1))))}))
|
|
|
|
(define
|
|
mo-eq-result
|
|
(fn (dag id) (artdag/result-of (artdag/run dag mo-eq-runner (persist/open)) id)))
|
|
|
|
(define
|
|
mo-eq-opt-result
|
|
(fn
|
|
(dag id)
|
|
(let
|
|
((o (artdag/opt-reduce dag id)))
|
|
(artdag/result-of (artdag/run o mo-eq-runner (persist/open)) (artdag/opt-last (artdag/dag-order o))))))
|
|
|
|
; fixture: blur;blur chain + id + zero-radius bright (all collapse to one blur)
|
|
(define
|
|
mo-chain5
|
|
(artdag/build
|
|
(list
|
|
(list "s" "src" (list) {})
|
|
(list "b1" "blur" (list "s") {:radius 1})
|
|
(list "b2" "blur" (list "b1") {:radius 1})
|
|
(list "i" "id" (list "b2") {})
|
|
(list "z" "bright" (list "i") {:radius 0}))))
|
|
(define mo-chain5-id (artdag/dag-id mo-chain5 "z"))
|
|
(define mo-chain5-opt (artdag/opt-reduce mo-chain5 mo-chain5-id))
|
|
(define mo-chain5-sink (artdag/opt-last (artdag/dag-order mo-chain5-opt)))
|
|
|
|
(artdag-test
|
|
"opt-reduce: 5-node chain collapses to 2 nodes"
|
|
(artdag/node-count mo-chain5-opt)
|
|
2)
|
|
|
|
(artdag-test
|
|
"opt-reduce: fused sink op is blur"
|
|
(artdag/node-op (artdag/dag-get mo-chain5-opt mo-chain5-sink))
|
|
"blur")
|
|
|
|
(artdag-test
|
|
"opt-reduce: fused sink radius is the sum"
|
|
(artdag/node-params (artdag/dag-get mo-chain5-opt mo-chain5-sink))
|
|
{:radius 2})
|
|
|
|
(artdag-test
|
|
"opt-reduce: result-preserving on chain"
|
|
(= (mo-eq-result mo-chain5 mo-chain5-id) (mo-eq-opt-result mo-chain5 mo-chain5-id))
|
|
true)
|
|
|
|
; fixture: over of identical subpipelines (idempotent dedup)
|
|
(define
|
|
mo-dedup
|
|
(artdag/build
|
|
(list
|
|
(list "s" "src" (list) {})
|
|
(list "b" "blur" (list "s") {:radius 2})
|
|
(list "o" "over" (list "b" "b") {} true))))
|
|
(define mo-dedup-id (artdag/dag-id mo-dedup "o"))
|
|
|
|
(artdag-test
|
|
"opt-reduce: over dedup collapses to 2 nodes"
|
|
(artdag/node-count (artdag/opt-reduce mo-dedup mo-dedup-id))
|
|
2)
|
|
|
|
(artdag-test
|
|
"opt-reduce: result-preserving on dedup"
|
|
(= (mo-eq-result mo-dedup mo-dedup-id) (mo-eq-opt-result mo-dedup mo-dedup-id))
|
|
true)
|
|
|
|
; non-optimisable DAG: opt-reduce is a faithful round-trip (no laws fire)
|
|
(define
|
|
mo-plain
|
|
(artdag/build
|
|
(list
|
|
(list "s" "src" (list) {})
|
|
(list "b" "blur" (list "s") {:radius 3}))))
|
|
(define mo-plain-id (artdag/dag-id mo-plain "b"))
|
|
(define mo-plain-opt (artdag/opt-reduce mo-plain mo-plain-id))
|
|
|
|
(artdag-test
|
|
"opt-reduce: untouched DAG keeps its node count"
|
|
(artdag/node-count mo-plain-opt)
|
|
2)
|
|
|
|
(artdag-test
|
|
"opt-reduce: untouched DAG keeps its radius (unary round-trip)"
|
|
(artdag/node-params
|
|
(artdag/dag-get mo-plain-opt (artdag/opt-last (artdag/dag-order mo-plain-opt))))
|
|
{:radius 3})
|
|
|
|
; ---- cost-directed: optimisation never increases cost ----
|
|
|
|
(define
|
|
mo-rcost
|
|
(fn (op params) (if (= op "blur") (max 1 (get params :radius)) 1)))
|
|
|
|
(artdag-test
|
|
"opt-improvement: const-cost total work drops on fused chain"
|
|
(let ((imp (artdag/opt-improvement mo-chain5 mo-chain5-id artdag/const-cost)))
|
|
(list (get imp :before) (get imp :after)))
|
|
(list 5 2))
|
|
|
|
(artdag-test
|
|
"opt-improvement: critical path shrinks under const cost"
|
|
(let ((imp (artdag/opt-improvement mo-chain5 mo-chain5-id artdag/const-cost)))
|
|
(< (get imp :after-path) (get imp :before-path)))
|
|
true)
|
|
|
|
(artdag-test
|
|
"opt-cheaper?: fused chain is cheaper under radius-weighted cost"
|
|
(artdag/opt-cheaper? mo-chain5 mo-chain5-id mo-rcost)
|
|
true)
|
|
|
|
(artdag-test
|
|
"opt-cheaper?: over dedup is cheaper"
|
|
(artdag/opt-cheaper? mo-dedup mo-dedup-id artdag/const-cost)
|
|
true)
|
|
|
|
(artdag-test
|
|
"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)
|