task3 reviewed

property_specification added

README.md

@@ -102,7 +102,7 @@ Matching uses **word-set containment + synonym expansion** — words don't need
 | `get_function_code` | `function_name` | −0.10 |
 | `get_state_variable` | `variable_name` (opt.) | −0.05 |
 | `get_call_graph` | — | −0.08 |
-| `get_formalized_property` | — | **−0.03** (cheapest — read this first!) |
+| `get_property_specification` | — | **−0.03** (cheapest — read this first!) |
 | `submit_function` | `function_name` | **+5.0 / +1.5 / −1.5**, ONE attempt |
 
 ### Grader (three-tier deterministic)
@@ -111,7 +111,7 @@ Matching uses **word-set containment + synonym expansion** — words don't need
 - **0.3** → a direct internal subfunction of the target → reward **+1.5**
 - **0.0** → anything else → reward **−1.5**
 
-`get_formalized_property` returns the precise pre/post-condition (`rule_broken_specs`). Reading it costs only −0.03 and usually provides enough information to identify the violating function without inspecting all code.
+`get_property_specification` returns the precise pre/post-condition (`rule_broken_specs`). Reading it costs only −0.03 and usually provides enough information to identify the violating function without inspecting all code.
 
 ---
 
@@ -125,7 +125,7 @@ All tasks share the same `Observation` structure:
   "contract_name": "SimpleVault",
   "contract_description": "An ETH vault that allows users to deposit...",
   "available_actions": ["list_functions", "get_function_metadata", "..."],
-  "last_action": "get_formalized_property",
+  "last_action": "get_property_specification",
   "last_action_result": "Formal property:\nPre: caller != owner...",
   "step_count": 1,
   "cumulative_reward": -0.03,
@@ -217,7 +217,7 @@ r = env.reset(seed=42)
 print(r.observation.extra["property_english"])
 # "Only the owner should be able to drain the vault..."
 
-s = env.step(Action(action_type=ActionType.GET_FORMALIZED_PROPERTY))
+s = env.step(Action(action_type=ActionType.GET_PROPERTY_SPECIFICATION))
 s = env.step(Action(action_type=ActionType.SUBMIT_FUNCTION,
              params={"function_name": "emergencyDrain"}))
 print(s.reward.value)  # +5.0
@@ -245,7 +245,7 @@ curl -X POST localhost:7860/reset \
 
 curl -X POST localhost:7860/step \
   -H "Content-Type: application/json" \
-  -d '{"action_type":"get_formalized_property","params":{}}'
+  -d '{"action_type":"get_property_specification","params":{}}'
 
 curl -X POST localhost:7860/step \
   -H "Content-Type: application/json" \

app.py

@@ -205,7 +205,7 @@ def action_space(task_id: str = "task1_vuln_detection"):
                 {"type": "get_function_code",       "params": {"function_name": "string"}, "reward": -0.10, "description": "Read full Solidity source of a function"},
                 {"type": "get_state_variable",      "params": {"variable_name": "string (opt)"}, "reward": -0.05, "description": "Get a state variable or list all"},
                 {"type": "get_call_graph",          "params": {},                             "reward": -0.08, "description": "Get function call graph"},
-                {"type": "get_formalized_property", "params": {},                             "reward": -0.03, "description": "Get formal pre/post-condition for the property"},
+                {"type": "get_property_specification", "params": {},                             "reward": -0.03, "description": "Get formal pre/post-condition for the property"},
                 {"type": "submit_function",         "params": {"function_name": "string"}, "reward": "+5.0 / +1.5 / -1.5", "description": "Submit answer. ONE attempt. Ends episode."},
             ],
         }

data/Template.json

@@ -1,14 +1,12 @@
 {
   "contract_name": "ExampleContract",
   "file_name": "ExampleContract.sol",
-  
   "metadata": {
     "license": "MIT",
     "solidity_version": "0.8.0",
     "description": "Example contract demonstrating the template structure",
     "author": "Example Author"
   },
-  
   "state_variables": [
     {
       "name": "owner",
@@ -25,7 +23,6 @@
       "description": "User token balances"
     }
   ],
-  
   "functions": [
     {
       "name": "transfer",
@@ -48,7 +45,9 @@
       ],
       "returns": "bool - true on success",
       "output_property": "Decreases caller's balance by amount, increases recipient's balance by amount. Emits Transfer event. Reverts if recipient is zero address or caller has insufficient balance.",
-      "events": ["Transfer"],
+      "events": [
+        "Transfer"
+      ],
       "vulnerable": false,
       "vulnerability_details": null,
       "property": null,
@@ -79,10 +78,14 @@
         "mitigation": "Use checks-effects-interactions pattern: update balance before external call"
       },
       "property": "When a user withdraws x amount of ETH, the user's balance should decrease by x. Due to reentrancy, an attacker can call withdraw recursively before balance is updated, draining more than their balance.",
-      "property_specification": "Pre-condition: User has balance B. Operation: withdraw(amount). Expected post-condition: User balance = B - amount. Actual vulnerability: Reentrant calls allow multiple withdrawals before balance update, resulting in user balance = B - (n * amount) where n > 1, violating the expected post-condition."
+      "property_specification": {
+        "Pre-condition": "User balance = B",
+        "Operation": "withdraw(amount)",
+        "Expected": "User balance = B - amount",
+        "Actual": "Reentrant calls allow user balance = B - (n * amount) where n > 1"
+      }
     }
   ],
-  
   "structs": [
     {
       "name": "MintLocalVars",
@@ -90,7 +93,6 @@
       "description": "Local variables used in mint function to avoid stack too deep errors"
     }
   ],
-  
   "modifiers": [
     {
       "name": "onlyOwner",
@@ -103,12 +105,10 @@
       "purpose": "Prevents reentrancy attacks by using a mutex lock"
     }
   ],
-  
   "inheritance": [
     "ERC20",
     "Ownable"
   ],
-  
   "call_graph": {
     "constructor": [
       "ERC20.constructor()"
@@ -120,7 +120,6 @@
       "msg.sender.call()"
     ]
   },
-  
   "audit_issues": [
     {
       "function": "withdraw",
@@ -130,10 +129,14 @@
       "status": "Fixed",
       "mitigation": "Moved balance update before external call (checks-effects-interactions pattern)",
       "property": "When a user withdraws x amount, the user's balance should decrease by x. Due to reentrancy, an attacker can withdraw multiple times before balance updates, draining more than their balance.",
-      "property_specification": "Pre-condition: User balance = B. Operation: withdraw(amount). Expected: User balance = B - amount. Actual: Reentrant calls allow user balance = B - (n * amount) where n > 1."
+      "property_specification": {
+        "Pre-condition": "User balance = B",
+        "Operation": "withdraw(amount)",
+        "Expected": "User balance = B - amount",
+        "Actual": "Reentrant calls allow user balance = B - (n * amount) where n > 1"
+      }
     }
   ],
-  
   "events": [
     {
       "name": "Transfer",

data/data_loader.py

@@ -163,15 +163,14 @@ def get_all_task3_entries(
     contracts: List[Dict[str, Any]],
 ) -> List[Tuple[Dict[str, Any], Dict[str, Any]]]:
     """
-    Returns (contract, function) pairs where function has a task3 field
-    with a non-empty property_english. These are the episode pool for Task 3.
+    Returns (contract, function) pairs where function is vulnerable
+    and has a property field.
     """
+    vulnerable_entries = get_all_vulnerable_entries(contracts)
     entries = []
-    for contract in contracts:
-        for fn in contract.get("functions", []):
-            t3 = fn.get("task3", {})
-            if t3.get("property_english"):
-                entries.append((contract, fn))
+    for contract, fn in vulnerable_entries:
+        if fn.get("property", None) is not None:
+            entries.append((contract, fn))
     return entries
 
 

demo.py

@@ -363,7 +363,7 @@ def run_auto_demo_t2(seed: int = 42, delay: float = 0.9):
 
 DEMO_SCRIPTS_T3 = {
     42: [
-        (ActionType.GET_FORMALIZED_PROPERTY, {},
+        (ActionType.GET_PROPERTY_SPECIFICATION, {},
          "Read the formal spec first — cheapest action at -0.03."),
         (ActionType.LIST_FUNCTIONS, {},
          "List all functions to survey candidates."),
@@ -373,7 +373,7 @@ DEMO_SCRIPTS_T3 = {
          "Confident. emergencyDrain violates the access-control property."),
     ],
     45: [
-        (ActionType.GET_FORMALIZED_PROPERTY, {},
+        (ActionType.GET_PROPERTY_SPECIFICATION, {},
          "Formal spec: first caller at valid price should win."),
         (ActionType.LIST_FUNCTIONS, {},
          "Auction contract — bid() immediately looks suspicious."),

env/schemas.py

@@ -42,7 +42,7 @@ class ActionType(str, Enum):
     SUBMIT_PROPERTY       = "submit_property"         # scored 0–5, one attempt
 
     # ── Task 3 – Rule Checker ────────────────────────────────────────────────
-    GET_FORMALIZED_PROPERTY = "get_formalized_property"  # -0.03
+    GET_PROPERTY_SPECIFICATION = "get_property_specification"  # -0.03
     GET_FUNCTION_METADATA   = "get_function_metadata"    # -0.05
     SUBMIT_FUNCTION         = "submit_function"          # +5.0 / +1.5 / -1.5, one attempt
 

eval.py

@@ -151,7 +151,7 @@ def oracle_t3(env: Task3Environment, seed: int, verbose: bool = False) -> Dict[s
     if verbose:
         prop = obs.extra.get("property_english", "")[:60]
         print(f"    {contract}.{fn_name}()  \"{prop}\"")
-    env.step(Action(action_type=ActionType.GET_FORMALIZED_PROPERTY))
+    env.step(Action(action_type=ActionType.GET_PROPERTY_SPECIFICATION))
     env.step(Action(action_type=ActionType.LIST_FUNCTIONS))
     result = env.step(Action(action_type=ActionType.SUBMIT_FUNCTION,
                               params={"function_name": fn_name}))

openenv.yaml

@@ -73,7 +73,7 @@ action_space:
     get_function_natspec:  {params: {}, reward: -0.08}
     get_file_natspec:      {params: {}, reward: -0.03}
     get_related_functions: {params: {}, reward: -0.06}
-    get_io:                {params: {}, reward: -0.04}
+    get_signature:         {params: {}, reward: -0.04}
     get_similar_rule:      {params: {}, reward: -0.20}
     submit_property:       {params: {property: string}, reward: "0.0-5.0 keyword-weighted, one attempt"}
   task3:
@@ -82,7 +82,7 @@ action_space:
     get_function_code:       {params: {function_name: string},       reward: -0.10}
     get_state_variable:      {params: {variable_name: "string opt"}, reward: -0.05}
     get_call_graph:          {params: {},                            reward: -0.08}
-    get_formalized_property: {params: {},                            reward: -0.03}
+    get_property_specification: {params: {},                            reward: -0.03}
     submit_function:         {params: {function_name: string},       reward: "+5.0 / +1.5 / -1.5, one attempt"}
 
 reward:

tasks/task3/actions.py

@@ -1,5 +1,8 @@
-"""Task 3: Identify the function that violates a specified property."""
+"""
+Task 3: Identify the function that violates a specified property.
+"""
 
+import json
 from typing import Any, Dict, Tuple
 from data.data_loader import (
     get_function_by_name, 
@@ -105,17 +108,20 @@ def get_call_graph(ctx: Any, qkey: str, params: Dict) -> Tuple[str, Reward]:
         Reward(value=-0.08, reason="get_call_graph cost"),
     )
 
-# TODO: Need to change this, property_formal doesn't exists
-def get_formalized_property(ctx: Any, qkey: str, params: Dict) -> Tuple[str, Reward]:
-    """Handle GET_FORMALIZED_PROPERTY action."""
+def get_property_specification(ctx: Any, qkey: str, params: Dict) -> Tuple[str, Reward]:
+    """Handle GET_PROPERTY_SPECIFICATION action."""
     if ctx._is_repeated(qkey):
         return "Repeated query.", Reward(value=-0.40, reason="Repeated query")
-    formal = ctx._target_fn.get("task3", {}).get("property_formal", "")
-    if not formal:
-        formal = "No formal specification available for this property."
+    
+    rule = ctx._target_fn.get("property_specification", {})
+    if not rule:
+        rule = "No rule specification available for this property."
+    
+    rule_parsed = json.dumps(rule) if isinstance(rule, dict) else rule
+    
     return (
-        f"Formal property:\n{formal}",
-        Reward(value=-0.03, reason="get_formalized_property cost"),
+        f"Formal property:\n{rule_parsed}",
+        Reward(value=-0.03, reason="get_property_specification cost"),
     )
 
 

tasks/task3/environment.py

@@ -22,7 +22,7 @@ Actions & rewards
   get_function_code       -0.10   full Solidity source of any function
   get_state_variables     -0.05   list or inspect state variables
   get_call_graph          -0.08   function call graph
-  get_formalized_property -0.03   formal pre/post-condition version of property
+  get_property_specification -0.03   formal pre/post-condition version of property
   submit_function         terminal: +5.0 / +1.5 / -1.5  (ONE attempt)
   repeated_query          -0.40
 
@@ -59,7 +59,7 @@ AVAILABLE_ACTIONS = [
     ActionType.GET_FUNCTION_CODE,
     ActionType.GET_STATE_VARIABLE,
     ActionType.GET_CALL_GRAPH,
-    ActionType.GET_FORMALIZED_PROPERTY,
+    ActionType.GET_PROPERTY_SPECIFICATION,
     ActionType.SUBMIT_FUNCTION,
 ]
 
@@ -113,7 +113,7 @@ class Task3Environment(BaseEnv):
                 f"Find the function in this contract that violates the property above.\n"
                 f"Use list_functions then get_function_code to investigate.\n"
                 f"Submit with submit_function, params={{\"function_name\": \"...\"}}.\n"
-                f"ONE submission allowed."
+                f"Only ONE submission allowed."
             ),
         )
         return ResetResult(observation=obs, info={"task_id": TASK_ID})
@@ -190,13 +190,13 @@ class Task3Environment(BaseEnv):
 
         # Mapping from ActionType to handler function
         handlers = {
-            ActionType.LIST_FUNCTIONS:           actions.list_functions,
-            ActionType.GET_FUNCTION_METADATA:    actions.get_function_metadata,
-            ActionType.GET_FUNCTION_CODE:        actions.get_function_code,
-            ActionType.GET_STATE_VARIABLE:       actions.get_state_variable,
-            ActionType.GET_CALL_GRAPH:           actions.get_call_graph,
-            ActionType.GET_FORMALIZED_PROPERTY:  actions.get_formalized_property,
-            ActionType.SUBMIT_FUNCTION:          actions.submit_function,
+            ActionType.LIST_FUNCTIONS:                  actions.list_functions,
+            ActionType.GET_FUNCTION_METADATA:           actions.get_function_metadata,
+            ActionType.GET_FUNCTION_CODE:               actions.get_function_code,
+            ActionType.GET_STATE_VARIABLE:              actions.get_state_variable,
+            ActionType.GET_CALL_GRAPH:                  actions.get_call_graph,
+            ActionType.GET_PROPERTY_SPECIFICATION:      actions.get_property_specification,
+            ActionType.SUBMIT_FUNCTION:                 actions.submit_function,
         }
 
         handler = handlers.get(at)

utils/prompts.py

@@ -83,7 +83,7 @@ Your task is to find the ONE function that violates this property.
 
 ## Actions (respond with JSON only, ONE action per turn):
 {"action": "list_functions",          "params": {}}
-{"action": "get_formalized_property", "params": {}}
+{"action": "get_property_specification", "params": {}}
 {"action": "get_function_metadata",   "params": {"function_name": "<n>"}}
 {"action": "get_function_code",       "params": {"function_name": "<n>"}}
 {"action": "get_state_variable",      "params": {"variable_name": "<n>"}}
@@ -93,7 +93,7 @@ Your task is to find the ONE function that violates this property.
 ## Strategy:
 1. Read the property shown as property_english in the observation.
 2. list_functions to survey candidates.
-3. get_formalized_property for the precise pre/post-condition (cheap: -0.03).
+3. get_property_specification for the precise pre/post-condition (cheap: -0.03).
 4. get_function_code on the 1-2 most suspicious functions.
 5. submit_function when confident — ONE attempt only.
 

validate.py

@@ -42,7 +42,7 @@ def check_pydantic_models():
     from env.schemas import Observation, Action, ActionType, Reward, StepResult, ResetResult
     obs = Observation(task_id="t", contract_name="C", contract_description="D", available_actions=[])
     for at in [ActionType.LIST_FUNCTIONS, ActionType.SUBMIT_PROPERTY,
-               ActionType.GET_FORMALIZED_PROPERTY, ActionType.SUBMIT_FUNCTION]:
+               ActionType.GET_PROPERTY_SPECIFICATION, ActionType.SUBMIT_FUNCTION]:
         Action(action_type=at)
     Reward(value=-1.5, reason="test")
     StepResult(observation=obs, reward=Reward(value=0, reason=""), done=False)
@@ -90,7 +90,7 @@ def check_t3_env():
     assert "property_english" in r.observation.extra
     prop = r.observation.extra["property_english"]
     assert len(prop) > 10, "property_english too short"
-    for at in [ActionType.LIST_FUNCTIONS, ActionType.GET_FORMALIZED_PROPERTY,
+    for at in [ActionType.LIST_FUNCTIONS, ActionType.GET_PROPERTY_SPECIFICATION,
                ActionType.GET_CALL_GRAPH, ActionType.GET_STATE_VARIABLE]:
         s = env.step(Action(action_type=at))
         assert s.reward.value < 0, f"{at.value} should have negative shaping reward"
@@ -100,7 +100,7 @@ def check_t3_action_costs():
     from env.schemas import Action, ActionType
     env = Task3Environment(); env.reset(seed=42)
     costs = {
-        ActionType.GET_FORMALIZED_PROPERTY: -0.03,
+        ActionType.GET_PROPERTY_SPECIFICATION: -0.03,
         ActionType.LIST_FUNCTIONS: -0.05,
         ActionType.GET_CALL_GRAPH: -0.08,
     }
@@ -201,7 +201,7 @@ def check_reward_shaping():
     env = Task3Environment(); env.reset(seed=1)
     rewards = {env.step(Action(action_type=at)).reward.value
                for at in [ActionType.LIST_FUNCTIONS,
-                           ActionType.GET_FORMALIZED_PROPERTY,
+                           ActionType.GET_PROPERTY_SPECIFICATION,
                            ActionType.GET_CALL_GRAPH]}
     assert len(rewards) >= 2