Various small enhancements

Lampe/Lampe.lean

@@ -299,6 +299,29 @@ example : STHoare p Γ ⟦⟧ (simple_array.fn.body _ h![] |>.body h![])
   steps <;> try tauto
   aesop
 
+nr_def simple_rep_array<>() -> [Field; 4] {
+  let arr = [1 : Field ; 4];
+  arr
+}
+
+example : STHoare p Γ ⟦⟧ (simple_rep_array.fn.body _ h![] |>.body h![])
+    fun (v : Tp.denote p $ .array _ _) => v.toList = [1, 1, 1, 1] := by
+  simp only [simple_rep_array, Expr.mkArray]
+  steps <;> try tauto
+  aesop
+
+nr_def simple_rep_slice<>() -> [Field] {
+  let arr = &[1 : Field ; 4];
+  arr
+}
+
+example : STHoare p Γ ⟦⟧ (simple_rep_slice.fn.body _ h![] |>.body h![])
+    fun (v : Tp.denote p $ .slice _) => v = [1, 1, 1, 1] := by
+  simp only [simple_rep_slice, Expr.mkArray]
+  steps <;> try tauto
+  aesop
+
+
 nr_def tuple_lens<>() -> Field {
   let mut p = `(`(1 : Field, 2 : Field), 3 : Field);
   p .0 .1 = 3 : Field;
@@ -364,6 +387,21 @@ nr_def simple_func<>() -> Field {
   10 : Field
 }
 
+nr_def deref_lens<>() -> Field {
+  let r = #ref(`(5 : Field)) : &`(Field);
+  *(r).0 = 3 : Field;
+  *(r).0
+}
+
+example : STHoare p Γ ⟦⟧ (deref_lens.fn.body _ h![] |>.body h![])
+    fun (v : Tp.denote p .field) => v = 3 := by
+  simp only [deref_lens]
+  steps
+  subst_vars
+  simp_all only [exists_const, Lens.modify, Lens.get]
+  subst_vars
+  simp_all [Builtin.indexTpl]
+
 nr_def call<>(f : λ() → Field) -> Field {
   f()
 }

Lampe/Lampe/Builtin/Lens.lean

@@ -10,39 +10,6 @@ lemma Finmap.insert_mem_disjoint [DecidableEq α] {m₁ m₂ : Finmap fun _ : α
 
 namespace Lampe.Builtin
 
-inductive readLensOmni (lens : Lens rep tp₁ tp₂) : Omni where
- | ok {st Q ref} {s : Tp.denote p tp₁} {hr : rep = Tp.denote p} :
-   st.lookup ref = some ⟨tp₁, hr ▸ s⟩ →
-   (some v = Lens.get (hr ▸ lens) s) →
-   Q (some (st, v)) →
-   (readLensOmni lens) p st [tp₁.ref] tp₂ h![ref] Q
-| err {st Q ref} {s : Tp.denote p tp₁} {hr : rep = Tp.denote p} :
-   st.lookup ref = some ⟨tp₁, hr ▸ s⟩ →
-   (none = Lens.get (hr ▸ lens) s) →
-   Q none →
-   (readLensOmni lens) p st [tp₁.ref] tp₂ h![ref] Q
-
- def readLens (lens : Lens rep tp₁ tp₂) : Builtin := {
-   omni := readLensOmni lens
-   conseq := by
-    unfold omni_conseq
-    intros
-    cases_type readLensOmni
-    constructor <;> tauto
-    apply readLensOmni.err <;> tauto
-   frame := by
-    unfold omni_frame
-    intros
-    cases_type readLensOmni
-    . constructor <;> try tauto
-      rw [Finmap.lookup_union_left] <;> try tauto
-      apply Finmap.mem_of_lookup_eq_some <;> tauto
-      repeat apply Exists.intro <;> tauto
-    . apply readLensOmni.err <;> try tauto
-      rw [Finmap.lookup_union_left] <;> try tauto
-      apply Finmap.mem_of_lookup_eq_some <;> tauto
- }
-
  inductive modifyLensOmni (lens : Lens rep tp₁ tp₂) : Omni where
  | ok {p st Q ref} {s s' : Tp.denote p tp₁} {v' : Tp.denote p tp₂} {hr : rep = Tp.denote p} :
    st.lookup ref = some ⟨tp₁, s⟩ →

Lampe/Lampe/Hoare/Builtins.lean

@@ -468,26 +468,6 @@ theorem projectTuple_intro : STHoarePureBuiltin p Γ (Builtin.projectTuple mem)
 
 -- Lens
 
-theorem readLens_intro {lens : Lens (Tp.denote p) tp₁ tp₂} :
-    STHoare p Γ
-    [r ↦ ⟨tp₁, s⟩]
-    (.callBuiltin [tp₁.ref] tp₂ (.readLens lens) h![r])
-    (fun v' => ⟦lens.get s = some v'⟧ ⋆ [r ↦ ⟨tp₁, s⟩]) := by
-  unfold STHoare THoare
-  intros H st h
-  constructor
-  cases hl : (lens.get s)
-  . apply Builtin.readLensOmni.err <;> try tauto
-    unfold SLP.star State.valSingleton at *
-    aesop
-  . apply Builtin.readLensOmni.ok <;> try tauto
-    . unfold SLP.star State.valSingleton at *
-      aesop
-    . unfold mapToValHeapCondition
-      simp_all only [Option.map_some', SLP.true_star, SLP.star_assoc]
-      apply SLP.ent_star_top at h
-      simp_all
-
  theorem modifyLens_intro {lens : Lens (Tp.denote p) tp₁ tp₂} {s : Tp.denote p tp₁} {v : Tp.denote p tp₂} :
     STHoare p Γ
     [r ↦ ⟨tp₁, s⟩]

Lampe/Lampe/Lens.lean

@@ -5,6 +5,9 @@ import Lampe.Builtin.Slice
 
 namespace Lampe
 
+/--
+Instructs how to access a inner value from another value, e.g., a particular value of a slice.
+-/
 inductive Access (rep : Tp → Type _) : Tp → Tp → Type _
 | tuple : (mem : Builtin.Member tp tps) → Access rep (.tuple name tps) tp
 | array : (idx : rep $ .u 32) → Access rep (.array tp n) tp
@@ -39,6 +42,9 @@ theorem Access.modify_get {acc : Access (Tp.denote p) tp₁ tp₂} {h : acc.modi
       apply Builtin.index_replaced_slice
     . aesop
 
+/--
+Represents a lens between two `Tp`s, which is a concetanation of several `Access` operations.
+-/
 inductive Lens (rep : Tp → Type _) : Tp → Tp → Type _
 | nil : Lens rep tp tp
 | cons : Lens rep tp₁ tp₂ → Access rep tp₂ tp₃ → Lens rep tp₁ tp₃

Lampe/Lampe/Semantics.lean

@@ -36,8 +36,8 @@ inductive Omni : Env → State p → Expr (Tp.denote p) tp → (Option (State p
 | litField {Q} : Q (some (st, n)) → Omni Γ st (.lit .field n) Q
 | litFalse {Q} : Q (some (st, false)) → Omni Γ st (.lit .bool 0) Q
 | litTrue {Q} : Q (some (st, true)) → Omni Γ st (.lit .bool 1) Q
-| litRef {Q} : Q (some (st, ⟨r⟩)) → Omni Γ st (.lit (.ref tp) r) Q
 | litU {Q} : Q (some (st, ↑n)) → Omni Γ st (.lit (.u s) n) Q
+| litUnit {Q} : Q (some (st, ())) → Omni Γ st (.lit .unit n) Q
 | fn {Q} : Q (some (st, r)) → Omni Γ st (.fn _ _ r) Q
 | var {Q} : Q (some (st, v)) → Omni Γ st (.var v) Q
 | skip {Q} : Q (some (st, ())) → Omni Γ st (.skip) Q
@@ -128,7 +128,7 @@ theorem Omni.frame {p Γ tp} {st₁ st₂ : State p} {e : Expr (Tp.denote p) tp}
   | litFalse hq
   | litTrue hq
   | litU hq
-  | litRef hq
+  | litUnit
   | skip hq
   | fn
   | var hq =>