# Transaction Predicate Language for Constraint-Based Intents [TOC] #### Rationale We aim to provide a flexible and expressive language for defining transaction constraints, enhancing the capabilities of smart contracts and dApps. By leveraging established semantics, it ensures a robust and theoretically sound framework. #### Abstract This EIP proposes a transaction predicate language based on the Fretish semantics for specifying constraints in Ethereum transactions. The language allows users to define complex constraints and conditions for transaction execution, enhancing the flexibility and security of smart contract interactions. #### Motivation Current transaction mechanisms in Ethereum lack a flexible and expressive way to define constraints and conditions for transaction execution. By introducing a predicate language based on established semantics, this EIP aims to provide a robust framework for specifying transaction intents, improving the usability and security of decentralized applications (dApps). #### Specification 1. **Introduction** - This section provides an overview of the predicate language, its purpose, and the foundational semantics it builds upon, referencing key works in graphical interval logic and concurrent system specifications. 2. **Scope Semantics** - Defines the scope semantics for both infinite and finite states, detailing intervals relevant to different scopes ("in", "before", "after") and their properties. 3. **Timing Semantics** - Explains the timing semantics, including basic and conditional timing conditions, with examples and patterns for applying these conditions within defined intervals. 4. **Real-Time Semantics** - Details real-time conditions such as "within n", "for n", and "after n", emphasizing the importance of the End of Scope (EOS) marker and the application of timing conditions and their negations. 5. **Adding Conditions** - Provides examples of adding conditions to timing semantics, explaining how to apply conditional patterns to intervals for specifying transaction constraints. 6. **Negations and Special Cases** - Discusses the handling of negations for timing conditions and special cases, offering guidance on interpreting these within the defined framework. ### 1. Introduction This section introduces the transaction predicate language, outlining its purpose to enhance transaction execution flexibility and security. It leverages foundational semantics from graphical interval logic to provide a robust framework for defining transaction constraints. ### 2. Scope Semantics #### Infinite State - **In**: Interval starts after a mode and ends before the mode ends. - **Before**: Checks if a mode never occurs. - **After**: No requirement if mode never exits. #### Finite State - **In**: Interval starts and ends within the execution time (EE). - **Before**: Checks if a mode never occurs during execution. - **After**: No requirement if mode never exits during execution. ### 3. Timing Semantics #### Basic Timing Conditions - **Immediately P**: P holds immediately. - **Always P**: P holds throughout the interval. - **Never P**: P never holds within the interval. - **Eventually P**: P holds at some point within the interval. #### Adding Conditions - **Example**: If a condition (COND) is met, then P holds eventually. ### 4. Real-Time Semantics #### Conditions - **Within n**: P must hold within n time units. - **For n**: P must hold for n time units. - **After n**: P must hold after n time units. ### 5. Adding Conditions - Conditions apply patterns to intervals, allowing for specifying complex transaction constraints. - Example: "Eventually P" within a specified condition. ### 6. Negations and Special Cases #### Negation Handling - **Not (within n P)**: Equivalent to "for n (not P)". - **Not (for n P)**: Equivalent to "within n (not P)". - **Not (after n P)**: Equivalent to "(within n P) or (for (n+1) not P)". #### Special Cases - Special handling for conditions that do not fit typical patterns, ensuring comprehensive coverage of possible scenarios. ### Additional Specifications #### Scope The optional scope field specifies the period where the requirement holds. If omitted, the requirement is deemed to hold universally, subject to condition, below. The scope is specified relative to system modes. The scope can specify system behavior before a specified mode occurs, or after a specified mode ends, or when the system is in a specified mode. In the latter case, there may be many intervals in which the requirement holds. The mode is specified by giving its mode name. #### Condition The condition field is a boolean expression that further constrains when the requirement response is to occur. #### Timing The timing field specifies when the response shall happen, relative to the scope and condition. Timing can be immediately (synonyms: initially, at the first timepoint, at the same timepoint), at the next timepoint, finally (synonym: at the last timepoint), eventually, always, never, within N time units, for N time units, after N time units, until stop_condition, or before stop_condition. The timing after means that the response happens N time units from the beginning of the requirement's period, and does not happen before that; i.e., does not happen for N-1 time units after the beginning of the period. ### Boolean and Temporal Operators - **Boolean Operators**: ! (negation), & (conjunction), | (disjunction), xor (exclusive or), -> or => (implication), <-> or <=> (equivalence). An alternative phrasing for implication is "if p then q". - **Temporal Predicates**: preBool, preInt, preReal, persisted, occurred, persists, occurs, prevOcc, and nextOcc. - **Arithmetic Comparison Operators**: =, !=, <, >, <=, >=. - **Arithmetic Operators**: +, -, *, /, mod, ^ (exponentiation). #### Note The Boolean operators allowed in the boolean expression while scope, condition, until and before timings, and response fields are: ! (negation), & (conjunction), | (disjunction), xor (exclusive or), -> or => (implication), <-> or <=> (equivalence). An alternative phrasing for implication is if p then q. There are nine predefined temporal predicates: , preBool, preInt, preReal, persisted, occurred, persists, occurs, prevOcc and nextOcc. The arithmetic comparison operators are =, !=, <, >, <=, >=. The arithmetic operators are +, -, *, /, mod, and ^ (exponentiation). Arithmetic terms and predicates are in standard form; e.g., f(x,y), p(x,y,z).