Skip to content

Commit

Permalink
Update DSL so that we can translate the FFS example
Browse files Browse the repository at this point in the history
  • Loading branch information
@Kiiyya
Kiiyya committed Dec 17, 2024
1 parent 2286302 commit 29f5d8c
Show file tree
Hide file tree
Showing 4 changed files with 363 additions and 291 deletions.
280 changes: 126 additions & 154 deletions Examples/Ffs.lean
View file
Original file line number Diff line number Diff line change
@@ -1,34 +1,25 @@
import LeanBoogie.BoogieDsl
import LeanBoogie.Dsl

#check 1

open Boogie


theorem unit_seq : ITree.seq (Pure.pure ()) b = b := by rw [ITree.seq]; simp_all only [pure_bind]
open LeanBoogie

abbrev adaptBool (f : BitVec 32 -> BitVec 32 -> Bool) (x y : Int) : Int := if f x y then 1 else 0

def trunc (i : Int) : Int := @BitVec.truncate 32 8 i |>.toInt
-- def sext (i : Int) : Int := @BitVec.signExtend 32 i
def bv.slt (x : Int) (y : Int) : Int := if @BitVec.slt 32 x y then 1 else 0
def bv.add (x : Int) (y : Int) : Int := x + y
def bv.shl (x : Int) (y : Int) : Int := @BitVec.shiftLeft 32 x y.toNat |>.toInt
def bv.and (x : Int) (y : Int) : Int := @BitVec.and 32 x y |>.toInt
def bv.lshr (x : Int) (y : Int) : Int := @BitVec.ushiftRight 32 x y.toNat |>.toInt
def bv.ne (x y : Int) : Int := if x ≠ y then 1 else 0
def bv.trunc_32_8 (x : BitVec 32) : BitVec 8 := BitVec.truncate _ x
def bv.sext_8_32 (x : BitVec 8) : BitVec 32 := BitVec.signExtend _ x
def bv.slt (x y : BitVec n) : BitVec 1 := if BitVec.slt x y then 1 else 0
def bv.add (x y : BitVec n) : BitVec n := BitVec.add x y
def bv.shl (x y : BitVec n) : BitVec n := BitVec.shiftLeft x y.toNat
def bv.and (x y : BitVec n) : BitVec n := BitVec.and x y
def bv.lshr (x y : BitVec n) : BitVec n := BitVec.ushiftRight x y.toNat
def bv.ne (x y : BitVec n) : BitVec 1 := if x ≠ y then 1 else 0

-- set_option pp.explicit true
-- set_option trace.Meta.isDefEq true

procedure ffs_ref(i0: bv32) returns (r: bv32) {
var i1: bv1;
var i3: bv32;
var i4: bv32;
var i5: bv1;
var i6: bv32;
var i7: bv32;
var i8: bv32;
var i9: bv1;
var i10: bv32;
var i2: bv32;
var i1: bv1; var i3: bv32; var i4: bv32; var i5: bv1; var i6: bv32; var i7: bv32; var i8: bv32;
var i9: bv1; var i10: bv32; var i2: bv32;
goto bb0;
bb0:
i1 := bv.ne(i0, 0);
goto bb1, bb2;
Expand Down Expand Up @@ -72,132 +63,113 @@ bb9:
goto bb4;
}

-- procedure ffs_imp(i0: bv32) returns (r: bv32) {
-- var i1: bv32;
-- var i2: bv1;
-- var i5: bv32;
-- var i6: bv32;
-- var i7: bv8;
-- var i8: bv32;
-- var i3: bv8;
-- var i4: bv32;
-- var i9: bv32;
-- var i10: bv1;
-- var i13: bv32;
-- var i14: bv32;
-- var i15: bv8;
-- var i16: bv32;
-- var i11: bv8;
-- var i12: bv32;
-- var i17: bv32;
-- var i18: bv1;
-- var i21: bv32;
-- var i22: bv32;
-- var i23: bv8;
-- var i24: bv32;
-- var i19: bv8;
-- var i20: bv32;
-- var i25: bv32;
-- var i26: bv1;
-- var i29: bv32;
-- var i30: bv32;
-- var i31: bv8;
-- var i32: bv32;
-- var i27: bv8;
-- var i28: bv32;
-- var i33: bv1;
-- var i34: bv32;
-- var i35: bv32;
-- var i36: bv32;
-- var i37: bv32;
-- var i38: bv32;
-- bb0:
-- i1 := and(i0, 65535);
-- i2 := ne(i1, 0);
-- i3, i4 := 1, i0;
-- goto bb1, bb3;
-- bb1:
-- assume (i2 == 1);
-- goto bb2;
-- bb2:
-- i9 := and(i4, 255);
-- i10 := ne(i9, 0);
-- i11, i12 := i3, i4;
-- goto bb4, bb6;
-- bb3:
-- assume !((i2 == 1));
-- i5 := sext(1);
-- i6 := add(i5, 16);
-- i7 := trunc(i6);
-- i8 := lshr(i0, 16);
-- i3, i4 := i7, i8;
-- goto bb2;
-- bb4:
-- assume (i10 == 1);
-- goto bb5;
-- bb5:
-- i17 := and(i12, 15);
-- i18 := ne(i17, 0);
-- i19, i20 := i11, i12;
-- goto bb7, bb9;
-- bb6:
-- assume !((i10 == 1));
-- i13 := sext(i3);
-- i14 := add(i13, 8);
-- i15 := trunc(i14);
-- i16 := lshr(i4, 8);
-- i11, i12 := i15, i16;
-- goto bb5;
-- bb7:
-- assume (i18 == 1);
-- goto bb8;
-- bb8:
-- i25 := and(i20, 3);
-- i26 := ne(i25, 0);
-- i27, i28 := i19, i20;
-- goto bb10, bb12;
-- bb9:
-- assume !((i18 == 1));
-- i21 := sext(i11);
-- i22 := add(i21, 4);
-- i23 := trunc(i22);
-- i24 := lshr(i12, 4);
-- i19, i20 := i23, i24;
-- goto bb8;
-- bb10:
-- assume (i26 == 1);
-- goto bb11;
-- bb11:
-- i33 := ne(i28, 0);
-- goto bb13, bb14;
-- bb12:
-- assume !((i26 == 1));
-- i29 := sext(i19);
-- i30 := add(i29, 2);
-- i31 := trunc(i30);
-- i32 := lshr(i20, 2);
-- i27, i28 := i31, i32;
-- goto bb11;
-- bb13:
-- assume (i33 == 1);
-- i34 := sext(i27);
-- i35 := add(i28, 1);
-- i36 := and(i35, 1);
-- i37 := add(i34, i36);
-- i38 := i37;
-- goto bb15;
-- bb14:
-- assume !((i33 == 1));
-- i38 := 0;
-- goto bb15;
-- bb15:
-- r := i38;
-- return;
-- }
-- procedure check(x: bv32) {
-- var r_ref: bv32;
-- var r_imp: bv32;
-- call r_ref := ffs_ref(x);
-- call r_imp := ffs_imp(x);
-- assert r_ref == r_imp;
-- }
#print ffs_ref

-- set_option trace.LeanBoogie.dsl true
-- set_option trace.Meta.isDefEq true

procedure ffs_imp(i0: bv32) returns (r: bv32) {
var i1: bv32; var i2: bv1; var i5: bv32; var i6: bv32; var i7: bv8; var i8: bv32; var i3: bv8;
var i4: bv32; var i9: bv32; var i10: bv1; var i13: bv32; var i14: bv32; var i15: bv8;
var i16: bv32; var i11: bv8; var i12: bv32; var i17: bv32; var i18: bv1; var i21: bv32;
var i22: bv32; var i23: bv8; var i24: bv32; var i19: bv8; var i20: bv32; var i25: bv32;
var i26: bv1; var i29: bv32; var i30: bv32; var i31: bv8; var i32: bv32; var i27: bv8;
var i28: bv32; var i33: bv1; var i34: bv32; var i35: bv32; var i36: bv32; var i37: bv32;
var i38: bv32;
goto bb0;
bb0:
i1 := bv.and(i0, 65535);
i2 := bv.ne(i1, 0);
i3 := 1;
i4 := i0;
goto bb1, bb3;
bb1:
assume (i2 == 1);
goto bb2;
bb2:
i9 := bv.and(i4, 255);
i10 := bv.ne(i9, 0);
i11 := i3;
i12 := i4;
goto bb4, bb6;
bb3:
assume !((i2 == 1));
i5 := bv.sext_8_32(1);
i6 := bv.add(i5, 16);
i7 := bv.trunc_32_8(i6);
i8 := bv.lshr(i0, 16);
i3 := i7;
i4 := i8;
goto bb2;
bb4:
assume (i10 == 1);
goto bb5;
bb5:
i17 := bv.and(i12, 15);
i18 := bv.ne(i17, 0);
i19 := i11;
i20 := i12;
goto bb7, bb9;
bb6:
assume !((i10 == 1));
i13 := bv.sext_8_32(i3);
i14 := bv.add(i13, 8);
i15 := bv.trunc_32_8(i14);
i16 := bv.lshr(i4, 8);
i11 := i15;
i12 := i16;
goto bb5;
bb7:
assume (i18 == 1);
goto bb8;
bb8:
i25 := bv.and(i20, 3);
i26 := bv.ne(i25, 0);
i27 := i19;
i28 := i20;
goto bb10, bb12;
bb9:
assume !((i18 == 1));
i21 := bv.sext_8_32(i11);
i22 := bv.add(i21, 4);
i23 := bv.trunc_32_8(i22);
i24 := bv.lshr(i12, 4);
i19 := i23;
i20 := i24;
goto bb8;
bb10:
assume (i26 == 1);
goto bb11;
bb11:
i33 := bv.ne(i28, 0);
goto bb13, bb14;
bb12:
assume !((i26 == 1));
i29 := bv.sext_8_32(i19);
i30 := bv.add(i29, 2);
i31 := bv.trunc_32_8(i30);
i32 := bv.lshr(i20, 2);
i27 := i31;
i28 := i32;
goto bb11;
bb13:
assume (i33 == 1);
i34 := bv.sext_8_32(i27);
i35 := bv.add(i28, 1);
i36 := bv.and(i35, 1);
i37 := bv.add(i34, i36);
i38 := i37;
goto bb15;
bb14:
assume !((i33 == 1));
i38 := 0;
goto bb15;
bb15:
r := i38;
return;
}

#check 10

example : interp ffs_imp = interp ffs_ref := by
sorry
2 changes: 2 additions & 0 deletions Examples/SimpleIter.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,7 @@ example : interp p1 = interp p2 := by
rw [while_fp]
rw [while_fp]
rw [while_fp]
simp

-- 2. Push `interp` inwards as far as possible,
-- this will change `ITree.{pure, bind, iter, ite, read, write}`
Expand Down Expand Up @@ -122,6 +123,7 @@ example : interp p1 = interp p2 := by
normalize
simp


sorry

done
Loading

0 comments on commit 29f5d8c

Please sign in to comment.