Added manual refinement framework

examples/contracts/dev.contract

@@ -367,7 +367,7 @@ contract KeepsDistance(perception_distance, min_dist, max_brake=float("inf"), ma
         true_relative_speed = lead_car.speed - self.speed
 
         stopping_time = math.ceil(self.speed/max_brake)
-        rel_dist_covered = stopping_time*self.speed + (true_relative_speed + abs_speed_err)
+        rel_dist_covered = stopping_time*self.speed + (true_relative_speed)
         delta_stopping_time = math.ceil((self.speed+max_accel)/max_brake)
         max_rdc_delta = delta_stopping_time*self.speed + (true_relative_speed + max_brake + max_accel + abs_speed_err)
         buffer_dist = min_dist + (max(0, max_rdc_delta + rel_dist_covered))
@@ -389,7 +389,7 @@ contract KeepsDistance(perception_distance, min_dist, max_brake=float("inf"), ma
         always -max_brake <= (next lead_car.speed) - lead_car.speed <= max_accel
 
         # Assume we start stopped outside the danger zone
-        (lead_dist > buffer_dist) and (self.speed == 0)
+        (lead_dist > (buffer_dist+10)) and (self.speed == 0)
 
         # Assume no one cuts in front us too closely
         always ((next lead_dist) == (lead_dist - true_relative_speed))
@@ -452,11 +452,9 @@ keeps_distance_raw = compose over car:
     use cs_safety
     use max_braking_force
 
-# keeps_distance = refine keeps_distance_raw as KeepsDistance(PERCEPTION_DISTANCE,
-#     MIN_DIST,
-#     abs_dist_err=ABS_DIST_ERR,
-#     abs_speed_err=ABS_SPEED_ERR,
-#     max_brake=MAX_BRAKE,
-#     max_accel=MAX_ACCEL) using LeanProof("KeepsDistanceRefinement")
+keeps_distance = refine keeps_distance_raw as KeepsDistance(PERCEPTION_DISTANCE,
+    MIN_DIST,
+    max_brake=MAX_BRAKE,
+    max_accel=MAX_ACCEL) using LeanProof("KeepsDistanceRefinement")
 
-verify keeps_distance_raw
+verify keeps_distance

src/scenic/contracts/composition.py

@@ -182,6 +182,7 @@ def __init__(
                 print("Guarantees:")
                 for g in tl_guarantees:
                     print(f"    {g}")
+                assert False
                 breakpoint()
 
             ## Add guarantees to accumulated top-level guarantees

src/scenic/contracts/refinement.py

@@ -0,0 +1,62 @@
+from functools import cached_property
+
+from scenic.contracts.contracts import ContractResult, VerificationTechnique
+
+
+class Refinement(VerificationTechnique):
+    def __init__(self, stmt, contract, method):
+        self.stmt = stmt
+        self.contract = contract
+        self.method = method
+
+        self.method.check()
+
+    @cached_property
+    def assumptions(self):
+        return self.contract.assumptions
+
+    @cached_property
+    def guarantees(self):
+        return self.contract.guarantees
+
+    def verify(self):
+        return RefinementContractResult(
+            self.assumptions,
+            self.guarantees,
+            self.stmt.component,
+            self.stmt.verify(),
+            self.method,
+        )
+
+
+class RefinementContractResult(ContractResult):
+    def __init__(self, assumptions, guarantees, component, sub_result, method):
+        super().__init__(assumptions, guarantees, component)
+        self.sub_result = sub_result
+        self.method = method
+
+    @cached_property
+    def correctness(self):
+        return self.sub_result.correctness
+
+    @cached_property
+    def confidence(self):
+        return self.sub_result.confidence
+
+    @property
+    def evidenceSummary(self):
+        string = ""
+        string += f"Refinement Method: {self.method}\n"
+        string += self.sub_result.evidenceSummary
+        return string
+
+
+class LeanProof:
+    def __init__(self, proof_loc):
+        self.proof_loc = proof_loc
+
+    def check(self):
+        pass
+
+    def __str__(self):
+        return f"LeanProof ('{self.proof_loc}')"

src/scenic/contracts/veneer.py

@@ -15,6 +15,8 @@
     "registerVerifyStatement",
     "Assumption",
     "Composition",
+    "Refinement",
+    "LeanProof",
 )
 
 # various Python types and functions used in the language but defined elsewhere
@@ -27,6 +29,7 @@
 from scenic.contracts.components import ActionComponent, BaseComponent, ComposeComponent
 from scenic.contracts.composition import Composition
 from scenic.contracts.contracts import Contract
+from scenic.contracts.refinement import LeanProof, Refinement
 from scenic.contracts.testing import (
     CorrectnessRequirementCondition,
     CountTerminationCondition,

src/scenic/syntax/ast.py

@@ -1423,27 +1423,29 @@ def __init__(
         self.name = name
 
 
-class ContractVerify(AST):
+class ContractRefine(AST):
     def __init__(
         self,
-        target,
+        name,
+        contract,
+        method,
         *args,
         **kwargs,
     ) -> None:
         super().__init__(*args, **kwargs)
-        self.target = target
+        self.name = name
+        self.contract = contract
+        self.method = method
 
 
-class ContractRefine(AST):
+class ContractVerify(AST):
     def __init__(
         self,
-        name,
         target,
         *args,
         **kwargs,
     ) -> None:
         super().__init__(*args, **kwargs)
-        self.name = name
         self.target = target
 
 

src/scenic/syntax/compiler.py

@@ -3031,6 +3031,24 @@ def visit_ContractCompose(self, node: s.ContractCompose):
             keywords=keywords,
         )
 
+    def visit_ContractRefine(self, node: s.ContractRefine):
+        # Map contract name
+        assert isinstance(node.contract, ast.Call)
+        assert isinstance(node.contract.func, ast.Name)
+        node.contract.func.id = self.toContractName(node.contract.func.id)
+
+        # Package keywords
+        keywords = []
+        keywords.append(ast.keyword("stmt", ast.Name(node.name, loadCtx)))
+        keywords.append(ast.keyword("contract", node.contract))
+        keywords.append(ast.keyword("method", node.method))
+
+        return ast.Call(
+            func=ast.Name("Refinement", loadCtx),
+            args=[],
+            keywords=keywords,
+        )
+
     def visit_ContractVerify(self, node: s.ContractVerify):
         return ast.Call(ast.Name("registerVerifyStatement", loadCtx), [node.target], [])
 

src/scenic/syntax/scenic.gram

@@ -663,6 +663,7 @@ scenic_compound_stmt:
     | scenic_assign_contract_test_stmt
     | scenic_assign_contract_assume_stmt
     | scenic_assign_contract_compose_stmt
+    | scenic_assign_contract_refine_stmt
 
 # SIMPLE STATEMENTS
 # =================
@@ -1076,9 +1077,6 @@ scenic_implement_stmt:
 scenic_verify_expr:
     | "verify" e=scenic_prefix_operators {s.ContractVerify(e, LOCATIONS)}
 
-scenic_refine_expr:
-    | "refine" name=NAME "as" e=scenic_prefix_operators {s.ContractRefine(name, e, LOCATIONS)}
-
 # Contract
 # --------
 
@@ -1223,7 +1221,7 @@ scenic_assign_contract_compose_stmt:
      }
 
 scenic_contract_compose_stmt:
-    | "compose" "over" name=scenic_subcomponent_name ':' NEWLINE INDENT a=(scenic_contract_compose_inner)+ DEDENT {s.ContractCompose(name, a)}
+    | "compose" "over" name=scenic_subcomponent_name ':' NEWLINE INDENT a=(scenic_contract_compose_inner)+ DEDENT {s.ContractCompose(name, a, LOCATIONS)}
 
 scenic_contract_compose_inner:
     | scenic_contract_test_stmt
@@ -1233,6 +1231,16 @@ scenic_contract_compose_inner:
 scenic_contract_use_stmt:
     | "use" component=NAME NEWLINE {s.ContractUse(component.string)}
 
+# Contract Refine Statements
+# ---------------------------
+scenic_assign_contract_refine_stmt:
+    | a=(z=star_targets '=' { z })+ b=scenic_contract_refine_stmt {
+         ast.Assign(targets=a, value=b, LOCATIONS)
+     }
+
+scenic_contract_refine_stmt:
+    | "refine" name=NAME "as" contract=primary "using" method=primary NEWLINE {s.ContractRefine(name.string, contract, method, LOCATIONS)}
+
 # Component/Contracts General
 # ---------------------------
 
@@ -2106,7 +2114,6 @@ scenic_prefix_operators:
     | "visible" e=scenic_prefix_operators { s.VisibleOp(region=e, LOCATIONS) }
     | 'not' "visible" e=scenic_prefix_operators { s.NotVisibleOp(region=e, LOCATIONS) }
     | p=scenic_position_of_op_position 'of' e=scenic_prefix_operators { s.PositionOfOp(position=p, target=e, LOCATIONS) }
-    | scenic_refine_expr
     | "next" e=scenic_prefix_operators {s.ContractNext(e, 1, LOCATIONS)}
     | scenic_verify_expr
     | sum