// SPDX-License-Identifier: MIT
// Generated by EML-lang Solidity backend
// Source module: rc_filter
// Source file:   /home/monogate/monogate/forge/examples/rc_filter.eml
// Functions:     6 (5 @verify-annotated)
// Constants:     0
// Transcendental stubs: exp -- override in a derived contract (see PRBMath SD59x18)

pragma solidity ^0.8.20;

contract RcFilter {
    /// @notice circuit -- compiled from EML-lang.
    /// @dev Pfaffian profile: chain_order=0, cost_class=p0-d0-w0-c0, drift_risk=LOW.
    /// @dev Gas estimate: ~203 gas (PRBMath SD59x18 overrides assumed; run forge gas-bench for the canonical signal).
    function circuit() internal pure returns (int256) {
        return 0;
    }

    /// @notice Formal proof: rc_time_constant_def (MachLib). Compiled from EML-lang.
    /// @dev Pfaffian profile: chain_order=0, cost_class=p0-d1-w0-c0, drift_risk=LOW.
    /// @dev Gas estimate: ~211 gas (PRBMath SD59x18 overrides assumed; run forge gas-bench for the canonical signal).
    /// @param r r (int256)
    /// @param c c (int256)
    /// @dev ensures: (result == (r * c))
    function tau(int256 r, int256 c) external pure returns (int256) {
        require((r > 0), "tau: requires (r > 0)");
        require((c > 0), "tau: requires (c > 0)");
        return (r * c);
    }

    /// @notice Formal proof: rc_steady_state_equals_input (MachLib). Compiled from EML-lang.
    /// @dev Pfaffian profile: chain_order=0, cost_class=p0-d0-w0-c0, drift_risk=LOW.
    /// @dev Gas estimate: ~203 gas (PRBMath SD59x18 overrides assumed; run forge gas-bench for the canonical signal).
    /// @param vin vin (int256)
    /// @dev ensures: (result == vin)
    function voutSteady(int256 vin) external pure returns (int256) {
        return vin;
    }

    /// @notice Formal proof: rc_initial_output_zero (MachLib). Compiled from EML-lang.
    /// @dev Pfaffian profile: chain_order=0, cost_class=p0-d0-w0-c0, drift_risk=LOW.
    /// @dev Gas estimate: ~203 gas (PRBMath SD59x18 overrides assumed; run forge gas-bench for the canonical signal).
    /// @dev ensures: (result == 0)
    function voutInitial() external pure returns (int256) {
        return 0;
    }

    /// @notice Formal proof: rc_step_response_form (MachLib). Compiled from EML-lang.
    /// @dev Pfaffian profile: chain_order=1, cost_class=p1-d6-w1-c0, drift_risk=MEDIUM.
    /// @dev Gas estimate: ~3,750 gas (PRBMath SD59x18 overrides assumed; run forge gas-bench for the canonical signal).
    /// @param vin vin (int256)
    /// @param t t (int256)
    /// @param tauVal tau_val (int256)
    /// @dev ensures: (result == (vin * (1 - _exp(((-t) / tauVal)))))
    function voutCharging(int256 vin, int256 t, int256 tauVal) external pure returns (int256) {
        require((tauVal > 0), "vout_charging: requires (tauVal > 0)");
        return (vin * (1 - _exp(((-t) / tauVal))));
    }

    /// @notice Formal proof: rc_step_response_at_zero (MachLib). Compiled from EML-lang.
    /// @dev Pfaffian profile: chain_order=0, cost_class=p0-d0-w0-c0, drift_risk=LOW.
    /// @dev Gas estimate: ~3,700 gas (PRBMath SD59x18 overrides assumed; run forge gas-bench for the canonical signal).
    /// @param vin vin (int256)
    /// @param tauVal tau_val (int256)
    /// @dev ensures: (result == 0)
    function voutChargingAtZero(int256 vin, int256 tauVal) external pure returns (int256) {
        require((tauVal > 0), "vout_charging_at_zero: requires (tauVal > 0)");
        return (vin * (1 - _exp((0 / tauVal))));
    }

    /// @dev exp stub — override with a fixed-point implementation.
    function _exp(int256 x) internal pure virtual returns (int256) {
        x; // silence unused-param warning
        revert("_exp: stub — override in a derived contract (see PRBMath SD59x18.exp)");
    }

}