#!/usr/bin/env python3
"""Build the FC11 card source from the shared FreeRTOS C card vocabulary."""

import hashlib
import json
import subprocess
import uuid
from pathlib import Path


ROOT = Path(__file__).resolve().parents[1]
BASE = ROOT.parent / "lab-rv32i-freertos-c-notifications" / "json" / "card_source.json"


def sha256(path: Path) -> str:
    return hashlib.sha256(path.read_bytes()).hexdigest()


def code_step(step_id, number, label, code_ref, evidence, strategy="code.storage"):
    return {
        "id": step_id, "number": number, "label": label, "mode": "CODE",
        "strategy_ref": strategy, "svg_label": f"{number:02d}",
        "code_ref": code_ref, "description": label, "evidence": evidence,
    }


def run_step(step_id, number, label, event, code_ref, evidence, strategy="run.heap"):
    snapshot = {
        1: "h0", 2: "h1", 3: "h2", 4: "dynamic-run",
        5: "static-run", 6: "dynamic-callback", 7: "static-callback",
        8: "pass",
    }[event]
    return {
        "id": step_id, "number": number, "label": label, "mode": "RUN",
        "event_id": f"E{event:02d}", "strategy_ref": strategy,
        "svg_label": f"{number:02d}", "code_ref": code_ref,
        "snapshot_ref": f"task01.{snapshot}", "description": label,
        "evidence": evidence,
    }


def section(aid, label, title, content, asset, orientation, steps):
    width, height = (940, 560) if orientation == "landscape" else (660, 760)
    return {
        "title": f"{aid} — {label.title()}",
        "order": int(aid[1:]) * 10,
        "content_kind": "prose",
        "asset_page_mode": "one-per-page",
        "page_orientation": orientation,
        "content_tex": content,
        "assets": [{
            "path": f"assets/{asset}.png",
            "html_path": f"assets/{asset}.svg",
            "source_path": f"assets/{asset}.puml",
            "caption": f"{aid} {label} — {title}.",
            "label": f"fig:{asset}",
            "alt": title,
            "kind": "diagram",
            "width": 1.0,
            "page_grid": {
                "columns": 1, "rows": 1, "page_width": width,
                "page_height": height, "overview": True,
                "step_tiles": {s["id"]: 1 for s in steps},
            },
            "interactive": {
                "kind": "uml-class",
                "storage_key": f"fc11-{asset}",
                "title": f"{aid} · {title}",
                "task": {"id": "task01", "label": "Task01 · two storage policies"},
                "block": {"id": aid.lower(), "label": f"{aid} {label}", "description": content},
                "phases": [{"id": label.lower(), "label": title.upper(), "steps": steps}],
            },
        }],
    }


data = json.loads(BASE.read_text())
card_uuid = str(uuid.uuid5(uuid.NAMESPACE_URL, "stem:freertos-c:fc11:static-allocation"))
task_uuid = str(uuid.uuid5(uuid.NAMESPACE_URL, "stem:freertos-c:fc11:task01"))
issued = "2026-07-19T00:00:00+02:00"
repo_url = "http://77.90.8.171:3001/edu-inf/lab-rv32i-freertos-c-static-allocation"
html_url = f"https://{card_uuid}/{task_uuid}"

data["card"].update({
    "id": "mpabi-freertos-c-11-static-allocation",
    "number": "11", "count": "15", "slug": "static-allocation",
    "title": "Static and dynamic allocation",
    "topic": "task, queue and timer with two storage policies",
    "level": "Rok 2 · L11 · RV32I/Hazard3", "revision_date": issued,
    "version": "v00.01", "uuid": card_uuid,
})
data["title_block"].update({
    "title": "Static and dynamic allocation", "url": html_url,
    "repository_url": repo_url, "url_host_uuid": card_uuid,
    "doc_uuid": task_uuid, "issued_on": issued, "series": "FREERTOS-C-11",
})
data["front_page_scope"] = {
    "title": "Cel karty",
    "content_tex": "Uczeń rozdziela semantykę obiektu FreeRTOS od polityki przechowywania i dowodzi jej przez adresy oraz cztery pomiary wolnego heap.",
    "scope_title": "Zakres karty",
    "scope_content_tex": "Dynamiczny i statyczny task, queue oraz timer wykonują ten sam eksperyment. H1 jest mniejsze od H0, H2 równa się H1, a H3 równa się H2. Pamięć Idle i timer-service dostarcza aplikacja.",
    "scope_table": {"headers": ["Lekcja", "Task", "Idea", "Priorytet", "Status", "Version"], "rows": [{
        "chapter": "FC11", "task": "Task01", "idea_tex": "behavior parity plus storage provenance",
        "priority": "główny", "status": "ready", "version": "v00.01", "key": True,
    }]},
}
data["viewpoints"] = [
    {"id": "A1", "label": "CONTEXT", "subtitle": "ownership boundaries", "status": "enabled", "target_label": "fig:a1-context"},
    {"id": "A2", "label": "STRUCTURE", "subtitle": "dynamic/static object pairs", "status": "enabled", "target_label": "fig:a2-structure"},
    {"id": "A3", "label": "DISPATCH", "subtitle": "same kernel dispatch", "status": "unavailable", "reason": "Storage policy does not change callback dispatch."},
    {"id": "A4", "label": "APPLICATION", "subtitle": "behavior parity", "status": "enabled", "target_label": "fig:a4-application"},
    {"id": "A5", "label": "FLOW", "subtitle": "H0/H1/H2/H3", "status": "enabled", "target_label": "fig:a5-flow"},
    {"id": "A6", "label": "STATE", "subtitle": "covered by flow", "status": "unavailable", "reason": "No new lifecycle state machine; the card compares storage."},
    {"id": "A7", "label": "RUNTIME", "subtitle": "address provenance", "status": "enabled", "target_label": "fig:a7-runtime"},
    {"id": "A8", "label": "PATTERNS", "subtitle": "policy comparison", "status": "unavailable", "reason": "No wrapper pattern is introduced in this C card."},
]
data["debug_strategies"] = {
    "code.storage": {
        "id": "code.storage", "kind": "code", "action": "open",
        "expected_observations": ["persistent Static* buffers", "application static Idle/timer task memory"],
        "assertions": ["no local-lifetime storage", "both allocation modes enabled"],
        "evidence_fields": ["symbol", "section", "code_ref"], "prerequisites": ["FC11 source"],
        "layout": ["buffers", "create APIs", "FreeRTOSConfig"],
        "commands": ["rg -n 'x.*CreateStatic|vApplicationGet.*TaskMemory|Static(Task|Queue|Timer)_t' include src"],
    },
    "run.heap": {
        "id": "run.heap", "kind": "run", "action": "replay",
        "expected_observations": ["H1 < H0", "H2 == H1", "H3 == H2"],
        "assertions": ["objects alive at H3", "no exact delta assumption"],
        "evidence_fields": ["H0", "H1", "H2", "H3", "timestamp"],
        "prerequisites": ["clean Hazard3 RAM"], "layout": ["heap values", "event order"],
        "commands": ["print g_fc11.heap_h0", "print g_fc11.heap_h1", "print g_fc11.heap_h2", "print g_fc11.heap_h3"],
    },
    "run.parity": {
        "id": "run.parity", "kind": "run", "action": "replay",
        "expected_observations": ["both receive 0xCAFE", "both timers callback once"],
        "assertions": ["distinct stacks", "PASS and deterministic digest"],
        "evidence_fields": ["received", "timer calls", "SP", "digest"],
        "prerequisites": ["scheduler running"], "layout": ["two branches", "verifier"],
        "commands": ["print/x g_fc11.dynamic_received", "print/x g_fc11.static_received", "print g_fc11_pass"],
    },
}

a1 = [
    code_step("application", 1, "application owns experiment", "src/tasks/task01_static_allocation.c:20", "global experiment"),
    code_step("dynamic", 2, "dynamic APIs request storage", "src/tasks/task01_static_allocation.c:218", "xTaskCreate/xQueueCreate/xTimerCreate"),
    code_step("static", 3, "static APIs receive storage", "src/tasks/task01_static_allocation.c:239", "named buffers"),
    code_step("kernel", 4, "kernel owns object semantics", "vendor/FreeRTOS-Kernel/tasks.c:1", "same scheduler"),
    code_step("ram", 5, "both policies coexist in RAM", "src/tasks/task01_static_allocation.c:26", "ucHeap plus static buffers"),
]
a2 = [
    run_step("dynamic-task", 1, "dynamic task handle is in heap", 2, "src/tasks/task01_static_allocation.c:218", "heap address"),
    run_step("static-task", 2, "static task uses TCB and stack buffers", 3, "src/tasks/task01_static_allocation.c:239", "outside heap"),
    run_step("dynamic-queue", 3, "dynamic queue object is in heap", 2, "src/tasks/task01_static_allocation.c:228", "heap address"),
    run_step("static-queue", 4, "static queue uses supplied storage", 3, "src/tasks/task01_static_allocation.c:247", "outside heap"),
    run_step("dynamic-timer", 5, "dynamic timer object is in heap", 2, "src/tasks/task01_static_allocation.c:229", "heap address"),
    run_step("static-timer", 6, "static timer uses StaticTimer_t", 3, "src/tasks/task01_static_allocation.c:250", "outside heap"),
    code_step("services", 7, "Idle and timer-service storage is static", "src/tasks/task01_static_allocation.c:45", "two application callbacks"),
]
a4 = [
    run_step("dynamic-worker", 1, "dynamic branch receives message", 4, "src/tasks/task01_static_allocation.c:121", "0xCAFE", "run.parity"),
    run_step("static-worker", 2, "static branch receives message", 5, "src/tasks/task01_static_allocation.c:139", "0xCAFE", "run.parity"),
    run_step("daemon", 3, "daemon executes both callbacks", 7, "src/tasks/task01_static_allocation.c:99", "1 + 1", "run.parity"),
    run_step("verifier", 4, "verifier checks behavior parity", 8, "src/tasks/task01_static_allocation.c:157", "PASS", "run.parity"),
]
a5 = [
    run_step("h0", 1, "H0 baseline", 1, "src/tasks/task01_static_allocation.c:214", "baseline"),
    run_step("h1", 2, "dynamic objects make H1 smaller", 2, "src/tasks/task01_static_allocation.c:236", "H1 < H0"),
    run_step("h2", 3, "static objects leave heap unchanged", 3, "src/tasks/task01_static_allocation.c:263", "H2 = H1"),
    run_step("dynamic-run", 4, "dynamic worker runs", 4, "src/tasks/task01_static_allocation.c:121", "message" , "run.parity"),
    run_step("static-run", 5, "static worker runs", 5, "src/tasks/task01_static_allocation.c:139", "message", "run.parity"),
    run_step("dynamic-callback", 6, "dynamic timer callback", 6, "src/tasks/task01_static_allocation.c:99", "count 1", "run.parity"),
    run_step("static-callback", 7, "static timer callback", 7, "src/tasks/task01_static_allocation.c:99", "count 1", "run.parity"),
    run_step("pass", 8, "H3 unchanged and verifier passes", 8, "src/tasks/task01_static_allocation.c:157", "H3 = H2", "run.parity"),
]
a7 = [
    run_step("heap-arena", 1, "dynamic handles lie in ucHeap", 8, "src/tasks/task01_static_allocation.c:174", "three true predicates"),
    run_step("named-buffers", 2, "static handles lie outside ucHeap", 8, "src/tasks/task01_static_allocation.c:177", "three false predicates"),
    code_step("service-buffers", 3, "kernel-service buffers are named", "src/tasks/task01_static_allocation.c:34", "Idle and daemon buffers"),
    run_step("heap-relation", 4, "four checkpoints satisfy relation", 8, "include/task01_static_allocation_model.h:34", "H1<H0; H2=H1; H3=H2"),
    run_step("evidence", 5, "commit-last evidence is deterministic", 8, "src/tasks/task01_static_allocation.c:72", "cdf44a0a", "run.parity"),
]
data["sections"] = [
    section("A1", "CONTEXT", "ownership boundaries", "Application, kernel and RAM responsibilities are explicit.", "a1-context", "portrait", a1),
    section("A2", "STRUCTURE", "object pairs", "Task, queue and timer are compared pairwise.", "a2-structure", "landscape", a2),
    section("A4", "APPLICATION", "behavior parity", "Storage differs while application behavior remains equal.", "a4-application", "portrait", a4),
    section("A5", "FLOW", "four heap checkpoints", "H0/H1/H2/H3 bracket creation and scheduler startup.", "a5-flow", "landscape", a5),
    section("A7", "RUNTIME", "address provenance", "Debugger evidence connects handles to heap or named buffers.", "a7-runtime", "portrait", a7),
    {"title": "Task01 — two storage policies", "order": 90, "content_kind": "tasks", "task_refs": ["task01"]},
]
data["tasks_order"] = ["task01"]
data["tasks"] = {"task01": {
    "title": "Same behavior, two storage policies", "uuid": task_uuid,
    "prompt_tex": "Przejdź po A1, A2, A4, A5 i A7. Odtwórz E01–E08 oraz udowodnij relacje H1<H0, H2=H1 i H3=H2.",
    "criterion": "PASS; address provenance; message and callback parity; deterministic digest.",
    "conclusion_tex": "Statyczne API zmienia własność pamięci, ale nie semantykę taska, kolejki ani timera.",
    "flow": [
        {"kind": "block", "id": "predict", "title": "A — przewidywanie", "content_tex": "Przewidź cztery pomiary heap.", "steps": [
            {"id": "relation", "title": "Zapisz relacje H0–H3.", "content_tex": "Nie zakładaj dokładnej liczby bajtów."},
            {"id": "ownership", "title": "Wskaż właściciela pamięci.", "content_tex": "Rozdziel ucHeap i named buffers."},
        ]},
        {"kind": "block", "id": "replay", "title": "B — replay Hazard3", "content_tex": "Wykonaj E01–E08 z clean RAM.", "steps": [
            {"id": "heap", "title": "Zbadaj H0/H1/H2/H3.", "content_tex": "Zapisz wartości i relacje."},
            {"id": "parity", "title": "Zbadaj obie gałęzie.", "content_tex": "Porównaj message, timer callback i stack."},
            {"id": "pass", "title": "Zbadaj E08.", "content_tex": "Zapisz PASS, digest i timestamp."},
        ]},
        {"kind": "exercise", "id": "choose-policy", "title": "Ćwiczenie — wybór polityki", "prompt_tex": "Dla taska okresowego, kolejki telemetrycznej i timera bezpieczeństwa wybierz dynamiczne albo statyczne tworzenie. Uzasadnij lifetime i ownership.", "evidence_tex": "Tabela obiekt→API→storage→lifetime oraz ślad H0–H3.", "criterion": "Każdy bufor ma trwałość co najmniej tak długą jak obiekt kernelowy.", "based_on": ["predict", "replay"]},
    ],
    "educational_requirement_refs": ["FC11.WE01"], "learning_effect_refs": ["FC11.EN01", "FC11.EK01"], "assessment_criterion_ref": "FC11.KW01",
}}

elf = ROOT / "build/task01_static_allocation/prog.elf"
image = ROOT / "build/task01_static_allocation/prog.bin"
blob = subprocess.check_output(["git", "hash-object", "src/tasks/task01_static_allocation.c"], cwd=ROOT, text=True).strip()
items = {}
checks = {
    1: ("h0", ["g_fc11_event_count", 1]),
    2: ("h1", ["g_fc11.heap_h1 < g_fc11.heap_h0", 1]),
    3: ("h2", ["g_fc11.heap_h2 == g_fc11.heap_h1", 1]),
    4: ("dynamic-run", ["g_fc11.dynamic_received", 0xCAFE]),
    5: ("static-run", ["g_fc11.static_received", 0xCAFE]),
    6: ("dynamic-callback", ["g_fc11.dynamic_timer_calls", 1]),
    7: ("static-callback", ["g_fc11.static_timer_calls", 1]),
    8: ("pass", ["g_fc11_pass", 1]),
}
for event, (name, check) in checks.items():
    items[f"task01.{name}"] = {
        "event_id": f"E{event:02d}",
        "stop": {"symbol": "fc11_checkpoint_committed", "offset": 0, "condition": f"$a0 == {event}"},
        "verify": {"expressions": [{"expr": check[0], "equals": check[1]}]},
    }
data["debug_checkpoints"] = {
    "schema": "stem-debug-checkpoints.v1", "semantics": "deterministic-replay",
    "artifact": {"source": "src/tasks/task01_static_allocation.c", "source_git_blob": blob,
                 "elf": "build/task01_static_allocation/prog.elf", "hazard3_elf_sha256": sha256(elf),
                 "hazard3_image": "build/task01_static_allocation/prog.bin", "hazard3_image_sha256": sha256(image)},
    "targets": {"hazard3-sim": {"adapter": "hazard3-reset-load-replay.v1", "baseline": "restart-backend", "clean_ram": True}},
    "items": items,
}
data["educational_requirements"] = {"FC11.WE01": {
    "text": "Porównanie dynamicznej i statycznej polityki pamięci obiektów FreeRTOS.", "label": "storage policy and behavior parity",
    "learning_effects": ["FC11.EN01", "FC11.EK01"], "learning_tree": {
        "schema": "we-learning-tree.v1", "policy": "Każda aktywna kotwica wskazuje kod lub checkpoint.",
        "ogolne": [{"effect_ref": "FC11.EN01", "display": "EN LOCAL RTOS.11", "source": "LOCAL", "official": "RTOS", "local": "11", "kind": "EN", "tree_id": "FC11.WE01.OG.LOCAL.RTOS.11", "text": "Uczeń rozdziela semantykę obiektu i politykę przechowywania.", "kw": [{"criterion_ref": "FC11.KW01", "display": "KW LOCAL RTOS.11", "source": "LOCAL", "kind": "KW", "official": "RTOS", "local": "11", "text": "Łączy kod, diagram i dowód runtime."}]}],
        "zawodowe": [{"effect_ref": "FC11.EK01", "display": "EK LOCAL RTOS.11", "source": "LOCAL", "official": "RTOS", "local": "11", "kind": "EK", "tree_id": "FC11.WE01.TECH.LOCAL.RTOS.11", "text": "Uczeń odtwarza E01–E08 i dowodzi H1<H0, H2=H1, H3=H2.", "kw": [{"criterion_ref": "FC11.KW01", "display": "KW LOCAL RTOS.11", "source": "LOCAL", "kind": "KW", "official": "RTOS", "local": "11", "text": "Łączy kod, diagram i dowód runtime."}]}],
    },
}}
data["learning_effects"] = {
    "FC11.EN01": {"bloom_level": "Analiza", "label": "Storage ownership", "text": "Uczeń rozdziela semantykę obiektu i politykę przechowywania.", "assessment_criteria": ["FC11.KW01"]},
    "FC11.EK01": {"bloom_level": "Zastosowanie", "label": "Heap replay", "text": "Uczeń odtwarza E01–E08 i dowodzi H1<H0, H2=H1, H3=H2.", "assessment_criteria": ["FC11.KW01"]},
}
data["assessment_criteria"] = {"FC11.KW01": {"text": "PASS; address provenance; message and callback parity; deterministic digest.", "learning_effects": ["FC11.EN01", "FC11.EK01"]}}

spec_sections = []
for expanded in data["sections"]:
    if expanded.get("content_kind") == "tasks":
        continue
    aid = expanded["title"].split()[0]
    asset = expanded["assets"][0]
    interactive = asset["interactive"]
    stem = Path(asset["path"]).stem
    spec_asset = {
        "stem": stem,
        "title": interactive["title"],
        "caption": asset["caption"],
        "label": asset["label"],
        "alt": asset["alt"],
        "phases": interactive["phases"],
    }
    if aid == "A5":
        spec_asset["diagram_kind"] = "sequence"
    spec_sections.append({
        "id": aid,
        "label": interactive["block"]["label"].split(maxsplit=1)[1],
        "title": expanded["title"].split("—", 1)[1].strip(),
        "order": expanded["order"],
        "orientation": expanded["page_orientation"],
        "description": interactive["block"]["description"],
        "content_tex": expanded["content_tex"],
        "assets": [spec_asset],
    })

task = data["tasks"]["task01"]
spec = {
    "card": {key: data["card"][key] for key in ("number", "slug", "title", "topic", "status", "version")},
    "front": {"goal": data["front_page_scope"]["content_tex"], "scope": data["front_page_scope"]["scope_content_tex"]},
    "viewpoints": [{key: value[key] for key in ("id", "label", "status", "subtitle", "reason") if key in value} for value in data["viewpoints"]],
    "artifact": {"source": "src/tasks/task01_static_allocation.c", "elf": "build/task01_static_allocation/prog.elf", "image": "build/task01_static_allocation/prog.bin"},
    "strategies": list(data["debug_strategies"].values()),
    "checkpoints": data["debug_checkpoints"]["items"],
    "sections": spec_sections,
    "learning": {
        "model_label": data["learning_effects"]["FC11.EN01"]["label"],
        "model": data["learning_effects"]["FC11.EN01"]["text"],
        "replay_label": data["learning_effects"]["FC11.EK01"]["label"],
        "replay": data["learning_effects"]["FC11.EK01"]["text"],
        "criterion": data["assessment_criteria"]["FC11.KW01"]["text"],
        "requirement": data["educational_requirements"]["FC11.WE01"]["text"],
    },
    "task": {
        "short_label": "two storage policies",
        "title": task["title"], "prompt_tex": task["prompt_tex"],
        "conclusion_tex": task["conclusion_tex"], "flow": task["flow"],
    },
}

out = ROOT / "json/card_spec.json"
out.write_text(json.dumps(spec, ensure_ascii=False, indent=2) + "\n")
print(out)