| # 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""" | |