@@ -45,6 +45,87 @@ Ltac t_arm_op :=
4545 rewrite ?zero_extend_u ?addn1;
4646 t_simpl_rewrites.
4747
48+ Module ARMCopnP.
49+
50+ Section WITH_PARAMS.
51+
52+ Context
53+ {wsw : WithSubWord}
54+ {dc : DirectCall}
55+ {syscall_state : Type }
56+ {sc_sem : syscall_sem syscall_state}
57+ {atoI : arch_toIdent}
58+ {pT : progT}
59+ {sCP : semCallParams}
60+ (p : prog)
61+ (evt : extra_val_t)
62+ .
63+
64+ Let mkv xname vi :=
65+ let : x := {| vname := xname; vtype := sword arm_reg_size; |} in
66+ let : xi := {| v_var := x; v_info := vi; |} in
67+ (xi, x).
68+
69+ Lemma sem_copn_equiv gd args s :
70+ ARMCopn_coreP.sem_copn_args gd args s
71+ = sem_copn_args gd (ARMCopn.to_opn args) s.
72+ Proof .
73+ rewrite /sem_copn_args /sem_sopn /exec_sopn /=.
74+ case: args => -[lvs o] es /=.
75+ case: sem_pexprs => //= ?.
76+ by case: app_sopn.
77+ Qed .
78+
79+ Lemma sem_copns_equiv gd args s :
80+ ARMCopn_coreP.sem_copns_args gd s args
81+ = sem_copns_args gd s (map ARMCopn.to_opn args).
82+ Proof .
83+ elim: args s => //= o os ih s.
84+ rewrite sem_copn_equiv.
85+ by case: sem_copn_args.
86+ Qed .
87+
88+ Lemma li_sem gd s xname vi imm :
89+ let : (xi, x) := mkv xname vi in
90+ let : lcmd := ARMCopn.li xi imm in
91+ exists vm',
92+ [/\ sem_copns_args gd s lcmd = ok (with_vm s vm')
93+ , vm' =[\ Sv.singleton x ] evm s
94+ & get_var true vm' x = ok (Vword (wrepr reg_size imm))
95+ ].
96+ Proof .
97+ have [vm' []] := ARMCopn_coreP.li_sem_copns_args gd s xname vi imm.
98+ rewrite sem_copns_equiv => h1 h2 h3.
99+ by exists vm'.
100+ Qed .
101+ Opaque ARMCopn.li.
102+
103+ Lemma load_mem_immP pre eimm xname vi imm ii tag s :
104+ let : x := {| vname := xname; vtype := sword arm_reg_size; |} in
105+ let : xi := {| v_var := x; v_info := vi; |} in
106+ let : c := [seq i_of_copn_args ii tag a | a <- pre ] in
107+ ARMCopn.load_mem_imm xi imm = (pre, eimm) ->
108+ exists vm,
109+ let : s' := with_vm s vm in
110+ [/\ sem p evt s c s'
111+ , vm =[\ Sv.singleton x ] evm s
112+ & sem_pexpr true (p_globs p) s' eimm = ok (Vword imm)
113+ ].
114+ Proof .
115+ set x := {| vname := _; |}; set xi := {| v_var := _; |}.
116+ rewrite /ARMCopn.load_mem_imm.
117+ case: is_mem_immediate => -[??]; subst pre eimm.
118+ - exists (evm s); split => //. + rewrite with_vm_same /=. by econstructor.
119+ by rewrite /= /sem_sop1 /= wrepr_signed.
120+ have [vm [hsem hvm hget]] := li_sem (p_globs p) s xname vi (wunsigned imm).
121+ exists vm; split=> //; first exact: sem_copns_args_sem.
122+ by rewrite /sem_pexpr /= /get_gvar /= hget wrepr_unsigned.
123+ Qed .
124+
125+ End WITH_PARAMS.
126+
127+ End ARMCopnP.
128+
48129Module ARMFopnP.
49130
50131Section WITH_PARAMS.
0 commit comments