inductive ISAR.Instruction : Type

Stack-based VM instructions.

• push_I : Instruction
• push_K : Instruction
• push_S : Instruction
• app : Instruction

@[implicit_reducible]

instance ISAR.instDecidableEqInstruction : DecidableEq Instruction

Equations

• ISAR.instDecidableEqInstruction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ISAR.instReprInstruction.repr : Instruction → ℕ → Std.Format

Equations

• ISAR.instReprInstruction.repr ISAR.Instruction.push_I prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.Instruction.push_I")).group prec✝
• ISAR.instReprInstruction.repr ISAR.Instruction.push_K prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.Instruction.push_K")).group prec✝
• ISAR.instReprInstruction.repr ISAR.Instruction.push_S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.Instruction.push_S")).group prec✝
• ISAR.instReprInstruction.repr ISAR.Instruction.app prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.Instruction.app")).group prec✝

@[implicit_reducible]

instance ISAR.instReprInstruction : Repr Instruction

Equations

• ISAR.instReprInstruction = { reprPrec := ISAR.instReprInstruction.repr }

def ISAR.run : List Instruction → List TTerm → List TTerm

Execute a list of bytecode instructions on a VM stack of TTerms.

Equations

• ISAR.run [] x✝ = x✝
• ISAR.run (ISAR.Instruction.push_I :: insts) x✝ = ISAR.run insts (ISAR.TTerm.I :: x✝)
• ISAR.run (ISAR.Instruction.push_K :: insts) x✝ = ISAR.run insts (ISAR.TTerm.K :: x✝)
• ISAR.run (ISAR.Instruction.push_S :: insts) x✝ = ISAR.run insts (ISAR.TTerm.S :: x✝)
• ISAR.run (ISAR.Instruction.app :: insts) (x_2 :: y :: stack) = ISAR.run insts (y.app x_2 :: stack)
• ISAR.run (ISAR.Instruction.app :: insts) x✝ = ISAR.run insts (ISAR.TTerm.I :: x✝)

theorem ISAR.run_app_nil (insts : List Instruction) : run (Instruction.app :: insts) [] = run insts [TTerm.I]

Step lemmas for VM execution when the stack is concrete.

theorem ISAR.run_app_one (insts : List Instruction) (x : TTerm) : run (Instruction.app :: insts) [x] = run insts [TTerm.I, x]

theorem ISAR.run_app_two (insts : List Instruction) (x y : TTerm) (stack : List TTerm) : run (Instruction.app :: insts) (x :: y :: stack) = run insts (y.app x :: stack)

def ISAR.compile_bytecode (p : List Instruction) : TTerm

Compile a bytecode program by running it on an empty stack and taking the top term.

Equations

• ISAR.compile_bytecode p = match ISAR.run p [] with | x :: tail => x | [] => ISAR.TTerm.I

def ISAR.decompile : TTerm → List Instruction

Decompile a TTerm into a list of postfix stack instructions.

Equations

• ISAR.decompile ISAR.TTerm.I = [ISAR.Instruction.push_I]
• ISAR.decompile ISAR.TTerm.K = [ISAR.Instruction.push_K]
• ISAR.decompile ISAR.TTerm.S = [ISAR.Instruction.push_S]
• ISAR.decompile (t1.app t2) = ISAR.decompile t1 ++ ISAR.decompile t2 ++ [ISAR.Instruction.app]

theorem ISAR.run_concat (p1 p2 : List Instruction) (stack : List TTerm) : run (p1 ++ p2) stack = run p2 (run p1 stack)

Lemma: Executing a concatenated program corresponds to staged execution.

theorem ISAR.run_decompile_eq (t : TTerm) (stack : List TTerm) : run (decompile t) stack = t :: stack

Lemma: Executing a decompiled TTerm on any stack pushes the term onto the stack.

theorem ISAR.compile_bytecode_decompile (t : TTerm) : compile_bytecode (decompile t) = t

Theorem: Compiling a decompiled TTerm returns the original term.

def ISAR.bytecode_obs_eq (p1 p2 : List Instruction) : Prop

Observational equivalence for bytecode programs (evaluating to equivalent terms).

Equations

• ISAR.bytecode_obs_eq p1 p2 = ISAR.OperEq (ISAR.trs_encode (ISAR.compile_bytecode p1)) (ISAR.trs_encode (ISAR.compile_bytecode p2))

theorem ISAR.bytecode_obs_equiv : Equivalence bytecode_obs_eq

Observational equivalence is a setoid.

def ISAR.bytecodeObsSetoid : Setoid (List Instruction)

Setoid of bytecode observations.

Equations

• ISAR.bytecodeObsSetoid = { r := ISAR.bytecode_obs_eq, iseqv := ISAR.bytecode_obs_equiv }

@[reducible, inline]

abbrev ISAR.BytecodeObs : Type

Observation space: bytecode programs modulo observational equivalence.

Equations

• ISAR.BytecodeObs = Quotient ISAR.bytecodeObsSetoid

def ISAR.decode_bytecode_raw (t : ISKSubtype) : List Instruction

Substrate term → bytecode program (computable).

Equations

• ISAR.decode_bytecode_raw t = ISAR.decompile (ISAR.decode_raw t)

def ISAR.decode_bytecode (q : InvariantLayer) : BytecodeObs

Decode an OperEq-class to a bytecode observation. Well-defined via compile ∘ decompile = id and trs_encode ∘ decode_raw = id.

Equations

• ISAR.decode_bytecode q = Quotient.lift (fun (t : ISAR.ISKSubtype) => ⟦ISAR.decode_bytecode_raw t⟧) ISAR.decode_bytecode._proof_1 q

def ISAR.Bytecode_Dialect : Dialect

The concrete Bytecode_Dialect : Dialect instance (computable; OperEq observations).

Equations

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