i am missing the basic user understanding of when something should go into the argument list of the Contract or just be captured in the closure of the body.

Your actual hardware would go into the argument list. And the body then describes what your hardware does:

val z_impl = Instance(new MyFancyMultiplier(a, b))
val z = FormalContract(z_impl) { case z =>
  EnsureProperty(z === a * b)
}

This will turn into a AssertProperty(z_impl === a * b) to check that the multiplier works, and a separate val z = a * b during formal verification.

what is the user intuition for why you put the (a << 3) + a term into the argument list for the Contract but the a*9 term is only used in the body of the contract?

The example is a bit simplistic, but you would pass the actual implementation of your circuit, for example a radix-4 Booth multiplier, to the contract as an argument. The rationale is that you want the contract to act as a cutpoint, detaching the implementation and replacing it with a symbolic value during formal verification. You'd then use a simpler expression inside the contract to characterize your circuit, for example a * b for your multiplier.

kind of a nit but using the same variable b both inside and as the return value of the contract is a little confusing. What is the point of the return value b, how does one use that returned value?

The body of the contract wants to talk about the result of the contract, which is either what you pass into the argument list (during synthesis and when checking that your hardware upholds the contract), or it's a symbolic value (during formal verification when you assume that the contract holds). There isn't really a good way to do this in Scala... so the contract passes the value it produces as a result to the body as well.

again, what is the point of val (u, v) that is returned here? what are they and what do you do with them?

what are "the contract results"? what does that mean? If I am passing the arguments anyway, why do i need the contract to return them again, couldn't i just use that myself like:

val a = ...
Contract(a) { b => 
  assume (b == ...)
}
AssertProperty(a)

i guess if you didn't to have to give a named variable to a before you pass it to the contract, this can help

This is due to the cutpoint behaviour of a contract during formal verification. When doing formal verification, the contract doesn't just forward its argument list to its results, but instead creates symbolic values as its results that are then constrained by the contract body. (Which is why the body takes arguments as well: it needs to constrain either the hardware, or the symbolic value, depending on which part you're verifying.)

What about Scala 3? The code that can be shared should be in src/main/scala. The macro is cool and I do think it's better, but if you just did the annoying thing and write the method for 1 to N arguments (e.g. DataProduct support for Tuples), then it would work for both Scala 2 and 3.

Good call. I've moved the common code into scala/chisel3 and added an explicit scala-3/chisel3 with the Scala 3 specific stuff.

This is fantastic Scaladoc. It's on a private trait, though. Where is it expected to show up? Is there some other place it should go?

My hope was that this would show up on Scala 2 and Scala 3 object FormalContract which extends ObjectFormalContractImpl. Let me check how doc inheritance works for private base classes/traits -- otherwise I can always factor this into a public dummy base as we do for some of the source location macro stuff.

I just realized that this should actually be public. The apply and mapped functions are supposed to be available to users of the API. That should also fix the doc issue.

I just realized that this should actually be public

This should not be public--we don't want the Scala 2 / Scala 3 split visible in the public API.

The apply and mapped functions are supposed to be available to users of the API.

Even wit the trait package private, apply and mapped are public on any classes/objects that mix the trait in so no problem there.

That should also fix the doc issue.

That won't really fix the doc issue because users would still have to click through to the trait to see the doc which isn't what we want, we want it to show up on the object FormalContract.

I think you need to put /** @inheritdoc */ on each object FormalContract to make inheritance work. Now if that can't work from a package private trait, then you could move the Scala doc to a public trait that is nothing but the doc, but I think the implementations of mapped and apply should stick around on a private trait.

All of this being said

I'd like to invert the public/private relationship such that the public classes and objects lives in src/main/scala and only package private traits that provide the public methods using macros live in src/main/scala-2 and src/main/scala-3. So here's what I think you should really do.

Create a new package private trait (probably called FormalContract$VirtualMethods¹) in this file (core/src/main/scala/chisel3/FormalContractImpl.scala) that just defines the virtual method mapped. Change the code in src/main/scala-2 and src/main/scala-3 to be package private traits (probably called FormalContract$Intf) that extend FormalContract$VirtualMethods and self-typed on FormalContract.type² but still provide the public methods that use macros. Then back in this file, make object FormalContract extends FormalContract$Intf and you'll just need the ScalaDoc there. It's more clear than the old pattern IMO, I need to roll out this new approach to the rest of the code base.

A lot of this FormalContractIntf vs. FormalContract$Intf may feel silly since there's no class FormalContract, but elsewhere in the code base we have classes and companion objects so I want to define a single style that works across the board.

I've laid this out more explicitly and with an example in #4768

Really nice. I've moved the contracts to this new pattern.