SplitLastSeq

This module provides a tactic splitting the last instruction off a code sequence.

def extractLwAndLb (e : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

Extract the written and branched address sets L_w' and L_b'' from an equality expression.

Equations

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

def extractQ (arr : Lean.PersistentArray (Option Lean.LocalDecl)) : Lean.MetaM Lean.Expr

Find the postcondition Q of the Hoare triple among the hypotheses arr.

Equations

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

def incPcExpr (state : Lean.Expr) : Lean.Expr

Build the Expr MState.incPc state.

Equations

• incPcExpr state = (Lean.Expr.const `MState.incPc []).app state

def getStateExpr (state? : Option Lean.Expr) : Lean.Expr

The given state expression, or the bound state identifier st if none is supplied.

Equations

• getStateExpr (some state) = state
• getStateExpr none = Lean.Expr.bvar 0

def getExprOfInstForR (instr : Instr) (oldState : Lean.Expr) : Lean.MetaM Lean.Expr

Build the Expr describing how instruction instr updates oldState.

Equations

• getExprOfInstForR (Instr.LoadAddress r v) oldState = pure (Lean.mkAppN (Lean.Expr.const `MState.addRegister []) #[incPcExpr oldState, mkUInt64Lit r, mkUInt64Lit v])
• getExprOfInstForR (Instr.LoadImmediate r v) oldState = pure (Lean.mkAppN (Lean.Expr.const `MState.addRegister []) #[incPcExpr oldState, mkUInt64Lit r, mkUInt64Lit v])
• getExprOfInstForR (Instr.StoreWord reg dst) oldState = pure (Lean.mkAppN (Lean.Expr.const `MState.addMemory []) #[incPcExpr oldState, mkUInt64Lit reg, mkUInt64Lit dst])
• getExprOfInstForR instr oldState = Lean.throwError (Lean.toMessageData "Error while building R, the Instruction is not implemented yet\n for this feature")

def getExprOfInstrForRFromExpr (instr oldState : Lean.Expr) : Lean.MetaM Lean.Expr

Build the Expr describing how the reflected instruction instr updates oldState.

Equations

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

def typeSetUInt64 : Lean.Expr

The Expr of the type Set UInt64.

Equations

• typeSetUInt64 = Lean.mkApp (Lean.Expr.const `Set [Lean.Level.zero]) (Lean.Expr.const `UInt64 [])

def mkSingletonOf (n : UInt64) : Lean.Expr

Build the Expr of the singleton set {n} of UInt64.

Equations

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

def getNeSet (n : UInt64) : Lean.Expr

Build the Expr of the set of UInt64 values not equal to n.

Equations

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

def calcRExprDefault (Q lastInstrExpr : Lean.Expr) : Lean.MetaM Lean.Expr

Build the default written-register relation expression for the last instruction.

Equations

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

def tacticPeelLastInstr : Lean.ParserDescr

Peel the last instruction off the current code sequence.

Equations

• tacticPeelLastInstr = Lean.ParserDescr.node `tacticPeelLastInstr 1024 (Lean.ParserDescr.nonReservedSymbol "peelLastInstr" false)