# alp-carry — carry-chain proof kernel
# Copyright (C) 2026 Ahmad Ali Parr
# SPDX-License-Identifier: AGPL-3.0-only

"""C emission templates for the atomizer."""

CONSTRAINTS_H = """\
/* alp-carry — carry-chain proof kernel
 * Copyright (C) 2026 Ahmad Ali Parr
 * SPDX-License-Identifier: AGPL-3.0-only
 * GENERATED by atomizer from induced ALP program — do not edit.
 * Enforces spec conditions C1–C4; consumed by atomized.c and verifier.c */
#ifndef GENERATED_CONSTRAINTS_H
#define GENERATED_CONSTRAINTS_H
#include <stddef.h>
#define ALP_MAXD 64
/* C4-induced literals: {N_LITERALS} active */
static const float ALP_LO[ALP_MAXD] = {{ {LO_INIT} }};
static const float ALP_HI[ALP_MAXD] = {{ {HI_INIT} }};
static const float ALP_EPS = {EPS};
/* clause shape from induced program */
{BODY}
#endif /* GENERATED_CONSTRAINTS_H */
"""

BODY_BOTH = """\
/* clause 1 body: conjunction { clamp_all, project_eps } */
#define ALP_HAS_PROJECTION 1"""

BODY_CLAMP_ONLY = """\
/* clause 1 body: conjunction { clamp_all }  (projection subsumed — C4) */
#define ALP_HAS_PROJECTION 0"""