Skip to content

native_api_reference.md

Latest commit

 

History

History
204 lines (149 loc) · 5.74 KB

native_api_reference.md

File metadata and controls

204 lines (149 loc) · 5.74 KB
Raw

Native API and checked proof reference

This reference is generated from the selected C header and Lean source. The default corpus is src/scpn_control/core/solver.h and lean/SCPNControl/PulsedFSM.lean. The selected C header is the normative ABI contract. The Lean section describes only the checked finite-state model; it is not evidence of continuous plant or plasma safety.

C ABI version 1

ABI version: SCPN_SOLVER_ABI_VERSION == 1. Status OK means the call was valid; convergence is reported separately by the convergence function.

scpn_solver_create_v1

Allocate a fixed-boundary Grad-Shafranov SOR state.

nr and nz are point counts and must each be at least 3. Radial and vertical bounds are finite metres with r_max > r_min and z_max > z_min. On success, *solver_out becomes a library-owned opaque handle whose initial poloidal-flux state and boundary are zero. The caller owns that handle and must pass it exactly once to scpn_solver_destroy_v1. On failure, a non-null solver_out is set to null. This operation is deterministic apart from allocation success and does not retain pointers supplied by the caller.

scpn_solver_status_v1 scpn_solver_create_v1(
    int nr,
    int nz,
    double r_min,
    double r_max,
    double z_min,
    double z_max,
    scpn_solver_v1** solver_out
);

scpn_solver_set_boundary_dirichlet_v1

Set the Dirichlet value on every edge point of solver.

boundary_value is finite poloidal flux in the same convention and units as the solution array (Wb/rad in this kernel). The call mutates only the referenced handle. Concurrent calls on the same handle are unsupported; distinct handles share no mutable state.

scpn_solver_status_v1 scpn_solver_set_boundary_dirichlet_v1(
    scpn_solver_v1* solver,
    double boundary_value
);

scpn_solver_run_steps_v1

Execute a fixed number of red-black SOR sweeps with omega = 1.5.

source and psi_out each address exactly size == nz * nr doubles in C row-major [nz][nr] order. source is read-only, finite, and already scaled as the elliptic right-hand side in solution-units per square metre; it is not interpreted as raw current density. psi_out is caller-owned and is overwritten with the complete current solution. The arrays must not overlap. iterations must be non-negative. Results are deterministic for the same ABI, compiler arithmetic, inputs, and initial handle state.

scpn_solver_status_v1 scpn_solver_run_steps_v1(
    scpn_solver_v1* solver,
    const double* source,
    double* psi_out,
    int size,
    int iterations
);

scpn_solver_run_until_converged_v1

Execute red-black SOR sweeps until tolerance or the iteration cap.

Array layout, units, ownership, non-aliasing, determinism, and thread-safety match scpn_solver_run_steps_v1. max_iterations must be positive, omega finite and in (0, 2), and tolerance finite and non-negative in solution units. On OK, all three outputs are written: iterations_used is in [1, max_iterations], final_delta is the maximum absolute update from the final sweep, and converged is 1 exactly when final_delta <= tolerance (otherwise 0). Scientific non-convergence is an OK call outcome, not an ABI error.

scpn_solver_status_v1 scpn_solver_run_until_converged_v1(
    scpn_solver_v1* solver,
    const double* source,
    double* psi_out,
    int size,
    int max_iterations,
    double omega,
    double tolerance,
    int* iterations_used,
    double* final_delta,
    int* converged
);

scpn_solver_destroy_v1

Release a handle returned by scpn_solver_create_v1.

Passing null is a successful no-op. Any non-null handle becomes invalid as soon as this function is called; subsequent use or a second destroy is undefined caller behaviour. The function does not throw across the C ABI.

scpn_solver_status_v1 scpn_solver_destroy_v1(scpn_solver_v1* solver);

Legacy compatibility ABI

These unversioned symbols remain loadable for existing clients. They preserve historical null, zero, or silent error signalling. New clients should use the typed version 1 ABI above.

create_solver

void* create_solver(
    int nr, int nz, double r_min, double r_max, double z_min, double z_max
);

set_boundary_dirichlet

void set_boundary_dirichlet(void* solver, double boundary_value);

run_step

void run_step(
    void* solver, double* source, double* psi_out, int size, int iterations
);

run_step_converged

int run_step_converged(
    void* solver,
    double* source,
    double* psi_out,
    int size,
    int max_iterations,
    double omega,
    double tolerance,
    double* final_delta
);

destroy_solver

void destroy_solver(void* solver);

Lean checked declarations

State

Kind: inductive. The eight ordered phases in one abstract pulsed-control cycle.

next

Kind: def. Return the sole admitted successor of a scheduler state.

actionRank

Kind: def. Map each phase to its zero-based position in the abstract cycle.

stepN

Kind: def. Apply next exactly n times to state.

legalTransition

Kind: def. State that toState is exactly the declared successor of fromState.

adjacent_transition_deterministic

Kind: theorem. Two legal successors of the same state are equal.

pulsed_fsm_eventually_returns_to_idle

Kind: theorem. Every declared state reaches idle in at most eight abstract steps.

idle_returns_to_idle_after_full_cycle

Kind: theorem. Starting at idle, eight abstract steps complete one full cycle.

manual_transition_cannot_skip_burn_from_idle

Kind: theorem. The declared transition relation forbids a direct idle to burn jump.