Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adding preserves-definedness attributes to domains.md #4680

Draft
wants to merge 3 commits into
base: develop
Choose a base branch
from
Draft

Adding preserves-definedness attributes to domains.md #4680

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
0bf722f
adding preserves-definedness in domains.md
PetarMax Nov 2, 2024
699ca38
Merge branch 'develop' into petar/pres-def
PetarMax Nov 19, 2024
68e532c
Merge branch 'develop' into petar/pres-def
palinatolmach Nov 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
41 changes: 21 additions & 20 deletions k-distribution/include/kframework/builtin/domains.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -414,19 +414,19 @@ module MAP-KORE-SYMBOLIC [symbolic,haskell]

// Adding the definedness condition `notBool (K in_keys(M))` in the ensures clause of the following rule would be redundant
// because K also appears in the rhs, preserving the case when it's #Bottom.
rule (K |-> _ M:Map) [ K <- V ] => (K |-> V M) [simplification]
rule M:Map [ K <- V ] => (K |-> V M) requires notBool (K in_keys(M)) [simplification]
rule (K |-> _ M:Map) [ K <- V ] => (K |-> V M) [simplification, preserves-definedness]
rule M:Map [ K <- V ] => (K |-> V M) requires notBool (K in_keys(M)) [simplification, preserves-definedness]
rule M:Map [ K <- _ ] [ K <- V ] => M [ K <- V ] [simplification]
// Adding the definedness condition `notBool (K1 in_keys(M))` in the ensures clause of the following rule would be redundant
// because K1 also appears in the rhs, preserving the case when it's #Bottom.
rule (K1 |-> V1 M:Map) [ K2 <- V2 ] => (K1 |-> V1 (M [ K2 <- V2 ])) requires K1 =/=K K2 [simplification]
rule (K1 |-> V1 M:Map) [ K2 <- V2 ] => (K1 |-> V1 (M [ K2 <- V2 ])) requires K1 =/=K K2 [simplification, preserves-definedness]

// Symbolic remove
rule (K |-> _ M:Map) [ K <- undef ] => M ensures notBool (K in_keys(M)) [simplification]
rule M:Map [ K <- undef ] => M requires notBool (K in_keys(M)) [simplification]
// Adding the definedness condition `notBool (K1 in_keys(M))` in the ensures clause of the following rule would be redundant
// because K1 also appears in the rhs, preserving the case when it's #Bottom.
rule (K1 |-> V1 M:Map) [ K2 <- undef ] => (K1 |-> V1 (M [ K2 <- undef ])) requires K1 =/=K K2 [simplification]
rule (K1 |-> V1 M:Map) [ K2 <- undef ] => (K1 |-> V1 (M [ K2 <- undef ])) requires K1 =/=K K2 [simplification, preserves-definedness]

// Symbolic lookup
rule (K |-> V M:Map) [ K ] => V ensures notBool (K in_keys(M)) [simplification]
Expand Down Expand Up @@ -854,8 +854,7 @@ module SET-KORE-SYMBOLIC [symbolic,haskell]
rule S |Set .Set => S [simplification, comm]
rule S |Set S => S [simplification]

rule (S SetItem(X)) |Set SetItem(X) => S SetItem(X)
ensures notBool (X in S) [simplification, comm]
rule (S SetItem(X)) |Set SetItem(X) => S SetItem(X) [simplification, comm, preserves-definedness]
// Currently disabled, see runtimeverification/haskell-backend#3301
// rule (S SetItem(X)) |Set S => S SetItem(X)
// ensures notBool (X in S) [simplification, comm]
Expand Down Expand Up @@ -1156,7 +1155,7 @@ operations listed above.
rule _:Bool impliesBool true => true [simplification]
rule B:Bool impliesBool false => notBool B [simplification]

rule B1:Bool =/=Bool B2:Bool => notBool (B1 ==Bool B2)
rule B1:Bool =/=Bool B2:Bool => notBool (B1 ==Bool B2) [priority(10)]
endmodule

module BOOL-KORE [symbolic]
Expand Down Expand Up @@ -1362,8 +1361,8 @@ module INT-SYMBOLIC [symbolic]
rule I +Int 0 => I [simplification]
rule I -Int 0 => I [simplification]

rule X modInt N => X requires 0 <=Int X andBool X <Int N [simplification]
rule X %Int N => X requires 0 <=Int X andBool X <Int N [simplification]
rule X modInt N => X requires 0 <=Int X andBool X <Int N [simplification, preserves-definedness]
rule X %Int N => X requires 0 <=Int X andBool X <Int N [simplification, preserves-definedness]

// Bit-shifts
rule X <<Int 0 => X [simplification, preserves-definedness]
Expand Down Expand Up @@ -1425,22 +1424,23 @@ module INT
imports private BOOL

rule bitRangeInt(I::Int, IDX::Int, LEN::Int) => (I >>Int IDX) modInt (1 <<Int LEN)
requires 0 <=Int IDX andBool 0 <=Int LEN [preserves-definedness]

rule signExtendBitRangeInt(I::Int, IDX::Int, LEN::Int) => (bitRangeInt(I, IDX, LEN) +Int (1 <<Int (LEN -Int 1))) modInt (1 <<Int LEN) -Int (1 <<Int (LEN -Int 1))
requires 0 <=Int IDX andBool 0 <Int LEN [preserves-definedness]

rule I1:Int divInt I2:Int => (I1 -Int (I1 modInt I2)) /Int I2
requires I2 =/=Int 0
rule
I1:Int modInt I2:Int
=>
((I1 %Int absInt(I2)) +Int absInt(I2)) %Int absInt(I2)
requires I2 =/=Int 0 [concrete, simplification]
requires I2 =/=Int 0 [preserves-definedness]

rule I1:Int modInt I2:Int => ((I1 %Int absInt(I2)) +Int absInt(I2)) %Int absInt(I2)
requires I2 =/=Int 0 [concrete, simplification, preserves-definedness]

rule minInt(I1:Int, I2:Int) => I1 requires I1 <Int I2
rule minInt(I1:Int, I2:Int) => I2 requires I1 >=Int I2

rule I1:Int =/=Int I2:Int => notBool (I1 ==Int I2)
rule (I1:Int dividesInt I2:Int) => (I2 %Int I1) ==Int 0
rule (I1:Int dividesInt I2:Int) => (I2 %Int I1) ==Int 0 requires notBool (I1 ==Int 0) [preserves-definedness]

rule I1:Int =/=Int I2:Int => notBool (I1 ==Int I2) [priority(10)]

syntax Int ::= freshInt(Int) [freshGenerator, function, total, private]
rule freshInt(I:Int) => I
Expand Down Expand Up @@ -1634,7 +1634,7 @@ IEEE 754 arithmetic. `0.0 ==Float -0.0` is also true.
| Float "==Float" Float [function, comm, smt-hook(fp.eq), hook(FLOAT.eq), symbol(_==Float_)]
| Float "=/=Float" Float [function, comm, smt-hook((not (fp.eq #1 #2)))]

rule F1:Float =/=Float F2:Float => notBool (F1 ==Float F2)
rule F1:Float =/=Float F2:Float => notBool (F1 ==Float F2) [priority(10)]
```

### Conversion between integer and float
Expand Down Expand Up @@ -1853,7 +1853,8 @@ another according to the natural lexicographic ordering of strings.
```k
syntax Bool ::= String "==String" String [function, total, comm, hook(STRING.eq)]
| String "=/=String" String [function, total, comm, hook(STRING.ne)]
rule S1:String =/=String S2:String => notBool (S1 ==String S2)

rule S1:String =/=String S2:String => notBool (S1 ==String S2) [priority(10)]

syntax Bool ::= String "<String" String [function, total, hook(STRING.lt)]
| String "<=String" String [function, total, hook(STRING.le)]
Expand Down Expand Up @@ -2319,7 +2320,7 @@ module K-EQUAL
imports K-EQUAL-SYNTAX
imports K-EQUAL-KORE

rule K1:K =/=K K2:K => notBool (K1 ==K K2)
rule K1:K =/=K K2:K => notBool (K1 ==K K2) [priority(10)]

rule #if C:Bool #then B1::K #else _ #fi => B1 requires C
rule #if C:Bool #then _ #else B2::K #fi => B2 requires notBool C
Expand Down
Loading