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

Bring sequence axiomatization more in line with carbon to fix #629 #638

Closed
wants to merge 1 commit into from
Closed

Bring sequence axiomatization more in line with carbon to fix #629 #638

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
59 changes: 45 additions & 14 deletions src/main/resources/dafny_axioms/sequences.vpr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,9 @@ domain $Seq[E] {
function Seq_drop(s: $Seq[E], n: Int): $Seq[E]
function Seq_equal(s1: $Seq[E], s2: $Seq[E]): Bool
function Seq_sameuntil(s1: $Seq[E], s2: $Seq[E], i: Int): Bool
function Seq_skolemdiff(s1: $Seq[E], s2: $Seq[E]): Int
function Seq_arith_add(i: Int, j: Int): Int
function Seq_arith_sub(i: Int, j: Int): Int

axiom seq_length_non_negative {
forall s: $Seq[E] :: {Seq_length(s)}
Expand All @@ -30,7 +33,7 @@ domain $Seq[E] {
}

axiom length_singleton_seq {
forall e: E :: {Seq_length(Seq_singleton(e))}
forall e: E :: {Seq_singleton(e)}
Seq_length(Seq_singleton(e)) == 1
}

Expand Down Expand Up @@ -66,24 +69,41 @@ domain $Seq[E] {
e1 == e2
}

axiom seq_append_empty_left { // The axiom was not in the Dafny version
forall s: $Seq[E] :: {Seq_append(Seq_empty(), s)}
Seq_append(Seq_empty(), s) == s
axiom seq_append_empty {
forall s1: $Seq[E], s2: $Seq[E] :: {Seq_append(s1, s2)}
(s1 == Seq_empty() ==> Seq_append(s1, s2) == s2) &&
(s2 == Seq_empty() ==> Seq_append(s1, s2) == s1)
}

axiom seq_append_empty_right { // The axiom was not in the Dafny version
forall s: $Seq[E] :: {Seq_append(s, Seq_empty())}
Seq_append(s, Seq_empty()) == s
axiom seq_index_over_append_left {
forall s1: $Seq[E], s2: $Seq[E], i: Int ::
{Seq_index(Seq_append(s1, s2), i)}
{Seq_index(s1, i), Seq_append(s1, s2)}
s1 != Seq_empty() && s2 != Seq_empty() && 0 <= i && i < Seq_length(s1) ==> Seq_index(Seq_append(s1, s2), i) == Seq_index(s1, i)
}

axiom seq_index_over_append {
axiom seq_index_over_append_right {
forall s1: $Seq[E], s2: $Seq[E], i: Int ::
{Seq_index(Seq_append(s1, s2), i)}
{Seq_index(s1, i), Seq_append(s1, s2)}
s1 != Seq_empty() && s2 != Seq_empty() /*&& 0 <= i && i < Seq_length(Seq_append(s1, s2))*/ ==> ( // Implication not in the Dafny version
i < Seq_length(s1)
? Seq_index(Seq_append(s1, s2), i) == Seq_index(s1, i)
: Seq_index(Seq_append(s1, s2), i) == Seq_index(s2, i - Seq_length(s1)))
s1 != Seq_empty() && s2 != Seq_empty() && Seq_length(s1) <= i && i < Seq_length(Seq_append(s1, s2)) ==>
Seq_arith_add(Seq_arith_sub(i, Seq_length(s1)), Seq_length(s1)) == i &&
Seq_index(Seq_append(s1, s2), i) == Seq_index(s2, Seq_arith_sub(i, Seq_length(s1)))
}

axiom seq_index_over_append_right_inv {
forall s1: $Seq[E], s2: $Seq[E], i: Int ::
{Seq_index(s2, i), Seq_append(s1, s2)}
s1 != Seq_empty() && s2 != Seq_empty() && 0 <= i && i < Seq_length(s2) ==>
Seq_arith_sub(Seq_arith_add(i, Seq_length(s1)), Seq_length(s1)) == i &&
Seq_index(Seq_append(s1, s2), Seq_arith_add(i, Seq_length(s1))) == Seq_index(s2, i)
}

axiom seq_add_def {
forall i: Int, j: Int :: {Seq_arith_add(i, j)} Seq_arith_add(i, j) == i + j
}

axiom seq_sub_def {
forall i: Int, j: Int :: {Seq_arith_sub(i, j)} Seq_arith_sub(i, j) == i - j
}

axiom seq_length_invariant_over_update {
Expand Down Expand Up @@ -156,7 +176,7 @@ domain $Seq[E] {
axiom extensional_seq_equality {
forall s1: $Seq[E], s2: $Seq[E] :: {Seq_equal(s1, s2)}
Seq_equal(s1, s2)
<==> // Two implications in the Dafny version
==>
(Seq_length(s1) == Seq_length(s2) &&
forall i: Int :: {Seq_index(s1, i)} {Seq_index(s2, i)}
0 <= i && i < Seq_length(s1) ==>
Expand All @@ -168,6 +188,17 @@ domain $Seq[E] {
Seq_equal(s1, s2) ==> s1 == s2
}

axiom seq_disequality_skolem {
forall s1: $Seq[E], s2: $Seq[E] :: {Seq_equal(s1, s2)}
(s1 == s2 && Seq_equal(s1, s2)) ||
(s1 != s2 && !Seq_equal(s1, s2) && Seq_length(s1) != Seq_length(s2)) ||
(s1 != s2 && !Seq_equal(s1, s2) && Seq_length(s1) == Seq_length(s2) &&
Seq_skolemdiff(s1, s2) == Seq_skolemdiff(s2, s1) &&
0 <= Seq_skolemdiff(s1, s2) && Seq_skolemdiff(s1, s2) < Seq_length(s1) &&
Seq_index(s1, Seq_skolemdiff(s1, s2)) != Seq_index(s2, Seq_skolemdiff(s1, s2))
)
}

axiom extensional_seq_equality_prefix {
forall s1: $Seq[E], s2: $Seq[E], n: Int :: {Seq_sameuntil(s1, s2, n)}
Seq_sameuntil(s1, s2, n)
Expand Down