// Attempt: claim 1 = 2 using reflexivity

cppl::kernel::Context ctx;

const auto goal = Proposition::equality(u32(), one32(), two32());

const auto forged = ProofTerm::reflexivity();

const auto result = cppl::kernel::check(ctx, goal, forged, {});

CPPL_CHECK(!result.has_value());

CPPL_CHECK(result.error().kind == RejectionKind::NotDefinitionallyEqual);

// Attempt: instantiate evidence for "forall x. x = x"

// but claim it proves "forall x. x = x + 1"

cppl::kernel::Context ctx;

// Real evidence: forall x : u32. x = x

const auto real_goal = Proposition::for_all(u32(), Proposition::equality(u32(), var0(), var0()));

const auto real_evidence = ProofTerm::forall_introduction(u32(), ProofTerm::reflexivity());

// Wrong restatement: claim it's "forall x. x = x + 1"

const auto wrong_quantified = Proposition::for_all(

u32(), Proposition::equality(u32(), var0(), Term::primitive(PrimOp::AddWrap, kU32, {var0(), one32()})));

// Try to eliminate with wrong restatement

const auto forged = ProofTerm::forall_elimination(wrong_quantified, real_evidence, zero32());

// Goal would be 0 = 1 if accepted

const auto attack_goal = Proposition::equality(u32(), zero32(), one32());

const auto result = cppl::kernel::check(ctx, attack_goal, forged, {});

CPPL_CHECK(!result.has_value());

// Attempt: use hypothesis 0 without any implication introduction

cppl::kernel::Context ctx;

const auto goal = Proposition::equality(u32(), zero32(), zero32());

const auto forged = ProofTerm::hypothesis(cppl::kernel::HypothesisIndex{0});

const auto result = cppl::kernel::check(ctx, goal, forged, {});

CPPL_CHECK(!result.has_value());

// Attempt: use hypothesis 1 when only hypothesis 0 exists

cppl::kernel::Context ctx;

// Goal: (0 = 0) -> (0 = 0)

const auto eq = Proposition::equality(u32(), zero32(), zero32());

const auto goal = Proposition::implication(eq, eq);

// Body tries to use hypothesis 1 instead of 0

const auto wrong_hyp = ProofTerm::hypothesis(cppl::kernel::HypothesisIndex{1});

const auto forged = ProofTerm::implication_introduction(eq, wrong_hyp);

const auto result = cppl::kernel::check(ctx, goal, forged, {});

CPPL_CHECK(!result.has_value());

// Attempt: introduce premise P, but use hypothesis claiming to be Q

cppl::kernel::Context ctx;

const auto premise = Proposition::equality(u32(), zero32(), one32());

const auto wrong_conclusion = Proposition::equality(u32(), zero32(), two32());

const auto goal = Proposition::implication(premise, premise);

// Try to use hypothesis but claim it's the wrong thing

const auto forged =

ProofTerm::implication_introduction(premise, ProofTerm::hypothesis(cppl::kernel::HypothesisIndex{0}));

const auto result = cppl::kernel::check(ctx, goal, forged, {});

// This should succeed because hypothesis 0 IS the premise

CPPL_CHECK(result.has_value());

// But this should fail: wrong goal

const auto attack_goal = Proposition::implication(premise, wrong_conclusion);

const auto attack_result = cppl::kernel::check(ctx, attack_goal, forged, {});

CPPL_CHECK(!attack_result.has_value());

// Attempt: eliminate "forall x : u32. P" at an argument of type u8

cppl::kernel::Context ctx;

const auto quantified = Proposition::for_all(u32(), Proposition::equality(u32(), var0(), var0()));

const auto evidence = ProofTerm::forall_introduction(u32(), ProofTerm::reflexivity());

// Try to instantiate at u8 argument instead of u32

const auto wrong_arg = Term::literal(kU8, 0);

const auto forged = ProofTerm::forall_elimination(quantified, evidence, wrong_arg);

// The goal wouldn't even type-check properly

const auto result = cppl::kernel::check(ctx, Proposition::equality(u8(), wrong_arg, wrong_arg), forged, {});

CPPL_CHECK(!result.has_value());

// Attempt: eliminate at a term containing an outer binder variable

cppl::kernel::Context ctx;

// forall y : u32. forall x : u32. x = x

const auto inner = Proposition::for_all(u32(), Proposition::equality(u32(), var0(), var0()));

const auto outer = Proposition::for_all(u32(), inner);

const auto inner_evidence = ProofTerm::forall_introduction(u32(), ProofTerm::reflexivity());

const auto outer_evidence = ProofTerm::forall_introduction(u32(), inner_evidence);

// Verify this works properly

const auto result = cppl::kernel::check(ctx, outer, outer_evidence, {});

CPPL_CHECK(result.has_value());

// Now try to misuse: eliminate inner forall at outer variable

// This tests capture-avoidance

// After introducing outer, var0 refers to the outer binding

// Trying to eliminate inner forall at var0 should either:

// - fail because var0 isn't in scope for the inner elimination

// - correctly substitute without capture

//

// The kernel MUST NOT let this create a confused binding structure

// Test: forall x : u32. forall x : u32. inner_x = inner_x

// The inner x shadows the outer x

cppl::kernel::Context ctx;

const auto inner_body = Proposition::equality(u32(), var0(), var0());

const auto inner = Proposition::for_all(u32(), inner_body);

const auto outer = Proposition::for_all(u32(), inner);

const auto inner_proof = ProofTerm::forall_introduction(u32(), ProofTerm::reflexivity());

const auto outer_proof = ProofTerm::forall_introduction(u32(), inner_proof);

const auto result = cppl::kernel::check(ctx, outer, outer_proof, {});

CPPL_CHECK(result.has_value());

// Now try to construct invalid evidence that confuses the binding levels

// forall x. (eliminate (forall x. x = x) at outer_x)

// This should either work correctly or fail cleanly, never produce garbage

// Attempt: use equality at type u32 to rewrite proposition at type u8

cppl::kernel::Context ctx;

// Have: 0 = 0 at u32

const auto eq_u32 = Proposition::equality(u32(), zero32(), zero32());

const auto eq_evidence = ProofTerm::reflexivity();

// Want to prove: 0 = 0 at u8

const auto goal = Proposition::equality(u8(), Term::literal(kU8, 0), Term::literal(kU8, 0));

// Try to use u32 equality to prove u8 goal

// Motive: the type of the hole

const auto motive = Proposition::equality(u8(), Term::literal(kU8, 0), var0());

const auto forged =

ProofTerm::equality_elimination(u32(), // wrong type!

zero32(), zero32(), motive, eq_evidence, ProofTerm::reflexivity());

const auto result = cppl::kernel::check(ctx, goal, forged, {});

CPPL_CHECK(!result.has_value());

// Attempt: provide a motive that doesn't actually yield the goal

cppl::kernel::Context ctx;

// Have: 0 = 1 (suppose we had evidence, which we don't)

// Want: 0 = 2

// Motive: 0 = 0 (doesn't involve the hole correctly)

const auto goal = Proposition::equality(u32(), zero32(), two32());

// Motive must be C[-] such that C[1] is provable and C[0] is the goal

// But provide wrong motive

const auto wrong_motive = Proposition::equality(u32(), zero32(), zero32());

// This should be rejected because the motive doesn't reconstruct the goal

const auto forged = ProofTerm::equality_elimination(u32(), zero32(), one32(), wrong_motive,

ProofTerm::reflexivity(), // 0 = 1 evidence (won't work anyway)

ProofTerm::reflexivity());

const auto result = cppl::kernel::check(ctx, goal, forged, {});

CPPL_CHECK(!result.has_value());

// Attempt: claim to rewrite using a = b but provide evidence for C[a] instead of C[b]

cppl::kernel::Context ctx;

// Suppose: 0 = 1 (we'll use 0 = 0 as we can prove it)

// Motive: 0 = -

// Should provide evidence for 0 = 1, try to provide evidence for 0 = 0

const auto goal = Proposition::equality(u32(), zero32(), zero32());

// Motive: 0 = - where - is var0

const auto motive = Proposition::equality(u32(), zero32(), var0());

// Attempting: use 0 = 0 to prove 0 = 0 by substitution

// lhs = 0, rhs = 0

// Should need evidence for C[rhs] = (0 = 0), which we have

// Then derive C[lhs] = (0 = 0)

// This is actually valid!

// For a real attack, try:

// Goal: 0 = 2

// Have: 0 = 0

// Motive: 0 = - + 2

// Provide evidence for 0 = 0 + 2 (which is 0 = 2)

// Try to derive 0 = 0 + 2 which is 0 = 2

const auto attack_goal = Proposition::equality(u32(), zero32(), two32());

const auto add_two = Term::primitive(PrimOp::AddWrap, kU32, {var0(), two32()});

const auto attack_motive = Proposition::equality(u32(), zero32(), add_two);

// Can't provide valid evidence for 0 = 0 + 2 though

// This test verifies the kernel checks the evidence properly

// Attempt: eliminate P -> Q with evidence for R instead of P

cppl::kernel::Context ctx;

const auto p = Proposition::equality(u32(), zero32(), zero32());

const auto q = Proposition::equality(u32(), one32(), one32());

const auto r = Proposition::equality(u32(), two32(), two32());

// Have: P -> Q (trivially, both are provable)

const auto impl = Proposition::implication(p, q);

const auto impl_evidence = ProofTerm::implication_introduction(p, ProofTerm::reflexivity());

// Try to eliminate with evidence for R instead of P

const auto wrong_premise = ProofTerm::reflexivity(); // proves R not P

const auto forged = ProofTerm::implication_elimination(impl, impl_evidence, wrong_premise);

const auto result = cppl::kernel::check(ctx, q, forged, {});

// Should fail or succeed? Let's check

// impl_evidence proves P -> Q

// wrong_premise proves R

// Can't eliminate P -> Q with evidence for R

// Actually wait, wrong_premise proves 2 = 2, not P or R as a separate statement

// Need to structure this better

// Attempt: claim P -> Q but provide evidence for R -> S

cppl::kernel::Context ctx;

const auto p = Proposition::equality(u32(), zero32(), zero32());

const auto q = Proposition::equality(u32(), one32(), one32());

const auto r = Proposition::equality(u32(), two32(), two32());

// Real evidence: R -> R

const auto real_impl = Proposition::implication(r, r);

const auto real_evidence =

ProofTerm::implication_introduction(r, ProofTerm::hypothesis(cppl::kernel::HypothesisIndex{0}));

// Forged claim: this is actually P -> Q

const auto forged_impl = Proposition::implication(p, q);

const auto forged = ProofTerm::implication_elimination(forged_impl, real_evidence, ProofTerm::reflexivity());

const auto result = cppl::kernel::check(ctx, q, forged, {});

CPPL_CHECK(!result.has_value());

// This test documents correct behavior: reflexivity is checked against the GOAL

// not against some independent proposition the proof "carries".

cppl::kernel::Context ctx;

// Goal: (0 = 0) /\ (1 = 1) - both sides true

const auto goal = Proposition::conjunction(eq(0, 0), eq(1, 1));

const auto proof = ProofTerm::conjunction_introduction(ProofTerm::reflexivity(), ProofTerm::reflexivity());

const auto result = cppl::kernel::check(ctx, goal, proof, {});

CPPL_CHECK(result.has_value()); // Should succeed

// Cannot prove false: (0 = 1) /\ (1 = 2)

const auto false_goal = Proposition::conjunction(eq(0, 1), eq(1, 2));

const auto false_result = cppl::kernel::check(ctx, false_goal, proof, {});

CPPL_CHECK(!false_result.has_value()); // Should fail - reflexivity can't prove 0=1

// Document correct behavior: conjunction elimination checks evidence properly

cppl::kernel::Context ctx;

// Real evidence: (0 = 0) /\ (1 = 1)

const auto real_conj = Proposition::conjunction(eq(0, 0), eq(1, 1));

const auto real_evidence = ProofTerm::conjunction_introduction(ProofTerm::reflexivity(), ProofTerm::reflexivity());

// Correctly extract left: 0 = 0

const auto left_goal = eq(0, 0);

const auto left_proof = ProofTerm::conjunction_elimination(real_conj, real_evidence, false);

const auto left_result = cppl::kernel::check(ctx, left_goal, left_proof, {});

CPPL_CHECK(left_result.has_value());

// Correctly extract right: 1 = 1

const auto right_goal = eq(1, 1);

const auto right_proof = ProofTerm::conjunction_elimination(real_conj, real_evidence, true);

const auto right_result = cppl::kernel::check(ctx, right_goal, right_proof, {});

CPPL_CHECK(right_result.has_value());

// Cannot extract wrong proposition

const auto wrong_goal = eq(2, 2);

const auto wrong_proof = ProofTerm::conjunction_elimination(real_conj, real_evidence, false);

const auto wrong_result = cppl::kernel::check(ctx, wrong_goal, wrong_proof, {});

CPPL_CHECK(!wrong_result.has_value()); // Goal doesn't match what's extracted

// Attempt: claim to extract "third" element from binary conjunction

// This is a structural attack - the `right` bool should only allow left(false) or right(true)

// No direct way to attack this with current API, but ensure the cases are covered

// Attempt: provide a certificate that doesn't actually refute the system

cppl::kernel::Context ctx;

// Goal: 0 = 1

const auto goal = Proposition::equality(u32(), zero32(), one32());

// Fact: 0 = 0

cppl::kernel::ArithmeticFact fact{Proposition::equality(u32(), zero32(), zero32()),

cppl::kernel::Box<ProofTerm>{ProofTerm::reflexivity()}};

// Certificate: FarkasSum that doesn't actually prove contradiction

cppl::kernel::FarkasSum fake_sum{};

cppl::kernel::ArithmeticCertificate cert{fake_sum};

const auto forged = ProofTerm::linear_arithmetic({fact}, cert);

const auto result = cppl::kernel::check(ctx, goal, forged, {});

CPPL_CHECK(!result.has_value());

// Attempt: provide a motive that doesn't derive the goal correctly

cppl::kernel::Context ctx;

// Condition: 0 = 0 (true)

const auto cond = zero32();

const auto when_true = one32();

const auto when_false = two32();

// if 0 = 0 then 1 else 2 => 1

const auto& selected = when_true;

// Goal: selected = 1, which is true

const auto goal = Proposition::equality(u32(), selected, one32());

// Wrong motive: doesn't use the conditional result correctly

const auto wrong_motive = Proposition::equality(u32(), zero32(), one32());

const auto forged = ProofTerm::conditional_elimination(u32(), cond, when_true, when_false, wrong_motive,

ProofTerm::reflexivity(), ProofTerm::reflexivity());

const auto result = cppl::kernel::check(ctx, goal, forged, {});

CPPL_CHECK(!result.has_value());