include "RTLabs/import.ma". include "common/Animation.ma". (*program:*) definition id_search := ident_of_nat 0. definition search9 := 53. definition search8 := 52. definition search7 := 51. definition search6 := 50. definition search53 := 49. definition search52 := 48. definition search51 := 47. definition search50 := 46. definition search5 := 45. definition search49 := 44. definition search48 := 43. definition search47 := 42. definition search46 := 41. definition search45 := 40. definition search44 := 39. definition search43 := 38. definition search42 := 37. definition search41 := 36. definition search40 := 35. definition search4 := 34. definition search39 := 33. definition search38 := 32. definition search37 := 31. definition search36 := 30. definition search35 := 29. definition search34 := 28. definition search33 := 27. definition search32 := 26. definition search31 := 25. definition search30 := 24. definition search3 := 23. definition search29 := 22. definition search28 := 21. definition search27 := 20. definition search26 := 19. definition search25 := 18. definition search24 := 17. definition search23 := 16. definition search22 := 15. definition search21 := 14. definition search20 := 13. definition search2 := 12. definition search19 := 11. definition search18 := 10. definition search17 := 9. definition search16 := 8. definition search15 := 7. definition search14 := 6. definition search13 := 5. definition search12 := 4. definition search11 := 3. definition search10 := 2. definition search1 := 1. definition search0 := 0. definition C_cost0 := costlabel_of_nat 8. definition C_cost8 := costlabel_of_nat 7. definition C_cost1 := costlabel_of_nat 6. definition C_cost6 := costlabel_of_nat 5. definition C_cost4 := costlabel_of_nat 4. definition C_cost7 := costlabel_of_nat 3. definition C_cost5 := costlabel_of_nat 2. definition C_cost2 := costlabel_of_nat 1. definition C_cost3 := costlabel_of_nat 0. definition pre_search := mk_pre_internal_function (mk_signature [ASTptr Any; ASTint I8 Signed; ASTint I8 Signed] (Some ? (ASTint I8 Signed))) (Some ? 8) [7; 1; 2] [3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18; 19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34; 35; 36; 37; 38; 39; 40] [7; 15; 23; 29] 0 [ (pair ?? search9 (make_St_cost C_cost0 search8)); (pair ?? search8 (make_St_op1 Ocast8unsigned 10 6 search7)); (pair ?? search7 (make_St_const 11 (Ointconst (repr 1)) search6)); (pair ?? search6 (make_St_op2 Oadd 4 10 11 search4)); (pair ?? search53 (make_St_cost C_cost8 search52)); (pair ?? search52 (make_St_const 4 (Ointconst (repr 0)) search51)); (pair ?? search51 (make_St_op1 Ocast8unsigned 39 1 search50)); (pair ?? search50 (make_St_const 40 (Ointconst (repr 1)) search49)); (pair ?? search5 (make_St_cost C_cost1 search4)); (pair ?? search49 (make_St_op2 Osub 5 39 40 search4)); (pair ?? search48 (make_St_op1 Ocast8unsigned 37 5 search47)); (pair ?? search47 (make_St_op1 Ocast8unsigned 38 4 search46)); (pair ?? search46 (make_St_op2 (Ocmp Cge) 36 37 38 search45)); (pair ?? search45 (make_St_cond1 Onotbool 36 search3 search44)); (pair ?? search44 (make_St_cost C_cost6 search43)); (pair ?? search43 (make_St_op1 Ocast8unsigned 34 5 search42)); (pair ?? search42 (make_St_op1 Ocast8unsigned 35 4 search41)); (pair ?? search41 (make_St_op2 Oadd 32 34 35 search40)); (pair ?? search40 (make_St_const 33 (Ointconst (repr 2)) search39)); (pair ?? search4 (make_St_skip search48)); (pair ?? search39 (make_St_op2 Odiv 6 32 33 search38)); (pair ?? search38 (make_St_const 31 (Ointconst (repr 1)) search37)); (pair ?? search37 (make_St_op2 Omul 30 6 31 search36)); (pair ?? search36 (make_St_op2 Oaddp 29 7 30 search35)); (pair ?? search35 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[29]] 28 search34)); (pair ?? search34 (make_St_op1 Ocast8unsigned 26 28 search33)); (pair ?? search33 (make_St_op1 Ocast8unsigned 27 2 search32)); (pair ?? search32 (make_St_cond2 (Ocmp Ceq) 26 27 search31 search29)); (pair ?? search31 (make_St_cost C_cost4 search30)); (pair ?? search30 (make_St_op1 Oid 8 6 search0)); (pair ?? search3 (make_St_cost C_cost7 search2)); (pair ?? search29 (make_St_cost C_cost5 search28)); (pair ?? search28 (make_St_const 25 (Ointconst (repr 1)) search27)); (pair ?? search27 (make_St_op2 Omul 24 6 25 search26)); (pair ?? search26 (make_St_op2 Oaddp 23 7 24 search25)); (pair ?? search25 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[23]] 22 search24)); (pair ?? search24 (make_St_op1 Ocast8unsigned 20 22 search23)); (pair ?? search23 (make_St_op1 Ocast8unsigned 21 2 search22)); (pair ?? search22 (make_St_cond2 (Ocmp Cgt) 20 21 search21 search17)); (pair ?? search21 (make_St_cost C_cost2 search20)); (pair ?? search20 (make_St_op1 Ocast8unsigned 18 6 search19)); (pair ?? search2 (make_St_const 9 (Ointconst (repr 1)) search1)); (pair ?? search19 (make_St_const 19 (Ointconst (repr 1)) search18)); (pair ?? search18 (make_St_op2 Osub 5 18 19 search16)); (pair ?? search17 (make_St_cost C_cost3 search16)); (pair ?? search16 (make_St_const 17 (Ointconst (repr 1)) search15)); (pair ?? search15 (make_St_op2 Omul 16 6 17 search14)); (pair ?? search14 (make_St_op2 Oaddp 15 7 16 search13)); (pair ?? search13 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[15]] 14 search12)); (pair ?? search12 (make_St_op1 Ocast8unsigned 12 14 search11)); (pair ?? search11 (make_St_op1 Ocast8unsigned 13 2 search10)); (pair ?? search10 (make_St_cond2 (Ocmp Clt) 12 13 search9 search5)); (pair ?? search1 (make_St_op1 Onegint 8 9 search0)); (pair ?? search0 (make_St_return)) ] search53 search0. definition id_main := ident_of_nat 1. definition main9 := 41. definition main8 := 40. definition main7 := 39. definition main6 := 38. definition main5 := 37. definition main41 := 36. definition main40 := 35. definition main4 := 34. definition main39 := 33. definition main38 := 32. definition main37 := 31. definition main36 := 30. definition main35 := 29. definition main34 := 28. definition main33 := 27. definition main32 := 26. definition main31 := 25. definition main30 := 24. definition main3 := 23. definition main29 := 22. definition main28 := 21. definition main27 := 20. definition main26 := 19. definition main25 := 18. definition main24 := 17. definition main23 := 16. definition main22 := 15. definition main21 := 14. definition main20 := 13. definition main2 := 12. definition main19 := 11. definition main18 := 10. definition main17 := 9. definition main16 := 8. definition main15 := 7. definition main14 := 6. definition main13 := 5. definition main12 := 4. definition main11 := 3. definition main10 := 2. definition main1 := 1. definition main0 := 0. definition C_cost9 := costlabel_of_nat 0. definition pre_main := mk_pre_internal_function (mk_signature [] (Some ? (ASTint I32 Signed))) (Some ? 2) [] [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18; 19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34; 35] [3; 6; 8; 12; 14; 18; 20; 24; 26; 30; 32] 5 [ (pair ?? main9 (make_St_op2 Omul 9 10 11 main8)); (pair ?? main8 (make_St_op2 Oaddp 6 8 9 main7)); (pair ?? main7 (make_St_const 7 (Ointconst (repr 120)) main6)); (pair ?? main6 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[6]] 7 main5)); (pair ?? main5 (make_St_const 3 (Oaddrstack (repr 0)) main4)); (pair ?? main41 (make_St_cost C_cost9 main40)); (pair ?? main40 (make_St_const 32 (Oaddrstack (repr 0)) main39)); (pair ?? main4 (make_St_const 4 (Ointconst (repr 5)) main3)); (pair ?? main39 (make_St_const 34 (Ointconst (repr 0)) main38)); (pair ?? main38 (make_St_const 35 (Ointconst (repr 1)) main37)); (pair ?? main37 (make_St_op2 Omul 33 34 35 main36)); (pair ?? main36 (make_St_op2 Oaddp 30 32 33 main35)); (pair ?? main35 (make_St_const 31 (Ointconst (repr 0)) main34)); (pair ?? main34 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[30]] 31 main33)); (pair ?? main33 (make_St_const 26 (Oaddrstack (repr 0)) main32)); (pair ?? main32 (make_St_const 28 (Ointconst (repr 1)) main31)); (pair ?? main31 (make_St_const 29 (Ointconst (repr 1)) main30)); (pair ?? main30 (make_St_op2 Omul 27 28 29 main29)); (pair ?? main3 (make_St_const 5 (Ointconst (repr 57)) main2)); (pair ?? main29 (make_St_op2 Oaddp 24 26 27 main28)); (pair ?? main28 (make_St_const 25 (Ointconst (repr 18)) main27)); (pair ?? main27 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[24]] 25 main26)); (pair ?? main26 (make_St_const 20 (Oaddrstack (repr 0)) main25)); (pair ?? main25 (make_St_const 22 (Ointconst (repr 2)) main24)); (pair ?? main24 (make_St_const 23 (Ointconst (repr 1)) main23)); (pair ?? main23 (make_St_op2 Omul 21 22 23 main22)); (pair ?? main22 (make_St_op2 Oaddp 18 20 21 main21)); (pair ?? main21 (make_St_const 19 (Ointconst (repr 23)) main20)); (pair ?? main20 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[18]] 19 main19)); (pair ?? main2 (make_St_call_id id_search [3; 4; 5] (Some ? 1) main1)); (pair ?? main19 (make_St_const 14 (Oaddrstack (repr 0)) main18)); (pair ?? main18 (make_St_const 16 (Ointconst (repr 3)) main17)); (pair ?? main17 (make_St_const 17 (Ointconst (repr 1)) main16)); (pair ?? main16 (make_St_op2 Omul 15 16 17 main15)); (pair ?? main15 (make_St_op2 Oaddp 12 14 15 main14)); (pair ?? main14 (make_St_const 13 (Ointconst (repr 57)) main13)); (pair ?? main13 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[12]] 13 main12)); (pair ?? main12 (make_St_const 8 (Oaddrstack (repr 0)) main11)); (pair ?? main11 (make_St_const 10 (Ointconst (repr 4)) main10)); (pair ?? main10 (make_St_const 11 (Ointconst (repr 1)) main9)); (pair ?? main1 (make_St_op1 Ocast8unsigned 2 1 main0)); (pair ?? main0 make_St_return) ] main41 main0. definition prog : res RTLabs_program := do f_main \larr make_internal_function pre_main; do f_search \larr make_internal_function pre_search; OK ? (mk_program ?? ( (pair ?? id_main f_main):: (pair ?? id_search f_search):: (nil ?)) id_main (*globals:*) [] ). example exec: finishes_with (repr 3) ? (do p ← prog; do r ← exec_up_to RTLabs_fullexec p 1000 [ ]; OK ? r). normalize (* you can examine the result here *) @refl qed.