%% CARRY — Tau-Prolog Braid Kernel
%% Three strands: Curry (σ₁), Crystal (σ₂), C3 (σ₃)
%% Crossings encode state transitions as braid group generators
%% Writhe invariant = net integrity of the pipeline
%%
%% Compatible with Tau-Prolog (ISO Prolog subset)
%% Author: Ahmad <ahmedparr93@gmail.com>
%% License: AGPL-3.0-only

:- module(braid_kernel, [
    strand/2,
    crossing/5,
    braid_word/1,
    writhe/2,
    valid_braid/1,
    braid_step/4,
    entropy_bounded/2,
    strand_position/3,
    braid_invariant/1
]).

%% --- Strand definitions (the three computational fibers) ---

strand(curry,   1).  % σ₁ — position 1 (leftmost)
strand(crystal, 2).  % σ₂ — position 2 (middle)
strand(c3,      3).  % σ₃ — position 3 (rightmost)

%% --- Crossing types ---
%% A positive crossing (σᵢ) = strand i crosses OVER strand i+1
%% A negative crossing (σᵢ⁻¹) = strand i crosses UNDER strand i+1
%% This encodes trust: OVER = active takes authority, UNDER = active yields

crossing(sigma_1, positive, curry, crystal, r1_ffi).
crossing(sigma_2, positive, crystal, c3, r2_native_binding).
crossing(sigma_1_inv, negative, crystal, curry, revert_r1).
crossing(sigma_2_inv, negative, c3, crystal, revert_r2).
crossing(sigma_12, positive, curry, c3, full_descent).

%% --- Braid word: the sequence of crossings that constitutes a valid pipeline ---
%% The canonical CARRY pipeline is: σ₂ · σ₁ (C3 over Crystal, then C3 over Curry)
%% This transfers authority to C3 (hardware execution layer)

braid_word([sigma_2, sigma_1]).

%% --- Writhe number: sum of crossing signs ---
%% +1 for positive (over), -1 for negative (under)
%% Writhe = net "authority taken" through the pipeline
%% Invariant: writhe(canonical) = +2 (two authority transfers, both positive)

crossing_sign(positive, 1).
crossing_sign(negative, -1).

writhe([], 0).
writhe([C|Rest], W) :-
    crossing(C, Sign, _, _, _),
    crossing_sign(Sign, S),
    writhe(Rest, W0),
    W is W0 + S.

%% --- Entropy bound per crossing ---

entropy_ceiling(0.20).

entropy_bounded(Crossing, Entropy) :-
    crossing(Crossing, _, _, _, _),
    entropy_ceiling(Max),
    Entropy =< Max.

%% --- Braid validity: Reidemeister moves preserve topology ---
%% R1: σᵢ · σᵢ⁻¹ = identity (cancel adjacent inverses)
%% R2: σᵢ · σⱼ = σⱼ · σᵢ when |i-j| >= 2 (far commutativity)
%% R3: σᵢ · σᵢ₊₁ · σᵢ = σᵢ₊₁ · σᵢ · σᵢ₊₁ (Yang-Baxter)

cancels(sigma_1, sigma_1_inv).
cancels(sigma_1_inv, sigma_1).
cancels(sigma_2, sigma_2_inv).
cancels(sigma_2_inv, sigma_2).

reduce([], []).
reduce([X], [X]).
reduce([A, B | Rest], Reduced) :-
    cancels(A, B), !,
    reduce(Rest, Reduced).
reduce([A | Rest], [A | Reduced]) :-
    reduce(Rest, Reduced).

valid_braid(Word) :-
    reduce(Word, Reduced),
    Reduced \= [].

%% --- Braid step: transition the FSM via a crossing ---

braid_step(State, Crossing, Entropy, NextState) :-
    entropy_bounded(Crossing, Entropy),
    crossing(Crossing, _, From, To, _),
    state_layer(State, From),
    next_state(State, Crossing, NextState).

%% --- State-to-layer mapping (which strand is active at each DAG node) ---

state_layer(input, curry).
state_layer(memory, crystal).
state_layer(retrieval, c3).
state_layer(transform, c3).
state_layer(constraint, c3).
state_layer(proof, c3).
state_layer(output, c3).

%% --- State transitions via braid crossings ---

next_state(input, sigma_1, memory).
next_state(memory, sigma_2, retrieval).
next_state(retrieval, sigma_12, transform).
next_state(transform, sigma_12, constraint).
next_state(constraint, sigma_12, proof).
next_state(proof, sigma_12, output).
next_state(output, sigma_12, output).

%% --- Strand position tracking (which physical position each strand occupies) ---
%% After σ₁: curry and crystal swap positions
%% After σ₂: crystal and c3 swap positions

strand_position([], curry, 1).
strand_position([], crystal, 2).
strand_position([], c3, 3).

strand_position([sigma_1 | Rest], Strand, Pos) :-
    strand_position(Rest, Strand, Pos0),
    swap_12(Strand, Pos0, Pos).
strand_position([sigma_2 | Rest], Strand, Pos) :-
    strand_position(Rest, Strand, Pos0),
    swap_23(Strand, Pos0, Pos).

swap_12(curry, 1, 2) :- !.
swap_12(curry, 2, 1) :- !.
swap_12(crystal, 1, 2) :- !.
swap_12(crystal, 2, 1) :- !.
swap_12(_, P, P).

swap_23(crystal, 2, 3) :- !.
swap_23(crystal, 3, 2) :- !.
swap_23(c3, 2, 3) :- !.
swap_23(c3, 3, 2) :- !.
swap_23(_, P, P).

%% --- The Braid Invariant ---
%% After the canonical pipeline [σ₁, σ₂]:
%%   curry ends at position 2 (middle)
%%   crystal ends at position 3 (right)
%%   c3 ends at position 1 (left — now has authority)
%% This IS the trust transfer: C3 rises to leftmost = highest authority

braid_invariant(Word) :-
    writhe(Word, W),
    W >= 2,
    strand_position(Word, c3, 1),
    valid_braid(Word).

%% --- Full pipeline proof ---
%% Run the canonical braid word and verify the invariant holds

prove_pipeline :-
    braid_word(W),
    braid_invariant(W),
    writhe(W, Writhe),
    format("CARRY BRAID PROOF~n", []),
    format("  Word:    ~w~n", [W]),
    format("  Writhe:  ~w~n", [Writhe]),
    format("  C3 pos:  1 (AUTHORITY TRANSFERRED)~n", []),
    format("  Status:  INVARIANT HOLDS~n", []).