diff --git a/docs/Disaggregated/notes/p7/device-window-2/tools/30-gate3.sh b/docs/Disaggregated/notes/p7/device-window-2/tools/30-gate3.sh old mode 100644 new mode 100755 diff --git a/docs/Disaggregated/notes/p7/device-window-2/tools/60-reduce-selftest.py b/docs/Disaggregated/notes/p7/device-window-2/tools/60-reduce-selftest.py index 70a4cafa..5c15a6f4 100644 --- a/docs/Disaggregated/notes/p7/device-window-2/tools/60-reduce-selftest.py +++ b/docs/Disaggregated/notes/p7/device-window-2/tools/60-reduce-selftest.py @@ -33,18 +33,24 @@ says otherwise. The scenarios: NEEDS-ADJUDICATION naming it; one case differing, adjudicated (+ a stale line) -> PASS; one inproc repeat differs from its siblings -> FAIL (within-arm identity) unfinished a pair without .done; a repeat without an actual PNG -> GATE3 INCOMPLETE - monolith-determinism ID-P7-62, on synthetic 8x8 pictures (base grey 128, the first n px at - another level): a bit-identical monolith x3 + a nondeterministic inproc -> FAIL - (strict clause); a nondeterministic monolith (3 distinct / 3 passes, 10 px / delta - 4 apart) + split pictures inside 1.25x (10 px / delta 5) -> PASS, exit 0, no - adjudication line needed, the numbers printed; the same with the stdlib decoder - (W2_REDUCE_PNG_DECODER=pure) -> the same numbers; split beyond 1.25x in delta - (6 > 5) or in pixels (13 > 12.5) -> FAIL; one split ssim 0.0005+ from ONE - monolith reading -> FAIL; the pre-ID-P7-62 monolith x1 + a nondeterministic - split -> FAIL naming the >= 3 passes it lacks; a finished monolith pair short of - arms.txt's monolith_repeat -> FAIL; --extra-monolith DIR@BOOT adding two passes - to that x1 archive -> the rule applies, GATE3 PASS-WITH-EXTRA-READINGS (exit 1), - without @BOOT or with another boot -> INVALID-SESSION + monolith-determinism ID-P7-62, clause (2) in its nearest-monolith form, on synthetic 8x8 + pictures (grey 128 with runs of pixels at other levels): a bit-identical monolith + x3 + a nondeterministic inproc -> FAIL (strict clause); a nondeterministic + monolith in a chain (4 / 4 / 8 px apart, delta 2: D_mm 4, Delta_mm 2, bound + 1.25 x 4 + 32 = 37 px / 2 + 1 = 3) + split passes at most 37 px / delta 3 from + their nearest monolith pass (45 px from the farthest: outside the first form's + 1.25 x max-pair) -> PASS, exit 0, no adjudication line, the numbers printed, each + pass's nearest named (a px tie goes to the smaller delta); the stdlib decoder + (W2_REDUCE_PNG_DECODER=pure) -> the same numbers; a split pass 38 px from its + nearest -> FAIL; one at delta 4 from its nearest-by-px pass (M1, 4 px) -> FAIL + though another pass is delta 2 away; monolith x4 with a bit-identical twin pair + -> leave-one-out over passes (D_mm 4, not 20 over pictures), a split pass 40 px + from its nearest -> FAIL; one split ssim 0.0005+ from ONE monolith reading -> + FAIL; the pre-ID-P7-62 monolith x1 + a nondeterministic split -> FAIL naming the + >= 3 passes it lacks; a finished monolith pair short of arms.txt's + monolith_repeat -> FAIL; --extra-monolith DIR@BOOT adding two passes to that x1 + archive -> the rule applies, GATE3 PASS-WITH-EXTRA-READINGS (exit 1), without + @BOOT or with another boot -> INVALID-SESSION rate-gate the gate rate alone decides (no crash anywhere): k $BASE-Pass dsa cases turn Fail. k=1: 367/370, -0.270 pp -> PASS, exit 0; k=2: -0.541 pp -> FAIL on the rate; k=4: 364/6/0/1/0, -1.081 pp -> FAIL, CTS FAIL @@ -143,6 +149,12 @@ def write(path, data): path.write_text(data, encoding="utf-8") +def speck(*runs): + """A Canned.png picture: 8x8 grey 128 with each (start, count, level) run of pixels (row-major, + 0..63) at grey `level`; px(a, b) / delta(a, b) between two specks follow by hand.""" + return tuple(runs) + + def lookup(table, arm, case, repeat, default): """A canned per-repeat value: (arm, case, repeat), else (arm, case), else arm, else default.""" for key in ((arm, case, repeat), (arm, case), arm): @@ -186,13 +198,13 @@ class Canned: self.root, self.tree, self.ca = root, tree, ca def png(self, value): - """value: a grey level (a solid 8x8 picture), or (n, level): grey 128 with its first n pixels - (row-major) at `level` - the synthetic 'speckle' the ID-P7-62 scenarios move around.""" + """value: a grey level (a solid 8x8 picture), or speck(...): grey 128 with runs of pixels at + other levels - the synthetic 'speckle' the ID-P7-62 scenarios move around.""" if isinstance(value, tuple): - n, level = value rgba = bytearray(self.ca._solid(8, 8, 128)) - for i in range(n): - rgba[i * 4:i * 4 + 3] = bytes([level] * 3) + for start, n, level in value: + for i in range(start, start + n): + rgba[i * 4:i * 4 + 3] = bytes([level] * 3) return self.ca._png_bytes(8, 8, bytes(rgba)) return self.ca._png_bytes(8, 8, self.ca._solid(8, 8, value)) @@ -671,24 +683,38 @@ def scenario_unfinished(k, cn, tree): def scenario_determinism(k, cn, tree): print("[monolith-determinism] ID-P7-62: a monolith not bit-identical over >= 3 passes swaps the split arms' " - "bit-identity clause for the distributional check") - # A nondeterministic monolith: 3 distinct pictures, pairwise 10 px apart, largest delta 4 -> the - # split bound is 12.5 px / delta 5.0. - mono = {("monolith", A, 1): (10, 128), ("monolith", A, 2): (10, 132), ("monolith", A, 3): (10, 130)} - inside = {("inproc", A, 1): (10, 129), ("inproc", A, 2): (10, 131), ("inproc", A, 3): (10, 133), - ("spawn", A, 1): (10, 130), ("spawn", A, 2): (10, 132), ("spawn", A, 3): (10, 128)} + "bit-identity clause for the distributional check, clause (2) in its nearest-monolith form") + # A nondeterministic monolith in a chain: M1 = px 0..7 at 130, M2 = px 0..3 at 130, M3 = solid + # 128. M1-M2 4 px / delta 2, M2-M3 4 px / 2, M1-M3 8 px / 2 -> each pass's nearest OTHER pass is + # 4 px / delta 2: D_mm 4, Delta_mm 2, bound 1.25 x 4 + 32 = 37 px / 2 + 1 = 3. (The first form, + # 1.25 x the max over all pairs, bounded the split at 10 px / delta 2.5.) + m1, m2, m3 = speck((0, 8, 130)), speck((0, 4, 130)), 128 + mono = {("monolith", A, 1): m1, ("monolith", A, 2): m2, ("monolith", A, 3): m3} + # inproc rep3: px 8..44 at 131 -> nearest M3 at 37 px / delta 3 (41 px from M2, 45 from M1); + # spawn rep2: px 0..3 at 130 + 8..27 at 129 -> nearest M2, 20 px / delta 1; spawn rep3: px 0..7 + # at 131 -> 8 px from both M1 (delta 1) and M2 (delta 3): the tie goes to the smaller delta. + inside = {("inproc", A, 1): m1, ("inproc", A, 2): m2, ("inproc", A, 3): speck((8, 37, 131)), + ("spawn", A, 1): m3, ("spawn", A, 2): speck((0, 4, 130), (8, 20, 129)), + ("spawn", A, 3): speck((0, 8, 131))} rule_line = "nondeterministic monolith (3 distinct / 3 passes) -> distributional check (ID-P7-62)" - numbers = {"passes": 3, "distinct": 3, "rule": "distributional", "mono_pairs": 3, "mono_px_max": 10, - "mono_delta_max": 4, "split_pairs": 18, "split_px_max": 10, "split_delta_max": 5, "within": True} + numbers = {"passes": 3, "distinct": 3, "rule": "distributional", "mono_nearest_px_max": 4, + "mono_nearest_delta_max": 2, "split_nearest_px_max": 37, "split_nearest_delta_max": 3, + "px_bound": 37.0, "delta_bound": 3, "within": True} + numbers_line = ("monolith leave-one-out nearest: D_mm 4 px / Delta_mm 2 (3 passes); split-to-nearest-monolith max " + "37 px / delta 3 (6 passes; most px: inproc rep3 -> monolith rep3 37 px / delta 3); bound 1.25 x 4 " + "+ 32 = 37.00 px / 2 + 1 = 3: within") def det(v): return case(v, A).get("monolith_determinism", {}) + def near(v, label): + return next((n for n in det(v).get("split_nearest", []) if n.get("pass") == label), {}) + def has(v, needle): return any(needle in r for r in case(v, A).get("reasons", [])) # (a) the strict clause stands when the monolith is bit-identical over its 3 passes. - cn.window("det-strict", gate3_args={"picture": {("inproc", A, 2): (10, 131)}}) + cn.window("det-strict", gate3_args={"picture": {("inproc", A, 2): speck((0, 4, 130))}}) rc, text, v = run_reducer(cn.root, "det-strict", tree) k.expect("bit-identical monolith x3 + a nondeterministic inproc -> %s FAIL (strict clause), GATE3 FAIL" % A, case(v, A).get("verdict") == "FAIL" and overall(v) == "FAIL" and rc != 0 and det(v).get("rule") == "strict" @@ -696,18 +722,32 @@ def scenario_determinism(k, cn, tree): "bit-identical over 3 passes") and case(v, B).get("verdict") == "PASS", (case(v, A).get("reasons"), det(v))) - # (b) a nondeterministic monolith, the split pictures inside its spread -> PASS, no adjudication. + # (b) a nondeterministic monolith, every split pass within its nearest monolith pass's bound -> PASS. cn.window("det-inside", gate3_args={"picture": {**mono, **inside}}) rc, text, v = run_reducer(cn.root, "det-inside", tree) - k.expect("nondeterministic monolith (3 distinct / 3 passes) + split inside 1.25x -> %s PASS, GATE3 PASS, exit 0" % A, + k.expect("nondeterministic monolith (3 distinct / 3 passes) + every split pass within 1.25 x D_mm + 32 px / " + "Delta_mm + 1 of its nearest monolith pass (37 px / delta 3; 45 px / delta 3 from the farthest) -> %s " + "PASS, GATE3 PASS, exit 0" % A, case(v, A).get("verdict") == "PASS" and overall(v) == "PASS" and rc == 0 and "GATE3 PASS: 36/36 cases PASS\n" in text, (case(v, A).get("reasons"), overall(v), text[-400:])) - k.expect("...the rule line and the numbers: 10 px / delta 4 over 3 monolith pairs, 10 px / delta 5 over 18 " - "split pairs, bound 12.50 px / 5.00", - {key: det(v).get(key) for key in numbers} == numbers and rule_line in text - and "monolith-vs-monolith max 10 px / delta 4 (3 pairs); split-vs-monolith max 10 px / delta 5 (18 pairs); " - "bound 1.25x = 12.50 px / 5.00: within" in text - and g3(v, "determinism", {}).get("distributional") == [A], (det(v), text[:1500])) + k.expect("...the rule line and the numbers: D_mm 4 px / Delta_mm 2 over 3 monolith passes, split-to-nearest max " + "37 px / delta 3 over 6 split passes, bound 37.00 px / 3", + {key: det(v).get(key) for key in numbers} == numbers and rule_line in text and numbers_line in text + and len(det(v).get("split_nearest", [])) == 6 and g3(v, "determinism", {}).get("distributional") == [A], + (det(v), text[:1500])) + k.expect("...leave-one-out over the monolith passes: each pass's nearest OTHER pass is 4 px / delta 2", + [(n.get("pass"), n.get("px"), n.get("delta")) for n in det(v).get("mono_nearest", [])] + == [("monolith rep1", 4, 2), ("monolith rep2", 4, 2), ("monolith rep3", 4, 2)], det(v).get("mono_nearest")) + k.expect("...each split pass is scored against its NEAREST monolith pass (fewest px; a px tie goes to the " + "smaller delta)", + near(v, "inproc rep3") == {"pass": "inproc rep3", "nearest": "monolith rep3", "px": 37, "delta": 3, + "within": True} + and near(v, "spawn rep2") == {"pass": "spawn rep2", "nearest": "monolith rep2", "px": 20, "delta": 1, + "within": True} + and near(v, "spawn rep3") == {"pass": "spawn rep3", "nearest": "monolith rep1", "px": 8, "delta": 1, + "within": True} + and near(v, "inproc rep1").get("px") == 0 and near(v, "spawn rep1").get("nearest") == "monolith rep3", + det(v).get("split_nearest")) k.expect("...its cross-arm difference needs no gate3/adjudication.tsv line (decided by the rule)", case(v, A).get("cross_arm", {}).get("identical") is False and case(v, A).get("cross_arm", {}).get("distributional") is True @@ -719,23 +759,48 @@ def scenario_determinism(k, cn, tree): % decoder, {key: det(v).get(key) for key in numbers} == numbers and det(v).get("decoder", "").startswith("pure-python") and rc == 0, det(v)) - # (c) beyond 1.25x: in the per-channel delta, then in the pixel count. - cn.window("det-delta", gate3_args={"picture": {**mono, **inside, ("inproc", A, 3): (10, 134)}}) - rc, text, v = run_reducer(cn.root, "det-delta", tree) - k.expect("...one split picture at delta 6 > 1.25 x 4 -> %s FAIL, GATE3 FAIL" % A, - case(v, A).get("verdict") == "FAIL" and overall(v) == "FAIL" and rc != 0 - and det(v).get("split_delta_max") == 6 and det(v).get("within") is False - and has(v, "split-vs-monolith max per-channel delta 6 > 1.25 x the monolith-vs-monolith max 4 (= 5.00)") - and not has(v, "differing px"), case(v, A).get("reasons")) - cn.window("det-px", gate3_args={"picture": {**mono, **inside, ("inproc", A, 3): (13, 131)}}) + # (c) outside the bound: in pixels, then in the per-channel delta to the nearest-by-px pass. + cn.window("det-px", gate3_args={"picture": {**mono, **inside, ("inproc", A, 3): speck((8, 38, 131))}}) rc, text, v = run_reducer(cn.root, "det-px", tree) - k.expect("...one split picture 13 px off > 1.25 x 10 (delta inside) -> %s FAIL" % A, - case(v, A).get("verdict") == "FAIL" and rc != 0 and det(v).get("split_px_max") == 13 - and det(v).get("split_delta_max") == 4 - and has(v, "split-vs-monolith max 13 differing px > 1.25 x the monolith-vs-monolith max 10 (= 12.50)") - and not has(v, "per-channel delta"), (det(v), case(v, A).get("reasons"))) + k.expect("...one split pass 38 px from its nearest monolith pass > 1.25 x 4 + 32 = 37 (delta 3 inside) -> %s " + "FAIL, GATE3 FAIL" % A, + case(v, A).get("verdict") == "FAIL" and overall(v) == "FAIL" and rc != 0 + and det(v).get("split_nearest_px_max") == 38 and det(v).get("within") is False + and near(v, "inproc rep3").get("within") is False + and case(v, A).get("reasons") == ["ID-P7-62: inproc rep3 is 38 differing px from its nearest monolith pass " + "(monolith rep3) > 1.25 x D_mm 4 + 32 (= 37.00)"], + (det(v).get("split_nearest"), case(v, A).get("reasons"))) + # inproc rep3: px 0..3 at 126, 4..7 at 130 -> M1 4 px / delta 4 (the nearest), M2 8 px / 4, M3 8 px / 2. + cn.window("det-delta", gate3_args={"picture": {**mono, **inside, ("inproc", A, 3): speck((0, 4, 126), (4, 4, 130))}}) + rc, text, v = run_reducer(cn.root, "det-delta", tree) + k.expect("...one split pass at delta 4 from its nearest-by-px monolith pass (M1, 4 px) > 2 + 1 -> %s FAIL, though " + "another pass (M3, 8 px) is only delta 2 away" % A, + case(v, A).get("verdict") == "FAIL" and overall(v) == "FAIL" and rc != 0 + and det(v).get("split_nearest_delta_max") == 4 and det(v).get("within") is False + and case(v, A).get("reasons") == ["ID-P7-62: inproc rep3's per-channel delta to its nearest monolith pass " + "(monolith rep1, 4 px) is 4 > Delta_mm 2 + 1 (= 3)"], + (det(v).get("split_nearest"), case(v, A).get("reasons"))) - # (d) clause (1) holds against EVERY monolith reading, not one of them. + # (d) leave-one-out is over PASSES: a bit-identical twin pair is 0 px from each other. Monolith x4: + # rep1 = rep2 = solid, rep3 = px 0..19 at 130, rep4 = px 0..23 at 130 -> D_mm = max(0, 0, 4, 4) = 4 + # (over distinct pictures it would be 20); inproc rep3 = px 24..63 at 129 is 40 px from its nearest + # (rep1) > 37 -> FAIL. + twins = {("monolith", A, 1): 128, ("monolith", A, 2): 128, ("monolith", A, 3): speck((0, 20, 130)), + ("monolith", A, 4): speck((0, 24, 130)), ("inproc", A, 3): speck((24, 40, 129))} + cn.window("det-twins", gate3_args={"arms": (("monolith", 4),) + ARMS[1:], "picture": twins}) + rc, text, v = run_reducer(cn.root, "det-twins", tree) + k.expect("monolith x4 with a bit-identical twin pair (3 distinct / 4 passes): D_mm 4 over the passes, not 20 " + "over the pictures; a split pass 40 px from its nearest -> %s FAIL" % A, + case(v, A).get("verdict") == "FAIL" and rc != 0 and det(v).get("rule") == "distributional" + and (det(v).get("passes"), det(v).get("distinct")) == (4, 3) + and [(n.get("pass"), n.get("nearest"), n.get("px")) for n in det(v).get("mono_nearest", [])] + == [("monolith rep1", "monolith rep2", 0), ("monolith rep2", "monolith rep1", 0), + ("monolith rep3", "monolith rep4", 4), ("monolith rep4", "monolith rep3", 4)] + and det(v).get("px_bound") == 37.0 + and has(v, "inproc rep3 is 40 differing px from its nearest monolith pass (monolith rep1)"), + (det(v), case(v, A).get("reasons"))) + + # (e) clause (1) holds against EVERY monolith reading, not one of them. ssim = {("monolith", A, 1): 0.9978, ("monolith", A, 2): 0.998, ("monolith", A, 3): 0.9982, ("spawn", A, 2): 0.99831} cn.window("det-ssim", gate3_args={"picture": {**mono, **inside}, "ssim": ssim}) rc, text, v = run_reducer(cn.root, "det-ssim", tree) @@ -744,7 +809,7 @@ def scenario_determinism(k, cn, tree): and case(v, A).get("reasons") == ["spawn rep2 |ssim-monolith|=0.000510 > 0.0005 (max over 3 monolith readings)"], case(v, A).get("reasons")) - # (e) the pre-ID-P7-62 archives (monolith x1, no monolith_repeat= in arms.txt): the rule cannot apply. + # (f) the pre-ID-P7-62 archives (monolith x1, no monolith_repeat= in arms.txt): the rule cannot apply. cn.window("det-mono1", gate3_args={"arms": ARMS_MONO1, "arms_txt": ARMS_TXT_MONO1, "picture": inside}) rc, text, v = run_reducer(cn.root, "det-mono1", tree) k.expect("monolith x1 (the earlier 30-gate3.sh) + a nondeterministic split -> %s FAIL naming the >= 3 monolith " @@ -755,7 +820,7 @@ def scenario_determinism(k, cn, tree): "rule needs >= 3 same-session monolith passes, this session has 1") and case(v, B).get("verdict") == "PASS", (det(v), case(v, A).get("reasons"))) - # (f) the monolith pair's own bookkeeping: arms.txt monolith_repeat=3 holds a finished pair to 3. + # (g) the monolith pair's own bookkeeping: arms.txt monolith_repeat=3 holds a finished pair to 3. out = cn.window("det-short") shutil.rmtree(out / "gate3/archive/monolith" / (A + "-DirectVulkan") / "repeat-03") rc, text, v = run_reducer(cn.root, "det-short", tree) @@ -768,16 +833,17 @@ def scenario_determinism(k, cn, tree): case(v, A).get("verdict") == "INCOMPLETE" and overall(v) == "INCOMPLETE" and "monolith: 2/3 repeats" in case(v, A).get("reasons", []), case(v, A).get("reasons")) - # (g) --extra-monolith: the g3det E1-mono re-reduction shape (x1 archive + passes outside gate3/). + # (h) --extra-monolith: the g3det E1-mono re-reduction shape (x1 archive = M3 + passes outside gate3/). cn.window("det-extra", gate3_args={"arms": ARMS_MONO1, "arms_txt": ARMS_TXT_MONO1, "picture": inside}) - extra = cn.extra_monolith(cn.root / "extra-unstamped", A, [(10, 132), (10, 130)]) + extra = cn.extra_monolith(cn.root / "extra-unstamped", A, [m1, m2]) rc, text, v = run_reducer(cn.root, "det-extra", tree, extra=["%s@%s" % (extra, BOOT)]) k.expect("x1 archive + 2 extra monolith passes attested @session boot -> the rule applies (3 distinct / 3), " "%s PASS, GATE3 PASS-WITH-EXTRA-READINGS, exit 1" % A, case(v, A).get("verdict") == "PASS" and det(v).get("rule") == "distributional" and overall(v) == "PASS-WITH-EXTRA-READINGS" and rc == 1 and "GATE3 PASS-WITH-EXTRA-READINGS: 36/36 cases PASS" in text and "NOT a gate verdict" in text - and "monolith 38/38 repeat(s) (2 of them --extra-monolith)" in text, + and "monolith 38/38 repeat(s) (2 of them --extra-monolith)" in text + and near(v, "spawn rep3").get("nearest") == "monolith +extra-unstamped rep1", (overall(v), case(v, A).get("reasons"), det(v), text[-600:])) rc, text, v = run_reducer(cn.root, "det-extra", tree, extra=[extra]) s = g3(v, "session", {}) @@ -788,7 +854,7 @@ def scenario_determinism(k, cn, tree): k.expect("...attested @another boot -> GATE3 INVALID-SESSION naming it", overall(v) == "INVALID-SESSION" and rc != 0 and any(OTHER_BOOT in p for p in g3(v, "session", {}).get("problems", [])), g3(v, "session")) - stamped = cn.extra_monolith(cn.root / "extra-stamped", A, [(10, 132), (10, 130)], boot=BOOT) + stamped = cn.extra_monolith(cn.root / "extra-stamped", A, [m1, m2], boot=BOOT) rc, text, v = run_reducer(cn.root, "det-extra", tree, extra=[stamped]) k.expect("...extra passes whose own boot_id.txt is the session's (no @BOOT_ID) -> PASS-WITH-EXTRA-READINGS", overall(v) == "PASS-WITH-EXTRA-READINGS" and rc == 1 and case(v, A).get("verdict") == "PASS", overall(v)) diff --git a/docs/Disaggregated/notes/p7/device-window-2/tools/60-reduce.py b/docs/Disaggregated/notes/p7/device-window-2/tools/60-reduce.py index 31cd3834..d878ca25 100644 --- a/docs/Disaggregated/notes/p7/device-window-2/tools/60-reduce.py +++ b/docs/Disaggregated/notes/p7/device-window-2/tools/60-reduce.py @@ -38,15 +38,19 @@ GATE 3 (CONTRACT-P7 7.1/7.2), per case of gate3/cases.txt: presupposes a bit-reproducible reference. A case whose same-session monolith pictures are NOT all bit-identical over >= 3 passes has none, so for it the split arms' bit-identity clause is replaced by the distributional check: (1) the |ssim - m| clause above, for every monolith - reading m; (2) over every split-vs-monolith picture pair (inproc and spawn repeats x monolith - passes) the maximum differing-pixel count (any RGBA channel differs) and the maximum - per-channel delta are each <= 1.25 x the monolith-vs-monolith maximum. The pixels are read - from the archived actual PNGs (numpy + PIL; without them, or with W2_REDUCE_PNG_DECODER=pure, - compare_actuals' stdlib decoder - the same numbers, slower). Such a case prints - 'nondeterministic monolith (N distinct / M passes) -> distributional check' and its numbers, - and its cross-arm difference is decided by (2), not by gate3/adjudication.tsv. A case whose - monolith is bit-identical, or that has fewer than 3 monolith passes (the pre-ID-P7-62 x1 - archives), keeps the strict clause; + reading m; (2) NEAREST MONOLITH (integrator ruling on ID-P7-62, replacing the first form's + 1.25 x the max over all pairs): px(a, b) = the pixels where any RGBA channel differs, delta(a, b) + = the largest per-channel difference; the nearest of a pass among candidate monolith passes is + the one with the fewest differing px (a tie: the smaller delta), and its delta is measured to + that same pass. D_mm / Delta_mm = the max over the monolith passes of px / delta to the nearest + OTHER monolith pass (leave-one-out, over passes: a bit-identical twin is 0 / 0); every split + pass s (inproc and spawn repeats) must hold px(s, nearest) <= 1.25 x D_mm + 32 AND + delta(s, nearest) <= Delta_mm + 1. The pixels are read from the archived actual PNGs (numpy + + PIL; without them, or with W2_REDUCE_PNG_DECODER=pure, compare_actuals' stdlib decoder - the + same numbers, slower). Such a case prints 'nondeterministic monolith (N distinct / M passes) + -> distributional check' and its numbers, and its cross-arm difference is decided by (2), not + by gate3/adjudication.tsv. A case whose monolith is bit-identical, or that has fewer than 3 + monolith passes (the pre-ID-P7-62 x1 archives), keeps the strict clause; * --extra-monolith DIR[@BOOT_ID] (repeatable; an adjudication re-reduction, never the gate): adds the passes under DIR/-DirectVulkan/repeat-NN (a run_android_retrace_local.py --archive-dir tree) to the case's monolith readings. Each must be the session's: a repeat's @@ -111,7 +115,6 @@ non-skipped case of the run's caselist and unrun.txt is empty, 3 when not (the r """ import argparse import hashlib -import itertools import json import os import re @@ -121,10 +124,14 @@ from pathlib import Path TOL = 0.0005 # ID-P7-62 (g3det VERDICT.md section 2): a case whose same-session monolith is not bit-identical -# over >= MONOLITH_RULE_PASSES passes is judged by the distributional check, whose pixel bound is -# SPREAD_FACTOR x the monolith's own spread. +# over >= MONOLITH_RULE_PASSES passes is judged by the distributional check, whose clause (2) holds +# every split pass to its nearest monolith pass within SPREAD_FACTOR x D_mm + PX_HEADROOM px and +# Delta_mm + DELTA_HEADROOM per channel (D_mm / Delta_mm: the monolith's leave-one-out nearest +# spread; integrator ruling on ID-P7-62). MONOLITH_RULE_PASSES = 3 SPREAD_FACTOR = 1.25 +PX_HEADROOM = 32 +DELTA_HEADROOM = 1 RULING_62 = "ID-P7-62" UUID = re.compile(r"^(.+)@([0-9a-f]{8}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{12})$") # CONTRACT-P7 7.1/7.2's constants: the gate is held to these, never to what gate3/arms.txt, @@ -372,10 +379,14 @@ def picture_reader(ca): return PurePictures(ca) -def spread(reader, mono, split): - """ID-P7-62 clause (2). mono, split: [(sha, path)] over every reading (a picture repeated in - several readings is decoded and compared once; an identical pair counts as 0 px / delta 0). - -> {mono_pairs, mono_px_max, mono_delta_max, split_pairs, split_px_max, split_delta_max}.""" +def nearest_spread(reader, mono, split): + """ID-P7-62 clause (2), nearest-monolith form. mono, split: [(label, sha, path)] over every + reading (a picture repeated in several readings is decoded and compared once; an identical pair + is 0 px / delta 0). The nearest of a pass among candidates is the one with the fewest differing + px, a tie broken by the smaller delta (then the first listed); its delta is measured to that + same pass. -> {mono_nearest: [{pass, nearest, px, delta}] (leave-one-out: the nearest OTHER + monolith pass), mono_nearest_px_max (D_mm), mono_nearest_delta_max (Delta_mm), split_nearest: + [...] (the nearest monolith pass), split_nearest_px_max, split_nearest_delta_max}.""" cache, memo = {}, {} def load(sha, path): @@ -383,22 +394,27 @@ def spread(reader, mono, split): cache[sha] = reader.load(path) return cache[sha] - def worst(pairs): - px = delta = 0 - for (sa, pa), (sb, pb) in pairs: - if sa == sb: - continue - key = (sa, sb) if sa < sb else (sb, sa) - if key not in memo: - memo[key] = reader.diff(load(sa, pa), load(sb, pb)) - px, delta = max(px, memo[key][0]), max(delta, memo[key][1]) - return px, delta - mono_pairs = list(itertools.combinations(mono, 2)) - split_pairs = list(itertools.product(split, mono)) - mono_px, mono_delta = worst(mono_pairs) - split_px, split_delta = worst(split_pairs) - return {"mono_pairs": len(mono_pairs), "mono_px_max": mono_px, "mono_delta_max": mono_delta, - "split_pairs": len(split_pairs), "split_px_max": split_px, "split_delta_max": split_delta} + def diff(a, b): + (_, sa, pa), (_, sb, pb) = a, b + if sa == sb: + return 0, 0 + key = (sa, sb) if sa < sb else (sb, sa) + if key not in memo: + memo[key] = reader.diff(load(sa, pa), load(sb, pb)) + return memo[key] + + def nearest(item, candidates): + px, delta, _, other = min((diff(item, c) + (i, c) for i, c in enumerate(candidates)), + key=lambda t: t[:3]) + return {"pass": item[0], "nearest": other[0], "px": px, "delta": delta} + mono_nearest = [nearest(m, mono[:i] + mono[i + 1:]) for i, m in enumerate(mono)] + split_nearest = [nearest(s, mono) for s in split] + return {"mono_nearest": mono_nearest, + "mono_nearest_px_max": max(n["px"] for n in mono_nearest), + "mono_nearest_delta_max": max(n["delta"] for n in mono_nearest), + "split_nearest": split_nearest, + "split_nearest_px_max": max((n["px"] for n in split_nearest), default=0), + "split_nearest_delta_max": max((n["delta"] for n in split_nearest), default=0)} def extra_monolith(ca, specs): @@ -498,6 +514,9 @@ def gate3(out, ca, extras=()): def picture(row): return str(Path(row["dir"]) / row["actual"]) if row and row.get("actual") else None + def mono_label(row): # a monolith reading, short: "monolith rep2", "monolith +E1-mono rep3" + return "monolith %srep%d" % ("+%s " % Path(row["extra"]).name if row.get("extra") else "", row["repeat"]) + def ra0_proof(row): p = Path(row["dir"]) / "mobilegl.log" if not p.is_file(): @@ -619,30 +638,37 @@ def gate3(out, ca, extras=()): if lc[i] and lc[i] == lc[i - 1]: reasons.append("%s rep%d STALE (logcat identical to rep%d)" % (arm, rs[i]["repeat"], rs[i - 1]["repeat"])) if distributional: - # ID-P7-62 clause (2): the split pictures lie inside the monolith's own spread. - split_valid = [r for arm in SPLIT_ARMS for r in split_rows[arm] if not r.get("error") and r.get("actual")] - split_ssims = [r["ssim_vs_golden"] for r in split_valid if isinstance(r.get("ssim_vs_golden"), (int, float))] + # ID-P7-62 clause (2), nearest-monolith form: every split pass lies within the monolith's + # own leave-one-out nearest spread of its nearest monolith pass. + split_valid = [("%s rep%d" % (arm, r["repeat"]), r) for arm in SPLIT_ARMS for r in split_rows[arm] + if not r.get("error") and r.get("actual")] + split_ssims = [r["ssim_vs_golden"] for _, r in split_valid if isinstance(r.get("ssim_vs_golden"), (int, float))] det["max_dssim"] = max((abs(s - m) for s in split_ssims for m in mono_ssims), default=None) reader = reader or picture_reader(ca) det["decoder"] = reader.name try: - det.update(spread(reader, [(m["actual_sha256"], picture(m)) for m in mono_rows if m.get("actual")], - [(r["actual_sha256"], picture(r)) for r in split_valid])) + det.update(nearest_spread( + reader, [(mono_label(m), m["actual_sha256"], picture(m)) for m in mono_rows if m.get("actual")], + [(label, r["actual_sha256"], picture(r)) for label, r in split_valid])) except Exception as error: # an unreadable / mis-sized picture: no measurement, no pass det["error"] = "%s: %s" % (type(error).__name__, error) reasons.append("%s distributional check cannot be measured (%s)" % (RULING_62, det["error"])) else: - det["px_bound"] = SPREAD_FACTOR * det["mono_px_max"] - det["delta_bound"] = SPREAD_FACTOR * det["mono_delta_max"] - det["within"] = det["split_px_max"] <= det["px_bound"] and det["split_delta_max"] <= det["delta_bound"] - if det["split_px_max"] > det["px_bound"]: - reasons.append("%s: split-vs-monolith max %d differing px > %.2f x the monolith-vs-monolith max %d " - "(= %.2f)" % (RULING_62, det["split_px_max"], SPREAD_FACTOR, det["mono_px_max"], - det["px_bound"])) - if det["split_delta_max"] > det["delta_bound"]: - reasons.append("%s: split-vs-monolith max per-channel delta %d > %.2f x the monolith-vs-monolith " - "max %d (= %.2f)" % (RULING_62, det["split_delta_max"], SPREAD_FACTOR, - det["mono_delta_max"], det["delta_bound"])) + d_mm, delta_mm = det["mono_nearest_px_max"], det["mono_nearest_delta_max"] + det["px_bound"] = SPREAD_FACTOR * d_mm + PX_HEADROOM + det["delta_bound"] = delta_mm + DELTA_HEADROOM + for n in det["split_nearest"]: + n["within"] = n["px"] <= det["px_bound"] and n["delta"] <= det["delta_bound"] + if n["px"] > det["px_bound"]: + reasons.append("%s: %s is %d differing px from its nearest monolith pass (%s) > %.2f x D_mm %d " + "+ %d (= %.2f)" % (RULING_62, n["pass"], n["px"], n["nearest"], SPREAD_FACTOR, + d_mm, PX_HEADROOM, det["px_bound"])) + if n["delta"] > det["delta_bound"]: + reasons.append("%s: %s's per-channel delta to its nearest monolith pass (%s, %d px) is %d > " + "Delta_mm %d + %d (= %d)" % (RULING_62, n["pass"], n["nearest"], n["px"], + n["delta"], delta_mm, DELTA_HEADROOM, + det["delta_bound"])) + det["within"] = all(n["within"] for n in det["split_nearest"]) # The RUN_AHEAD=0 control arm: required on every case (CONTRACT-P7 7.2 "RUN_AHEAD=0 对照臂一遍 # 记录"), and it must be that arm; its picture is recorded, never gating. ra0 = rows("inproc-ra0", case) @@ -790,11 +816,17 @@ def print_gate3(g3): print("%-*s nondeterministic monolith (%d distinct / %d passes) -> distributional check (%s)" % ( w, "", det["distinct"], det["passes"], RULING_62)) if "error" not in det: - print("%-*s monolith-vs-monolith max %d px / delta %d (%d pairs); split-vs-monolith max %d px / " - "delta %d (%d pairs); bound %.2fx = %.2f px / %.2f: %s; max |ssim - monolith| %s; decoder %s" % ( - w, "", det["mono_px_max"], det["mono_delta_max"], det["mono_pairs"], det["split_px_max"], - det["split_delta_max"], det["split_pairs"], SPREAD_FACTOR, det["px_bound"], - det["delta_bound"], "within" if det["within"] else "OUTSIDE", + worst = max(det["split_nearest"], key=lambda n: (n["px"], n["delta"]), default=None) + print("%-*s monolith leave-one-out nearest: D_mm %d px / Delta_mm %d (%d passes); split-to-nearest-" + "monolith max %d px / delta %d (%d passes%s); bound %.2f x %d + %d = %.2f px / %d + %d = %d: %s; " + "max |ssim - monolith| %s; decoder %s" % ( + w, "", det["mono_nearest_px_max"], det["mono_nearest_delta_max"], len(det["mono_nearest"]), + det["split_nearest_px_max"], det["split_nearest_delta_max"], len(det["split_nearest"]), + "; most px: %s -> %s %d px / delta %d" % (worst["pass"], worst["nearest"], worst["px"], + worst["delta"]) if worst else "", + SPREAD_FACTOR, det["mono_nearest_px_max"], PX_HEADROOM, det["px_bound"], + det["mono_nearest_delta_max"], DELTA_HEADROOM, det["delta_bound"], + "within" if det["within"] else "OUTSIDE", "-" if det["max_dssim"] is None else "%.1e" % det["max_dssim"], det["decoder"])) for reason in e["reasons"]: print("%-*s ! %s" % (w, "", reason)) diff --git a/docs/Disaggregated/notes/p7/device-window-2/tools/window.sh b/docs/Disaggregated/notes/p7/device-window-2/tools/window.sh old mode 100644 new mode 100755