// SPDX-License-Identifier: MIT // Generated by EML-lang Solidity backend // Source module: aerospace_actuator_guard_band // Source file: /home/monogate/monogate/forge/examples/actuator_guard.eml // Functions: 1 (1 @verify-annotated) // Constants: 0 pragma solidity ^0.8.20; contract AerospaceActuatorGuardBand { /// @notice Formal proof: actuator_command_within_band (MachLib). Compiled from EML-lang. /// @dev Pfaffian profile: chain_order=0, cost_class=p0-d4-w0-c0, drift_risk=LOW. /// @dev Gas estimate: ~305 gas (PRBMath SD59x18 overrides assumed; run forge gas-bench for the canonical signal). /// @param error error (int256) /// @param integral integral (int256) /// @param deriv deriv (int256) /// @param kp kp (int256) /// @param ki ki (int256) /// @param kd kd (int256) /// @param uMin u_min (int256) /// @param uMax u_max (int256) /// @dev ensures: (uMin <= result) /// @dev ensures: (result <= uMax) function actuatorCommandWithinBand(int256 error, int256 integral, int256 deriv, int256 kp, int256 ki, int256 kd, int256 uMin, int256 uMax) external pure returns (int256) { require((uMin <= uMax), "actuator_command_within_band: requires (uMin <= uMax)"); return _clamp((((kp * error) + (ki * integral)) + (kd * deriv)), uMin, uMax); } /// @dev clamp helper -- min(max(x, lo), hi). function _clamp(int256 x, int256 lo, int256 hi) internal pure returns (int256) { if (x < lo) return lo; if (x > hi) return hi; return x; } }