very restricted cpp subset.lean

notation `i32_variable_t` := ℕ
notation `i64_variable_t` := ℕ
notation `i8_value_t` := fin 256
notation `i32_value_t` := fin 4294967296
notation `i64_value_t` := fin 18446744073709551616
notation `ℕ` := ℕ

inductive instruction_t
| i32_const (value : i32_value_t) (output : i32_variable_t) : instruction_t
| i32_duplicate (input : i32_variable_t) (output : i32_variable_t) : instruction_t
| i32_add (input1 : i32_variable_t) (input2 : i32_variable_t) (output : i32_variable_t) : instruction_t
| i32_subtract (input1 : i32_variable_t) (input2 : i32_variable_t) (output : i32_variable_t) : instruction_t
| i32_multiply (input1 : i32_variable_t) (input2 : i32_variable_t) (output : i32_variable_t) : instruction_t
| i32_unsigned_divide (input1 : i32_variable_t) (input2 : i32_variable_t) (output : i32_variable_t) : instruction_t
| i32_signed_divide (input1 : i32_variable_t) (input2 : i32_variable_t) (output : i32_variable_t) : instruction_t
| i32_unsigned_mod (input1 : i32_variable_t) (input2 : i32_variable_t) (output : i32_variable_t) : instruction_t
| i32_signed_mod (input1 : i32_variable_t) (input2 : i32_variable_t) (output : i32_variable_t) : instruction_t
| i32_and (input1 : i32_variable_t) (input2 : i32_variable_t) (output : i32_variable_t) : instruction_t
| i32_or (input1 : i32_variable_t) (input2 : i32_variable_t) (output : i32_variable_t) : instruction_t
| i32_xor (input1 : i32_variable_t) (input2 : i32_variable_t) (output : i32_variable_t) : instruction_t
| i32_not (input : i32_variable_t) (output : i32_variable_t) : instruction_t
| i32_shift_left (input1 : i32_variable_t) (input2 : i32_variable_t) (output : i32_variable_t) : instruction_t
| i32_shift_right (input1 : i32_variable_t) (input2 : i32_variable_t) (output : i32_variable_t) : instruction_t
| i32_to_i64 (input : i32_variable_t) (output : i64_variable_t) : instruction_t
| i64_const (value : i64_value_t) (output : i64_variable_t) : instruction_t
| i64_duplicate (input : i64_variable_t) (output : i64_variable_t) : instruction_t
| i64_add (input1 : i64_variable_t) (input2 : i64_variable_t) (output : i64_variable_t) : instruction_t
| i64_subtract (input1 : i64_variable_t) (input2 : i64_variable_t) (output : i64_variable_t) : instruction_t
| i64_multiply (input1 : i64_variable_t) (input2 : i64_variable_t) (output : i64_variable_t) : instruction_t
| i64_unsigned_divide (input1 : i64_variable_t) (input2 : i64_variable_t) (output : i64_variable_t) : instruction_t
| i64_signed_divide (input1 : i64_variable_t) (input2 : i64_variable_t) (output : i64_variable_t) : instruction_t
| i64_unsigned_mod (input1 : i64_variable_t) (input2 : i64_variable_t) (output : i64_variable_t) : instruction_t
| i64_signed_mod (input1 : i64_variable_t) (input2 : i64_variable_t) (output : i64_variable_t) : instruction_t
| i64_and (input1 : i64_variable_t) (input2 : i64_variable_t) (output : i64_variable_t) : instruction_t
| i64_or (input1 : i64_variable_t) (input2 : i64_variable_t) (output : i64_variable_t) : instruction_t
| i64_xor (input1 : i64_variable_t) (input2 : i64_variable_t) (output : i64_variable_t) : instruction_t
| i64_not (input : i64_variable_t) (output : i64_variable_t) : instruction_t
| i64_shift_left (input1 : i64_variable_t) (input2 : i64_variable_t) (output : i64_variable_t) : instruction_t
| i64_shift_right (input1 : i64_variable_t) (input2 : i64_variable_t) (output : i64_variable_t) : instruction_t
| i64_to_i32 (input : i64_variable_t) (output : i32_variable_t) : instruction_t
| i8_unsigned_load (address : i32_variable_t) (output : i32_variable_t) : instruction_t
| i8_signed_load (address : i32_variable_t) (output : i32_variable_t) : instruction_t
| i8_store (address : i32_variable_t) (input : i32_variable_t) : instruction_t
| i16_unsigned_load (address : i32_variable_t) (output : i32_variable_t) : instruction_t
| i16_signed_load (address : i32_variable_t) (output : i32_variable_t) : instruction_t
| i16_store (address : i32_variable_t) (input : i32_variable_t) : instruction_t
| i32_load (address : i32_variable_t) (output : i32_variable_t) : instruction_t
| i32_store (address : i32_variable_t) (input : i32_variable_t) : instruction_t
| i64_load (address : i32_variable_t) (output : i64_variable_t) : instruction_t
| i64_store (address : i32_variable_t) (input : i64_variable_t) : instruction_t
| break : instruction_t
| break_if (input : i32_variable_t) : instruction_t
| loop (instructions : list instruction_t) : instruction_t

inductive with_fictive_instructions_t
| basic_instruction (instruction : instruction_t) : with_fictive_instructions_t
| expanded_loop (next_iteration : list instruction_t) (current : list instruction_t) : with_fictive_instructions_t
| terminated_normally : with_fictive_instructions_t
| terminated_abnormally : with_fictive_instructions_t

structure program_t :=
(instructions : list instruction_t)
(memory_size : ℕ)
(i32_count : ℕ)
(i64_count : ℕ)

namespace internal
open instruction_t

def extract_body (i32_count i64_count : ℕ) : list instruction_t → string
| [] := ""
| (i32_const value output::rest) := (if output < i32_count then "s" ++ to_string output ++ "=" ++ to_string value ++ ";" else "") ++ extract_body rest
| (i32_duplicate input output::rest) := (if input < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=s" ++ to_string input ++ ";" else "") ++ extract_body rest
| (i32_add input1 input2 output::rest) := (if input1 < i32_count ∧ input2 < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=s" ++ to_string input1 ++ "+s" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i32_subtract input1 input2 output::rest) := (if input1 < i32_count ∧ input2 < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=s" ++ to_string input1 ++ "-s" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i32_multiply input1 input2 output::rest) := (if input1 < i32_count ∧ input2 < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=s" ++ to_string input1 ++ "*s" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i32_unsigned_divide input1 input2 output::rest) := (if input1 < i32_count ∧ input2 < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=s" ++ to_string input1 ++ "/s" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i32_signed_divide input1 input2 output::rest) := (if input1 < i32_count ∧ input2 < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=(int32_t)s" ++ to_string input1 ++ "/(int32_t)s" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i32_unsigned_mod input1 input2 output::rest) := (if input1 < i32_count ∧ input2 < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=s" ++ to_string input1 ++ "%s" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i32_signed_mod input1 input2 output::rest) := (if input1 < i32_count ∧ input2 < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=(int32_t)s" ++ to_string input1 ++ "%(int32_t)s" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i32_and input1 input2 output::rest) := (if input1 < i32_count ∧ input2 < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=s" ++ to_string input1 ++ "&s" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i32_or input1 input2 output::rest) := (if input1 < i32_count ∧ input2 < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=s" ++ to_string input1 ++ "|s" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i32_xor input1 input2 output::rest) := (if input1 < i32_count ∧ input2 < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=s" ++ to_string input1 ++ "^s" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i32_not input output::rest) := (if input < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=~s" ++ to_string input ++ ";" else "") ++ extract_body rest
| (i32_shift_left input1 input2 output::rest) := (if input1 < i32_count ∧ input2 < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=s" ++ to_string input1 ++ "<<" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i32_shift_right input1 input2 output::rest) := (if input1 < i32_count ∧ input2 < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=s" ++ to_string input1 ++ ">>" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i32_to_i64 input output::rest) := (if input < i32_count ∧ output < i64_count then "l" ++ to_string output ++ "=s" ++ to_string input ++ ";" else "") ++ extract_body rest
| (i64_const value output::rest) := (if output < i64_count then "l" ++ to_string output ++ "=" ++ to_string value ++ ";" else "") ++ extract_body rest
| (i64_duplicate input output::rest) := (if input < i64_count ∧ output < i64_count then "l" ++ to_string output ++ "=l" ++ to_string input ++ ";" else "") ++ extract_body rest
| (i64_add input1 input2 output::rest) := (if input1 < i64_count ∧ input2 < i64_count ∧ output < i64_count then "l" ++ to_string output ++ "=l" ++ to_string input1 ++ "+l" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i64_subtract input1 input2 output::rest) := (if input1 < i64_count ∧ input2 < i64_count ∧ output < i64_count then "l" ++ to_string output ++ "=l" ++ to_string input1 ++ "-l" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i64_multiply input1 input2 output::rest) := (if input1 < i64_count ∧ input2 < i64_count ∧ output < i64_count then "l" ++ to_string output ++ "=l" ++ to_string input1 ++ "*l" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i64_unsigned_divide input1 input2 output::rest) := (if input1 < i64_count ∧ input2 < i64_count ∧ output < i64_count then "l" ++ to_string output ++ "=l" ++ to_string input1 ++ "/l" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i64_signed_divide input1 input2 output::rest) := (if input1 < i64_count ∧ input2 < i64_count ∧ output < i64_count then "l" ++ to_string output ++ "=(int64_t)l" ++ to_string input1 ++ "/(int64_t)l" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i64_unsigned_mod input1 input2 output::rest) := (if input1 < i64_count ∧ input2 < i64_count ∧ output < i64_count then "l" ++ to_string output ++ "=l" ++ to_string input1 ++ "%l" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i64_signed_mod input1 input2 output::rest) := (if input1 < i64_count ∧ input2 < i64_count ∧ output < i64_count then "l" ++ to_string output ++ "=(int64_t)l" ++ to_string input1 ++ "%(int64_t)l" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i64_and input1 input2 output::rest) := (if input1 < i64_count ∧ input2 < i64_count ∧ output < i64_count then "l" ++ to_string output ++ "=l" ++ to_string input1 ++ "&l" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i64_or input1 input2 output::rest) := (if input1 < i64_count ∧ input2 < i64_count ∧ output < i64_count then "l" ++ to_string output ++ "=l" ++ to_string input1 ++ "|l" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i64_xor input1 input2 output::rest) := (if input1 < i64_count ∧ input2 < i64_count ∧ output < i64_count then "l" ++ to_string output ++ "=l" ++ to_string input1 ++ "^l" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i64_not input output::rest) := (if input < i64_count ∧ output < i64_count then "l" ++ to_string output ++ "=~l" ++ to_string input ++ ";" else "") ++ extract_body rest
| (i64_shift_left input1 input2 output::rest) := (if input1 < i64_count ∧ input2 < i64_count ∧ output < i64_count then "l" ++ to_string output ++ "=l" ++ to_string input1 ++ "<<l" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i64_shift_right input1 input2 output::rest) := (if input1 < i64_count ∧ input2 < i64_count ∧ output < i64_count then "l" ++ to_string output ++ "=l" ++ to_string input1 ++ ">>l" ++ to_string input2 ++ ";" else "") ++ extract_body rest
| (i64_to_i32 input output::rest) := (if input < i64_count ∧ output < i64_count then "s" ++ to_string output ++ "=l" ++ to_string input ++ ";" else "") ++ extract_body rest
| (i8_unsigned_load address output::rest) := (if address < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=m.x[s" ++ to_string address ++ "];" else "") ++ extract_body rest
| (i8_signed_load address output::rest) := (if address < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=(int8_t)m.x[s" ++ to_string address ++ "];" else "") ++ extract_body rest
| (i8_store address input::rest) := (if address < i32_count ∧ input < i32_count then "m.x[s" ++ to_string address ++ "]=s" ++ to_string input ++ ";" else "") ++ extract_body rest
| (i16_unsigned_load address output::rest) := (if address < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=*(uint16_t*(void*(m.x+s" ++ to_string address ++ ")));" else "") ++ extract_body rest
| (i16_signed_load address output::rest) := (if address < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=*(int16_t*(void*(m.x+s" ++ to_string address ++ ")));" else "") ++ extract_body rest
| (i16_store address input::rest) := (if address < i32_count ∧ input < i32_count then "*(uint16_t*(void*(m.x+s" ++ to_string address ++ ")))=s" ++ to_string input ++ ";" else "") ++ extract_body rest
| (i32_load address output::rest) := (if address < i32_count ∧ output < i32_count then "s" ++ to_string output ++ "=*(uint32_t*(void*(m.x+s" ++ to_string address ++ ")));" else "") ++ extract_body rest
| (i32_store address input::rest) := (if address < i32_count ∧ input < i32_count then "*(uint32_t*(void*(m.x+s" ++ to_string address ++ ")))=s" ++ to_string input ++ ";" else "") ++ extract_body rest
| (i64_load address output::rest) := (if address < i32_count ∧ output < i64_count then "l" ++ to_string output ++ "=*(uint64_t*(void*(m.x+s" ++ to_string address ++ ")));" else "") ++ extract_body rest
| (i64_store address input::rest) := (if address < i32_count ∧ input < i64_count then "*(uint64_t*(void*(m.x+s" ++ to_string address ++ ")))=l" ++ to_string input ++ ";" else "") ++ extract_body rest
| (break::rest) := ("break;") ++ extract_body rest
| (break_if input::rest) := (if input < i32_count then "if(s" ++ to_string input ++ ")break;" else "") ++ extract_body rest
| (loop instructions::rest) := ("while(1){" ++ extract_body instructions ++ "}") ++ extract_body rest
end internal

def extract_cpp_program : program_t → string :=
λ program,
"#include <cstdint>\n" ++
"union {uint8_t x[" ++ to_string program.memory_size ++ "];uint64_t y;} m;" ++
let i32_variables := ((list.range program.i32_count).map (λ i, "s" ++ to_string i ++ "=0,")).foldl (++) "" in
"uint32_t " ++ i32_variables.pop_back ++ ";" ++
let i64_variables := ((list.range program.i64_count).map (λ i, "l" ++ to_string i ++ "=0,")).foldl (++) "" in
"uint64_t " ++ i64_variables.pop_back ++ ";" ++
"int main(){do{" ++ internal.extract_body program.i32_count program.i64_count program.instructions ++ "}while(0);}"

inductive memory_t
| make (linear_memory : list i8_value_t) (i32_variables : list i32_value_t) (i64_variables : list i64_value_t) : memory_t

inductive machine_t
| make (memory : memory_t) (instructions : list with_fictive_instructions_t) : machine_t

inductive reduction_t (state1 : machine_t) (state2 : machine_t)