From 00542447b9f69e356f264f599f38d3718b86e46f Mon Sep 17 00:00:00 2001 From: Your Name Date: Thu, 5 Mar 2026 10:02:06 +0100 Subject: [PATCH] Replaced some cases instances with grind --- InductiveVerification/Event.lean | 12 +- InductiveVerification/Message.lean | 11 +- InductiveVerification/NS_Public.lean | 256 ++++++++++----------------- InductiveVerification/Public.lean | 8 +- Main.lean | 2 +- 5 files changed, 115 insertions(+), 174 deletions(-) diff --git a/InductiveVerification/Event.lean b/InductiveVerification/Event.lean index a9b1408..23c44c9 100644 --- a/InductiveVerification/Event.lean +++ b/InductiveVerification/Event.lean @@ -11,10 +11,11 @@ inductive Event -- Define the `initState` function class HasInitState (α : Type) where initState : α → Set Msg - + variable [ hasInitStateAgent : HasInitState Agent ] open HasInitState +attribute [simp] initState -- Define the `bad` set abbrev DecidableMem ( A : Set Agent ) := (a : Agent) → Decidable (a ∈ A) @@ -27,8 +28,8 @@ class Bad where instance [Bad] : DecidableMem Bad.bad := Bad.decidableBad open Bad --- attribute [simp] Spy_in_bad --- attribute [simp] Server_not_bad +attribute [simp, grind .] Spy_in_bad +attribute [simp] Server_not_bad instance decidableAgentEq : DecidableEq Agent := λ a b => @@ -60,9 +61,12 @@ def knows [Bad] : Agent → List Event → Set Msg if A = A' then insert X (knows A evs) else knows A evs | A, Event.Notes A' X :: evs => if A = A' then insert X (knows A evs) else knows A evs + +attribute [simp] knows -- Define the `spies` abbreviation abbrev spies (evs : List Event) [Bad] : Set Msg := knows Agent.Spy evs +attribute [simp] spies -- Define the `used` function def used : List Event → Set Msg @@ -172,6 +176,7 @@ lemma Notes_imp_knows_Spy [Bad] {A : Agent} {X : Msg} {evs : List Event} : -- Elimination rules: derive contradictions from old Says events containing -- items known to be fresh +@[grind ., grind! .] lemma Says_imp_parts_knows_Spy [Bad] : ∀ {A B : Agent} {X : Msg} {evs : List Event}, Event.Says A B X ∈ evs → X ∈ parts (knows Agent.Spy evs) := by @@ -364,6 +369,7 @@ lemma knows_Spy_imp_Says_Notes_initState [Bad] {X : Msg} {evs : List Event} : · apply ih at h; aapply knows_Spy_imp_Says_Notes_initState_aux -- Parts of what the Spy knows are a subset of what is used +@[grind! .] lemma parts_knows_Spy_subset_used [Bad] : parts (knows Agent.Spy evs) ⊆ used evs := by induction evs with diff --git a/InductiveVerification/Message.lean b/InductiveVerification/Message.lean index 04ce031..33f9bdc 100644 --- a/InductiveVerification/Message.lean +++ b/InductiveVerification/Message.lean @@ -604,6 +604,12 @@ by | snd h ih => exact analz.snd ih | decrypt h₁ h₂ ih₁ ih₂ => exact analz.decrypt ih₁ ih₂ +@[grind .] +lemma analz_insert_mono [InvKey] : + X ∈ analz H → X ∈ analz (insert Y H) +:= by + apply_rules [ analz_mono, Set.subset_insert] + lemma analz_mono_neg [InvKey] { h : A ⊆ B } : X ∉ analz B → X ∉ analz A := by @@ -624,7 +630,7 @@ by · apply analz.fst h · apply analz.snd h -@[simp] +@[simp, grind! .] lemma analz_increasing [InvKey] {H : Set Msg} : H ⊆ analz H := λ _ hx => analz.inj hx @@ -637,6 +643,7 @@ by | snd _ ih => aapply parts.snd | decrypt _ _ ih₁ => aapply parts.body +@[grind! .] lemma analz_subset_parts {H : Set Msg} [InvKey] : analz H ⊆ parts H := λ _ hx => analz_into_parts hx @@ -1628,5 +1635,3 @@ X ∈ A ∨ h₁ → X ∈ B ∨ h₁ intro h; cases h <;> try simp_all left; aapply h -attribute [-simp] Key.injEq - diff --git a/InductiveVerification/NS_Public.lean b/InductiveVerification/NS_Public.lean index eb3e230..e733639 100644 --- a/InductiveVerification/NS_Public.lean +++ b/InductiveVerification/NS_Public.lean @@ -40,75 +40,68 @@ theorem possibility_property : constructor · apply ns_public.NS3 · apply ns_public.NS2 - · apply_rules [ns_public.NS1, ns_public.Nil, Nonce_notin_used_empty] + · apply_rules[ns_public.NS1, ns_public.Nil, Nonce_notin_used_empty] · simp · tauto all_goals tauto · simp -- Spy never sees another agent's private key unless it's bad at the start -@[simp] +@[simp, grind =] theorem Spy_see_priEK {h : ns_public evs} : (Key (priEK A) ∈ parts (spies evs)) ↔ A ∈ bad := by constructor · induction h with - | Nil => - simp[spies, knows, initState, pubEK, priEK, pubSK] - | Fake _ h ih => + | Nil => simp[priEK] + | Fake _ h => apply Fake_parts_sing at h intro h₁; simp at h₁; apply Fake_parts_sing_helper (h := h) at h₁ simp_all | NS1 => simp_all | NS2 => simp_all | NS3 => simp_all - · intro h₁; apply parts_increasing; aapply Spy_spies_bad_privateKey + · intro _; apply_rules [ parts_increasing, Spy_spies_bad_privateKey ] @[simp] theorem Spy_analz_priEK {h : ns_public evs} : - Key (priEK A) ∈ analz (spies evs) ↔ A ∈ bad := by - constructor - · intro h₁; apply analz_subset_parts at h₁; aapply Spy_see_priEK.mp - · intro h₁; apply analz_increasing; aapply Spy_spies_bad_privateKey + Key (priEK A) ∈ analz (spies evs) ↔ A ∈ bad +:= by grind --- It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce is secret +-- It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce is +-- secret +@[grind! .] theorem no_nonce_NS1_NS2 { evs: List Event} { h : ns_public evs } : (Crypt (pubEK C) ⦃NA', Nonce NA, Agent D⦄ ∈ parts (spies evs) → (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄ ∈ parts (spies evs) → Nonce NA ∈ analz (spies evs))) := by intro h₁ h₂ induction h with - | Nil => simp[spies, knows] at h₂ - | Fake _ h ih => - simp; apply analz_insert; - apply Fake_parts_sing at h - simp at h₁; apply Fake_parts_sing_helper (h := h) at h₁; simp at h₁ - simp at h₂; apply Fake_parts_sing_helper (h := h) at h₂; simp at h₂ - rcases h₁ with ((_ | _) | _) <;> - rcases h₂ with ((_ | _) | _) <;> - simp_all - all_goals (right; aapply ih <;> aapply analz_subset_parts) - | NS1 _ nonce_not_used => - apply analz_spies_mono + | Nil => simp at h₂ + | Fake _ h => + simp [*] at * + apply Fake_parts_sing at h + apply Fake_parts_sing_helper (h := h) at h₁ + apply Fake_parts_sing_helper (h := h) at h₂ + simp_all; grind + | NS1 => simp [*] at * - apply parts_knows_Spy_subset_used_neg at nonce_not_used; expand_parts_element at h₁; expand_parts_element at h₂; - cases h₂ <;> simp_all - | NS2 _ nonce_not_used => - apply analz_spies_mono + grind + | NS2 => simp [*] at * - apply parts_knows_Spy_subset_used_neg at nonce_not_used; expand_parts_element at h₂; - cases h₁ <;> simp_all[-Key.injEq] - | NS3 _ _ _ a_ih => apply analz_spies_mono; simp_all + grind + | NS3 => apply analz_spies_mono; simp_all -- Unicity for NS1: nonce NA identifies agents A and B +@[grind! .] theorem unique_NA { h : ns_public evs } : (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄ ∈ parts (spies evs) → (Crypt (pubEK B') ⦃Nonce NA, Agent A'⦄ ∈ parts (spies evs) → (Nonce NA ∉ analz (spies evs) → A = A' ∧ B = B'))) := by induction h with - | Nil => simp[spies, knows] + | Nil => simp | Fake _ a a_ih => apply Fake_parts_sing at a; intro h₁ h₂ h₃; apply analz_spies_mono_neg at h₃; @@ -116,18 +109,14 @@ theorem unique_NA { h : ns_public evs } : apply Fake_parts_sing_helper (h := a) at h₁ apply Fake_parts_sing_helper (h := a) at h₂ simp_all - | NS1 _ nonce_not_used a_ih => - intro h₁ h₂ h₃ - apply analz_insert_mono_neg at h₃ - simp [*] at * - expand_parts_element at h₁ - expand_parts_element at h₂ - apply parts_knows_Spy_subset_used_neg at nonce_not_used - cases h₁ <;> cases h₂ <;> simp_all - | NS2 => intro _ _ h₃; apply analz_insert_mono_neg at h₃; simp_all - | NS3 => intro _ _ h₃; apply analz_insert_mono_neg at h₃; simp_all; + | NS1 => + intro h₁ h₂ _; simp [*] at * + expand_parts_element at h₁; expand_parts_element at h₂; grind + | NS2 => intro _ _ _; simp_all; grind + | NS3 => intro _ _ _; simp_all; grind -- Spy does not see the nonce sent in NS1 if A and B are secure +@[grind! .] theorem Spy_not_see_NA { h : ns_public evs } { not_bad_A : A ∉ bad } { not_bad_B : B ∉ bad } : @@ -136,37 +125,27 @@ theorem Spy_not_see_NA { h : ns_public evs } intro h₁ h₄ induction h with | Nil => simp_all - | Fake _ a => - have _ := Spy_in_bad; apply Fake_analz_insert at a; apply a at h₄; simp_all - | NS1 _ a a_ih => + | Fake _ a => apply Fake_analz_insert at a; apply a at h₄; simp_all + | NS1 _ a => simp_all; rcases h₁ with (_ | h) · simp_all; apply a; aapply analz_knows_Spy_subset_used · apply analz_insert_Crypt_subset at h₄; simp at h₄; cases h₄ <;> simp_all - apply Says_imp_used at h; apply used_parts_subset_parts at h + apply Says_imp_used at h; apply used_parts_subset_parts at h; simp_all[Set.subset_def] - | NS2 _ not_used_NB a a_ih => - simp at h₁ - have _ := h₄ - simp at h₄; apply analz_insert_Crypt_subset at h₄ - simp at h₄; rcases h₄ with ( h | h | h) - · simp [*] at *; have c := h₁; apply a_ih at c; - have _ := c; - apply Says_imp_parts_knows_Spy at h₁ - apply Says_imp_parts_knows_Spy at a + | NS2 _ _ a a_ih => + simp [*] at *; have _ := h₄; have c := h₁ + apply Says_imp_parts_knows_Spy at h₁ + have d := h₁ + expand_parts_element at d + apply analz_insert_Crypt_subset at h₄; simp at h₄; rcases h₄ with (h |h |h) + <;> simp [*] at *; + · apply a_ih at c; have _ := c; apply Says_imp_parts_knows_Spy at a apply unique_NA at h₁; apply h₁ at a; apply a at c; all_goals simp_all - · simp_all - apply not_used_NB; apply parts_knows_Spy_subset_used; apply parts.fst; - apply parts.body; apply Says_imp_parts_knows_Spy; assumption - · aapply a_ih - | NS3 _ _ a₂ a_ih => - simp [*] at * - have _ := h₄ - apply analz_insert_Crypt_subset at h₄; simp[*] at h₄; - have _ := h₁; simp[*] at h₁; apply Says_imp_parts_knows_Spy at h₁ - apply Says_imp_parts_knows_Spy at a₂ - aapply a_ih; apply no_nonce_NS1_NS2 <;> try simp [*] <;> assumption + · grind + | NS3 => apply analz_insert_Crypt_subset at h₄; simp[*] at h₄; grind --- Authentication for `A`: if she receives message 2 and has used `NA` to start a run, then `B` has sent message 2. +-- Authentication for `A`: if she receives message 2 and has used `NA` to start +-- a run, then `B` has sent message 2. theorem A_trusts_NS2 {h : ns_public evs } { not_bad_A : A ∉ bad } { not_bad_B : B ∉ bad } : @@ -179,28 +158,19 @@ theorem A_trusts_NS2 {h : ns_public evs } -- use unique_NA to show that B' = B induction h with | Nil => simp_all - | Fake _ a a_ih => + | Fake _ a => have snsNA := h₁; apply Spy_not_see_NA at snsNA <;> try assumption apply analz_spies_mono_neg at snsNA simp [*] at * cases h₁ - · have _ := Spy_in_bad; simp_all + · simp_all · apply Fake_parts_sing at a; apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂ - rcases h₂ with ((_ | _) | _) <;> (right; aapply a_ih) - · aapply analz_subset_parts - · tauto + grind · aapply ns_public.Fake - | NS1 _ a a_ih => - apply parts_knows_Spy_subset_used_neg at a; - simp [*] at *; expand_parts_element at h₂; cases h₁ <;> simp_all - | NS2 _ _ a a_ih => - simp [*] at * - have snsNA := h₁; apply Spy_not_see_NA at snsNA <;> try assumption - cases h₂ <;> simp_all - apply Says_imp_parts_knows_Spy at a; apply unique_NA at a; - apply Says_imp_parts_knows_Spy at h₁; apply a at h₁; all_goals simp_all - | NS3 _ _ a a_ih => simp_all; + | NS1 => simp [*] at *; expand_parts_element at h₂; grind + | NS2 => simp [*] at *; grind + | NS3 => simp_all; -- If the encrypted message appears then it originated with Alice in `NS1` lemma B_trusts_NS1 { h : ns_public evs} : @@ -210,19 +180,19 @@ lemma B_trusts_NS1 { h : ns_public evs} : := by intro h₁ h₂ induction h with - | Nil => simp[spies, knows] at h₁ - | Fake _ a a_ih => + | Nil => simp at h₁ + | Fake _ a => apply analz_spies_mono_neg at h₂ simp at h₁; apply Fake_parts_sing at a; apply Fake_parts_sing_helper (h := a) at h₁; simp_all - | NS1 _ _ a_ih => - apply analz_spies_mono_neg at h₂; simp_all; cases h₁ <;> simp_all - | NS2 _ _ _ a_ih => apply analz_spies_mono_neg at h₂; simp_all; - | NS3 _ _ _ a_ih => apply analz_spies_mono_neg at h₂; simp_all; + | NS1 => apply analz_spies_mono_neg at h₂; simp_all; grind + | NS2 => apply analz_spies_mono_neg at h₂; simp_all; + | NS3 => apply analz_spies_mono_neg at h₂; simp_all; -- Authenticity Properties obtained from `NS2` -- Unicity for `NS2`: nonce `NB` identifies nonce `NA` and agent `A` +@[grind! .] theorem unique_NB { h : ns_public evs } : (Crypt (pubEK A) ⦃Nonce NA, Nonce NB, Agent B⦄ ∈ parts (spies evs) → (Crypt (pubEK A') ⦃Nonce NA', Nonce NB, Agent B'⦄ ∈ parts (spies evs) → @@ -230,30 +200,22 @@ theorem unique_NB { h : ns_public evs } : A = A' ∧ NA = NA' ∧ B = B'))) := by -- Proof closely follows that of unique_NA induction h with - | Nil => aesop (add norm spies, norm knows, safe analz_insertI) - | Fake _ a a_ih => + | Nil => aesop (add safe analz_insertI) + | Fake _ a => apply Fake_parts_sing at a; intro h₁ h₂ h₃; simp [*] at * apply Fake_parts_sing_helper (h := a) at h₁; apply Fake_parts_sing_helper (h := a) at h₂; simp [*] at * apply analz_insert_mono_neg at h₃ - rcases h₁ with ((_ | _) | _) <;> - rcases h₂ with ((_ | _) | _) <;> - simp_all - all_goals (aapply a_ih; repeat aapply analz_subset_parts) - | NS1 _ _ a_ih => intro h₁ h₂ h₃; simp at h₁; simp at h₂; aapply a_ih - aapply analz_spies_mono_neg - | NS2 _ nonce_not_used _ a_ih => - intro h₁ h₂ h₃; simp [*] at * - expand_parts_element at h₁ - expand_parts_element at h₂ - apply analz_insert_mono_neg at h₃; - apply parts_knows_Spy_subset_used_neg at nonce_not_used - rcases h₁ with (_ | h₁) <;> - rcases h₂ with (_ | h₂) <;> simp_all - | NS3 _ _ _ a_ih => - intro h₁ h₂ h₃; apply analz_spies_mono_neg at h₃; simp_all[-Key.injEq] + grind + | NS1 => intro _ _ h₃; apply analz_spies_mono_neg at h₃; simp_all + | NS2 => + intro h₁ h₂ _; simp [*] at * + expand_parts_element at h₁; expand_parts_element at h₂ + grind + | NS3 => intro _ _ _; simp_all; grind -- `NB` remains secret +@[grind! .] theorem Spy_not_see_NB { h : ns_public evs } { not_bad_A : A ∉ bad } { not_bad_B : B ∉ bad } : @@ -263,33 +225,25 @@ theorem Spy_not_see_NB { h : ns_public evs } intro h₁ h₄ induction h with | Nil => simp_all - | Fake _ a a_ih => - have _ := Spy_in_bad; apply Fake_analz_insert at a; apply a at h₄; simp_all; - | NS1 _ nonce_not_used a_ih => + | Fake _ a => apply Fake_analz_insert at a; apply a at h₄; simp_all; + | NS1 => simp [*] at * apply analz_insert_Crypt_subset at h₄; simp at h₄ - apply parts_knows_Spy_subset_used_neg at nonce_not_used - have h₂ := h₁; apply Says_imp_parts_knows_Spy at h₂ - expand_parts_element at h₂; simp_all - | NS2 _ not_used_NB a a_ih => + have _ := h₁; apply Says_imp_parts_knows_Spy at h₁ + expand_parts_element at h₁ + grind + | NS2 => simp [*] at * - apply parts_knows_Spy_subset_used_neg at not_used_NB + have _ := h₄ + apply analz_insert_Crypt_subset at h₄; simp at h₄; rcases h₁ with (_ | h₁) - · simp_all; apply not_used_NB; aapply analz_subset_parts - · apply analz_insert_Crypt_subset at h₄; simp at h₄; rcases h₄ with (_ |_ |_ ) - · aapply a_ih; apply Says_imp_parts_knows_Spy at a; - apply Says_imp_parts_knows_Spy at h₁; simp_all; aapply no_nonce_NS1_NS2 - · apply Says_imp_parts_knows_Spy at h₁; - expand_parts_element at h₁; simp_all - · aapply a_ih - | NS3 _ _ a a_ih => - simp at h₁; simp[analz_insert_Crypt_element] at h₄; - rcases h₄ with (⟨_, _⟩ | ⟨_, _⟩) <;> simp_all - apply Says_imp_parts_knows_Spy at a - apply Says_imp_parts_knows_Spy at h₁; apply unique_NB at a - apply a at h₁; apply h₁ at a_ih; simp_all; assumption + · simp_all; grind + · have _ := h₁; apply Says_imp_parts_knows_Spy at h₁; + expand_parts_element at h₁; grind + | NS3 => simp[analz_insert_Crypt_element] at h₄; simp [*] at *; grind --- Authentication for `B`: if he receives message 3 and has used `NB` in message 2, then `A` has sent message 3. +-- Authentication for `B`: if he receives message 3 and has used `NB` in message +-- 2, then `A` has sent message 3. theorem B_trusts_NS3 { h : ns_public evs } { not_bad_A : A ∉ bad } { not_bad_B : B ∉ bad } : @@ -301,28 +255,14 @@ theorem B_trusts_NS3 { h : ns_public evs } apply Says_imp_parts_knows_Spy at h₂ induction h with | Nil => simp_all - | Fake _ a a_ih => + | Fake _ a => simp [*] at * apply Fake_parts_sing at a apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂ - expand_parts_element at h₂; - rcases h₁ with (_ | h₁) <;> - rcases h₂ with ((h₂ | _) | _) <;> simp_all[Spy_in_bad] - · apply analz_subset_parts at h₂; simp_all - · apply Spy_not_see_NB at h₁ <;> simp_all + grind | NS1 => simp_all - | NS2 _ nonce_not_used => - simp [*] at * - apply parts_knows_Spy_subset_used_neg at nonce_not_used; - expand_parts_element at h₂; cases h₁ <;> simp_all - | NS3 _ _ a₂ => - simp [*] at *; - expand_parts_element at h₂; cases h₂ <;> simp_all - have h₁c := h₁ - apply Spy_not_see_NB at h₁c - apply Says_imp_parts_knows_Spy at h₁; apply unique_NB at h₁; - apply Says_imp_parts_knows_Spy at a₂; apply h₁ at a₂ - all_goals simp_all + | NS2 => simp [*] at *; expand_parts_element at h₂; grind + | NS3 => simp [*] at *; grind -- Overall guarantee for `B` @@ -337,29 +277,13 @@ theorem B_trusts_protocol { h : ns_public evs } intro h₁ h₂ induction h with | Nil => simp_all - | Fake _ a a_ih => + | Fake _ a => simp [*] at * apply Fake_parts_sing at a - apply Fake_parts_sing_helper (h := a) at h₁; - expand_parts_element at h₁ - rcases h₂ with (_ | h₂) <;> simp_all[Spy_in_bad] - rcases h₁ with (((_ |_ ) | _) | _) <;> try simp_all - · right; aapply a_ih; aapply analz_subset_parts - · apply Spy_not_see_NB at h₂ <;> simp_all + apply Fake_parts_sing_helper (h := a) at h₁; expand_parts_element at h₁ + grind | NS1 => simp_all - | NS2 _ nonce_not_used a a_ih => - simp [*] at * - apply parts_knows_Spy_subset_used_neg at nonce_not_used; - expand_parts_element at h₁; cases h₂ <;> simp_all - | NS3 _ _ a₂ a_ih => - simp [*] at * - expand_parts_element at h₁ - cases h₁ <;> simp_all - have h₂c := h₂ - apply Spy_not_see_NB at h₂c - apply Says_imp_parts_knows_Spy at h₂ - apply Says_imp_parts_knows_Spy at a₂ - apply unique_NB at h₂; apply h₂ at a₂ - apply a₂ at h₂c; all_goals simp_all + | NS2 => simp [*] at *; expand_parts_element at h₁; grind + | NS3 => simp [*] at *; grind end NS_Public diff --git a/InductiveVerification/Public.lean b/InductiveVerification/Public.lean index 5e2f4a0..26aaf34 100644 --- a/InductiveVerification/Public.lean +++ b/InductiveVerification/Public.lean @@ -33,6 +33,11 @@ noncomputable abbrev priSK (A : Agent) : Key := privateKey KeyMode.Signature A noncomputable abbrev pubK (A : Agent) : Key := pubEK A noncomputable abbrev priK (A : Agent) : Key := invKey (pubEK A) +attribute [simp] pubEK +attribute [simp] pubSK +-- attribute [simp] priEK +-- attribute [simp] priSK + -- Axioms for private and public keys @[simp] axiom privateKey_neq_publicKey {b c : KeyMode} {A A' : Agent} : @@ -320,7 +325,7 @@ lemma priK_in_initState {b : KeyMode} {A : Agent} : Msg.Key (privateKey b A) ∈ initState A := by induction A <;> simp [HasInitState.initState, initState, privateKey, pubEK, pubSK] <;> - cases b <;> simp[Spy_in_bad] + cases b <;> simp @[simp] lemma publicKey_in_initState {b : KeyMode} {A : Agent} {B : Agent} : @@ -344,6 +349,7 @@ lemma analz_spies_pubK : Msg.Key (publicKey b A) ∈ analz (spies evs) := by exact analz.inj spies_pubK -- Spy sees private keys of bad agents +@[grind .] lemma Spy_spies_bad_privateKey { h : A ∈ bad } : Msg.Key (privateKey b A) ∈ spies evs := by induction evs with | nil => simp_all [spies, knows, pubSK, pubEK]; cases b <;> tauto diff --git a/Main.lean b/Main.lean index bfa0201..b647d88 100644 --- a/Main.lean +++ b/Main.lean @@ -1,5 +1,5 @@ -- import InductiveVerification -import InductiveVerification.Public +import InductiveVerification.NS_Public def main : IO Unit := IO.println "Hello, world!"