.NET Backend

Version: 1.0.0

This document specifies how the .NET backend must implement Calor semantics. The backend conforms to Calor semantics; it does not define them.

Why This Document Exists

"It emits C#" is not a semantics specification.

The .NET backend generates C# code, but C# is not the source of truth for Calor semantics. This document specifies:

1. Where C# behavior matches Calor - Direct emission is safe
2. Where C# behavior differs or is unspecified - Additional code is required
3. How to verify conformance - Test cases and validation checklists

Without this specification, subtle differences between C# and Calor could cause:

• "Works on my machine" bugs
• Version-specific behavior changes
• Agent-generated code that fails on different .NET versions

Core Principle

The emitter must not rely on unspecified behavior in C#.

When C# evaluation order matches Calor semantics, direct emission is acceptable. When C# behavior is unspecified or differs, the emitter must generate code that enforces Calor semantics.

What "Unspecified" Means

C# specifies many behaviors, but not all. For example:

• Argument evaluation order is specified (left-to-right)
• checked overflow behavior is specified
• Some optimization behaviors are not specified

The emitter must never assume unspecified behavior matches Calor semantics.

Evaluation Order

Function Arguments

C# specifies left-to-right argument evaluation (C# spec 12.6.2.2), which matches Calor.

Direct emission is safe:

// Calor: f(a(), b(), c())
f(a(), b(), c());  // C# guarantees left-to-right

Binary Operators

C# evaluates binary operator operands left-to-right (C# spec 12.4.1), matching Calor.

Direct emission is safe:

// Calor: a() + b()
a() + b();  // C# guarantees left-to-right

From CNF

When emitting from CNF (which has explicit temporaries), preserve them:

CNF:

t1 = a()
t2 = b()
t3 = t1 + t2

C#:

var t1 = a();
var t2 = b();
var t3 = t1 + t2;

Short-Circuit Operators

Logical AND and OR

C# && and || short-circuit identically to Calor.

Direct emission is safe:

// Calor: A && B
A && B;  // C# short-circuits

// Calor: A || B
A || B;  // C# short-circuits

Numeric Semantics

Integer Overflow

Calor Default: TRAP (throw OverflowException)

C# Implementation:

// Use checked arithmetic
checked
{
    var result = a + b;  // Throws OverflowException on overflow
}

Project-Level Configuration:

<PropertyGroup>
  <CheckForOverflowUnderflow>true</CheckForOverflowUnderflow>
</PropertyGroup>

Type Mapping

Conversions

Implicit Widening:

// Calor: INT to FLOAT (implicit)
int i = 42;
double f = i;  // C# allows implicit widening

Explicit Narrowing:

// Calor: FLOAT to INT (explicit required)
double f = 3.14;
int i = (int)f;  // Explicit cast required

Contracts

Preconditions

C# Implementation:

public int MyFunction(int x)
{
    // REQUIRES: x > 0
    if (!(x > 0))
    {
        throw new Calor.Runtime.ContractViolationException(
            functionId: "f001",
            message: "Precondition failed",
            expression: "x > 0",
            kind: ContractKind.Requires);
    }

    // Body
    return x * 2;
}

Postconditions

C# Implementation:

public int MyFunction(int x)
{
    // Body
    var __result = x * 2;

    // ENSURES: result > x
    if (!(__result > x))
    {
        throw new Calor.Runtime.ContractViolationException(
            functionId: "f001",
            message: "Postcondition failed",
            expression: "result > x",
            kind: ContractKind.Ensures);
    }

    return __result;
}

Contract Mode

Generated Code Markers

The emitter includes markers in generated code:

// <auto-generated>
// This file was generated by the Calor compiler.
// Semantics version: 1.0.0
// Do not modify directly.
// </auto-generated>

Validation Checklist

The backend must ensure:

• Left-to-right evaluation preserved
• Short-circuit semantics correct
• Integer overflow traps (default)
• Type conversions explicit where required
• Contracts generate correct exception type
• Contract exception includes function ID
• Option/Result types from runtime library
• Pattern matching exhaustive (compiler enforced)

References

• Core Semantics
• Normal Form
• Implementation: src/Calor.Compiler/CodeGen/CSharpEmitter.cs