# Generated by tools/algo/check.py from lib/algo/algo.spec: do not edit.
# Each case prints its input (= X), its results, and the verdict of each postcondition
# (? ...) as lib/algo/props.viv computes it; check.py checks them again in Python.
from algo.cases import algo_case, CASE_NAMES
from algo.props import algo_all_gcd
from algo.legacy.gcd_post import gcd
#| gcd_post: the gcd of posts/2026-09-25-the-error-follows-the-condition-number.viv
def algo_t_gcd_post(kind, n, inside, skip: Arr) -> Bool {
X = algo_case(kind, n, 1 + 97 * kind + n)
print("@ gcd_post", CASE_NAMES[kind], n)
A = floor(X * 200)
B = floor(algo_case(kind, len(X), len(X) + 7) * 200)
R = zeros(len(X))
for i to len(X) {
R[i] = gcd(A[i], B[i])
}
print("= X", fmt(X))
print("= R", fmt(R))
print("= A", fmt(A))
print("= B", fmt(B))
p0 = algo_all_gcd(R, A, B)
print("?", p0)
return inside == 0 or ((p0 or skip[0] == 1))
}
algo_t_ok_gcd_post = true
algo_t_kinds_gcd_post = [0.0, 1.0]
algo_t_inside_gcd_post = [0.0, 1.0]
algo_t_sizes_gcd_post = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 7.0, 8.0, 9.0, 15.0, 16.0, 17.0, 31.0, 32.0, 33.0, 63.0, 64.0, 65.0, 129.0, 257.0]
algo_t_skip_gcd_post = [0.0, 0.0]
for algo_t_k to len(algo_t_kinds_gcd_post) {
for algo_t_s to len(algo_t_sizes_gcd_post) {
algo_t_r = algo_t_gcd_post(algo_t_kinds_gcd_post[algo_t_k], algo_t_sizes_gcd_post[algo_t_s], algo_t_inside_gcd_post[algo_t_k], algo_t_skip_gcd_post[algo_t_k * 1:(algo_t_k + 1) * 1])
algo_t_ok_gcd_post = algo_t_ok_gcd_post and algo_t_r
}
}
test "gcd_post: gcd R A B (kinds dups)" {
assert_true(algo_t_ok_gcd_post)
}