Skip to content

Commit

Permalink
remove commented out code
Browse files Browse the repository at this point in the history
  • Loading branch information
@utaal
utaal committed Aug 21, 2024
1 parent adff7ae commit 7ab42a6
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 270 deletions.
183 changes: 1 addition & 182 deletions milli/doubly-linked-list/creusot.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,79 +16,6 @@ mod lemmas {
#[ensures(x.set(k1, v1).set(k2, v2) == x.set(k2, v2).set(k1, v1))]
pub fn map_set_commute<K, V>(x: Mapping<K, V>, k1: K, k2: K, v1: V, v2: V) {}

// #[law]
// #[open(self)]
// #[requires(x.get(k) == v)]
// #[ensures(x.set(k, v) == x)]
// pub fn map_set_id<K, V>(x: Mapping<K, V>, k: K, v: V) {}

// #[law]
// #[open(self)]
// #[requires(x1.disjoint(x2))]
// #[ensures(x1.union(x2) == x2.union(x1))]
// pub fn union_commute<K, V>(x1: FMap<K, V>, x2: FMap<K, V>) {
// proof_assert!(x1.union(x2).ext_eq(x2.union(x1)));
// }

// #[law]
// #[open(self)]
// #[requires(x1.disjoint(x2))]
// #[requires(x1.contains(k))]
// #[ensures(x1.union(x2).remove(k).ext_eq(x1.remove(k).union(x2)))]
// pub fn union_remove<K, V>(x1: FMap<K, V>, x2: FMap<K, V>, k: K) {}

// #[law]
// #[open(self)]
// #[requires(x1.insert(k,v).disjoint(x2))]
// #[ensures(x1.union(x2).insert(k, v).ext_eq(x1.insert(k, v).union(x2)))]
// pub fn union_insert<K, V>(x1: FMap<K, V>, x2: FMap<K, V>, k: K, v: V) {}

// #[law]
// #[open(self)]
// #[ensures(FMap::empty().union(x).ext_eq(x))]
// pub fn union_empty<K, V>(x: FMap<K, V>) {}

// #[logic]
// #[open(self)]
// #[ensures(s.subsequence(0, s.len()) == s)]
// pub fn subseq_full<T>(s: Seq<T>) {
// s.subsequence(0, s.len()).ext_eq(s);
// }

// #[logic]
// #[open(self)]
// #[requires(0 <= i && i < s.len())]
// #[ensures(s.subsequence(i, i+1) == Seq::singleton(s[i]))]
// pub fn subseq_singleton<T>(s: Seq<T>, i: Int) {
// s.subsequence(i, i + 1).ext_eq(Seq::singleton(s[i]));
// }

// #[logic]
// #[open(self)]
// #[requires(0 <= i && i <= j && j <= k && k <= s.len())]
// #[ensures(s.subsequence(i, j).concat(s.subsequence(j, k)) == s.subsequence(i, k))]
// pub fn concat_subseq<T>(s: Seq<T>, i: Int, j: Int, k: Int) {
// s.subsequence(i, k)
// .ext_eq(s.subsequence(i, j).concat(s.subsequence(j, k)));
// }

// #[logic]
// #[open(self)]
// #[ensures(s1.concat(s2).subsequence(0, s1.len()) == s1)]
// #[ensures(s1.concat(s2).subsequence(s1.len(), s1.len() + s2.len()) == s2)]
// pub fn subseq_concat<T>(s1: Seq<T>, s2: Seq<T>) {
// s1.ext_eq(s1.concat(s2).subsequence(0, s1.len()));
// s2.ext_eq(s1.concat(s2).subsequence(s1.len(), s1.len() + s2.len()));
// }

// #[logic]
// #[open(self)]
// #[requires(0 <= i && i <= j && j <= s.len() && 0 <= k && k <= l && i + l <= j)]
// #[ensures(s.subsequence(i, j).subsequence(k, l) == s.subsequence(i + k, i + l))]
// pub fn subseq_subseq<T>(s: Seq<T>, i: Int, j: Int, k: Int, l: Int) {
// s.subsequence(i + k, i + l)
// .ext_eq(s.subsequence(i, j).subsequence(k, l));
// }
}

mod linked_list {
Expand All @@ -106,114 +33,6 @@ mod linked_list {
prev: *const Node<T>,
}

/// Is there a linked list segment from ptr to other
// #[predicate]
// #[variant(token.len())]
// #[ensures(ptr == other ==> result == (token == FMap::empty()))]
// #[ensures(result && ptr != other ==> token.contains(ptr))]
// fn lseg_forward<T>(
// ptr: *const Node<T>,
// other: *const Node<T>,
// token: FMap<*const Node<T>, Node<T>>,
// ) -> bool {
// if ptr == other {
// token == FMap::empty()
// } else {
// match token.get(ptr) {
// None => false,
// Some(node) => lseg_forward(node.next, other, token.remove(ptr)),
// }
// }
// }
//
// #[ghost]
// #[variant(token.len())]
// #[ensures(ptr == other ==> result == Seq::EMPTY)]
// fn lseg_forward_seq<T>(
// ptr: *const Node<T>,
// other: *const Node<T>,
// token: FMap<*const Node<T>, Node<T>>,
// ) -> Seq<T> {
// if ptr == other {
// Seq::EMPTY
// } else {
// match token.get(ptr) {
// None => Seq::EMPTY,
// Some(node) => {
// Seq::singleton(node.data).concat(lseg_forward_seq(node.next, other, token.remove(ptr)))
// }
// }
// }
// }

// // ptr <-- other
// #[predicate]
// #[variant(token.len())]
// #[ensures(ptr == other ==> result == (token == FMap::empty()))]
// #[ensures(result && ptr != other ==> token.contains(other))]
// fn lseg_backward<T>(
// ptr: *const Node<T>,
// other: *const Node<T>,
// token: FMap<*const Node<T>, Node<T>>,
// ) -> bool {
// if ptr == other {
// token == FMap::empty()
// } else {
// match token.get(other) {
// None => false,
// Some(node) => lseg_backward(ptr, node.prev, token.remove(other)),
// }
// }
// }
//
// // ptr <-- other
// #[ghost]
// #[variant(token.len())]
// #[ensures(ptr == other ==> result == Seq::EMPTY)]
// fn lseg_backward_seq<T>(
// ptr: *const Node<T>,
// other: *const Node<T>,
// token: FMap<*const Node<T>, Node<T>>,
// ) -> Seq<T> {
// if ptr == other {
// Seq::EMPTY
// } else {
// match token.get(other) {
// None => Seq::EMPTY,
// Some(node) => {
// lseg_backward_seq(ptr, node.prev, token.remove(other)).concat(Seq::singleton(node.data))
// }
// }
// }
// }

/// Lemma for concatenating 2 segments
// #[logic]
// #[variant(token12.len())]
// #[requires(token12.disjoint(token23))]
// #[requires(lseg_forward(ptr1, ptr2, token12))]
// #[requires(lseg_forward(ptr2, ptr3, token23))]
// #[requires(!token12.contains(ptr3))]
// #[ensures(result)]
// #[ensures(lseg_forward(ptr1, ptr3, token12.union(token23)))]
// #[ensures(lseg_forward_seq(ptr1, ptr3, token12.union(token23)).ext_eq(lseg_forward_seq(ptr1, ptr2, token12).concat(lseg_forward_seq(ptr2, ptr3, token23))))]
// fn lseg_trans<T>(
// ptr1: *const Node<T>,
// ptr2: *const Node<T>,
// ptr3: *const Node<T>,
// token12: FMap<*const Node<T>, Node<T>>,
// token23: FMap<*const Node<T>, Node<T>>,
// ) -> bool {
// union_remove::<*const Node<T>, Node<T>>;
// union_empty::<*const Node<T>, Node<T>>;
// if ptr1 != ptr2 {
// let next = token12.lookup(ptr1).next;
// lseg_trans(next, ptr2, ptr3, token12.remove(ptr1), token23)
// } else {
// true
// }
// }

pub struct LinkedList<T> {
head: *const Node<T>,
tail: *const Node<T>,
Expand Down Expand Up @@ -533,4 +352,4 @@ mod main {
// proof_assert!([email protected]() == 1);
}

}
}
88 changes: 0 additions & 88 deletions milli/linked-list/dafny.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -292,91 +292,3 @@ method Main() {
}
}

// module Main2 {
// import opened LinkedList
// method Main() {
// var l1 := new LinkedList();
// var l2 := new LinkedList();
// // TODO use machine integers
// l1.Push(1);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l1.Push(1);
// l1.Push(1);
// l1.Push(1);
// l1.Push(1);
// l1.Push(1);
// l1.Push(1);
// l1.Push(1);
// l1.Push(1);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l1.Push(1);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l1.Push(1);
// l1.Push(1);
// l1.Push(1);
// l1.Push(1);
// l1.Push(1);
// l1.Push(1);
// l1.Push(1);
// l1.Push(1);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// l2.Push(1);
// l1.Push(0);
// l2.Push(0);
// // assert(|l1.contents| == 2);
// // assert(|l2.contents| == 2);
// // var v1 := l1.Pop();
// // var v2 := l2.Pop();
// // assert(|l1.contents| == 1);
// // assert(|l2.contents| == 1);
// // assert(v1 == 0);
// // assert(v2 == 0);
// }
// }

0 comments on commit 7ab42a6

Please sign in to comment.