Skip to content

Commit 3395a56

Browse files
zhengyao-linzhengyao-lin
committed
Add some string/list built-in functions
1 parent 7648ea7 commit 3395a56

12 files changed

Lines changed: 312 additions & 81 deletions

File tree

‎README.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,7 @@ TODO:
8080
- [x] Integers
8181
- [x] Strings
8282
- [x] Lists
83-
- [ ] Built-in functions for strings, lists
83+
- [x] Some built-in functions for strings, lists
8484
- [x] Arithmetic
8585
- [x] Disjunction `;`
8686
- [x] Anonymous variables
@@ -90,6 +90,6 @@ TODO:
9090
- [x] `forall(base_pred(...), ..)`
9191
- [x] `findall(X, base_pred(..., X), ..)`
9292
- [ ] Handle the module system better when loading files
93-
- [ ] Other required special cases of `\+`, `forall`, `findall`
9493
- [ ] Private clauses in modules
9594
- [ ] Adapt to optimizations done by the compiler
95+
- [ ] Right now we conflate atom and nullary applications (e.g. `hey` vs `hey()`); need to fix this

‎prolog/meta.pl‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@
1313
gen_id(Id),
1414
write(Id), write(". "),
1515
% TODO: ignore_ops(true) will produce things like ==(...)
16-
write_term(Goal, [quoted(true), numbervars(true), character_escapes(true)]),
16+
write_term(Goal, [quoted(true), numbervars(true)]),
1717
write(" by ").
1818

1919
% Helper function for prove(maplist(...), ...)

‎src/checker.rs‎

Lines changed: 163 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -192,10 +192,10 @@ impl TermX {
192192

193193
for i in 0..args1.len()
194194
invariant
195-
args1.len() == args2.len() &&
196-
args1.deep_view() =~= self@->App_1 &&
197-
args2.deep_view() =~= other@->App_1 &&
198-
(forall |j: int| 0 <= j < i ==> (#[trigger] args1[j as int])@ == args2[j as int]@)
195+
args1.len() == args2.len(),
196+
args1.deep_view() =~= self@->App_1,
197+
args2.deep_view() =~= other@->App_1,
198+
forall |j: int| 0 <= j < i ==> (#[trigger] args1[j as int])@ == args2[j as int]@,
199199
{
200200
assert(args1[i as int]@ == self@->App_1[i as int]);
201201
if !(&args1[i]).eq(&args2[i]) {
@@ -271,10 +271,10 @@ impl TermX {
271271
// Check if any subterms are not unifiable
272272
for i in 0..args1.len()
273273
invariant
274-
args1.len() == args2.len() &&
275-
self@ =~= SpecTerm::App(f1@, args1.deep_view()) &&
276-
other@ =~= SpecTerm::App(f2@, args2.deep_view()) &&
277-
(forall |j| 0 <= j < i ==> !(#[trigger] args1[j])@.not_unifiable(args2[j]@))
274+
args1.len() == args2.len(),
275+
self@ =~= SpecTerm::App(f1@, args1.deep_view()),
276+
other@ =~= SpecTerm::App(f2@, args2.deep_view()),
277+
forall |j| 0 <= j < i ==> !(#[trigger] args1[j])@.not_unifiable(args2[j]@),
278278
{
279279
if (&args1[i]).not_unifiable(&args2[i]) {
280280
assert(self@->App_1[i as int].not_unifiable(other@->App_1[i as int]));
@@ -373,8 +373,8 @@ impl Theorem {
373373
/// Build on subproofs via the axiom SpecProof::ApplyRule
374374
pub fn apply_rule(program: &Program, rule_id: RuleId, subst: &Subst, subproofs: Vec<&Theorem>) -> (res: Option<Theorem>)
375375
requires
376-
0 <= rule_id < program.rules.len() &&
377-
forall |i| 0 <= i < subproofs.len() ==> (#[trigger] subproofs[i]).wf(program@)
376+
0 <= rule_id < program.rules.len(),
377+
forall |i| 0 <= i < subproofs.len() ==> (#[trigger] subproofs[i]).wf(program@),
378378

379379
ensures
380380
res matches Some(thm) ==> thm.wf(program@)
@@ -389,8 +389,8 @@ impl Theorem {
389389
// Check that each subproof matches the corresponding body term (after substitution)
390390
for i in 0..rule.body.len()
391391
invariant
392-
rule.body.len() == subproofs.len() &&
393-
forall |j| 0 <= j < i ==> (#[trigger] rule.body[j])@.subst(subst@) == subproofs[j].stmt@
392+
rule.body.len() == subproofs.len(),
393+
forall |j| 0 <= j < i ==> (#[trigger] rule.body[j])@.subst(subst@) == subproofs[j].stmt@,
394394
{
395395
let obligation = &TermX::subst(&rule.body[i], subst);
396396
if !obligation.eq(&subproofs[i].stmt) {
@@ -483,13 +483,13 @@ impl Theorem {
483483
// Goal[loop_var |-> list[i]]
484484
for i in 0..list.len()
485485
invariant
486-
list.len() == subproofs.len() &&
486+
list.len() == subproofs.len(),
487487

488-
(forall |j| 0 <= j < i ==> {
488+
forall |j| 0 <= j < i ==> {
489489
let subst = SpecSubst(map!{ loop_var@ => list[j]@ });
490490
let subst_goal = goal@.subst(subst);
491491
(#[trigger] subproofs[j]).stmt@ == subst_goal
492-
})
492+
},
493493
{
494494
let mut subst = Subst::new();
495495
subst.insert(loop_var.clone(), list[i].clone());
@@ -542,20 +542,20 @@ impl Theorem {
542542
for i in 0..program.rules.len()
543543
invariant
544544
// filter stays unchanged
545-
(filter == |rule: SpecRule| {
545+
filter == |rule: SpecRule| {
546546
if let Some(subst) = pattern@.matches(rule.head) {
547547
Some(template@.subst(subst))
548548
} else {
549549
None
550550
}
551-
}) &&
551+
},
552552

553553
// A prefix version of program.only_unifiable_with_base
554-
(forall |j: int| 0 <= j < i ==>
555-
(#[trigger] program@.rules[j]).matching_or_not_unifiable(pattern@)) &&
554+
forall |j: int| 0 <= j < i ==>
555+
(#[trigger] program@.rules[j]).matching_or_not_unifiable(pattern@),
556556

557557
// The first i rules are corrected processed
558-
filter_map(program@.rules.take(i as int), filter) =~= insts.deep_view()
558+
filter_map(program@.rules.take(i as int), filter) =~= insts.deep_view(),
559559
{
560560
let rule = &program.rules[i];
561561
if rule.body.len() != 0 {
@@ -616,8 +616,8 @@ impl Theorem {
616616

617617
for i in 0..insts.len()
618618
invariant
619-
insts.len() == list.len() &&
620-
(forall |j| #![auto] 0 <= j < i ==> insts[j]@ == list[j]@)
619+
insts.len() == list.len(),
620+
forall |j| #![auto] 0 <= j < i ==> insts[j]@ == list[j]@
621621
{
622622
if !(&insts[i]).eq(list[i]) {
623623
return None;
@@ -652,8 +652,8 @@ impl Theorem {
652652
// Check that the instances match the statements of the subproofs
653653
for i in 0..insts.len()
654654
invariant
655-
insts.len() == subproofs.len() &&
656-
(forall |j| #![auto] 0 <= j < i ==> insts[j]@ == subproofs[j].stmt@)
655+
insts.len() == subproofs.len(),
656+
forall |j| #![auto] 0 <= j < i ==> insts[j]@ == subproofs[j].stmt@,
657657
{
658658
if !(&insts[i]).eq(&subproofs[i].stmt) {
659659
return None;
@@ -710,7 +710,7 @@ impl Theorem {
710710
// \+P holds if P is not unifiable with head of any rule
711711
for i in 0..program.rules.len()
712712
invariant
713-
args.len() == 1 &&
713+
args.len() == 1,
714714
forall |j| 0 <= j < i ==> (#[trigger] program.rules[j]).head@.not_unifiable(args[0]@)
715715
{
716716
if !(&program.rules[i].head).not_unifiable(&args[0]) {
@@ -763,6 +763,144 @@ impl Theorem {
763763
return Some(Theorem { stmt: goal.clone(), proof: Ghost(SpecProof::BuiltIn) });
764764
}
765765
}
766+
} else if let Some(args) = goal.headed_by(FN_NAME_NONVAR, 1) {
767+
match rc_as_ref(&args[0]) {
768+
TermX::Var(..) => return None,
769+
_ => return Some(Theorem { stmt: goal.clone(), proof: Ghost(SpecProof::BuiltIn) }),
770+
}
771+
} else if let Some(args) = goal.headed_by(FN_NAME_VAR, 1) {
772+
match rc_as_ref(&args[0]) {
773+
TermX::Var(..) => return Some(Theorem { stmt: goal.clone(), proof: Ghost(SpecProof::BuiltIn) }),
774+
_ => return None,
775+
}
776+
} else if let Some(args) = goal.headed_by(FN_NAME_ATOM_STRING, 2) {
777+
match rc_as_ref(&args[1]) {
778+
(TermX::Literal(Literal::String(string))) => {
779+
if (&args[0]).headed_by(rc_str_to_str(string), 0).is_some() {
780+
return Some(Theorem { stmt: goal.clone(), proof: Ghost(SpecProof::BuiltIn) });
781+
} else {
782+
return None;
783+
}
784+
}
785+
_ => return None,
786+
}
787+
} else if let Some(args) = goal.headed_by(FN_NAME_STRING_CHARS, 2) {
788+
match rc_as_ref(&args[0]) {
789+
(TermX::Literal(Literal::String(string))) => {
790+
if let Some(chars) = (&args[1]).as_list() {
791+
if chars.len() != string.unicode_len() {
792+
return None;
793+
}
794+
795+
// Compare each char
796+
// TODO: get_char and unicode_len are O(n)
797+
// Verus doesn't support iterator string.chars() yet
798+
for i in 0..chars.len()
799+
invariant
800+
chars.len() == string@.len(),
801+
forall |j| 0 <= j < i ==>
802+
(#[trigger] chars[j])@ =~= SpecTerm::App(SpecFnName::User(seq![string@[j as int]], 0), seq![]),
803+
{
804+
match rc_as_ref(&chars[i]) {
805+
TermX::App(FnName::User(s, arity), args) => {
806+
if *arity == 0 && args.len() == 0 &&
807+
s.unicode_len() == 1 && s.get_char(0) == string.get_char(i) {
808+
assert(s@ =~= seq![string@[i as int]]);
809+
assert(args.deep_view() =~= seq![]);
810+
} else {
811+
return None;
812+
}
813+
}
814+
_ => return None,
815+
}
816+
}
817+
818+
return Some(Theorem { stmt: goal.clone(), proof: Ghost(SpecProof::BuiltIn) });
819+
} else {
820+
return None;
821+
}
822+
}
823+
_ => return None,
824+
}
825+
} else if let Some(args) = goal.headed_by(FN_NAME_SUB_STRING, 5) {
826+
match (
827+
rc_as_ref(&args[0]),
828+
rc_as_ref(&args[1]),
829+
rc_as_ref(&args[2]),
830+
rc_as_ref(&args[3]),
831+
rc_as_ref(&args[4]),
832+
) {
833+
(
834+
TermX::Literal(Literal::String(string)),
835+
TermX::Literal(Literal::Int(before)),
836+
TermX::Literal(Literal::Int(len)),
837+
TermX::Literal(Literal::Int(after)),
838+
TermX::Literal(Literal::String(substring)),
839+
) => {
840+
if *before < 0 || *len < 0 || *after < 0 {
841+
return None;
842+
}
843+
844+
// TODO: these overflow checks are not precise
845+
if *before > u32::MAX as i64 || *len > u32::MAX as i64 || *after > u32::MAX as i64 {
846+
return None;
847+
}
848+
849+
if let Some(end) = (*before).checked_add(*len) {
850+
if let Some(sum) = end.checked_add(*after) {
851+
if sum > u32::MAX as i64 {
852+
return None;
853+
}
854+
855+
if string.unicode_len() != sum as usize {
856+
return None;
857+
}
858+
859+
if substring.unicode_len() != *len as usize {
860+
return None;
861+
}
862+
863+
if *len != 0 {
864+
if !rc_str_eq_str(substring, string.substring_char(*before as usize, end as usize)) {
865+
return None;
866+
}
867+
}
868+
869+
return Some(Theorem { stmt: goal.clone(), proof: Ghost(SpecProof::BuiltIn) });
870+
}
871+
} else {
872+
return None;
873+
}
874+
}
875+
_ => return None,
876+
}
877+
} else if let Some(args) = goal.headed_by(FN_NAME_REVERSE, 2) {
878+
match ((&args[0]).as_list(), (&args[1]).as_list()) {
879+
(Some(mut list), Some(reversed)) => {
880+
let ghost old_list = list.deep_view();
881+
vec_reverse(&mut list);
882+
883+
assert(old_list.reverse() == list.deep_view());
884+
885+
// Check that list == reversed
886+
if list.len() != reversed.len() {
887+
return None;
888+
}
889+
890+
for i in 0..list.len()
891+
invariant
892+
list.len() == reversed.len(),
893+
forall |j| 0 <= j < i ==> #[trigger] list[j]@ == reversed[j]@,
894+
{
895+
if !list[i].eq(reversed[i]) {
896+
return None;
897+
}
898+
}
899+
900+
return Some(Theorem { stmt: goal.clone(), proof: Ghost(SpecProof::BuiltIn) });
901+
}
902+
_ => return None,
903+
}
766904
}
767905

768906
Self::unverified_builtins(program, goal)

0 commit comments

Comments
 (0)