[minor] Add contracts #273

fabianschuiki · 2025-01-31T21:03:00Z

Add the contract declaration to the FIRRTL spec.

fabianschuiki · 2025-01-31T21:27:16Z

Hmmm, not sure why the firrtl,notest code blocks don't render as FIRRTL properly 🤔

seldridge

Awesome to see this coming together.

Mostly copy-editing. However, I would like to take another pass.

seldridge · 2025-01-31T21:22:58Z

spec.md

@@ -2961,6 +2961,104 @@ For this reason, it is an error to use `rwprobe`{.firrtl} on any port on a publi

 Probes may not be inputs to modules.

+# Contracts
+
+The `contract`{.firrtl} declaration provides a mechanism to verify a predicate or property, and to then use this predicate or property to simplify the circuit for further verification or simulation.


Supreme-nit: please use two sentences here to make this easier to read.

also nit didn't we have some sort of one-sentence-per-line rule at some point?

seldridge · 2025-01-31T21:25:02Z

spec.md

+The `contract`{.firrtl} declaration provides a mechanism to verify a predicate or property, and to then use this predicate or property to simplify the circuit for further verification or simulation.
+
+``` firrtl,notest
+FIRRTL version 4.2.0
+circuit Foo:
+  public module Foo:
+    input a: UInt<42>
+    input b: UInt<1337>
+    output x: UInt<42>
+    output y: UInt<1337>
+    ;; snippetbegin
+    contract c, d = a, b:
+      ; contract body
+    connect x, c
+    connect y, d
+    ;; snippetend
+```
+
+A contract conceptually acts like a `node`{.firrtl}, defining one or more names and assigning a value to each.
+It also has a block to hold statements that describe the predicates and properties to be verified.
+Most commonly the `circt_verif_require` and `circt_verif_ensure` intrinsics ([@sec:intrinsics]) are used to describe pre- and post-conditions of the contract.
+These intrinsics can only be used in the body block of a contract.
+The types of the defined names are the types of the expressions given in the definition and must be a ground type or a potentially nested aggregate type of only ground types.
+Probes, properties, and bundles with flips cannot be used in a contract.


Can the PR reorder this discussion slightly. Specifically, I wouldn't lead with the example, but end with the example. See some of the structure for how layers or layer blocks are discussed.

Roughly:

FIRRTL has contracts.

This is what a contract is.

This is how you declare a contract.

This is how you associate node assignments to a contract.

These are the restrictions around a contract.

This is an example.

seldridge · 2025-01-31T21:27:35Z

spec.md

+The `contract`{.firrtl} declaration provides a mechanism to verify a predicate or property, and to then use this predicate or property to simplify the circuit for further verification or simulation.
+
+``` firrtl,notest
+FIRRTL version 4.2.0
+circuit Foo:
+  public module Foo:
+    input a: UInt<42>
+    input b: UInt<1337>
+    output x: UInt<42>
+    output y: UInt<1337>
+    ;; snippetbegin
+    contract c, d = a, b:
+      ; contract body
+    connect x, c
+    connect y, d
+    ;; snippetend
+```
+
+A contract conceptually acts like a `node`{.firrtl}, defining one or more names and assigning a value to each.
+It also has a block to hold statements that describe the predicates and properties to be verified.
+Most commonly the `circt_verif_require` and `circt_verif_ensure` intrinsics ([@sec:intrinsics]) are used to describe pre- and post-conditions of the contract.
+These intrinsics can only be used in the body block of a contract.
+The types of the defined names are the types of the expressions given in the definition and must be a ground type or a potentially nested aggregate type of only ground types.
+Probes, properties, and bundles with flips cannot be used in a contract.


Is it that you can't use probe, properties, and bundles with flips or that you aren't allowed to send data out of a contract body?

Put differently, it seems odd that you can't do this:

contract a = b: wire a: Probe<UInt<1>>

However, this is illegal based on how this is written.

The example that comes to my mind is something like:

wire b: Probe<UInt<1>> contract a = b:

When you use the contract as a cutpoint, this would essentially become this in MLIR:

node a = symbolic_value : Probe<UInt<1>>

I'm not sure what a symbolic probe would be. This is almost like a pointer in software that is symbolic, potentially pointing anywhere.

You could argue that the standard should allow for this, and that the compiler should just not introduce symbolic values for types such as probes or properties. That might actually be a decent way of dealing with this.

seldridge · 2025-01-31T21:31:54Z

spec.md

+Simply put, a contract's properties can be verified to hold using an `assert` in one step, and then can be assumed to hold using an `assume` in subsequent steps.
+And similarly, if a contract only applies under certain assumptions, these are `assume`d in the first step, and then `assert`ed to hold in subsequent steps.


What are steps?

seldridge · 2025-01-31T21:36:44Z

spec.md

+
+1.  A contract can be *checked* by turning `require`s into `assume`s and `ensure`s into `assert`s.
+    Doing so verifies that a circuit upholds the contract by placing asserts on the values it produces, and by placing assumes on the input values the circuit sees.
+    In a nutshell, this checks that, assuming the inputs to the circuit honor the contract, the output from the circuit also upholds the contract.


Nit: I'd drop the softer transitions. No need for that in a spec:

Suggested change

In a nutshell, this checks that, assuming the inputs to the circuit honor the contract, the output from the circuit also upholds the contract.

Assuming the inputs to the circuit honor the contract, the output from the circuit also upholds the contract.

(Or: More Hemmingway, less Nabokov.)

seldridge · 2025-01-31T21:41:41Z

spec.md

+2.  A contract can be *applied* by turning `require`s into `assert`s and `ensure`s into `assume`s.
+    Doing so verifies that the inputs fed into a circuit uphold the contract, such that the outputs can be assumed to have the promised values.
+    In a nutshell, this checks that the inputs to a circuit honor the contract and therefore the circuit can be assumed to uphold the contract.
+    Assuming a contract can often eliminate large parts of the circuit's actual implementation, since the contracts tend to be a simpler description of a circuit's functionality.


Is there a way to write this section in terms of the behavior of a contract as opposed to how a compiler could implement them?

seldridge · 2025-01-31T21:43:11Z

spec.md

+A contract can be used to implement cutpoints, a technique commonly used in formal verification software to subdivide a large verification problem in multiple smaller ones.
+This technique separates a contract into two individual verification problems:


Similar to the above, is there a way to describe this more generically as opposed to specifically about cutpoints and assumes and asserts?

seldridge · 2025-01-31T21:44:48Z

Hmmm, not sure why the firrtl,notest code blocks don't render as FIRRTL properly 🤔

I think it has to be {.firrtl .notest}. The lua filter could likely be improved or looked at.

Add the `contract` declaration to the FIRRTL spec.

mmaloney-sf · 2025-02-03T18:20:52Z

spec.md

+    contract c, d = a, b:
+      ; contract body


These lines seem to be in subtle violation of the normal indentation grammar rules, which require a skip if the body is empty.

I was curious about this and I realized that we're inconsistently handling this today in CIRCT. Currently, an indented block is required for when, but not required for layerblock. The spec grammar says they are required for both. Python prior art has mandatory indented blocks after ifs as one form of prior art.

WDYT is saner?

I saw that layerblock doesn't require it and impemented contract in the same way. I'm fine with both -- although supporting lack of an indented block to signify an empty block feels like a more permissive approach.

My immediate reaction was that it should probably be permissive. If doing this, we should propagate that change into the grammar.

mmaloney-sf · 2025-02-03T18:23:12Z

spec.md

+    contract c, d = a, b:
+      ; contract body


Could we put a full working example here?

Otherwise, it comes off as this feature is experimental and unfinished.

👍 Good idea

mmaloney-sf · 2025-02-03T18:25:41Z

spec.md

+    ;; snippetend
+```
+
+A contract conceptually acts like a `node`{.firrtl}, defining one or more names and assigning a value to each.


What is the intention behind this?

Is there a reason this has a different syntax than nodes? Why is this necessary when we have access to the node concept already in the language?

The problem is that contracts define new values that you need to be able to refer to. For synthesis and simulation, the contract then simply passes the RHS values through to the LHS results it defines. For formal verification, the contract instead creates symbolic values for its results, and uses the contract body to check the RHS values and to constrain the LHS symbolic values.

This also has to operate on multiple values. If it only operates on a single value, you could theoretically make the whole thing an expression (a weird one with an indented body block) and use node to define a name for the result.

mmaloney-sf · 2025-02-03T18:32:15Z

spec.md

+
+A contract conceptually acts like a `node`{.firrtl}, defining one or more names and assigning a value to each.
+It also has a block to hold statements that describe the predicates and properties to be verified.
+Most commonly the `circt_verif_require` and `circt_verif_ensure` intrinsics ([@sec:intrinsics]) are used to describe pre- and post-conditions of the contract.


"Most commonly" introduces a normative claim. But this doesn't actually give any rule for what statements are allowed inside a contract block.

Can I put when statements inside them? Can I declare circuit components? Can I make connections?

If the intention is that they should only allow intrinsics, let's make that the rule. If we want to declare a placeholder concept such as "contract statements", then let's do that.

But every time we introduce a new block statement, we run afoul of specifying what should be allowed inside.

Yeah good point. I think you can put anything you want in here, the only limitation being that you cannot have data leak out of a contract by the means of connect or force.

fabianschuiki requested a review from seldridge January 31, 2025 21:03

fabianschuiki force-pushed the fschuiki/contracts branch from b876c2f to 2504804 Compare January 31, 2025 21:18

fabianschuiki changed the base branch from main to fschuiki/fix-ci January 31, 2025 21:19

fabianschuiki force-pushed the fschuiki/contracts branch from 2504804 to e44f69f Compare January 31, 2025 21:23

seldridge reviewed Jan 31, 2025

View reviewed changes

fabianschuiki changed the base branch from fschuiki/fix-ci to main January 31, 2025 23:43

[minor] Add contracts

6cd4cb2

Add the `contract` declaration to the FIRRTL spec.

fabianschuiki force-pushed the fschuiki/contracts branch from e44f69f to 6cd4cb2 Compare January 31, 2025 23:44

mmaloney-sf reviewed Feb 3, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[minor] Add contracts #273

[minor] Add contracts #273

fabianschuiki commented Jan 31, 2025

fabianschuiki commented Jan 31, 2025

seldridge left a comment

seldridge Jan 31, 2025

mwachs5 Feb 3, 2025

seldridge Jan 31, 2025

seldridge Jan 31, 2025

fabianschuiki Jan 31, 2025

seldridge Jan 31, 2025

seldridge Jan 31, 2025

seldridge Jan 31, 2025

seldridge Jan 31, 2025

seldridge commented Jan 31, 2025

mmaloney-sf Feb 3, 2025

seldridge Feb 4, 2025

fabianschuiki Feb 4, 2025

seldridge Feb 4, 2025

mmaloney-sf Feb 3, 2025

fabianschuiki Feb 4, 2025

mmaloney-sf Feb 3, 2025

fabianschuiki Feb 4, 2025

mmaloney-sf Feb 3, 2025

fabianschuiki Feb 4, 2025

		Simply put, a contract's properties can be verified to hold using an `assert` in one step, and then can be assumed to hold using an `assume` in subsequent steps.
		And similarly, if a contract only applies under certain assumptions, these are `assume`d in the first step, and then `assert`ed to hold in subsequent steps.

	In a nutshell, this checks that, assuming the inputs to the circuit honor the contract, the output from the circuit also upholds the contract.
	Assuming the inputs to the circuit honor the contract, the output from the circuit also upholds the contract.

		A contract can be used to implement cutpoints, a technique commonly used in formal verification software to subdivide a large verification problem in multiple smaller ones.
		This technique separates a contract into two individual verification problems:

[minor] Add contracts #273

Are you sure you want to change the base?

[minor] Add contracts #273

Conversation

fabianschuiki commented Jan 31, 2025

fabianschuiki commented Jan 31, 2025

seldridge left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

seldridge commented Jan 31, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment