ASELSANMicrokernel
S86 · SOURCE-BOUND GATE EVIDENCE

G8g hardened production machine-code ve layout kapısı yeşil

Operations komutu/kapı ailesi → gerçek repository yürütme sözleşmesi Bu sayfa yalnız S86 kapısına aittir; komşu kapıların kaynakları bu kabulün içine katılmaz.

S86Komut / fiziksel sözleşmeOperations id exactsource SHA exact

operation: rpi5-g8g-production-layout-green

script/Makefile/config · Operations · 2 exact excerpt

sequence-bound=true · implementation-bound=false
01 · Yürütme sözleşmesi

Gerçek script / Makefile / config kaynağı

tam dosyaL1–L1926
scripts/verify-rpi5-g8g-layout.sh::verify-rpi5-g8g-layout.sh
#!/bin/sh
set -eu

if [ "$#" -ne 2 ]; then
    echo "usage: $0 <llvm-objdump> <rpi5-kernel-elf>" >&2
    exit 2
fi

objdump=$1
kernel=$2
if [ ! -f "$objdump" ] || [ ! -x "$objdump" ]; then
    echo "HATA: G8g gate llvm-objdump çalıştıramıyor: $objdump" >&2
    exit 1
fi
if [ ! -f "$kernel" ] || [ ! -r "$kernel" ]; then
    echo "HATA: G8g gate kernel ELF'ini okuyamıyor: $kernel" >&2
    exit 1
fi

tmpdir=$(mktemp -d "${TMPDIR:-/tmp}/aselsanos-g8g-layout.XXXXXX")
trap 'rm -rf "$tmpdir"' EXIT HUP INT TERM

format=$tmpdir/format
symbols=$tmpdir/symbols
ppi=$tmpdir/ppi
released=$tmpdir/released
active=$tmpdir/active
secondary=$tmpdir/secondary
handler=$tmpdir/handler
primary=$tmpdir/primary
g8f_secondary=$tmpdir/g8f-secondary
g8f_primary=$tmpdir/g8f-primary
irq_dispatch=$tmpdir/irq-dispatch
timer_snapshot=$tmpdir/timer-snapshot
timer_prepare=$tmpdir/timer-prepare
timer_advance=$tmpdir/timer-advance
timer_disable=$tmpdir/timer-disable
secondary_fail=$tmpdir/secondary-fail
consume_error=$tmpdir/consume-error
publish_error=$tmpdir/publish-error
primary_fail=$tmpdir/primary-fail
error_name=$tmpdir/error-name
prerequisite_complete=$tmpdir/prerequisite-complete
continue_to_g8h=$tmpdir/continue-to-g8h
primary_require=$tmpdir/primary-require
primary_closure0=$tmpdir/primary-closure0
primary_closure1=$tmpdir/primary-closure1
primary_closure2=$tmpdir/primary-closure2
primary_closure3=$tmpdir/primary-closure3
primary_closure4=$tmpdir/primary-closure4
primary_closure5=$tmpdir/primary-closure5
primary_closure6=$tmpdir/primary-closure6

fail() {
    echo "HATA: G8g layout gate: $*" >&2
    exit 1
}

LC_ALL=C "$objdump" -f "$kernel" > "$format"
grep -Fq 'file format elf64-littleaarch64' "$format" || \
    fail 'girdi little-endian AArch64 ELF değil'
grep -Eq '^architecture:[[:space:]]+aarch64$' "$format" || \
    fail 'girdi AArch64 makine kodu taşımıyor'
LC_ALL=C "$objdump" -t "$kernel" > "$symbols"

instruction_count() {
    body=$1
    pattern=$2
    grep -Ec "$pattern" "$body" || true
}

validate_disassembly_size() {
    body=$1
    size_hex=$2
    description=$3
    expected_bytes=$(printf '%d' "0x$size_hex")
    instructions=$(grep -Ec '^[[:space:]]*[[:xdigit:]]+:[[:space:]]+[[:alnum:].]+' "$body" || true)
    observed_bytes=$((instructions * 4))
    [ "$observed_bytes" -eq "$expected_bytes" ] || \
        fail "$description symbol size/disassembly sınırı uyuşmuyor (symbol=$expected_bytes disassembly=$observed_bytes)"
}

extract_global_exact() {
    symbol=$1
    expected_size=$2
    output=$3
    if ! awk -v wanted="$symbol" -v size="$expected_size" '
        $2 == "g" && $3 == "F" && $4 == ".text" &&
            $NF == wanted && $5 == size { valid++ }
        END { exit(valid == 1 ? 0 : 1) }
    ' "$symbols"; then
        fail "global .text symbol/size exact değil: $symbol size=$expected_size"
    fi
    LC_ALL=C "$objdump" -d --no-show-raw-insn \
        --disassemble-symbols="$symbol" "$kernel" > "$output" || \
        fail "function-bounded disassembly üretilemedi: $symbol"
    headers=$(grep -Ec "^[[:xdigit:]]+ <$symbol>:$" "$output" || true)
    [ "$headers" -eq 1 ] || fail "fonksiyon sınırı exact-once değil: $symbol"
    validate_disassembly_size "$output" "$expected_size" "$symbol"
}

extract_local_exact() {
    suffix=$1
    expected_size=$2
    output=$3
    matches=$(awk -v wanted="$suffix" -v size="$expected_size" '
        $2 == "l" && $3 == "F" && $4 == ".text" &&
            $NF ~ wanted && $5 == size { print $NF }
    ' "$symbols")
    count=$(printf '%s\n' "$matches" | grep -c . || true)
    [ "$count" -eq 1 ] || \
        fail "local .text symbol/size suffix exact değil: $suffix size=$expected_size"
    local_symbol=$matches
    LC_ALL=C "$objdump" -d --no-show-raw-insn \
        --disassemble-symbols="$local_symbol" "$kernel" > "$output" || \
        fail "local function-bounded disassembly üretilemedi: $local_symbol"
    headers=$(grep -Ec "^[[:xdigit:]]+ <$local_symbol>:$" "$output" || true)
    [ "$headers" -eq 1 ] || fail "local fonksiyon sınırı exact-once değil: $local_symbol"
    validate_disassembly_size "$output" "$expected_size" "$local_symbol"
    printf '%s\n' "$local_symbol"
}

require_contract() {
    body=$1
    contract=$2
    description=$3
    grep -Eq "$contract" "$body" || fail "$description"
}

call_count() {
    body=$1
    callee=$2
    grep -Ec \
        "[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<$callee>$" \
        "$body" || true
}

call_line() {
    body=$1
    callee=$2
    grep -nE \
        "[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<$callee>$" \
        "$body" | sed -n '1s/:.*//p'
}

nth_call_line() {
    body=$1
    callee=$2
    index=$3
    grep -nE \
        "[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<$callee>$" \
        "$body" | sed -n "${index}s/:.*//p"
}

pattern_line() {
    body=$1
    pattern=$2
    grep -nE "$pattern" "$body" | sed -n '1s/:.*//p'
}

nth_pattern_line() {
    body=$1
    pattern=$2
    index=$3
    grep -nE "$pattern" "$body" | sed -n "${index}s/:.*//p"
}

last_pattern_line() {
    body=$1
    pattern=$2
    grep -nE "$pattern" "$body" | sed -n '$s/:.*//p'
}

first_pattern_after() {
    body=$1
    pattern=$2
    minimum=$3
    grep -nE "$pattern" "$body" | awk -F: -v minimum="$minimum" '
        $1 > minimum { print $1; exit }
    '
}

last_pattern_before() {
    body=$1
    pattern=$2
    maximum=$3
    grep -nE "$pattern" "$body" | awk -F: -v maximum="$maximum" '
        $1 < maximum { line = $1 }
        END { if (line != 0) print line }
    '
}

require_order() {
    description=$1
    shift
    previous=0
    for line in "$@"; do
        [ -n "$line" ] || fail "$description için sıra öğesi bulunamadı"
        [ "$line" -gt "$previous" ] || fail "$description sırası bozuk"
        previous=$line
    done
}

address_at_line() {
    body=$1
    line=$2
    sed -n "${line}s/^[[:space:]]*\([[:xdigit:]]*\):.*/\1/p" "$body"
}

line_at_address() {
    body=$1
    address=$2
    grep -nE "^[[:space:]]*$address:[[:space:]]" "$body" | sed -n '1s/:.*//p'
}

next_instruction_line() {
    body=$1
    minimum=$2
    awk -v minimum="$minimum" '
        NR > minimum && /^[[:space:]]*[[:xdigit:]]+:[[:space:]]/ { print NR; exit }
    ' "$body"
}

require_line_contract() {
    body=$1
    line=$2
    contract=$3
    description=$4
    [ -n "$line" ] || fail "$description için instruction bulunamadı"
    sed -n "${line}p" "$body" | grep -Eq "$contract" || fail "$description"
}

instruction_count_between() {
    body=$1
    start=$2
    stop=$3
    awk -v start="$start" -v stop="$stop" '
        NR > start && NR < stop && /^[[:space:]]*[[:xdigit:]]+:[[:space:]]/ { count++ }
        END { print count + 0 }
    ' "$body"
}

branch_target_at_line() {
    body=$1
    line=$2
    sed -nE "${line}s/^.*[[:space:]](b|b[.][a-z]+|cbz|cbnz|tbz|tbnz)[[:space:]]+([^,]+,[[:space:]]+)*((0x)?[[:xdigit:]]+)[[:space:]]+<.*$/\3/p" \
        "$body" | sed 's/^0x//'
}

indirect_cf_pattern='[[:space:]](br|blr|br(aa|ab)z?|blr(aa|ab)z?|retaa|retab|eretaa|eretab)([[:space:]]|$)|[[:space:]]ret[[:space:]]+x[0-9]+'
direct_cf_target_pattern='[[:space:]](b([.][a-z0-9]+)?|bc[.][a-z0-9]+|bl|cbz|cbnz|tbz|tbnz)[[:space:]]+([^,]+,[[:space:]]+)*((0x)?[[:xdigit:]]+)[[:space:]]+<[^>]+>$'
panic_cf_pattern='[[:space:]](b([.][a-z0-9]+)?|bc[.][a-z0-9]+|bl|cbz|cbnz|tbz|tbnz)[[:space:]]+([^,]+,[[:space:]]+)*((0x)?[[:xdigit:]]+)[[:space:]]+<[^>]*(panic|unwrap|overflow)[^>]*>$'
fp_surface_pattern='(^|[[:space:],\[])([qvsdbhzp][0-9]+|pn[0-9]+|za([0-9]+[hv]?)?|zt[0-9]+|ffr)([.]|/|\[|\]|,|[[:space:]]|$)|[[:space:]](FPCR|FPSR)([[:space:],]|$)'

require_no_indirect() {
    body=$1
    description=$2
    indirect=$(grep -E "$indirect_cf_pattern" "$body" || true)
    [ -z "$indirect" ] || \
        fail "$description incelenemeyen indirect/PAC control-flow içeriyor: $indirect"
}

require_no_panic_edge() {
    body=$1
    description=$2
    bad=$(grep -E "$panic_cf_pattern" "$body" || true)
    [ -z "$bad" ] || fail "$description panic/unwrap/overflow edge içeriyor: $bad"
}

require_no_return_surface() {
    body=$1
    description=$2
    unexpected=$(grep -E \
        '^[[:space:]]*[[:xdigit:]]+:[[:space:]]+(ret|retaa|retab|eret|eretaa|eretab|wfi)([[:space:]]|$)' \
        "$body" || true)
    [ -z "$unexpected" ] || \
        fail "$description beklenmeyen return/exception-return/WFI yüzeyi içeriyor: $unexpected"
}

require_terminal_wfe_loop() {
    body=$1
    anchor=$2
    description=$3
    terminal_wfe=$(next_instruction_line "$body" "$anchor")
    require_line_contract "$body" "$terminal_wfe" \
        '[[:space:]]wfe([[:space:]]|$)' \
        "$description doğrudan terminal WFE'ye düşmüyor"
    terminal_loop=$(next_instruction_line "$body" "$terminal_wfe")
    require_line_contract "$body" "$terminal_loop" \
        '[[:space:]]b[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<[^>]+>$' \
        "$description terminal WFE sonrasında doğrudan plain branch taşımıyor"
    [ "$(branch_target_at_line "$body" "$terminal_loop")" = \
        "$(address_at_line "$body" "$terminal_wfe")" ] || \
        fail "$description terminal branchi aynı WFE instructionına dönmüyor"
}

require_msr_surface() {
    body=$1
    expected=$2
    allowlist=$3
    description=$4
    observed=$(instruction_count "$body" '[[:space:]]msr[[:space:]]')
    [ "$observed" -eq "$expected" ] || \
        fail "$description MSR sayısı exact değil (expected=$expected observed=$observed)"
    unexpected=$(grep -E '[[:space:]]msr[[:space:]]' "$body" | \
        grep -Ev "$allowlist" || true)
    [ -z "$unexpected" ] || \
        fail "$description allowlist dışı system-register write içeriyor: $unexpected"
}

# Keep the security-sensitive parsers mutation-sensitive independently of the
# current production ELF. These fixtures exercise conditional panic edges,
# pointer-authenticated indirect control-flow, scalar/NEON/SVE/SME registers,
# and FP status-register access.
parser_fixture=$tmpdir/parser-fixture
printf '%s\n' \
    '  100: b.eq 0x200 <panic_conditional>' \
    '  104: cbz w0, 0x200 <unwrap_conditional>' \
    '  108: tbnz w0, #0x0, 0x200 <overflow_conditional>' \
    '  10a: b.eq 0x300 <scheduler_tick>' \
    '  10b: cbnz w1, 0x304 <uart_write>' \
    '  10c: braa x0, x1' \
    '  110: blrabz x2' \
    '  114: retaa' \
    '  118: ret x19' \
    '  11c: movi v0.16b, #0' \
    '  120: fmov h0, w0' \
    '  124: ptrue p0.b' \
    '  128: add z0.d, z1.d, z2.d' \
    '  12c: zero za' \
    '  130: mrs x0, FPCR' > "$parser_fixture"
[ "$(grep -Ec "$panic_cf_pattern" "$parser_fixture" || true)" -eq 3 ] || \
    fail 'conditional panic/unwrap/overflow parser self-test RED'
[ "$(grep -Ec "$direct_cf_target_pattern" "$parser_fixture" || true)" -eq 5 ] || \
    fail 'conditional forbidden-target parser self-test RED'
[ "$(grep -Ec "$indirect_cf_pattern" "$parser_fixture" || true)" -eq 4 ] || \
    fail 'indirect/PAC control-flow parser self-test RED'
[ "$(grep -Ec "$fp_surface_pattern" "$parser_fixture" || true)" -eq 6 ] || \
    fail 'FP/SIMD/SVE/SME parser self-test RED'

# Sequence 97 versions the Sequence 86 G8g layout after the only authorized
# downstream consumer (G8h) makes the immutable prerequisite and two terminal
# continuation seams live.  No other G8g production symbol growth is accepted.
actual_g8g_globals=$(awk '
    $2 == "g" && $3 == "F" && $4 == ".text" && $NF ~ /^rpi5_g8g/ { print $NF }
' "$symbols" | LC_ALL=C sort)
expected_g8g_globals=$(printf '%s\n' \
    rpi5_g8g_prerequisite_complete \
    rpi5_g8g_primary_run \
    rpi5_g8g_read_secondary_ppi_state \
    rpi5_g8g_secondary_irq_active \
    rpi5_g8g_secondary_released \
    rpi5_g8g_secondary_run \
    rpi5_g8g_try_handle_secondary_irq | LC_ALL=C sort)
[ "$actual_g8g_globals" = "$expected_g8g_globals" ] || \
    fail "global G8g symbol yüzeyi exact değil: $actual_g8g_globals"

ticks_symbol=$(awk '
    $2 == "l" && $3 == "O" && $4 == ".bss" &&
        $5 == "0000000000000008" && $NF ~ /exceptions5TICKS$/ { print $NF }
' "$symbols")
[ "$(printf '%s\n' "$ticks_symbol" | grep -c . || true)" -eq 1 ] || \
    fail 'CPU0 compatibility TICKS object/size exact değil'

extract_global_exact rpi5_g8g_read_secondary_ppi_state 00000000000000a4 "$ppi"
extract_global_exact rpi5_g8g_secondary_released 0000000000000058 "$released"
extract_global_exact rpi5_g8g_secondary_irq_active 0000000000000034 "$active"
extract_global_exact rpi5_g8g_secondary_run 0000000000000530 "$secondary"
extract_global_exact rpi5_g8g_try_handle_secondary_irq 00000000000007b8 "$handler"
extract_global_exact rpi5_g8g_primary_run 0000000000000f1c "$primary"
extract_global_exact rpi5_g8g_prerequisite_complete 00000000000000a0 "$prerequisite_complete"
extract_global_exact rpi5_g8f_secondary_run 000000000000035c "$g8f_secondary"
extract_global_exact rpi5_g8f_primary_run 0000000000000714 "$g8f_primary"
extract_global_exact rust_irq_handler 0000000000000270 "$irq_dispatch"

snapshot_symbol=$(extract_local_exact \
    'timerNtB2_19PerCpuPeriodicTimer8snapshot[.]llvm[.][0-9]+$' \
    00000000000001d8 "$timer_snapshot")
prepare_symbol=$(extract_local_exact \
    'timer31rpi5_g8g_prepare_local_periodic$' \
    0000000000000208 "$timer_prepare")
advance_symbol=$(extract_local_exact \
    'timer31rpi5_g8g_advance_local_periodic$' \
    00000000000001d4 "$timer_advance")
disable_symbol=$(extract_local_exact \
    'timer28rpi5_g8g_disable_local_timer$' \
    0000000000000184 "$timer_disable")
secondary_fail_symbol=$(extract_local_exact \
    'kernel8rpi5_g8g14secondary_fail$' \
    00000000000000bc "$secondary_fail")
consume_error_symbol=$(extract_local_exact \
    'kernel8rpi5_g8g17consume_irq_error$' \
    00000000000000e4 "$consume_error")
publish_error_symbol=$(extract_local_exact \
    'kernel8rpi5_g8g23publish_secondary_error$' \
    00000000000000b8 "$publish_error")
primary_fail_symbol=$(extract_local_exact \
    'kernel8rpi5_g8g12primary_fail$' \
    0000000000000058 "$primary_fail")
error_name_symbol=$(extract_local_exact \
    'kernel8rpi5_g8g10error_name$' \
    0000000000000038 "$error_name")
continue_to_g8h_symbol=$(extract_local_exact \
    'kernel8rpi5_g8g15continue_to_g8h$' \
    000000000000001c "$continue_to_g8h")
primary_require_symbol=$(extract_local_exact \
    'kernel8rpi5_g8g15primary_require$' \
    000000000000001c "$primary_require")
primary_closure0_symbol=$(extract_local_exact \
    'kernel8rpi5_g8g20rpi5_g8g_primary_run0B5_$' \
    0000000000000018 "$primary_closure0")
primary_closure1_symbol=$(extract_local_exact \
    'kernel8rpi5_g8g20rpi5_g8g_primary_runs1_0B5_$' \
    0000000000000018 "$primary_closure1")
primary_closure2_symbol=$(extract_local_exact \
    'kernel8rpi5_g8g20rpi5_g8g_primary_runs2_0B5_$' \
    0000000000000018 "$primary_closure2")
primary_closure3_symbol=$(extract_local_exact \
    'kernel8rpi5_g8g20rpi5_g8g_primary_runs3_0B5_$' \
    0000000000000018 "$primary_closure3")
primary_closure4_symbol=$(extract_local_exact \
    'kernel8rpi5_g8g20rpi5_g8g_primary_runs4_0B5_$' \
    0000000000000018 "$primary_closure4")
primary_closure5_symbol=$(extract_local_exact \
    'kernel8rpi5_g8g20rpi5_g8g_primary_runs5_0B5_$' \
    0000000000000018 "$primary_closure5")
primary_closure6_symbol=$(extract_local_exact \
    'kernel8rpi5_g8g20rpi5_g8g_primary_runs_0B5_$' \
    0000000000000018 "$primary_closure6")

# Sequence 97 makes the previously dead G8g completion predicate and the two
# G8h continuation helpers live. Freeze their bounded machine-code surfaces.
[ "$(instruction_count "$prerequisite_complete" 'ldar(b)?[[:space:]]+[wx][0-9]+, \[x[0-9]+\]$')" -eq 8 ] || \
    fail 'G8g prerequisite exact sekiz Acquire evidence loadu taşımıyor'
[ "$(instruction_count "$prerequisite_complete" '[[:space:]]bl[[:space:]]')" -eq 0 ] || \
    fail 'G8g prerequisite beklenmeyen direct call içeriyor'
[ "$(instruction_count "$prerequisite_complete" '[[:space:]](str|stur|stp|stlr|stxr|stlxr)[b]?[[:space:]]')" -eq 0 ] || \
    fail 'G8g prerequisite read-only değil'
require_contract "$prerequisite_complete" 'cmp[[:space:]]+x[0-9]+, #0x4' \
    'G8g prerequisite PARKED stage 4 kontrolü taşımıyor'
[ "$(instruction_count "$prerequisite_complete" 'cmp[[:space:]]+x[0-9]+, #0x2')" -eq 4 ] || \
    fail 'G8g prerequisite dört exact count==2 kontrolü taşımıyor'
[ "$(instruction_count "$prerequisite_complete" '[[:space:]]ret([[:space:]]|$)')" -eq 2 ] || \
    fail 'G8g prerequisite bool return yüzeyi exact iki değil'

[ "$(call_count "$continue_to_g8h" rpi5_g8h_secondary_released)" -eq 2 ] || \
    fail 'G8g CPU1 continuation exact iki peeled G8h release pollu taşımıyor'
[ "$(call_count "$continue_to_g8h" rpi5_g8h_secondary_run)" -eq 1 ] || \
    fail 'G8g CPU1 continuation exact bir direct G8h runtime edge taşımıyor'
[ "$(instruction_count "$continue_to_g8h" '[[:space:]]wfe([[:space:]]|$)')" -eq 1 ] || \
    fail 'G8g CPU1 continuation exact bir bounded WFE pollu taşımıyor'
[ "$(instruction_count "$continue_to_g8h" '[[:space:]]bl[[:space:]]')" -eq 3 ] || \
    fail 'G8g CPU1 continuation direct-call yüzeyi exact üç değil'
continue_first_poll=$(nth_call_line "$continue_to_g8h" rpi5_g8h_secondary_released 1)
continue_fast_branch=$(next_instruction_line "$continue_to_g8h" "$continue_first_poll")
continue_wfe=$(first_pattern_after "$continue_to_g8h" '[[:space:]]wfe([[:space:]]|$)' "$continue_fast_branch")
continue_second_poll=$(nth_call_line "$continue_to_g8h" rpi5_g8h_secondary_released 2)
continue_loopback=$(next_instruction_line "$continue_to_g8h" "$continue_second_poll")
continue_run=$(call_line "$continue_to_g8h" rpi5_g8h_secondary_run)
require_order 'G8g CPU1 peeled release/WFE/G8h continuation' \
    "$continue_first_poll" "$continue_fast_branch" "$continue_wfe" \
    "$continue_second_poll" "$continue_loopback" "$continue_run"
require_line_contract "$continue_to_g8h" "$continue_fast_branch" \
    '[[:space:]]tbnz[[:space:]]+w0, #0x0,' \
    'G8g CPU1 release fast-path sonucu doğrudan tüketilmiyor'
require_line_contract "$continue_to_g8h" "$continue_loopback" \
    '[[:space:]]tbz[[:space:]]+w0, #0x0,' \
    'G8g CPU1 release WFE-loop sonucu doğrudan tüketilmiyor'
require_no_return_surface "$continue_to_g8h" 'G8g CPU1 G8h continuation'

[ "$(instruction_count "$primary_require" '[[:space:]]tbz[[:space:]]+w0, #0x0,')" -eq 1 ] || \
    fail 'G8g primary_require condition-false edge exact değil'
[ "$(instruction_count "$primary_require" '[[:space:]]ret([[:space:]]|$)')" -eq 1 ] || \
    fail 'G8g primary_require condition-true return exact değil'

# G8f -> G8g continuation seams are direct and ordered. LLVM peels the release
# loop into an initial poll and one loop poll, so the production CFG contains
# two predicate BL sites. Each conditional branch is tied to its immediately
# preceding call and both fallthrough edges are proven below.
[ "$(call_count "$g8f_primary" rpi5_g8g_primary_run)" -eq 1 ] || \
    fail 'G8f -> G8g CPU0 seam exact bir direct BL değil'
g8g_primary_call=$(call_line "$g8f_primary" rpi5_g8g_primary_run)
g8f_last_uart=$(last_pattern_before "$g8f_primary" \
    '[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<[^>]*uart[^>]*write_fmt[^>]*>$' \
    "$g8g_primary_call")
require_order 'BOOT8F final UART/G8g CPU0 tail handoff' \
    "$g8f_last_uart" "$g8g_primary_call"

release_calls=$(call_count "$g8f_secondary" rpi5_g8g_secondary_released)
[ "$release_calls" -eq 2 ] || \
    fail "G8f CPU1 peeled release predicate direct BL sayısı exact iki değil: $release_calls"
[ "$(call_count "$g8f_secondary" rpi5_g8g_secondary_run)" -eq 1 ] || \
    fail 'G8f -> G8g CPU1 run seam exact bir direct BL değil'
release_first=$(nth_call_line "$g8f_secondary" rpi5_g8g_secondary_released 1)
release_second=$(nth_call_line "$g8f_secondary" rpi5_g8g_secondary_released 2)
g8g_secondary_call=$(call_line "$g8f_secondary" rpi5_g8g_secondary_run)
release_first_branch=$(next_instruction_line "$g8f_secondary" "$release_first")
require_line_contract "$g8f_secondary" "$release_first_branch" \
    '[[:space:]]tbnz[[:space:]]+w0, #0x0, (0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8f_secondary_run[+]0x[[:xdigit:]]+>$' \
    'G8f ilk release predicate BL hemen ardından true tbnz taşımıyor'
release_wfe=$(next_instruction_line "$g8f_secondary" "$release_first_branch")
require_line_contract "$g8f_secondary" "$release_wfe" \
    '[[:space:]]wfe([[:space:]]|$)' \
    'G8f ilk release false fallthrough doğrudan WFE değil'
release_second_fallthrough=$(next_instruction_line "$g8f_secondary" "$release_wfe")
[ "$release_second_fallthrough" = "$release_second" ] || \
    fail 'G8f WFE fallthrough doğrudan ikinci release predicate BL değil'
release_second_branch=$(next_instruction_line "$g8f_secondary" "$release_second")
require_line_contract "$g8f_secondary" "$release_second_branch" \
    '[[:space:]]tbz[[:space:]]+w0, #0x0, (0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8f_secondary_run[+]0x[[:xdigit:]]+>$' \
    'G8f ikinci release predicate BL hemen ardından false tbz taşımıyor'
release_second_true=$(next_instruction_line "$g8f_secondary" "$release_second_branch")
[ "$release_second_true" = "$g8g_secondary_call" ] || \
    fail 'G8f ikinci release true fallthrough doğrudan G8g CPU1 run BL değil'
require_order 'G8f CPU1 release-poll/WFE/G8g run' \
    "$release_first" "$release_first_branch" "$release_wfe" \
    "$release_second" "$release_second_branch" "$g8g_secondary_call"
run_address=$(address_at_line "$g8f_secondary" "$g8g_secondary_call")
[ "$(branch_target_at_line "$g8f_secondary" "$release_first_branch")" = "$run_address" ] || \
    fail 'G8f ilk release-poll true branch doğrudan G8g CPU1 run seamine gitmiyor'
[ "$(branch_target_at_line "$g8f_secondary" "$release_second_branch")" = \
    "$(address_at_line "$g8f_secondary" "$release_wfe")" ] || \
    fail 'peeled release-poll false branch doğrudan WFE loopuna dönmüyor'
require_no_indirect "$g8f_primary" 'G8f CPU0 seam'
require_no_indirect "$g8f_secondary" 'G8f CPU1 seam'

# IRQ dispatch order is proven only through anchored direct BL instructions.
# Historical generic timer overflow panics below this seam are outside G8g.
for interceptor in \
    rpi5_g8g_try_handle_secondary_irq \
    rpi5_g8e_try_handle_secondary_irq \
    rpi5_g8d_try_handle_secondary_irq \
    rpi5_g8b_try_handle_secondary_irq; do
    [ "$(call_count "$irq_dispatch" "$interceptor")" -eq 1 ] || \
        fail "IRQ interceptor exact bir direct BL değil: $interceptor"
done
irq_g8g=$(call_line "$irq_dispatch" rpi5_g8g_try_handle_secondary_irq)
irq_g8e=$(call_line "$irq_dispatch" rpi5_g8e_try_handle_secondary_irq)
irq_g8d=$(call_line "$irq_dispatch" rpi5_g8d_try_handle_secondary_irq)
irq_g8b=$(call_line "$irq_dispatch" rpi5_g8b_try_handle_secondary_irq)
generic_timer=$(first_pattern_after "$irq_dispatch" \
    'cmp[[:space:]]+w[0-9]+, #0x1b' "$irq_g8b")
require_order 'IRQ dispatch G8g/G8e/G8d/G8b/generic' \
    "$irq_g8g" "$irq_g8e" "$irq_g8d" "$irq_g8b" "$generic_timer"
handled_target=
for interceptor_line in "$irq_g8g" "$irq_g8e" "$irq_g8d" "$irq_g8b"; do
    if [ "$interceptor_line" = "$irq_g8g" ]; then
        next_dispatch_bound=$irq_g8e
        expected_fallthrough_instructions=3
    elif [ "$interceptor_line" = "$irq_g8e" ]; then
        next_dispatch_bound=$irq_g8d
        expected_fallthrough_instructions=3
    elif [ "$interceptor_line" = "$irq_g8d" ]; then
        next_dispatch_bound=$irq_g8b
        expected_fallthrough_instructions=3
    else
        next_dispatch_bound=$generic_timer
        expected_fallthrough_instructions=0
    fi
    handled_branch=$(next_instruction_line "$irq_dispatch" "$interceptor_line")
    require_line_contract "$irq_dispatch" "$handled_branch" \
        '[[:space:]]tbnz[[:space:]]+w0, #0x0, (0x)?[[:xdigit:]]+[[:space:]]+<rust_irq_handler[+]0x[[:xdigit:]]+>$' \
        'IRQ interceptor direct BL hemen ardından handled tbnz taşımıyor'
    [ "$handled_branch" -lt "$next_dispatch_bound" ] || \
        fail 'IRQ interceptor handled branchi kendi bounded segmentinde değil'
    segment_handled_branches=$(awk -v start="$interceptor_line" -v stop="$next_dispatch_bound" '
        NR > start && NR < stop && /tbnz[[:space:]]+w0, #0x0,/ { count++ }
        END { print count + 0 }
    ' "$irq_dispatch")
    [ "$segment_handled_branches" -eq 1 ] || \
        fail "IRQ interceptor segmenti exact bir handled branch taşımıyor: $segment_handled_branches"
    fallthrough_instructions=$(instruction_count_between \
        "$irq_dispatch" "$handled_branch" "$next_dispatch_bound")
    [ "$fallthrough_instructions" -eq "$expected_fallthrough_instructions" ] || \
        fail "IRQ interceptor false fallthrough instruction sayısı exact değil: $fallthrough_instructions"
    unexpected_fallthrough_cf=$(awk -v start="$handled_branch" -v stop="$next_dispatch_bound" '
        NR > start && NR < stop && /[[:space:]](b([.][a-z]+)?|cbz|cbnz|tbz|tbnz|bl|blr|br|ret)[[:space:]]/ { print }
    ' "$irq_dispatch")
    [ -z "$unexpected_fallthrough_cf" ] || \
        fail "IRQ interceptor false fallthrough ek control-flow içeriyor: $unexpected_fallthrough_cf"
    target=$(branch_target_at_line "$irq_dispatch" "$handled_branch")
    if [ -z "$handled_target" ]; then
        handled_target=$target
    else
        [ "$target" = "$handled_target" ] || \
            fail 'IRQ interceptors ortak handled-return epilogue kullanmıyor'
    fi
done
handled_epilogue=$(line_at_address "$irq_dispatch" "$handled_target")
require_line_contract "$irq_dispatch" "$handled_epilogue" \
    '[[:space:]]mov[[:space:]]+x0, x19([[:space:]]|$)' \
    'IRQ handled hedefi gerçek ortak return epilogu başlangıcı değil'
handled_epilogue_2=$(next_instruction_line "$irq_dispatch" "$handled_epilogue")
require_line_contract "$irq_dispatch" "$handled_epilogue_2" \
    '[[:space:]]ldp[[:space:]]+x20, x19, \[sp, #0x90\]' \
    'IRQ handled epilogu x20/x19 restore etmiyor'
handled_epilogue_3=$(next_instruction_line "$irq_dispatch" "$handled_epilogue_2")
require_line_contract "$irq_dispatch" "$handled_epilogue_3" \
    '[[:space:]]ldp[[:space:]]+x22, x21, \[sp, #0x80\]' \
    'IRQ handled epilogu x22/x21 restore etmiyor'
handled_epilogue_4=$(next_instruction_line "$irq_dispatch" "$handled_epilogue_3")
require_line_contract "$irq_dispatch" "$handled_epilogue_4" \
    '[[:space:]]ldr[[:space:]]+x30, \[sp, #0x60\]' \
    'IRQ handled epilogu link register restore etmiyor'
handled_epilogue_5=$(next_instruction_line "$irq_dispatch" "$handled_epilogue_4")
require_line_contract "$irq_dispatch" "$handled_epilogue_5" \
    '[[:space:]]ldp[[:space:]]+x24, x23, \[sp, #0x70\]' \
    'IRQ handled epilogu x24/x23 restore etmiyor'
handled_epilogue_6=$(next_instruction_line "$irq_dispatch" "$handled_epilogue_5")
require_line_contract "$irq_dispatch" "$handled_epilogue_6" \
    '[[:space:]]add[[:space:]]+sp, sp, #0xa0' \
    'IRQ handled epilogu stack framei kapatmıyor'
handled_epilogue_ret=$(next_instruction_line "$irq_dispatch" "$handled_epilogue_6")
require_line_contract "$irq_dispatch" "$handled_epilogue_ret" \
    '[[:space:]]ret([[:space:]]|$)' \
    'IRQ handled hedefi return ile bitmiyor'

# The active predicate is a read-only CPU1+ownership leaf, and the release
# predicate consumes BOOT8F before three Acquire observations.
[ "$(call_count "$handler" rpi5_g8g_secondary_irq_active)" -eq 1 ] || \
    fail 'G8g handler active predicate exact bir direct BL değil'
active_call=$(call_line "$handler" rpi5_g8g_secondary_irq_active)
handler_inactive_branch=$(next_instruction_line "$handler" "$active_call")
require_line_contract "$handler" "$handler_inactive_branch" \
    '[[:space:]]tbz[[:space:]]+w0, #0x0, (0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_try_handle_secondary_irq[+]0x[[:xdigit:]]+>$' \
    'handler active predicate BL hemen ardından inactive tbz taşımıyor'
handler_epilogue_address=$(branch_target_at_line "$handler" "$handler_inactive_branch")
handler_epilogue=$(line_at_address "$handler" "$handler_epilogue_address")
require_line_contract "$handler" "$handler_epilogue" \
    '[[:space:]]ldp[[:space:]]+x20, x19, \[sp, #0x80\]' \
    'handler inactive=false branchi gerçek bounded epiloga gitmiyor'
handler_epilogue_bool=$(next_instruction_line "$handler" "$handler_epilogue")
require_line_contract "$handler" "$handler_epilogue_bool" \
    '[[:space:]]and[[:space:]]+w0, w0, #0x1' \
    'handler epilogu bool dönüşünü fail-closed normalize etmiyor'
handler_true_base=$(next_instruction_line "$handler" "$handler_inactive_branch")
require_line_contract "$handler" "$handler_true_base" \
    '[[:space:]]adrp[[:space:]]+x23,' \
    'handler active=true fallthrough STAGE base adresini çözmüyor'
handler_true_add=$(next_instruction_line "$handler" "$handler_true_base")
require_line_contract "$handler" "$handler_true_add" \
    '[[:space:]]add[[:space:]]+x23, x23, #0x3b0' \
    'handler active=true fallthrough STAGE adresini tamamlamıyor'
handler_stage=$(next_instruction_line "$handler" "$handler_true_add")
require_line_contract "$handler" "$handler_stage" \
    '[[:space:]]ldar[[:space:]]+x19, \[x23\]$' \
    'handler active=true fallthrough STAGE değerini Acquire okumuyor'
require_order 'active predicate/delegation/stage ownership' \
    "$active_call" "$handler_inactive_branch" "$handler_true_base" \
    "$handler_true_add" "$handler_stage"
for contract in \
    'mrs[[:space:]]+x[0-9]+, MPIDR_EL1' \
    'cmp[[:space:]]+x[0-9]+, #0x100' \
    'ldarb[[:space:]]+w[0-9]+, \[x[0-9]+\]' \
    '[[:space:]]ret([[:space:]]|$)'; do
    require_contract "$active" "$contract" "active predicate kanıtı eksik: $contract"
done
active_mpidr=$(pattern_line "$active" \
    'mrs[[:space:]]+x8, MPIDR_EL1')
active_aff_mask1=$(next_instruction_line "$active" "$active_mpidr")
require_line_contract "$active" "$active_aff_mask1" \
    '[[:space:]]and[[:space:]]+x8, x8, #0xffffffffff' \
    'active predicate MPIDR implemented affinity maskesini uygulamıyor'
active_aff_mask2=$(next_instruction_line "$active" "$active_aff_mask1")
require_line_contract "$active" "$active_aff_mask2" \
    '[[:space:]]and[[:space:]]+x8, x8, #0xffffffff00ffffff' \
    'active predicate Aff0 alanını fail-closed sıfırlamıyor'
active_cpu_cmp=$(next_instruction_line "$active" "$active_aff_mask2")
require_line_contract "$active" "$active_cpu_cmp" \
    '[[:space:]]cmp[[:space:]]+x8, #0x100' \
    'active predicate exact CPU1 MPIDR compareı yok'
active_cpu_false_branch=$(next_instruction_line "$active" "$active_cpu_cmp")
require_line_contract "$active" "$active_cpu_false_branch" \
    '[[:space:]]b[.]ne[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_secondary_irq_active[+]0x[[:xdigit:]]+>$' \
    'active predicate CPU1 mismatch koşulu b.ne değil'
active_owner_base=$(next_instruction_line "$active" "$active_cpu_false_branch")
require_line_contract "$active" "$active_owner_base" \
    '[[:space:]]adrp[[:space:]]+x8,' \
    'active predicate CPU1 true fallthrough ownership base çözmüyor'
active_owner_add=$(next_instruction_line "$active" "$active_owner_base")
require_line_contract "$active" "$active_owner_add" \
    '[[:space:]]add[[:space:]]+x8, x8, #0x3a8' \
    'active predicate ownership adresini exact tamamlamıyor'
active_owner_load=$(next_instruction_line "$active" "$active_owner_add")
require_line_contract "$active" "$active_owner_load" \
    '[[:space:]]ldarb[[:space:]]+w8, \[x8\]$' \
    'active predicate ownership bayrağını Acquire okumuyor'
active_owner_cmp=$(next_instruction_line "$active" "$active_owner_load")
require_line_contract "$active" "$active_owner_cmp" \
    '[[:space:]]cmp[[:space:]]+w8, #0x0' \
    'active predicate ownership false compareı yok'
active_owner_true=$(next_instruction_line "$active" "$active_owner_cmp")
require_line_contract "$active" "$active_owner_true" \
    '[[:space:]]cset[[:space:]]+w0, ne' \
    'active predicate yalnız ownership!=false için true üretmiyor'
active_true_ret=$(next_instruction_line "$active" "$active_owner_true")
require_line_contract "$active" "$active_true_ret" \
    '[[:space:]]ret([[:space:]]|$)' \
    'active predicate CPU1 ownership sonucu doğrudan dönmüyor'
active_false_address=$(branch_target_at_line "$active" "$active_cpu_false_branch")
active_false=$(line_at_address "$active" "$active_false_address")
require_line_contract "$active" "$active_false" \
    '[[:space:]]mov[[:space:]]+w0, wzr' \
    'active predicate CPU1 mismatch yolunda exact false üretmiyor'
active_false_ret=$(next_instruction_line "$active" "$active_false")
require_line_contract "$active" "$active_false_ret" \
    '[[:space:]]ret([[:space:]]|$)' \
    'active predicate CPU1 mismatch false yolunu doğrudan döndürmüyor'
active_cf_count=$(instruction_count "$active" \
    '[[:space:]](b([.][a-z]+)?|cbz|cbnz|tbz|tbnz|bl|blr|br|ret)([[:space:]]|$)')
[ "$active_cf_count" -eq 3 ] || \
    fail "active predicate control-flow yüzeyi exact üç değil: $active_cf_count"
if grep -Eq '[[:space:]](st[a-z0-9]*|bl|blr|br|dsb|sev|wfe|wfi|msr)[[:space:]]' "$active"; then
    fail 'active predicate mutation/call/barrier/event/sleep içeriyor'
fi
[ "$(call_count "$released" rpi5_g8f_prerequisite_complete)" -eq 1 ] || \
    fail 'G8g release predicate BOOT8F prerequisiteini exact bir direct BL ile tüketmiyor'
released_acquires=$(instruction_count "$released" \
    'ldar(b)?[[:space:]]+[wx][0-9]+, \[x[0-9]+\]')
[ "$released_acquires" -eq 3 ] || \
    fail "G8g release predicate exact üç Acquire gözlem taşımıyor: $released_acquires"
released_prereq_call=$(call_line "$released" rpi5_g8f_prerequisite_complete)
released_prereq_branch=$(next_instruction_line "$released" "$released_prereq_call")
require_line_contract "$released" "$released_prereq_branch" \
    '[[:space:]]tbz[[:space:]]+w0, #0x0, (0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_secondary_released[+]0x[[:xdigit:]]+>$' \
    'release predicate BOOT8F=false yolunu fail-closed dallandırmıyor'
released_flag_base=$(next_instruction_line "$released" "$released_prereq_branch")
require_line_contract "$released" "$released_flag_base" \
    '[[:space:]]adrp[[:space:]]+x8,' \
    'release predicate prerequisite true fallthrough RELEASED base çözmüyor'
released_flag_add=$(next_instruction_line "$released" "$released_flag_base")
require_line_contract "$released" "$released_flag_add" \
    '[[:space:]]add[[:space:]]+x8, x8, #0x3c8' \
    'release predicate RELEASED adresini exact tamamlamıyor'
released_flag_load=$(next_instruction_line "$released" "$released_flag_add")
require_line_contract "$released" "$released_flag_load" \
    '[[:space:]]ldarb[[:space:]]+w8, \[x8\]$' \
    'release predicate RELEASED bayrağını Acquire okumuyor'
released_flag_branch=$(next_instruction_line "$released" "$released_flag_load")
require_line_contract "$released" "$released_flag_branch" \
    '[[:space:]]cbz[[:space:]]+w8, (0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_secondary_released[+]0x[[:xdigit:]]+>$' \
    'release predicate RELEASED=false yolunu fail-closed dallandırmıyor'
released_capture_ref=$(first_pattern_after "$released" \
    'adr[[:space:]]+x8, (0x)?[[:xdigit:]]+[[:space:]]+<[^>]*CPU0_CAPTURE_COUNT[^>]*>$' \
    "$released_flag_branch")
released_capture_load=$(next_instruction_line "$released" "$released_capture_ref")
require_line_contract "$released" "$released_capture_load" \
    '[[:space:]]ldar[[:space:]]+x8, \[x8\]$' \
    'release predicate CPU0 captureı Acquire okumuyor'
released_capture_cmp=$(next_instruction_line "$released" "$released_capture_load")
require_line_contract "$released" "$released_capture_cmp" \
    '[[:space:]]cmn[[:space:]]+x8, #0x1' \
    'release predicate unpublished CPU0 capture sentinelini karşılaştırmıyor'
released_capture_branch=$(next_instruction_line "$released" "$released_capture_cmp")
require_line_contract "$released" "$released_capture_branch" \
    '[[:space:]]b[.]eq[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_secondary_released[+]0x[[:xdigit:]]+>$' \
    'release predicate unpublished CPU0 captureı fail-closed dallandırmıyor'
released_stage_base=$(next_instruction_line "$released" "$released_capture_branch")
require_line_contract "$released" "$released_stage_base" \
    '[[:space:]]adrp[[:space:]]+x8,' \
    'release predicate published capture fallthrough STAGE base çözmüyor'
released_stage_add=$(next_instruction_line "$released" "$released_stage_base")
require_line_contract "$released" "$released_stage_add" \
    '[[:space:]]add[[:space:]]+x8, x8, #0x3b0' \
    'release predicate STAGE adresini exact tamamlamıyor'
released_stage_load=$(next_instruction_line "$released" "$released_stage_add")
require_line_contract "$released" "$released_stage_load" \
    '[[:space:]]ldar[[:space:]]+x8, \[x8\]$' \
    'release predicate STAGE değerini Acquire okumuyor'
released_stage_cmp=$(next_instruction_line "$released" "$released_stage_load")
require_line_contract "$released" "$released_stage_cmp" \
    '[[:space:]]cmp[[:space:]]+x8, #0x0' \
    'release predicate yalnız IDLE stage kabul karşılaştırmasını taşımıyor'
released_true=$(next_instruction_line "$released" "$released_stage_cmp")
require_line_contract "$released" "$released_true" \
    '[[:space:]]cset[[:space:]]+w0, eq' \
    'release predicate yalnız STAGE_IDLE için true üretmiyor'
released_true_restore=$(next_instruction_line "$released" "$released_true")
require_line_contract "$released" "$released_true_restore" \
    '[[:space:]]ldr[[:space:]]+x30, \[sp\], #0x10' \
    'release predicate true yolu link registerı restore etmiyor'
released_true_ret=$(next_instruction_line "$released" "$released_true_restore")
require_line_contract "$released" "$released_true_ret" \
    '[[:space:]]ret([[:space:]]|$)' \
    'release predicate true yolu doğrudan dönmüyor'
released_false_address=$(branch_target_at_line "$released" "$released_prereq_branch")
[ "$(branch_target_at_line "$released" "$released_flag_branch")" = \
    "$released_false_address" ] && \
    [ "$(branch_target_at_line "$released" "$released_capture_branch")" = \
    "$released_false_address" ] || \
    fail 'release predicate üç prerequisite sapmasını ortak false epilogda birleştirmiyor'
released_false=$(line_at_address "$released" "$released_false_address")
require_line_contract "$released" "$released_false" \
    '[[:space:]]mov[[:space:]]+w0, wzr' \
    'release predicate prerequisite sapmalarında exact false üretmiyor'
released_false_restore=$(next_instruction_line "$released" "$released_false")
require_line_contract "$released" "$released_false_restore" \
    '[[:space:]]ldr[[:space:]]+x30, \[sp\], #0x10' \
    'release predicate false yolu link registerı restore etmiyor'
released_false_ret=$(next_instruction_line "$released" "$released_false_restore")
require_line_contract "$released" "$released_false_ret" \
    '[[:space:]]ret([[:space:]]|$)' \
    'release predicate false yolu doğrudan dönmüyor'
released_cf_count=$(instruction_count "$released" \
    '[[:space:]](b([.][a-z]+)?|cbz|cbnz|tbz|tbnz|bl|blr|br|ret)([[:space:]]|$)')
[ "$released_cf_count" -eq 6 ] || \
    fail "release predicate control-flow yüzeyi exact altı değil: $released_cf_count"
released_bad_store=$(grep -E \
    '[[:space:]](stp|str|stur|strb|strh|sturb|sturh|stlr|stlxr|stxr|swp|cas|ldadd)[[:space:]]' \
    "$released" | grep -Ev '\[sp(, #[^]]+)?\]!?$' || true)
[ -z "$released_bad_store" ] || \
    fail "G8g release predicate non-stack mutation içeriyor: $released_bad_store"
if grep -Eq '[[:space:]](blr|br|dsb|sev|wfe|wfi|msr)[[:space:]]' "$released"; then
    fail 'G8g release predicate beklenmeyen indirect/barrier/sleep içeriyor'
fi

# The PPI27 snapshot is read-only.  Every store belongs to the x8 Result/sret
# object; no GIC register store or panic-shift edge is permitted.
for contract in \
    'and[[:space:]]+w9, w0, #0xfffffff0' \
    'cmp[[:space:]]+w9, #0x10' \
    'b[.]ne[[:space:]]+(0x)?[[:xdigit:]]+' \
    'cmp[[:space:]]+w0, #0x20' \
    'b[.]hs[[:space:]]+(0x)?[[:xdigit:]]+' \
    'ldr[[:space:]]+w[0-9]+, \[x[0-9]+\]$' \
    'ldr[[:space:]]+w[0-9]+, \[x[0-9]+, #0x1000\]' \
    'ldr[[:space:]]+w[0-9]+, \[x[0-9]+, #0x100\]' \
    'ldr[[:space:]]+w[0-9]+, \[x[0-9]+, #0x200\]' \
    'ldr[[:space:]]+w[0-9]+, \[x[0-9]+, #0x300\]'; do
    require_contract "$ppi" "$contract" "read-only PPI snapshot kanıtı eksik: $contract"
done
ppi_lower_mask=$(pattern_line "$ppi" \
    'and[[:space:]]+w9, w0, #0xfffffff0')
ppi_lower_cmp=$(next_instruction_line "$ppi" "$ppi_lower_mask")
require_line_contract "$ppi" "$ppi_lower_cmp" \
    '[[:space:]]cmp[[:space:]]+w9, #0x10' \
    'PPI snapshot lower-bound compare maskeden hemen sonra değil'
ppi_lower_branch=$(next_instruction_line "$ppi" "$ppi_lower_cmp")
require_line_contract "$ppi" "$ppi_lower_branch" \
    '[[:space:]]b[.]ne[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_read_secondary_ppi_state[+]0x[[:xdigit:]]+>$' \
    'PPI snapshot SGI kimliklerini lower-bound error yoluna dallandırmıyor'
ppi_upper_cmp=$(pattern_line "$ppi" 'cmp[[:space:]]+w0, #0x20')
ppi_upper_branch=$(first_pattern_after "$ppi" \
    'b[.]hs[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_read_secondary_ppi_state[+]0x[[:xdigit:]]+>$' \
    "$ppi_upper_cmp")
[ -n "$ppi_upper_branch" ] && [ "$ppi_upper_branch" -le $((ppi_upper_cmp + 4)) ] || \
    fail 'PPI snapshot checked-shift upper-bound branchi compare ile bounded değil'
ppi_shift=$(first_pattern_after "$ppi" \
    'lsl[[:space:]]+w9, w9, w0' "$ppi_upper_cmp")
ppi_mask_select=$(next_instruction_line "$ppi" "$ppi_shift")
require_line_contract "$ppi" "$ppi_mask_select" \
    '[[:space:]]csel[[:space:]]+w10, w9, w10, lo' \
    'PPI snapshot checked-shift maskesini upper-bound sonucu ile seçmiyor'
[ "$(next_instruction_line "$ppi" "$ppi_mask_select")" = "$ppi_upper_branch" ] || \
    fail 'PPI snapshot checked-shift select doğrudan upper-bound error branchine geçmiyor'
ppi_gicd_base=$(next_instruction_line "$ppi" "$ppi_upper_branch")
require_line_contract "$ppi" "$ppi_gicd_base" \
    '[[:space:]]mov[[:space:]]+x11, #0x9000' \
    'PPI snapshot GICD base low halfwordu exact değil'
ppi_gicc_base=$(next_instruction_line "$ppi" "$ppi_gicd_base")
require_line_contract "$ppi" "$ppi_gicc_base" \
    '[[:space:]]mov[[:space:]]+x12, #0xa004' \
    'PPI snapshot GICC PMR base low halfwordu exact değil'
ppi_gicd_mid=$(next_instruction_line "$ppi" "$ppi_gicc_base")
require_line_contract "$ppi" "$ppi_gicd_mid" \
    '[[:space:]]movk[[:space:]]+x11, #0x7fff, lsl #16' \
    'PPI snapshot GICD base middle halfwordu exact değil'
ppi_gicc_mid=$(next_instruction_line "$ppi" "$ppi_gicd_mid")
require_line_contract "$ppi" "$ppi_gicc_mid" \
    '[[:space:]]movk[[:space:]]+x12, #0x7fff, lsl #16' \
    'PPI snapshot GICC base middle halfwordu exact değil'
ppi_gicd_high=$(next_instruction_line "$ppi" "$ppi_gicc_mid")
require_line_contract "$ppi" "$ppi_gicd_high" \
    '[[:space:]]movk[[:space:]]+x11, #0x10, lsl #32' \
    'PPI snapshot GICD base high halfwordu exact değil'
ppi_gicc_high=$(next_instruction_line "$ppi" "$ppi_gicd_high")
require_line_contract "$ppi" "$ppi_gicc_high" \
    '[[:space:]]movk[[:space:]]+x12, #0x10, lsl #32' \
    'PPI snapshot GICC base high halfwordu exact değil'
ppi_gicd_ctlr=$(next_instruction_line "$ppi" "$ppi_gicc_high")
require_line_contract "$ppi" "$ppi_gicd_ctlr" \
    '[[:space:]]ldr[[:space:]]+w13, \[x11\]$' \
    'PPI snapshot GICD_CTLR exact base readi yok'
ppi_gicc_ctlr=$(next_instruction_line "$ppi" "$ppi_gicd_ctlr")
require_line_contract "$ppi" "$ppi_gicc_ctlr" \
    '[[:space:]]ldr[[:space:]]+w14, \[x11, #0x1000\]' \
    'PPI snapshot GICC_CTLR exact base+0x1000 readi yok'
ppi_gicc_pmr=$(next_instruction_line "$ppi" "$ppi_gicc_ctlr")
require_line_contract "$ppi" "$ppi_gicc_pmr" \
    '[[:space:]]ldr[[:space:]]+w15, \[x12\]$' \
    'PPI snapshot GICC_PMR exact readi yok'
ppi_gicc_bpr=$(next_instruction_line "$ppi" "$ppi_gicc_pmr")
require_line_contract "$ppi" "$ppi_gicc_bpr" \
    '[[:space:]]ldr[[:space:]]+w12, \[x12, #0x4\]' \
    'PPI snapshot GICC_BPR exact readi yok'
ppi_enabled_read=$(next_instruction_line "$ppi" "$ppi_gicc_bpr")
require_line_contract "$ppi" "$ppi_enabled_read" \
    '[[:space:]]ldr[[:space:]]+w16, \[x11, #0x100\]' \
    'PPI snapshot GICD_ISENABLER exact readi yok'
ppi_pending_read=$(next_instruction_line "$ppi" "$ppi_enabled_read")
require_line_contract "$ppi" "$ppi_pending_read" \
    '[[:space:]]ldr[[:space:]]+w17, \[x11, #0x200\]' \
    'PPI snapshot GICD_ISPENDR exact readi yok'
ppi_active_read=$(next_instruction_line "$ppi" "$ppi_pending_read")
require_line_contract "$ppi" "$ppi_active_read" \
    '[[:space:]]ldr[[:space:]]+w11, \[x11, #0x300\]' \
    'PPI snapshot GICD_ISACTIVER exact readi yok'
[ "$(instruction_count "$ppi" \
    '[[:space:]]ldr[[:space:]]+w[0-9]+, \[x[0-9]+(, #[^]]+)?\]$')" -eq 7 ] || \
    fail 'PPI snapshot MMIO read yüzeyi exact yedi değil'
ppi_mask_enabled=$(first_pattern_after "$ppi" \
    'and[[:space:]]+w13, w16, w10' "$ppi_active_read")
ppi_mask_pending=$(next_instruction_line "$ppi" "$ppi_mask_enabled")
require_line_contract "$ppi" "$ppi_mask_pending" \
    '[[:space:]]and[[:space:]]+w12, w17, w10' \
    'PPI snapshot pending readbackını checked PPI maskesiyle filtrelemiyor'
ppi_mask_active=$(next_instruction_line "$ppi" "$ppi_mask_pending")
require_line_contract "$ppi" "$ppi_mask_active" \
    '[[:space:]]and[[:space:]]+w10, w11, w10' \
    'PPI snapshot active readbackını checked PPI maskesiyle filtrelemiyor'
[ "$(instruction_count "$ppi" \
    'and[[:space:]]+w(13|12|10), w(16|17|11), w10')" -eq 3 ] || \
    fail 'PPI snapshot enabled/pending/active checked-mask AND yüzeyi exact üç değil'

ppi_lower_fail_address=$(branch_target_at_line "$ppi" "$ppi_lower_branch")
ppi_lower_fail=$(line_at_address "$ppi" "$ppi_lower_fail_address")
require_line_contract "$ppi" "$ppi_lower_fail" \
    '[[:space:]]nop([[:space:]]|$)' \
    'PPI lower-bound sapması bounded Err literal yoluna gitmiyor'
ppi_lower_error_literal=$(next_instruction_line "$ppi" "$ppi_lower_fail")
require_line_contract "$ppi" "$ppi_lower_error_literal" \
    '[[:space:]]adr[[:space:]]+x9,' \
    'PPI lower-bound Err literal adresini çözmüyor'
ppi_lower_error_len=$(next_instruction_line "$ppi" "$ppi_lower_error_literal")
require_line_contract "$ppi" "$ppi_lower_error_len" \
    '[[:space:]]mov[[:space:]]+w10, #0x1a' \
    'PPI lower-bound Err literal uzunluğu exact değil'
ppi_lower_error_jump=$(next_instruction_line "$ppi" "$ppi_lower_error_len")
require_line_contract "$ppi" "$ppi_lower_error_jump" \
    '[[:space:]]b[[:space:]]+(0x)?[[:xdigit:]]+' \
    'PPI lower-bound Err yolu common sret bloğuna gitmiyor'
ppi_upper_fail_address=$(branch_target_at_line "$ppi" "$ppi_upper_branch")
ppi_upper_fail=$(line_at_address "$ppi" "$ppi_upper_fail_address")
require_line_contract "$ppi" "$ppi_upper_fail" \
    '[[:space:]]nop([[:space:]]|$)' \
    'PPI upper-bound sapması bounded checked-shift Err yoluna gitmiyor'
ppi_upper_error_literal=$(next_instruction_line "$ppi" "$ppi_upper_fail")
require_line_contract "$ppi" "$ppi_upper_error_literal" \
    '[[:space:]]adr[[:space:]]+x9,' \
    'PPI upper-bound Err literal adresini çözmüyor'
ppi_error_common=$(next_instruction_line "$ppi" "$ppi_upper_error_literal")
require_line_contract "$ppi" "$ppi_error_common" \
    '[[:space:]]stp[[:space:]]+x9, x10, \[x8, #0x8\]' \
    'PPI checked-shift Err common sret payloadı yok'
[ "$(branch_target_at_line "$ppi" "$ppi_lower_error_jump")" = \
    "$(address_at_line "$ppi" "$ppi_error_common")" ] || \
    fail 'PPI lower/upper bound sapmaları aynı checked Err sret bloğunda birleşmiyor'
ppi_error_tag=$(next_instruction_line "$ppi" "$ppi_error_common")
require_line_contract "$ppi" "$ppi_error_tag" \
    '[[:space:]]mov[[:space:]]+w9, #0x1' \
    'PPI Err sret discriminant değeri exact bir değil'
ppi_error_store=$(next_instruction_line "$ppi" "$ppi_error_tag")
require_line_contract "$ppi" "$ppi_error_store" \
    '[[:space:]]str[[:space:]]+w9, \[x8\]$' \
    'PPI Err sret discriminantı result objesine yazılmıyor'
ppi_error_ret=$(next_instruction_line "$ppi" "$ppi_error_store")
require_line_contract "$ppi" "$ppi_error_ret" \
    '[[:space:]]ret([[:space:]]|$)' \
    'PPI Err sret yolu doğrudan dönmüyor'
[ "$(instruction_count "$ppi" '[[:space:]]bl[[:space:]]')" -eq 0 ] || \
    fail 'read-only PPI snapshot direct call içeriyor'
ppi_stores=$(instruction_count "$ppi" \
    '[[:space:]](stp|str|stur|strb|strh|sturb|sturh)[[:space:]]')
[ "$ppi_stores" -eq 7 ] || fail "PPI sret store şekli değişti: $ppi_stores"
ppi_bad_store=$(grep -E \
    '[[:space:]](stp|str|stur|strb|strh|sturb|sturh)[[:space:]]' "$ppi" | \
    grep -Ev '\[x8(, #[^]]+)?\]$' || true)
[ -z "$ppi_bad_store" ] || fail "PPI snapshot x8 sret dışına store içeriyor: $ppi_bad_store"

# Timer helpers are leaf, CPU1-identity checked, checked-arithmetic paths.  The
# only register writes are the local virtual timer registers.
for timer_body in "$timer_snapshot" "$timer_prepare" "$timer_advance" "$timer_disable"; do
    require_no_indirect "$timer_body" 'G8g timer helper'
    require_no_panic_edge "$timer_body" 'G8g timer helper'
    if grep -Eq '[[:space:]]bl[[:space:]]' "$timer_body"; then
        fail "G8g timer helper leaf değil: $timer_body"
    fi
    if grep -Eq '[[:space:]](tlbi|smc|hvc)[[:space:]]' "$timer_body"; then
        fail "G8g timer helper TLBI/PSCI instruction içeriyor: $timer_body"
    fi
done
for timer_body in "$timer_prepare" "$timer_advance" "$timer_disable"; do
    require_contract "$timer_body" 'mrs[[:space:]]+x[0-9]+, MPIDR_EL1' \
        'timer write helper CPU1 physical identity okumuyor'
    require_contract "$timer_body" 'ubfx[[:space:]]+x[0-9]+, x[0-9]+, #8, #8' \
        'timer write helper MPIDR Aff1/logical CPU çözümlemiyor'
    require_contract "$timer_body" 'cmp[[:space:]]+x[0-9]+, #0x1' \
        'timer write helper logical CPU1 sınırı taşımıyor'
done
require_contract "$timer_prepare" 'msr[[:space:]]+CNTV_CTL_EL0, x[0-9]+' \
    'periodic prepare timer control yazmıyor'
require_contract "$timer_prepare" 'msr[[:space:]]+CNTV_CVAL_EL0, x[0-9]+' \
    'periodic prepare absolute CVAL yazmıyor'
require_contract "$timer_advance" 'msr[[:space:]]+CNTV_CVAL_EL0, x[0-9]+' \
    'periodic advance absolute CVAL yazmıyor'
require_contract "$timer_disable" 'msr[[:space:]]+CNTV_CTL_EL0, x[0-9]+' \
    'periodic disable local timer control yazmıyor'
require_msr_surface "$timer_snapshot" 0 'a^' 'timer snapshot'
require_msr_surface "$timer_prepare" 3 \
    '[[:space:]]msr[[:space:]]+CNTV_(CTL|CVAL)_EL0, x[0-9]+$' \
    'timer prepare'
[ "$(instruction_count "$timer_prepare" \
    'msr[[:space:]]+CNTV_CTL_EL0, x[0-9]+$')" -eq 2 ] || \
    fail 'timer prepare exact iki CNTV_CTL_EL0 write taşımıyor'
[ "$(instruction_count "$timer_prepare" \
    'msr[[:space:]]+CNTV_CVAL_EL0, x[0-9]+$')" -eq 1 ] || \
    fail 'timer prepare exact bir CNTV_CVAL_EL0 write taşımıyor'
require_msr_surface "$timer_advance" 1 \
    '[[:space:]]msr[[:space:]]+CNTV_CVAL_EL0, x[0-9]+$' \
    'timer advance'
require_msr_surface "$timer_disable" 1 \
    '[[:space:]]msr[[:space:]]+CNTV_CTL_EL0, x[0-9]+$' \
    'timer disable'

# Handler success machine code: active ownership first; snapshot/count/absolute
# advance; second-delivery-only disable; raw EOI; completion barrier; evidence;
# saved SPSR unmask/mask; and one shared Release stage CAS.
[ "$(call_count "$handler" "$snapshot_symbol")" -eq 1 ] || \
    fail 'handler timer snapshot çağrısı exact bir değil'
[ "$(call_count "$handler" "$advance_symbol")" -eq 1 ] || \
    fail 'handler absolute-CVAL advance çağrısı exact bir değil'
[ "$(call_count "$handler" "$disable_symbol")" -eq 1 ] || \
    fail 'handler IRQ2 local disable çağrısı exact bir değil'
[ "$(call_count "$handler" "$consume_error_symbol")" -eq 1 ] || \
    fail 'handler bounded consume-error çağrısı exact bir değil'
[ "$(call_count "$handler" "$publish_error_symbol")" -eq 1 ] || \
    fail 'handler CAS-error publication çağrısı exact bir değil'
handler_calls=$(instruction_count "$handler" \
    '[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<[^>]+>$')
[ "$handler_calls" -eq 6 ] || fail "handler direct-call yüzeyi exact altı değil: $handler_calls"
handler_int_arg=$(pattern_line "$handler" \
    'mov[[:space:]]+w22, w2([[:space:]]|$)')
handler_ack_arg=$(pattern_line "$handler" \
    'mov[[:space:]]+w21, w1([[:space:]]|$)')
int_id_cmp=$(first_pattern_after "$handler" \
    'cmp[[:space:]]+w22, #0x1b' "$handler_stage")
int_id_branch=$(next_instruction_line "$handler" "$int_id_cmp")
require_line_contract "$handler" "$int_id_branch" \
    '[[:space:]]b[.]ne[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_try_handle_secondary_irq[+]0x[[:xdigit:]]+>$' \
    'handler int_id!=PPI27 fail-closed branchi compare ile bitişik değil'
ack_raw_cmp=$(next_instruction_line "$handler" "$int_id_branch")
require_line_contract "$handler" "$ack_raw_cmp" \
    '[[:space:]]cmp[[:space:]]+w21, #0x1b' \
    'handler raw ACK exact PPI27 compareı int_id kapısından hemen sonra değil'
ack_raw_branch=$(next_instruction_line "$handler" "$ack_raw_cmp")
require_line_contract "$handler" "$ack_raw_branch" \
    '[[:space:]]b[.]ne[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_try_handle_secondary_irq[+]0x[[:xdigit:]]+>$' \
    'handler raw ACK!=PPI27 fail-closed branchi compare ile bitişik değil'
require_order 'handler active/stage/int_id=PPI27/raw-ACK=PPI27' \
    "$handler_int_arg" "$handler_ack_arg" "$active_call" "$handler_stage" \
    "$int_id_cmp" "$int_id_branch" "$ack_raw_cmp" "$ack_raw_branch"
advance_call=$(call_line "$handler" "$advance_symbol")
disable_call=$(call_line "$handler" "$disable_symbol")
stage_load=$(last_pattern_line "$handler" 'ldaxr[[:space:]]+x10, \[x23\]$')
stage_store=$(last_pattern_line "$handler" 'stlxr[[:space:]]+w10, x9, \[x23\]$')
require_order 'handler advance/disable/stage publication' \
    "$advance_call" "$disable_call" "$stage_load" "$stage_store"
eoi_base_count=$(awk -v start="$advance_call" -v stop="$stage_load" '
    NR > start && NR < stop && /mov[[:space:]]+x8, #0xa010/ { count++ }
    END { print count + 0 }
' "$handler")
[ "$eoi_base_count" -eq 2 ] || \
    fail "success path GICC_EOIR base kuruluşu exact iki değil: $eoi_base_count"
eoi_base1=$(awk -v start="$advance_call" -v stop="$stage_load" '
    NR > start && NR < stop && /mov[[:space:]]+x8, #0xa010/ { print NR; exit }
' "$handler")
eoi_base2=$(awk -v start="$eoi_base1" -v stop="$stage_load" '
    NR > start && NR < stop && /mov[[:space:]]+x8, #0xa010/ { print NR; exit }
' "$handler")

eoi1_value=$(next_instruction_line "$handler" "$eoi_base1")
require_line_contract "$handler" "$eoi1_value" \
    '[[:space:]]mov[[:space:]]+w9, #0x1b' \
    'IRQ1 EOIR payload exact raw PPI27 değil'
eoi1_movk1=$(next_instruction_line "$handler" "$eoi1_value")
require_line_contract "$handler" "$eoi1_movk1" \
    '[[:space:]]movk[[:space:]]+x8, #0x7fff, lsl #16' \
    'IRQ1 GICC_EOIR base middle halfwordu exact değil'
eoi1_movk2=$(next_instruction_line "$handler" "$eoi1_movk1")
require_line_contract "$handler" "$eoi1_movk2" \
    '[[:space:]]movk[[:space:]]+x8, #0x10, lsl #32' \
    'IRQ1 GICC_EOIR base high halfwordu exact değil'
eoi1=$(next_instruction_line "$handler" "$eoi1_movk2")
require_line_contract "$handler" "$eoi1" \
    '[[:space:]]str[[:space:]]+w9, \[x8\]$' \
    'IRQ1 raw PPI27 GICC_EOIR storeu yok'
eoi1_evidence_base=$(next_instruction_line "$handler" "$eoi1")
require_line_contract "$handler" "$eoi1_evidence_base" \
    '[[:space:]]adrp[[:space:]]+x8,' \
    'IRQ1 EOI sonrası evidence base hazırlığı exact değil'
dsb1=$(next_instruction_line "$handler" "$eoi1_evidence_base")
require_line_contract "$handler" "$dsb1" \
    '[[:space:]]dsb[[:space:]]+ish$' \
    'IRQ1 EOI completion DSB ISH taşımıyor'
isb1=$(next_instruction_line "$handler" "$dsb1")
require_line_contract "$handler" "$isb1" \
    '[[:space:]]isb([[:space:]]|$)' \
    'IRQ1 EOI completion DSB sonrasında ISB taşımıyor'
evidence1=$(next_instruction_line "$handler" "$isb1")
require_line_contract "$handler" "$evidence1" \
    '[[:space:]]str[[:space:]]+x27, \[x8, #0x348\]$' \
    'IRQ1 EOI/DSB/ISB sonrasında delivery evidence yayını yok'

eoi2_value=$(next_instruction_line "$handler" "$eoi_base2")
require_line_contract "$handler" "$eoi2_value" \
    '[[:space:]]mov[[:space:]]+w9, #0x1b' \
    'IRQ2 EOIR payload exact raw PPI27 değil'
eoi2_spill=$(next_instruction_line "$handler" "$eoi2_value")
require_line_contract "$handler" "$eoi2_spill" \
    '[[:space:]]ldr[[:space:]]+x10, \[sp, #0x18\]' \
    'IRQ2 EOI bloğu disable sonucu kontrolünü korumuyor'
eoi2_movk1=$(next_instruction_line "$handler" "$eoi2_spill")
require_line_contract "$handler" "$eoi2_movk1" \
    '[[:space:]]movk[[:space:]]+x8, #0x7fff, lsl #16' \
    'IRQ2 GICC_EOIR base middle halfwordu exact değil'
eoi2_movk2=$(next_instruction_line "$handler" "$eoi2_movk1")
require_line_contract "$handler" "$eoi2_movk2" \
    '[[:space:]]movk[[:space:]]+x8, #0x10, lsl #32' \
    'IRQ2 GICC_EOIR base high halfwordu exact değil'
eoi2=$(next_instruction_line "$handler" "$eoi2_movk2")
require_line_contract "$handler" "$eoi2" \
    '[[:space:]]str[[:space:]]+w9, \[x8\]$' \
    'IRQ2 raw PPI27 GICC_EOIR storeu yok'
eoi2_evidence_base=$(next_instruction_line "$handler" "$eoi2")
require_line_contract "$handler" "$eoi2_evidence_base" \
    '[[:space:]]adrp[[:space:]]+x8,' \
    'IRQ2 EOI sonrası evidence base hazırlığı exact değil'
dsb2=$(next_instruction_line "$handler" "$eoi2_evidence_base")
require_line_contract "$handler" "$dsb2" \
    '[[:space:]]dsb[[:space:]]+ish$' \
    'IRQ2 EOI completion DSB ISH taşımıyor'
isb2=$(next_instruction_line "$handler" "$dsb2")
require_line_contract "$handler" "$isb2" \
    '[[:space:]]isb([[:space:]]|$)' \
    'IRQ2 EOI completion DSB sonrasında ISB taşımıyor'
evidence2=$(next_instruction_line "$handler" "$isb2")
require_line_contract "$handler" "$evidence2" \
    '[[:space:]]str[[:space:]]+x27, \[x8, #0x348\]$' \
    'IRQ2 EOI/DSB/ISB sonrasında delivery evidence yayını yok'
success_word_store_lines=$(awk -v start="$advance_call" -v stop="$stage_load" '
    NR > start && NR < stop &&
        /[[:space:]](stp|stnp|str|stur|stlr)[[:space:]]+w[0-9]+(,|[[:space:]])/ { print NR }
' "$handler")
expected_eoi_store_lines=$(printf '%s\n%s' "$eoi1" "$eoi2")
[ "$success_word_store_lines" = "$expected_eoi_store_lines" ] || \
    fail "success interval exact iki raw EOIR word store dışında store içeriyor: $success_word_store_lines"
require_order 'IRQ1 EOIR-address/raw27/DSB/ISB/evidence' \
    "$eoi_base1" "$eoi1_value" "$eoi1" "$dsb1" "$isb1" "$evidence1" "$eoi_base2"
require_order 'IRQ2 EOIR-address/raw27/DSB/ISB/evidence/stage' \
    "$eoi_base2" "$eoi2_value" "$eoi2" "$dsb2" "$isb2" "$evidence2" \
    "$stage_load" "$stage_store"
irq1_evidence_stores=$(awk -v start="$dsb1" -v stop="$eoi2" '
    NR > start && NR < stop && /str[[:space:]]+x[0-9]+, \[x[0-9]+, #[^]]+\]$/ { count++ }
    END { print count + 0 }
' "$handler")
irq2_evidence_stores=$(awk -v start="$dsb2" -v stop="$stage_load" '
    NR > start && NR < stop && /str[[:space:]]+x[0-9]+, \[x[0-9]+, #[^]]+\]$/ { count++ }
    END { print count + 0 }
' "$handler")
[ "$irq1_evidence_stores" -ge 9 ] || \
    fail "IRQ1 EOI sonrası evidence store yetersiz: $irq1_evidence_stores"
[ "$irq2_evidence_stores" -ge 10 ] || \
    fail "IRQ2 EOI sonrası evidence store yetersiz: $irq2_evidence_stores"
irq1_unmask=$(first_pattern_after "$handler" \
    'and[[:space:]]+x[0-9]+, x[0-9]+, #0xffffffffffffff7f' "$dsb1")
irq2_mask=$(first_pattern_after "$handler" \
    'orr[[:space:]]+x[0-9]+, x[0-9]+, #0x80' "$dsb2")
require_order 'saved IRQ1-unmask/IRQ2-mask/stage' \
    "$irq1_unmask" "$eoi2" "$irq2_mask" "$stage_load"
delivery_cmp=$(first_pattern_after "$handler" \
    'cmp[[:space:]]+x19, #0x1' "$advance_call")
delivery_irq1_branch=$(first_pattern_after "$handler" \
    'b[.]eq[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_try_handle_secondary_irq[+]0x[[:xdigit:]]+>$' \
    "$delivery_cmp")
[ -n "$delivery_irq1_branch" ] && [ "$delivery_irq1_branch" -lt "$disable_call" ] || \
    fail 'delivery==1 branchi IRQ2 disable çağrısından önce bounded değil'
[ "$(branch_target_at_line "$handler" "$delivery_irq1_branch")" = \
    "$(address_at_line "$handler" "$eoi_base1")" ] || \
    fail 'delivery==1 branchi doğrudan IRQ1 EOI bloğuna gitmiyor'
disable_ok_branch=$(next_instruction_line "$handler" "$disable_call")
disable_result_load=$(next_instruction_line "$handler" "$disable_ok_branch")
if sed -n "${disable_ok_branch}p" "$handler" | grep -Eq '[[:space:]]ldr[[:space:]]+x8, \[sp, #0x10\]'; then
    disable_result_load=$disable_ok_branch
    disable_ok_branch=$(next_instruction_line "$handler" "$disable_result_load")
fi
require_line_contract "$handler" "$disable_result_load" \
    '[[:space:]]ldr[[:space:]]+x8, \[sp, #0x10\]' \
    'IRQ2 disable Result discriminantı okunmuyor'
require_line_contract "$handler" "$disable_ok_branch" \
    '[[:space:]]cbz[[:space:]]+x8, (0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_try_handle_secondary_irq[+]0x[[:xdigit:]]+>$' \
    'IRQ2 disable success branchi Result discriminantına bağlı değil'
[ "$(branch_target_at_line "$handler" "$disable_ok_branch")" = \
    "$(address_at_line "$handler" "$eoi_base2")" ] || \
    fail 'IRQ2 timer disable success branchi doğrudan IRQ2 EOI bloğuna gitmiyor'
irq1_stage_value=$(first_pattern_after "$handler" \
    'mov[[:space:]]+w9, #0x2' "$evidence1")
irq1_saved_load=$(next_instruction_line "$handler" "$irq1_stage_value")
require_line_contract "$handler" "$irq1_saved_load" \
    '[[:space:]]ldr[[:space:]]+x8, \[x20, #0x100\]' \
    'IRQ1 shared stage yolunda saved SPSR okunmuyor'
irq1_saved_unmask=$(next_instruction_line "$handler" "$irq1_saved_load")
require_line_contract "$handler" "$irq1_saved_unmask" \
    '[[:space:]]and[[:space:]]+x8, x8, #0xffffffffffffff7f' \
    'IRQ1 shared stage yolunda saved SPSR IRQ maskesi açılmıyor'
irq1_common_branch=$(next_instruction_line "$handler" "$irq1_saved_unmask")
require_line_contract "$handler" "$irq1_common_branch" \
    '[[:space:]]b[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_try_handle_secondary_irq[+]0x[[:xdigit:]]+>$' \
    'IRQ1 stage=2 yolu shared publication bloğuna doğrudan dallanmıyor'
irq2_stage_value=$(first_pattern_after "$handler" \
    'mov[[:space:]]+w9, #0x3' "$evidence2")
irq2_saved_load=$(next_instruction_line "$handler" "$irq2_stage_value")
require_line_contract "$handler" "$irq2_saved_load" \
    '[[:space:]]ldr[[:space:]]+x8, \[x20, #0x100\]' \
    'IRQ2 shared stage yolunda saved SPSR okunmuyor'
irq2_saved_mask=$(next_instruction_line "$handler" "$irq2_saved_load")
require_line_contract "$handler" "$irq2_saved_mask" \
    '[[:space:]]orr[[:space:]]+x8, x8, #0x80' \
    'IRQ2 shared stage yolunda saved SPSR IRQ maskesi kapanmıyor'
stage_ctx_store=$(next_instruction_line "$handler" "$irq2_saved_mask")
require_line_contract "$handler" "$stage_ctx_store" \
    '[[:space:]]str[[:space:]]+x8, \[x20, #0x100\]' \
    'shared stage publication saved SPSR değerini context içine yazmıyor'
[ "$(branch_target_at_line "$handler" "$irq1_common_branch")" = \
    "$(address_at_line "$handler" "$stage_ctx_store")" ] || \
    fail 'IRQ1 stage=2 branchi IRQ2 ile aynı shared publication bloğunu kullanmıyor'
[ "$(next_instruction_line "$handler" "$stage_ctx_store")" = "$stage_load" ] || \
    fail 'shared saved-SPSR publication doğrudan STAGE CAS loaduna geçmiyor'
stage_expected_cmp=$(next_instruction_line "$handler" "$stage_load")
require_line_contract "$handler" "$stage_expected_cmp" \
    '[[:space:]]cmp[[:space:]]+x10, x19' \
    'shared STAGE CAS Acquire loadunu girişteki expected stage ile karşılaştırmıyor'
stage_mismatch_branch=$(next_instruction_line "$handler" "$stage_expected_cmp")
require_line_contract "$handler" "$stage_mismatch_branch" \
    '[[:space:]]b[.]ne[[:space:]]+(0x)?[[:xdigit:]]+' \
    'shared STAGE CAS mismatch fail-closed branchi yok'
stage_mismatch_address=$(branch_target_at_line "$handler" "$stage_mismatch_branch")
stage_mismatch=$(line_at_address "$handler" "$stage_mismatch_address")
require_line_contract "$handler" "$stage_mismatch" \
    '[[:space:]]orr[[:space:]]+x8, x8, #0x80' \
    'shared STAGE CAS mismatch hedefi saved SPSR IRQ-mask fail yoluna gitmiyor'
stage_mismatch_clrex=$(next_instruction_line "$handler" "$stage_mismatch")
require_line_contract "$handler" "$stage_mismatch_clrex" \
    '[[:space:]]clrex([[:space:]]|$)' \
    'shared STAGE CAS mismatch exclusive monitorü temizlemiyor'
stage_mismatch_code=$(next_instruction_line "$handler" "$stage_mismatch_clrex")
require_line_contract "$handler" "$stage_mismatch_code" \
    '[[:space:]]mov[[:space:]]+w0, #0x3' \
    'shared STAGE CAS mismatch ERR_STAGE kodunu taşımıyor'
stage_mismatch_ctx=$(next_instruction_line "$handler" "$stage_mismatch_code")
require_line_contract "$handler" "$stage_mismatch_ctx" \
    '[[:space:]]str[[:space:]]+x8, \[x20, #0x100\]' \
    'shared STAGE CAS mismatch saved SPSR IRQ maskesini context içine yazmıyor'
stage_mismatch_base=$(next_instruction_line "$handler" "$stage_mismatch_ctx")
require_line_contract "$handler" "$stage_mismatch_base" \
    '[[:space:]]adrp[[:space:]]+x8,' \
    'shared STAGE CAS mismatch actual-stage base çözmüyor'
stage_mismatch_expected=$(next_instruction_line "$handler" "$stage_mismatch_base")
require_line_contract "$handler" "$stage_mismatch_expected" \
    '[[:space:]]mov[[:space:]]+x1, x19' \
    'shared STAGE CAS mismatch expected stage değerini korumuyor'
stage_mismatch_actual=$(next_instruction_line "$handler" "$stage_mismatch_expected")
require_line_contract "$handler" "$stage_mismatch_actual" \
    '[[:space:]]ldr[[:space:]]+x2, \[x8, #0x3b0\]' \
    'shared STAGE CAS mismatch actual stage değerini okumuyor'
stage_mismatch_publish=$(next_instruction_line "$handler" "$stage_mismatch_actual")
require_line_contract "$handler" "$stage_mismatch_publish" \
    "[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<$publish_error_symbol>$" \
    'shared STAGE CAS mismatch publish_secondary_error direct edge taşımıyor'
stage_mismatch_result=$(next_instruction_line "$handler" "$stage_mismatch_publish")
require_line_contract "$handler" "$stage_mismatch_result" \
    '[[:space:]]mov[[:space:]]+w0, w24' \
    'shared STAGE CAS mismatch handled sonucunu korumuyor'
stage_mismatch_return=$(next_instruction_line "$handler" "$stage_mismatch_result")
require_line_contract "$handler" "$stage_mismatch_return" \
    '[[:space:]]b[[:space:]]+(0x)?[[:xdigit:]]+' \
    'shared STAGE CAS mismatch bounded handler epiloguna dönmüyor'
[ "$(branch_target_at_line "$handler" "$stage_mismatch_return")" = \
    "$handler_epilogue_address" ] || \
    fail 'shared STAGE CAS mismatch gerçek handler return epiloguna gitmiyor'
[ "$(next_instruction_line "$handler" "$stage_mismatch_branch")" = "$stage_store" ] || \
    fail 'shared STAGE CAS compare successi direct Release storea geçmiyor'
stage_retry=$(next_instruction_line "$handler" "$stage_store")
require_line_contract "$handler" "$stage_retry" \
    '[[:space:]]cbnz[[:space:]]+w10, (0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_try_handle_secondary_irq[+]0x[[:xdigit:]]+>$' \
    'shared STAGE CAS retry branchi status registerına bağlı değil'
[ "$(branch_target_at_line "$handler" "$stage_retry")" = \
    "$(address_at_line "$handler" "$stage_load")" ] || \
    fail 'shared STAGE CAS retry branchi aynı Acquire loaduna dönmüyor'
stage_dsb=$(next_instruction_line "$handler" "$stage_retry")
require_line_contract "$handler" "$stage_dsb" \
    '[[:space:]]dsb[[:space:]]+ishst' \
    'handler Release CAS success fallthrough doğrudan DSB ISHST değil'
stage_sev=$(next_instruction_line "$handler" "$stage_dsb")
require_line_contract "$handler" "$stage_sev" \
    '[[:space:]]sev([[:space:]]|$)' \
    'handler Release CAS DSB sonrasında doğrudan SEV yok'
stage_success_result=$(next_instruction_line "$handler" "$stage_sev")
require_line_contract "$handler" "$stage_success_result" \
    '[[:space:]]mov[[:space:]]+w0, w24' \
    'handler stage-publication success handled sonucunu korumuyor'
stage_success_return=$(next_instruction_line "$handler" "$stage_success_result")
require_line_contract "$handler" "$stage_success_return" \
    '[[:space:]]b[[:space:]]+(0x)?[[:xdigit:]]+' \
    'handler stage-publication success bounded epiloga dönmüyor'
[ "$(branch_target_at_line "$handler" "$stage_success_return")" = \
    "$handler_epilogue_address" ] || \
    fail 'handler stage-publication success gerçek handler return epiloguna gitmiyor'
require_order 'handler Release CAS/DSB/SEV/handled-return' \
    "$stage_store" "$stage_retry" "$stage_dsb" "$stage_sev" \
    "$stage_success_result" "$stage_success_return"

# CPU1 publishes ARMED, waits for the distinct CPU0 acknowledgement, unmasks,
# actively samples the third deadline, reads PPI state, republishes all final
# evidence, then Release-publishes PARKED and terminally WFE-parks.
[ "$(call_count "$secondary" rpi5_g8f_prerequisite_complete)" -eq 1 ] || \
    fail 'CPU1 BOOT8F prerequisite direct-call sayısı exact bir değil'
[ "$(call_count "$secondary" "$prepare_symbol")" -eq 1 ] || \
    fail 'CPU1 periodic prepare direct-call sayısı exact bir değil'
[ "$(call_count "$secondary" rpi5_g8g_read_secondary_ppi_state)" -eq 1 ] || \
    fail 'CPU1 read-only PPI snapshot direct-call sayısı exact bir değil'
[ "$(call_count "$secondary" "$secondary_fail_symbol")" -eq 19 ] || \
    fail 'CPU1 fail-closed edge sayısı exact on dokuz değil'
secondary_calls=$(instruction_count "$secondary" \
    '[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<[^>]+>$')
[ "$secondary_calls" -eq 23 ] || \
    fail "CPU1 direct-call yüzeyi exact yirmi üç değil: $secondary_calls"
armed_store=$(nth_pattern_line "$secondary" \
    'stlxr[[:space:]]+w[0-9]+, x[0-9]+, \[x[0-9]+\]$' 1)
armed_dsb=$(first_pattern_after "$secondary" 'dsb[[:space:]]+ishst' "$armed_store")
armed_sev=$(first_pattern_after "$secondary" '[[:space:]]sev([[:space:]]|$)' "$armed_dsb")
armed_ack=$(first_pattern_after "$secondary" \
    'ldarb[[:space:]]+w[0-9]+, \[x[0-9]+\]' "$armed_sev")
irq_unmask=$(first_pattern_after "$secondary" 'msr[[:space:]]+DAIFClr, #0x2' "$armed_ack")
require_order 'CPU1 ARMED/notify/CPU0-ack/IRQ-unmask' \
    "$armed_store" "$armed_dsb" "$armed_sev" "$armed_ack" "$irq_unmask"
timer_ctl=$(first_pattern_after "$secondary" \
    'mrs[[:space:]]+x[0-9]+, CNTV_CTL_EL0' "$irq_unmask")
ppi_call=$(call_line "$secondary" rpi5_g8g_read_secondary_ppi_state)
third_cval_load=$(first_pattern_after "$secondary" \
    'ldar[[:space:]]+x8, \[x8\]$' "$timer_ctl")
period_load=$(first_pattern_after "$secondary" \
    'ldar[[:space:]]+x20, \[x9\]$' "$third_cval_load")
third_cval_spill=$(next_instruction_line "$secondary" "$period_load")
require_line_contract "$secondary" "$third_cval_spill" \
    '[[:space:]]str[[:space:]]+x8, \[sp, #0x8\]$' \
    'CPU1 third_cval bounded stack spill exact değil'
third_upper_add=$(next_instruction_line "$secondary" "$third_cval_spill")
require_line_contract "$secondary" "$third_upper_add" \
    '[[:space:]]adds[[:space:]]+x22, x20, x8' \
    'CPU1 third upper bound period+third_cval checked add taşımıyor'
third_upper_select=$(next_instruction_line "$secondary" "$third_upper_add")
require_line_contract "$secondary" "$third_upper_select" \
    '[[:space:]]csinv[[:space:]]+x9, x22, xzr, lo' \
    'CPU1 third upper overflow sentinel seçimi checked add ile bağlı değil'
third_poll_entry_branch=$(next_instruction_line "$secondary" "$third_upper_select")
require_line_contract "$secondary" "$third_poll_entry_branch" \
    '[[:space:]]b[.]lo[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_secondary_run[+]0x[[:xdigit:]]+>$' \
    'CPU1 third poll yalnız no-overflow add yolundan başlamıyor'
third_count1_address=$(branch_target_at_line "$secondary" "$third_poll_entry_branch")
third_count1=$(line_at_address "$secondary" "$third_count1_address")
require_line_contract "$secondary" "$third_count1" \
    '[[:space:]]mrs[[:space:]]+x8, CNTVCT_EL0' \
    'CPU1 third poll entry raw CNTVCT sampleı değil'
third_count1_copy=$(next_instruction_line "$secondary" "$third_count1")
require_line_contract "$secondary" "$third_count1_copy" \
    '[[:space:]]mov[[:space:]]+x10, x8' \
    'CPU1 third poll ilk sampleını bounded result registerında korumuyor'
third_upper_cmp1=$(next_instruction_line "$secondary" "$third_count1_copy")
require_line_contract "$secondary" "$third_upper_cmp1" \
    '[[:space:]]cmp[[:space:]]+x8, x9' \
    'CPU1 third poll ilk sampleı exclusive upper ile karşılaştırmıyor'
third_upper_fail1=$(next_instruction_line "$secondary" "$third_upper_cmp1")
require_line_contract "$secondary" "$third_upper_fail1" \
    '[[:space:]]b[.]hs[[:space:]]+(0x)?[[:xdigit:]]+' \
    'CPU1 third poll now>=upper fail-closed branchi yok'
third_lower_reload=$(next_instruction_line "$secondary" "$third_upper_fail1")
require_line_contract "$secondary" "$third_lower_reload" \
    '[[:space:]]ldr[[:space:]]+x11, \[sp, #0x8\]$' \
    'CPU1 third poll third_cval lower boundını stackten geri yüklemiyor'
third_lower_cmp=$(next_instruction_line "$secondary" "$third_lower_reload")
require_line_contract "$secondary" "$third_lower_cmp" \
    '[[:space:]]cmp[[:space:]]+x10, x11' \
    'CPU1 third poll now>=third_cval compareı yok'
third_lower_flag=$(next_instruction_line "$secondary" "$third_lower_cmp")
require_line_contract "$secondary" "$third_lower_flag" \
    '[[:space:]]cset[[:space:]]+w8, lo' \
    'CPU1 third poll now<third_cval flagını korumuyor'
third_lower_success=$(next_instruction_line "$secondary" "$third_lower_flag")
require_line_contract "$secondary" "$third_lower_success" \
    '[[:space:]]b[.]hs[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_secondary_run[+]0x[[:xdigit:]]+>$' \
    'CPU1 third poll now>=third_cval success branchi yok'
third_spin_isb=$(next_instruction_line "$secondary" "$third_lower_success")
require_line_contract "$secondary" "$third_spin_isb" \
    '[[:space:]]isb([[:space:]]|$)' \
    'CPU1 third poll bounded spin barrierı yok'
third_count2=$(next_instruction_line "$secondary" "$third_spin_isb")
require_line_contract "$secondary" "$third_count2" \
    '[[:space:]]mrs[[:space:]]+x10, CNTVCT_EL0' \
    'CPU1 third poll loop sampleı raw CNTVCT değil'
third_upper_cmp2=$(next_instruction_line "$secondary" "$third_count2")
require_line_contract "$secondary" "$third_upper_cmp2" \
    '[[:space:]]cmp[[:space:]]+x10, x9' \
    'CPU1 third poll loop sampleı exclusive upper ile karşılaştırmıyor'
third_loopback=$(next_instruction_line "$secondary" "$third_upper_cmp2")
require_line_contract "$secondary" "$third_loopback" \
    '[[:space:]]b[.]lo[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_secondary_run[+]0x[[:xdigit:]]+>$' \
    'CPU1 third poll loopback now<upper koşuluna bağlı değil'
[ "$(branch_target_at_line "$secondary" "$third_loopback")" = \
    "$(address_at_line "$secondary" "$third_lower_cmp")" ] || \
    fail 'CPU1 third poll loopback aynı now>=third_cval compareına dönmüyor'
third_upper_exit=$(next_instruction_line "$secondary" "$third_loopback")
require_line_contract "$secondary" "$third_upper_exit" \
    '[[:space:]]b[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8g_secondary_run[+]0x[[:xdigit:]]+>$' \
    'CPU1 third poll upper-bound terminal yolu shared result bloğuna gitmiyor'
third_poll_result_address=$(branch_target_at_line "$secondary" "$third_lower_success")
[ "$(branch_target_at_line "$secondary" "$third_upper_exit")" = "$third_poll_result_address" ] || \
    fail 'CPU1 third poll success/upper-bound yolları aynı bounded result bloğunda birleşmiyor'
third_poll_result=$(line_at_address "$secondary" "$third_poll_result_address")
require_line_contract "$secondary" "$third_poll_result" \
    '[[:space:]]str[[:space:]]+x10, \[sp\]$' \
    'CPU1 third poll sampleını post-PPI alt sınırı için korumuyor'
third_poll_result_branch=$(next_instruction_line "$secondary" "$third_poll_result")
require_line_contract "$secondary" "$third_poll_result_branch" \
    '[[:space:]]tbz[[:space:]]+w8, #0x0, (0x)?[[:xdigit:]]+' \
    'CPU1 third poll result flagı fail-closed tüketilmiyor'
[ "$(branch_target_at_line "$secondary" "$third_upper_fail1")" = \
    "$(address_at_line "$secondary" "$(last_pattern_before "$secondary" 'mov[[:space:]]+w8, #0x1' "$third_poll_result")")" ] || \
    fail 'CPU1 first now>=upper edge bounded error flag yoluna gitmiyor'
ppi_arg=$(last_pattern_before "$secondary" \
    'mov[[:space:]]+w0, #0x1b' "$ppi_call")
[ "$(next_instruction_line "$secondary" "$ppi_arg")" = "$ppi_call" ] || \
    fail 'CPU1 read-only PPI snapshot çağrısı exact PPI27 argümanının hemen ardından değil'
require_order 'CPU1 timer-off/third interval poll/PPI27 snapshot' \
    "$timer_ctl" "$third_cval_load" "$period_load" "$third_cval_spill" \
    "$third_upper_add" "$third_count1" "$third_count2" \
    "$third_poll_result_branch" "$ppi_arg" "$ppi_call"
if awk -v start="$third_count1" -v stop="$ppi_call" '
    NR > start && NR < stop && /[[:space:]]wfe([[:space:]]|$)/ { found=1 }
    END { exit(found ? 0 : 1) }
' "$secondary"; then
    fail 'CPU1 third-deadline bounded poll WFE içeriyor'
fi
ppi_result_load=$(next_instruction_line "$secondary" "$ppi_call")
require_line_contract "$secondary" "$ppi_result_load" \
    '[[:space:]]ldr[[:space:]]+w8, \[sp, #0x10\]$' \
    'CPU1 PPI snapshot Result discriminantını okumuyor'
ppi_result_branch=$(next_instruction_line "$secondary" "$ppi_result_load")
require_line_contract "$secondary" "$ppi_result_branch" \
    '[[:space:]]cbz[[:space:]]+w8, (0x)?[[:xdigit:]]+' \
    'CPU1 PPI snapshot errorunu fail-closed dallandırmıyor'
ppi_success_address=$(branch_target_at_line "$secondary" "$ppi_result_branch")
ppi_bpr_enabled_load=$(line_at_address "$secondary" "$ppi_success_address")
require_line_contract "$secondary" "$ppi_bpr_enabled_load" \
    '[[:space:]]ldp[[:space:]]+w11, w8, \[sp, #0x20\]' \
    'CPU1 PPI BPR/enabled readback alanlarını bağlamıyor'
ppi_pending_active_load=$(next_instruction_line "$secondary" "$ppi_bpr_enabled_load")
require_line_contract "$secondary" "$ppi_pending_active_load" \
    '[[:space:]]ldp[[:space:]]+w10, w9, \[sp, #0x28\]' \
    'CPU1 PPI pending/active readback alanlarını bağlamıyor'
ppi_bpr_cmp=$(next_instruction_line "$secondary" "$ppi_pending_active_load")
require_line_contract "$secondary" "$ppi_bpr_cmp" \
    '[[:space:]]cmp[[:space:]]+w11, #0x7' \
    'CPU1 PPI BPR reserved-bit üst sınırını doğrulamıyor'
ppi_bpr_branch=$(next_instruction_line "$secondary" "$ppi_bpr_cmp")
require_line_contract "$secondary" "$ppi_bpr_branch" \
    '[[:space:]]b[.]hi[[:space:]]+(0x)?[[:xdigit:]]+' \
    'CPU1 PPI BPR invalid readbackını fail-closed dallandırmıyor'
ppi_pmr_load=$(next_instruction_line "$secondary" "$ppi_bpr_branch")
require_line_contract "$secondary" "$ppi_pmr_load" \
    '[[:space:]]ldrb[[:space:]]+w11, \[sp, #0x1c\]' \
    'CPU1 PPI PMR readbackını okumuyor'
ppi_pmr_cmp=$(next_instruction_line "$secondary" "$ppi_pmr_load")
require_line_contract "$secondary" "$ppi_pmr_cmp" \
    '[[:space:]]cmp[[:space:]]+w11, #0x81' \
    'CPU1 PPI PMR>0x80 sınırını doğrulamıyor'
ppi_pmr_branch=$(next_instruction_line "$secondary" "$ppi_pmr_cmp")
require_line_contract "$secondary" "$ppi_pmr_branch" \
    '[[:space:]]b[.]lo[[:space:]]+(0x)?[[:xdigit:]]+' \
    'CPU1 PPI PMR invalid readbackını fail-closed dallandırmıyor'
ppi_interfaces_load=$(next_instruction_line "$secondary" "$ppi_pmr_branch")
require_line_contract "$secondary" "$ppi_interfaces_load" \
    '[[:space:]]ldp[[:space:]]+w11, w12, \[sp, #0x14\]' \
    'CPU1 distributor/CPU-interface control readbacklarını bağlamıyor'
ppi_interfaces_and=$(next_instruction_line "$secondary" "$ppi_interfaces_load")
require_line_contract "$secondary" "$ppi_interfaces_and" \
    '[[:space:]]and[[:space:]]+w11, w12, w11' \
    'CPU1 distributor ve CPU-interface enable bitlerini birlikte doğrulamıyor'
ppi_interfaces_branch=$(next_instruction_line "$secondary" "$ppi_interfaces_and")
require_line_contract "$secondary" "$ppi_interfaces_branch" \
    '[[:space:]]tbz[[:space:]]+w11, #0x0, (0x)?[[:xdigit:]]+' \
    'CPU1 distributor/CPU-interface disabled durumunu fail-closed dallandırmıyor'
ppi_quiescent_or=$(next_instruction_line "$secondary" "$ppi_interfaces_branch")
require_line_contract "$secondary" "$ppi_quiescent_or" \
    '[[:space:]]orr[[:space:]]+w11, w9, w10' \
    'CPU1 pending|active quiescence readbacklarını birleştirmiyor'
ppi_quiescent_cmp=$(next_instruction_line "$secondary" "$ppi_quiescent_or")
require_line_contract "$secondary" "$ppi_quiescent_cmp" \
    '[[:space:]]cmp[[:space:]]+w11, #0x0' \
    'CPU1 pending|active quiescence sonucunu zero ile karşılaştırmıyor'
ppi_enabled_value=$(next_instruction_line "$secondary" "$ppi_quiescent_cmp")
require_line_contract "$secondary" "$ppi_enabled_value" \
    '[[:space:]]mov[[:space:]]+w11, #0x8000000' \
    'CPU1 enabled maskesi exact PPI27 biti değil'
ppi_enabled_cmp=$(next_instruction_line "$secondary" "$ppi_enabled_value")
require_line_contract "$secondary" "$ppi_enabled_cmp" \
    '[[:space:]]ccmp[[:space:]]+w8, w11, #0x0, eq' \
    'CPU1 enabled readbackı yalnız quiescent PPI27 ile karşılaştırılmıyor'
ppi_enabled_branch=$(next_instruction_line "$secondary" "$ppi_enabled_cmp")
require_line_contract "$secondary" "$ppi_enabled_branch" \
    '[[:space:]]b[.]ne[[:space:]]+(0x)?[[:xdigit:]]+' \
    'CPU1 enabled!=PPI27 veya non-quiescent durumunu fail-closed dallandırmıyor'
ppi_validation_fail_address=$(branch_target_at_line "$secondary" "$ppi_bpr_branch")
for ppi_fail_branch in \
    "$ppi_pmr_branch" "$ppi_interfaces_branch" "$ppi_enabled_branch"; do
    [ "$(branch_target_at_line "$secondary" "$ppi_fail_branch")" = \
        "$ppi_validation_fail_address" ] || \
        fail 'CPU1 PPI readback sapmaları ortak bounded fail bloğuna gitmiyor'
done
ppi_validation_fail=$(line_at_address "$secondary" "$ppi_validation_fail_address")
require_line_contract "$secondary" "$ppi_validation_fail" \
    '[[:space:]]cmp[[:space:]]+w10, #0x0' \
    'CPU1 PPI readback fail hedefi actual pending değerini encode etmiyor'
ppi_validation_fail_call=$(first_pattern_after "$secondary" \
    "[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<$secondary_fail_symbol>$" \
    "$ppi_validation_fail")
[ "$(instruction_count_between "$secondary" "$ppi_validation_fail" \
    "$ppi_validation_fail_call")" -eq 9 ] || \
    fail 'CPU1 PPI readback fail bloğu bounded secondary_fail edge şekline sahip değil'
ppi_validation_unexpected_cf=$(awk -v start="$ppi_validation_fail" -v stop="$ppi_validation_fail_call" '
    NR > start && NR < stop && /[[:space:]](b([.][a-z]+)?|cbz|cbnz|tbz|tbnz|bl|blr|br|ret)([[:space:]]|$)/ { print }
' "$secondary")
[ -z "$ppi_validation_unexpected_cf" ] || \
    fail "CPU1 PPI readback fail bloğu secondary_fail öncesi başka control-flow içeriyor: $ppi_validation_unexpected_cf"

ppi_result_fail=$(next_instruction_line "$secondary" "$ppi_result_branch")
require_line_contract "$secondary" "$ppi_result_fail" \
    '[[:space:]]mov[[:space:]]+w0, #0x11' \
    'CPU1 PPI Result error hedefi ERR_FINAL_GIC kodu taşımıyor'
ppi_result_fail_expected=$(next_instruction_line "$secondary" "$ppi_result_fail")
require_line_contract "$secondary" "$ppi_result_fail_expected" \
    '[[:space:]]mov[[:space:]]+w1, #0x1b' \
    'CPU1 PPI Result error hedefi expected PPI27 taşımıyor'
ppi_result_fail_actual=$(next_instruction_line "$secondary" "$ppi_result_fail_expected")
require_line_contract "$secondary" "$ppi_result_fail_actual" \
    '[[:space:]]mov[[:space:]]+x2, xzr' \
    'CPU1 PPI Result error hedefi bounded actual=0 taşımıyor'
ppi_result_fail_call=$(next_instruction_line "$secondary" "$ppi_result_fail_actual")
require_line_contract "$secondary" "$ppi_result_fail_call" \
    "[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<$secondary_fail_symbol>$" \
    'CPU1 PPI Result error hedefi direct secondary_fail edge taşımıyor'
post_third_reload=$(next_instruction_line "$secondary" "$ppi_enabled_branch")
require_line_contract "$secondary" "$post_third_reload" \
    '[[:space:]]ldr[[:space:]]+x8, \[sp, #0x8\]$' \
    'CPU1 post-PPI third_cval alt sınırını geri yüklemiyor'
post_upper_cmp=$(next_instruction_line "$secondary" "$post_third_reload")
require_line_contract "$secondary" "$post_upper_cmp" \
    '[[:space:]]cmp[[:space:]]+x22, x8' \
    'CPU1 post-PPI third_upper overflow/range kontrolü yok'
post_upper_branch=$(next_instruction_line "$secondary" "$post_upper_cmp")
require_line_contract "$secondary" "$post_upper_branch" \
    '[[:space:]]b[.]hs[[:space:]]+(0x)?[[:xdigit:]]+' \
    'CPU1 post-PPI third_upper>=third_cval success yolunu taşımıyor'
post_upper_fail=$(next_instruction_line "$secondary" "$post_upper_branch")
require_line_contract "$secondary" "$post_upper_fail" \
    '[[:space:]]ldr[[:space:]]+x1, \[sp, #0x8\]$' \
    'CPU1 post-PPI upper overflow hedefi third_cval taşımıyor'
post_upper_fail_code=$(next_instruction_line "$secondary" "$post_upper_fail")
require_line_contract "$secondary" "$post_upper_fail_code" \
    '[[:space:]]mov[[:space:]]+w0, #0x6' \
    'CPU1 post-PPI upper overflow hedefi ERR_TIMER_ARITHMETIC taşımıyor'
post_upper_fail_actual=$(next_instruction_line "$secondary" "$post_upper_fail_code")
require_line_contract "$secondary" "$post_upper_fail_actual" \
    '[[:space:]]mov[[:space:]]+x2, x20' \
    'CPU1 post-PPI upper overflow hedefi period taşımıyor'
post_upper_fail_call=$(next_instruction_line "$secondary" "$post_upper_fail_actual")
require_line_contract "$secondary" "$post_upper_fail_call" \
    "[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<$secondary_fail_symbol>$" \
    'CPU1 post-PPI upper overflow hedefi direct secondary_fail edge taşımıyor'
post_ppi_count_address=$(branch_target_at_line "$secondary" "$post_upper_branch")
post_ppi_count=$(line_at_address "$secondary" "$post_ppi_count_address")
require_line_contract "$secondary" "$post_ppi_count" \
    '[[:space:]]mrs[[:space:]]+x2, CNTVCT_EL0' \
    'CPU1 post-PPI count raw CNTVCT sampleı değil'
post_sample_reload=$(next_instruction_line "$secondary" "$post_ppi_count")
require_line_contract "$secondary" "$post_sample_reload" \
    '[[:space:]]ldr[[:space:]]+x8, \[sp\]$' \
    'CPU1 post-PPI prior third sampleını geri yüklemiyor'
post_deadline_cmp=$(next_instruction_line "$secondary" "$post_sample_reload")
require_line_contract "$secondary" "$post_deadline_cmp" \
    '[[:space:]]cmp[[:space:]]+x2, x22' \
    'CPU1 post-PPI count exclusive upper ile karşılaştırılmıyor'
post_sample_cmp=$(next_instruction_line "$secondary" "$post_deadline_cmp")
require_line_contract "$secondary" "$post_sample_cmp" \
    '[[:space:]]ccmp[[:space:]]+x2, x8, #0x0, lo' \
    'CPU1 post-PPI count upper altında ise prior sample alt sınırıyla karşılaştırılmıyor'
post_interval_success=$(next_instruction_line "$secondary" "$post_sample_cmp")
require_line_contract "$secondary" "$post_interval_success" \
    '[[:space:]]b[.]hs[[:space:]]+(0x)?[[:xdigit:]]+' \
    'CPU1 post-PPI sample<=count<upper birleşik success branchi yok'
post_interval_fail=$(next_instruction_line "$secondary" "$post_interval_success")
require_line_contract "$secondary" "$post_interval_fail" \
    '[[:space:]]mov[[:space:]]+w0, #0x12' \
    'CPU1 post-PPI interval sapma hedefi ERR_THIRD_CHECK taşımıyor'
post_interval_fail_expected=$(next_instruction_line "$secondary" "$post_interval_fail")
require_line_contract "$secondary" "$post_interval_fail_expected" \
    '[[:space:]]mov[[:space:]]+x1, x22' \
    'CPU1 post-PPI interval sapma hedefi exclusive upper taşımıyor'
post_interval_fail_call=$(next_instruction_line "$secondary" "$post_interval_fail_expected")
require_line_contract "$secondary" "$post_interval_fail_call" \
    "[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<$secondary_fail_symbol>$" \
    'CPU1 post-PPI interval sapma hedefi direct secondary_fail edge taşımıyor'
ownership_off=$(first_pattern_after "$secondary" \
    'stlrb[[:space:]]+wzr, \[x[0-9]+\]' "$post_ppi_count")
park_load=$(last_pattern_line "$secondary" \
    'ldaxr[[:space:]]+x[0-9]+, \[x[0-9]+\]$')
park_store=$(last_pattern_line "$secondary" \
    'stlxr[[:space:]]+w[0-9]+, x[0-9]+, \[x[0-9]+\]$')
park_dsb=$(first_pattern_after "$secondary" 'dsb[[:space:]]+ishst' "$park_store")
park_sev=$(first_pattern_after "$secondary" '[[:space:]]sev([[:space:]]|$)' "$park_dsb")
park_continue=$(next_instruction_line "$secondary" "$park_sev")
require_line_contract "$secondary" "$park_continue" \
    "[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<$continue_to_g8h_symbol>$" \
    'CPU1 PARKED successi direct G8h continuation edge taşımıyor'
require_order 'CPU1 PPI/post-count/final-publication/PARKED/SEV/G8h' \
    "$ppi_call" "$post_ppi_count" "$ownership_off" "$park_load" \
    "$park_store" "$park_dsb" "$park_sev" "$park_continue"
[ "$(call_count "$secondary" "$continue_to_g8h_symbol")" -eq 1 ] || \
    fail 'CPU1 direct G8h continuation edge exact bir değil'
[ "$(instruction_count "$secondary" '[[:space:]]wfe([[:space:]]|$)')" -eq 2 ] || \
    fail 'CPU1 yalnız iki bounded coordination WFE yüzeyi taşımıyor'
if awk -v start="$park_sev" '
    NR > start && /[[:space:]]wfe([[:space:]]|$)/ { found=1 }
    END { exit(found ? 0 : 1) }
' "$secondary"; then
    fail 'CPU1 PARKED sonrası G8h continuation öncesi WFE içeriyor'
fi
require_no_return_surface "$secondary" 'CPU1 terminal runtime'
require_contract "$secondary" 'cmp[[:space:]]+x[0-9]+, #0x3' \
    'CPU1 PARKED CAS prior IRQ2 stage 3 kontrolü yok'
require_contract "$secondary" 'mov[[:space:]]+w[0-9]+, #0x4' \
    'CPU1 PARKED CAS new stage 4 değeri yok'
post_ppi_acquires=$(awk -v start="$post_ppi_count" -v stop="$ownership_off" '
    NR > start && NR < stop && /ldar[[:space:]]+x[0-9]+, \[x[0-9]+\]$/ { count++ }
    END { print count + 0 }
' "$secondary")
[ "$post_ppi_acquires" -ge 5 ] || \
    fail "CPU1 PPI sonrası quiescence Acquire recheck yetersiz: $post_ppi_acquires"

# CPU0 captures first, publishes RELEASE with DSB+SEV, acknowledges ARMED,
# Acquire-observes PARKED, validates the full evidence set, and only then
# reaches the first of four marker writes.
capture=$(pattern_line "$primary" 'mrs[[:space:]]+x[0-9]+, CNTVCT_EL0')
capture_publish=$(first_pattern_after "$primary" \
    'stlr[[:space:]]+x[0-9]+, \[x[0-9]+\]$' "$capture")
release_load=$(first_pattern_after "$primary" \
    'ldaxrb[[:space:]]+w[0-9]+, \[x[0-9]+\]$' "$capture_publish")
release_store=$(first_pattern_after "$primary" \
    'stlxrb[[:space:]]+w[0-9]+, w[0-9]+, \[x[0-9]+\]$' "$release_load")
release_dsb=$(first_pattern_after "$primary" 'dsb[[:space:]]+ishst' "$release_store")
release_sev=$(first_pattern_after "$primary" '[[:space:]]sev([[:space:]]|$)' "$release_dsb")
armed_observe=$(first_pattern_after "$primary" \
    'cmp[[:space:]]+x[0-9]+, #0x1' "$release_sev")
armed_ack_store=$(nth_pattern_line "$primary" \
    'stlxrb[[:space:]]+w[0-9]+, w[0-9]+, \[x[0-9]+\]$' 2)
armed_ack_dsb=$(first_pattern_after "$primary" 'dsb[[:space:]]+ishst' "$armed_ack_store")
armed_ack_sev=$(first_pattern_after "$primary" '[[:space:]]sev([[:space:]]|$)' "$armed_ack_dsb")
parked_observe=$(first_pattern_after "$primary" \
    'cmp[[:space:]]+x[0-9]+, #0x4' "$armed_ack_sev")
first_marker=$(pattern_line "$primary" \
    '[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<[^>]*kernel4uart4Uart[^>]*core3fmt5Write9write_fmt[^>]*>$')
require_order 'CPU0 capture/RELEASE/ARMED-ack/PARKED/evidence/marker' \
    "$capture" "$capture_publish" "$release_load" "$release_store" \
    "$release_dsb" "$release_sev" "$armed_observe" "$armed_ack_store" \
    "$armed_ack_dsb" "$armed_ack_sev" "$parked_observe" "$first_marker"
marker_calls=$(instruction_count "$primary" \
    '[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<[^>]*kernel4uart4Uart[^>]*core3fmt5Write9write_fmt[^>]*>$')
[ "$marker_calls" -eq 4 ] || fail "CPU0 marker write sayısı exact dört değil: $marker_calls"
last_marker=$(last_pattern_line "$primary" \
    '[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<[^>]*kernel4uart4Uart[^>]*core3fmt5Write9write_fmt[^>]*>$')
g8h_primary_arg1=$(next_instruction_line "$primary" "$last_marker")
require_line_contract "$primary" "$g8h_primary_arg1" \
    '[[:space:]]ldr[[:space:]]+x1, \[sp, #0x60\]$' \
    'CPU0 G8h handoff second argümanı validated third check değil'
g8h_primary_arg0=$(next_instruction_line "$primary" "$g8h_primary_arg1")
require_line_contract "$primary" "$g8h_primary_arg0" \
    '[[:space:]]mov[[:space:]]+x0, x25' \
    'CPU0 G8h handoff first argümanı final_ticks değil'
g8h_primary_call=$(next_instruction_line "$primary" "$g8h_primary_arg0")
require_line_contract "$primary" "$g8h_primary_call" \
    '[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<rpi5_g8h_primary_run>$' \
    'CPU0 BOOT8G final marker sonrası direct G8h handoff yok'
[ "$(call_count "$primary" rpi5_g8h_primary_run)" -eq 1 ] || \
    fail 'CPU0 direct G8h handoff edge exact bir değil'
[ "$(instruction_count "$primary" '[[:space:]]wfe([[:space:]]|$)')" -eq 0 ] || \
    fail 'CPU0 G8h handoff öncesi historical WFE yüzeyi kalmış'
require_no_return_surface "$primary" 'CPU0 no-return runtime'
evidence_acquires=$(awk -v start="$parked_observe" -v stop="$first_marker" '
    NR > start && NR < stop && /ldar(b)?[[:space:]]+[wx][0-9]+, \[x[0-9]+\]$/ { count++ }
    END { print count + 0 }
' "$primary")
[ "$evidence_acquires" -ge 30 ] || \
    fail "PARKED sonrası marker-öncesi evidence Acquire sayısı yetersiz: $evidence_acquires"

# The historical CPU0 compatibility tick address is now hoisted once across
# both required Acquire reads: one before release and one after PARKED.  The
# address register remains read-only until a definite overwrite, and no other
# bounded G8g function obtains the TICKS address.
ticks_primary_refs=$(grep -Ec \
    "[[:space:]]adr[[:space:]]+x[0-9]+, (0x)?[[:xdigit:]]+[[:space:]]+<$ticks_symbol>$" \
    "$primary" || true)
[ "$ticks_primary_refs" -eq 1 ] || \
    fail "CPU0 TICKS symbolic reference sayısı exact bir değil: $ticks_primary_refs"
ticks_ref=$(grep -nE \
    "[[:space:]]adr[[:space:]]+x[0-9]+, (0x)?[[:xdigit:]]+[[:space:]]+<$ticks_symbol>$" \
    "$primary" | sed -n '1s/:.*//p')
require_line_contract "$primary" "$ticks_ref" \
    "[[:space:]]adr[[:space:]]+x24, (0x)?[[:xdigit:]]+[[:space:]]+<$ticks_symbol>$" \
    'CPU0 hoisted TICKS adresi expected x24 symbolic resolution değil'
ticks_load1=$(first_pattern_after "$primary" \
    'ldar[[:space:]]+x19, \[x24\]$' "$ticks_ref")
require_line_contract "$primary" "$ticks_load1" \
    '[[:space:]]ldar[[:space:]]+x19, \[x24\]$' \
    'CPU0 base TICKS symbolic addressi Acquire load ile tüketilmiyor'
[ "$(instruction_count_between "$primary" "$ticks_ref" "$ticks_load1")" -eq 4 ] || \
    fail 'CPU0 base TICKS address-to-Acquire windowu exact değil'
ticks_load2=$(first_pattern_after "$primary" \
    'ldar[[:space:]]+x25, \[x24\]$' "$ticks_load1")
require_line_contract "$primary" "$ticks_load2" \
    '[[:space:]]ldar[[:space:]]+x25, \[x24\]$' \
    'CPU0 final TICKS hoisted addressi Acquire load ile tüketilmiyor'
ticks_addr_kill=$(first_pattern_after "$primary" \
    'adrp[[:space:]]+x24,' "$ticks_load2")
require_line_contract "$primary" "$ticks_addr_kill" \
    '[[:space:]]adrp[[:space:]]+x24,' \
    'CPU0 TICKS address registerı expected definite overwrite ile öldürülmüyor'
ticks_early_overwrite=$(awk -v start="$ticks_ref" -v stop="$ticks_addr_kill" '
    NR > start && NR < stop &&
        (/^[[:space:]]*[[:xdigit:]]+:[[:space:]]+[[:alnum:].]+[[:space:]]+[wx]24([,[:space:]]|$)/ ||
         /^[[:space:]]*[[:xdigit:]]+:[[:space:]]+ldp[[:space:]]+[wx][0-9]+, [wx]24,/) { print }
' "$primary")
[ -z "$ticks_early_overwrite" ] || \
    fail "CPU0 TICKS address registerı expected lifetime öncesi değişiyor: $ticks_early_overwrite"
ticks_acquire_uses=$(awk -v start="$ticks_ref" -v stop="$ticks_addr_kill" '
    NR > start && NR < stop && /ldar[[:space:]]+x(19|25), \[x24\]$/ { count++ }
    END { print count + 0 }
' "$primary")
[ "$ticks_acquire_uses" -eq 2 ] || \
    fail "CPU0 TICKS address registerı exact iki Acquire load taşımıyor: $ticks_acquire_uses"
ticks_unsafe_use=$(awk -v start="$ticks_ref" -v stop="$ticks_addr_kill" '
    NR > start && NR < stop &&
        (/[[:space:]](stp|stnp|str|stur|stlr|stxr|stlxr)[[:space:]].*\[x24/ ||
         /[[:space:]]mov[[:space:]]+x[0-9]+, x24/ ||
         /[[:space:]]add[[:space:]]+x[0-9]+, x24,/) { print }
' "$primary")
[ -z "$ticks_unsafe_use" ] || \
    fail "CPU0 TICKS addressi Acquire dışında kullanılıyor: $ticks_unsafe_use"
require_order 'CPU0 frozen historical TICKS before/release/PARKED/after/marker' \
    "$ticks_ref" "$ticks_load1" "$release_store" "$parked_observe" \
    "$ticks_load2" "$ticks_addr_kill" "$first_marker"
ticks_all_refs=$(awk -v symbol="<$ticks_symbol>" '
    index($0, symbol) != 0 && /[[:space:]]adr[[:space:]]+x[0-9]+,/ { count++ }
    END { print count + 0 }
' "$ppi" "$released" "$active" "$prerequisite_complete" \
    "$continue_to_g8h" "$primary_require" "$secondary" "$handler" \
    "$timer_snapshot" "$timer_prepare" "$timer_advance" "$timer_disable" \
    "$secondary_fail" "$consume_error" "$publish_error" "$primary" \
    "$primary_fail" "$error_name" "$primary_closure0" "$primary_closure1" \
    "$primary_closure2" "$primary_closure3" "$primary_closure4" \
    "$primary_closure5" "$primary_closure6")
[ "$ticks_all_refs" -eq 1 ] || \
    fail "bounded G8g TICKS address yüzeyi exact bir hoisted read-only reference değil: $ticks_all_refs"
boot_store=$(nth_pattern_line "$primary" \
    'stlxrb[[:space:]]+w[0-9]+, w[0-9]+, \[x[0-9]+\]$' 3)
[ -n "$boot_store" ] && [ "$boot_store" -lt "$first_marker" ] || \
    fail 'BOOT8G exact-once CAS bütün markerların önünde değil'
if grep -Eq 'msr[[:space:]]+CNT[PV]_(CTL|CVAL|TVAL)_EL0' "$primary"; then
    fail 'G8g CPU0 yolu local timer registerına yazıyor'
fi

# Narrow bounded G8g CPU1 surfaces may not grow panic, indirect call,
# UART/scheduler/heap, SGI, TLBI, PSCI, GIC configuration, CPU2/3, or FP/SIMD
# edges.  Raw EOI in the handler is explicitly required above.
[ "$(call_count "$primary" "$error_name_symbol")" -eq 1 ] || \
    fail 'CPU0 error-name helper edge exact bir değil'
[ "$(call_count "$primary" "$primary_fail_symbol")" -eq 27 ] || \
    fail 'CPU0 direct primary-fail edge yüzeyi exact yirmi yedi değil'
[ "$(call_count "$primary" "$primary_require_symbol")" -eq 2 ] || \
    fail 'CPU0 factored primary_require edge exact iki değil'
[ "$(call_count "$primary_require" "$primary_fail_symbol")" -eq 1 ] || \
    fail 'CPU0 primary_require fail-closed primary_fail edge taşımıyor'
[ "$(instruction_count "$primary_require" '[[:space:]]bl[[:space:]]')" -eq 1 ] || \
    fail 'CPU0 primary_require çağrı yüzeyi exact bir değil'
for closure_symbol in \
    "$primary_closure0_symbol" "$primary_closure1_symbol" \
    "$primary_closure2_symbol" "$primary_closure3_symbol" \
    "$primary_closure4_symbol" "$primary_closure5_symbol" \
    "$primary_closure6_symbol"; do
    [ "$(call_count "$primary" "$closure_symbol")" -eq 1 ] || \
        fail "CPU0 checked-arithmetic fail closure edge exact bir değil: $closure_symbol"
done
for closure_body in \
    "$primary_closure0" "$primary_closure1" "$primary_closure2" \
    "$primary_closure3" "$primary_closure4" "$primary_closure5" \
    "$primary_closure6"; do
    [ "$(call_count "$closure_body" "$primary_fail_symbol")" -eq 1 ] || \
        fail "CPU0 checked-arithmetic closure primary_fail'e direct bağlı değil: $closure_body"
    [ "$(instruction_count "$closure_body" '[[:space:]]bl[[:space:]]')" -eq 1 ] || \
        fail "CPU0 checked-arithmetic closure çağrı yüzeyi exact bir değil: $closure_body"
done
[ "$(instruction_count "$primary_fail" '[[:space:]]bl[[:space:]]')" -eq 1 ] || \
    fail 'CPU0 primary_fail yalnız bounded marker formatter çağrısı taşımıyor'
require_contract "$primary_fail" \
    '[[:space:]]bl[[:space:]]+(0x)?[[:xdigit:]]+[[:space:]]+<[^>]*core3fmt5write>$' \
    'CPU0 primary_fail exact formatter edge taşımıyor'
[ "$(instruction_count "$primary_fail" '[[:space:]]wfe([[:space:]]|$)')" -eq 1 ] || \
    fail 'CPU0 primary_fail terminal WFE yüzeyi exact bir değil'
primary_fail_marker=$(call_line "$primary_fail" '_RNvNtCslRlV1jPdCox_4core3fmt5write')
require_terminal_wfe_loop "$primary_fail" "$primary_fail_marker" \
    'CPU0 primary_fail yolu'
require_no_return_surface "$primary_fail" 'CPU0 primary_fail no-return helperı'
[ "$(instruction_count "$secondary_fail" '[[:space:]]wfe([[:space:]]|$)')" -eq 1 ] || \
    fail 'CPU1 secondary_fail terminal WFE yüzeyi exact bir değil'
secondary_fail_sev=$(last_pattern_line "$secondary_fail" '[[:space:]]sev([[:space:]]|$)')
require_terminal_wfe_loop "$secondary_fail" "$secondary_fail_sev" \
    'CPU1 secondary_fail yolu'
require_no_return_surface "$secondary_fail" 'CPU1 secondary_fail no-return helperı'
[ "$(instruction_count "$error_name" '[[:space:]]bl[[:space:]]')" -eq 0 ] || \
    fail 'CPU0 error_name beklenmeyen call edge içeriyor'

for no_msr_body in \
    "$ppi" "$released" "$active" "$prerequisite_complete" \
    "$continue_to_g8h" "$primary_require" "$error_name" "$primary_fail" \
    "$primary_closure0" "$primary_closure1" "$primary_closure2" \
    "$primary_closure3" "$primary_closure4" "$primary_closure5" \
    "$primary_closure6"; do
    require_msr_surface "$no_msr_body" 0 'a^' 'bounded G8g read-only/helper'
done
require_msr_surface "$secondary" 2 \
    '[[:space:]]msr[[:space:]]+DAIF(Set|Clr), #0x2$' \
    'G8g CPU1 runtime'
[ "$(instruction_count "$secondary" 'msr[[:space:]]+DAIFSet, #0x2$')" -eq 1 ] && \
    [ "$(instruction_count "$secondary" 'msr[[:space:]]+DAIFClr, #0x2$')" -eq 1 ] || \
    fail 'G8g CPU1 runtime exact mask-then-unmask DAIF yüzeyi taşımıyor'
require_msr_surface "$handler" 15 \
    '[[:space:]]msr[[:space:]]+(DAIFSet, #0x2|CNTV_CTL_EL0, x[0-9]+)$' \
    'G8g IRQ handler'
[ "$(instruction_count "$handler" 'msr[[:space:]]+DAIFSet, #0x2$')" -eq 10 ] && \
    [ "$(instruction_count "$handler" 'msr[[:space:]]+CNTV_CTL_EL0, x[0-9]+$')" -eq 5 ] || \
    fail 'G8g IRQ handler exact error-mask/local-disable MSR yüzeyi taşımıyor'
require_msr_surface "$secondary_fail" 2 \
    '[[:space:]]msr[[:space:]]+(DAIFSet, #0x2|CNTV_CTL_EL0, x[0-9]+)$' \
    'G8g secondary_fail'
[ "$(instruction_count "$secondary_fail" 'msr[[:space:]]+DAIFSet, #0x2$')" -eq 1 ] && \
    [ "$(instruction_count "$secondary_fail" 'msr[[:space:]]+CNTV_CTL_EL0, x[0-9]+$')" -eq 1 ] || \
    fail 'G8g secondary_fail exact DAIF/timer-disable MSR yüzeyi taşımıyor'
require_msr_surface "$consume_error" 3 \
    '[[:space:]]msr[[:space:]]+(DAIFSet, #0x2|CNTV_CTL_EL0, x[0-9]+)$' \
    'G8g consume_irq_error'
[ "$(instruction_count "$consume_error" 'msr[[:space:]]+DAIFSet, #0x2$')" -eq 2 ] && \
    [ "$(instruction_count "$consume_error" 'msr[[:space:]]+CNTV_CTL_EL0, x[0-9]+$')" -eq 1 ] || \
    fail 'G8g consume_irq_error exact DAIF/timer-disable MSR yüzeyi taşımıyor'
require_msr_surface "$publish_error" 2 \
    '[[:space:]]msr[[:space:]]+(DAIFSet, #0x2|CNTV_CTL_EL0, x[0-9]+)$' \
    'G8g publish_secondary_error'
[ "$(instruction_count "$publish_error" 'msr[[:space:]]+DAIFSet, #0x2$')" -eq 1 ] && \
    [ "$(instruction_count "$publish_error" 'msr[[:space:]]+CNTV_CTL_EL0, x[0-9]+$')" -eq 1 ] || \
    fail 'G8g publish_secondary_error exact DAIF/timer-disable MSR yüzeyi taşımıyor'
require_msr_surface "$primary" 1 \
    '[[:space:]]msr[[:space:]]+DAIFSet, #0x2$' \
    'G8g CPU0 primary'

for bounded in \
    "$ppi" "$released" "$active" "$prerequisite_complete" \
    "$continue_to_g8h" "$primary_require" "$secondary" "$handler" \
    "$timer_snapshot" "$timer_prepare" "$timer_advance" "$timer_disable" \
    "$secondary_fail" "$consume_error" "$publish_error" "$primary" \
    "$primary_fail" "$error_name" "$primary_closure0" "$primary_closure1" \
    "$primary_closure2" "$primary_closure3" "$primary_closure4" \
    "$primary_closure5" "$primary_closure6"; do
    require_no_indirect "$bounded" 'bounded G8g function'
    require_no_panic_edge "$bounded" 'bounded G8g function'
    bad_global_transfer=$(grep -E "$direct_cf_target_pattern" "$bounded" | grep -Ei \
        '<[^>]*(scheduler|context_switch|spawn_kernel_task|yield_now|send_sgi|SGIR|tlbi|shootdown|psci|cpu_on|bring_up_secondary|alloc|dealloc|realloc|exchange_malloc|box_|gic[^>]*(init|write|send|clear|deactivat|cpend|icactive)|cpu[_-]?[23])[^>]*>$' || true)
    [ -z "$bad_global_transfer" ] || \
        fail "G8g yasak scheduler/heap/SGI/GIC-write/SMP edge içeriyor: $bad_global_transfer"
    if grep -Eq '[[:space:]](tlbi|smc|hvc)[[:space:]]' "$bounded"; then
        fail "G8g TLBI/PSCI instruction içeriyor: $bounded"
    fi
    if grep -Eq "$fp_surface_pattern" "$bounded"; then
        fail "G8g FP=TRAP kapsamı FP/SIMD registerı kullanıyor: $bounded"
    fi
done
for cpu1_body in \
    "$ppi" "$released" "$active" "$prerequisite_complete" \
    "$continue_to_g8h" "$secondary" "$handler" \
    "$timer_snapshot" "$timer_prepare" "$timer_advance" "$timer_disable" \
    "$secondary_fail" "$consume_error" "$publish_error"; do
    bad_transfer=$(grep -E "$direct_cf_target_pattern" "$cpu1_body" | grep -Ei \
        '<[^>]*(uart|fmt5write|scheduler|context_switch|spawn_kernel_task|yield_now|send_sgi|SGIR|tlbi|shootdown|psci|cpu_on|bring_up_secondary|alloc|dealloc|realloc|exchange_malloc|box_|gic[^>]*(init|write|send|clear|deactivat|cpend|icactive)|cpu[_-]?[23])[^>]*>$' || true)
    [ -z "$bad_transfer" ] || \
        fail "CPU1 yasak UART/scheduler/heap/SGI/GIC-write/SMP edge içeriyor: $bad_transfer"
done

for marker in \
    'ASELSAN/G8G0 CPU=0 PREREQ=BOOT8F TARGET=CPU1' \
    'ASELSAN/G8G1 REPORTER=CPU0 CPU=1' \
    'ASELSAN/G8G2 REPORTER=CPU0 CPU=1' \
    'ASELSAN/BOOT8G TIMER=PER_CPU CPU0_SLOT=' \
    'ASELSAN/G8GERR CODE='; do
    marker_count=$(strings "$kernel" | grep -Fc "$marker" || true)
    [ "$marker_count" -eq 1 ] || \
        fail "G8g marker ELF içinde exact-once değil: $marker (count=$marker_count)"
done

echo 'PASS: G8g production AArch64 layout has exact bounded symbols, direct G8f continuation CFG, G8g-first IRQ ownership, two ordered PPI27 EOI/evidence publications, active third-deadline/PPI quiescence proof, CPU0-only markers, and no panic/indirect/UART/task/heap/SGI/TLBI/GIC-write expansion'
snippet sha256: 239494a8e915file sha256: 239494a8e915
02 · Kapı kimlik kaydı

Operations sıra, kimlik ve başlık bağı

tam Operations kaydıL29234–L29323
website/src/lib/operations.ts::rpi5-g8g-production-layout-green
  {
    id: "rpi5-g8g-production-layout-green",
    date: "2026-08-22",
    sequence: 86,
    status: "verified",
    title: "G8g hardened production machine-code ve layout kapısı yeşil",
    summary:
      "Sıra 85 RPi5 wiring kabulünden sonra gerçek production AArch64 ELF'i hardened, function-bounded makine-kodu/layout kapısından ve bağımsız incelemeden geçti. Gate peeled iki G8f release-poll call-site'ını ayrı true/false/WFE/no-return-run CFG segmentleri olarak; primary-run/interceptor çağrılarını exact direct BL olarak; G8g active predicate, dispatcher ownership, PPI27 bounds, exact iki EOIR→DSB/ISB→evidence sırası, stage CAS, full third-deadline loop, TICKS freeze/address lifetime, no-return terminal akışlar ve geniş forbidden instruction/call/store yüzeyini semantik olarak bağlar. İlk mevcut-ELF GREEN script false-negative açıklıkları nedeniyle kabul edilmedi; parser self-fixture'ları ve provenance/CFG kapıları eklendi, ara plain-b target false RED'i düzeltildi ve GIC shift panic edge'i checked_shl ile kaldırıldı. Final `make verify-rpi5-g8g-layout` exit 0; contract/runtime/integration 27/14/6=47/47, actual RPi5 build ve G8/G8b/G8c/G8d/G8e/G8f/G8g layout zinciri PASS, reviewer GO. ELF 7.692.096 B / 91697a37…54f1b8. Bu layout kabulüdür: Sıra 87 tam matris, reproducibility, image/package, microSD, UART ve fiziksel BOOT8G hâlâ STOP'tur; son fiziksel PASS Sıra 80 BOOT8F'tir.",
    evidence: [
      "Değişmeyen fiziksel prerequisite Sıra 80 BOOT8F raw'ıdır: 17.363 B, mode 0444, e70e1a9a2cf35f9079ee1b1a73d992106bf5ee9a19f1bbf2628582e836ea5068, direct validator PASS ve SCOPE=QUIESCENT_ATOMIC_HANDOFF_ONLY.",
      "Hardened `scripts/verify-rpi5-g8g-layout.sh` exact 100.507 B / a42b613fb90dde061db2f6593eef42f0c77a3462c1dae184ac39bf4bd6d3aa20; `sh -n` ve kendi adversarial parser/gate fixture'ları PASS'tir.",
      "Yeni layout hedefini taşıyan Makefile exact 17.405 B / fe9616783f78f132f62847b24e78f6c2c99f31e8441989aaa9aa923dde1b6a9e.",
      "PPI mask shift'ini checked_shl ile bound ederek release panic edge'ini kaldıran GIC exact 18.332 B / 7a5e876413389d2cb7d3e0eb3902dee1a56c7cb24e7ab188766763011333f8d9.",
      "Bounded runtime davranışı değişmeyen `rpi5_g8g.rs` exact 37.958 B / 7f09aa1cf4df43c65ca80db7a97bff21a73e3e8a480fef4524bb44d058dc7545.",
      "Per-CPU timer implementation exact 18.169 B / 35edb3758192aa23877962b92b6ab81e858a2523726d174069d6c17e231855d2 olarak kaldı.",
      "Final production RPi5 ELF exact 7.692.096 B / 91697a37a0f4cf07da9406184a2eba340fafc36f5955302043946ab69154f1b8; bu layout girdisidir, flat image/package değildir.",
      "`make verify-rpi5-g8g-layout` exit 0: contract 27/27 + runtime 14/14 + integration 6/6 = 47/47, canonical CLI ve actual AArch64/RPi5 production build PASS.",
      "Tarihsel G8, G8b, G8c, G8d, G8e ve G8f production layout kapıları ile yeni G8g layout kapısı aynı final ELF üzerinde PASS'tir.",
      "LLVM'nin peeled release poll'ü için iki direct BL exact iki CFG segmentine bağlanır; primary-run, secondary-run hedefleri ve interceptor direct/no-indirect/no-return şartları function sınırlarında doğrulanır.",
      "Dispatcher G8g→G8e→G8d→G8b→generic timer segmentleri, handled branch/false fallthrough/shared return; active predicate CPU1 MPIDR + Acquire ownership true/false CFG'si ile kanıtlanır.",
      "PPI snapshot INTID aralığı 16..32, checked shift, exact GIC base/mask/yedi read ve yalnız sret write ile read-only'dir; handler raw ACK/INTID 27 ve exact iki EOIR base/payload→DSB/ISB→evidence sırasını taşır.",
      "Stage CAS old/new/base ve failure target'ları, CPU1 `[d3,d3+period)` active third-check loop'u, post-deadline PPI recheck'i ve CPU0 exact iki Acquire TICKS read/no-store/address-lifetime kapıları GREEN'dir.",
      "Primary, fail, secondary, IRQ, error-name ve checked arithmetic closure'ları transitive audit içindedir; panic, forbidden direct/indirect/PAC, FP/SIMD/SVE/SME, FPCR/MSR ve WFE→RET drift self-fixture'ları fail-closed reddedilir.",
      "İlk current-ELF GREEN script reviewer tarafından false-negative alanları nedeniyle reddedildi; hardened final tekrar ve bağımsız reviewer blocker olmadan GO verdi. Ara plain `b` target parser false RED'i kabul sayılmadan düzeltildi.",
      "Sıra 86 production layout proof exact 9.890 B / 72cc342a14c0823dc53906db458e209ebb33164eb6673c3321c4afc164b13731.",
      "Updated staged proof exact 11.258 B / e7f2e9d47b74ce7adce7a5a85449b8175db96a954057bc38dee93a390daa04ff.",
      "Güncellenmiş Sıra 87–93 roadmap exact 30.082 B / a9a59df812f6f15986ff6a0fb4ddd356698d5f128b445a5fd09dac56ed698b55; sıradaki tek yetkili işlem Sıra 87 tam regresyon matrisidir.",
    ],
    terminalSessionsNote:
      "Oturumlar final production ELF'in hardened function-bounded layout kabulünü ve önceki layout regresyonlarını gösterir. Flat image, microSD veya fiziksel BOOT8G kanıtı değildir.",
    terminalSessions: [
      {
        id: "g8g-sequence86-hardened-layout-gate",
        title: "Function-bounded G8g CFG, IRQ, timer ve evidence kapısı",
        commandLines: [
          "make verify-rpi5-g8g-layout",
          "inspect exact symbol bounds and production AArch64 disassembly",
          "run embedded adversarial parser/gate self-fixtures",
        ],
        outputLines: [
          "contract/runtime/integration=27/14/6=47/47 PASS",
          "actual AArch64/RPi5 build=PASS · G8g layout=PASS",
          "peeled release poll CFG + predicate + EOIR/barrier + third-check=PASS",
          "exit=0",
        ],
        exitCode: 0,
        outputMode: "complete",
      },
      {
        id: "g8g-sequence86-historical-layouts",
        title: "Aynı ELF üzerinde tarihsel layout regresyon zinciri",
        commandLines: [
          "verify G8, G8b, G8c, G8d, G8e and G8f production layouts",
          "verify G8g production layout last",
        ],
        outputLines: [
          "G8/G8b/G8c/G8d/G8e/G8f/G8g layouts=PASS",
          "ELF=7692096 B",
          "sha256=91697a37a0f4cf07da9406184a2eba340fafc36f5955302043946ab69154f1b8",
        ],
        exitCode: 0,
        outputMode: "complete",
      },
      {
        id: "g8g-sequence86-review-hardening",
        title: "İlk false-negative yüzeyleri ve bağımsız final karar",
        commandLines: [
          "reject initial current-ELF-green gate after semantic audit",
          "harden CFG/provenance/self-fixtures and fix checked PPI shift",
          "independent rerun and reviewer audit",
        ],
        outputLines: [
          "initial current-ELF green=REJECTED · not accepted as checkpoint",
          "plain-b parser false RED=corrected",
          "hardened final gate=PASS",
          "independent reviewer=GO · matrix/image/physical=STOP",
        ],
        exitCode: 0,
        outputMode: "selected",
      },
    ],
    limitations: [
      "Bu kayıt yalnız mevcut production RPi5 ELF'teki function-bounded G8g ve tarihsel G8–G8f machine-code/layout kanıtıdır; tam regresyon matrisi veya fiziksel BOOT8G PASS değildir.",
      "Sıra 87 workspace, RPi4 dahil beş board/feature profili, tarihsel kapılar ve QEMU smoke tamamlanmadan reproducibility başlamaz.",
      "ELF flat payload/image/package olarak dondurulmadı; üç temiz üretim, DTB/config/manifest freeze ve artifact promotion yapılmadı.",
      "microSD, UART, Debug Probe ve Pi güç durumuna dokunulmadı. Son fiziksel PASS Sıra 80 BOOT8F'tir.",
      "Generic SMP, CPU1 preemption, runqueue, migration, TLBI, CPU2/CPU3, soak ve hotplug kapalıdır.",
      "Production deployment dirty/untracked workspace ve stale 47d22c9 source etiketiyle yapılır; canlı artifact doğrulansa da Git-provider provenance kurulmuş sayılmaz.",
    ],
  },
snippet sha256: d82c723aed13file sha256: 9726dbf00f84
Kayıtlı yürütme/kanıt komutu
make verify-rpi5-g8g-layout
Registry schema v5 · generator website/scripts/generate-code-gates.mjs · Tam SHA-256: 3050638b71a684d8f8f947a8a6faa237a17fa8db5dc0db04fb207b668b462af9