feature: add @let support

internal/contract/contract.go

@@ -40,7 +40,7 @@ func NewTypeContract(target string) (c *TypeContract) {
 }
 
 // AddEnsures adds a ensures to this contract
-// ensures len(c.ensures) == len(@old(c.ensures)) + 1
+// ensures len(c.ensures) == len(@old{c.ensures}) + 1
 // @ensures c.ensures[len(c.ensures)-1] == e
 func (c *TypeContract) AddEnsures(e Ensures) {
 	c.ensures = append(c.ensures, e)
@@ -53,7 +53,7 @@ func (c *TypeContract) Ensures() (r []Ensures) {
 }
 
 // AddRequires adds a requires to this contract
-// @ensures len(c.requires) == len(@old(c.requires)) + 1
+// @ensures len(c.requires) == len(@old{c.requires}) + 1
 // @ensures c.requires[len(c.requires)-1] == r
 func (c *TypeContract) AddRequires(r Requires) {
 	c.requires = append(c.requires, r)
@@ -80,6 +80,7 @@ type FuncContract struct {
 	requires []Requires
 	ensures  []Ensures
 	imports  map[string]struct{}
+	lets     []Let
 	target   *ast.FuncDecl
 }
 
@@ -100,7 +101,7 @@ func (c *FuncContract) Target() (t *ast.FuncDecl) {
 }
 
 // AddRequires adds a requires to this contract
-// ensures len(c.requires) == len(@old(c.requires)) + 1
+// ensures len(c.requires) == len(@old{c.requires}) + 1
 // @ensures c.requires[len(c.requires)-1] == r
 func (c *FuncContract) AddRequires(r Requires) {
 	c.requires = append(c.requires, r)
@@ -113,7 +114,7 @@ func (c *FuncContract) Requires() (r []Requires) {
 }
 
 // AddEnsures adds a ensures to this contract
-// ensures len(c.ensures) == len(@old(c.ensures)) + 1
+// ensures len(c.ensures) == len(@old{c.ensures}) + 1
 // @ensures c.ensures[len(c.ensures)-1] == e
 func (c *FuncContract) AddEnsures(e Ensures) {
 	c.ensures = append(c.ensures, e)
@@ -135,6 +136,40 @@ func (c *FuncContract) Imports() map[string]struct{} {
 	return c.imports
 }
 
+// AddLet adds a requires to this contract
+// @ensures len(c.lets) == @old{len(c.lets)}.(int) + 1
+// @ensures c.lets[len(c.lets)-1] == l
+func (c *FuncContract) AddLet(l Let) {
+	c.lets = append(c.lets, l)
+}
+
+// Requires yields requires clauses of this contract
+// @ensures len(r) == len(c.lets)
+func (c *FuncContract) Lets() (r []Let) {
+	return c.lets
+}
+
+type Let struct {
+	expr        string
+	description string
+}
+
+// NewLet creates a Let object
+// @requires expr != ""
+func NewLet(expr, description string) Let {
+	return Let{expr: expr, description: description}
+}
+
+// ExpandedExpression yields the expanded let expression
+func (l Let) ExpandedExpression() string {
+	return l.expr
+}
+
+// Description yields the let description
+func (l Let) Description() string {
+	return l.description
+}
+
 // Requires is a @requires clause of a contract
 type Requires struct {
 	expr        string

internal/contract/generator/generator.go

@@ -241,6 +241,12 @@ func (fa fileAnalyzer) getReceiverTypeName(receiver *ast.FieldList) string {
 func (fa fileAnalyzer) generateCode(c *contract.FuncContract) (stmts []string, errs []error) {
 	result := []string{}
 	errs = []error{}
+
+	for _, let := range c.Lets() {
+		stmt := fa.generateLetCode(let)
+		result = append(result, stmt)
+	}
+
 	for _, r := range c.Requires() {
 		stmt := fa.generateRequiresCode(r, "")
 		result = append(result, stmt)
@@ -311,6 +317,14 @@ func (fileAnalyzer) generateRequiresCode(req contract.Requires, panicMsgPrefix s
 	return r
 }
 
+func (fileAnalyzer) generateLetCode(let contract.Let) (r string) {
+	const templateLet = commentPrefix + `%decl% // %description%`
+	r = strings.Replace(templateLet, "%decl%", let.ExpandedExpression(), 1)
+	r = strings.Replace(r, "%description%", let.Description(), 1)
+
+	return r
+}
+
 // @requires fd != nil
 // @requires clauses != nil && len(clauses) > 0
 // @ensures r != ""

internal/contract/parser/parser.go

@@ -100,6 +100,17 @@ func (p Parser) ParseFuncContract(funcContract *contract.FuncContract, line stri
 		}
 
 		funcContract.AddImport(clause)
+	case "let":
+		if contract.Re4old.MatchString(expr) {
+			return fmt.Errorf("@old can not be used in @let expressions: %s", expr)
+		}
+
+		clause, err := p.parseLet(expr, description)
+		if err != nil {
+			return fmt.Errorf("invalid @let clause: %w", err)
+		}
+
+		funcContract.AddLet(clause)
 	case "unmodified":
 		clauses, err := p.parseUnmodified(expr)
 		if err != nil {
@@ -116,6 +127,11 @@ func (p Parser) ParseFuncContract(funcContract *contract.FuncContract, line stri
 	return nil
 }
 
+// @requires expr != ""
+func (p Parser) parseLet(expr string, description string) (r contract.Let, err error) {
+	return contract.NewLet(expr, description), nil
+}
+
 // @requires path != ""
 // @ensures r == "" ==> err != nil
 func (p Parser) parseImport(path string) (r string, err error) {