From 057c2ddaefe7b490f097fb55cba2d3b09a8a822e Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Mon, 13 Jan 2025 12:55:01 +0100 Subject: [PATCH 1/9] `Prelude.lean`: Add uninterpreted `Map` implementation --- pyk/src/pyk/k2lean4/Prelude.lean | 109 ++++++++++++++++++++++++++++--- 1 file changed, 101 insertions(+), 8 deletions(-) diff --git a/pyk/src/pyk/k2lean4/Prelude.lean b/pyk/src/pyk/k2lean4/Prelude.lean index ce14a59bfd..f233af6f77 100644 --- a/pyk/src/pyk/k2lean4/Prelude.lean +++ b/pyk/src/pyk/k2lean4/Prelude.lean @@ -1,10 +1,103 @@ -abbrev SortBool : Type := Int -abbrev SortBytes: Type := ByteArray -abbrev SortId : Type := String -abbrev SortInt : Type := Int -abbrev SortString : Type := String +/- +K Prelude in Lean 4 + +Functions with the `hook` attribute need to have a manual implementation in the backends. +This file contains the Lean 4 definitions of the hooked functions in `domains.md`. + +Currently we translate hooked functions as uninterpreted functions together with axioms asserting their behavior. +The current definition can be put into three levels: + +1. Signature Level: +The signature of the hooks, this includes aliases for Sorts and function symbols for hooked functions. + +2. Rule Level: +The behavior of the uninterpreted symbols can be asserted through axioms or theorems. +Inconsistencies can arise from them, so it falls under the user to make sure axioms are consistent and/or theorems provable. + +3. Simplification Level: +With the theory defined through function rules, simplifications can be stated as theorems. +These theorems should be provable directly from the function rules and the semantics of the Sorts. + -/ + +-- Basic K types +abbrev SortBool : Type := Int +abbrev SortBytes : Type := ByteArray +abbrev SortId : Type := String +abbrev SortInt : Type := Int +abbrev SortString : Type := String abbrev SortStringBuffer : Type := String -abbrev ListHook (E : Type) : Type := List E -abbrev MapHook (K : Type) (V : Type) : Type := List (K × V) -abbrev SetHook (E : Type) : Type := List E + +namespace MapHookDef +/- +The `Map` sort represents a generalized associative array. +Each key can be paired with an arbitrary value, and can be used to reference its associated value. +Multiple bindings for the same key are not allowed. +Note that both keys and values will always be KItems. + -/ + +-- Signature to be instantiated by map implementations +structure MapHookSig (K V : Type) where + map : Type -- Carrier, such as List (KItem × KItem) + unit : map + cons : K → V → map → map + lookup : map → K → V + lookup? : map → K → V -- lookup with default + update : K → V → map → map + delete : map → K → map + concat : map → map → Option map + difference : map → map → map + updateMap : map → map → map + removeAll : map → List K → map + keys : map → List K + in_keys : map → K → Bool + values : map → List V + size : map → Nat + includes : map → map → Bool -- map inclusion + choice : map → K -- arbitrary key from a map + nodup : forall al : map, List.Nodup (keys al) + +-- We use axioms to have uninterpreted functions +variable (K V : Type) +axiom mapCAx : Type -- Map Carrier +axiom unitAx : mapCAx +axiom consAx : K → V → mapCAx → mapCAx +axiom lookupAx : mapCAx → K → V +axiom lookupAx? : mapCAx → K → V -- lookup with default +axiom updateAx : K → V → mapCAx → mapCAx +axiom deleteAx : mapCAx → K → mapCAx +axiom concatAx : mapCAx → mapCAx → Option mapCAx +axiom differenceAx : mapCAx → mapCAx → mapCAx +axiom updateMapAx : mapCAx → mapCAx → mapCAx +axiom removeAllAx : mapCAx → List K → mapCAx +axiom keysAx : mapCAx → List K +axiom in_keysAx : mapCAx → K → Bool +axiom valuesAx : mapCAx → List V +axiom sizeAx : mapCAx → Nat +axiom includesAx : mapCAx → mapCAx → Bool -- map inclusion +axiom choiceAx : mapCAx → K -- arbitrary key from a map +axiom nodupAx : forall al : mapCAx, List.Nodup (keysAx K al) + +-- Uninterpreted Map implementation +noncomputable def mapImpl (K V : Type) : MapHookSig K V := + MapHookSig.mk + mapCAx + unitAx + (consAx K V) + (lookupAx K V) + (lookupAx? K V) + (updateAx K V) + (deleteAx K) + concatAx + differenceAx + updateMapAx + (removeAllAx K) + (keysAx K) + (in_keysAx K) + (valuesAx V) + sizeAx + includesAx + (choiceAx K) + (nodupAx K) + +end MapHookDef From 9cffbc7ff5f199f1fe603ff7e47bcaac82e600c4 Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Thu, 16 Jan 2025 13:11:52 +0100 Subject: [PATCH 2/9] Add back `ListHook` and `SetHook` --- pyk/src/pyk/k2lean4/Prelude.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/pyk/src/pyk/k2lean4/Prelude.lean b/pyk/src/pyk/k2lean4/Prelude.lean index f233af6f77..31196456e7 100644 --- a/pyk/src/pyk/k2lean4/Prelude.lean +++ b/pyk/src/pyk/k2lean4/Prelude.lean @@ -27,6 +27,8 @@ abbrev SortInt : Type := Int abbrev SortString : Type := String abbrev SortStringBuffer : Type := String +abbrev ListHook (E : Type) : Type := List E +abbrev SetHook (E : Type) : Type := List E namespace MapHookDef /- From 4f8646e3be43fcfa46f34bfa45f7560d32f71da5 Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Thu, 16 Jan 2025 13:14:48 +0100 Subject: [PATCH 3/9] Better writing of `nodupAx` --- pyk/src/pyk/k2lean4/Prelude.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/k2lean4/Prelude.lean b/pyk/src/pyk/k2lean4/Prelude.lean index 31196456e7..f5bdca6b66 100644 --- a/pyk/src/pyk/k2lean4/Prelude.lean +++ b/pyk/src/pyk/k2lean4/Prelude.lean @@ -78,7 +78,7 @@ axiom valuesAx : mapCAx → List V axiom sizeAx : mapCAx → Nat axiom includesAx : mapCAx → mapCAx → Bool -- map inclusion axiom choiceAx : mapCAx → K -- arbitrary key from a map -axiom nodupAx : forall al : mapCAx, List.Nodup (keysAx K al) +axiom nodupAx : forall m, List.Nodup (keysAx K m) -- Uninterpreted Map implementation noncomputable def mapImpl (K V : Type) : MapHookSig K V := From 8c617c2fc87f25e2468ce28cc4575193e131eea3 Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Thu, 16 Jan 2025 15:25:57 +0100 Subject: [PATCH 4/9] Use `{ _ := _ }` notation in `mapImpl` --- pyk/src/pyk/k2lean4/Prelude.lean | 37 ++++++++++++++++---------------- 1 file changed, 18 insertions(+), 19 deletions(-) diff --git a/pyk/src/pyk/k2lean4/Prelude.lean b/pyk/src/pyk/k2lean4/Prelude.lean index f5bdca6b66..066cd68615 100644 --- a/pyk/src/pyk/k2lean4/Prelude.lean +++ b/pyk/src/pyk/k2lean4/Prelude.lean @@ -82,24 +82,23 @@ axiom nodupAx : forall m, List.Nodup (keysAx K m) -- Uninterpreted Map implementation noncomputable def mapImpl (K V : Type) : MapHookSig K V := - MapHookSig.mk - mapCAx - unitAx - (consAx K V) - (lookupAx K V) - (lookupAx? K V) - (updateAx K V) - (deleteAx K) - concatAx - differenceAx - updateMapAx - (removeAllAx K) - (keysAx K) - (in_keysAx K) - (valuesAx V) - sizeAx - includesAx - (choiceAx K) - (nodupAx K) + { map := mapCAx, + unit := unitAx, + cons := (consAx K V), + lookup := (lookupAx K V), + lookup? := (lookupAx? K V), + update := (updateAx K V), + delete := (deleteAx K), + concat := concatAx, + difference := differenceAx, + updateMap := updateMapAx, + removeAll := (removeAllAx K), + keys := (keysAx K), + in_keys := (in_keysAx K), + values := (valuesAx V), + size := sizeAx, + includes := includesAx, + choice := (choiceAx K), + nodup := (nodupAx K) } end MapHookDef From a3199fe0d5040212cb6e4383fcee3e6648fd065d Mon Sep 17 00:00:00 2001 From: "Juan C." <38925412+JuanCoRo@users.noreply.github.com> Date: Fri, 17 Jan 2025 12:56:31 +0100 Subject: [PATCH 5/9] =?UTF-8?q?Change=20`lookup`=20type=20to=20`map=20?= =?UTF-8?q?=E2=86=92=20K=20=E2=86=92=20Option=20V`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Tamás Tóth --- pyk/src/pyk/k2lean4/Prelude.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/k2lean4/Prelude.lean b/pyk/src/pyk/k2lean4/Prelude.lean index 066cd68615..c5b1faa9c4 100644 --- a/pyk/src/pyk/k2lean4/Prelude.lean +++ b/pyk/src/pyk/k2lean4/Prelude.lean @@ -43,7 +43,7 @@ structure MapHookSig (K V : Type) where map : Type -- Carrier, such as List (KItem × KItem) unit : map cons : K → V → map → map - lookup : map → K → V + lookup : map → K → Option V lookup? : map → K → V -- lookup with default update : K → V → map → map delete : map → K → map From 75db10836607635ba217f236ed2a63d845c3745a Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Fri, 17 Jan 2025 13:00:48 +0100 Subject: [PATCH 6/9] Add correct type of `lookupAx` --- pyk/src/pyk/k2lean4/Prelude.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/k2lean4/Prelude.lean b/pyk/src/pyk/k2lean4/Prelude.lean index c5b1faa9c4..514fddd6d8 100644 --- a/pyk/src/pyk/k2lean4/Prelude.lean +++ b/pyk/src/pyk/k2lean4/Prelude.lean @@ -64,7 +64,7 @@ variable (K V : Type) axiom mapCAx : Type -- Map Carrier axiom unitAx : mapCAx axiom consAx : K → V → mapCAx → mapCAx -axiom lookupAx : mapCAx → K → V +axiom lookupAx : mapCAx → K → Option V axiom lookupAx? : mapCAx → K → V -- lookup with default axiom updateAx : K → V → mapCAx → mapCAx axiom deleteAx : mapCAx → K → mapCAx From 62695126dcd0fbf7264c95e52496fbf06cba1526 Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Fri, 17 Jan 2025 18:37:03 +0100 Subject: [PATCH 7/9] Remove `ListHook` and `SetHook` --- pyk/src/pyk/k2lean4/Prelude.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/pyk/src/pyk/k2lean4/Prelude.lean b/pyk/src/pyk/k2lean4/Prelude.lean index 17c5ec7581..ef05e668f3 100644 --- a/pyk/src/pyk/k2lean4/Prelude.lean +++ b/pyk/src/pyk/k2lean4/Prelude.lean @@ -27,9 +27,6 @@ abbrev SortInt : Type := Int abbrev SortString : Type := String abbrev SortStringBuffer : Type := String -abbrev ListHook (E : Type) : Type := List E -abbrev SetHook (E : Type) : Type := List E - namespace MapHookDef /- The `Map` sort represents a generalized associative array. From 3fa52f4a8479edd9abe762e3a141c9f32ce91b32 Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Fri, 17 Jan 2025 18:37:31 +0100 Subject: [PATCH 8/9] Generate correct `MAP` hook implementations --- pyk/src/pyk/k2lean4/k2lean4.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py index 56c5da967d..f9e0e61b47 100644 --- a/pyk/src/pyk/k2lean4/k2lean4.py +++ b/pyk/src/pyk/k2lean4/k2lean4.py @@ -154,7 +154,7 @@ def _collection(self, sort: str) -> Structure: val = Term(f'List {item}') case CollectionKind.MAP: key, value = sorts - val = Term(f'List ({key} × {value})') + val = Term(f'(MapHook {key} {value}).map') field = ExplBinder(('coll',), val) return Structure(sort, Signature((), Term('Type')), ctor=StructCtor((field,))) From 3afb864ada017a8bcf7cafc50adeddcec09793bd Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Fri, 17 Jan 2025 18:41:02 +0100 Subject: [PATCH 9/9] Rename `mapImpl` to `MapHook` --- pyk/src/pyk/k2lean4/Prelude.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/k2lean4/Prelude.lean b/pyk/src/pyk/k2lean4/Prelude.lean index ef05e668f3..d0aed86a96 100644 --- a/pyk/src/pyk/k2lean4/Prelude.lean +++ b/pyk/src/pyk/k2lean4/Prelude.lean @@ -78,7 +78,7 @@ axiom choiceAx : mapCAx → K -- arbitrary key from a map axiom nodupAx : forall m, List.Nodup (keysAx K m) -- Uninterpreted Map implementation -noncomputable def mapImpl (K V : Type) : MapHookSig K V := +noncomputable def MapHook (K V : Type) : MapHookSig K V := { map := mapCAx, unit := unitAx, cons := (consAx K V),