bump lean version

prover/server/formal-verification/FormalVerification/Circuit.lean

@@ -16,7 +16,7 @@ def sbox (Inp: F) (k: F -> Prop): Prop :=
     ∃gate_2, gate_2 = Gates.mul Inp gate_1 ∧
     k gate_2
 
-def mds_3 (Inp: Vector F 3) (k: Vector F 3 -> Prop): Prop :=
+def mds_3 (Inp: List.Vector F 3) (k: List.Vector F 3 -> Prop): Prop :=
     ∃gate_0, gate_0 = Gates.mul Inp[0] (7511745149465107256748700652201246547602992235352608707588321460060273774987:F) ∧
     ∃gate_1, gate_1 = Gates.add (0:F) gate_0 ∧
     ∃gate_2, gate_2 = Gates.mul Inp[1] (10370080108974718697676803824769673834027675643658433702224577712625900127200:F) ∧
@@ -37,7 +37,7 @@ def mds_3 (Inp: Vector F 3) (k: Vector F 3 -> Prop): Prop :=
     ∃gate_17, gate_17 = Gates.add gate_15 gate_16 ∧
     k vec![gate_5, gate_11, gate_17]
 
-def fullRound_3_3 (Inp: Vector F 3) (Consts: Vector F 3) (k: Vector F 3 -> Prop): Prop :=
+def fullRound_3_3 (Inp: List.Vector F 3) (Consts: List.Vector F 3) (k: List.Vector F 3 -> Prop): Prop :=
     ∃gate_0, gate_0 = Gates.add Inp[0] Consts[0] ∧
     ∃gate_1, gate_1 = Gates.add Inp[1] Consts[1] ∧
     ∃gate_2, gate_2 = Gates.add Inp[2] Consts[2] ∧
@@ -47,15 +47,15 @@ def fullRound_3_3 (Inp: Vector F 3) (Consts: Vector F 3) (k: Vector F 3 -> Prop)
     mds_3 vec![gate_3, gate_4, gate_5] fun gate_6 =>
     k gate_6
 
-def halfRound_3_3 (Inp: Vector F 3) (Consts: Vector F 3) (k: Vector F 3 -> Prop): Prop :=
+def halfRound_3_3 (Inp: List.Vector F 3) (Consts: List.Vector F 3) (k: List.Vector F 3 -> Prop): Prop :=
     ∃gate_0, gate_0 = Gates.add Inp[0] Consts[0] ∧
     ∃gate_1, gate_1 = Gates.add Inp[1] Consts[1] ∧
     ∃gate_2, gate_2 = Gates.add Inp[2] Consts[2] ∧
     sbox gate_0 fun gate_3 =>
     mds_3 vec![gate_3, gate_1, gate_2] fun gate_4 =>
     k gate_4
 
-def poseidon_3 (Inputs: Vector F 3) (k: Vector F 3 -> Prop): Prop :=
+def poseidon_3 (Inputs: List.Vector F 3) (k: List.Vector F 3 -> Prop): Prop :=
     fullRound_3_3 Inputs vec![(6745197990210204598374042828761989596302876299545964402857411729872131034734:F), (426281677759936592021316809065178817848084678679510574715894138690250139748:F), (4014188762916583598888942667424965430287497824629657219807941460227372577781:F)] fun gate_0 =>
     fullRound_3_3 gate_0 vec![(21328925083209914769191926116470334003273872494252651254811226518870906634704:F), (19525217621804205041825319248827370085205895195618474548469181956339322154226:F), (1402547928439424661186498190603111095981986484908825517071607587179649375482:F)] fun gate_1 =>
     fullRound_3_3 gate_1 vec![(18320863691943690091503704046057443633081959680694199244583676572077409194605:F), (17709820605501892134371743295301255810542620360751268064484461849423726103416:F), (15970119011175710804034336110979394557344217932580634635707518729185096681010:F)] fun gate_2 =>
@@ -134,7 +134,7 @@ def ProveParentHash (Bit: F) (Hash: F) (Sibling: F) (k: F -> Prop): Prop :=
     Poseidon2 gate_1 gate_2 fun gate_3 =>
     k gate_3
 
-def MerkleRootGadget_26_26 (Hash: F) (Index: F) (Path: Vector F 26) (k: F -> Prop): Prop :=
+def MerkleRootGadget_26_26 (Hash: F) (Index: F) (Path: List.Vector F 26) (k: F -> Prop): Prop :=
     ∃gate_0, Gates.to_binary Index 26 gate_0 ∧
     ProveParentHash gate_0[0] Hash Path[0] fun gate_1 =>
     ProveParentHash gate_0[1] gate_1 Path[1] fun gate_2 =>
@@ -164,7 +164,7 @@ def MerkleRootGadget_26_26 (Hash: F) (Index: F) (Path: Vector F 26) (k: F -> Pro
     ProveParentHash gate_0[25] gate_25 Path[25] fun gate_26 =>
     k gate_26
 
-def InclusionProof_8_8_8_26_8_8_26 (Roots: Vector F 8) (Leaves: Vector F 8) (InPathIndices: Vector F 8) (InPathElements: Vector (Vector F 26) 8) (k: Vector F 8 -> Prop): Prop :=
+def InclusionProof_8_8_8_26_8_8_26 (Roots: List.Vector F 8) (Leaves: List.Vector F 8) (InPathIndices: List.Vector F 8) (InPathElements: List.Vector (List.Vector F 26) 8) (k: List.Vector F 8 -> Prop): Prop :=
     MerkleRootGadget_26_26 Leaves[0] InPathIndices[0] InPathElements[0] fun gate_0 =>
     Gates.eq gate_0 Roots[0] ∧
     MerkleRootGadget_26_26 Leaves[1] InPathIndices[1] InPathElements[1] fun gate_2 =>
@@ -189,7 +189,7 @@ def AssertIsLess_248 (A: F) (B: F) : Prop :=
     ∃_ignored_, Gates.to_binary gate_1 248 _ignored_ ∧
     True
 
-def mds_4 (Inp: Vector F 4) (k: Vector F 4 -> Prop): Prop :=
+def mds_4 (Inp: List.Vector F 4) (k: List.Vector F 4 -> Prop): Prop :=
     ∃gate_0, gate_0 = Gates.mul Inp[0] (16023668707004248971294664614290028914393192768609916554276071736843535714477:F) ∧
     ∃gate_1, gate_1 = Gates.add (0:F) gate_0 ∧
     ∃gate_2, gate_2 = Gates.mul Inp[1] (17849615858846139011678879517964683507928512741474025695659909954675835121177:F) ∧
@@ -224,7 +224,7 @@ def mds_4 (Inp: Vector F 4) (k: Vector F 4 -> Prop): Prop :=
     ∃gate_31, gate_31 = Gates.add gate_29 gate_30 ∧
     k vec![gate_7, gate_15, gate_23, gate_31]
 
-def fullRound_4_4 (Inp: Vector F 4) (Consts: Vector F 4) (k: Vector F 4 -> Prop): Prop :=
+def fullRound_4_4 (Inp: List.Vector F 4) (Consts: List.Vector F 4) (k: List.Vector F 4 -> Prop): Prop :=
     ∃gate_0, gate_0 = Gates.add Inp[0] Consts[0] ∧
     ∃gate_1, gate_1 = Gates.add Inp[1] Consts[1] ∧
     ∃gate_2, gate_2 = Gates.add Inp[2] Consts[2] ∧
@@ -236,7 +236,7 @@ def fullRound_4_4 (Inp: Vector F 4) (Consts: Vector F 4) (k: Vector F 4 -> Prop)
     mds_4 vec![gate_4, gate_5, gate_6, gate_7] fun gate_8 =>
     k gate_8
 
-def halfRound_4_4 (Inp: Vector F 4) (Consts: Vector F 4) (k: Vector F 4 -> Prop): Prop :=
+def halfRound_4_4 (Inp: List.Vector F 4) (Consts: List.Vector F 4) (k: List.Vector F 4 -> Prop): Prop :=
     ∃gate_0, gate_0 = Gates.add Inp[0] Consts[0] ∧
     ∃gate_1, gate_1 = Gates.add Inp[1] Consts[1] ∧
     ∃gate_2, gate_2 = Gates.add Inp[2] Consts[2] ∧
@@ -245,7 +245,7 @@ def halfRound_4_4 (Inp: Vector F 4) (Consts: Vector F 4) (k: Vector F 4 -> Prop)
     mds_4 vec![gate_4, gate_1, gate_2, gate_3] fun gate_5 =>
     k gate_5
 
-def poseidon_4 (Inputs: Vector F 4) (k: Vector F 4 -> Prop): Prop :=
+def poseidon_4 (Inputs: List.Vector F 4) (k: List.Vector F 4 -> Prop): Prop :=
     fullRound_4_4 Inputs vec![(11633431549750490989983886834189948010834808234699737327785600195936805266405:F), (17353750182810071758476407404624088842693631054828301270920107619055744005334:F), (11575173631114898451293296430061690731976535592475236587664058405912382527658:F), (9724643380371653925020965751082872123058642683375812487991079305063678725624:F)] fun gate_0 =>
     fullRound_4_4 gate_0 vec![(20936725237749945635418633443468987188819556232926135747685274666391889856770:F), (6427758822462294912934022562310355233516927282963039741999349770315205779230:F), (16782979953202249973699352594809882974187694538612412531558950864304931387798:F), (8979171037234948998646722737761679613767384188475887657669871981433930833742:F)] fun gate_1 =>
     fullRound_4_4 gate_1 vec![(5428827536651017352121626533783677797977876323745420084354839999137145767736:F), (507241738797493565802569310165979445570507129759637903167193063764556368390:F), (6711578168107599474498163409443059675558516582274824463959700553865920673097:F), (2197359304646916921018958991647650011119043556688567376178243393652789311643:F)] fun gate_2 =>
@@ -322,7 +322,7 @@ def LeafHashGadget (LeafLowerRangeValue: F) (NextIndex: F) (LeafHigherRangeValue
     Poseidon3 LeafLowerRangeValue NextIndex LeafHigherRangeValue fun gate_2 =>
     k gate_2
 
-def NonInclusionProof_8_8_8_8_8_8_26_8_8_26 (Roots: Vector F 8) (Values: Vector F 8) (LeafLowerRangeValues: Vector F 8) (LeafHigherRangeValues: Vector F 8) (NextIndices: Vector F 8) (InPathIndices: Vector F 8) (InPathElements: Vector (Vector F 26) 8) (k: Vector F 8 -> Prop): Prop :=
+def NonInclusionProof_8_8_8_8_8_8_26_8_8_26 (Roots: List.Vector F 8) (Values: List.Vector F 8) (LeafLowerRangeValues: List.Vector F 8) (LeafHigherRangeValues: List.Vector F 8) (NextIndices: List.Vector F 8) (InPathIndices: List.Vector F 8) (InPathElements: List.Vector (List.Vector F 26) 8) (k: List.Vector F 8 -> Prop): Prop :=
     LeafHashGadget LeafLowerRangeValues[0] NextIndices[0] LeafHigherRangeValues[0] Values[0] fun gate_0 =>
     MerkleRootGadget_26_26 gate_0 InPathIndices[0] InPathElements[0] fun gate_1 =>
     Gates.eq gate_1 Roots[0] ∧
@@ -349,17 +349,17 @@ def NonInclusionProof_8_8_8_8_8_8_26_8_8_26 (Roots: Vector F 8) (Values: Vector
     Gates.eq gate_22 Roots[7] ∧
     k vec![gate_1, gate_4, gate_7, gate_10, gate_13, gate_16, gate_19, gate_22]
 
-def InclusionCircuit_8_8_8_26_8_8_26 (Roots: Vector F 8) (Leaves: Vector F 8) (InPathIndices: Vector F 8) (InPathElements: Vector (Vector F 26) 8): Prop :=
+def InclusionCircuit_8_8_8_26_8_8_26 (Roots: List.Vector F 8) (Leaves: List.Vector F 8) (InPathIndices: List.Vector F 8) (InPathElements: List.Vector (List.Vector F 26) 8): Prop :=
     InclusionProof_8_8_8_26_8_8_26 Roots Leaves InPathIndices InPathElements fun _ =>
     True
 
-def NonInclusionCircuit_8_8_8_8_8_8_26_8_8_26 (Roots: Vector F 8) (Values: Vector F 8) (LeafLowerRangeValues: Vector F 8) (LeafHigherRangeValues: Vector F 8) (NextIndices: Vector F 8) (InPathIndices: Vector F 8) (InPathElements: Vector (Vector F 26) 8): Prop :=
+def NonInclusionCircuit_8_8_8_8_8_8_26_8_8_26 (Roots: List.Vector F 8) (Values: List.Vector F 8) (LeafLowerRangeValues: List.Vector F 8) (LeafHigherRangeValues: List.Vector F 8) (NextIndices: List.Vector F 8) (InPathIndices: List.Vector F 8) (InPathElements: List.Vector (List.Vector F 26) 8): Prop :=
     NonInclusionProof_8_8_8_8_8_8_26_8_8_26 Roots Values LeafLowerRangeValues LeafHigherRangeValues NextIndices InPathIndices InPathElements fun _ =>
     True
 
-def CombinedCircuit_8_8_8_26_8_8_8_8_8_8_8_26_8 (Inclusion_Roots: Vector F 8) (Inclusion_Leaves: Vector F 8) (Inclusion_InPathIndices: Vector F 8) (Inclusion_InPathElements: Vector (Vector F 26) 8) (NonInclusion_Roots: Vector F 8) (NonInclusion_Values: Vector F 8) (NonInclusion_LeafLowerRangeValues: Vector F 8) (NonInclusion_LeafHigherRangeValues: Vector F 8) (NonInclusion_NextIndices: Vector F 8) (NonInclusion_InPathIndices: Vector F 8) (NonInclusion_InPathElements: Vector (Vector F 26) 8): Prop :=
+def CombinedCircuit_8_8_8_26_8_8_8_8_8_8_8_26_8 (Inclusion_Roots: List.Vector F 8) (Inclusion_Leaves: List.Vector F 8) (Inclusion_InPathIndices: List.Vector F 8) (Inclusion_InPathElements: List.Vector (List.Vector F 26) 8) (NonInclusion_Roots: List.Vector F 8) (NonInclusion_Values: List.Vector F 8) (NonInclusion_LeafLowerRangeValues: List.Vector F 8) (NonInclusion_LeafHigherRangeValues: List.Vector F 8) (NonInclusion_NextIndices: List.Vector F 8) (NonInclusion_InPathIndices: List.Vector F 8) (NonInclusion_InPathElements: List.Vector (List.Vector F 26) 8): Prop :=
     InclusionProof_8_8_8_26_8_8_26 Inclusion_Roots Inclusion_Leaves Inclusion_InPathIndices Inclusion_InPathElements fun _ =>
     NonInclusionProof_8_8_8_8_8_8_26_8_8_26 NonInclusion_Roots NonInclusion_Values NonInclusion_LeafLowerRangeValues NonInclusion_LeafHigherRangeValues NonInclusion_NextIndices NonInclusion_InPathIndices NonInclusion_InPathElements fun _ =>
     True
 
-end LightProver
+end LightProver

prover/server/formal-verification/FormalVerification/Lemmas.lean

@@ -1,5 +1,5 @@
 import Mathlib
-import «ProvenZk»
+import ProvenZk
 import FormalVerification.Circuit
 
 open LightProver (F Order)
@@ -8,38 +8,38 @@ axiom bn254_Fr_prime : Nat.Prime Order
 instance : Fact (Nat.Prime Order) := Fact.mk bn254_Fr_prime
 
 instance : Membership α (MerkleTree α H d) where
-  mem x t := ∃i, t.itemAtFin i = x
+  mem t x := ∃i, t.itemAtFin i = x
 
 namespace ZMod
 
-lemma castInt_lt [NeZero N] {n : ZMod N}: (n:ℤ) < N := by
+lemma castInt_lt [NeZero N] {n : ZMod N}: (n.cast:ℤ) < N := by
   rw [cast_eq_val, Nat.cast_lt]
   apply ZMod.val_lt
 
-lemma castInt_nonneg [NeZero N] {n : ZMod N}: (0:ℤ) ≤ n := by
+lemma castInt_nonneg [NeZero N] {n : ZMod N}: (0:ℤ) ≤ n.cast := by
   rw [cast_eq_val]
   apply Int.ofNat_nonneg
 
-lemma castInt_neg [NeZero N] {n : ZMod N}: (((-n): ZMod N) : ℤ) = -(n:ℤ) % N := by
+lemma castInt_neg [NeZero N] {n : ZMod N}: ((-n).cast : ℤ) = -(n.cast:ℤ) % N := by
   rw [cast_eq_val, neg_val]
   split
   . simp [*]
   . rw [Nat.cast_sub]
     . rw [←Int.add_emod_self_left, Int.emod_eq_of_lt]
       . simp; rfl
-      . linarith [castInt_lt (N:=N)]
+      . linarith [castInt_lt (N:=N) (n:=n)]
       . simp_arith
         rw [ZMod.cast_eq_val, ←Int.ofNat_zero, Int.ofNat_lt]
         apply Nat.zero_lt_of_ne_zero
         simp [*]
     . exact Nat.le_of_lt (ZMod.val_lt _)
 
 
-lemma castInt_add [NeZero N] {n m : ZMod N}: (((n + m): ZMod N) : ℤ) = ((n:ℤ) + (m:ℤ)) % N := by
+lemma castInt_add [NeZero N] {n m : ZMod N}: ((n + m).cast : ℤ) = ((n.cast:ℤ) + (m.cast:ℤ)) % N := by
   rw [ZMod.cast_eq_val, val_add]
   simp
 
-lemma castInt_sub [NeZero N] {n m : ZMod N}: (((n - m): ZMod N) : ℤ) = ((n:ℤ) - (m:ℤ)) % N := by
+lemma castInt_sub [NeZero N] {n m : ZMod N}: ((n - m).cast : ℤ) = ((n.cast:ℤ) - (m.cast:ℤ)) % N := by
   rw [sub_eq_add_neg, castInt_add, castInt_neg]
   simp
   rfl
@@ -64,8 +64,8 @@ theorem negSucc_le_negSucc (m n : Nat) : negSucc m ≤ negSucc n ↔ n ≤ m :=
     . rename_i hpc
       linarith [Nat.lt_of_sub_eq_succ hpc]
 
-theorem emod_negSucc (m : Nat) (n : Int) :
-  negSucc m % n = subNatNat (natAbs n) (Nat.succ (m % natAbs n)) := rfl
+-- theorem emod_negSucc (m : Nat) (n : Int) :
+  -- negSucc m % n = subNatNat (natAbs n) (Nat.succ (m % natAbs n)) := rfl
 
 theorem emod_eq_add_self_of_neg_and_lt_neg_self {a : ℤ} {mod : ℤ}: a < 0 → a ≥ -mod → a % mod = a + mod := by
   intro hlt hge
@@ -76,53 +76,125 @@ theorem emod_eq_add_self_of_neg_and_lt_neg_self {a : ℤ} {mod : ℤ}: a < 0 →
 
 end Int
 
-lemma Membership.get_elem_helper {i n : ℕ} {r : Std.Range} (h₁ : i ∈ r) (h₂ : r.stop = n) :
-    i < n := h₂ ▸ h₁.2
-
 macro_rules
 | `(tactic| get_elem_tactic_trivial) => `(tactic| (exact Membership.get_elem_helper (by assumption) (by rfl)))
 
-def Std.Range.toList (r : Std.Range): List Nat := go r.start (r.stop - r.start)  where
-  go start
+def Std.Range.toList (r : Std.Range): List Nat := go r.step r.step_pos r.start (r.stop - r.start) where
+  step_pos := r.step_pos
+  go step step_pos start
   | 0 => []
-  | i + 1 => start :: go (start + 1) i
+  | i + 1 => start :: go step step_pos (start + step) (i + 1 - step)
+    termination_by fuel => fuel
+    decreasing_by
+      simpa
 
 theorem Std.Range.mem_toList_of_mem {r : Std.Range} (hp : i ∈ r) : i ∈ r.toList := by
-  rcases hp with ⟨h₁, h₂⟩
-  rcases r with ⟨start, stop, _⟩
+  rcases r with ⟨start, stop, step, step_pos⟩
+  rcases hp with ⟨h₁, h₂, h₃⟩
   simp at h₁ h₂
-  have h₃ : ∃d, stop = start + d := by
-    exists stop - start
-    apply Eq.symm
-    apply Nat.add_sub_cancel'
-    apply Nat.le_trans h₁ (Nat.le_of_lt h₂)
-  rcases h₃ with ⟨d, ⟨_⟩⟩
-  induction d generalizing start i with
-  | zero => linarith
+  have h₃ : ∃d d', stop = start + d * step + d' ∧ d' < step := by
+    exists (stop - start) / step
+    exists (stop - start) % step
+    apply And.intro
+    · have : start < stop := Nat.lt_of_le_of_lt h₁ h₂
+      zify [this]
+      rw [Int.add_assoc, Int.ediv_add_emod']
+      simp
+    · apply Nat.mod_lt; simpa
+  rcases h₃ with ⟨d, d', ⟨_⟩, _⟩
+  induction d generalizing start i d' with
+  | zero =>
+    simp at h₂
+    simp at h₃
+    have : i ≤ start := by
+      rw [Nat.mod_eq_of_lt] at h₃
+      · apply Nat.le_of_sub_eq_zero
+        assumption
+      · apply Nat.lt_trans (m := d')
+        · apply Nat.sub_lt_left_of_lt_add <;> assumption
+        · assumption
+    have : i = start := by
+      apply Nat.le_antisymm <;> assumption
+    cases this
+    unfold toList toList.go
+    simp
+    split
+    · linarith
+    · simp
   | succ d ih =>
     simp [toList, toList.go]
+    unfold toList.go
+    have : start + (d + 1) * step + d' - start ≠ 0 := by
+      rw [Nat.add_comm, ←Nat.add_assoc, Nat.add_comm, ←Nat.add_assoc]
+      simp
+      rintro rfl
+      contradiction
+    split
+    · contradiction
+    rename_i heq
     cases h₁ with
-    | refl => tauto
+    | refl => simp
     | @step m h₁ =>
-      simp at h₁
+      simp
       apply Or.inr
       simp [toList] at ih
-      apply ih <;> linarith
+      simp at h₃
+      simp only [Nat.add_one, ←heq]
+      conv =>
+        lhs; arg 4
+        calc
+          _ = start + d.succ * step + d' - (start + step) := Nat.sub_sub _ _ _
+          _ = start + step + d * step + d' - (start + step) := by rw [Nat.succ_mul]; ring_nf
+
+      have h₄ : start + step ≤ m.succ := by
+        have := Nat.dvd_of_mod_eq_zero h₃
+        cases this
+        rename_i dd h
+        cases dd
+        · simp_arith at h
+          have := Nat.le_of_sub_eq_zero h
+          have := Nat.lt_of_le_of_lt h₁ (Nat.lt_add_one m)
+          linarith
+        · rename_i n
+          have : m.succ = start + step * (n + 1) := by
+            rw [add_comm]
+            apply Nat.eq_add_of_sub_eq
+            · apply Nat.le_succ_of_le
+              assumption
+            · assumption
+          rw [this]
+          simp [Nat.mul_succ]
+
+      apply ih
+      · assumption
+      · assumption
+      · calc
+          _ < _ := h₂
+          _ = start + step + d * step + d' := by simp_arith [Nat.succ_mul]
+      · apply Nat.mod_eq_zero_of_dvd
+        rw [←Nat.sub_sub]
+        apply Nat.dvd_sub
+        apply Nat.le_sub_of_add_le
+        · rw [Nat.add_comm]
+          assumption
+        · apply Nat.dvd_of_mod_eq_zero
+          assumption
+        · simp
 
 @[simp]
 lemma MerkleTree.GetElem.def {tree : MerkleTree α H d} {i : ℕ} {ih : i < 2^d}:
   tree[i] = tree.itemAtFin ⟨i, ih⟩ := by rfl
 
-theorem Vector.exists_ofElems {p : Fin n → α → Prop} : (∀ (i : Fin n), ∃j, p i j) ↔ ∃(v : Vector α n), ∀i (_: i<n), p ⟨i, by assumption⟩ v[i] := by
+theorem Vector.exists_ofElems {p : Fin n → α → Prop} : (∀ (i : Fin n), ∃j, p i j) ↔ ∃(v : List.Vector α n), ∀i (_: i<n), p ⟨i, by assumption⟩ v[i] := by
   apply Iff.intro
   . intro h
     induction n with
     | zero =>
-      exists Vector.nil
+      exists List.Vector.nil
       intro i h
       linarith [h]
     | succ n ih =>
-      rw [Vector.exists_succ_iff_exists_snoc]
+      rw [List.Vector.exists_succ_iff_exists_snoc]
       have hp_init := ih fun (i : Fin n) => h (Fin.castLE (by linarith) i)
       rcases hp_init with ⟨vinit, hpinit⟩
       exists vinit