CodeProofTactics

This module provides tactics for discharging MRiscX code-proof goals.

def tacticAutoSeq : Lean.ParserDescr

Apply S_SEQ to 'peel' off the last instruction. Also, try to solve all goals which are created during the process except for the two goals, which involve the actual Hoare-triples which will be generated.

Equations

• tacticAutoSeq = Lean.ParserDescr.node `tacticAutoSeq 1022 (Lean.ParserDescr.nonReservedSymbol "autoSeq" false)

def «tacticSapplySSeqP:=_,R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» : Lean.ParserDescr

Apply the Hoare rule S_SEQ in order to split the current Hoare triple into two. To do so, the names and values must be provided explicitly, each separated by a colon.

The order is:

1. P
2. R
3. L_W
4. L_W'
5. L_B
6. L_B'

Also, try to automatically solve most of the "side goals" that are generated during the process. These side goals are generally statements about the provided sets (e.g., L_W ≠ ∅), which are trivial in most cases.

The same tactic can be used without providing P

Equations

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

def «tacticSapplySSeqR:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» : Lean.ParserDescr

The same as the other sapplySSeq tactic, but without having to provide P.

Equations

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

def «tacticSapplySSeq'_,_,_,_» : Lean.ParserDescr

Apply the sequencing rule S_SEQ with the given assertions and address sets.

Equations

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

def «tacticSapplySSeq''_,_,_,_,_» : Lean.ParserDescr

Like sapplySSeq, but without solving the sidegoal L_b = L_b' ∩ L_b''.

Equations

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

def «tacticSapplySSeq''R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» : Lean.ParserDescr

Apply S_SEQ without explicitly providing the names of the parameters. The order is:

1. R
2. L_W
3. L_W'
4. L_B
5. L_B'

Also, try to automatically solve the most "side goals", which are generated during the process. Those side goals generally are goals about the set provided (e.g. L_W ≠ ∅), which are trivial is most cases.

Equations

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

def «tacticSapplySSeq''P:=_,R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» : Lean.ParserDescr

Apply S_SEQ with explicitly providing the names and values of the parameters. The order is:

1. P
2. R
3. L_W
4. L_W'
5. L_B
6. L_B'

Also, try to automatically solve the most "side goals", which are generated during the process. Those side goals generally are goals about the set provided (e.g. L_W ≠ ∅), which are trivial is most cases.

Equations

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

def «tacticSapplySSeqPlainP:=_,R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» : Lean.ParserDescr

Apply S_SEQ without explicitly providing the names of the parameters. The order is:

1. P
2. R
3. L_W
4. L_W'
5. L_B
6. L_B'

Equations

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

def «tacticSapplySSeqPlainR:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» : Lean.ParserDescr

Apply the plain sequencing rule with the given assertions and address sets.

Equations

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

def «tacticSapplySSeq'''P:=_,R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» : Lean.ParserDescr

Like sapplySSeq'', but also apply a tactic to automatically solve the set equality which should be able to show L_{B''} = L_B ∩ L_{B'}.

Equations

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

def «tacticSapplySSeq'''R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» : Lean.ParserDescr

Apply S_SEQ with explicitly providing the names of the parameters. The order is:

1. R
2. L_W
3. L_W'
4. L_B
5. L_B'

Also, apply a tactic to automatically solve set equality which should be able to show L_{B''} = L_B ∩ L_{B'}.

Equations

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

def tacticCleanupGoalsAfterSpec : Lean.ParserDescr

Discharge the routine side goals left after applying an instruction specification.

Equations

• tacticCleanupGoalsAfterSpec = Lean.ParserDescr.node `tacticCleanupGoalsAfterSpec 1024 (Lean.ParserDescr.nonReservedSymbol "cleanupGoalsAfterSpec" false)

def tacticCleanupAfterAutomation : Lean.ParserDescr

Clean up the goals remaining after the proof automation has run.

Equations

• tacticCleanupAfterAutomation = Lean.ParserDescr.node `tacticCleanupAfterAutomation 1024 (Lean.ParserDescr.nonReservedSymbol "cleanupAfterAutomation" false)

def tacticCleanupGoalsAfterSpecWSetEq : Lean.ParserDescr

Discharge the side goals after applying a specification, using set equalities.

Equations

• tacticCleanupGoalsAfterSpecWSetEq = Lean.ParserDescr.node `tacticCleanupGoalsAfterSpecWSetEq 1024 (Lean.ParserDescr.nonReservedSymbol "cleanupGoalsAfterSpecWSetEq" false)

def tacticApplySpecAndCleanup_ : Lean.ParserDescr

Apply the given instruction specification and clean up the resulting goals.

Equations

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

def tacticApplySpecDefault_ : Lean.ParserDescr

Apply the default instruction specification and clean up the resulting goals.

Equations

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

def tacticApplySpecForSecond_ : Lean.ParserDescr

Apply an instruction specification to the second goal and clean up.

Equations

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

def tacticApplySpec_ : Lean.ParserDescr

Apply a given specification and try to get rid of all proof goals which are create during the process.

To be able to apply a specification, L_B must contain every line except the one that is being executed. For example, if you want to apply the specification for the Instr.LoadImmediate, which is on line l, and you have some (P Q : Prop), then the Hoare-triple needs to look like this:

⦃P⦄ l ↦ ⟨{l+1} | {n:UInt64 | n ≠ l + 1}⟩ ⦃Q⦄

TODO: Avoid having to provide pc, registers and values in application of specification

Equations

• tacticApplySpec_ = Lean.ParserDescr.node `tacticApplySpec_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "applySpec" false) (Lean.ParserDescr.cat `term 0))

def tacticApplySpec'_ : Lean.ParserDescr

Apply the instruction specification named by the given identifier.

Equations

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

def tacticApplySpec'' : Lean.ParserDescr

Apply the instruction specification inferred from the current goal.

Equations

• tacticApplySpec'' = Lean.ParserDescr.node `tacticApplySpec'' 1024 (Lean.ParserDescr.nonReservedSymbol "applySpec''" false)