/*
 * Revera — a real-time kernel with hardware-enforced isolation.
 * Copyright (c) 2026 VIACERTO LLC. All rights reserved.
 *
 * This file is dual-licensed under the PolyForm Noncommercial License 1.0.0 OR
 * a commercial license from VIACERTO LLC. You may choose to use this file under
 * the terms of either license.
 *
 * For the full license terms, see the LICENSE and LICENSE-COMMERCIAL.md files in
 * the root directory of this source tree.
 *
 * SPDX-FileCopyrightText: © 2026 VIACERTO LLC
 * SPDX-License-Identifier: LicenseRef-PolyForm-Noncommercial-1.0.0 OR LicenseRef-VIACERTO-Commercial
 */

/*
 * isolation/main.c — PROVE per-thread stack isolation under full MPU lockdown (ARMv7-M).
 *
 * Two UNPRIVILEGED threads, each with an MPU-isolatable stack (TK_THREAD_STACK -> the .thread_stacks
 * linker zone, power-of-two + naturally aligned). Under TK_CONFIG_UNPRIV_THREADS +
 * TK_CONFIG_ENABLE_MPU_ISOLATION the kernel grants ONLY the running thread's own stack per context
 * switch; every other thread's stack (and the kernel's privileged RAM) is denied to unprivileged code
 * by the MPU. This is freedom-from-interference at the thread level (ADR 0002 review, Bucket C).
 *
 * `worker` just runs. `tripwire` then deliberately writes into worker's stack (a peer). The ARMv7-M MPU
 * BLOCKS that store and raises a MemManage fault BEFORE a single bit of worker's stack changes; this
 * example's tk_fault_report() prints the decode — the blocked address is inside worker's stack — which
 * is the proof. The "ISOLATION FAILED" line after the write can only print if the store completed; it
 * must NOT appear.
 *
 *   make BOARD=nrf52832_pca10040 flash    # watch the debug UART (GP…/UART0 TX), 115200 8N1
 *
 * Needs an MPU arch + the board's .privileged_bss/.thread_stacks linker zones (nRF52's default .ld has
 * them). The Makefile turns on full lockdown; the guard below fails the build if it's not effective.
 */
#include <stdint.h>
#include "tk_kernel.h"     /* TK_THREAD_STACK / tk_thread_* / TK_FEAT_ISOLATION (via tk_config.h) */
#include "tk_time.h"
#include "tk_board.h"
#include "tk_console.h"

#if !TK_FEAT_ISOLATION
#error "isolation needs full lockdown — build it via its Makefile (UNPRIV + MPU_ISOLATION) on an MPU arch (nRF52)."
#endif

/* Isolatable stacks: power-of-two, aligned to their own size, placed in the .thread_stacks MPU zone.
 * Each is exactly what the MPU grants to its thread while running (and denies to every other thread). */
TK_THREAD_STACK(worker_stack,   2048);
TK_THREAD_STACK(tripwire_stack, 2048);

/* Compact hex printer for the fault decode (tk_print_u32 is decimal only). */
static void print_hex32(uint32_t v)
{
    static const char hexd[] = "0123456789abcdef";
    char buf[11];
    int  i;
    buf[0] = '0'; buf[1] = 'x';
    for (i = 0; i < 8; i++) { buf[2 + i] = hexd[(v >> ((7 - i) * 4)) & 0xFu]; }
    buf[10] = '\0';
    tk_print(buf);
}

static void* worker(void* arg)
{
    (void)arg;
    for (uint32_t i = 0u; ; i++) {
        tk_print("[worker]   running, iter ");
        tk_print_u32(i);
        tk_print("  — my stack is mine alone\n");
        tk_sleep_ms(500u);
    }
    return 0;
}

static void* tripwire(void* arg)
{
    (void)arg;
    tk_sleep_ms(1200u);                          /* let worker run a couple of iterations first */

    tk_print("\n[tripwire] attempting an out-of-bounds write into worker's stack (a peer)...\n");
    tk_print("[tripwire] target &worker_stack[0] = ");
    print_hex32((uint32_t)(uintptr_t)&worker_stack[0]);
    tk_print("\n");

    /* THE VIOLATION. volatile so the optimiser cannot drop this never-read store. The MPU must block
     * it — this store is into the .thread_stacks zone, of which only tripwire's OWN stack is granted. */
    *(volatile tk_stack_cell_t*)&worker_stack[0] = (tk_stack_cell_t)0x55u;

    /* Reached only if the write COMPLETED — i.e. isolation did not hold. */
    tk_print("[tripwire] !!! WROTE INTO PEER STACK — ISOLATION FAILED !!!\n");
    for (;;) { tk_sleep_ms(1000u); }
    return 0;
}

/* Strong override of the arch's weak tk_fault_report(): make the MPU catch VISIBLE. For this violation
 * is_hardfault==0 and the CFSR's MemManage byte has DACCVIOL|MMARVALID, with mmfar == the blocked
 * address (inside worker_stack). The arch halts after this returns (tk_fault_terminal). */
void tk_fault_report(int is_hardfault, uint32_t cfsr, uint32_t hfsr, uint32_t mmfar, uint32_t pc, uint32_t lr);
void tk_fault_report(int is_hardfault, uint32_t cfsr, uint32_t hfsr, uint32_t mmfar, uint32_t pc, uint32_t lr)
{
    (void)hfsr; (void)lr;
    tk_print("\n==== MPU CAUGHT THE VIOLATION (freedom-from-interference held) ====\n");
    tk_print(is_hardfault ? "  fault : HardFault\n" : "  fault : MemManage (MPU)\n");
    tk_print("  cfsr  = "); print_hex32(cfsr);  tk_print("\n");
    tk_print("  addr  = "); print_hex32(mmfar); tk_print("   <- the blocked write, inside worker's stack\n");
    tk_print("  pc    = "); print_hex32(pc);    tk_print("   <- the tripwire store that was stopped\n");
    tk_print("  => the store never completed; worker's stack is intact. Halting.\n");
}

int main(void)
{
    tk_board_init();
    tk_console_init(TK_UART_CH_DEBUG);
    tk_print("\nisolation: per-thread stack isolation under full MPU lockdown (nRF52).\n");
    tk_print("  worker runs; tripwire will try to scribble on worker's stack and the MPU should stop it.\n\n");

    tk_kernel_init();
    tk_time_init();

    /* Both stacks are TK_THREAD_STACK -> isolatable, so create_core's D2 check accepts them. */
    tk_thread_create(worker,   0, worker_stack,   sizeof worker_stack,   TK_PRIO_MIN + 1u);
    tk_thread_create(tripwire, 0, tripwire_stack, sizeof tripwire_stack, TK_PRIO_MIN + 2u);  /* higher: preempts to attack */

    tk_kernel_start();
    return 0;
}