// Generated by EML-lang WGSL backend (function library)
// Source module: rc_filter
// Source file:   /home/monogate/monogate/forge/examples/rc_filter.eml
// Functions:     6
// Constants:     0
//
// Float32-only. EML `Real` and `f64` lower to WGSL `f32`.
// WebGPU has no native f64; f16 is an optional extension
// (`enable f16;`). If you need >32-bit precision, do the
// high-precision step on CPU and ship a float32 result.
//
// At least one function in this module has chain_order >= 2; per-function drift
// warnings appear inline above each affected function.
//
// No entry point is provided; this is a function library.
// Validate with `naga <output.wgsl>` or include in your own
// vertex / fragment / compute shader and call from there.

// circuit
//   Pfaffian profile: chain_order=0, cost_class=p0-d0-w0-c0, drift_risk=LOW.
fn circuit() -> f32 {
    return 0.0;
}

// tau
//   Pfaffian profile: chain_order=0, cost_class=p0-d1-w0-c0, drift_risk=LOW.
//   forge.requires: (r > 0.0)
//   forge.requires: (c > 0.0)
//   forge.ensures: (result == (r * c))
//   forge.verify: lean theorem=rc_time_constant_def
fn tau(r: f32, c: f32) -> f32 {
    return (r * c);
}

// vout_steady
//   Pfaffian profile: chain_order=0, cost_class=p0-d0-w0-c0, drift_risk=LOW.
//   forge.ensures: (result == vin)
//   forge.verify: lean theorem=rc_steady_state_equals_input
fn vout_steady(vin: f32) -> f32 {
    return vin;
}

// vout_initial
//   Pfaffian profile: chain_order=0, cost_class=p0-d0-w0-c0, drift_risk=LOW.
//   forge.ensures: (result == 0.0)
//   forge.verify: lean theorem=rc_initial_output_zero
fn vout_initial() -> f32 {
    return 0.0;
}

// vout_charging
//   Pfaffian profile: chain_order=1, cost_class=p1-d6-w1-c0, drift_risk=MEDIUM.
//   WARNING: float32 precision drift risk -- drift_risk=MEDIUM.
//   Consider doing the high-precision composition on CPU and
//   passing the float32 result into the shader.
//   forge.requires: (tau_val > 0.0)
//   forge.ensures: (result == (vin * (1.0 - exp(((-t) / tau_val)))))
//   forge.verify: lean theorem=rc_step_response_form
fn vout_charging(vin: f32, t: f32, tau_val: f32) -> f32 {
    return (vin * (1.0 - exp(((-t) / tau_val))));
}

// vout_charging_at_zero
//   Pfaffian profile: chain_order=0, cost_class=p0-d0-w0-c0, drift_risk=LOW.
//   forge.requires: (tau_val > 0.0)
//   forge.ensures: (result == 0.0)
//   forge.verify: lean theorem=rc_step_response_at_zero
fn vout_charging_at_zero(vin: f32, tau_val: f32) -> f32 {
    return (vin * (1.0 - exp((-0.0 / tau_val))));
}