From cd05bac6c7e5d2af51a986208ab70fb32cd7074f Mon Sep 17 00:00:00 2001
From: utkn <utkns09@gmail.com>
Date: Sat, 28 Dec 2024 20:35:04 +0300
Subject: [PATCH] proofs fixed

---
 Lampe/Lampe.lean                | 23 ++++++++++++-----------
 Lampe/Lampe/Hoare/Builtins.lean | 16 ++++++++--------
 2 files changed, 20 insertions(+), 19 deletions(-)

diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean
index 2124714..6e3fcb5 100644
--- a/Lampe/Lampe.lean
+++ b/Lampe/Lampe.lean
@@ -269,12 +269,18 @@ nr_def call_decl<>(x: Field, y : Field) -> Field {
    STHoare p ⟨[(struct_construct.name, struct_construct.fn)], []⟩
      ⟦⟧ (call_decl.fn.body _ h![] |>.body h![x, y]) (fun v => v = x) := by
   simp only [call_decl, struct_construct]
-  steps <;> tauto
-  . simp_all [exists_const, SLP.true_star]
+  apply STHoare.letIn_intro
+  on_goal 3 => exact (fun (v : Tp.denote p $ .tuple _ [.field, .field]) => v = (x, y, ()))
+  apply STHoare.callDecl_intro <;> tauto
+  . apply STHoare.letIn_intro
+    . steps
+    . intros
+      steps
+      aesop
+  . intros
     steps
-    simp only [exists_const, SLP.true_star]
-    simp_all [SLP.entails, SLP.wand, SLP.star, SLP.lift, SLP.forall']
-  . sorry
+    aesop
+
 
 nr_def simple_tuple<>() -> Field {
   let t = `(1 : Field, true, 3 : Field);
@@ -303,9 +309,4 @@ nr_def simple_array<>() -> Field {
 example : STHoare p Γ ⟦⟧ (simple_array.fn.body _ h![] |>.body h![]) (fun (v : Tp.denote p .field) => v = 2) := by
   simp only [simple_array, Expr.mkArray]
   steps <;> tauto
-  on_goal 3 => exact fun v => v = 2
-  rotate_left
-  steps; aesop
-  simp_all
-  simp only [Expr.readArray]
-  sorry
+  aesop
diff --git a/Lampe/Lampe/Hoare/Builtins.lean b/Lampe/Lampe/Hoare/Builtins.lean
index 0f7ecf2..cde31bf 100644
--- a/Lampe/Lampe/Hoare/Builtins.lean
+++ b/Lampe/Lampe/Hoare/Builtins.lean
@@ -131,20 +131,20 @@ theorem mkArray_intro {n} {argTps : List Tp} {args : HList (Tp.denote p) argTps}
   apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
-theorem arrayIndex_intro : STHoarePureBuiltin p Γ Builtin.arrayIndex (by tauto) h![arr, i] := by
-  apply pureBuiltin_intro_consequence <;> try rfl
+theorem arrayIndex_intro : STHoarePureBuiltin p Γ Builtin.arrayIndex (by tauto) h![arr, i] (a := (tp, n)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
-theorem arrayLen_intro : STHoarePureBuiltin p Γ Builtin.arrayLen (by tauto) h![arr] := by
-  apply pureBuiltin_intro_consequence <;> try rfl
+theorem arrayLen_intro : STHoarePureBuiltin p Γ Builtin.arrayLen (by tauto) h![arr] (a := (tp, n)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
-theorem arrayAsSlice_intro : STHoarePureBuiltin p Γ Builtin.arrayAsSlice (by tauto) h![arr] := by
-  apply pureBuiltin_intro_consequence <;> try rfl
+theorem arrayAsSlice_intro : STHoarePureBuiltin p Γ Builtin.arrayAsSlice (by tauto) h![arr] (a := (tp, n)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
-theorem replaceArray_intro : STHoarePureBuiltin p Γ Builtin.replaceArray (by tauto) h![arr, idx, v] := by
-  apply pureBuiltin_intro_consequence <;> try rfl
+theorem replaceArray_intro : STHoarePureBuiltin p Γ Builtin.replaceArray (by tauto) h![arr, idx, v] (a := (tp, n)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
 -- BigInt