Syntax for hoare terms

def hoareTerm.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.hoareTerm : Category

Syntax category for a full MRiscX Hoare triple together with its program.

Equations

• Lean.Parser.Category.hoareTerm = { }

def «hoareTerm___⦃_⦄_↦⟨_|_⟩⦃_⦄» : Lean.ParserDescr

A Hoare triple written with concrete mriscx ... end assembly before the triple.

Equations

• One or more equations did not get rendered due to their size.

def «hoareTerm___⦃_⦄_↦⟨_|_⟩⦃_⦄_1» : Lean.ParserDescr

A Hoare triple written with a named Code identifier before the triple.

Equations

• One or more equations did not get rendered due to their size.

def «term⦃_⦄» : Lean.ParserDescr

Notation ⦃P⦄ for a Hoare assertion on the machine state.

Equations

• One or more equations did not get rendered due to their size.

def «termX[_]» : Lean.ParserDescr

Notation x[r] for the value of register r in the current state.

Equations

• One or more equations did not get rendered due to their size.

def «termMem[_]» : Lean.ParserDescr

Notation mem[a] for the value at memory address a in the current state.

Equations

• One or more equations did not get rendered due to their size.

def «termLabels[_]» : Lean.ParserDescr

Notation labels[l] for the target index of label l in the current state.

Equations

• One or more equations did not get rendered due to their size.

def «termLabels[._]» : Lean.ParserDescr

Notation labels[.l] for the target index of a dotted label l.

Equations

• One or more equations did not get rendered due to their size.

def «term⸨pc⸩» : Lean.ParserDescr

To avoid parsing errors we decided to put these double parenthesis around these tokens

Equations

• «term⸨pc⸩» = Lean.ParserDescr.node `«term⸨pc⸩» 1024 (Lean.ParserDescr.symbol "⸨pc⸩")

def «term⸨terminated⸩» : Lean.ParserDescr

Notation ⸨terminated⸩ for the termination flag of the current state.

Equations

• «term⸨terminated⸩» = Lean.ParserDescr.node `«term⸨terminated⸩» 1024 (Lean.ParserDescr.symbol "⸨terminated⸩")

def hoareAssignment.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.hoareAssignment : Category

Syntax category for a single state assignment in a Hoare postcondition.

Equations

• Lean.Parser.Category.hoareAssignment = { }

def Lean.Parser.Category.hoareAssignmentChain : Category

Syntax category for a chain of state assignments separated by ;.

Equations

• Lean.Parser.Category.hoareAssignmentChain = { }

def hoareAssignmentChain.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.hoareAssignmentTerm : Category

Syntax category for a bracketed Hoare assignment block ⟦ ... ⟧.

Equations

• Lean.Parser.Category.hoareAssignmentTerm = { }

def hoareAssignmentTerm.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «hoareAssignmentX[_]←_» : Lean.ParserDescr

Assignment x[r] ← v setting register r to v.

Equations

• One or more equations did not get rendered due to their size.

def «hoareAssignmentX[_]<-_» : Lean.ParserDescr

Assignment x[r] <- v, an ASCII variant of x[r] ← v.

Equations

• One or more equations did not get rendered due to their size.

def «hoareAssignmentMem[_]←_» : Lean.ParserDescr

Assignment mem[a] ← v setting memory address a to v.

Equations

• One or more equations did not get rendered due to their size.

def «hoareAssignmentMem[_]<-_» : Lean.ParserDescr

Assignment mem[a] <- v, an ASCII variant of mem[a] ← v.

Equations

• One or more equations did not get rendered due to their size.

def «hoareAssignmentPc++» : Lean.ParserDescr

Assignment pc++ incrementing the program counter.

Equations

• One or more equations did not get rendered due to their size.

def «hoareAssignmentPc←_» : Lean.ParserDescr

Assignment pc ← l setting the program counter to l.

Equations

• One or more equations did not get rendered due to their size.

def «hoareAssignmentTerm⟦⟧» : Lean.ParserDescr

The empty assignment block ⟦⟧, denoting the unchanged state.

Equations

• «hoareAssignmentTerm⟦⟧» = Lean.ParserDescr.node `«hoareAssignmentTerm⟦⟧» 1024 (Lean.ParserDescr.symbol "⟦⟧")

def hoareAssignmentChain_ : Lean.ParserDescr

A single assignment, viewed as a one-element assignment chain.

Equations

• hoareAssignmentChain_ = Lean.ParserDescr.node `hoareAssignmentChain_ 1022 (Lean.ParserDescr.cat `hoareAssignment 0)

def «hoareAssignmentChain_;_» : Lean.ParserDescr

Two assignments composed with ;.

Equations

• One or more equations did not get rendered due to their size.

def «hoareAssignmentChain_;__1» : Lean.ParserDescr

An assignment followed by a further assignment chain, composed with ;.

Equations

• One or more equations did not get rendered due to their size.

def «hoareAssignmentChain_;__2» : Lean.ParserDescr

An assignment followed by a base-case term, composed with ;.

Equations

• One or more equations did not get rendered due to their size.

def «hoareAssignmentTerm⟦_⟧» : Lean.ParserDescr

A bracketed assignment block ⟦ ... ⟧ denoting the resulting state update.

Equations

• One or more equations did not get rendered due to their size.