Why3: имитация серверной части компилятора

Question

Для школьного проекта мне нужно написать бэкэнд небольшого компилятора, который переводит арифметические выражения в инструкции стековой машины. Наша отправная точка - это синтаксическое дерево выражения, а не его текстовое представление (как вы можете видеть на изображении 1).

Первая часть проекта состоит в написании того, что нужно для вычисления арифметических выражений с переменными. Для этого нам нужно работать с понятием состояния, которое представляет фактические значения переменных.

Для упрощения предполагается, что состояние определено для всех переменных, даже если в выражении упоминаются только некоторые из них. Поскольку каждая переменная будет иметь связанный номер, можно представить состояние как отображение строки в int, используя 0 в качестве стандарта.

Также было бы полезно иметь представление состояния (где все переменные отображаются в 0) и функцию для состояния с заданным состоянием s, переменной y и числом n, которое возвращает состояние где y связан с n, а другие переменные связаны со значением, которое они уже имели в s.

Для второй части у нас есть следующий список инструкций:

      SPush n: puts n on top of the stack.
SLoad x: "puts" the value associated to the state for variable x on top of the stack.
SSym: takes the number on top and puts its symmetric on top instead.
SPlus: takes the two top numbers, add them and puts the result on top instead.
SMinus: similar, but for minus.
SMult: similar, but for times.

И мы должны написать функцию для оценки программ на языке стековых машин. Функция получает состояние s, стек st (который представляет собой список чисел) и программу pg (которая представляет собой список инструкций) и возвращает стек после выполнения программы.

Для третьей и последней части мы должны написать функцию для компиляции арифметического выражения в программу стекового автомата. Выполнение такой программы должно быть таким же, как помещает значение выражения на вершину стека.

Пока у меня есть следующий код:

      theory Test

use map.Map
use map.Const

use int.Int 
use List.Append

type stack = list int

type instr =
    | SPush int
    | SLoad string
    | SSim int
    | SPlus int int
    | SMinus int int
    | SMult int int
    
type prog = list instr

type state = map string int

type operator = Oplus | Ominus | Omult

type aexp =
    | Econst int
    | Esym int
    | Evar string
    | Ebin aexp operator aexp
    
function aeval_op (x : int) (op : operator) (y : int) : int =
    match op with
    | Oplus -> x + y
    | Ominus -> x - y
    | Omult -> x * y
    end
   
function aeval (s : state) (e : aexp) : int =
    match e with
    | (Econst x) -> x
    | (Esym x) -> -x
    | (Evar x) -> (get s x)
    | (Ebin x op y) -> aeval_op (aeval s x) op (aeval s y)
    end
   
goal Test42 :
    let s = const 0 in
    aeval s (Econst 42) = 42
    
goal Test10sym :
    let s = const 0 in
    aeval s (Esym 10) = -10
    
goal TestVar13 :
    let s = set (const 0) "x" 13 in
    aeval s (Evar "x") = 13
    
goal TestPlus :
    let s = set (const 0) "x" 13 in
    aeval s (Ebin (Evar "x") Oplus (Econst 13)) = 26
    
goal TestMinus :
    let s = const 0 in
    aeval s (Ebin (Econst 13) Ominus (Econst 13)) = 0
    
goal TestMult :
    let s = const 0 in
    aeval s (Ebin (Econst 13) Omult (Econst 13)) = 169

inductive aevalR state aexp state int =
    | econst : forall n : int, s : state.
                aevalR s (Econst n) s n
    | esym : forall n : int, s : state.
                aevalR s (Esym n) s (-n)
    | evar : forall x : string, s : state.
                aevalR s (Evar x) s (get s x)
    | ebin : forall e1 e2 : aexp, op : operator, n1 n2 : int, s s1 s2 : state.
                (aevalR s e1 s1 n1) ->
                (aevalR s1 e2 s2 n2) ->
                (aevalR s (Ebin e1 op e2) s2 (aeval_op n1 op n2))
               
goal Test42r :
    let s = const 0 in
    aevalR s (Econst 42) s 42

goal Test10symr :
    let s = const 0 in
    aevalR s (Esym 10) s (-10)
    
goal TestVar10r :
    let s = set (const 0) "x" 10 in
    aevalR s (Evar "x") s 10
    
lemma TestVar10r_Plus :
    let s = set (const 0) "x" 10 in (* para ficar com o mesmo estado *)
    aevalR s (Evar "x") s 10

lemma Test13r_Plus :
    let s = set (const 0) "x" 10 in (* para ficar com o mesmo estado *)
    aevalR s (Econst 13) s 13

goal TestPlusr :
    let s = set (const 0) "x" 10 in
    aevalR s (Ebin (Evar "x") Oplus (Econst 13)) s 23
   
goal TestMinusr :
    let s = set (const 0) "x" 10 in
    aevalR s (Ebin (Econst 13) Ominus (Econst 13)) s 0
    
goal TestMultr :
    let s = set (const 0) "x" 10 in
    aevalR s (Ebin (Econst 13) Omult (Econst 13)) s 169

lemma aux_no_side_effects: forall s0 s1 : state, e : aexp, x : int. aevalR s0 e s1 x -> s0 = s1
  
lemma agree_func_rel0: forall a : aexp, s: state, n : int. (aevalR s a s n) -> (aeval s a = n)
lemma agree_func_rel1: forall a : aexp, s: state, n : int. (aeval s a = n) -> (aevalR s a s n)

function execute (s : state) (st : stack) (pg : prog) : stack =
    Nil
    
function executeInst (s : state) (i : instr) (st : stack) : stack =
  match i with
    | SPush n -> s (Cons n st)
    | SLoad str -> ((get s str):st)
    | SSim n -> s (-n:st)
    | SPlus n1 n2 -> s (n1+n2:st)
    | SMinus n1 n2 -> s (n1-n2:st)
    | SMult n1 n2 -> s (n1*n2:st)
  end

function compile (a : aexp) : prog :=
  match a with
    | Econst n -> (SPush n:nil)
    | Esym n -> (SSim n:nil)
    | Evar x -> (SLoad x:nil)
    | Ebin e1 op e2 -> compile e2 ++ compile e1 ++ ((aeval_op e1 op e2):nil)
  end.

Итак, у меня есть три вопроса:

1 - Как мне сделать а также ?

2 - Как исправить ? Я пытался сделать и функцию aux только для инструкции, но я не совсем уверен, как заставить ее работать.

3 - Как исправить ? Я не думаю, что представляю его поведение так, как его просили.

Я знаю, что вопрос немного сложен, но если что-то слишком непонятно, скажите мне. Спасибо!