ARM Instructions

This file defines ARM AArch64 instructions used in s2n-bignum. This will be expanded to include all instructions needed for bignum operations.

References

Source: s2n-bignum/arm/proofs/instruction.ml (ARM instruction definitions)

inductive Bignum.Arm.Instruction : Type

ARM instruction type.

This is a simplified model focusing on the instructions used in s2n-bignum. Each instruction corresponds to an ARM opcode.

• ADD : Reg → Reg → Reg → Instruction
• SUB : Reg → Reg → Reg → Instruction
• ADDS : Reg → Reg → Reg → Instruction
• SUBS : Reg → Reg → Reg → Instruction
• ADCS : Reg → Reg → Reg → Instruction
• SBCS : Reg → Reg → Reg → Instruction
• AND : Reg → Reg → Reg → Instruction
• ORR : Reg → Reg → Reg → Instruction
• EOR : Reg → Reg → Reg → Instruction
• LSL : Reg → Reg → ℕ → Instruction
• LSR : Reg → Reg → ℕ → Instruction
• LDR : Reg → Address → Instruction
• STR : Reg → Address → Instruction
• MOV : Reg → Reg → Instruction
• MOVZ : Reg → ℕ → ℕ → Instruction
• MUL : Reg → Reg → Reg → Instruction
• RET : Instruction

instance Bignum.Arm.instReprInstruction : Repr Instruction

Equations

• Bignum.Arm.instReprInstruction = { reprPrec := Bignum.Arm.instReprInstruction.repr }

def Bignum.Arm.instReprInstruction.repr : Instruction → ℕ → Std.Format

Equations

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

def Bignum.Arm.Instruction.toString : Instruction → String

Pretty-print an instruction in ARM assembly syntax.

Equations

• (Bignum.Arm.Instruction.ADD rd rn rm).toString = toString "ADD " ++ toString rd ++ toString ", " ++ toString rn ++ toString ", " ++ toString rm
• (Bignum.Arm.Instruction.SUB rd rn rm).toString = toString "SUB " ++ toString rd ++ toString ", " ++ toString rn ++ toString ", " ++ toString rm
• (Bignum.Arm.Instruction.ADDS rd rn rm).toString = toString "ADDS " ++ toString rd ++ toString ", " ++ toString rn ++ toString ", " ++ toString rm
• (Bignum.Arm.Instruction.SUBS rd rn rm).toString = toString "SUBS " ++ toString rd ++ toString ", " ++ toString rn ++ toString ", " ++ toString rm
• (Bignum.Arm.Instruction.ADCS rd rn rm).toString = toString "ADCS " ++ toString rd ++ toString ", " ++ toString rn ++ toString ", " ++ toString rm
• (Bignum.Arm.Instruction.SBCS rd rn rm).toString = toString "SBCS " ++ toString rd ++ toString ", " ++ toString rn ++ toString ", " ++ toString rm
• (Bignum.Arm.Instruction.AND rd rn rm).toString = toString "AND " ++ toString rd ++ toString ", " ++ toString rn ++ toString ", " ++ toString rm
• (Bignum.Arm.Instruction.ORR rd rn rm).toString = toString "ORR " ++ toString rd ++ toString ", " ++ toString rn ++ toString ", " ++ toString rm
• (Bignum.Arm.Instruction.EOR rd rn rm).toString = toString "EOR " ++ toString rd ++ toString ", " ++ toString rn ++ toString ", " ++ toString rm
• (Bignum.Arm.Instruction.LSL rd rn imm).toString = toString "LSL " ++ toString rd ++ toString ", " ++ toString rn ++ toString ", #" ++ toString imm
• (Bignum.Arm.Instruction.LSR rd rn imm).toString = toString "LSR " ++ toString rd ++ toString ", " ++ toString rn ++ toString ", #" ++ toString imm
• (Bignum.Arm.Instruction.LDR rd addr).toString = toString "LDR " ++ toString rd ++ toString ", [" ++ toString (Bignum.Word64.val addr) ++ toString "]"
• (Bignum.Arm.Instruction.STR rd addr).toString = toString "STR " ++ toString rd ++ toString ", [" ++ toString (Bignum.Word64.val addr) ++ toString "]"
• (Bignum.Arm.Instruction.MOV rd rn).toString = toString "MOV " ++ toString rd ++ toString ", " ++ toString rn
• (Bignum.Arm.Instruction.MOVZ rd imm pos).toString = toString "MOVZ " ++ toString rd ++ toString ", #" ++ toString imm ++ toString ", LSL #" ++ toString pos
• (Bignum.Arm.Instruction.MUL rd rn rm).toString = toString "MUL " ++ toString rd ++ toString ", " ++ toString rn ++ toString ", " ++ toString rm
• Bignum.Arm.Instruction.RET.toString = "RET"

instance Bignum.Arm.instToStringInstruction : ToString Instruction

Equations

• Bignum.Arm.instToStringInstruction = { toString := Bignum.Arm.Instruction.toString }

structure Bignum.Arm.Program : Type

A program is a sequence of instructions with a base address (PC).

• base_addr : Word64
• instructions : List Instruction

def Bignum.Arm.instReprProgram.repr : Program → ℕ → Std.Format

Equations

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

instance Bignum.Arm.instReprProgram : Repr Program

Equations

• Bignum.Arm.instReprProgram = { reprPrec := Bignum.Arm.instReprProgram.repr }

def Bignum.Arm.Program.split (p : Program) (i : ℕ) : Program × Program

Equations

• p.split i = ({ base_addr := p.base_addr, instructions := List.take i p.instructions }, { base_addr := p.base_addr + Bignum.Word64.ofNat (i * 4), instructions := List.drop i p.instructions })

ARM Instruction Semantics

This section defines the operational semantics of ARM instructions. Each instruction transforms an ArmState to a new ArmState.

The step function corresponds to the small-step operational semantics τ ⊆ Σ × Σ from the article (Section 4), where execution of a single instruction updates state s to s'.

References

Source: s2n-bignum/arm/proofs/arm.ml (ARM semantics)

def Bignum.Arm.step (instr : Instruction) (s : ArmState) : ArmState

Execute a single ARM instruction, transforming the state.

This corresponds to the symbolic execution performed by HOL Light's ARM_STEPS_TAC in the proof.

Equations

• One or more equations did not get rendered due to their size.
• Bignum.Arm.step (Bignum.Arm.Instruction.ADD rd rn rm) s = (s.write_reg rd (s.read_reg rn + s.read_reg rm)).write_reg Bignum.Arm.Reg.PC (s.read_reg Bignum.Arm.Reg.PC + 4)
• Bignum.Arm.step (Bignum.Arm.Instruction.SUB rd rn rm) s = (s.write_reg rd (s.read_reg rn - s.read_reg rm)).write_reg Bignum.Arm.Reg.PC (s.read_reg Bignum.Arm.Reg.PC + 4)
• Bignum.Arm.step (Bignum.Arm.Instruction.AND rd rn rm) s = (s.write_reg rd (s.read_reg rn &&& s.read_reg rm)).write_reg Bignum.Arm.Reg.PC (s.read_reg Bignum.Arm.Reg.PC + 4)
• Bignum.Arm.step (Bignum.Arm.Instruction.ORR rd rn rm) s = (s.write_reg rd (s.read_reg rn ||| s.read_reg rm)).write_reg Bignum.Arm.Reg.PC (s.read_reg Bignum.Arm.Reg.PC + 4)
• Bignum.Arm.step (Bignum.Arm.Instruction.EOR rd rn rm) s = (s.write_reg rd (s.read_reg rn ^^^ s.read_reg rm)).write_reg Bignum.Arm.Reg.PC (s.read_reg Bignum.Arm.Reg.PC + 4)
• Bignum.Arm.step (Bignum.Arm.Instruction.LSL rd rn imm) s = (s.write_reg rd (s.read_reg rn <<< imm)).write_reg Bignum.Arm.Reg.PC (s.read_reg Bignum.Arm.Reg.PC + 4)
• Bignum.Arm.step (Bignum.Arm.Instruction.LSR rd rn imm) s = (s.write_reg rd (s.read_reg rn >>> imm)).write_reg Bignum.Arm.Reg.PC (s.read_reg Bignum.Arm.Reg.PC + 4)
• Bignum.Arm.step (Bignum.Arm.Instruction.STR rd addr) s = (s.write_mem_word64 addr (s.read_reg rd)).write_reg Bignum.Arm.Reg.PC (s.read_reg Bignum.Arm.Reg.PC + 4)
• Bignum.Arm.step (Bignum.Arm.Instruction.MOV rd rn) s = (s.write_reg rd (s.read_reg rn)).write_reg Bignum.Arm.Reg.PC (s.read_reg Bignum.Arm.Reg.PC + 4)
• Bignum.Arm.step (Bignum.Arm.Instruction.MOVZ rd imm pos) s = (s.write_reg rd (Bignum.Word64.ofNat (imm * 2 ^ pos))).write_reg Bignum.Arm.Reg.PC (s.read_reg Bignum.Arm.Reg.PC + 4)
• Bignum.Arm.step (Bignum.Arm.Instruction.MUL rd rn rm) s = (s.write_reg rd (s.read_reg rn * s.read_reg rm)).write_reg Bignum.Arm.Reg.PC (s.read_reg Bignum.Arm.Reg.PC + 4)
• Bignum.Arm.step Bignum.Arm.Instruction.RET s = s.write_reg Bignum.Arm.Reg.PC (s.read_reg Bignum.Arm.Reg.X30)

def Bignum.Arm.exec (instrs : List Instruction) (s : ArmState) : ArmState

Execute multiple instructions sequentially.

This corresponds to ARM_STEPS_TAC EXEC (1--n) in HOL Light proofs. Source: s2n-bignum/arm/tutorial/simple.ml:92 (ARM_STEPS_TAC EXEC (1--2))

Equations

• Bignum.Arm.exec instrs s = List.foldl (fun (state : Bignum.Arm.ArmState) (instr : Bignum.Arm.Instruction) => Bignum.Arm.step instr state) s instrs

def Bignum.Arm.exec_program (prog : Program) (s : ArmState) : ArmState

Execute a program from its base address.

Equations

• Bignum.Arm.exec_program prog s = if s.read_reg Bignum.Arm.Reg.PC = prog.base_addr then Bignum.Arm.exec prog.instructions s else s